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)
hst : s ≠ t
k : Fin n
his :
  Membership.mem (α := I) s
    ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
          (a : Fin n) → I)
        k :
      I)
hit :
  ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) : (a : Fin n) → I)
        k :
      I) ∉
    t
apply :
  ∀ (i : 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) ↦
            (b.coord
                  ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
                      (a : Fin n) → I)
                    j) :
                (a : M) → R)
              (Function.comp (β := I) (⇑b : (a : I) → M)
                (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) t : Fin n ↪o I) :
                  (a : Fin n) → I)
                i))
          i k :
        R)
      (0 : 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) ↦
        (b.coord
              ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
                  (a : Fin n) → I)
                j) :
            (a : M) → R)
          (Function.comp (β := I) (⇑b : (a : I) → M)
            (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) t : Fin n ↪o I) :
              (a : Fin n) → I)
            i)))
    0

Tactic:
apply Matrix.det_eq_zero_of_column_eq_zero k

Premises used: Matrix.det_eq_zero_of_column_eq_zero
-- 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
k : Fin n
his :
  Membership.mem (α := I) s
    ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
          (a : Fin n) → I)
        k :
      I)
hit :
  ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) : (a : Fin n) → I)
        k :
      I) ∉
    t
simp_rw :
  ∀ (i : Fin n),
    Eq.{u_1 + 1} (α := R)
      (((Finsupp.single
                ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) t : Fin n ↪o I) :
                    (a : Fin n) → I)
                  i)
                1 :
              I →₀ R) :
            (a : I) → R)
          ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
                (a : Fin n) → I)
              k :
            I) :
        R)
      (0 : R)
⊢ ∀ (i : 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) ↦
            (b.coord
                  ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
                      (a : Fin n) → I)
                    j) :
                (a : M) → R)
              (Function.comp (β := I) (⇑b : (a : I) → M)
                (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) t : Fin n ↪o I) :
                  (a : Fin n) → I)
                i))
          i k :
        R)
      (0 : R)

Tactic:
simp_rw [Matrix.of_apply, Basis.coord_apply, Function.comp_apply, Basis.repr_self]

Premises used: Matrix.of_apply, Function.comp_apply, Module.Basis.coord_apply, Module.Basis.repr_self
-- 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
k : Fin n
his :
  Membership.mem (α := I) s
    ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
          (a : Fin n) → I)
        k :
      I)
hit :
  ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) : (a : Fin n) → I)
        k :
      I) ∉
    t
j : Fin n
h :
  Ne (α := I)
    ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
          (a : Fin n) → I)
        k :
      I)
    ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) t : Fin n ↪o I) :
          (a : Fin n) → I)
        j :
      I)
⊢ Eq.{u_1 + 1} (α := R)
    (((Finsupp.single
              ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) t : Fin n ↪o I) :
                  (a : Fin n) → I)
                j)
              1 :
            I →₀ R) :
          (a : I) → R)
        ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
              (a : Fin n) → I)
            k :
          I) :
      R)
    (0 : R)

Tactic:
apply Finsupp.single_eq_of_ne

Premises used: Finsupp.single_eq_of_ne
-- 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
k : Fin n
his :
  Membership.mem (α := I) s
    ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
          (a : Fin n) → I)
        k :
      I)
hit :
  ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) : (a : Fin n) → I)
        k :
      I) ∉
    t
j : Fin n
h :
  ∀
    (h :
      Eq (α := I)
        ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
              (a : Fin n) → I)
            k :
          I)
        ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) t : Fin n ↪o I) :
              (a : Fin n) → I)
            j :
          I)),
    False
⊢ Ne (α := I)
    ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
          (a : Fin n) → I)
        k :
      I)
    ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) t : Fin n ↪o I) :
          (a : Fin n) → I)
        j :
      I)

Tactic:
by_contra! h
-- 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
k : Fin n
his :
  Membership.mem (α := I) s
    ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
          (a : Fin n) → I)
        k :
      I)
hit :
  ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) : (a : Fin n) → I)
        k :
      I) ∉
    t
j : Fin n
h :
  Eq (α := I)
    ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
          (a : Fin n) → I)
        k :
      I)
    ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) t : Fin n ↪o I) :
          (a : Fin n) → I)
        j :
      I)
h₁ :
  Membership.mem (α := I) t
    ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
          (a : Fin n) → I)
        k :
      I)
⊢ False

Tactic:
apply hit
-- 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
k : Fin n
his :
  Membership.mem (α := I) s
    ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
          (a : Fin n) → I)
        k :
      I)
hit :
  ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) : (a : Fin n) → I)
        k :
      I) ∉
    t
j : Fin n
h :
  Eq (α := I)
    ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
          (a : Fin n) → I)
        k :
      I)
    ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) t : Fin n ↪o I) :
          (a : Fin n) → I)
        j :
      I)
h₁ : Membership.mem (α := I) (↑t : Finset I) (((↑t : Finset I).orderEmbOfFin ⋯ : (a : Fin n) → I) j : I)
⊢ Membership.mem (α := I) t
    ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
          (a : Fin n) → I)
        k :
      I)

Tactic:
rw [h, powersetCard.ofFinEmbEquiv_symm_apply, ← powersetCard.mem_coe_iff]

Premises used: Set.powersetCard.mem_coe_iff, Set.powersetCard.ofFinEmbEquiv_symm_apply
-- 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
k : Fin n
his :
  Membership.mem (α := I) s
    ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
          (a : Fin n) → I)
        k :
      I)
hit :
  ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) : (a : Fin n) → I)
        k :
      I) ∉
    t
j : Fin n
h :
  Eq (α := I)
    ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
          (a : Fin n) → I)
        k :
      I)
    ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) t : Fin n ↪o I) :
          (a : Fin n) → I)
        j :
      I)
⊢ Membership.mem (α := I) (↑t : Finset I) (((↑t : Finset I).orderEmbOfFin ⋯ : (a : Fin n) → I) j : I)

Tactic:
Finset.orderEmbOfFin_mem t.val t.prop j

Premises used: Subtype.prop, Subtype.val, Finset.orderEmbOfFin_mem
-- 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
k : Fin n
his :
  Membership.mem (α := I) s
    ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
          (a : Fin n) → I)
        k :
      I)
hit :
  ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) : (a : Fin n) → I)
        k :
      I) ∉
    t
j : Fin n
h :
  Eq (α := I)
    ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
          (a : Fin n) → I)
        k :
      I)
    ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) t : Fin n ↪o I) :
          (a : Fin n) → I)
        j :
      I)
⊢ Membership.mem (α := I) (↑t : Finset I) (((↑t : Finset I).orderEmbOfFin ⋯ : (a : Fin n) → I) j : I)

Tactic:
exact Finset.orderEmbOfFin_mem t.val t.prop j

Premises used: Subtype.prop, Subtype.val, Finset.orderEmbOfFin_mem
-- 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
⊢ LinearIndependent (ι := (↑(powersetCard I n) : Type u_5)) R (M := ↥(⋀[R]^n M)) (ιMulti_family R n (⇑b : (a : I) → M))

Tactic:
LinearIndependent.of_pairwise_dual_eq_zero_one _ (fun s ↦ ιMultiDual R n b s)
    (fun _ _ h => ιMultiDual_apply_nondiag R n b _ _ h)
    (fun _ => ιMultiDual_apply_diag _ _ _ _)

Premises used: exteriorPower.ιMultiDual, Set.Mem, exteriorPower.ιMultiDual_apply_diag, LinearIndependent.of_pairwise_dual_eq_zero_one, exteriorPower.ιMultiDual_apply_nondiag
-- 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
⊢ Eq (α := (a : (↑(powersetCard I n) : Type u_5)) → ↥(⋀[R]^n M))
    (⇑(Basis.exteriorPower n b) : (a : (↑(powersetCard I n) : Type u_5)) → ↥(⋀[R]^n M))
    (ιMulti_family R n (⇑b : (a : I) → M))

Tactic:
Basis.coe_mk _ _

Premises used: Module.Basis.coe_mk
-- 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 : (↑(powersetCard I n) : Type u_5)
rw rw₁ : Eq (α := ↥(⋀[R]^n M)) (ιMulti_family R n (⇑b : (a : I) → M) s) (ιMulti_family R n (⇑b : (a : I) → M) s)
⊢ Eq (α := ↥(⋀[R]^n M))
    ((Basis.exteriorPower n b : (a : (↑(powersetCard I n) : Type u_5)) → ↥(⋀[R]^n M)) s : ↥(⋀[R]^n M))
    (ιMulti_family R n (⇑b : (a : I) → M) s : ↥(⋀[R]^n M))

Tactic:
rw [coe_basis]

Premises used: exteriorPower.coe_basis
-- 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 : (↑(powersetCard I n) : Type u_5)
apply :
  EqOn (α := ↥(⋀[R]^n M)) (β := R) (⇑((Basis.exteriorPower n b).coord s) : (a : ↥(⋀[R]^n M)) → R)
    (⇑(ιMultiDual R n b s) : (a : ↥(⋀[R]^n M)) → R)
    (range (ι := (↑(powersetCard I n) : Type u_5)) (ιMulti_family R n (⇑b : (a : I) → M)))
⊢ (Basis.exteriorPower n b).coord s = ιMultiDual R n b s

Tactic:
apply LinearMap.ext_on (ιMulti_family_span_of_span R (Basis.span_eq b))

Premises used: LinearMap.ext_on, exteriorPower.ιMulti_family_span_of_span, Module.Basis.span_eq
-- 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)
rw :
  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)
⊢ Eq.{u_1 + 1} (α := R)
    (((Basis.exteriorPower n b).coord s : (a : ↥(⋀[R]^n M)) → R) (ιMulti_family R n (⇑b : (a : I) → M) t) : R)
    ((ιMultiDual R n b s : (a : ↥(⋀[R]^n M)) → R) (ιMulti_family R n (⇑b : (a : I) → M) t) : R)

Tactic:
rw [Basis.coord_apply]

Premises used: Module.Basis.coord_apply
-- 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) 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)
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) 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)
⊢ 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)

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
pos :
  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)
        t :
      R)
    ((ιMultiDual R n b t : (a : ↥(⋀[R]^n M)) → R) (ιMulti_family R n (⇑b : (a : I) → M) t) : R)
pos₁ :
  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)
        t :
      R)
    (1 : R)
pos₂ :
  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)
        t :
      R)
    (1 : R)
pos₃ : Eq.{u_1 + 1} (α := R) ((Finsupp.single t 1 : (a : (↑(powersetCard I n) : Type u_5)) → R) t : R) (1 : R)
pos₄ pos₅ : Eq.{u_1 + 1} (α := R) 1 1
⊢ 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)

Tactic:
rw [hst, ιMultiDual_apply_diag, ← basis_apply, Basis.repr_self, Finsupp.single_eq_same]

Premises used: exteriorPower.basis_apply, Finsupp.single_eq_same, exteriorPower.ιMultiDual_apply_diag, Module.Basis.repr_self
-- 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
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)
neg₃ neg₄ : Eq.{u_1 + 1} (α := R) 0 0
⊢ 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)

Tactic:
rw [ιMultiDual_apply_nondiag R n b s t hst, ← basis_apply, Basis.repr_self,
      Finsupp.single_eq_of_ne hst]

Premises used: exteriorPower.basis_apply, Finsupp.single_eq_of_ne, exteriorPower.ιMultiDual_apply_nondiag, Module.Basis.repr_self
-- 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
x : ↥(⋀[R]^n M)
s : (↑(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) x :
            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) x : R)

Tactic:
simpa [← Basis.coord_apply] using LinearMap.congr_fun (basis_coord R n b s) x

Premises used: exteriorPower.basis_coord, LinearMap.congr_fun, Module.Basis.coord_apply
-- 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 : (↑(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)
        s :
      R)
    (1 : R)

Tactic:
simpa [basis_repr_apply] using ιMultiDual_apply_diag R n b s

Premises used: exteriorPower.ιMultiDual_apply_diag, exteriorPower.basis_repr_apply
-- 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)
    (0 : R)

Tactic:
simpa [basis_repr_apply] using ιMultiDual_apply_nondiag R n b t s hst.symm

Premises used: Ne.symm, exteriorPower.basis_repr_apply, exteriorPower.ιMultiDual_apply_nondiag
-- 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 : (↑(powersetCard I n) : Type u_5)
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)
⊢ 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)

Tactic:
ext t