case refine'_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
⊢ x = 0 ∧ r = 0

case refine'_2
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
⊢ x = 0 ∧ r = 0 → ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
⊢ ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r ↔ x = 0 ∧ r = 0
refine' ⟨fun h => _, _⟩
case refine'_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
this : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
⊢ x = 0 ∧ r = 0
case refine'_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
⊢ x = 0 ∧ r = 0
letI : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)
case refine'_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
this✝ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this : IsCentralScalar R M
⊢ x = 0 ∧ r = 0
case refine'_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
this : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
⊢ x = 0 ∧ r = 0
haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
case refine'_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
this✝ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this : IsCentralScalar R M
hf0 : ↑toTrivSqZeroExt (↑(ι R) x) = (0, x)
⊢ x = 0 ∧ r = 0
case refine'_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
this✝ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this : IsCentralScalar R M
⊢ x = 0 ∧ r = 0
have hf0 : toTrivSqZeroExt (ι R x) = (0, x) := lift_ι_apply _ _
case refine'_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
this✝ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this : IsCentralScalar R M
hf0 : ↑(algebraMap R (TrivSqZeroExt R M)) r = (0, x)
⊢ x = 0 ∧ r = 0
case refine'_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
this✝ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this : IsCentralScalar R M
hf0 : ↑toTrivSqZeroExt (↑(ι R) x) = (0, x)
⊢ x = 0 ∧ r = 0
rw [h, AlgHom.commutes] at hf0
case refine'_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
this✝¹ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this✝ : IsCentralScalar R M
hf0 : ↑(algebraMap R (TrivSqZeroExt R M)) r = (0, x)
this : r = 0 ∧ 0 = x
⊢ x = 0 ∧ r = 0
case refine'_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
this✝ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this : IsCentralScalar R M
hf0 : ↑(algebraMap R (TrivSqZeroExt R M)) r = (0, x)
⊢ x = 0 ∧ r = 0
have : r = 0 ∧ 0 = x := Prod.ext_iff.1 hf0
no goals
case refine'_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
this✝¹ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this✝ : IsCentralScalar R M
hf0 : ↑(algebraMap R (TrivSqZeroExt R M)) r = (0, x)
this : r = 0 ∧ 0 = x
⊢ x = 0 ∧ r = 0
exact this.symm.imp_left Eq.symm
case refine'_2.intro
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ↑(ι R) 0 = ↑(algebraMap R (TensorAlgebra R M)) 0
case refine'_2
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
⊢ x = 0 ∧ r = 0 → ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
rintro ⟨rfl, rfl⟩
no goals
case refine'_2.intro
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ↑(ι R) 0 = ↑(algebraMap R (TensorAlgebra R M)) 0
rw [LinearMap.map_zero, RingHom.map_zero]