Inner commit eq of flatten eq

theorem inner_commit_eq_of_flatten_eq {base : ZMod q} {βSq γ κ : Nat}    {pp : PublicParams Φ innerRows messageRows messageDigits outerRows blocks innerDigits}    {u : Commitment Φ outerRows}    {opening₁ opening₂ : Opening Φ innerRows messageRows messageDigits blocks innerDigits}    (hv₁ : VerifiedOpening Φ base βSq γ κ pp u opening₁)    (hv₂ : VerifiedOpening Φ base βSq γ κ pp u opening₂)    (hflat : PolyVec.flattenBlocks opening₁.innerDecomp =      PolyVec.flattenBlocks opening₂.innerDecomp)    (i : Fin blocks) :    Simple.commit Φ pp.innerMatrix (opening₁.message i) =      Simple.commit Φ pp.innerMatrix (opening₂.message i) := by  have hblock : opening₁.innerDecomp i = opening₂.innerDecomp i :=    PolyVec.block_eq_of_flattenBlocks_eq hflat i  calc Simple.commit Φ pp.innerMatrix (opening₁.message i)      = Simple.commit Φ (gadgetMatrix Φ base innerRows innerDigits) (opening₁.innerDecomp i) :=        (hv₁.block i).inner_eq.symm    _ = Simple.commit Φ (gadgetMatrix Φ base innerRows innerDigits) (opening₂.innerDecomp i) := by        rw [hblock]    _ = Simple.commit Φ pp.innerMatrix (opening₂.message i) := (hv₂.block i).inner_eq