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
i : I
his : i ∈ s
hit : i ∉ t
⊢ 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
have obtain : ∀ (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),
  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: obtain ⟨k, rfl⟩ := (mem_range_ofFinEmbEquiv_symm_iff_mem s i).mpr his
Cleared hypotheses: i, his, hit
-- 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
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
⊢ 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
have 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)
Tactic: apply Matrix.det_eq_zero_of_column_eq_zero k
-- 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
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
⊢ ∀ (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)
have 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)
Tactic: simp_rw [Matrix.of_apply, Basis.coord_apply, Function.comp_apply, Basis.repr_self]
-- 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
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
⊢ 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)
have 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)
Tactic: apply Finsupp.single_eq_of_ne
-- 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
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)
⊢ False
have 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)
Tactic: apply hit
-- 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
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
    ((((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)
have h₁ : Membership.mem (α := I) (↑t : Finset I) (((↑t : Finset I).orderEmbOfFin sorry : (a : Fin n) → I) j : I)
Tactic: rw [h, powersetCard.ofFinEmbEquiv_symm_apply, ← powersetCard.mem_coe_iff]
-- 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 (α := ↥(⋀[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))
have rw : Eq (α := ↥(⋀[R]^n M)) (ιMulti_family R n (⇑b : (a : I) → M) s) (ιMulti_family R n (⇑b : (a : I) → M) s)
Tactic: rw [coe_basis]
-- 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)
⊢ (Basis.exteriorPower n b).coord s = ιMultiDual R n b s
have 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)))
Tactic: apply LinearMap.ext_on (ιMulti_family_span_of_span R (Basis.span_eq b))
-- 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).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)
have 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)
Tactic: rw [Basis.coord_apply]
-- 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) 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 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)
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) 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)
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) 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
-- 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 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)
Tactic: rw [hst, ιMultiDual_apply_diag, ← basis_apply, Basis.repr_self, Finsupp.single_eq_same]
-- 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
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)
⊢ 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 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)
Tactic: rw [hst, ιMultiDual_apply_diag, ← basis_apply, Basis.repr_self, Finsupp.single_eq_same]
-- 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
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)
⊢ 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 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)
Tactic: rw [hst, ιMultiDual_apply_diag, ← basis_apply, Basis.repr_self, Finsupp.single_eq_same]
-- 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
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)
⊢ 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 pos₃ : Eq.{u_1 + 1} (α := R) ((Finsupp.single t 1 : (a : (↑(powersetCard I n) : Type u_5)) → R) t : R) (1 : R)
Tactic: rw [hst, ιMultiDual_apply_diag, ← basis_apply, Basis.repr_self, Finsupp.single_eq_same]
-- 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
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)
⊢ 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 pos₄ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [hst, ιMultiDual_apply_diag, ← basis_apply, Basis.repr_self, Finsupp.single_eq_same]