[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ ↑(ι R) m ∈ LinearMap.range (ι R) ^ 1
[PROOFSTEP]
simpa only [pow_one] using LinearMap.mem_range_self _ m
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ ↑(ι R) m ∈ LinearMap.range (ι R) ^ 1
[PROOFSTEP]
simpa only [pow_one] using LinearMap.mem_range_self _ m
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ ↑(GradedAlgebra.ι R M) m * ↑(GradedAlgebra.ι R M) m = 0
[PROOFSTEP]
rw [GradedAlgebra.ι_apply, DirectSum.of_mul_of]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) (1 + 1))
      (GradedMonoid.GMul.mul { val := ↑(ι R) m, property := (_ : ↑(ι R) m ∈ LinearMap.range (ι R) ^ 1) }
        { val := ↑(ι R) m, property := (_ : ↑(ι R) m ∈ LinearMap.range (ι R) ^ 1) }) =
    0
[PROOFSTEP]
refine DFinsupp.single_eq_zero.mpr (Subtype.ext <| ExteriorAlgebra.ι_sq_zero _)
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ M →ₗ[R] ⨁ (i : ℕ), { x // x ∈ LinearMap.range (ι R) ^ i }
[PROOFSTEP]
apply GradedAlgebra.ι R M
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : { x // x ∈ LinearMap.range (ι R) ^ i }
⊢ ↑(liftι R M) ↑x = ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i) x
[PROOFSTEP]
cases' x with x hx
[GOAL]
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 ∈ LinearMap.range (ι R) ^ i
⊢ ↑(liftι R M) ↑{ val := x, property := hx } =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i) { val := x, property := hx }
[PROOFSTEP]
dsimp only [Subtype.coe_mk, DirectSum.lof_eq_of]
  -- Porting note: original statement was
    --  refine Submodule.pow_induction_on_left' _ (fun r => ?_) (fun x y i hx hy ihx ihy => ?_)
    --    (fun m hm i x hx ih => ?_) hx
    -- but it created invalid goals
[GOAL]
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 ∈ LinearMap.range (ι R) ^ i
⊢ ↑(liftι R M) x = ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i) { val := x, property := hx }
[PROOFSTEP]
induction hx using Submodule.pow_induction_on_left' with
| hr => simp_rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
| hadd _ _ _ _ _ ihx ihy => simp_rw [AlgHom.map_add, ihx, ihy, ← map_add]; rfl
| hmul _ hm _ _ _ ih =>
  obtain ⟨_, rfl⟩ := hm
  simp_rw [AlgHom.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)
[GOAL]
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 ∈ LinearMap.range (ι R) ^ i
⊢ ↑(liftι R M) x = ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i) { val := x, property := hx }
[PROOFSTEP]
induction hx using Submodule.pow_induction_on_left' with
| hr => simp_rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
| hadd _ _ _ _ _ ihx ihy => simp_rw [AlgHom.map_add, ihx, ihy, ← map_add]; rfl
| hmul _ hm _ _ _ ih =>
  obtain ⟨_, rfl⟩ := hm
  simp_rw [AlgHom.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)
[GOAL]
case mk.hr
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 => { x // x ∈ LinearMap.range (ι R) ^ i }) 0)
      { val := ↑(algebraMap R (ExteriorAlgebra R M)) r✝,
        property := (_ : ↑(algebraMap R (ExteriorAlgebra R M)) r✝ ∈ 1) }
[PROOFSTEP]

| hr => simp_rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
[GOAL]
case mk.hr
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 => { x // x ∈ LinearMap.range (ι R) ^ i }) 0)
      { val := ↑(algebraMap R (ExteriorAlgebra R M)) r✝,
        property := (_ : ↑(algebraMap R (ExteriorAlgebra R M)) r✝ ∈ 1) }
[PROOFSTEP]
simp_rw [AlgHom.commutes, DirectSum.algebraMap_apply]
[GOAL]
case mk.hr
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 => { x // x ∈ LinearMap.range (ι R) ^ i }) 0) (↑DirectSum.GAlgebra.toFun r✝) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) 0)
      { val := ↑(algebraMap R (ExteriorAlgebra R M)) r✝,
        property := (_ : ↑(algebraMap R (ExteriorAlgebra R M)) r✝ ∈ 1) }
[PROOFSTEP]
rfl
[GOAL]
case mk.hadd
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 => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝) { val := x✝, property := hx✝ }
ihy :
  ↑(liftι R M) y✝ = ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝) { val := y✝, property := hy✝ }
⊢ ↑(liftι R M) (x✝ + y✝) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝)
      { val := x✝ + y✝, property := (_ : x✝ + y✝ ∈ LinearMap.range (ι R) ^ i✝) }
[PROOFSTEP]

| hadd _ _ _ _ _ ihx ihy => simp_rw [AlgHom.map_add, ihx, ihy, ← map_add]; rfl
[GOAL]
case mk.hadd
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 => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝) { val := x✝, property := hx✝ }
ihy :
  ↑(liftι R M) y✝ = ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝) { val := y✝, property := hy✝ }
⊢ ↑(liftι R M) (x✝ + y✝) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝)
      { val := x✝ + y✝, property := (_ : x✝ + y✝ ∈ LinearMap.range (ι R) ^ i✝) }
[PROOFSTEP]
simp_rw [AlgHom.map_add, ihx, ihy, ← map_add]
[GOAL]
case mk.hadd
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 => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝) { val := x✝, property := hx✝ }
ihy :
  ↑(liftι R M) y✝ = ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝) { val := y✝, property := hy✝ }
⊢ ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝)
      ({ val := x✝, property := hx✝ } + { val := y✝, property := hy✝ }) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝)
      { val := x✝ + y✝, property := (_ : x✝ + y✝ ∈ LinearMap.range (ι R) ^ i✝) }
[PROOFSTEP]
rfl
[GOAL]
case mk.hmul
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 => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝) { val := x✝, property := hx✝ }
⊢ ↑(liftι R M) (m✝ * x✝) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) (Nat.succ i✝))
      { val := m✝ * x✝, property := (_ : m✝ * x✝ ∈ LinearMap.range (ι R) * npowRec i✝ (LinearMap.range (ι R))) }
[PROOFSTEP]

| hmul _ hm _ _ _ ih =>
  obtain ⟨_, rfl⟩ := hm
  simp_rw [AlgHom.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)
[GOAL]
case mk.hmul
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 => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝) { val := x✝, property := hx✝ }
⊢ ↑(liftι R M) (m✝ * x✝) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) (Nat.succ i✝))
      { val := m✝ * x✝, property := (_ : m✝ * x✝ ∈ LinearMap.range (ι R) * npowRec i✝ (LinearMap.range (ι R))) }
[PROOFSTEP]
obtain ⟨_, rfl⟩ := hm
[GOAL]
case mk.hmul.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 => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝) { val := x✝, property := hx✝ }
w✝ : M
⊢ ↑(liftι R M) (↑(ι R) w✝ * x✝) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) (Nat.succ i✝))
      { val := ↑(ι R) w✝ * x✝,
        property := (_ : ↑(ι R) w✝ * x✝ ∈ LinearMap.range (ι R) * npowRec i✝ (LinearMap.range (ι R))) }
[PROOFSTEP]
simp_rw [AlgHom.map_mul, ih, GradedAlgebra.liftι, lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.of_mul_of]
[GOAL]
case mk.hmul.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 => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝) { val := x✝, property := hx✝ }
w✝ : M
⊢ ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) (1 + i✝))
      (GradedMonoid.GMul.mul { val := ↑(ι R) w✝, property := (_ : ↑(ι R) w✝ ∈ LinearMap.range (ι R) ^ 1) }
        { val := x✝, property := hx✝ }) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) (Nat.succ i✝))
      { val := ↑(ι R) w✝ * x✝,
        property := (_ : ↑(ι R) w✝ * x✝ ∈ LinearMap.range (ι R) * npowRec i✝ (LinearMap.range (ι R))) }
[PROOFSTEP]
exact DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext (add_comm _ _) rfl)
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ExteriorAlgebra R M →ₐ[R] ⨁ (i : ℕ), { x // x ∈ LinearMap.range (ι R) ^ i }
[PROOFSTEP]
apply GradedAlgebra.liftι R M
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ AlgHom.comp (DirectSum.coeAlgHom fun x => LinearMap.range (ι R) ^ x) (GradedAlgebra.liftι R M) =
    AlgHom.id R (ExteriorAlgebra R M)
[PROOFSTEP]
ext m
[GOAL]
case a.h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ ↑(LinearMap.comp
          (AlgHom.toLinearMap
            (AlgHom.comp (DirectSum.coeAlgHom fun x => LinearMap.range (ι R) ^ x) (GradedAlgebra.liftι R M)))
          (CliffordAlgebra.ι 0))
      m =
    ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (ExteriorAlgebra R M))) (CliffordAlgebra.ι 0)) m
[PROOFSTEP]
dsimp only [LinearMap.comp_apply, AlgHom.toLinearMap_apply, AlgHom.comp_apply, AlgHom.id_apply, GradedAlgebra.liftι]
[GOAL]
case a.h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ ↑(DirectSum.coeAlgHom fun x => LinearMap.range (ι R) ^ x)
      (↑(↑(lift R)
            { val := GradedAlgebra.ι R M,
              property := (_ : ∀ (m : M), ↑(GradedAlgebra.ι R M) m * ↑(GradedAlgebra.ι R M) m = 0) })
        (↑(CliffordAlgebra.ι 0) m)) =
    ↑(CliffordAlgebra.ι 0) m
[PROOFSTEP]
rw [lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.coeAlgHom_of, Subtype.coe_mk]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ∀ (i : ℕ) (x : { x // x ∈ LinearMap.range (ι R) ^ i }),
    ↑(GradedAlgebra.liftι R M) ↑x = ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i) x
[PROOFSTEP]
apply GradedAlgebra.liftι_eq R M
