α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a : (_ : Fin (n + 2)) × Fin (n + 2)
ha₁ : a ∈ finPairsLT (n + 2)
ha₂ : ¬a ∈ {{ fst := 1, snd := 0 }}
⊢ (if ↑(swap 0 1) a.fst ≤ ↑(swap 0 1) a.snd then -1 else 1) = 1
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
⊢ signAux (swap 0 1) = ∏ x in {{ fst := 1, snd := 0 }}, if ↑(swap 0 1) x.fst ≤ ↑(swap 0 1) x.snd then -1 else 1
refine' Eq.symm (prod_subset (fun ⟨x₁, x₂⟩ => by
  simp (config := { contextual := true }) [mem_finPairsLT, Fin.one_pos]) fun a ha₁ ha₂ => _)
case mk
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₁ : { fst := a₁, snd := a₂ } ∈ finPairsLT (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
⊢ (if ↑(swap 0 1) { fst := a₁, snd := a₂ }.fst ≤ ↑(swap 0 1) { fst := a₁, snd := a₂ }.snd then -1 else 1) = 1
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a : (_ : Fin (n + 2)) × Fin (n + 2)
ha₁ : a ∈ finPairsLT (n + 2)
ha₂ : ¬a ∈ {{ fst := 1, snd := 0 }}
⊢ (if ↑(swap 0 1) a.fst ≤ ↑(swap 0 1) a.snd then -1 else 1) = 1
rcases a with ⟨a₁, a₂⟩
case mk
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
⊢ (if ↑(swap 0 1) { fst := a₁, snd := a₂ }.fst ≤ ↑(swap 0 1) { fst := a₁, snd := a₂ }.snd then -1 else 1) = 1
case mk
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₁ : { fst := a₁, snd := a₂ } ∈ finPairsLT (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
⊢ (if ↑(swap 0 1) { fst := a₁, snd := a₂ }.fst ≤ ↑(swap 0 1) { fst := a₁, snd := a₂ }.snd then -1 else 1) = 1
replace ha₁ : a₂ < a₁ := mem_finPairsLT.1 ha₁
case mk
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) a₂ then -1 else 1) = 1
case mk
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
⊢ (if ↑(swap 0 1) { fst := a₁, snd := a₂ }.fst ≤ ↑(swap 0 1) { fst := a₁, snd := a₂ }.snd then -1 else 1) = 1
dsimp only
case mk.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₂ : Fin (n + 2)
ha₂ : ¬{ fst := 0, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < 0
⊢ (if ↑(swap 0 1) 0 ≤ ↑(swap 0 1) a₂ then -1 else 1) = 1

case mk.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
H : 0 < a₁
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) a₂ then -1 else 1) = 1
case mk
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) a₂ then -1 else 1) = 1
rcases a₁.zero_le.eq_or_lt with (rfl | H)
case mk.inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₂ : ¬{ fst := a₁, snd := 0 } ∈ {{ fst := 1, snd := 0 }}
ha₁ : 0 < a₁
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) 0 then -1 else 1) = 1

case mk.inr.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) a₂ then -1 else 1) = 1
case mk.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
H : 0 < a₁
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) a₂ then -1 else 1) = 1
rcases a₂.zero_le.eq_or_lt with (rfl | H')
no goals
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x✝ : (_ : Fin (n + 2)) × Fin (n + 2)
x₁ x₂ : Fin (n + 2)
⊢ { fst := x₁, snd := x₂ } ∈ {{ fst := 1, snd := 0 }} → { fst := x₁, snd := x₂ } ∈ finPairsLT (n + 2)
simp (config := { contextual := true }) [mem_finPairsLT, Fin.one_pos]
no goals
case mk.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₂ : Fin (n + 2)
ha₂ : ¬{ fst := 0, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < 0
⊢ (if ↑(swap 0 1) 0 ≤ ↑(swap 0 1) a₂ then -1 else 1) = 1
exact absurd a₂.zero_le ha₁.not_le
case mk.inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) 0 then -1 else 1) = 1
case mk.inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₂ : ¬{ fst := a₁, snd := 0 } ∈ {{ fst := 1, snd := 0 }}
ha₁ : 0 < a₁
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) 0 then -1 else 1) = 1
simp only [and_true_iff, eq_self_iff_true, heq_iff_eq, mem_singleton, Sigma.mk.inj_iff] at ha₂
case mk.inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
this : 1 < a₁
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) 0 then -1 else 1) = 1
case mk.inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) 0 then -1 else 1) = 1
have : 1 < a₁ := lt_of_le_of_ne (Nat.succ_le_of_lt ha₁)
  (Ne.symm (by intro h; apply ha₂; simp [h]))
case mk.inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
this : 1 < a₁
h01 : ↑(swap 0 1) 0 = 1
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) 0 then -1 else 1) = 1
case mk.inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
this : 1 < a₁
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) 0 then -1 else 1) = 1
have h01 : Equiv.swap (0 : Fin (n + 2)) 1 0 = 1 := by simp
no goals
case mk.inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
this : 1 < a₁
h01 : ↑(swap 0 1) 0 = 1
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) 0 then -1 else 1) = 1
rw [swap_apply_of_ne_of_ne (ne_of_gt H) ha₂, h01, if_neg this.not_le]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
h : a₁ = 1
⊢ False
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
⊢ a₁ ≠ 1
intro h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
h : a₁ = 1
⊢ a₁ = 1
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
h : a₁ = 1
⊢ False
apply ha₂
no goals
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
h : a₁ = 1
⊢ a₁ = 1
simp [h]
no goals
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
this : 1 < a₁
⊢ ↑(swap 0 1) 0 = 1
simp
case mk.inr.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) a₂ then -1 else 1) = 1
case mk.inr.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) a₂ then -1 else 1) = 1
have le : 1 ≤ a₂ := Nat.succ_le_of_lt H'
case mk.inr.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) a₂ then -1 else 1) = 1
case mk.inr.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) a₂ then -1 else 1) = 1
have lt : 1 < a₁ := le.trans_lt ha₁
case mk.inr.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
h01 : ↑(swap 0 1) 1 = 0
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) a₂ then -1 else 1) = 1
case mk.inr.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) a₂ then -1 else 1) = 1
have h01 : Equiv.swap (0 : Fin (n + 2)) 1 1 = 0 := by simp only [swap_apply_right]
case mk.inr.inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
lt : 1 < a₁
h01 : ↑(swap 0 1) 1 = 0
ha₂ : ¬{ fst := a₁, snd := 1 } ∈ {{ fst := 1, snd := 0 }}
ha₁ : 1 < a₁
H' : 0 < 1
le : 1 ≤ 1
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) 1 then -1 else 1) = 1

case mk.inr.inr.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
h01 : ↑(swap 0 1) 1 = 0
lt' : 1 < a₂
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) a₂ then -1 else 1) = 1
case mk.inr.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
h01 : ↑(swap 0 1) 1 = 0
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) a₂ then -1 else 1) = 1
rcases le.eq_or_lt with (rfl | lt')
no goals
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
⊢ ↑(swap 0 1) 1 = 0
simp only [swap_apply_right]
no goals
case mk.inr.inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
lt : 1 < a₁
h01 : ↑(swap 0 1) 1 = 0
ha₂ : ¬{ fst := a₁, snd := 1 } ∈ {{ fst := 1, snd := 0 }}
ha₁ : 1 < a₁
H' : 0 < 1
le : 1 ≤ 1
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) 1 then -1 else 1) = 1
rw [swap_apply_of_ne_of_ne H.ne' lt.ne', h01, if_neg H.not_le]
no goals
case mk.inr.inr.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
h01 : ↑(swap 0 1) 1 = 0
lt' : 1 < a₂
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) a₂ then -1 else 1) = 1
rw [swap_apply_of_ne_of_ne (ne_of_gt H) (ne_of_gt lt),
  swap_apply_of_ne_of_ne (ne_of_gt H') (ne_of_gt lt'), if_neg ha₁.not_le]