Split Data fst is Structured

theorem SplitData.fst_isStructured :    {r : Fin (m + 1)} → (S : SplitData S₁.arity S₂.arity r) →    S.src.IsStructured (S₁.append S₂) → S.fst.IsStructured S₁  | _, .boundary _, _ => trivial  | _, .msg i h m₁ child, hS => by      have hround : (Fin.castAdd n i).succ = leftRound i.succ := by        apply Fin.ext        rfl      simp only [SplitData.src, ChallengeTree.IsStructured] at hS      apply SplitData.fst_isStructured child      convert hS using 1      · exact hround.symm      · rfl  | _, .chal i h chals children, hS => by      have hApp : (pSpec₁ ++ₚ pSpec₂).dir (Fin.castAdd n i) = .V_to_P := by        simpa [ProtocolSpec.append, Fin.vappend_eq_append, Fin.append_left] using h      have hIdx : (⟨Fin.castAdd n i, hApp⟩ : (pSpec₁ ++ₚ pSpec₂).ChallengeIdx)          = ChallengeIdx.inl ⟨i, h⟩ := by ext; rfl      have hAr : appendArity S₁.arity S₂.arity ⟨Fin.castAdd n i, hApp⟩ = S₁.arity ⟨i, h⟩ := by        rw [hIdx]; simpa [appendArity] using          congrArg (Sum.elim S₁.arity S₂.arity)            (ChallengeIdx.sumEquiv_symm_inl (pSpec₂ := pSpec₂) ⟨i, h⟩)      have hS' := hS      simp only [SplitData.src, ChallengeTree.IsStructured] at hS'      refine ⟨?_, fun j => SplitData.fst_isStructured (children j) (hS'.2 (Fin.cast hAr.symm j))⟩      have hsymm : ∀ (P : (pSpec₁ ++ₚ pSpec₂).dir (Fin.castAdd n i) = .V_to_P),          ChallengeIdx.sumEquiv.symm (⟨Fin.castAdd n i, P⟩ : (pSpec₁ ++ₚ pSpec₂).ChallengeIdx)            = Sum.inl ⟨i, h⟩ := fun P => by        rw [show (⟨Fin.castAdd n i, P⟩ : (pSpec₁ ++ₚ pSpec₂).ChallengeIdx) = ChallengeIdx.inl ⟨i, h⟩          from by ext; rfl, ChallengeIdx.sumEquiv_symm_inl]      have hS1 := hS'.1      simp only [ChallengeTreeShape.append] at hS1      split at hS1      · rename_i i₁ heqs        obtain rfl : i₁ = ⟨i, h⟩ := Sum.inl.inj (heqs.symm.trans (hsymm _))        convert hS1 using 2        simp [cast_cast]      · rename_i i₂ heqs; exact absurd (heqs.symm.trans (hsymm _)) (by simp)