awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
f : Fin n → (↑((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) : Type (max u u_1))
hx :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n
a :
  Membership.mem (γ := Set (Fin n → M)) {a : Fin n → M | range a ⊆ s}
    ((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
      Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Set (ExteriorAlgebra R M))
            ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
        f)
⊢ List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    (↑(span R
          (image (α := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)
            {a : Fin n → M | range a ⊆ s})) :
      Set (ExteriorAlgebra R M))
have a₁ : Eq (α := ExteriorAlgebra R M)
  ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M)
      ((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
        Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Set (ExteriorAlgebra R M))
              ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
          f) :
    ExteriorAlgebra R M)
  (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) : ExteriorAlgebra R M)
Tactic: refine mem_span_of_mem ⟨ExteriorAlgebra.ιInv ∘ Subtype.val ∘ f, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
f : Fin n → (↑((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) : Type (max u u_1))
hx :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n
⊢ Membership.mem (γ := Set (Fin n → M)) {a : Fin n → M | range a ⊆ s}
    ((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
      Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Set (ExteriorAlgebra R M))
            ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
        f)
have a : range
    (Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
        Membership.mem (γ := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s)
          x) ∘
      f) ⊆
  (⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ⁻¹' s
Tactic: rw [Set.mem_setOf_eq, Set.range_comp, Set.image_subset_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
f : Fin n → (↑((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) : Type (max u u_1))
hx :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n
⊢ range
      (Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Set (ExteriorAlgebra R M))
            ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
        f) ⊆
    (⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ⁻¹' s
have apply : range
    (Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
        Membership.mem (γ := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s)
          x) ∘
      f) ⊆
  (⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s
Tactic: apply Subset.trans ?_ (s.image_subset_preimage_of_inverse ExteriorAlgebra.ι_leftInverse)
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
f : Fin n → (↑((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) : Type (max u u_1))
hx :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n
⊢ Eq (α := ExteriorAlgebra R M)
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M)
        ((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
          Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
              Membership.mem (γ := Set (ExteriorAlgebra R M))
                ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
            f) :
      ExteriorAlgebra R M)
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) : ExteriorAlgebra R M)
have a : Eq (α := ExteriorAlgebra R M)
  (List.prod
    (List.ofFn (n := n) fun (i : Fin n) ↦
      (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
        (((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
            Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
                Membership.mem (γ := Set (ExteriorAlgebra R M))
                  ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
              f)
          i)))
  (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)))
Tactic: rw [ExteriorAlgebra.ιMulti_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
f : Fin n → (↑((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) : Type (max u u_1))
hx :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n
⊢ Eq (α := ExteriorAlgebra R M)
    (List.prod
      (List.ofFn (n := n) fun (i : Fin n) ↦
        (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
          (((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
              Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
                  Membership.mem (γ := Set (ExteriorAlgebra R M))
                    ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
                f)
            i)))
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)))
have a : Eq (α := Fin n → ExteriorAlgebra R M)
  (fun (i : Fin n) ↦
    (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
      (((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
          Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
              Membership.mem (γ := Set (ExteriorAlgebra R M))
                ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
            f)
        i))
  fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)
Tactic: apply congrArg (List.prod ∘ List.ofFn)
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
f : Fin n → (↑((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) : Type (max u u_1))
hx :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n
⊢ Eq (α := Fin n → ExteriorAlgebra R M)
    (fun (i : Fin n) ↦
      (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
        (((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
            Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
                Membership.mem (γ := Set (ExteriorAlgebra R M))
                  ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
              f)
          i))
    fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)
have a : ∀ (i : Fin n),
  (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
      (((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
          Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
              Membership.mem (γ := Set (ExteriorAlgebra R M))
                ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
            f)
        i) =
    (↑(f i) : ExteriorAlgebra R M)
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
f : Fin n → (↑((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) : Type (max u u_1))
hx :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n
i : Fin n
⊢ (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
      (((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
          Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
              Membership.mem (γ := Set (ExteriorAlgebra R M))
                ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
            f)
        i) =
    (↑(f i) : ExteriorAlgebra R M)
have a : ∀ (m : M) (hm : (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M) m = (↑(f i) : ExteriorAlgebra R M)),
  (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
      (((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
          Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
              Membership.mem (γ := Set (ExteriorAlgebra R M))
                ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
            f)
        i) =
    (↑(f i) : ExteriorAlgebra R M)
Tactic: obtain ⟨m, -, hm⟩ := (Set.mem_image _ _ _).mp (f i).2
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
f : Fin n → (↑((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) : Type (max u u_1))
hx :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n
i : Fin n
m : M
hm : (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M) m = (↑(f i) : ExteriorAlgebra R M)
⊢ (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
      (((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
          Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
              Membership.mem (γ := Set (ExteriorAlgebra R M))
                ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
            f)
        i) =
    (↑(f i) : ExteriorAlgebra R M)
have a : (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
    ((ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M)
      ((Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Set (ExteriorAlgebra R M))
              ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
          f)
        i)) =
  (↑(f i) : ExteriorAlgebra R M)
Tactic: rw [Function.comp_apply, Function.comp_apply, ← hm, ExteriorAlgebra.ι_leftInverse]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
f : Fin n → (↑((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) : Type (max u u_1))
hx :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n
i : Fin n
m : M
hm : (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M) m = (↑(f i) : ExteriorAlgebra R M)
a :
  (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
      ((ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M)
        ((Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
              Membership.mem (γ := Set (ExteriorAlgebra R M))
                ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
            f)
          i)) =
    (↑(f i) : ExteriorAlgebra R M)
⊢ (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
      (((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
          Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
              Membership.mem (γ := Set (ExteriorAlgebra R M))
                ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
            f)
        i) =
    (↑(f i) : ExteriorAlgebra R M)
have a₁ : (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
    ((ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) (↑(f i) : ExteriorAlgebra R M)) =
  (↑(f i) : ExteriorAlgebra R M)
Tactic: rw [Function.comp_apply, Function.comp_apply, ← hm, ExteriorAlgebra.ι_leftInverse]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
f : Fin n → (↑((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) : Type (max u u_1))
hx :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n
i : Fin n
m : M
hm : (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M) m = (↑(f i) : ExteriorAlgebra R M)
a :
  (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
      ((ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M)
        ((Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
              Membership.mem (γ := Set (ExteriorAlgebra R M))
                ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
            f)
          i)) =
    (↑(f i) : ExteriorAlgebra R M)
a₁ :
  (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
      ((ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) (↑(f i) : ExteriorAlgebra R M)) =
    (↑(f i) : ExteriorAlgebra R M)
⊢ (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
      (((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
          Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
              Membership.mem (γ := Set (ExteriorAlgebra R M))
                ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
            f)
        i) =
    (↑(f i) : ExteriorAlgebra R M)
have a₂ : Eq (α := ExteriorAlgebra R M)
  ((ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
      ((ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M)
        ((ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M)) :
    ExteriorAlgebra R M)
  ((ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M)
Tactic: rw [Function.comp_apply, Function.comp_apply, ← hm, ExteriorAlgebra.ι_leftInverse]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
f : Fin n → (↑((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) : Type (max u u_1))
hx :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n
i : Fin n
m : M
hm : (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M) m = (↑(f i) : ExteriorAlgebra R M)
a :
  (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
      ((ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M)
        ((Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
              Membership.mem (γ := Set (ExteriorAlgebra R M))
                ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
            f)
          i)) =
    (↑(f i) : ExteriorAlgebra R M)
a₁ :
  (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
      ((ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) (↑(f i) : ExteriorAlgebra R M)) =
    (↑(f i) : ExteriorAlgebra R M)
a₂ :
  Eq (α := ExteriorAlgebra R M)
    ((ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
        ((ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M)
          ((ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M)) :
      ExteriorAlgebra R M)
    ((ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M)
⊢ (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
      (((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
          Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
              Membership.mem (γ := Set (ExteriorAlgebra R M))
                ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
            f)
        i) =
    (↑(f i) : ExteriorAlgebra R M)
have a₃ : Eq (α := ExteriorAlgebra R M) ((ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M)
  ((ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M)
Tactic: rw [Function.comp_apply, Function.comp_apply, ← hm, ExteriorAlgebra.ι_leftInverse]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Eq (α := Submodule R ↥(⋀[R]^n M))
    (Submodule.span R (range (ι := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ↥(⋀[R]^n M)))) ⊤
have a : Eq (α := Submodule R (ExteriorAlgebra R M))
  (Submodule.map (M := ↥(⋀[R]^n M)) (Submodule.subtype (⋀[R]^n M))
    (Submodule.span R (range (ι := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ↥(⋀[R]^n M)))))
  (Submodule.map (M := ↥(⋀[R]^n M)) (Submodule.subtype (⋀[R]^n M)) ⊤)
Tactic: apply LinearMap.map_injective (Submodule.ker_subtype (⋀[R]^n M))
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Eq (α := Submodule R (ExteriorAlgebra R M))
    (Submodule.map (M := ↥(⋀[R]^n M)) (Submodule.subtype (⋀[R]^n M))
      (Submodule.span R (range (ι := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ↥(⋀[R]^n M)))))
    (Submodule.map (M := ↥(⋀[R]^n M)) (Submodule.subtype (⋀[R]^n M)) ⊤)
have a : Eq (α := Submodule R (ExteriorAlgebra R M))
  (Submodule.span R
    ((fun (x : Fin n → M) ↦
        (Submodule.subtype (⋀[R]^n M) : (a : ↥(⋀[R]^n M)) → ExteriorAlgebra R M)
          ((ιMulti R n : (a : Fin n → M) → ↥(⋀[R]^n M)) x)) ''
      univ))
  (Submodule.map (M := ↥(⋀[R]^n M)) (Submodule.subtype (⋀[R]^n M)) ⊤)
Tactic: rw [LinearMap.map_span, ← Set.image_univ, Set.image_image]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Eq (α := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      ((fun (x : Fin n → M) ↦
          (Submodule.subtype (⋀[R]^n M) : (a : ↥(⋀[R]^n M)) → ExteriorAlgebra R M)
            ((ιMulti R n : (a : Fin n → M) → ↥(⋀[R]^n M)) x)) ''
        univ))
    (Submodule.map (M := ↥(⋀[R]^n M)) (Submodule.subtype (⋀[R]^n M)) ⊤)
have a : Eq (α := Submodule R (ExteriorAlgebra R M))
  (Submodule.span R
    (range fun (a : Fin n → M) ↦ (ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) a))
  (⋀[R]^n M)
Tactic: simp only [Submodule.coe_subtype, ιMulti_apply_coe, Set.image_univ, Submodule.map_top,
    Submodule.range_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
⊢ Eq (α := Submodule R ↥(⋀[R]^n M))
    (span R (image (α := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ↥(⋀[R]^n M)) {a : Fin n → M | range a ⊆ s})) ⊤
have a : Eq (α := Submodule R (ExteriorAlgebra R M))
  (Submodule.map (M := ↥(⋀[R]^n M)) (Submodule.subtype (⋀[R]^n M))
    (span R (image (α := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ↥(⋀[R]^n M)) {a : Fin n → M | range a ⊆ s})))
  (Submodule.map (M := ↥(⋀[R]^n M)) (Submodule.subtype (⋀[R]^n M)) ⊤)
Tactic: apply LinearMap.map_injective (ker_subtype (⋀[R]^n M))
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M_1 : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
ι : Type u_4
inst_7 : DecidableEq ι
M : Type u_5
inst_8 : AddCommGroup M
inst_9 : Module R M
s : Module.Relations.Solution (relations R ι M) N
inst_10 : DecidableEq ι
m : (i : ι) → M
i : ι
x y : M
⊢ s.var (update (β := fun (x : ι) ↦ M) m i (x + y)) =
    s.var (update (β := fun (x : ι) ↦ M) m i x) + s.var (update (β := fun (x : ι) ↦ M) m i y)
have this : Eq.{u_2 + 1} (α := N)
  ((Finsupp.linearCombination R s.var : (a : (relations R ι M).G →₀ R) → N)
      (Module.Relations.relation (relations R ι M) (Rels.add m i x y)) :
    N)
  (0 : N)
Tactic: have := s.linearCombination_var_relation (.add m i x y)
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M_1 : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
ι : Type u_4
inst_7 : DecidableEq ι
M : Type u_5
inst_8 : AddCommGroup M
inst_9 : Module R M
s : Module.Relations.Solution (relations R ι M) N
inst_10 : DecidableEq ι
m : (i : ι) → M
i : ι
x y : M
this :
  Eq.{u_2 + 1} (α := N)
    ((Finsupp.linearCombination R s.var : (a : (ι → M) →₀ R) → N)
        (HAdd.hAdd (α := ((a : ι) → M) →₀ R) (Finsupp.single (update (β := fun (a : ι) ↦ M) m i x) 1)
            (Finsupp.single (update (β := fun (a : ι) ↦ M) m i y) 1) -
          Finsupp.single (update (β := fun (a : ι) ↦ M) m i (x + y)) 1) :
      N)
    (0 : N)
⊢ s.var (update (β := fun (x : ι) ↦ M) m i (x + y)) =
    s.var (update (β := fun (x : ι) ↦ M) m i x) + s.var (update (β := fun (x : ι) ↦ M) m i y)
have this₁ : s.var (update (β := fun (a : ι) ↦ M) m i x) + s.var (update (β := fun (a : ι) ↦ M) m i y) =
  s.var (update (β := fun (a : ι) ↦ M) m i (x + y))
Tactic: rw [map_sub, map_add, Finsupp.linearCombination_single, one_smul,
          Finsupp.linearCombination_single, one_smul,
          Finsupp.linearCombination_single, one_smul, sub_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M_1 : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
ι : Type u_4
inst_7 : DecidableEq ι
M : Type u_5
inst_8 : AddCommGroup M
inst_9 : Module R M
s : Module.Relations.Solution (relations R ι M) N
inst_10 : DecidableEq ι
m : (i : ι) → M
i : ι
r : R
x : M
⊢ s.var (update (β := fun (x : ι) ↦ M) m i (r • x)) = r • s.var (update (β := fun (x : ι) ↦ M) m i x)
have this : Eq.{u_2 + 1} (α := N)
  ((Finsupp.linearCombination R s.var : (a : (relations R ι M).G →₀ R) → N)
      (Module.Relations.relation (relations R ι M) (Rels.smul m i r x)) :
    N)
  (0 : N)
Tactic: have := s.linearCombination_var_relation (.smul m i r x)