awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basis (goal)
Goal:
R : Type u_1
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_5
inst_3 : LinearOrder I
b : Basis I R M
s t : (↑(powersetCard I n) : Type u_5)
hst : s ≠ t
⊢ Eq.{u_1 + 1} (α := R)
    (((((Basis.exteriorPower n b).repr : (a : ↥(⋀[R]^n M)) → (↑(powersetCard I n) : Type u_5) →₀ R)
              (ιMulti_family R n (⇑b : (a : I) → M) t) :
            Finsupp.{u_5, u_1} (↑(powersetCard I n) : Type u_5) R) :
          (a : (↑(powersetCard I n) : Type u_5)) → R)
        s :
      R)
    ((ιMultiDual R n b s : (a : ↥(⋀[R]^n M)) → R) (ιMulti_family R n (⇑b : (a : I) → M) t) : R)
have neg : Eq.{u_1 + 1} (α := R)
  (((((Basis.exteriorPower n b).repr : (a : ↥(⋀[R]^n M)) → (↑(powersetCard I n) : Type u_5) →₀ R)
            (ιMulti_family R n (⇑b : (a : I) → M) t) :
          Finsupp.{u_5, u_1} (↑(powersetCard I n) : Type u_5) R) :
        (a : (↑(powersetCard I n) : Type u_5)) → R)
      s :
    R)
  (0 : R)
Tactic: rw [ιMultiDual_apply_nondiag R n b s t hst, ← basis_apply, Basis.repr_self,
      Finsupp.single_eq_of_ne hst]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basis (goal)
Goal:
R : Type u_1
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_5
inst_3 : LinearOrder I
b : Basis I R M
s t : (↑(powersetCard I n) : Type u_5)
hst : s ≠ t
neg :
  Eq.{u_1 + 1} (α := R)
    (((((Basis.exteriorPower n b).repr : (a : ↥(⋀[R]^n M)) → (↑(powersetCard I n) : Type u_5) →₀ R)
              (ιMulti_family R n (⇑b : (a : I) → M) t) :
            Finsupp.{u_5, u_1} (↑(powersetCard I n) : Type u_5) R) :
          (a : (↑(powersetCard I n) : Type u_5)) → R)
        s :
      R)
    (0 : R)
⊢ Eq.{u_1 + 1} (α := R)
    (((((Basis.exteriorPower n b).repr : (a : ↥(⋀[R]^n M)) → (↑(powersetCard I n) : Type u_5) →₀ R)
              (ιMulti_family R n (⇑b : (a : I) → M) t) :
            Finsupp.{u_5, u_1} (↑(powersetCard I n) : Type u_5) R) :
          (a : (↑(powersetCard I n) : Type u_5)) → R)
        s :
      R)
    ((ιMultiDual R n b s : (a : ↥(⋀[R]^n M)) → R) (ιMulti_family R n (⇑b : (a : I) → M) t) : R)
have neg₁ : Eq.{u_1 + 1} (α := R)
  (((((Basis.exteriorPower n b).repr : (a : ↥(⋀[R]^n M)) → (↑(powersetCard I n) : Type u_5) →₀ R)
            ((Basis.exteriorPower n b : (a : (↑(powersetCard I n) : Type u_5)) → ↥(⋀[R]^n M)) t) :
          Finsupp.{u_5, u_1} (↑(powersetCard I n) : Type u_5) R) :
        (a : (↑(powersetCard I n) : Type u_5)) → R)
      s :
    R)
  (0 : R)
Tactic: rw [ιMultiDual_apply_nondiag R n b s t hst, ← basis_apply, Basis.repr_self,
      Finsupp.single_eq_of_ne hst]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basis (goal)
Goal:
R : Type u_1
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_5
inst_3 : LinearOrder I
b : Basis I R M
s t : (↑(powersetCard I n) : Type u_5)
hst : s ≠ t
neg :
  Eq.{u_1 + 1} (α := R)
    (((((Basis.exteriorPower n b).repr : (a : ↥(⋀[R]^n M)) → (↑(powersetCard I n) : Type u_5) →₀ R)
              (ιMulti_family R n (⇑b : (a : I) → M) t) :
            Finsupp.{u_5, u_1} (↑(powersetCard I n) : Type u_5) R) :
          (a : (↑(powersetCard I n) : Type u_5)) → R)
        s :
      R)
    (0 : R)
neg₁ :
  Eq.{u_1 + 1} (α := R)
    (((((Basis.exteriorPower n b).repr : (a : ↥(⋀[R]^n M)) → (↑(powersetCard I n) : Type u_5) →₀ R)
              ((Basis.exteriorPower n b : (a : (↑(powersetCard I n) : Type u_5)) → ↥(⋀[R]^n M)) t) :
            Finsupp.{u_5, u_1} (↑(powersetCard I n) : Type u_5) R) :
          (a : (↑(powersetCard I n) : Type u_5)) → R)
        s :
      R)
    (0 : R)
⊢ Eq.{u_1 + 1} (α := R)
    (((((Basis.exteriorPower n b).repr : (a : ↥(⋀[R]^n M)) → (↑(powersetCard I n) : Type u_5) →₀ R)
              (ιMulti_family R n (⇑b : (a : I) → M) t) :
            Finsupp.{u_5, u_1} (↑(powersetCard I n) : Type u_5) R) :
          (a : (↑(powersetCard I n) : Type u_5)) → R)
        s :
      R)
    ((ιMultiDual R n b s : (a : ↥(⋀[R]^n M)) → R) (ιMulti_family R n (⇑b : (a : I) → M) t) : R)
have neg₂ : Eq.{u_1 + 1} (α := R) ((Finsupp.single t 1 : (a : (↑(powersetCard I n) : Type u_5)) → R) s : R) (0 : R)
Tactic: rw [ιMultiDual_apply_nondiag R n b s t hst, ← basis_apply, Basis.repr_self,
      Finsupp.single_eq_of_ne hst]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basis (goal)
Goal:
R : Type u_1
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_5
inst_3 : LinearOrder I
b : Basis I R M
s t : (↑(powersetCard I n) : Type u_5)
hst : s ≠ t
neg :
  Eq.{u_1 + 1} (α := R)
    (((((Basis.exteriorPower n b).repr : (a : ↥(⋀[R]^n M)) → (↑(powersetCard I n) : Type u_5) →₀ R)
              (ιMulti_family R n (⇑b : (a : I) → M) t) :
            Finsupp.{u_5, u_1} (↑(powersetCard I n) : Type u_5) R) :
          (a : (↑(powersetCard I n) : Type u_5)) → R)
        s :
      R)
    (0 : R)
neg₁ :
  Eq.{u_1 + 1} (α := R)
    (((((Basis.exteriorPower n b).repr : (a : ↥(⋀[R]^n M)) → (↑(powersetCard I n) : Type u_5) →₀ R)
              ((Basis.exteriorPower n b : (a : (↑(powersetCard I n) : Type u_5)) → ↥(⋀[R]^n M)) t) :
            Finsupp.{u_5, u_1} (↑(powersetCard I n) : Type u_5) R) :
          (a : (↑(powersetCard I n) : Type u_5)) → R)
        s :
      R)
    (0 : R)
neg₂ : Eq.{u_1 + 1} (α := R) ((Finsupp.single t 1 : (a : (↑(powersetCard I n) : Type u_5)) → R) s : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R)
    (((((Basis.exteriorPower n b).repr : (a : ↥(⋀[R]^n M)) → (↑(powersetCard I n) : Type u_5) →₀ R)
              (ιMulti_family R n (⇑b : (a : I) → M) t) :
            Finsupp.{u_5, u_1} (↑(powersetCard I n) : Type u_5) R) :
          (a : (↑(powersetCard I n) : Type u_5)) → R)
        s :
      R)
    ((ιMultiDual R n b s : (a : ↥(⋀[R]^n M)) → R) (ιMulti_family R n (⇑b : (a : I) → M) t) : R)
have neg₃ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [ιMultiDual_apply_nondiag R n b s t hst, ← basis_apply, Basis.repr_self,
      Finsupp.single_eq_of_ne hst]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basis (goal)
Goal:
R : Type u_1
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_5
inst_3 : LinearOrder I
b : Basis I R M
s : (↑(powersetCard I n) : Type u_5)
⊢ Eq (α := Finsupp.{u_5, u_1} (↑(powersetCard I n) : Type u_5) R)
    (((Basis.exteriorPower n b).repr : (a : ↥(⋀[R]^n M)) → (↑(powersetCard I n) : Type u_5) →₀ R)
        (ιMulti_family R n (⇑b : (a : I) → M) s) :
      Finsupp.{u_5, u_1} (↑(powersetCard I n) : Type u_5) R)
    (Finsupp.single s 1 : Finsupp.{u_5, u_1} (↑(powersetCard I n) : Type u_5) R)
have h : ∀ (t : (↑(powersetCard I n) : Type u_5)),
  Eq.{u_1 + 1} (α := R)
    (((((Basis.exteriorPower n b).repr : (a : ↥(⋀[R]^n M)) → (↑(powersetCard I n) : Type u_5) →₀ R)
              (ιMulti_family R n (⇑b : (a : I) → M) s) :
            Finsupp.{u_5, u_1} (↑(powersetCard I n) : Type u_5) R) :
          (a : (↑(powersetCard I n) : Type u_5)) → R)
        t :
      R)
    ((Finsupp.single s 1 : (a : (↑(powersetCard I n) : Type u_5)) → R) t : R)
Tactic: ext t
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basis (goal)
Goal:
R : Type u_1
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_5
inst_3 : LinearOrder I
b : Basis I R M
s t : (↑(powersetCard I n) : Type u_5)
⊢ Eq.{u_1 + 1} (α := R)
    (((((Basis.exteriorPower n b).repr : (a : ↥(⋀[R]^n M)) → (↑(powersetCard I n) : Type u_5) →₀ R)
              (ιMulti_family R n (⇑b : (a : I) → M) s) :
            Finsupp.{u_5, u_1} (↑(powersetCard I n) : Type u_5) R) :
          (a : (↑(powersetCard I n) : Type u_5)) → R)
        t :
      R)
    ((Finsupp.single s 1 : (a : (↑(powersetCard I n) : Type u_5)) → R) t : R)
have pos : ∀ (hst : s = t),
  Eq.{u_1 + 1} (α := R)
    (((((Basis.exteriorPower n b).repr : (a : ↥(⋀[R]^n M)) → (↑(powersetCard I n) : Type u_5) →₀ R)
              (ιMulti_family R n (⇑b : (a : I) → M) s) :
            Finsupp.{u_5, u_1} (↑(powersetCard I n) : Type u_5) R) :
          (a : (↑(powersetCard I n) : Type u_5)) → R)
        t :
      R)
    ((Finsupp.single s 1 : (a : (↑(powersetCard I n) : Type u_5)) → R) t : R)
Tactic: by_cases hst : s = t
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basis (goal)
Goal:
R : Type u_1
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_5
inst_3 : LinearOrder I
b : Basis I R M
s t : (↑(powersetCard I n) : Type u_5)
pos :
  ∀ (hst : s = t),
    Eq.{u_1 + 1} (α := R)
      (((((Basis.exteriorPower n b).repr : (a : ↥(⋀[R]^n M)) → (↑(powersetCard I n) : Type u_5) →₀ R)
                (ιMulti_family R n (⇑b : (a : I) → M) s) :
              Finsupp.{u_5, u_1} (↑(powersetCard I n) : Type u_5) R) :
            (a : (↑(powersetCard I n) : Type u_5)) → R)
          t :
        R)
      ((Finsupp.single s 1 : (a : (↑(powersetCard I n) : Type u_5)) → R) t : R)
⊢ Eq.{u_1 + 1} (α := R)
    (((((Basis.exteriorPower n b).repr : (a : ↥(⋀[R]^n M)) → (↑(powersetCard I n) : Type u_5) →₀ R)
              (ιMulti_family R n (⇑b : (a : I) → M) s) :
            Finsupp.{u_5, u_1} (↑(powersetCard I n) : Type u_5) R) :
          (a : (↑(powersetCard I n) : Type u_5)) → R)
        t :
      R)
    ((Finsupp.single s 1 : (a : (↑(powersetCard I n) : Type u_5)) → R) t : R)
have neg : ∀ (hst : ¬s = t),
  Eq.{u_1 + 1} (α := R)
    (((((Basis.exteriorPower n b).repr : (a : ↥(⋀[R]^n M)) → (↑(powersetCard I n) : Type u_5) →₀ R)
              (ιMulti_family R n (⇑b : (a : I) → M) s) :
            Finsupp.{u_5, u_1} (↑(powersetCard I n) : Type u_5) R) :
          (a : (↑(powersetCard I n) : Type u_5)) → R)
        t :
      R)
    ((Finsupp.single s 1 : (a : (↑(powersetCard I n) : Type u_5)) → R) t : R)
Tactic: by_cases hst : s = t
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basis (goal)
Goal:
R : Type u_1
K : Type u_2
M : Type u_3
E : Type u_4
n : ℕ
inst : CommRing R
inst_1 : Field K
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup E
inst_5 : Module K E
inst_6 : Free R M
⊢ Free R ↥(⋀[R]^n M)
have have : ∀ (I : Type u_3) (b : Basis I R M), Free R ↥(⋀[R]^n M)
Tactic: have ⟨I, b⟩ := Module.Free.exists_basis R M
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basis (goal)
Goal:
R : Type u_1
K : Type u_2
M : Type u_3
E : Type u_4
n : ℕ
inst : CommRing R
inst_1 : Field K
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup E
inst_5 : Module K E
inst_6 : Free R M
⊢ Free R ↥(⋀[R]^n M)
have have : ∀ (I : Type u_3) (b : Basis I R M), Free R ↥(⋀[R]^n M)
Tactic: classical
  have ⟨I, b⟩ := Module.Free.exists_basis R M
  letI : LinearOrder I := linearOrderOfSTO WellOrderingRel
  exact Module.Free.of_basis (b.exteriorPower n)
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basis (goal)
Goal:
R : Type u_1
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
inst_4 : Free R M
inst_5 : Module.Finite R M
this : LinearOrder (Free.ChooseBasisIndex R M) := linearOrderOfSTO WellOrderingRel
B : Basis (↑(powersetCard (Free.ChooseBasisIndex R M) n) : Type u_3) R ↥(⋀[R]^n M) :=
  Basis.exteriorPower n (Free.chooseBasis R M)
⊢ finrank R ↥(⋀[R]^n M) = (finrank R M).choose n
have rw : finrank R ↥(⋀[R]^n M) = (Fintype.card.{u_3} (Free.ChooseBasisIndex R M)).choose n
Tactic: rw [Module.finrank_eq_card_basis (Module.Free.chooseBasis R M), Module.finrank_eq_card_basis B,
    Fintype.card_eq_nat_card, powersetCard.card, Fintype.card_eq_nat_card]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basis (goal)
Goal:
R : Type u_1
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
inst_4 : Free R M
inst_5 : Module.Finite R M
this : LinearOrder (Free.ChooseBasisIndex R M) := linearOrderOfSTO WellOrderingRel
B : Basis (↑(powersetCard (Free.ChooseBasisIndex R M) n) : Type u_3) R ↥(⋀[R]^n M) :=
  Basis.exteriorPower n (Free.chooseBasis R M)
rw : finrank R ↥(⋀[R]^n M) = (Fintype.card.{u_3} (Free.ChooseBasisIndex R M)).choose n
⊢ finrank R ↥(⋀[R]^n M) = (finrank R M).choose n
have rw₁ : Fintype.card.{u_3} (↑(powersetCard (Free.ChooseBasisIndex R M) n) : Type u_3) =
  (Fintype.card.{u_3} (Free.ChooseBasisIndex R M)).choose n
Tactic: rw [Module.finrank_eq_card_basis (Module.Free.chooseBasis R M), Module.finrank_eq_card_basis B,
    Fintype.card_eq_nat_card, powersetCard.card, Fintype.card_eq_nat_card]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basis (goal)
Goal:
R : Type u_1
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
inst_4 : Free R M
inst_5 : Module.Finite R M
this : LinearOrder (Free.ChooseBasisIndex R M) := linearOrderOfSTO WellOrderingRel
B : Basis (↑(powersetCard (Free.ChooseBasisIndex R M) n) : Type u_3) R ↥(⋀[R]^n M) :=
  Basis.exteriorPower n (Free.chooseBasis R M)
rw : finrank R ↥(⋀[R]^n M) = (Fintype.card.{u_3} (Free.ChooseBasisIndex R M)).choose n
rw₁ :
  Fintype.card.{u_3} (↑(powersetCard (Free.ChooseBasisIndex R M) n) : Type u_3) =
    (Fintype.card.{u_3} (Free.ChooseBasisIndex R M)).choose n
⊢ finrank R ↥(⋀[R]^n M) = (finrank R M).choose n
have rw₂ : Nat.card.{u_3} (↑(powersetCard (Free.ChooseBasisIndex R M) n) : Type u_3) =
  (Fintype.card.{u_3} (Free.ChooseBasisIndex R M)).choose n
Tactic: rw [Module.finrank_eq_card_basis (Module.Free.chooseBasis R M), Module.finrank_eq_card_basis B,
    Fintype.card_eq_nat_card, powersetCard.card, Fintype.card_eq_nat_card]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basis (goal)
Goal:
R : Type u_1
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
inst_4 : Free R M
inst_5 : Module.Finite R M
this : LinearOrder (Free.ChooseBasisIndex R M) := linearOrderOfSTO WellOrderingRel
B : Basis (↑(powersetCard (Free.ChooseBasisIndex R M) n) : Type u_3) R ↥(⋀[R]^n M) :=
  Basis.exteriorPower n (Free.chooseBasis R M)
rw : finrank R ↥(⋀[R]^n M) = (Fintype.card.{u_3} (Free.ChooseBasisIndex R M)).choose n
rw₁ :
  Fintype.card.{u_3} (↑(powersetCard (Free.ChooseBasisIndex R M) n) : Type u_3) =
    (Fintype.card.{u_3} (Free.ChooseBasisIndex R M)).choose n
rw₂ :
  Nat.card.{u_3} (↑(powersetCard (Free.ChooseBasisIndex R M) n) : Type u_3) =
    (Fintype.card.{u_3} (Free.ChooseBasisIndex R M)).choose n
⊢ finrank R ↥(⋀[R]^n M) = (finrank R M).choose n
have rw₃ : (Nat.card.{u_3} (Free.ChooseBasisIndex R M)).choose n = (Fintype.card.{u_3} (Free.ChooseBasisIndex R M)).choose n
Tactic: rw [Module.finrank_eq_card_basis (Module.Free.chooseBasis R M), Module.finrank_eq_card_basis B,
    Fintype.card_eq_nat_card, powersetCard.card, Fintype.card_eq_nat_card]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basis (goal)
Goal:
R : Type u_1
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
inst_4 : Free R M
inst_5 : Module.Finite R M
this : LinearOrder (Free.ChooseBasisIndex R M) := linearOrderOfSTO WellOrderingRel
B : Basis (↑(powersetCard (Free.ChooseBasisIndex R M) n) : Type u_3) R ↥(⋀[R]^n M) :=
  Basis.exteriorPower n (Free.chooseBasis R M)
rw : finrank R ↥(⋀[R]^n M) = (Fintype.card.{u_3} (Free.ChooseBasisIndex R M)).choose n
rw₁ :
  Fintype.card.{u_3} (↑(powersetCard (Free.ChooseBasisIndex R M) n) : Type u_3) =
    (Fintype.card.{u_3} (Free.ChooseBasisIndex R M)).choose n
rw₂ :
  Nat.card.{u_3} (↑(powersetCard (Free.ChooseBasisIndex R M) n) : Type u_3) =
    (Fintype.card.{u_3} (Free.ChooseBasisIndex R M)).choose n
rw₃ : (Nat.card.{u_3} (Free.ChooseBasisIndex R M)).choose n = (Fintype.card.{u_3} (Free.ChooseBasisIndex R M)).choose n
⊢ finrank R ↥(⋀[R]^n M) = (finrank R M).choose n
have rw₄ : (Nat.card.{u_3} (Free.ChooseBasisIndex R M)).choose n = (Nat.card.{u_3} (Free.ChooseBasisIndex R M)).choose n
Tactic: rw [Module.finrank_eq_card_basis (Module.Free.chooseBasis R M), Module.finrank_eq_card_basis B,
    Fintype.card_eq_nat_card, powersetCard.card, Fintype.card_eq_nat_card]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basis (goal)
Goal:
K : Type u_2
E : Type u_4
n : ℕ
inst : Field K
inst_1 : AddCommGroup E
inst_2 : Module K E
I : Type u_5
inst_3 : LinearOrder I
v : I → E
hv : LinearIndependent K v
W : Submodule K E := Submodule.span K (range v)
this : ∃ (b : Basis.{u_5, u_2, u_4} I K ↥W), v = Function.comp (β := ↥W) (⇑W.subtype : (a : ↥W) → E) (⇑b : (a : I) → ↥W)
⊢ LinearIndependent K (M := ↥(⋀[K]^n E)) (ιMulti_family K n v)
have obtain : ∀ (b : Basis.{u_5, u_2, u_4} I K ↥W) (hb : v = Function.comp (β := ↥W) (⇑W.subtype : (a : ↥W) → E) (⇑b : (a : I) → ↥W)),
  LinearIndependent K (M := ↥(⋀[K]^n E)) (ιMulti_family K n v)
Tactic: obtain ⟨b, hb⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basis (goal)
Goal:
K : Type u_2
E : Type u_4
n : ℕ
inst : Field K
inst_1 : AddCommGroup E
inst_2 : Module K E
I : Type u_5
inst_3 : LinearOrder I
v : I → E
hv : LinearIndependent K v
W : Submodule K E := Submodule.span K (range v)
b : Basis.{u_5, u_2, u_4} I K ↥W
hb : v = Function.comp (β := ↥W) (⇑W.subtype : (a : ↥W) → E) (⇑b : (a : I) → ↥W)
⊢ LinearIndependent K (M := ↥(⋀[K]^n E)) (ιMulti_family K n v)
have rw : LinearIndependent (ι := (↑(powersetCard I n) : Type u_5)) K (M := ↥(⋀[K]^n E))
  (Function.comp (β := ↥(⋀[K]^n ↥W)) (⇑(map n W.subtype) : (a : ↥(⋀[K]^n ↥W)) → ↥(⋀[K]^n E))
    (ιMulti_family K n (⇑b : (a : I) → ↥W)))
Tactic: rw [hb, ← map_comp_ιMulti_family]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basis (goal)
Goal:
K : Type u_2
E : Type u_4
n : ℕ
inst : Field K
inst_1 : AddCommGroup E
inst_2 : Module K E
I : Type u_5
inst_3 : LinearOrder I
v : I → E
hv : LinearIndependent K v
W : Submodule K E := Submodule.span K (range v)
⊢ LinearIndependent K (M := ↥(⋀[K]^n E)) (ιMulti_family K n v)
have suffices : ∃ (b : Basis.{u_5, u_2, u_4} I K ↥W), v = Function.comp (β := ↥W) (⇑W.subtype : (a : ↥W) → E) (⇑b : (a : I) → ↥W)
Tactic: suffices ∃ b : Basis I K W, v = W.subtype ∘ b by
    obtain ⟨b, hb⟩ := this
    rw [hb, ← map_comp_ιMulti_family]
    exact LinearIndependent.map' (coe_basis K n b ▸ (b.exteriorPower n).linearIndependent)
      _ (LinearMap.ker_eq_bot.mpr (map_injective_field (Submodule.subtype_injective _)))
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basis (goal)
Goal:
K : Type u_2
E : Type u_4
n : ℕ
inst : Field K
inst_1 : AddCommGroup E
inst_2 : Module K E
I : Type u_5
inst_3 : LinearOrder I
v : I → E
hv : LinearIndependent K v
W : Submodule K E := Submodule.span K (range v)
⊢ ∃ (b : Basis.{u_5, u_2, u_4} I K ↥W), v = Function.comp (β := ↥W) (⇑W.subtype : (a : ↥W) → E) (⇑b : (a : I) → ↥W)
have h : v = Function.comp (β := ↥W) (⇑W.subtype : (a : ↥W) → E) (⇑(Basis.span hv) : (a : I) → ↥W)
Tactic: use Module.Basis.span hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basis (goal)
Goal:
K : Type u_2
E : Type u_4
n : ℕ
inst : Field K
inst_1 : AddCommGroup E
inst_2 : Module K E
I : Type u_5
inst_3 : LinearOrder I
v : I → E
hv : LinearIndependent K v
W : Submodule K E := Submodule.span K (range v)
⊢ v = Function.comp (β := ↥W) (⇑W.subtype : (a : ↥W) → E) (⇑(Basis.span hv) : (a : I) → ↥W)
have h : ∀ (i : I), v i = Function.comp (β := ↥W) (⇑W.subtype : (a : ↥W) → E) (⇑(Basis.span hv) : (a : I) → ↥W) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basis (goal)
Goal:
K : Type u_2
E : Type u_4
n : ℕ
inst : Field K
inst_1 : AddCommGroup E
inst_2 : Module K E
I : Type u_5
inst_3 : LinearOrder I
v : I → E
hv : LinearIndependent K v
W : Submodule K E := Submodule.span K (range v)
i : I
⊢ v i = Function.comp (β := ↥W) (⇑W.subtype : (a : ↥W) → E) (⇑(Basis.span hv) : (a : I) → ↥W) i
have h : v i = Function.comp (β := ↥W) (Subtype.val (p := fun (x : E) ↦ x ∈ W)) (⇑(Basis.span hv) : (a : I) → ↥W) i
Tactic: rw [Submodule.coe_subtype, Function.comp_apply, Basis.span_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basis (goal)
Goal:
K : Type u_2
E : Type u_4
n : ℕ
inst : Field K
inst_1 : AddCommGroup E
inst_2 : Module K E
I : Type u_5
inst_3 : LinearOrder I
v : I → E
hv : LinearIndependent K v
W : Submodule K E := Submodule.span K (range v)
i : I
h : v i = Function.comp (β := ↥W) (Subtype.val (p := fun (x : E) ↦ x ∈ W)) (⇑(Basis.span hv) : (a : I) → ↥W) i
⊢ v i = Function.comp (β := ↥W) (⇑W.subtype : (a : ↥W) → E) (⇑(Basis.span hv) : (a : I) → ↥W) i
have h₁ : v i = (↑((Basis.span hv : (a : I) → ↥W) i) : E)
Tactic: rw [Submodule.coe_subtype, Function.comp_apply, Basis.span_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basis (goal)
Goal:
K : Type u_2
E : Type u_4
n : ℕ
inst : Field K
inst_1 : AddCommGroup E
inst_2 : Module K E
I : Type u_5
inst_3 : LinearOrder I
v : I → E
hv : LinearIndependent K v
W : Submodule K E := Submodule.span K (range v)
i : I
h : v i = Function.comp (β := ↥W) (Subtype.val (p := fun (x : E) ↦ x ∈ W)) (⇑(Basis.span hv) : (a : I) → ↥W) i
h₁ : v i = (↑((Basis.span hv : (a : I) → ↥W) i) : E)
⊢ v i = Function.comp (β := ↥W) (⇑W.subtype : (a : ↥W) → E) (⇑(Basis.span hv) : (a : I) → ↥W) i
have h₂ : v i =
  (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Submodule K E) (Submodule.span K (range v)) x) (v i) sorry) : E)
Tactic: rw [Submodule.coe_subtype, Function.comp_apply, Basis.span_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
f : Fin n → Module.Dual R M
i j : Fin n
hf : f i = f j
hij : i ≠ j
⊢ MultilinearMap.toFun (M₁ := fun (x : Fin n) ↦ Module.Dual R M)
      (LinearMap.compMultilinearMap (M₁ := fun (x : Fin n) ↦ Module.Dual R M) (LinearMap.dualMap (toTensorPower R M n))
        (TensorPower.multilinearMapToDual R M n))
      f =
    0
have heq : ∀ (v : Fin n → M),
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.compAlternatingMap
            (MultilinearMap.toFun (M₁ := fun (x : Fin n) ↦ Module.Dual R M)
              (LinearMap.compMultilinearMap (M₁ := fun (x : Fin n) ↦ Module.Dual R M)
                (LinearMap.dualMap (toTensorPower R M n)) (TensorPower.multilinearMapToDual R M n))
              f)
            (ιMulti R n) :
          (a : Fin n → M) → R)
        v :
      R)
    ((LinearMap.compAlternatingMap 0 (ιMulti R n) : (a : Fin n → M) → R) v : R)
Tactic: ext v
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
f : Fin n → Module.Dual R M
i j : Fin n
hf : f i = f j
hij : i ≠ j
v : Fin n → M
⊢ Eq.{u_1 + 1} (α := R)
    ((LinearMap.compAlternatingMap
            (MultilinearMap.toFun (M₁ := fun (x : Fin n) ↦ Module.Dual R M)
              (LinearMap.compMultilinearMap (M₁ := fun (x : Fin n) ↦ Module.Dual R M)
                (LinearMap.dualMap (toTensorPower R M n)) (TensorPower.multilinearMapToDual R M n))
              f)
            (ιMulti R n) :
          (a : Fin n → M) → R)
        v :
      R)
    ((LinearMap.compAlternatingMap 0 (ιMulti R n) : (a : Fin n → M) → R) v : R)
have heq : Eq.{u_1 + 1} (α := R)
  (Matrix.det (n := Fin n)
    ((Matrix.of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦ (f j : (a : M) → R) (v i)))
  0
Tactic: suffices Matrix.det (n := Fin n) (.of (fun i j ↦ f j (v i))) = 0 by
      simpa [Matrix.det_apply] using this