awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : M
⊢ Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) (HAdd.hAdd (α := ℕ) 1 1) :
            ↥(⋀[R]^(HAdd.hAdd (α := ℕ) 1 1) M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^(1 + 1) M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) instAddNat _ 1 1
          (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^1 M) x)
            ((ι R : (a : M) → ExteriorAlgebra R M) m) ⋯)
          (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^1 M) x)
            ((ι R : (a : M) → ExteriorAlgebra R M) m) ⋯)) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (0 : ⨁ (i : ℕ), ↥(⋀[R]^i M))

Tactic:
DFinsupp.single_eq_zero.mpr (Subtype.ext <| ExteriorAlgebra.ι_sq_zero _)

Premises used: Iff.mpr, DFinsupp.single, ExteriorAlgebra.ι_sq_zero, DFinsupp.single_eq_zero, DirectSum, Subtype.ext
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : M
⊢ Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) (HAdd.hAdd (α := ℕ) 1 1) :
            ↥(⋀[R]^(HAdd.hAdd (α := ℕ) 1 1) M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^(1 + 1) M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) instAddNat _ 1 1
          (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^1 M) x)
            ((ι R : (a : M) → ExteriorAlgebra R M) m) ⋯)
          (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^1 M) x)
            ((ι R : (a : M) → ExteriorAlgebra R M) m) ⋯)) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (0 : ⨁ (i : ℕ), ↥(⋀[R]^i M))

Tactic:
exact DFinsupp.single_eq_zero.mpr (Subtype.ext <| ExteriorAlgebra.ι_sq_zero _)

Premises used: Iff.mpr, DFinsupp.single_eq_zero, Subtype.ext
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ M →ₗ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M)

Tactic:
apply GradedAlgebra.ι R M

Premises used: ExteriorAlgebra.GradedAlgebra.ι
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
x : ↥(⋀[R]^i M)
obtain :
  ∀ (x : ExteriorAlgebra R M) (hx : Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) x),
    Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
      ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
          (↑(Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
                Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) x) x hx) :
            ExteriorAlgebra R M) :
        ⨁ (i : ℕ), ↥(⋀[R]^i M))
      (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i : ↥(⋀[R]^i M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
            (a : ↥(⋀[R]^i M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
          (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) x) x hx) :
        ⨁ (i : ℕ), ↥(⋀[R]^i M))
⊢ Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) (↑x : ExteriorAlgebra R M) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i : ↥(⋀[R]^i M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^i M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        x :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))

Tactic:
obtain ⟨x, hx⟩ := x
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
x : ExteriorAlgebra R M
hx : Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) x
dsimp :
  Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) x : ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i : ↥(⋀[R]^i M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^i M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) x) x hx) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
⊢ Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (↑(Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
              Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) x) x hx) :
          ExteriorAlgebra R M) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i : ↥(⋀[R]^i M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^i M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) x) x hx) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))

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

Premises used: Subtype.coe_mk, DirectSum.lof_eq_of
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
x : ExteriorAlgebra R M
r : R
algebraMap :
  Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) 0 : ↥(⋀[R]^0 M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^0 M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (((@DirectSum.GAlgebra.toFun _ R (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) CommRing.toCommSemiring
                (fun (i : ℕ) ↦ Submodule.addCommMonoid (⋀[R]^i M)) (fun (i : ℕ) ↦ Submodule.module (⋀[R]^i M))
                Nat.instAddMonoid (SetLike.gsemiring fun (i : ℕ) ↦ ⋀[R]^i M) _ :
              R →+ ↥(⋀[R]^0 M)) :
            (a : R) → ↥(⋀[R]^0 M))
          r) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) 0 : ↥(⋀[R]^0 M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^0 M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^0 M) x)
          ((Algebra.algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r) ⋯) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
⊢ Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        ((Algebra.algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) 0 : ↥(⋀[R]^0 M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^0 M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^0 M) x)
          ((Algebra.algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r) ⋯) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))

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

Premises used: DirectSum.algebraMap_apply, AlgHom.commutes
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
x : ExteriorAlgebra R M
r : R
⊢ Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) 0 : ↥(⋀[R]^0 M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^0 M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (((@DirectSum.GAlgebra.toFun _ R (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) CommRing.toCommSemiring
                (fun (i : ℕ) ↦ Submodule.addCommMonoid (⋀[R]^i M)) (fun (i : ℕ) ↦ Submodule.module (⋀[R]^i M))
                Nat.instAddMonoid (SetLike.gsemiring fun (i : ℕ) ↦ ⋀[R]^i M) _ :
              R →+ ↥(⋀[R]^0 M)) :
            (a : R) → ↥(⋀[R]^0 M))
          r) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) 0 : ↥(⋀[R]^0 M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^0 M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^0 M) x)
          ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r) ⋯) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
x x_1 y : ExteriorAlgebra R M
i_1 : ℕ
hx : x_1 ∈ HPow.hPow (α := Submodule R (ExteriorAlgebra R M)) (LinearMap.range (ι R)) i_1
hy : y ∈ HPow.hPow (α := Submodule R (ExteriorAlgebra R M)) (LinearMap.range (ι R)) i_1
ihx :
  Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) x_1 : ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i_1 : ↥(⋀[R]^i_1 M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^i_1 M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i_1 M) x) x_1 hx) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
ihy :
  Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) y : ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i_1 : ↥(⋀[R]^i_1 M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^i_1 M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i_1 M) x) y hy) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
add :
  Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i_1 : ↥(⋀[R]^i_1 M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^i_1 M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i_1 M) x) x_1 hx +
          Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i_1 M) x) y hy) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i_1 : ↥(⋀[R]^i_1 M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^i_1 M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i_1 M) x) (x_1 + y) ⋯) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
⊢ Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) (x_1 + y) : ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i_1 : ↥(⋀[R]^i_1 M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^i_1 M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i_1 M) x) (x_1 + y) ⋯) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))

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

Premises used: map_add
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
x x_1 y : ExteriorAlgebra R M
i_1 : ℕ
hx : x_1 ∈ HPow.hPow (α := Submodule R (ExteriorAlgebra R M)) (LinearMap.range (ι R)) i_1
hy : y ∈ HPow.hPow (α := Submodule R (ExteriorAlgebra R M)) (LinearMap.range (ι R)) i_1
ihx :
  Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) x_1 : ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i_1 : ↥(⋀[R]^i_1 M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^i_1 M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i_1 M) x) x_1 hx) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
ihy :
  Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) y : ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i_1 : ↥(⋀[R]^i_1 M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^i_1 M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i_1 M) x) y hy) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
⊢ Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i_1 : ↥(⋀[R]^i_1 M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^i_1 M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i_1 M) x) x_1 hx +
          Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i_1 M) x) y hy) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i_1 : ↥(⋀[R]^i_1 M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^i_1 M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i_1 M) x) (x_1 + y) ⋯) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
x m : ExteriorAlgebra R M
hm : Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (LinearMap.range (ι R)) m
i_1 : ℕ
x_1 : ExteriorAlgebra R M
hx : x_1 ∈ HPow.hPow (α := Submodule R (ExteriorAlgebra R M)) (LinearMap.range (ι R)) i_1
ih :
  Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) x_1 : ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i_1 : ↥(⋀[R]^i_1 M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^i_1 M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i_1 M) x) x_1 hx) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
mem_mul :
  ∀ (w : M),
    Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
      ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
          (HMul.hMul (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) w : ExteriorAlgebra R M) x_1) :
        ⨁ (i : ℕ), ↥(⋀[R]^i M))
      (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i_1.succ : ↥(⋀[R]^i_1.succ M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
            (a : ↥(⋀[R]^i_1.succ M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
          (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i_1.succ M) x)
            (HMul.hMul (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) w : ExteriorAlgebra R M) x_1)
            ⋯) :
        ⨁ (i : ℕ), ↥(⋀[R]^i M))
⊢ Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) (m * x_1) : ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i_1.succ : ↥(⋀[R]^i_1.succ M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^i_1.succ M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i_1.succ M) x) (m * x_1) ⋯) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))

Tactic:
obtain ⟨_, rfl⟩ := hm

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
x : ExteriorAlgebra R M
i_1 : ℕ
x_1 : ExteriorAlgebra R M
hx : x_1 ∈ HPow.hPow (α := Submodule R (ExteriorAlgebra R M)) (LinearMap.range (ι R)) i_1
ih :
  Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) x_1 : ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i_1 : ↥(⋀[R]^i_1 M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^i_1 M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i_1 M) x) x_1 hx) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
w : M
mem_mul :
  Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) (1 + i_1) : ↥(⋀[R]^(1 + i_1) M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^(1 + i_1) M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) instAddNat _ 1 i_1
          (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^1 M) x)
            ((ι R : (a : M) → ExteriorAlgebra R M) w) ⋯)
          (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i_1 M) x) x_1 hx)) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i_1.succ : ↥(⋀[R]^i_1.succ M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^i_1.succ M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i_1.succ M) x)
          (HMul.hMul (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) w : ExteriorAlgebra R M) x_1)
          ⋯) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
⊢ Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (HMul.hMul (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) w : ExteriorAlgebra R M) x_1) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i_1.succ : ↥(⋀[R]^i_1.succ M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^i_1.succ M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i_1.succ M) x)
          (HMul.hMul (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) w : ExteriorAlgebra R M) x_1)
          ⋯) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))

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

Premises used: ExteriorAlgebra.lift_ι_apply, DirectSum.of_mul_of, map_mul, ExteriorAlgebra.GradedAlgebra.ι_apply, ExteriorAlgebra.GradedAlgebra.liftι
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
x : ExteriorAlgebra R M
i_1 : ℕ
x_1 : ExteriorAlgebra R M
hx : x_1 ∈ HPow.hPow (α := Submodule R (ExteriorAlgebra R M)) (LinearMap.range (ι R)) i_1
ih :
  Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) x_1 : ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i_1 : ↥(⋀[R]^i_1 M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^i_1 M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i_1 M) x) x_1 hx) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
w : M
⊢ Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) (1 + i_1) : ↥(⋀[R]^(1 + i_1) M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^(1 + i_1) M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) instAddNat _ 1 i_1
          (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^1 M) x)
            ((ι R : (a : M) → ExteriorAlgebra R M) w) ⋯)
          (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i_1 M) x) x_1 hx)) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i_1.succ : ↥(⋀[R]^i_1.succ M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^i_1.succ M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i_1.succ M) x)
          (HMul.hMul (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) w : ExteriorAlgebra R M) x_1)
          ⋯) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))

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

Premises used: Sigma.subtype_ext, add_comm, DirectSum.of_eq_of_gradedMonoid_eq, rfl
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
x : ExteriorAlgebra R M
i_1 : ℕ
x_1 : ExteriorAlgebra R M
hx : x_1 ∈ HPow.hPow (α := Submodule R (ExteriorAlgebra R M)) (LinearMap.range (ι R)) i_1
ih :
  Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) x_1 : ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i_1 : ↥(⋀[R]^i_1 M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^i_1 M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i_1 M) x) x_1 hx) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
w : M
⊢ Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) (1 + i_1) : ↥(⋀[R]^(1 + i_1) M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^(1 + i_1) M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) instAddNat _ 1 i_1
          (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^1 M) x)
            ((ι R : (a : M) → ExteriorAlgebra R M) w) ⋯)
          (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i_1 M) x) x_1 hx)) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i_1.succ : ↥(⋀[R]^i_1.succ M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^i_1.succ M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i_1.succ M) x)
          (HMul.hMul (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) w : ExteriorAlgebra R M) x_1)
          ⋯) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))

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

Premises used: Sigma.subtype_ext, add_comm, DirectSum.of_eq_of_gradedMonoid_eq, rfl
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ ExteriorAlgebra R M →ₐ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M)

Tactic:
apply GradedAlgebra.liftι R M

Premises used: ExteriorAlgebra.GradedAlgebra.liftι
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
a :
  ∀ (m : M),
    Eq (α := ExteriorAlgebra R M)
      ((AlgHom.toLinearMap (AlgHom.comp (DirectSum.coeAlgHom fun (i : ℕ) ↦ ⋀[R]^i M) (GradedAlgebra.liftι R M)) ∘ₗ
              CliffordAlgebra.ι 0 :
            (a : M) → ExteriorAlgebra R M)
          m :
        ExteriorAlgebra R M)
      ((AlgHom.toLinearMap (AlgHom.id R (ExteriorAlgebra R M)) ∘ₗ CliffordAlgebra.ι 0 : (a : M) → ExteriorAlgebra R M)
          m :
        ExteriorAlgebra R M)
⊢ Eq (α := ExteriorAlgebra R M →ₐ[R] ExteriorAlgebra R M)
    (AlgHom.comp (DirectSum.coeAlgHom fun (i : ℕ) ↦ ⋀[R]^i M) (GradedAlgebra.liftι R M))
    (AlgHom.id R (ExteriorAlgebra R M))

Tactic:
ext m
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ ∀ (i : ℕ) (x : ↥(⋀[R]^i M)),
    Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
      ((GradedAlgebra.liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) (↑x : ExteriorAlgebra R M) :
        ⨁ (i : ℕ), ↥(⋀[R]^i M))
      (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) i : ↥(⋀[R]^i M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
            (a : ↥(⋀[R]^i M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
          x :
        ⨁ (i : ℕ), ↥(⋀[R]^i M))

Tactic:
apply GradedAlgebra.liftι_eq R M

Premises used: ExteriorAlgebra.GradedAlgebra.liftι_eq