revert

leanprover-community · Oct 28, 2024 · 97f5e9a · 97f5e9a
1 parent 9f9c59d
commit 97f5e9a
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean
@@ -59,7 +59,7 @@ noncomputable def quotientTensorQuotientEquiv (m : Submodule R M) (n : Submodule
       ext y
       simp only [LinearMap.compr₂_apply, LinearMap.flip_apply, mk_apply, Submodule.mkQ_apply,
         LinearMap.zero_apply, Submodule.Quotient.mk_eq_zero]
-      refine Submodule.mem_sup_right ⟨y ⊗ₜ ⟨x, hx⟩, rfl⟩) fun x hx => ?_
+      exact Submodule.mem_sup_right ⟨y ⊗ₜ ⟨x, hx⟩, rfl⟩) fun x hx => by
       ext y
       simp only [LinearMap.coe_comp, Function.comp_apply, Submodule.mkQ_apply, LinearMap.flip_apply,
         Submodule.liftQ_apply, LinearMap.compr₂_apply, mk_apply, LinearMap.zero_comp,