awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₁ : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x i) : R) (1 : R)
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a : Fin n ↪o ι
⊢ Eq.{u_1 + 1} (α := R)
    ((((pairingDual R M n : (a : ↥(⋀[R]^n (Module.Dual R M))) → Module.Dual R ↥(⋀[R]^n M))
              (((ιMulti R n (M := Module.Dual R M) : Module.Dual R M [⋀^Fin n]→ₗ[R] ↥(⋀[R]^n (Module.Dual R M))) :
                  (a : Fin n → Module.Dual R M) → ↥(⋀[R]^n (Module.Dual R M)))
                (f ∘ (⇑a : (a : Fin n) → ι))) :
            Module.Dual R ↥(⋀[R]^n M)) :
          (a : ↥(⋀[R]^n M)) → R)
        ((ιMulti R n : (a : Fin n → M) → ↥(⋀[R]^n M)) (x ∘ (⇑a : (a : Fin n) → ι)) : ↥(⋀[R]^n M)) :
      R)
    (1 : R)
have simp : Eq.{u_1 + 1} (α := R)
  (Matrix.det (n := Fin n)
    ((Matrix.of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦
      (f ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((a : (a : Fin n) → ι) i))))
  1
Tactic: simp only [pairingDual_ιMulti_ιMulti, Function.comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₁ : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x i) : R) (1 : R)
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a : Fin n ↪o ι
⊢ Eq.{u_1 + 1} (α := R)
    (Matrix.det (n := Fin n)
      ((Matrix.of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦
        (f ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((a : (a : Fin n) → ι) i))))
    1
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) ↦
      (f ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((a : (a : Fin n) → ι) i))))
  (Matrix.det (n := Fin n) 1)
Tactic: rw [← Matrix.det_one (n := Fin n)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₁ : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x i) : R) (1 : R)
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a : Fin n ↪o ι
⊢ Eq.{u_1 + 1} (α := R)
    (Matrix.det (n := Fin n)
      ((Matrix.of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦
        (f ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((a : (a : Fin n) → ι) i))))
    (Matrix.det (n := Fin n) 1)
have e_M : Eq.{u_1 + 1} (α := Matrix (Fin n) (Fin n) R)
  ((Matrix.of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦
      (f ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((a : (a : Fin n) → ι) i)) :
    Matrix (Fin n) (Fin n) R)
  (1 : Matrix (Fin n) (Fin n) R)
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₁ : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x i) : R) (1 : R)
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a : Fin n ↪o ι
⊢ Eq.{u_1 + 1} (α := Matrix (Fin n) (Fin n) R)
    ((Matrix.of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦
        (f ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((a : (a : Fin n) → ι) i)) :
      Matrix (Fin n) (Fin n) R)
    (1 : Matrix (Fin n) (Fin n) R)
have e_M : ∀ (i j : Fin n),
  Eq.{u_1 + 1} (α := R)
    ((Matrix.of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R)
        (fun (i j : Fin n) ↦ (f ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((a : (a : Fin n) → ι) i))) i j :
      R)
    (1 i j : R)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₁ : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x i) : R) (1 : R)
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a : Fin n ↪o ι
i j : Fin n
⊢ Eq.{u_1 + 1} (α := R)
    ((Matrix.of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R)
        (fun (i j : Fin n) ↦ (f ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((a : (a : Fin n) → ι) i))) i j :
      R)
    (1 i j : R)
have e_M : Eq.{u_1 + 1} (α := R) ((f ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((a : (a : Fin n) → ι) i)) : R) (1 i j : R)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₁ : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x i) : R) (1 : R)
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a : Fin n ↪o ι
i j : Fin n
⊢ Eq.{u_1 + 1} (α := R) ((f ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((a : (a : Fin n) → ι) i)) : R) (1 i j : R)
have pos : ∀ (hij : i = j),
  Eq.{u_1 + 1} (α := R) ((f ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((a : (a : Fin n) → ι) i)) : R) (1 i j : R)
Tactic: by_cases hij : i = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₁ : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x i) : R) (1 : R)
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a : Fin n ↪o ι
i j : Fin n
pos :
  ∀ (hij : i = j),
    Eq.{u_1 + 1} (α := R) ((f ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((a : (a : Fin n) → ι) i)) : R) (1 i j : R)
⊢ Eq.{u_1 + 1} (α := R) ((f ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((a : (a : Fin n) → ι) i)) : R) (1 i j : R)
have neg : ∀ (hij : ¬i = j),
  Eq.{u_1 + 1} (α := R) ((f ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((a : (a : Fin n) → ι) i)) : R) (1 i j : R)
Tactic: by_cases hij : i = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₁ : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x i) : R) (1 : R)
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a : Fin n ↪o ι
i j : Fin n
hij : i = j
⊢ Eq.{u_1 + 1} (α := R) ((f ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((a : (a : Fin n) → ι) i)) : R) (1 i j : R)
have pos : Eq.{u_1 + 1} (α := R) ((f ((a : (a : Fin n) → ι) i) : (a : M) → R) (x ((a : (a : Fin n) → ι) i)) : R) (1 i i : R)
Tactic: subst hij
Cleared hypotheses: j, hij
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₁ : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x i) : R) (1 : R)
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a : Fin n ↪o ι
i j : Fin n
hij : ¬i = j
⊢ Eq.{u_1 + 1} (α := R) ((f ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((a : (a : Fin n) → ι) i)) : R) (1 i j : R)
have neg : Eq.{u_1 + 1} (α := R) 0 (1 i j)
Tactic: rw [h₀ (by simpa using Ne.symm hij), Matrix.one_apply_ne hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₁ : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x i) : R) (1 : R)
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a : Fin n ↪o ι
i j : Fin n
hij : ¬i = j
neg : Eq.{u_1 + 1} (α := R) 0 (1 i j)
⊢ Eq.{u_1 + 1} (α := R) ((f ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((a : (a : Fin n) → ι) i)) : R) (1 i j : R)
have neg₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [h₀ (by simpa using Ne.symm hij), Matrix.one_apply_ne hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
⊢ Eq.{u_1 + 1} (α := R)
    ((((pairingDual R M n : (a : ↥(⋀[R]^n (Module.Dual R M))) → Module.Dual R ↥(⋀[R]^n M))
              (((ιMulti R n (M := Module.Dual R M) : Module.Dual R M [⋀^Fin n]→ₗ[R] ↥(⋀[R]^n (Module.Dual R M))) :
                  (a : Fin n → Module.Dual R M) → ↥(⋀[R]^n (Module.Dual R M)))
                (f ∘ (⇑a : (a : Fin n) → ι))) :
            Module.Dual R ↥(⋀[R]^n M)) :
          (a : ↥(⋀[R]^n M)) → R)
        ((ιMulti R n : (a : Fin n → M) → ↥(⋀[R]^n M)) (x ∘ (⇑b : (a : Fin n) → ι)) : ↥(⋀[R]^n M)) :
      R)
    (0 : R)
have simp : Eq.{u_1 + 1} (α := R)
  (∑ σ : Equiv.Perm (Fin n),
    HSMul.hSMul (α := ℤˣ) (β := R) ((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ : ℤˣ)
      (∏ i : Fin n,
        (Matrix.of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R)
          (fun (i j : Fin n) ↦ (f ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((b : (a : Fin n) → ι) i)))
          ((σ : (a : Fin n) → Fin n) i) i))
  0
Tactic: simp only [pairingDual_ιMulti_ιMulti, Function.comp_apply, Matrix.det_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
⊢ Eq.{u_1 + 1} (α := R)
    (∑ σ : Equiv.Perm (Fin n),
      HSMul.hSMul (α := ℤˣ) (β := R) ((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ : ℤˣ)
        (∏ i : Fin n,
          (Matrix.of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R)
            (fun (i j : Fin n) ↦ (f ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((b : (a : Fin n) → ι) i)))
            ((σ : (a : Fin n) → Fin n) i) i))
    0
have refine : ∀ (σ : Equiv.Perm (Fin n)),
  Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ →
    HSMul.hSMul (α := ℤˣ) (β := R) ((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ : ℤˣ)
        (∏ i : Fin n,
          (Matrix.of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R)
            (fun (i j : Fin n) ↦ (f ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((b : (a : Fin n) → ι) i)))
            ((σ : (a : Fin n) → Fin n) i) i) =
      0
Tactic: refine Finset.sum_eq_zero (fun σ _ ↦ ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
⊢ HSMul.hSMul (α := ℤˣ) (β := R) ((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ : ℤˣ)
      (∏ i : Fin n,
        (Matrix.of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R)
          (fun (i j : Fin n) ↦ (f ((a : (a : Fin n) → ι) j) : (a : M) → R) (x ((b : (a : Fin n) → ι) i)))
          ((σ : (a : Fin n) → Fin n) i) i) =
    0
have simp : Eq.{u_1 + 1} (α := R)
  (∏ x_1 : Fin n,
    (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R) (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
  0
Tactic: simp only [Matrix.of_apply, smul_eq_iff_eq_inv_smul, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
⊢ Eq.{u_1 + 1} (α := R)
    (∏ x_1 : Fin n,
      (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R) (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
    0
have by_contra : ∀
  (h' :
    ¬Eq.{u_1 + 1} (α := R)
        (∏ x_1 : Fin n,
          (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
            (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
        0),
  False
Tactic: by_contra h'
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
⊢ False
have apply : a = b
Tactic: apply h
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
⊢ Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
have h₁ : ∀ (i : Fin n),
  Eq (α := ι) ((a : (a : Fin n) → ι) i : ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n) i : ι)
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
i : Fin n
⊢ Eq (α := ι) ((a : (a : Fin n) → ι) i : ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n) i : ι)
have h₁ : ∀
  (hi :
    ¬Eq (α := ι) ((a : (a : Fin n) → ι) i : ι)
        (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n) i : ι)),
  False
Tactic: by_contra hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
⊢ a = b
have this : Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
  (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
Tactic: have : a = b ∘ σ := by
    ext i
    by_contra hi
    exact h' (Finset.prod_eq_zero (i := i) (by simp) (h₀ hi))
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
i j : Fin n
hij : i ≤ j
⊢ LE.le (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
have h'' : ∀ (a_1 : Fin n),
  Eq (α := ι) ((a : (a : Fin n) → ι) a_1 : ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n) a_1 : ι)
Tactic: have h'' := congr_fun this
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
i j : Fin n
hij : i ≤ j
h'' :
  ∀ (a_1 : Fin n),
    Eq (α := ι) ((a : (a : Fin n) → ι) a_1 : ι) ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) a_1 : Fin n) : ι)
⊢ LE.le (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
have hij₁ : LE.le (α := ι) ((a : (a : Fin n) → ι) i : ι) ((a : (a : Fin n) → ι) j : ι)
Tactic: rw [← a.map_rel_iff] at hij
Cleared hypotheses: hij, h''
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
⊢ a = b
have hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
Tactic: have hσ : Monotone σ := fun i j hij ↦ by
    have h'' := congr_fun this
    dsimp at h''
    rw [← a.map_rel_iff] at hij
    simpa only [← b.map_rel_iff, ← h'']
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
i j : Fin n
hij : i ≤ j
⊢ LE.le (α := Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) i : Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) j : Fin n)
have obtain : ∀ (i : Fin n) (hij : (σ : (a : Fin n) → Fin n) i ≤ j),
  LE.le (α := Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) ((σ : (a : Fin n) → Fin n) i) : Fin n)
    ((Equiv.symm σ : (a : Fin n) → Fin n) j : Fin n)
Tactic: obtain ⟨i, rfl⟩ := σ.surjective i
Cleared hypotheses: i, hij
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
j i : Fin n
hij : (σ : (a : Fin n) → Fin n) i ≤ j
⊢ LE.le (α := Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) ((σ : (a : Fin n) → Fin n) i) : Fin n)
    ((Equiv.symm σ : (a : Fin n) → Fin n) j : Fin n)
have obtain : ∀ (j : Fin n) (hij : LE.le (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)),
  LE.le (α := Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) ((σ : (a : Fin n) → Fin n) i) : Fin n)
    ((Equiv.symm σ : (a : Fin n) → Fin n) ((σ : (a : Fin n) → Fin n) j) : Fin n)
Tactic: obtain ⟨j, rfl⟩ := σ.surjective j
Cleared hypotheses: j, hij
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
i j : Fin n
hij : LE.le (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
⊢ LE.le (α := Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) ((σ : (a : Fin n) → Fin n) i) : Fin n)
    ((Equiv.symm σ : (a : Fin n) → Fin n) ((σ : (a : Fin n) → Fin n) j) : Fin n)
have simp : i ≤ j
Tactic: simp only [Equiv.symm_apply_apply]