awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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.ofFn ((⇑(ι R) : (a : M) → ExteriorAlgebra R M) ∘ a)))
      (List.prod (List.ofFn ((⇑(ι R) : (a : M) → ExteriorAlgebra R M) ∘ b)))

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
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)
⊢ Set.range (ι := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M) ⊆
    (↑(⋀[R]^n M) : Set (ExteriorAlgebra R M))

Tactic:
rw [Set.range_subset_iff]

Premises used: Set.range_subset_iff
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
v : Fin n → M
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))
⊢ 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)

Tactic:
rw [ιMulti_apply]

Premises used: ExteriorAlgebra.ιMulti_apply
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
v : Fin n → M
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
⊢ 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:
apply Submodule.pow_subset_pow

Premises used: Submodule.pow_subset_pow
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
v : Fin n → M
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)))
⊢ 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:
rw [Set.mem_pow]

Premises used: Set.mem_pow
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
v : Fin n → M
⊢ ∃ (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:
⟨fun i => ⟨ι R (v i), LinearMap.mem_range_self _ _⟩, rfl⟩

Premises used: LinearMap.mem_range_self, Subtype.mk, ExteriorAlgebra.ι, Exists.intro, DFunLike.coe, rfl
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
v : Fin n → M
⊢ ∃ (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:
exact ⟨fun i => ⟨ι R (v i), LinearMap.mem_range_self _ _⟩, rfl⟩
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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)

Tactic:
le_antisymm (Submodule.span_le.2 (ιMulti_range R n)) ?_

Premises used: Iff.mpr, ExteriorAlgebra.ιMulti_range, le_antisymm, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
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)))
⊢ 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)

Tactic:
refine le_antisymm (Submodule.span_le.2 (ιMulti_range R n)) ?_

Premises used: Iff.mpr, ExteriorAlgebra.ιMulti_range, le_antisymm, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
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))
⊢ 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:
rw [exteriorPower, Submodule.pow_eq_span_pow_set, Submodule.span_le]

Premises used: Submodule.pow_eq_span_pow_set, ExteriorAlgebra.exteriorPower, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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))

Tactic:
fun u hu ↦ Submodule.subset_span ?_

Premises used: Set.Mem, Set.Subset, Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
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
⊢ (↑(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:
refine fun u hu ↦ Submodule.subset_span ?_

Premises used: Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
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)))
⊢ Membership.mem (γ := Set (ExteriorAlgebra R M))
    (Set.range (ι := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)) u

Tactic:
obtain ⟨f, rfl⟩ := Set.mem_pow.mp hu

Premises used: Iff.mp, Set.mem_pow, rfl
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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)))

Tactic:
⟨fun i => ιInv (f i).1, ?_⟩

Premises used: Set.Mem, setOf, ExteriorAlgebra.ιInv, Exists.intro, Set.range, Subtype.val, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
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)))
⊢ 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:
refine ⟨fun i => ιInv (f i).1, ?_⟩
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
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)))
⊢ 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:
rw [ιMulti_apply]

Premises used: ExteriorAlgebra.ιMulti_apply
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
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)
⊢ 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:
congr with i
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
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)
⊢ (ι 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

Premises used: Subtype.prop
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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)
e_xs₁ 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)
⊢ (ι R : (a : M) → ExteriorAlgebra R M) ((ιInv : (a : ExteriorAlgebra R M) → M) (↑(f i) : ExteriorAlgebra R M)) =
    (↑(f i) : ExteriorAlgebra R M)

Tactic:
rw [← hv, ι_leftInverse]

Premises used: ExteriorAlgebra.ι_leftInverse
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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)
⊢ ∃ a ∈ (↑s : Finset I), a ∈ (↑t : Finset I)

Tactic:
rw [Finset.not_disjoint_iff] at h

Premises used: Finset.not_disjoint_iff
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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)
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
⊢ HMul.hMul (α := ExteriorAlgebra R M) (ιMulti_family R m v s) (ιMulti_family R n v t) = 0

Tactic:
obtain ⟨i, his, hit⟩ := h
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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)
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
⊢ 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

Premises used: Iff.mpr, Set.powersetCard.mem_range_ofFinEmbEquiv_symm_iff_mem
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
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
⊢ 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

Premises used: Iff.mpr, Set.powersetCard.mem_range_ofFinEmbEquiv_symm_iff_mem
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
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)
⊢ HMul.hMul (α := ExteriorAlgebra R M) (ιMulti_family R m v s) (ιMulti_family R n v t) = 0

Tactic:
simp only [ιMulti_family, ιMulti_mul_ιMulti]

Premises used: ExteriorAlgebra.ιMulti_mul_ιMulti, ExteriorAlgebra.ιMulti_family
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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)
hij : Fin.castAdd n j ≠ 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)

Tactic:
apply AlternatingMap.map_eq_zero_of_eq (i := Fin.castAdd n j) (j := Fin.natAdd m k)

Premises used: AlternatingMap.map_eq_zero_of_eq
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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.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:
simp [hj, hk]
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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 < Fin.natAdd m k
⊢ Fin.castAdd n j ≠ Fin.natAdd m k

Tactic:
apply ne_of_lt

Premises used: ne_of_lt
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
hij₁ : m ≤ (↑(Fin.natAdd m k) : ℕ)
⊢ Fin.castAdd n j < Fin.natAdd m k

Tactic:
apply lt_of_lt_of_le (b := m)

Premises used: lt_of_lt_of_le
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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) : ℕ) < m

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
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
⊢ m ≤ (↑(Fin.natAdd m k) : ℕ)

Tactic:
simp