awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
h :
  ∀ (m : M),
    Eq.{u_1 + 1} (α := Fin 1 → M) (fun (x : Fin 1) ↦ m) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m)
m₁ m₂ : M
⊢ (ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 (m₁ + m₂)) =
    HAdd.hAdd (α := ↥(⋀[R]^1 M)) (β := ↥(⋀[R]^1 M))
      ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m₁) :
        ↥(⋀[R]^1 M))
      ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m₂) :
        ↥(⋀[R]^1 M))

Tactic:
simp only [Fin.isValue, AlternatingMap.map_update_add]

Premises used: AlternatingMap.map_update_add, Fin.isValue
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
h :
  ∀ (m : M),
    Eq.{u_1 + 1} (α := Fin 1 → M) (fun (x : Fin 1) ↦ m) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m)
r : R
m : M
dsimp :
  ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) fun (x : Fin 1) ↦ r • m) =
    HSMul.hSMul (β := ↥(⋀[R]^1 M)) r ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) fun (x : Fin 1) ↦ m)
⊢ ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) fun (x : Fin 1) ↦ r • m) =
    HSMul.hSMul (α := R) (β := ↥(⋀[R]^1 M)) ((RingHom.id R : (a : R) → R) r : R)
      ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) fun (x : Fin 1) ↦ m)

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
h :
  ∀ (m : M),
    Eq.{u_1 + 1} (α := Fin 1 → M) (fun (x : Fin 1) ↦ m) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m)
r : R
m : M
rw :
  (ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 (r • m)) =
    HSMul.hSMul (β := ↥(⋀[R]^1 M)) r ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) fun (x : Fin 1) ↦ m)
⊢ ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) fun (x : Fin 1) ↦ r • m) =
    HSMul.hSMul (β := ↥(⋀[R]^1 M)) r ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) fun (x : Fin 1) ↦ m)

Tactic:
rw [h]
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
h :
  ∀ (m : M),
    Eq.{u_1 + 1} (α := Fin 1 → M) (fun (x : Fin 1) ↦ m) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m)
r : R
m : M
nth_rw :
  (ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 (r • m)) =
    HSMul.hSMul (β := ↥(⋀[R]^1 M)) r
      ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m) :
        ↥(⋀[R]^1 M))
⊢ (ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 (r • m)) =
    HSMul.hSMul (β := ↥(⋀[R]^1 M)) r ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) fun (x : Fin 1) ↦ m)

Tactic:
nth_rw 2 [h]
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
h :
  ∀ (m : M),
    Eq.{u_1 + 1} (α := Fin 1 → M) (fun (x : Fin 1) ↦ m) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m)
r : R
m : M
⊢ (ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 (r • m)) =
    HSMul.hSMul (β := ↥(⋀[R]^1 M)) r
      ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m) :
        ↥(⋀[R]^1 M))

Tactic:
simp only [Fin.isValue, AlternatingMap.map_update_smul]

Premises used: AlternatingMap.map_update_smul, Fin.isValue
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
h :
  ∀ (m : M),
    Eq.{u_1 + 1} (α := Fin 1 → M) (fun (x : Fin 1) ↦ m) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m)
⊢ M →ₗ[R] ↥(⋀[R]^1 M)

Tactic:
exact
        { toFun := fun m ↦ ιMulti _ _ (fun _ ↦ m)
          map_add' := fun m₁ m₂ ↦ by
            rw [h]; nth_rw 2 [h]; nth_rw 3 [h]
            simp only [Fin.isValue, AlternatingMap.map_update_add]
          map_smul' := fun r m ↦ by
            dsimp
            rw [h]; nth_rw 2 [h]
            simp only [Fin.isValue, AlternatingMap.map_update_smul] }
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
⊢ Eq.{u_1 + 1} (α := M →ₗ[R] M)
    ((alternatingMapLinearEquiv : (a : M [⋀^Fin 1]→ₗ[R] M) → ↥(⋀[R]^1 M) →ₗ[R] M)
        ((AlternatingMap.ofSubsingleton R M M 0 : (a : M →ₗ[R] M) → M [⋀^Fin 1]→ₗ[R] M) LinearMap.id) ∘ₗ
      have h :
        ∀ (m : M),
          Eq.{u_1 + 1} (α := Fin 1 → M) (fun (x : Fin 1) ↦ m)
            (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m) :=
        ⋯;
      { toFun := fun (m : M) ↦ (ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) fun (x : Fin 1) ↦ m, map_add' := ⋯,
        map_smul' := ⋯ })
    LinearMap.id

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
⊢ Eq (α := ↥(⋀[R]^1 M) →ₗ[R] ↥(⋀[R]^1 M))
    ((have h :
        ∀ (m : M),
          Eq.{u_1 + 1} (α := Fin 1 → M) (fun (x : Fin 1) ↦ m)
            (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m) :=
        ⋯;
      { toFun := fun (m : M) ↦ (ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) fun (x : Fin 1) ↦ m, map_add' := ⋯,
        map_smul' := ⋯ }) ∘ₗ
      (alternatingMapLinearEquiv : (a : M [⋀^Fin 1]→ₗ[R] M) → ↥(⋀[R]^1 M) →ₗ[R] M)
        ((AlternatingMap.ofSubsingleton R M M 0 : (a : M →ₗ[R] M) → M [⋀^Fin 1]→ₗ[R] M) LinearMap.id))
    LinearMap.id

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
f : Fin 1 → M
⊢ (oneEquiv R M : (a : ↥(⋀[R]^1 M)) → M) ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) f : ↥(⋀[R]^1 M)) = f 0

Tactic:
simp [oneEquiv]

Premises used: exteriorPower.oneEquiv
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
⊢ (↑(oneEquiv R N) : ↥(⋀[R]^1 N) →ₗ[R] N) ∘ₗ map 1 f = f ∘ₗ (↑(oneEquiv R M) : ↥(⋀[R]^1 M) →ₗ[R] M)

Tactic:
aesop
-- 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 : Module.Finite R M
rw : (HPow.hPow (α := Submodule R (ExteriorAlgebra R M)) (Submodule.map (ExteriorAlgebra.ι R) ⊤) n).FG
⊢ Module.Finite R ↥(⋀[R]^n M)

Tactic:
rw [Module.Finite.iff_fg, ExteriorAlgebra.exteriorPower, LinearMap.range_eq_map]

Premises used: Module.Finite.iff_fg, LinearMap.range_eq_map, ExteriorAlgebra.exteriorPower
-- 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 : Module.Finite R M
⊢ (HPow.hPow (α := Submodule R (ExteriorAlgebra R M)) (Submodule.map (ExteriorAlgebra.ι R) ⊤) n).FG

Tactic:
Submodule.FG.pow (Submodule.FG.map _ Module.Finite.fg_top) n

Premises used: Module.Finite.fg_top, Submodule.FG.map, Submodule.FG.pow
-- 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 : Module.Finite R M
⊢ (HPow.hPow (α := Submodule R (ExteriorAlgebra R M)) (Submodule.map (ExteriorAlgebra.ι R) ⊤) n).FG

Tactic:
exact Submodule.FG.pow (Submodule.FG.map _ Module.Finite.fg_top) n

Premises used: Module.Finite.fg_top, Submodule.FG.map, Submodule.FG.pow
-- 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)
v : Fin n → M
⊢ Eq.{u_1 + 1} (α := R)
    ((ιMultiDual R n b s : (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) ↦
          (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)
            (v i)) :
      R)

Tactic:
simp [ιMultiDual, ιMulti_family, pairingDual_ιMulti_ιMulti]

Premises used: exteriorPower.ιMultiDual, exteriorPower.pairingDual_ιMulti_ιMulti, exteriorPower.ιMulti_family
-- 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 :
  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) s : Fin n ↪o I) :
              (a : Fin n) → I)
            i)))
    1
⊢ Eq.{u_1 + 1} (α := R) ((ιMultiDual R n b s : (a : ↥(⋀[R]^n M)) → R) (ιMulti_family R n (⇑b : (a : I) → M) s) : R)
    (1 : R)

Tactic:
rw [ιMulti_family, ιMultiDual_apply_ιMulti]

Premises used: exteriorPower.ιMultiDual_apply_ιMulti, exteriorPower.ιMulti_family
-- 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)
this :
  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) ↦
        (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)
          ((b : (a : I) → M)
              ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
                    (a : Fin n) → I)
                  i :
                I) :
            M) :
      Matrix (Fin n) (Fin n) R)
    (1 : Matrix (Fin n) (Fin n) R)
simp_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) ↦
        (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)
          ((b : (a : I) → M)
              ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
                    (a : Fin n) → I)
                  i :
                I) :
            M)))
    1
simp_rw₁ : Eq.{u_1 + 1} (α := R) (Matrix.det (n := Fin n) 1) 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) ↦
        (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) s : Fin n ↪o I) :
              (a : Fin n) → I)
            i)))
    1

Tactic:
simp_rw [Function.comp_apply, this, Matrix.det_one]

Premises used: Matrix.det_one, Function.comp_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)
suffices :
  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) ↦
        (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)
          ((b : (a : I) → M)
              ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
                    (a : Fin n) → I)
                  i :
                I) :
            M) :
      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) ↦
        (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) s : Fin n ↪o I) :
              (a : Fin n) → I)
            i)))
    1

Tactic:
suffices Matrix.of (fun i j => b.coord (powersetCard.ofFinEmbEquiv.symm s j)
    (b (powersetCard.ofFinEmbEquiv.symm s i))) = 1 by
    simp_rw [Function.comp_apply, this, Matrix.det_one]
-- 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)
a :
  ∀ (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) ↦
            (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)
              ((b : (a : I) → M)
                  ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
                        (a : Fin n) → I)
                      i :
                    I) :
                M))
          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) ↦
        (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)
          ((b : (a : I) → M)
              ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
                    (a : Fin n) → I)
                  i :
                I) :
            M) :
      Matrix (Fin n) (Fin n) R)
    (1 : Matrix (Fin n) (Fin n) R)

Tactic:
ext
-- 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)
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) ↦
          (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)
            ((b : (a : I) → M)
                ((((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_5)) → Fin n ↪o I) s : Fin n ↪o I) :
                      (a : Fin n) → I)
                    i :
                  I) :
              M))
        i j :
      R)
    (1 i j : R)

Tactic:
simp [Matrix.one_apply, Finsupp.single_apply]

Premises used: Matrix.one_apply, Finsupp.single_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
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) ↦
        (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
⊢ Eq.{u_1 + 1} (α := R) ((ιMultiDual R n b s : (a : ↥(⋀[R]^n M)) → R) (ιMulti_family R n (⇑b : (a : I) → M) t) : R)
    (0 : R)

Tactic:
rw [ιMulti_family, ιMultiDual_apply_ιMulti]

Premises used: exteriorPower.ιMultiDual_apply_ιMulti, exteriorPower.ιMulti_family
-- 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
obtain :
  ∀ (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
⊢ 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 ⟨i, his, hit⟩ := (exists_mem_notMem_iff_ne s t).mp hst

Premises used: Iff.mp, Set.powersetCard.exists_mem_notMem_iff_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
i : I
his : i ∈ s
hit : i ∉ t
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
⊢ 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

Premises used: Iff.mpr, Set.powersetCard.mem_range_ofFinEmbEquiv_symm_iff_mem, rfl