awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
f : I → ↥(span R (range v))
hf : (⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M) ∘ f = v
htop : Eq (α := Submodule R ↥(span R (range v))) (span R (range f)) ⊤
rw :
  Eq (α := Submodule R ↥(⋀[R]^n M))
    (Submodule.map (M := ↥(⋀[R]^n ↥(span R (range v)))) (map n (Submodule.subtype (span R (range v)))) ⊤)
    (span R (range (ιMulti_family R n v)))
rw₁ :
  Submodule.map (map n (Submodule.subtype (span R (range v)))) (span R (range (ιMulti_family R n f))) =
    span R (range (ιMulti_family R n v))
rw₂ :
  Eq (α := Submodule R ↥(⋀[R]^n M))
    (span R
      (image (α := ↥(⋀[R]^n ↥(span R (range v))))
        (⇑(map n (Submodule.subtype (span R (range v)))) : (a : ↥(⋀[R]^n ↥(span R (range v)))) → ↥(⋀[R]^n M))
        (range (ιMulti_family R n f))))
    (span R (range (ιMulti_family R n v)))
rw₃ :
  Eq (α := Submodule R ↥(⋀[R]^n M))
    (span R
      (range
        (comp (β := ↥(⋀[R]^n ↥(span R (range v))))
          (⇑(map n (Submodule.subtype (span R (range v)))) : (a : ↥(⋀[R]^n ↥(span R (range v)))) → ↥(⋀[R]^n M))
          (ιMulti_family R n f))))
    (span R (range (ιMulti_family R n v)))
⊢ Eq (α := Submodule R ↥(⋀[R]^n M))
    (LinearMap.range (M := ↥(⋀[R]^n ↥(span R (range v)))) (map n (Submodule.subtype (span R (range v)))))
    (span R (range (ιMulti_family R n v)))
have rw₄ : Eq (α := Submodule R ↥(⋀[R]^n M))
  (span R (range (ιMulti_family R n ((⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M) ∘ f))))
  (span R (range (ιMulti_family R n v)))
Tactic: rw [LinearMap.range_eq_map (M := ⋀[R]^n _), ← ιMulti_family_span_of_span _ htop,
    Submodule.map_span, ← Set.range_comp, map_comp_ιMulti_family, hf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
f : I → ↥(span R (range v))
hf : (⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M) ∘ f = v
htop : Eq (α := Submodule R ↥(span R (range v))) (span R (range f)) ⊤
rw :
  Eq (α := Submodule R ↥(⋀[R]^n M))
    (Submodule.map (M := ↥(⋀[R]^n ↥(span R (range v)))) (map n (Submodule.subtype (span R (range v)))) ⊤)
    (span R (range (ιMulti_family R n v)))
rw₁ :
  Submodule.map (map n (Submodule.subtype (span R (range v)))) (span R (range (ιMulti_family R n f))) =
    span R (range (ιMulti_family R n v))
rw₂ :
  Eq (α := Submodule R ↥(⋀[R]^n M))
    (span R
      (image (α := ↥(⋀[R]^n ↥(span R (range v))))
        (⇑(map n (Submodule.subtype (span R (range v)))) : (a : ↥(⋀[R]^n ↥(span R (range v)))) → ↥(⋀[R]^n M))
        (range (ιMulti_family R n f))))
    (span R (range (ιMulti_family R n v)))
rw₃ :
  Eq (α := Submodule R ↥(⋀[R]^n M))
    (span R
      (range
        (comp (β := ↥(⋀[R]^n ↥(span R (range v))))
          (⇑(map n (Submodule.subtype (span R (range v)))) : (a : ↥(⋀[R]^n ↥(span R (range v)))) → ↥(⋀[R]^n M))
          (ιMulti_family R n f))))
    (span R (range (ιMulti_family R n v)))
rw₄ :
  Eq (α := Submodule R ↥(⋀[R]^n M))
    (span R (range (ιMulti_family R n ((⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M) ∘ f))))
    (span R (range (ιMulti_family R n v)))
⊢ Eq (α := Submodule R ↥(⋀[R]^n M))
    (LinearMap.range (M := ↥(⋀[R]^n ↥(span R (range v)))) (map n (Submodule.subtype (span R (range v)))))
    (span R (range (ιMulti_family R n v)))
have rw₅ : Eq (α := Submodule R ↥(⋀[R]^n M)) (span R (range (ιMulti_family R n v))) (span R (range (ιMulti_family R n v)))
Tactic: rw [LinearMap.range_eq_map (M := ⋀[R]^n _), ← ιMulti_family_span_of_span _ htop,
    Submodule.map_span, ← Set.range_comp, map_comp_ιMulti_family, hf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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'
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)
have h : ∀ (i : Fin 1), m = update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m i
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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'
m : M
i : Fin 1
⊢ m = update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m i
have h : m = update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m ((fun (i : Fin 1) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (hypothesis)
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'
⊢ 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)
Tactic: have h (m : M) : (fun (_ : Fin 1) ↦ m) = update (fun _ ↦ 0) 0 m := by
        ext i
        fin_cases i
        rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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)) fun (x : Fin 1) ↦ m₁ + m₂) =
    HAdd.hAdd (α := ↥(⋀[R]^1 M)) ((ι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) ↦ m₂)
have rw : (ι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)) ((ι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) ↦ m₂)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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)) ((ι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) ↦ m₂)
have nth_rw : (ι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)) fun (x : Fin 1) ↦ m₂ : ↥(⋀[R]^1 M))
Tactic: nth_rw 2 [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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)) fun (x : Fin 1) ↦ m₂ : ↥(⋀[R]^1 M))
have nth_rw : (ι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: nth_rw 3 [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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)) 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)
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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)) 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)
have 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)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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)) fun (x : Fin 1) ↦ m)
have 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))
Tactic: nth_rw 2 [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basis (goal)
Goal:
R : Type u_1
K : Type u_2
M : Type u_3
E : Type u_4
n : ℕ
inst : CommRing R
inst_1 : Field K
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup E
inst_5 : Module K E
inst_6 : Module.Finite R M
⊢ Module.Finite R ↥(⋀[R]^n M)
have rw : (HPow.hPow (α := Submodule R (ExteriorAlgebra R M)) (Submodule.map (ExteriorAlgebra.ι R) ⊤) n).FG
Tactic: rw [Module.Finite.iff_fg, ExteriorAlgebra.exteriorPower, LinearMap.range_eq_map]
-- 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.{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)
have 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
Tactic: rw [ιMulti_family, ιMultiDual_apply_ιMulti]
-- 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)
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)
⊢ 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
have 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
Tactic: simp_rw [Function.comp_apply, this, Matrix.det_one]
-- 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)
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
⊢ 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
have simp_rw₁ : Eq.{u_1 + 1} (α := R) (Matrix.det (n := Fin n) 1) 1
Tactic: simp_rw [Function.comp_apply, this, Matrix.det_one]
-- 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.{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
have 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)
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]
-- 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.{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)
have 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)
Tactic: ext
-- 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) ((ιMultiDual R n b s : (a : ↥(⋀[R]^n M)) → R) (ιMulti_family R n (⇑b : (a : I) → M) t) : R)
    (0 : R)
have 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
Tactic: rw [ιMulti_family, ιMultiDual_apply_ιMulti]
-- 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)
    (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 : ∀ (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
Tactic: obtain ⟨i, his, hit⟩ := (exists_mem_notMem_iff_ne s t).mp hst