-- Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean
theorem GradedAlgebra.liftι_eq (i : ℕ) (x : ⋀[R]^i M) :
    GradedAlgebra.liftι R M x = DirectSum.of (fun i => ⋀[R]^i M) i x

Proof state:
case mk.algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
r✝ : R
⊢ (DirectSum.of (fun i => ↥(⋀[R]^i M)) 0) (DirectSum.GAlgebra.toFun r✝) =
    (DirectSum.of (fun i => ↥(⋀[R]^i M)) 0) ⟨(algebraMap R (ExteriorAlgebra R M)) r✝, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
case mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
hx : x ∈ ⋀[R]^i M
⊢ (liftι R M) x = (DirectSum.of (fun i => ↥(⋀[R]^i M)) i) ⟨x, hx⟩

Tactic:
induction hx using Submodule.pow_induction_on_left' with
| algebraMap => simp_rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
| add _ _ _ _ _ ihx ihy => simp_rw [map_add, ihx, ihy, ← AddMonoidHom.map_add]; rfl
| mem_mul _ hm _ _ _ ih =>
    obtain ⟨_, rfl⟩ := hm
    simp_rw [map_mul, ih, GradedAlgebra.liftι, lift_ι_apply, GradedAlgebra.ι_apply R M,
      DirectSum.of_mul_of]
    exact DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext (add_comm _ _) rfl)

Result:
no goals

Proof state:
case mk.mem_mul.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
i✝ : ℕ
x✝ : ExteriorAlgebra R M
hx✝ : x✝ ∈ LinearMap.range (ι R) ^ i✝
ih : (liftι R M) x✝ = (DirectSum.of (fun i => ↥(⋀[R]^i M)) i✝) ⟨x✝, hx✝⟩
w✝ : M
⊢ (liftι R M) ((ι R) w✝ * x✝) = (DirectSum.of (fun i => ↥(⋀[R]^i M)) i✝.succ) ⟨(ι R) w✝ * x✝, ⋯⟩

Tactic:
simp_rw [map_mul, ih, GradedAlgebra.liftι, lift_ι_apply, GradedAlgebra.ι_apply R M,
  DirectSum.of_mul_of]

Result:
case mk.mem_mul.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
i✝ : ℕ
x✝ : ExteriorAlgebra R M
hx✝ : x✝ ∈ LinearMap.range (ι R) ^ i✝
ih : (liftι R M) x✝ = (DirectSum.of (fun i => ↥(⋀[R]^i M)) i✝) ⟨x✝, hx✝⟩
w✝ : M
⊢ (DirectSum.of (fun i => ↥(⋀[R]^i M)) (1 + i✝)) (GradedMonoid.GMul.mul ⟨(ι R) w✝, ⋯⟩ ⟨x✝, hx✝⟩) =
    (DirectSum.of (fun i => ↥(⋀[R]^i M)) i✝.succ) ⟨(ι R) w✝ * x✝, ⋯⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ↥(⋀[R]^i M)
⊢ (liftι R M) ↑x = (DirectSum.of (fun i => ↥(⋀[R]^i M)) i) x

Tactic:
obtain ⟨x, hx⟩ := x

Result:
case mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
hx : x ∈ ⋀[R]^i M
⊢ (liftι R M) ↑⟨x, hx⟩ = (DirectSum.of (fun i => ↥(⋀[R]^i M)) i) ⟨x, hx⟩

Proof state:
case mk.algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
r✝ : R
⊢ (liftι R M) ((algebraMap R (ExteriorAlgebra R M)) r✝) =
    (DirectSum.of (fun i => ↥(⋀[R]^i M)) 0) ⟨(algebraMap R (ExteriorAlgebra R M)) r✝, ⋯⟩

Tactic:
simp_rw [AlgHom.commutes, DirectSum.algebraMap_apply]

Result:
case mk.algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
r✝ : R
⊢ (DirectSum.of (fun i => ↥(⋀[R]^i M)) 0) (DirectSum.GAlgebra.toFun r✝) =
    (DirectSum.of (fun i => ↥(⋀[R]^i M)) 0) ⟨(algebraMap R (ExteriorAlgebra R M)) r✝, ⋯⟩

Proof state:
case mk.add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x x✝ y✝ : ExteriorAlgebra R M
i✝ : ℕ
hx✝ : x✝ ∈ LinearMap.range (ι R) ^ i✝
hy✝ : y✝ ∈ LinearMap.range (ι R) ^ i✝
ihx : (liftι R M) x✝ = (DirectSum.of (fun i => ↥(⋀[R]^i M)) i✝) ⟨x✝, hx✝⟩
ihy : (liftι R M) y✝ = (DirectSum.of (fun i => ↥(⋀[R]^i M)) i✝) ⟨y✝, hy✝⟩
⊢ (liftι R M) (x✝ + y✝) = (DirectSum.of (fun i => ↥(⋀[R]^i M)) i✝) ⟨x✝ + y✝, ⋯⟩

Tactic:
simp_rw [map_add, ihx, ihy, ← AddMonoidHom.map_add]

Result:
case mk.add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x x✝ y✝ : ExteriorAlgebra R M
i✝ : ℕ
hx✝ : x✝ ∈ LinearMap.range (ι R) ^ i✝
hy✝ : y✝ ∈ LinearMap.range (ι R) ^ i✝
ihx : (liftι R M) x✝ = (DirectSum.of (fun i => ↥(⋀[R]^i M)) i✝) ⟨x✝, hx✝⟩
ihy : (liftι R M) y✝ = (DirectSum.of (fun i => ↥(⋀[R]^i M)) i✝) ⟨y✝, hy✝⟩
⊢ (DirectSum.of (fun i => ↥(⋀[R]^i M)) i✝) (⟨x✝, hx✝⟩ + ⟨y✝, hy✝⟩) =
    (DirectSum.of (fun i => ↥(⋀[R]^i M)) i✝) ⟨x✝ + y✝, ⋯⟩

Proof state:
case mk.mem_mul.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
i✝ : ℕ
x✝ : ExteriorAlgebra R M
hx✝ : x✝ ∈ LinearMap.range (ι R) ^ i✝
ih : (liftι R M) x✝ = (DirectSum.of (fun i => ↥(⋀[R]^i M)) i✝) ⟨x✝, hx✝⟩
w✝ : M
⊢ (DirectSum.of (fun i => ↥(⋀[R]^i M)) (1 + i✝)) (GradedMonoid.GMul.mul ⟨(ι R) w✝, ⋯⟩ ⟨x✝, hx✝⟩) =
    (DirectSum.of (fun i => ↥(⋀[R]^i M)) i✝.succ) ⟨(ι R) w✝ * x✝, ⋯⟩

Tactic:
exact DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext (add_comm _ _) rfl)

Result:
no goals

Proof state:
case mk.mem_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x m✝ : ExteriorAlgebra R M
hm : m✝ ∈ LinearMap.range (ι R)
i✝ : ℕ
x✝ : ExteriorAlgebra R M
hx✝ : x✝ ∈ LinearMap.range (ι R) ^ i✝
ih : (liftι R M) x✝ = (DirectSum.of (fun i => ↥(⋀[R]^i M)) i✝) ⟨x✝, hx✝⟩
⊢ (liftι R M) (m✝ * x✝) = (DirectSum.of (fun i => ↥(⋀[R]^i M)) i✝.succ) ⟨m✝ * x✝, ⋯⟩

Tactic:
obtain ⟨_, rfl⟩ := hm

Result:
case mk.mem_mul.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
i✝ : ℕ
x✝ : ExteriorAlgebra R M
hx✝ : x✝ ∈ LinearMap.range (ι R) ^ i✝
ih : (liftι R M) x✝ = (DirectSum.of (fun i => ↥(⋀[R]^i M)) i✝) ⟨x✝, hx✝⟩
w✝ : M
⊢ (liftι R M) ((ι R) w✝ * x✝) = (DirectSum.of (fun i => ↥(⋀[R]^i M)) i✝.succ) ⟨(ι R) w✝ * x✝, ⋯⟩

Proof state:
case mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
hx : x ∈ ⋀[R]^i M
⊢ (liftι R M) ↑⟨x, hx⟩ = (DirectSum.of (fun i => ↥(⋀[R]^i M)) i) ⟨x, hx⟩

Tactic:
dsimp only [Subtype.coe_mk, DirectSum.lof_eq_of]

Result:
case mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
hx : x ∈ ⋀[R]^i M
⊢ (liftι R M) x = (DirectSum.of (fun i => ↥(⋀[R]^i M)) i) ⟨x, hx⟩

Proof state:
case mk.add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x x✝ y✝ : ExteriorAlgebra R M
i✝ : ℕ
hx✝ : x✝ ∈ LinearMap.range (ι R) ^ i✝
hy✝ : y✝ ∈ LinearMap.range (ι R) ^ i✝
ihx : (liftι R M) x✝ = (DirectSum.of (fun i => ↥(⋀[R]^i M)) i✝) ⟨x✝, hx✝⟩
ihy : (liftι R M) y✝ = (DirectSum.of (fun i => ↥(⋀[R]^i M)) i✝) ⟨y✝, hy✝⟩
⊢ (DirectSum.of (fun i => ↥(⋀[R]^i M)) i✝) (⟨x✝, hx✝⟩ + ⟨y✝, hy✝⟩) =
    (DirectSum.of (fun i => ↥(⋀[R]^i M)) i✝) ⟨x✝ + y✝, ⋯⟩

Tactic:
rfl

Result:
no goals