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
m n : ℕ
a : Fin m → M
b : Fin n → M
⊢ HMul.hMul (α := ExteriorAlgebra R M)
      (List.prod (List.ofFn (n := m) fun (i : Fin m) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (a i)))
      (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (b i))) =
    HMul.hMul (α := ExteriorAlgebra R M) (List.prod (List.map (⇑(ι R) : (a : M) → ExteriorAlgebra R M) (List.ofFn a)))
      (List.prod (List.map (⇑(ι R) : (a : M) → ExteriorAlgebra R M) (List.ofFn b)))
have simp : HMul.hMul (α := ExteriorAlgebra R M)
    (List.prod (List.ofFn (n := m) fun (i : Fin m) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (a i)))
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (b i))) =
  HMul.hMul (α := ExteriorAlgebra R M) (List.prod (List.ofFn ((⇑(ι R) : (a : M) → ExteriorAlgebra R M) ∘ a)))
    (List.prod (List.ofFn ((⇑(ι R) : (a : M) → ExteriorAlgebra R M) ∘ b)))
Tactic: simp only [List.map_ofFn]
-- 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 : ℕ
⊢ Set.range (ι := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M) ⊆
    (↑(⋀[R]^n M) : Set (ExteriorAlgebra R M))
have rw : ∀ (y : Fin n → M),
  Membership.mem (α := ExteriorAlgebra R M) (↑(⋀[R]^n M) : Set (ExteriorAlgebra R M))
    ((ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) y : ExteriorAlgebra R M)
Tactic: rw [Set.range_subset_iff]
-- 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 : ℕ
v : Fin n → M
⊢ Membership.mem (α := ExteriorAlgebra R M) (↑(⋀[R]^n M) : Set (ExteriorAlgebra R M))
    ((ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) v : ExteriorAlgebra R M)
have rw : List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i)) ∈
  (↑(⋀[R]^n M) : Set (ExteriorAlgebra R M))
Tactic: rw [ιMulti_apply]
-- 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 : ℕ
v : Fin n → M
⊢ List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i)) ∈
    (↑(⋀[R]^n M) : Set (ExteriorAlgebra R M))
have a : List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i)) ∈
  (↑(LinearMap.range (ι R)) : Set (ExteriorAlgebra R M)) ^ n
Tactic: apply Submodule.pow_subset_pow
-- 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 : ℕ
v : Fin n → M
⊢ List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i)) ∈
    (↑(LinearMap.range (ι R)) : Set (ExteriorAlgebra R M)) ^ n
have a : ∃ (f : Fin n → (↑(↑(LinearMap.range (ι R)) : Set (ExteriorAlgebra R M)) : Type (max u1 u2))),
  Eq (α := ExteriorAlgebra R M) (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)))
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i)))
Tactic: rw [Set.mem_pow]
-- 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 : ℕ
⊢ Eq (α := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R (Set.range (ι := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M))) (⋀[R]^n M)
have refine : LE.le (α := Submodule R (ExteriorAlgebra R M)) (⋀[R]^n M)
  (Submodule.span R (Set.range (ι := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)))
Tactic: refine le_antisymm (Submodule.span_le.2 (ιMulti_range R n)) ?_
-- 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 : ℕ
⊢ LE.le (α := Submodule R (ExteriorAlgebra R M)) (⋀[R]^n M)
    (Submodule.span R (Set.range (ι := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)))
have rw : (↑(LinearMap.range (ι R)) : Set (ExteriorAlgebra R M)) ^ n ⊆
  (↑(Submodule.span R (Set.range (ι := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M))) :
    Set (ExteriorAlgebra R M))
Tactic: rw [exteriorPower, Submodule.pow_eq_span_pow_set, Submodule.span_le]
-- 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 : ℕ
⊢ (↑(LinearMap.range (ι R)) : Set (ExteriorAlgebra R M)) ^ n ⊆
    (↑(Submodule.span R (Set.range (ι := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M))) :
      Set (ExteriorAlgebra R M))
have refine : ∀ (u : ExteriorAlgebra R M) (hu : u ∈ (↑(LinearMap.range (ι R)) : Set (ExteriorAlgebra R M)) ^ n),
  Membership.mem (γ := Set (ExteriorAlgebra R M))
    (Set.range (ι := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)) u
Tactic: refine fun u hu ↦ Submodule.subset_span ?_
-- 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 : ℕ
u : ExteriorAlgebra R M
hu : u ∈ (↑(LinearMap.range (ι R)) : Set (ExteriorAlgebra R M)) ^ n
⊢ Membership.mem (γ := Set (ExteriorAlgebra R M))
    (Set.range (ι := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)) u
have obtain : ∀ (f : Fin n → (↑(↑(LinearMap.range (ι R)) : Set (ExteriorAlgebra R M)) : Type (max u1 u2)))
  (hu :
    List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
      (↑(LinearMap.range (ι R)) : Set (ExteriorAlgebra R M)) ^ n),
  Membership.mem (γ := Set (ExteriorAlgebra R M))
    (Set.range (ι := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M))
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)))
Tactic: obtain ⟨f, rfl⟩ := Set.mem_pow.mp hu
Cleared hypotheses: u, hu
-- 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 : ℕ
f : Fin n → (↑(↑(LinearMap.range (ι R)) : Set (ExteriorAlgebra R M)) : Type (max u1 u2))
hu :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    (↑(LinearMap.range (ι R)) : Set (ExteriorAlgebra R M)) ^ n
⊢ Membership.mem (γ := Set (ExteriorAlgebra R M))
    (Set.range (ι := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M))
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)))
have refine : Eq (α := ExteriorAlgebra R M)
  ((ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) fun (i : Fin n) ↦
    (ιInv : (a : ExteriorAlgebra R M) → M) (↑(f i) : ExteriorAlgebra R M))
  (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)))
Tactic: refine ⟨fun i => ιInv (f i).1, ?_⟩
-- 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 : ℕ
f : Fin n → (↑(↑(LinearMap.range (ι R)) : Set (ExteriorAlgebra R M)) : Type (max u1 u2))
hu :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    (↑(LinearMap.range (ι R)) : Set (ExteriorAlgebra R M)) ^ n
⊢ Eq (α := ExteriorAlgebra R M)
    ((ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) fun (i : Fin n) ↦
      (ιInv : (a : ExteriorAlgebra R M) → M) (↑(f i) : ExteriorAlgebra R M))
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)))
have rw : Eq (α := ExteriorAlgebra R M)
  (List.prod
    (List.ofFn (n := n) fun (i : Fin n) ↦
      (ι R : (a : M) → ExteriorAlgebra R M) ((ιInv : (a : ExteriorAlgebra R M) → M) (↑(f i) : ExteriorAlgebra R M))))
  (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)))
Tactic: rw [ιMulti_apply]
-- 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 : ℕ
f : Fin n → (↑(↑(LinearMap.range (ι R)) : Set (ExteriorAlgebra R M)) : Type (max u1 u2))
hu :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    (↑(LinearMap.range (ι R)) : Set (ExteriorAlgebra R M)) ^ n
⊢ Eq (α := ExteriorAlgebra R M)
    (List.prod
      (List.ofFn (n := n) fun (i : Fin n) ↦
        (ι R : (a : M) → ExteriorAlgebra R M) ((ιInv : (a : ExteriorAlgebra R M) → M) (↑(f i) : ExteriorAlgebra R M))))
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)))
have e_xs : ∀ (i : Fin n),
  (ι R : (a : M) → ExteriorAlgebra R M) ((ιInv : (a : ExteriorAlgebra R M) → M) (↑(f i) : ExteriorAlgebra R M)) =
    (↑(f i) : ExteriorAlgebra R M)
Tactic: congr with i
-- 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 : ℕ
f : Fin n → (↑(↑(LinearMap.range (ι R)) : Set (ExteriorAlgebra R M)) : Type (max u1 u2))
hu :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    (↑(LinearMap.range (ι R)) : Set (ExteriorAlgebra R M)) ^ n
i : Fin n
⊢ (ι R : (a : M) → ExteriorAlgebra R M) ((ιInv : (a : ExteriorAlgebra R M) → M) (↑(f i) : ExteriorAlgebra R M)) =
    (↑(f i) : ExteriorAlgebra R M)
have e_xs : ∀ (v : M) (hv : (ι R : (a : M) → ExteriorAlgebra R M) v = (↑(f i) : ExteriorAlgebra R M)),
  (ι R : (a : M) → ExteriorAlgebra R M) ((ιInv : (a : ExteriorAlgebra R M) → M) (↑(f i) : ExteriorAlgebra R M)) =
    (↑(f i) : ExteriorAlgebra R M)
Tactic: obtain ⟨v, hv⟩ := (f i).prop
-- 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 : ℕ
f : Fin n → (↑(↑(LinearMap.range (ι R)) : Set (ExteriorAlgebra R M)) : Type (max u1 u2))
hu :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    (↑(LinearMap.range (ι R)) : Set (ExteriorAlgebra R M)) ^ n
i : Fin n
v : M
hv : (ι R : (a : M) → ExteriorAlgebra R M) v = (↑(f i) : ExteriorAlgebra R M)
⊢ (ι R : (a : M) → ExteriorAlgebra R M) ((ιInv : (a : ExteriorAlgebra R M) → M) (↑(f i) : ExteriorAlgebra R M)) =
    (↑(f i) : ExteriorAlgebra R M)
have e_xs : Eq (α := ExteriorAlgebra R M)
  ((ι R : (a : M) → ExteriorAlgebra R M)
      ((ιInv : (a : ExteriorAlgebra R M) → M) ((ι R : (a : M) → ExteriorAlgebra R M) v : ExteriorAlgebra R M)) :
    ExteriorAlgebra R M)
  ((ι R : (a : M) → ExteriorAlgebra R M) v : ExteriorAlgebra R M)
Tactic: rw [← hv, ι_leftInverse]
-- 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 : ℕ
f : Fin n → (↑(↑(LinearMap.range (ι R)) : Set (ExteriorAlgebra R M)) : Type (max u1 u2))
hu :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    (↑(LinearMap.range (ι R)) : Set (ExteriorAlgebra R M)) ^ n
i : Fin n
v : M
hv : (ι R : (a : M) → ExteriorAlgebra R M) v = (↑(f i) : ExteriorAlgebra R M)
e_xs :
  Eq (α := ExteriorAlgebra R M)
    ((ι R : (a : M) → ExteriorAlgebra R M)
        ((ιInv : (a : ExteriorAlgebra R M) → M) ((ι R : (a : M) → ExteriorAlgebra R M) v : ExteriorAlgebra R M)) :
      ExteriorAlgebra R M)
    ((ι R : (a : M) → ExteriorAlgebra R M) v : ExteriorAlgebra R M)
⊢ (ι R : (a : M) → ExteriorAlgebra R M) ((ιInv : (a : ExteriorAlgebra R M) → M) (↑(f i) : ExteriorAlgebra R M)) =
    (↑(f i) : ExteriorAlgebra R M)
have e_xs₁ : Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) v : ExteriorAlgebra R M)
  ((ι R : (a : M) → ExteriorAlgebra R M) v : ExteriorAlgebra R M)
Tactic: rw [← hv, ι_leftInverse]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (hypothesis)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
m n : ℕ
I : Type u_1
inst_3 : LinearOrder I
v : I → M
s : (↑(powersetCard I m) : Type u_1)
t : (↑(powersetCard I n) : Type u_1)
h : ¬Disjoint (↑s : Finset I) (↑t : Finset I)
⊢ HMul.hMul (α := ExteriorAlgebra R M) (ιMulti_family R m v s) (ιMulti_family R n v t) = 0
have h₁ : ∃ a ∈ (↑s : Finset I), a ∈ (↑t : Finset I)
Tactic: rw [Finset.not_disjoint_iff] at h
Cleared hypotheses: 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
m n : ℕ
I : Type u_1
inst_3 : LinearOrder I
v : I → M
s : (↑(powersetCard I m) : Type u_1)
t : (↑(powersetCard I n) : Type u_1)
h : ∃ a ∈ (↑s : Finset I), a ∈ (↑t : Finset I)
⊢ HMul.hMul (α := ExteriorAlgebra R M) (ιMulti_family R m v s) (ιMulti_family R n v t) = 0
have obtain : ∀ (i : I) (his : i ∈ (↑s : Finset I)) (hit : i ∈ (↑t : Finset I)),
  HMul.hMul (α := ExteriorAlgebra R M) (ιMulti_family R m v s) (ιMulti_family R n v t) = 0
Tactic: obtain ⟨i, his, hit⟩ := h
Cleared hypotheses: 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
m n : ℕ
I : Type u_1
inst_3 : LinearOrder I
v : I → M
s : (↑(powersetCard I m) : Type u_1)
t : (↑(powersetCard I n) : Type u_1)
i : I
his : i ∈ (↑s : Finset I)
hit : i ∈ (↑t : Finset I)
⊢ HMul.hMul (α := ExteriorAlgebra R M) (ιMulti_family R m v s) (ιMulti_family R n v t) = 0
have obtain : ∀ (j : Fin m)
  (hj :
    (((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) :
          (a : Fin m) → I)
        j =
      i),
  HMul.hMul (α := ExteriorAlgebra R M) (ιMulti_family R m v s) (ιMulti_family R n v t) = 0
Tactic: obtain ⟨j, hj⟩ := (mem_range_ofFinEmbEquiv_symm_iff_mem s i).mpr his
-- 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
m n : ℕ
I : Type u_1
inst_3 : LinearOrder I
v : I → M
s : (↑(powersetCard I m) : Type u_1)
t : (↑(powersetCard I n) : Type u_1)
i : I
his : i ∈ (↑s : Finset I)
hit : i ∈ (↑t : Finset I)
j : Fin m
hj :
  (((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) : (a : Fin m) → I)
      j =
    i
⊢ HMul.hMul (α := ExteriorAlgebra R M) (ιMulti_family R m v s) (ιMulti_family R n v t) = 0
have obtain : ∀ (k : Fin n)
  (hk :
    (((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) :
          (a : Fin n) → I)
        k =
      i),
  HMul.hMul (α := ExteriorAlgebra R M) (ιMulti_family R m v s) (ιMulti_family R n v t) = 0
Tactic: obtain ⟨k, hk⟩ := (mem_range_ofFinEmbEquiv_symm_iff_mem t i).mpr hit
-- 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
m n : ℕ
I : Type u_1
inst_3 : LinearOrder I
v : I → M
s : (↑(powersetCard I m) : Type u_1)
t : (↑(powersetCard I n) : Type u_1)
i : I
his : i ∈ (↑s : Finset I)
hit : i ∈ (↑t : Finset I)
j : Fin m
hj :
  (((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) : (a : Fin m) → I)
      j =
    i
k : Fin n
hk :
  (((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) : (a : Fin n) → I)
      k =
    i
⊢ HMul.hMul (α := ExteriorAlgebra R M) (ιMulti_family R m v s) (ιMulti_family R n v t) = 0
have simp : Eq (α := ExteriorAlgebra R M)
  ((ιMulti R (m + n) : (a : Fin (m + n) → M) → ExteriorAlgebra R M)
      (Fin.append
        (v ∘
          (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) :
            (a : Fin m) → I))
        (v ∘
          (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) :
            (a : Fin n) → I))) :
    ExteriorAlgebra R M)
  (0 : ExteriorAlgebra R M)
Tactic: simp only [ιMulti_family, ιMulti_mul_ιMulti]
-- 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
m n : ℕ
I : Type u_1
inst_3 : LinearOrder I
v : I → M
s : (↑(powersetCard I m) : Type u_1)
t : (↑(powersetCard I n) : Type u_1)
i : I
his : i ∈ (↑s : Finset I)
hit : i ∈ (↑t : Finset I)
j : Fin m
hj :
  (((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) : (a : Fin m) → I)
      j =
    i
k : Fin n
hk :
  (((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) : (a : Fin n) → I)
      k =
    i
⊢ Eq (α := ExteriorAlgebra R M)
    ((ιMulti R (m + n) : (a : Fin (m + n) → M) → ExteriorAlgebra R M)
        (Fin.append
          (v ∘
            (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) :
              (a : Fin m) → I))
          (v ∘
            (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) :
              (a : Fin n) → I))) :
      ExteriorAlgebra R M)
    (0 : ExteriorAlgebra R M)
have h : Fin.append
    (v ∘
      (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) :
        (a : Fin m) → I))
    (v ∘
      (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) :
        (a : Fin n) → I))
    (Fin.castAdd n j) =
  Fin.append
    (v ∘
      (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) :
        (a : Fin m) → I))
    (v ∘
      (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) :
        (a : Fin n) → I))
    (Fin.natAdd m k)
Tactic: apply AlternatingMap.map_eq_zero_of_eq (i := Fin.castAdd n j) (j := Fin.natAdd m k)
-- 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
m n : ℕ
I : Type u_1
inst_3 : LinearOrder I
v : I → M
s : (↑(powersetCard I m) : Type u_1)
t : (↑(powersetCard I n) : Type u_1)
i : I
his : i ∈ (↑s : Finset I)
hit : i ∈ (↑t : Finset I)
j : Fin m
hj :
  (((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) : (a : Fin m) → I)
      j =
    i
k : Fin n
hk :
  (((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) : (a : Fin n) → I)
      k =
    i
h :
  Fin.append
      (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) :
          (a : Fin m) → I))
      (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) :
          (a : Fin n) → I))
      (Fin.castAdd n j) =
    Fin.append
      (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) :
          (a : Fin m) → I))
      (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) :
          (a : Fin n) → I))
      (Fin.natAdd m k)
⊢ Eq (α := ExteriorAlgebra R M)
    ((ιMulti R (m + n) : (a : Fin (m + n) → M) → ExteriorAlgebra R M)
        (Fin.append
          (v ∘
            (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) :
              (a : Fin m) → I))
          (v ∘
            (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) :
              (a : Fin n) → I))) :
      ExteriorAlgebra R M)
    (0 : ExteriorAlgebra R M)
have hij : Fin.castAdd n j ≠ Fin.natAdd m k
Tactic: apply AlternatingMap.map_eq_zero_of_eq (i := Fin.castAdd n j) (j := Fin.natAdd m k)
-- 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
m n : ℕ
I : Type u_1
inst_3 : LinearOrder I
v : I → M
s : (↑(powersetCard I m) : Type u_1)
t : (↑(powersetCard I n) : Type u_1)
i : I
his : i ∈ (↑s : Finset I)
hit : i ∈ (↑t : Finset I)
j : Fin m
hj :
  (((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) : (a : Fin m) → I)
      j =
    i
k : Fin n
hk :
  (((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) : (a : Fin n) → I)
      k =
    i
⊢ Fin.castAdd n j ≠ Fin.natAdd m k
have hij : Fin.castAdd n j < Fin.natAdd m k
Tactic: apply ne_of_lt
-- 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
m n : ℕ
I : Type u_1
inst_3 : LinearOrder I
v : I → M
s : (↑(powersetCard I m) : Type u_1)
t : (↑(powersetCard I n) : Type u_1)
i : I
his : i ∈ (↑s : Finset I)
hit : i ∈ (↑t : Finset I)
j : Fin m
hj :
  (((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) : (a : Fin m) → I)
      j =
    i
k : Fin n
hk :
  (((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) : (a : Fin n) → I)
      k =
    i
⊢ Fin.castAdd n j < Fin.natAdd m k
have hij : (↑(Fin.castAdd n j) : ℕ) < m
Tactic: apply lt_of_lt_of_le (b := m)
-- 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
m n : ℕ
I : Type u_1
inst_3 : LinearOrder I
v : I → M
s : (↑(powersetCard I m) : Type u_1)
t : (↑(powersetCard I n) : Type u_1)
i : I
his : i ∈ (↑s : Finset I)
hit : i ∈ (↑t : Finset I)
j : Fin m
hj :
  (((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) : (a : Fin m) → I)
      j =
    i
k : Fin n
hk :
  (((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) : (a : Fin n) → I)
      k =
    i
hij : (↑(Fin.castAdd n j) : ℕ) < m
⊢ Fin.castAdd n j < Fin.natAdd m k
have hij₁ : m ≤ (↑(Fin.natAdd m k) : ℕ)
Tactic: apply lt_of_lt_of_le (b := m)
-- 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
m n : ℕ
I : Type u_1
inst_3 : LinearOrder I
v : I → M
s : (↑(powersetCard I m) : Type u_1)
t : (↑(powersetCard I n) : Type u_1)
h : Disjoint (↑s : Finset I) (↑t : Finset I)
⊢ HMul.hMul (α := ExteriorAlgebra R M) (ιMulti_family R m v s) (ιMulti_family R n v t) =
    HSMul.hSMul (α := ℤˣ) (β := ExteriorAlgebra R M)
      ((Equiv.Perm.sign : (a : Equiv.Perm (Fin (m + n))) → ℤˣ) (permOfDisjoint h) : ℤˣ)
      (ιMulti_family R (m + n) v (disjUnion h))
have simp : (ιMulti R (m + n) : (a : Fin (m + n) → M) → ExteriorAlgebra R M)
    (Fin.append
      (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) :
          (a : Fin m) → I))
      (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) :
          (a : Fin n) → I))) =
  HSMul.hSMul (α := ℤˣ) (β := ExteriorAlgebra R M)
    ((Equiv.Perm.sign : (a : Equiv.Perm (Fin (m + n))) → ℤˣ) (permOfDisjoint h) : ℤˣ)
    ((ιMulti R (m + n) : (a : Fin (m + n) → M) → ExteriorAlgebra R M)
        (v ∘
          (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I (m + n)) : Type u_1)) → Fin (m + n) ↪o I)
                  (disjUnion h) :
                Fin (m + n) ↪o I) :
            (a : Fin (m + n)) → I)) :
      ExteriorAlgebra R M)
Tactic: simp only [ιMulti_family, ιMulti_mul_ιMulti]