Theorem: DividedPowerAlgebra.ι_toTrivSqZeroExt_of_mem_grade_one (DividedPowers/DPAlgebra/Graded/GradeOne.lean)

State before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
ha : a ∈ grade R M 1
⊢ (ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a)) = a
Tactic:
suffices ⟨(ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a)), ι_mem_grade_one R _⟩ =
  (⟨a, ha⟩ : grade R M 1) by
  simpa only [sndHom_apply, Subtype.mk.injEq] using this
State after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
ha : a ∈ grade R M 1
⊢ ⟨(ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a)), ⋯⟩ = ⟨a, ha⟩

State before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
ha : a ∈ grade R M 1
⊢ ⟨(ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a)), ⋯⟩ = ⟨a, ha⟩
Tactic:
apply (linearEquivDegreeOne R M).symm.injective
State after:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
ha : a ∈ grade R M 1
⊢ (linearEquivDegreeOne R M).symm ⟨(ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a)), ⋯⟩ =
    (linearEquivDegreeOne R M).symm ⟨a, ha⟩

State before:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
ha : a ∈ grade R M 1
⊢ (linearEquivDegreeOne R M).symm ⟨(ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a)), ⋯⟩ =
    (linearEquivDegreeOne R M).symm ⟨a, ha⟩
Tactic:
rw [← LinearEquiv.invFun_eq_symm]
State after:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
ha : a ∈ grade R M 1
⊢ (linearEquivDegreeOne R M).invFun ⟨(ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a)), ⋯⟩ =
    (linearEquivDegreeOne R M).invFun ⟨a, ha⟩

State before:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
ha : a ∈ grade R M 1
⊢ (linearEquivDegreeOne R M).invFun ⟨(ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a)), ⋯⟩ =
    (linearEquivDegreeOne R M).invFun ⟨a, ha⟩
Tactic:
simp only [linearEquivDegreeOne, toTrivSqZeroExt_ι, sndHom_apply, snd_inr]
State after:
no goals

State before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
ha : a ∈ grade R M 1
this : ⟨(ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a)), ⋯⟩ = ⟨a, ha⟩
⊢ (ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a)) = a
Tactic:
simpa only [sndHom_apply, Subtype.mk.injEq] using this
State after:
no goals