Binding Advantage le module SIS of short Closure

theorem bindingAdvantage_le_moduleSIS_of_shortClosure {rows cols : Nat}    [SampleableType (PublicParams Φ rows cols)]    [DecidableEq (Message Φ cols)] [DecidableEq (Commitment Φ rows)]    (isShort : Message Φ cols → Bool) (isShortSIS : ModuleSIS.Solution Φ cols → Bool)    (hsub : ∀ s₁ s₂ : Message Φ cols, isShort s₁ = true → isShort s₂ = true →      isShortSIS (s₁ - s₂) = true)    (adv : BindingAdv (PublicParams Φ rows cols) (Message Φ cols) (Commitment Φ rows) Opening) :    bindingAdvantage (commitmentScheme Φ rows cols isShort) adv ≤      ModuleSIS.advantage Φ rows cols isShortSIS (bindingAdvToModuleSIS Φ isShortSIS adv) := by  unfold bindingAdvantage CommitmentScheme.bindingExp ModuleSIS.advantage    SIS.advantage SIS.experiment ModuleSIS.problem bindingAdvToModuleSIS    commitmentScheme ModuleSIS.relation  simp only [bind_pure_comp, Functor.map_map]  refine probOutput_bind_mono fun A _ => ?_  refine probOutput_bind_mono fun ⟨c, s₁, o₁, s₂, o₂⟩ _ => ?_  refine probOutput_pure_bool_le _ _ (fun hwin => ?_)  simp only [Bool.and_eq_true, decide_eq_true_eq] at hwin ⊢  obtain ⟨⟨hne, hshort₁, hverify₁⟩, hshort₂, hverify₂⟩ := hwin  have hc₁ : commit Φ A s₁ = c := (verify_eq_true_iff Φ A s₁ c o₁).1 hverify₁  have hc₂ : commit Φ A s₂ = c := (verify_eq_true_iff Φ A s₂ c o₂).1 hverify₂  have hmat : A *ᵥ s₁ = A *ᵥ s₂ := by simpa [commit] using hc₁.trans hc₂.symm  refine ⟨⟨sub_ne_zero.mpr hne, hsub s₁ s₂ hshort₁ hshort₂⟩, ?_⟩  rw [matVecMul_sub, hmat, sub_self]