awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ Eq (α := ExteriorAlgebra R M)
    ((DirectSum.coeAlgHom fun (i : ℕ) ↦ ⋀[R]^i M : (a : ⨁ (i : ℕ), ↥(⋀[R]^i M)) → ExteriorAlgebra R M)
        ((((lift R :
                  (a :
                      { f : M →ₗ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M) //
                        ∀ (m : M),
                          (f : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m * (f : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m = 0 }) →
                    ExteriorAlgebra R M →ₐ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M))
                (Subtype.mk (p := fun (f : M →ₗ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M)) ↦
                  ∀ (m : M),
                    HMul.hMul (α := ⨁ (i : ℕ), ↥(⋀[R]^i M)) (β := ⨁ (i : ℕ), ↥(⋀[R]^i M))
                        ((f : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m : ⨁ (i : ℕ), ↥(⋀[R]^i M))
                        ((f : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m : ⨁ (i : ℕ), ↥(⋀[R]^i M)) =
                      0)
                  (GradedAlgebra.ι R M) ⋯) :
              ExteriorAlgebra R M →ₐ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
            (a : CliffordAlgebra 0) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
          ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m)) :
      ExteriorAlgebra R M)
    ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
have a : Eq (α := ExteriorAlgebra R M)
  ((DirectSum.coeAlgHom fun (i : ℕ) ↦ ⋀[R]^i M : (a : ⨁ (i : ℕ), ↥(⋀[R]^i M)) → ExteriorAlgebra R M)
      ((GradedAlgebra.ι R M : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m) :
    ExteriorAlgebra R M)
  ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
Tactic: rw [lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.coeAlgHom_of, Subtype.coe_mk]
-- 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
a :
  Eq (α := ExteriorAlgebra R M)
    ((DirectSum.coeAlgHom fun (i : ℕ) ↦ ⋀[R]^i M : (a : ⨁ (i : ℕ), ↥(⋀[R]^i M)) → ExteriorAlgebra R M)
        ((GradedAlgebra.ι R M : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m) :
      ExteriorAlgebra R M)
    ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
⊢ Eq (α := ExteriorAlgebra R M)
    ((DirectSum.coeAlgHom fun (i : ℕ) ↦ ⋀[R]^i M : (a : ⨁ (i : ℕ), ↥(⋀[R]^i M)) → ExteriorAlgebra R M)
        ((((lift R :
                  (a :
                      { f : M →ₗ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M) //
                        ∀ (m : M),
                          (f : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m * (f : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m = 0 }) →
                    ExteriorAlgebra R M →ₐ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M))
                (Subtype.mk (p := fun (f : M →ₗ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M)) ↦
                  ∀ (m : M),
                    HMul.hMul (α := ⨁ (i : ℕ), ↥(⋀[R]^i M)) (β := ⨁ (i : ℕ), ↥(⋀[R]^i M))
                        ((f : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m : ⨁ (i : ℕ), ↥(⋀[R]^i M))
                        ((f : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m : ⨁ (i : ℕ), ↥(⋀[R]^i M)) =
                      0)
                  (GradedAlgebra.ι R M) ⋯) :
              ExteriorAlgebra R M →ₐ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
            (a : CliffordAlgebra 0) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
          ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m)) :
      ExteriorAlgebra R M)
    ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
have a₁ : Eq (α := ExteriorAlgebra R M)
  ((DirectSum.coeAlgHom fun (i : ℕ) ↦ ⋀[R]^i M : (a : ⨁ (i : ℕ), ↥(⋀[R]^i M)) → ExteriorAlgebra R M)
      (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) 1 : ↥(⋀[R]^1 M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^1 M)) → ⨁ (i : ℕ), ↥(⋀[R]^i 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) sorry)) :
    ExteriorAlgebra R M)
  ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
Tactic: rw [lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.coeAlgHom_of, Subtype.coe_mk]
-- 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
a :
  Eq (α := ExteriorAlgebra R M)
    ((DirectSum.coeAlgHom fun (i : ℕ) ↦ ⋀[R]^i M : (a : ⨁ (i : ℕ), ↥(⋀[R]^i M)) → ExteriorAlgebra R M)
        ((GradedAlgebra.ι R M : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m) :
      ExteriorAlgebra R M)
    ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
a₁ :
  Eq (α := ExteriorAlgebra R M)
    ((DirectSum.coeAlgHom fun (i : ℕ) ↦ ⋀[R]^i M : (a : ⨁ (i : ℕ), ↥(⋀[R]^i M)) → ExteriorAlgebra R M)
        (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) 1 : ↥(⋀[R]^1 M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
            (a : ↥(⋀[R]^1 M)) → ⨁ (i : ℕ), ↥(⋀[R]^i 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) ⋯)) :
      ExteriorAlgebra R M)
    ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
⊢ Eq (α := ExteriorAlgebra R M)
    ((DirectSum.coeAlgHom fun (i : ℕ) ↦ ⋀[R]^i M : (a : ⨁ (i : ℕ), ↥(⋀[R]^i M)) → ExteriorAlgebra R M)
        ((((lift R :
                  (a :
                      { f : M →ₗ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M) //
                        ∀ (m : M),
                          (f : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m * (f : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m = 0 }) →
                    ExteriorAlgebra R M →ₐ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M))
                (Subtype.mk (p := fun (f : M →ₗ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M)) ↦
                  ∀ (m : M),
                    HMul.hMul (α := ⨁ (i : ℕ), ↥(⋀[R]^i M)) (β := ⨁ (i : ℕ), ↥(⋀[R]^i M))
                        ((f : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m : ⨁ (i : ℕ), ↥(⋀[R]^i M))
                        ((f : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m : ⨁ (i : ℕ), ↥(⋀[R]^i M)) =
                      0)
                  (GradedAlgebra.ι R M) ⋯) :
              ExteriorAlgebra R M →ₐ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
            (a : CliffordAlgebra 0) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
          ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m)) :
      ExteriorAlgebra R M)
    ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
have a₂ : Eq (α := ExteriorAlgebra R 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) sorry) :
      ExteriorAlgebra R M) :
    ExteriorAlgebra R M)
  ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
Tactic: rw [lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.coeAlgHom_of, Subtype.coe_mk]
-- 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
a :
  Eq (α := ExteriorAlgebra R M)
    ((DirectSum.coeAlgHom fun (i : ℕ) ↦ ⋀[R]^i M : (a : ⨁ (i : ℕ), ↥(⋀[R]^i M)) → ExteriorAlgebra R M)
        ((GradedAlgebra.ι R M : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m) :
      ExteriorAlgebra R M)
    ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
a₁ :
  Eq (α := ExteriorAlgebra R M)
    ((DirectSum.coeAlgHom fun (i : ℕ) ↦ ⋀[R]^i M : (a : ⨁ (i : ℕ), ↥(⋀[R]^i M)) → ExteriorAlgebra R M)
        (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) 1 : ↥(⋀[R]^1 M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
            (a : ↥(⋀[R]^1 M)) → ⨁ (i : ℕ), ↥(⋀[R]^i 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) ⋯)) :
      ExteriorAlgebra R M)
    ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
a₂ :
  Eq (α := ExteriorAlgebra R 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) ⋯) :
        ExteriorAlgebra R M) :
      ExteriorAlgebra R M)
    ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
⊢ Eq (α := ExteriorAlgebra R M)
    ((DirectSum.coeAlgHom fun (i : ℕ) ↦ ⋀[R]^i M : (a : ⨁ (i : ℕ), ↥(⋀[R]^i M)) → ExteriorAlgebra R M)
        ((((lift R :
                  (a :
                      { f : M →ₗ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M) //
                        ∀ (m : M),
                          (f : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m * (f : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m = 0 }) →
                    ExteriorAlgebra R M →ₐ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M))
                (Subtype.mk (p := fun (f : M →ₗ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M)) ↦
                  ∀ (m : M),
                    HMul.hMul (α := ⨁ (i : ℕ), ↥(⋀[R]^i M)) (β := ⨁ (i : ℕ), ↥(⋀[R]^i M))
                        ((f : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m : ⨁ (i : ℕ), ↥(⋀[R]^i M))
                        ((f : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m : ⨁ (i : ℕ), ↥(⋀[R]^i M)) =
                      0)
                  (GradedAlgebra.ι R M) ⋯) :
              ExteriorAlgebra R M →ₐ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
            (a : CliffordAlgebra 0) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
          ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m)) :
      ExteriorAlgebra R M)
    ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
have a₃ : Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M)
  ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
Tactic: rw [lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.coeAlgHom_of, Subtype.coe_mk]
-- 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 (α := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    ⊤
have rw : ∀ (x : ExteriorAlgebra R M),
  Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    x
Tactic: rw [Submodule.eq_top_iff']
-- 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 : ℕ
hm : ↥(⋀[R]^i M)
⊢ Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    (↑hm : ExteriorAlgebra R M)
have homogeneous : ∀ (m : ExteriorAlgebra R M) (hm : Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) m),
  Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    (↑(Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) x) m hm) :
      ExteriorAlgebra R M)
Tactic: let ⟨m, hm⟩ := 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 : ℕ
hm_1 : ↥(⋀[R]^i M)
m : ExteriorAlgebra R M
hm : Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) m
⊢ Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    (↑(Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) x) m hm) :
      ExteriorAlgebra R M)
have homogeneous : (↑(⋀[R]^i M) : Set (ExteriorAlgebra R M)) ⊆
  (↑(Submodule.span R
        (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
          (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
            (x.snd (β := fun (n : ℕ) ↦ Fin n → M)))) :
    Set (ExteriorAlgebra R M))
Tactic: apply Set.mem_of_mem_of_subset 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 : ℕ
hm_1 : ↥(⋀[R]^i M)
m : ExteriorAlgebra R M
hm : Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) m
⊢ (↑(⋀[R]^i M) : Set (ExteriorAlgebra R M)) ⊆
    (↑(Submodule.span R
          (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
            (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
              (x.snd (β := fun (n : ℕ) ↦ Fin n → M)))) :
      Set (ExteriorAlgebra R M))
have homogeneous : (↑(Submodule.span R (Set.range (ι := Fin i → M) (⇑(ιMulti R i) : (a : Fin i → M) → ExteriorAlgebra R M))) :
    Set (ExteriorAlgebra R M)) ⊆
  (↑(Submodule.span R
        (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
          (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
            (x.snd (β := fun (n : ℕ) ↦ Fin n → M)))) :
    Set (ExteriorAlgebra R M))
Tactic: rw [← ιMulti_span_fixedDegree]
-- 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 : ℕ
hm_1 : ↥(⋀[R]^i M)
m : ExteriorAlgebra R M
hm : Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) m
⊢ (↑(Submodule.span R (Set.range (ι := Fin i → M) (⇑(ιMulti R i) : (a : Fin i → M) → ExteriorAlgebra R M))) :
      Set (ExteriorAlgebra R M)) ⊆
    (↑(Submodule.span R
          (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
            (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
              (x.snd (β := fun (n : ℕ) ↦ Fin n → M)))) :
      Set (ExteriorAlgebra R M))
have homogeneous : ∀ (x : ExteriorAlgebra R M)
  (hx :
    Membership.mem (γ := Set (ExteriorAlgebra R M))
      (Set.range (ι := Fin i → M) (⇑(ιMulti R i) : (a : Fin i → M) → ExteriorAlgebra R M)) x),
  Membership.mem (γ := Set (ExteriorAlgebra R M))
    (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
      (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
        (x.snd (β := fun (n : ℕ) ↦ Fin n → M)))
    x
Tactic: refine Submodule.span_mono fun _ 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
i : ℕ
hm_1 : ↥(⋀[R]^i M)
m : ExteriorAlgebra R M
hm : Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^i M) m
x : ExteriorAlgebra R M
hx :
  Membership.mem (γ := Set (ExteriorAlgebra R M))
    (Set.range (ι := Fin i → M) (⇑(ιMulti R i) : (a : Fin i → M) → ExteriorAlgebra R M)) x
⊢ Membership.mem (γ := Set (ExteriorAlgebra R M))
    (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
      (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
        (x.snd (β := fun (n : ℕ) ↦ Fin n → M)))
    x
have homogeneous : ∀ (y : Fin i → M),
  Membership.mem (α := ExteriorAlgebra R M) (γ := Set (ExteriorAlgebra R M))
    (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
      (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
        (x.snd (β := fun (n : ℕ) ↦ Fin n → M)))
    ((ιMulti R i : (a : Fin i → M) → ExteriorAlgebra R M) y : ExteriorAlgebra R M)
Tactic: obtain ⟨y, rfl⟩ := hx
Cleared hypotheses: x, 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
x : ExteriorAlgebra R M
⊢ Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    x
have zero : Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
  (Submodule.span R
    (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
      (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
        (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
  0
Tactic: induction x using DirectSum.Decomposition.inductionOn fun i => ⋀[R]^i M with
  | zero => exact Submodule.zero_mem _
  | add _ _ hm hm' => exact Submodule.add_mem _ hm hm'
  | homogeneous hm =>
    let ⟨m, hm⟩ := hm
    apply Set.mem_of_mem_of_subset hm
    rw [← ιMulti_span_fixedDegree]
    refine Submodule.span_mono fun _ hx ↦ ?_
    obtain ⟨y, rfl⟩ := hx
    exact ⟨⟨_, y⟩, rfl⟩
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
x : ExteriorAlgebra R M
zero :
  Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    0
⊢ Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    x
have add : ∀ (m m' : ExteriorAlgebra R M)
  (hm :
    Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
      (Submodule.span R
        (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
          (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
            (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
      m)
  (hm' :
    Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
      (Submodule.span R
        (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
          (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
            (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
      m'),
  Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    (m + m')
Tactic: induction x using DirectSum.Decomposition.inductionOn fun i => ⋀[R]^i M with
  | zero => exact Submodule.zero_mem _
  | add _ _ hm hm' => exact Submodule.add_mem _ hm hm'
  | homogeneous hm =>
    let ⟨m, hm⟩ := hm
    apply Set.mem_of_mem_of_subset hm
    rw [← ιMulti_span_fixedDegree]
    refine Submodule.span_mono fun _ hx ↦ ?_
    obtain ⟨y, rfl⟩ := hx
    exact ⟨⟨_, y⟩, rfl⟩
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
x : ExteriorAlgebra R M
zero :
  Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    0
add :
  ∀ (m m' : ExteriorAlgebra R M)
    (hm :
      Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
        (Submodule.span R
          (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
            (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
              (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
        m)
    (hm' :
      Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
        (Submodule.span R
          (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
            (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
              (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
        m'),
    Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
      (Submodule.span R
        (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
          (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
            (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
      (m + m')
⊢ Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    x
have homogeneous : ∀ {i : ℕ} (hm : ↥(⋀[R]^i M)),
  Membership.mem (γ := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (Set.range fun (x : (n : ℕ) × (Fin n → M)) ↦
        (ιMulti R (x.fst (β := fun (n : ℕ) ↦ Fin n → M)) : (a : Fin x.fst → M) → ExteriorAlgebra R M)
          (x.snd (β := fun (n : ℕ) ↦ Fin n → M))))
    (↑hm : ExteriorAlgebra R M)
Tactic: induction x using DirectSum.Decomposition.inductionOn fun i => ⋀[R]^i M with
  | zero => exact Submodule.zero_mem _
  | add _ _ hm hm' => exact Submodule.add_mem _ hm hm'
  | homogeneous hm =>
    let ⟨m, hm⟩ := hm
    apply Set.mem_of_mem_of_subset hm
    rw [← ιMulti_span_fixedDegree]
    refine Submodule.span_mono fun _ hx ↦ ?_
    obtain ⟨y, rfl⟩ := hx
    exact ⟨⟨_, y⟩, rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
this : ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] N
have refine : ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] N
Tactic: refine LinearMap.compr₂ this ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
this : ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] N
have refine : M [⋀^Fin 0]→ₗ[R] N ≃ₗ[R] N
Tactic: refine (LinearEquiv.toLinearMap ?_).comp (LinearMap.proj 0)