Theorem: DividedPowerAlgebra.deg_one_left_inv (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
⊢ LeftInverse (fun x => ((toTrivSqZeroExt R M) ↑x).snd) (⇑(proj' R M 1) ∘ ⇑(ι R M))
Tactic:
intro m
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
m : M
⊢ (fun x => ((toTrivSqZeroExt R M) ↑x).snd) ((⇑(proj' R M 1) ∘ ⇑(ι R M)) m) = m

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
m : M
⊢ (fun x => ((toTrivSqZeroExt R M) ↑x).snd) ((⇑(proj' R M 1) ∘ ⇑(ι R M)) m) = m
Tactic:
simp only [proj', proj, LinearMap.coe_mk, AddHom.coe_mk, ι, Function.comp_apply]
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
m : M
⊢ ((toTrivSqZeroExt R M) ↑(((DirectSum.decompose (grade R M)) (dp R 1 m)) 1)).snd = m

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
m : M
⊢ ((toTrivSqZeroExt R M) ↑(((DirectSum.decompose (grade R M)) (dp R 1 m)) 1)).snd = m
Tactic:
rw [← TrivSqZeroExt.snd_inr R m, ← ι_def]
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
m : M
⊢ ((toTrivSqZeroExt R M) ↑(((DirectSum.decompose (grade R M)) ((ι R M) (inr m).snd)) 1)).snd = (inr m).snd

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
m : M
⊢ ((toTrivSqZeroExt R M) ↑(((DirectSum.decompose (grade R M)) ((ι R M) (inr m).snd)) 1)).snd = (inr m).snd
Tactic:
apply congr_arg
State after:
case h
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
m : M
⊢ (toTrivSqZeroExt R M) ↑(((DirectSum.decompose (grade R M)) ((ι R M) (inr m).snd)) 1) = inr m

State before:
case h
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
m : M
⊢ (toTrivSqZeroExt R M) ↑(((DirectSum.decompose (grade R M)) ((ι R M) (inr m).snd)) 1) = inr m
Tactic:
rw [snd_inr, decompose_of_mem_same, toTrivSqZeroExt_ι]
State after:
case h.hx
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
m : M
⊢ (ι R M) m ∈ grade R M 1

State before:
case h.hx
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
m : M
⊢ (ι R M) m ∈ grade R M 1
Tactic:
apply ι_mem_grade_one
State after:
no goals