-- Mathlib/LinearAlgebra/ExteriorPower/Pairing.lean
lemma pairingDual_apply_apply_eq_one_zero (a b : Fin n ↪o ι) (h : a ≠ b) :
    pairingDual R M n (ιMulti _ _ (f ∘ a)) (ιMulti _ _ (x ∘ b)) = 0

Proof state:
case intro.intro
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ x_1 : Fin n, (f (a x_1)) (x (b (σ x_1))) = 0
this : ⇑a = ⇑b ∘ ⇑σ
hσ : Monotone ⇑σ
i j : Fin n
hij : σ i ≤ σ j
⊢ (Equiv.symm σ) (σ i) ≤ (Equiv.symm σ) (σ j)

Tactic:
simp only [Equiv.symm_apply_apply]

Result:
case intro.intro
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ x_1 : Fin n, (f (a x_1)) (x (b (σ x_1))) = 0
this : ⇑a = ⇑b ∘ ⇑σ
hσ : Monotone ⇑σ
i j : Fin n
hij : σ i ≤ σ j
⊢ i ≤ j

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ x_1 : Fin n, (f (a x_1)) (x (b (σ x_1))) = 0
i : Fin n
hi : ¬a i = (⇑b ∘ ⇑σ) i
⊢ False

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

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
⊢ Equiv.Perm.sign σ • ∏ i : Fin n, Matrix.of (fun i j => (f (a j)) (x (b i))) (σ i) i = 0

Tactic:
simp only [Matrix.of_apply, smul_eq_iff_eq_inv_smul, smul_zero]

Result:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
⊢ ∏ x_1 : Fin n, (f (a x_1)) (x (b (σ x_1))) = 0

Proof state:
case intro.intro
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h✝ : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ x_1 : Fin n, (f (a x_1)) (x (b (σ x_1))) = 0
this : ⇑a = ⇑b ∘ ⇑σ
hσ : Monotone ⇑σ
i : Fin n
hij : σ i ≤ σ i
h : i < i
⊢ False

Tactic:
simp only [lt_self_iff_false] at h

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ x_1 : Fin n, (f (a x_1)) (x (b (σ x_1))) = 0
this : ⇑a = ⇑b ∘ ⇑σ
i j : Fin n
hij : i ≤ j
h'' : ∀ (a_1 : Fin n), a a_1 = (⇑b ∘ ⇑σ) a_1
⊢ σ i ≤ σ j

Tactic:
dsimp at h''

Result:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ x_1 : Fin n, (f (a x_1)) (x (b (σ x_1))) = 0
this : ⇑a = ⇑b ∘ ⇑σ
i j : Fin n
hij : i ≤ j
h'' : ∀ (a_1 : Fin n), a a_1 = b (σ a_1)
⊢ σ i ≤ σ j

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ x_1 : Fin n, (f (a x_1)) (x (b (σ x_1))) = 0
⊢ a = b

Tactic:
have : a = b ∘ σ := by
  ext i
  by_contra hi
  exact h' (Finset.prod_eq_zero (i := i) (by simp) (h₀ hi))

Result:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ x_1 : Fin n, (f (a x_1)) (x (b (σ x_1))) = 0
this : ⇑a = ⇑b ∘ ⇑σ
⊢ a = b

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
⊢ ∏ x_1 : Fin n, (f (a x_1)) (x (b (σ x_1))) = 0

Tactic:
by_contra h'

Result:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ x_1 : Fin n, (f (a x_1)) (x (b (σ x_1))) = 0
⊢ False

Proof state:
case intro.intro
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h✝ : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ x_1 : Fin n, (f (a x_1)) (x (b (σ x_1))) = 0
this : ⇑a = ⇑b ∘ ⇑σ
hσ : Monotone ⇑σ
i j : Fin n
hij : σ i ≤ σ j
h : j < i
⊢ False

Tactic:
obtain rfl : i = j := σ.injective (le_antisymm hij (hσ h.le))

Result:
case intro.intro
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h✝ : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ x_1 : Fin n, (f (a x_1)) (x (b (σ x_1))) = 0
this : ⇑a = ⇑b ∘ ⇑σ
hσ : Monotone ⇑σ
i : Fin n
hij : σ i ≤ σ i
h : i < i
⊢ False

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ x_1 : Fin n, (f (a x_1)) (x (b (σ x_1))) = 0
this : ⇑a = ⇑b ∘ ⇑σ
⊢ a = b

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'']

Result:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ x_1 : Fin n, (f (a x_1)) (x (b (σ x_1))) = 0
this : ⇑a = ⇑b ∘ ⇑σ
hσ : Monotone ⇑σ
⊢ a = b