Verified Opening of verify eq true

theorem verifiedOpening_of_verify_eq_true {base : ZMod q}    (hq5 : q % 8 = 5) {βSq γ κ : Nat} (hκ : κ ^ 2 < q)    {pp : PublicParams 𝓜(q, α)      innerRows messageRows messageDigits outerRows blocks innerDigits}    {u : Commitment 𝓜(q, α) outerRows}    {opening : Opening 𝓜(q, α) innerRows messageRows messageDigits blocks innerDigits}    (hverify : verify_weak 𝓜(q, α) base βSq γ κ pp u opening = true) :    VerifiedOpening 𝓜(q, α) base βSq γ κ pp u opening := by  simp only [verify_weak, Bool.and_eq_true] at hverify  obtain ⟨⟨hall, hgamma⟩, houter⟩ := hverify  refine ⟨(Simple.verify_eq_true_iff 𝓜(q, α) _ _ u ()).1 houter, by simpa using hgamma,    fun i => ?_⟩  rw [List.all_eq_true] at hall  have hb := hall i (List.mem_finRange i)  simp only [Bool.and_eq_true, decide_eq_true_eq] at hb  obtain ⟨⟨⟨hpos, hshort⟩, hscaled⟩, hinner⟩ := hb  exact ⟨isUnit_of_l1Norm_le α hq5 hpos hshort hκ, hshort, hscaled,    (Simple.verify_eq_true_iff 𝓜(q, α) _ _ _ ()).1 hinner⟩