Theorem: DividedPowerAlgebra.mem_grade_one_iff (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
⊢ a ∈ grade R M 1 ↔ ∃ m, a = (ι R M) m
Tactic:
constructor
State after:
case mp
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
⊢ a ∈ grade R M 1 → ∃ m, a = (ι R M) m

case mpr
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
⊢ (∃ m, a = (ι R M) m) → a ∈ grade R M 1

State before:
case mp
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
⊢ a ∈ grade R M 1 → ∃ m, a = (ι R M) m

case mpr
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
⊢ (∃ m, a = (ι R M) m) → a ∈ grade R M 1
Tactic:
. intro ha
  use ((sndHom R M) ((toTrivSqZeroExt R M) a))
  rw [ι_toTrivSqZeroExt_of_mem_grade_one R M ha]
State after:
case mpr
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
⊢ (∃ m, a = (ι R M) m) → a ∈ grade R M 1

State before:
case mpr
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
⊢ (∃ m, a = (ι R M) m) → a ∈ grade R M 1
Tactic:
. rintro ⟨m, rfl⟩
  apply ι_mem_grade_one
State after:
no goals

State before:
case mp
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
⊢ a ∈ grade R M 1 → ∃ m, a = (ι R M) m
Tactic:
intro ha
State after:
case mp
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
⊢ ∃ m, a = (ι R M) m

State before:
case mp
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
⊢ ∃ m, a = (ι R M) m
Tactic:
use ((sndHom R M) ((toTrivSqZeroExt R M) a))
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
a : DividedPowerAlgebra R M
ha : a ∈ grade R M 1
⊢ a = (ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a))

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
a : DividedPowerAlgebra R M
ha : a ∈ grade R M 1
⊢ a = (ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a))
Tactic:
rw [ι_toTrivSqZeroExt_of_mem_grade_one R M ha]
State after:
no goals

State before:
case mpr
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
⊢ (∃ m, a = (ι R M) m) → a ∈ grade R M 1
Tactic:
rintro ⟨m, rfl⟩
State after:
case mpr.intro
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 mpr.intro
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