Perfectly Correct of lawful

theorem perfectlyCorrect_of_lawful (base : ZMod q) (βSq γ κ : Nat)    (decomp : Decomposition Φ messageRows messageDigits innerRows innerDigits)    (hMessageDecomp : IsLawfulGadgetDecomposition Φ base decomp.message)    (hInnerDecomp : IsLawfulGadgetDecomposition Φ base decomp.inner)    (hκpos : 0 < ‖(1 : Rq Φ)‖₁)    (hκle : ‖(1 : Rq Φ)‖₁ ≤ κ)    (hβ : ∀ (pp : PublicParams Φ innerRows messageRows messageDigits outerRows blocks innerDigits)            (m : Message Φ messageRows blocks) (i : Fin blocks),            ‖(generateDecomps Φ decomp pp m).message i‖₂² ≤ βSq)    (hγ : ∀ (pp : PublicParams Φ innerRows messageRows messageDigits outerRows blocks innerDigits)            (m : Message Φ messageRows blocks),            vecLInftyNorm Φ              (PolyVec.flattenBlocks (generateDecomps Φ decomp pp m).innerDecomp) ≤ γ) :    (commitmentScheme Φ (outerRows := outerRows) (blocks := blocks) base βSq γ κ      decomp).PerfectlyCorrect := by  intro pp _ m cd hmem  simp only [commitmentScheme, support_pure, Set.mem_singleton_iff] at hmem  rcases hmem with rfl  simp only [commitmentScheme, Bool.and_eq_true]  refine ⟨?_, ?_⟩  · -- the claimed message is the derived message of every block    rw [List.all_eq_true]    intro i _    rw [decide_eq_true_eq]    exact generateDecomps_derivedMessage Φ base decomp hMessageDecomp pp m i  · -- the honest opening (challenge `cᵢ = 1`) passes weak verification    have hone : ∀ (v : PolyVec (Rq Φ) (messageRows * messageDigits)),        (1 : Rq Φ) •ᵥ v = v := fun v => by funext j; simp    simp only [verify_weak, Bool.and_eq_true]    refine ⟨⟨?_, ?_⟩, ?_⟩    · rw [List.all_eq_true]      intro i _      simp only [Bool.and_eq_true, decide_eq_true_eq]      refine ⟨⟨⟨hκpos, hκle⟩, ?_⟩, ?_⟩      · rw [hone]; exact hβ pp m i      · rw [Simple.verify_eq_true_iff]        exact generateDecomps_inner_eq Φ base decomp hInnerDecomp pp m i    · rw [decide_eq_true_eq]; exact hγ pp m    · rw [Simple.verify_eq_true_iff]; rfl