Get Putative Batch Root With Hash unique

theorem getPutativeBatchRootWithHash_unique    (hashFn : α → α → α) (hinj : Function.Injective2 hashFn)    {s : Skeleton} {sel : LeafData Bool s}    (v₁ v₂ : SelectedValues α sel) (p₁ p₂ : BatchProof α sel)    (heq : getPutativeBatchRootWithHash hashFn v₁ p₁         = getPutativeBatchRootWithHash hashFn v₂ p₂) :    v₁ = v₂ ∧ p₁ = p₂ := by  induction p₁ with  | leaf =>    cases p₂ with    | leaf => exact ⟨heq, rfl⟩  | internalBoth pl₁ pr₁ ihl ihr =>    cases p₂ with    | internalBoth pl₂ pr₂ =>      simp only [getPutativeBatchRootWithHash] at heq      obtain ⟨hL, hR⟩ := hinj heq      obtain ⟨hvl, hpl⟩ := ihl v₁.1 v₂.1 pl₂ hL      obtain ⟨hvr, hpr⟩ := ihr v₁.2 v₂.2 pr₂ hR      exact ⟨Prod.ext hvl hvr, by rw [hpl, hpr]⟩    | pruneRight hr₂ rightRoot₂ pl₂ =>      exact absurd (BatchProof.anySelected_of_batchProof pr₁) (by simp [hr₂])    | pruneLeft hl₂ leftRoot₂ pr₂ =>      exact absurd (BatchProof.anySelected_of_batchProof pl₁) (by simp [hl₂])  | pruneRight hr₁ rightRoot₁ pl₁ ih =>    cases p₂ with    | internalBoth pl₂ pr₂ =>      exact absurd (BatchProof.anySelected_of_batchProof pr₂) (by simp [hr₁])    | pruneRight hr₂ rightRoot₂ pl₂ =>      simp only [getPutativeBatchRootWithHash] at heq      obtain ⟨hL, hRoot⟩ := hinj heq      obtain ⟨hvl, hpl⟩ := ih v₁.1 v₂.1 pl₂ hL      refine ⟨Prod.ext hvl (selectedValues_eq_of_not_anySelected hr₁ v₁.2 v₂.2), ?_⟩      rw [hpl, hRoot]    | pruneLeft hl₂ leftRoot₂ pr₂ =>      exact absurd (BatchProof.anySelected_of_batchProof pr₂) (by simp [hr₁])  | pruneLeft hl₁ leftRoot₁ pr₁ ih =>    cases p₂ with    | internalBoth pl₂ pr₂ =>      exact absurd (BatchProof.anySelected_of_batchProof pl₂) (by simp [hl₁])    | pruneRight hr₂ rightRoot₂ pl₂ =>      exact absurd (BatchProof.anySelected_of_batchProof pl₂) (by simp [hl₁])    | pruneLeft hl₂ leftRoot₂ pr₂ =>      simp only [getPutativeBatchRootWithHash] at heq      obtain ⟨hRoot, hR⟩ := hinj heq      obtain ⟨hvr, hpr⟩ := ih v₁.2 v₂.2 pr₂ hR      refine ⟨Prod.ext (selectedValues_eq_of_not_anySelected hl₁ v₁.1 v₂.1) hvr, ?_⟩      rw [hpr, hRoot]