awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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
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)
⊢ 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:
dsimp
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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)
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)
⊢ 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
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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
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)
⊢ 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:
subst hij
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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 : Fin n
⊢ 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:
simp only [h₁, Matrix.one_apply_eq]

Premises used: Matrix.one_apply_eq
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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
⊢ Ne (α := ι) ((a : (a : Fin n) → ι) j : ι) ((a : (a : Fin n) → ι) i : ι)

Tactic:
simpa using Ne.symm hij

Premises used: Ne.symm
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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)
neg₁ neg₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ 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:
rw [h₀ (by simpa using Ne.symm hij), Matrix.one_apply_ne hij]

Premises used: Matrix.one_apply_ne
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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
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
⊢ 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)

Tactic:
simp only [pairingDual_ιMulti_ιMulti, Function.comp_apply, Matrix.det_apply]

Premises used: Matrix.det_apply, exteriorPower.pairingDual_ιMulti_ιMulti, Function.comp_apply
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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

Tactic:
Finset.sum_eq_zero (fun σ _ ↦ ?_)

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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
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
⊢ 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:
refine Finset.sum_eq_zero (fun σ _ ↦ ?_)

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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 σ
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
⊢ 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 [Matrix.of_apply, smul_eq_iff_eq_inv_smul, smul_zero]

Premises used: smul_zero, Matrix.of_apply, smul_eq_iff_eq_inv_smul
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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 σ
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
⊢ 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:
by_contra h'
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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
apply : a = b
⊢ False

Tactic:
apply h
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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
h₁ :
  ∀ (i : Fin n),
    Eq (α := ι) ((a : (a : Fin n) → ι) i : ι)
      (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n) i : ι)
⊢ Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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
h₁ :
  ∀
    (hi :
      ¬Eq (α := ι) ((a : (a : Fin n) → ι) i : ι)
          (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n) i : ι)),
    False
⊢ Eq (α := ι) ((a : (a : Fin n) → ι) i : ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n) i : ι)

Tactic:
by_contra hi
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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
hi :
  ¬Eq (α := ι) ((a : (a : Fin n) → ι) i : ι)
      (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n) i : ι)
⊢ Membership.mem (γ := Finset (Fin n)) Finset.univ i

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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
hi :
  ¬Eq (α := ι) ((a : (a : Fin n) → ι) i : ι)
      (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n) i : ι)
⊢ False

Tactic:
exact h' (Finset.prod_eq_zero (i := i) (by simp) (h₀ hi))

Premises used: Finset.prod_eq_zero
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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))

Tactic:
have : a = b ∘ σ := by
    ext i
    by_contra hi
    exact h' (Finset.prod_eq_zero (i := i) (by simp) (h₀ hi))
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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
⊢ ∀ (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
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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 (α := ι) ((a : (a : Fin n) → ι) i : ι) ((a : (a : Fin n) → ι) j : ι)

Tactic:
rw [← a.map_rel_iff] at hij

Premises used: RelEmbedding.map_rel_iff
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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) : ι)
hij₁ : LE.le (α := ι) ((a : (a : Fin n) → ι) i : ι) ((a : (a : Fin n) → ι) j : ι)
⊢ ∀ (a_1 : Fin n),
    Eq (α := ι) ((a : (a : Fin n) → ι) a_1 : ι) ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) a_1 : Fin n) : ι)

Tactic:
rw [← a.map_rel_iff] at hij

Premises used: RelEmbedding.map_rel_iff
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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 : LE.le (α := ι) ((a : (a : Fin n) → ι) i : ι) ((a : (a : Fin n) → ι) 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)

Tactic:
simpa only [← b.map_rel_iff, ← h'']

Premises used: RelEmbedding.map_rel_iff
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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))
⊢ 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'']
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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
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)
⊢ LE.le (α := Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) i : Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) j : Fin n)

Tactic:
obtain ⟨i, rfl⟩ := σ.surjective i

Premises used: Equiv.surjective, rfl
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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
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)
⊢ 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 ⟨j, rfl⟩ := σ.surjective j

Premises used: Equiv.surjective, rfl
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
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)
simp : 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) ((σ : (a : Fin n) → Fin n) j) : Fin n)

Tactic:
simp only [Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply