awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
⊢ Function.Surjective (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R N)
      (⇑(map f) : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N) ↔
    Function.Surjective.{u2 + 1, u4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
have refine : ∀
  (h :
    Function.Surjective (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R N)
      (⇑(map f) : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N))
  (y : N), ∃ (a : M), (f : (a : M) → N) a = y
Tactic: refine ⟨fun h y ↦ ?_, fun h ↦ CliffordAlgebra.map_surjective _ h⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R N)
    (⇑(map f) : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N)
y : N
⊢ ∃ (a : M), (f : (a : M) → N) a = y
have obtain : ∀ (x : ExteriorAlgebra R M)
  (hx :
    Eq (α := ExteriorAlgebra R N) ((map f : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N) x : ExteriorAlgebra R N)
      ((ι R : (a : N) → ExteriorAlgebra R N) y : ExteriorAlgebra R N)),
  ∃ (a : M), (f : (a : M) → N) a = y
Tactic: obtain ⟨x, hx⟩ := h (ι R y)
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R N)
    (⇑(map f) : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N)
y : N
x : ExteriorAlgebra R M
hx :
  Eq (α := ExteriorAlgebra R N) ((map f : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N) x : ExteriorAlgebra R N)
    ((ι R : (a : N) → ExteriorAlgebra R N) y : ExteriorAlgebra R N)
⊢ ∃ (a : M), (f : (a : M) → N) a = y
have existsi : (f : (a : M) → N) ((ιInv : (a : ExteriorAlgebra R M) → M) x : M) = y
Tactic: existsi ιInv x
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R N)
    (⇑(map f) : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N)
y : N
x : ExteriorAlgebra R M
hx :
  Eq (α := ExteriorAlgebra R N) ((map f : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N) x : ExteriorAlgebra R N)
    ((ι R : (a : N) → ExteriorAlgebra R N) y : ExteriorAlgebra R N)
⊢ (f : (a : M) → N) ((ιInv : (a : ExteriorAlgebra R M) → M) x : M) = y
have rw : (ιInv : (a : ExteriorAlgebra R N) → N)
    (((map f).toLinearMap : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N) x : ExteriorAlgebra R N) =
  y
Tactic: rw [← LinearMap.comp_apply, ← ιInv_comp_map, LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basis (goal)
Goal:
R : Type u_1
M : Type u_2
n : ℕ
I : Type u_3
inst : LinearOrder I
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
b : Basis I R M
s : Finset I
s_card : s.card = n
⊢ Eq (α := ExteriorAlgebra R M) ((b.ExteriorAlgebra : (a : Finset I) → ExteriorAlgebra R M) s : ExteriorAlgebra R M)
    (ιMulti_family R n (⇑b : (a : I) → M) (ofCard s_card) : ExteriorAlgebra R M)
have subst : Eq (α := ExteriorAlgebra R M) ((b.ExteriorAlgebra : (a : Finset I) → ExteriorAlgebra R M) s : ExteriorAlgebra R M)
  (ιMulti_family R s.card (⇑b : (a : I) → M) (ofCard sorry) : ExteriorAlgebra R M)
Tactic: subst s_card
Cleared hypotheses: n, s_card
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basis (goal)
Goal:
R : Type u_1
M : Type u_2
m : ℕ
I : Type u_3
inst : LinearOrder I
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
b : Basis I R M
s : (↑(powersetCard I m) : Type u_3)
⊢ Eq (α := ExteriorAlgebra R M)
    ((b.ExteriorAlgebra : (a : Finset I) → ExteriorAlgebra R M) (↑s : Finset I) : ExteriorAlgebra R M)
    ((↑((Basis.exteriorPower m b : (a : (↑(powersetCard I m) : Type u_3)) → ↥(⋀[R]^m M)) s) : ExteriorAlgebra R M) :
      ExteriorAlgebra R M)
have rw : Eq (α := ExteriorAlgebra R M) (ιMulti_family R m (⇑b : (a : I) → M) s)
  (↑((Basis.exteriorPower m b : (a : (↑(powersetCard I m) : Type u_3)) → ↥(⋀[R]^m M)) s) : ExteriorAlgebra R M)
Tactic: rw [basis_apply_powersetCard, exteriorPower.basis_apply, ιMulti_family_apply_coe]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basis (goal)
Goal:
R : Type u_1
M : Type u_2
m : ℕ
I : Type u_3
inst : LinearOrder I
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
b : Basis I R M
s : (↑(powersetCard I m) : Type u_3)
rw :
  Eq (α := ExteriorAlgebra R M) (ιMulti_family R m (⇑b : (a : I) → M) s)
    (↑((Basis.exteriorPower m b : (a : (↑(powersetCard I m) : Type u_3)) → ↥(⋀[R]^m M)) s) : ExteriorAlgebra R M)
⊢ Eq (α := ExteriorAlgebra R M)
    ((b.ExteriorAlgebra : (a : Finset I) → ExteriorAlgebra R M) (↑s : Finset I) : ExteriorAlgebra R M)
    ((↑((Basis.exteriorPower m b : (a : (↑(powersetCard I m) : Type u_3)) → ↥(⋀[R]^m M)) s) : ExteriorAlgebra R M) :
      ExteriorAlgebra R M)
have rw₁ : Eq (α := ExteriorAlgebra R M) (ιMulti_family R m (⇑b : (a : I) → M) s)
  (↑(exteriorPower.ιMulti_family R m (⇑b : (a : I) → M) s) : ExteriorAlgebra R M)
Tactic: rw [basis_apply_powersetCard, exteriorPower.basis_apply, ιMulti_family_apply_coe]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basis (goal)
Goal:
R : Type u_1
M : Type u_2
m : ℕ
I : Type u_3
inst : LinearOrder I
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
b : Basis I R M
s : (↑(powersetCard I m) : Type u_3)
rw :
  Eq (α := ExteriorAlgebra R M) (ιMulti_family R m (⇑b : (a : I) → M) s)
    (↑((Basis.exteriorPower m b : (a : (↑(powersetCard I m) : Type u_3)) → ↥(⋀[R]^m M)) s) : ExteriorAlgebra R M)
rw₁ :
  Eq (α := ExteriorAlgebra R M) (ιMulti_family R m (⇑b : (a : I) → M) s)
    (↑(exteriorPower.ιMulti_family R m (⇑b : (a : I) → M) s) : ExteriorAlgebra R M)
⊢ Eq (α := ExteriorAlgebra R M)
    ((b.ExteriorAlgebra : (a : Finset I) → ExteriorAlgebra R M) (↑s : Finset I) : ExteriorAlgebra R M)
    ((↑((Basis.exteriorPower m b : (a : (↑(powersetCard I m) : Type u_3)) → ↥(⋀[R]^m M)) s) : ExteriorAlgebra R M) :
      ExteriorAlgebra R M)
have rw₂ : Eq (α := ExteriorAlgebra R M) (ιMulti_family R m (⇑b : (a : I) → M) s) (ιMulti_family R m (⇑b : (a : I) → M) s)
Tactic: rw [basis_apply_powersetCard, exteriorPower.basis_apply, ιMulti_family_apply_coe]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Grading (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : M
⊢ HMul.hMul (α := ⨁ (i : ℕ), ↥(⋀[R]^i M)) (β := ⨁ (i : ℕ), ↥(⋀[R]^i M))
      ((GradedAlgebra.ι R M : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m : ⨁ (i : ℕ), ↥(⋀[R]^i M))
      ((GradedAlgebra.ι R M : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m : ⨁ (i : ℕ), ↥(⋀[R]^i M)) =
    0
have rw : 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) sorry)
        (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) sorry)) :
    ⨁ (i : ℕ), ↥(⋀[R]^i M))
  (0 : ⨁ (i : ℕ), ↥(⋀[R]^i M))
Tactic: rw [GradedAlgebra.ι_apply, DirectSum.of_mul_of]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Grading (goal)
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))
    ((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))
have 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))
Tactic: obtain ⟨x, hx⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Grading (goal)
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
⊢ 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))
have 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))
Tactic: dsimp only [Subtype.coe_mk, DirectSum.lof_eq_of]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Grading (goal)
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))
    ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        ((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)
          ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r) ⋯) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
have 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)
        ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r) sorry) :
    ⨁ (i : ℕ), ↥(⋀[R]^i M))
Tactic: simp_rw [AlgHom.commutes, DirectSum.algebraMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Grading (goal)
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))
    ((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))
have 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) sorry) :
    ⨁ (i : ℕ), ↥(⋀[R]^i M))
Tactic: simp_rw [map_add, ihx, ihy, ← map_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Grading (goal)
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))
⊢ 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))
have 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)
          sorry) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
Tactic: obtain ⟨_, rfl⟩ := hm
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Grading (goal)
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))
    ((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))
have 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) sorry)
        (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) sorry) :
    ⨁ (i : ℕ), ↥(⋀[R]^i M))
Tactic: simp_rw [map_mul, ih, GradedAlgebra.liftι, lift_ι_apply, GradedAlgebra.ι_apply R M,
        DirectSum.of_mul_of]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Grading (goal)
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
⊢ 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))
have algebraMap : ∀ (r : R),
  Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    ((liftι R M : (a : ExteriorAlgebra R M) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        ((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)
          ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r) sorry) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
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, ← 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)
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Grading (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module 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))
have 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)
Tactic: ext m