awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basis
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)
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)
⊢ 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
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basis
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) 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:
simp [hst]
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basis
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) 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:
simp [hst]
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basis
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
have : ∀ (I : Type u_3) (b : Basis I R M), Free R ↥(⋀[R]^n M)
⊢ Free R ↥(⋀[R]^n M)

Tactic:
have ⟨I, b⟩ := Module.Free.exists_basis R M
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basis
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
I : Type u_3
b : Basis I R M
this : LinearOrder I := linearOrderOfSTO WellOrderingRel
⊢ Free R ↥(⋀[R]^n M)

Tactic:
Module.Free.of_basis (b.exteriorPower n)

Premises used: Module.Basis.exteriorPower, Module.Free.of_basis
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basis
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
I : Type u_3
b : Basis I R M
this : LinearOrder I := linearOrderOfSTO WellOrderingRel
⊢ Free R ↥(⋀[R]^n M)

Tactic:
exact Module.Free.of_basis (b.exteriorPower n)

Premises used: Module.Basis.exteriorPower, Module.Free.of_basis
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basis
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
have have₁ have₂ have₃ : ∀ (I : Type u_3) (b : Basis I R M), Free R ↥(⋀[R]^n 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)
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basis
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
rw₄ rw₅ : (Nat.card.{u_3} (Free.ChooseBasisIndex R M)).choose n = (Nat.card.{u_3} (Free.ChooseBasisIndex R M)).choose n
⊢ finrank R ↥(⋀[R]^n M) = (finrank 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]

Premises used: Module.finrank_eq_card_basis, Set.powersetCard.card, Fintype.card_eq_nat_card, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basis
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
let let₁ let₂ let₃ : finrank R ↥(⋀[R]^n M) = (finrank R M).choose n
⊢ finrank R ↥(⋀[R]^n M) = (finrank R M).choose n

Tactic:
classical
  let : LinearOrder (Module.Free.ChooseBasisIndex R M) := linearOrderOfSTO WellOrderingRel
  let B := (Module.Free.chooseBasis R M).exteriorPower n
  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]

Premises used: Module.finrank_eq_card_basis, Set.powersetCard.card, Fintype.card_eq_nat_card, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basis
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)
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)
⊢ LinearIndependent K (M := ↥(⋀[K]^n E)) (ιMulti_family K n v)

Tactic:
obtain ⟨b, hb⟩ := this
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basis
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)
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)))
⊢ LinearIndependent K (M := ↥(⋀[K]^n E)) (ιMulti_family K n v)

Tactic:
rw [hb, ← map_comp_ιMulti_family]

Premises used: exteriorPower.map_comp_ιMulti_family
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basis
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 (ι := (↑(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:
LinearIndependent.map' (coe_basis K n b ▸ (b.exteriorPower n).linearIndependent)
      _ (LinearMap.ker_eq_bot.mpr (map_injective_field (Submodule.subtype_injective _)))

Premises used: Iff.mpr, Set.Mem, LinearMap.ker_eq_bot, LinearIndependent.map', exteriorPower.map_injective_field, Submodule.subtype_injective
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basis
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 (ι := (↑(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:
exact LinearIndependent.map' (coe_basis K n b ▸ (b.exteriorPower n).linearIndependent)
      _ (LinearMap.ker_eq_bot.mpr (map_injective_field (Submodule.subtype_injective _)))

Premises used: Iff.mpr, LinearMap.ker_eq_bot, LinearIndependent.map', exteriorPower.map_injective_field, Submodule.subtype_injective
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basis
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)
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)
⊢ LinearIndependent K (M := ↥(⋀[K]^n E)) (ιMulti_family K n v)

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 _)))
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basis
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)
h : v = Function.comp (β := ↥W) (⇑W.subtype : (a : ↥W) → E) (⇑(Basis.span hv) : (a : I) → ↥W)
⊢ ∃ (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:
use Module.Basis.span hv

Premises used: Module.Basis.span
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basis
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)
h : ∀ (i : I), v i = Function.comp (β := ↥W) (⇑W.subtype : (a : ↥W) → E) (⇑(Basis.span hv) : (a : I) → ↥W) i
⊢ v = Function.comp (β := ↥W) (⇑W.subtype : (a : ↥W) → E) (⇑(Basis.span hv) : (a : I) → ↥W)

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basis
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)
h₂ h₃ :
  v i =
    (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Submodule K E) (Submodule.span K (range v)) x) (v i) ⋯) : E)
⊢ v i = Function.comp (β := ↥W) (⇑W.subtype : (a : ↥W) → E) (⇑(Basis.span hv) : (a : I) → ↥W) i

Tactic:
rw [Submodule.coe_subtype, Function.comp_apply, Basis.span_apply]

Premises used: Module.Basis.span_apply, Submodule.coe_subtype, Function.comp_apply
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
v : Fin n → M
⊢ Eq (α := ⨂[R]^n M)
    ((((alternatingMapLinearEquiv : (a : M [⋀^Fin n]→ₗ[R] ⨂[R]^n M) → ↥(⋀[R]^n M) →ₗ[R] ⨂[R]^n M)
              ((MultilinearMap.alternatization :
                  (a : MultilinearMap R (fun (x : Fin n) ↦ M) (⨂[R]^n M)) → M [⋀^Fin n]→ₗ[R] ⨂[R]^n M)
                (tprod R (s := fun (x : Fin n) ↦ M))) :
            ↥(⋀[R]^n M) →ₗ[R] ⨂[R]^n M) :
          (a : ↥(⋀[R]^n M)) → ⨂[R]^n M)
        ((ιMulti R n : (a : Fin n → M) → ↥(⋀[R]^n M)) v) :
      ⨂[R]^n M)
    (∑ σ : Perm (Fin n),
        HSMul.hSMul (α := ℤˣ) (β := ⨂[R] (i : Fin n), M) ((Perm.sign : (a : Perm (Fin n)) → ℤˣ) σ : ℤˣ)
          ((tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) fun (i : Fin n) ↦
            v ((σ : (a : Fin n) → Fin n) i)) :
      ⨂[R] (i : Fin n), M)

Tactic:
simp only [alternatingMapLinearEquiv_apply_ιMulti,
    MultilinearMap.alternatization_apply, MultilinearMap.domDomCongr_apply]

Premises used: exteriorPower.alternatingMapLinearEquiv_apply_ιMulti, MultilinearMap.alternatization_apply, MultilinearMap.domDomCongr_apply
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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
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)
⊢ 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

Tactic:
ext v
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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
this :
  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
⊢ 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:
simpa [Matrix.det_apply] using this

Premises used: Matrix.det_apply
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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
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
⊢ 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:
suffices Matrix.det (n := Fin n) (.of (fun i j ↦ f j (v i))) = 0 by
      simpa [Matrix.det_apply] using this
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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
⊢ ∀ (k : Fin n),
    Eq.{u_1 + 1} (α := R)
      ((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))
          k i :
        R)
      ((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))
          k j :
        R)

Tactic:
simp [hf]
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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)
    (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:
exact Matrix.det_zero_of_column_eq hij (by simp [hf])

Premises used: Matrix.det_zero_of_column_eq
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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
v : Fin n → M
⊢ Eq.{u_1 + 1} (α := R)
    ((((alternatingMapToDual R M n : (a : Fin n → Module.Dual R M) → Module.Dual R ↥(⋀[R]^n M)) f :
            Module.Dual R ↥(⋀[R]^n M)) :
          (a : ↥(⋀[R]^n M)) → R)
        ((ιMulti R n : (a : Fin n → M) → ↥(⋀[R]^n M)) v : ↥(⋀[R]^n M)) :
      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)) :
      R)

Tactic:
simp [alternatingMapToDual, Matrix.det_apply]

Premises used: Matrix.det_apply, exteriorPower.alternatingMapToDual
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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
v : Fin n → M
⊢ Eq.{u_1 + 1} (α := R)
    ((((pairingDual R M n : (a : ↥(⋀[R]^n (Module.Dual R M))) → Module.Dual R ↥(⋀[R]^n M))
              (((ιMulti R n (M := Module.Dual R M) : Module.Dual R M [⋀^Fin n]→ₗ[R] ↥(⋀[R]^n (Module.Dual R M))) :
                  (a : Fin n → Module.Dual R M) → ↥(⋀[R]^n (Module.Dual R M)))
                f) :
            Module.Dual R ↥(⋀[R]^n M)) :
          (a : ↥(⋀[R]^n M)) → R)
        ((ιMulti R n : (a : Fin n → M) → ↥(⋀[R]^n M)) v : ↥(⋀[R]^n M)) :
      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)) :
      R)

Tactic:
simp [pairingDual]

Premises used: exteriorPower.pairingDual
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₁ : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x i) : R) (1 : R)
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a : Fin n ↪o ι
simp :
  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 ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((a : (a : Fin n) → ι) i))))
    1
⊢ Eq.{u_1 + 1} (α := R)
    ((((pairingDual R M n : (a : ↥(⋀[R]^n (Module.Dual R M))) → Module.Dual R ↥(⋀[R]^n M))
              (((ιMulti R n (M := Module.Dual R M) : Module.Dual R M [⋀^Fin n]→ₗ[R] ↥(⋀[R]^n (Module.Dual R M))) :
                  (a : Fin n → Module.Dual R M) → ↥(⋀[R]^n (Module.Dual R M)))
                (f ∘ (⇑a : (a : Fin n) → ι))) :
            Module.Dual R ↥(⋀[R]^n M)) :
          (a : ↥(⋀[R]^n M)) → R)
        ((ιMulti R n : (a : Fin n → M) → ↥(⋀[R]^n M)) (x ∘ (⇑a : (a : Fin n) → ι)) : ↥(⋀[R]^n M)) :
      R)
    (1 : R)

Tactic:
simp only [pairingDual_ιMulti_ιMulti, Function.comp_apply]

Premises used: exteriorPower.pairingDual_ιMulti_ιMulti, Function.comp_apply
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₁ : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x i) : R) (1 : R)
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a : Fin n ↪o ι
rw :
  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 ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((a : (a : Fin n) → ι) i))))
    (Matrix.det (n := Fin n) 1)
⊢ 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 ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((a : (a : Fin n) → ι) i))))
    1

Tactic:
rw [← Matrix.det_one (n := Fin n)]

Premises used: Matrix.det_one
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₁ : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x i) : R) (1 : R)
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a : Fin n ↪o ι
e_M :
  Eq.{u_1 + 1} (α := Matrix (Fin n) (Fin n) R)
    ((Matrix.of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦
        (f ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((a : (a : Fin n) → ι) i)) :
      Matrix (Fin n) (Fin n) R)
    (1 : Matrix (Fin n) (Fin n) R)
⊢ 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 ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((a : (a : Fin n) → ι) i))))
    (Matrix.det (n := Fin n) 1)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₁ : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x i) : R) (1 : R)
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a : Fin n ↪o ι
e_M :
  ∀ (i j : Fin n),
    Eq.{u_1 + 1} (α := R)
      ((Matrix.of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R)
          (fun (i j : Fin n) ↦ (f ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((a : (a : Fin n) → ι) i))) i j :
        R)
      (1 i j : R)
⊢ Eq.{u_1 + 1} (α := Matrix (Fin n) (Fin n) R)
    ((Matrix.of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦
        (f ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((a : (a : Fin n) → ι) i)) :
      Matrix (Fin n) (Fin n) R)
    (1 : Matrix (Fin n) (Fin n) R)

Tactic:
ext i j