α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
⊢ signAux (f * g) = signAux f * signAux g⁻¹
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
⊢ signAux (f * g) = signAux f * signAux g
rw [← signAux_inv g]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
⊢ (∏ x in finPairsLT n, if ↑(f * g) x.fst ≤ ↑(f * g) x.snd then -1 else 1) =
    (∏ x in finPairsLT n, if ↑f x.fst ≤ ↑f x.snd then -1 else 1) *
      ∏ x in finPairsLT n, if ↑g⁻¹ x.fst ≤ ↑g⁻¹ x.snd then -1 else 1
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
⊢ signAux (f * g) = signAux f * signAux g⁻¹
unfold signAux
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
⊢ (∏ x in finPairsLT n, if ↑(f * g) x.fst ≤ ↑(f * g) x.snd then -1 else 1) =
    ∏ x in finPairsLT n, (if ↑f x.fst ≤ ↑f x.snd then -1 else 1) * if ↑g⁻¹ x.fst ≤ ↑g⁻¹ x.snd then -1 else 1
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
⊢ (∏ x in finPairsLT n, if ↑(f * g) x.fst ≤ ↑(f * g) x.snd then -1 else 1) =
    (∏ x in finPairsLT n, if ↑f x.fst ≤ ↑f x.snd then -1 else 1) *
      ∏ x in finPairsLT n, if ↑g⁻¹ x.fst ≤ ↑g⁻¹ x.snd then -1 else 1
rw [← prod_mul_distrib]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
⊢ ∀ (a : (_ : Fin n) × Fin n) (ha : a ∈ finPairsLT n),
    (if ↑(f * g) a.fst ≤ ↑(f * g) a.snd then -1 else 1) =
      (if ↑f ((fun a x => signBijAux g a) a ha).fst ≤ ↑f ((fun a x => signBijAux g a) a ha).snd then -1 else 1) *
        if ↑g⁻¹ ((fun a x => signBijAux g a) a ha).fst ≤ ↑g⁻¹ ((fun a x => signBijAux g a) a ha).snd then -1 else 1
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
⊢ (∏ x in finPairsLT n, if ↑(f * g) x.fst ≤ ↑(f * g) x.snd then -1 else 1) =
    ∏ x in finPairsLT n, (if ↑f x.fst ≤ ↑f x.snd then -1 else 1) * if ↑g⁻¹ x.fst ≤ ↑g⁻¹ x.snd then -1 else 1
refine'
  prod_bij (fun a _ => signBijAux g a) signBijAux_mem _ signBijAux_inj
  (by simpa using signBijAux_surj)
case mk
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b } ∈ finPairsLT n
⊢ (if ↑(f * g) { fst := a, snd := b }.fst ≤ ↑(f * g) { fst := a, snd := b }.snd then -1 else 1) =
    (if
          ↑f ((fun a x => signBijAux g a) { fst := a, snd := b } hab).fst ≤
            ↑f ((fun a x => signBijAux g a) { fst := a, snd := b } hab).snd then
        -1
      else 1) *
      if
          ↑g⁻¹ ((fun a x => signBijAux g a) { fst := a, snd := b } hab).fst ≤
            ↑g⁻¹ ((fun a x => signBijAux g a) { fst := a, snd := b } hab).snd then
        -1
      else 1
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
⊢ ∀ (a : (_ : Fin n) × Fin n) (ha : a ∈ finPairsLT n),
    (if ↑(f * g) a.fst ≤ ↑(f * g) a.snd then -1 else 1) =
      (if ↑f ((fun a x => signBijAux g a) a ha).fst ≤ ↑f ((fun a x => signBijAux g a) a ha).snd then -1 else 1) *
        if ↑g⁻¹ ((fun a x => signBijAux g a) a ha).fst ≤ ↑g⁻¹ ((fun a x => signBijAux g a) a ha).snd then -1 else 1
rintro ⟨a, b⟩ hab
case mk
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b } ∈ finPairsLT n
⊢ (if ↑(f * g) a ≤ ↑(f * g) b then -1 else 1) =
    (if
          ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1) *
      if
          ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1
case mk
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b } ∈ finPairsLT n
⊢ (if ↑(f * g) { fst := a, snd := b }.fst ≤ ↑(f * g) { fst := a, snd := b }.snd then -1 else 1) =
    (if
          ↑f ((fun a x => signBijAux g a) { fst := a, snd := b } hab).fst ≤
            ↑f ((fun a x => signBijAux g a) { fst := a, snd := b } hab).snd then
        -1
      else 1) *
      if
          ↑g⁻¹ ((fun a x => signBijAux g a) { fst := a, snd := b } hab).fst ≤
            ↑g⁻¹ ((fun a x => signBijAux g a) { fst := a, snd := b } hab).snd then
        -1
      else 1
dsimp only [signBijAux]
case mk
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b } ∈ finPairsLT n
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if
          ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1) *
      if
          ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1
case mk
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b } ∈ finPairsLT n
⊢ (if ↑(f * g) a ≤ ↑(f * g) b then -1 else 1) =
    (if
          ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1) *
      if
          ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1
rw [mul_apply, mul_apply]
case mk
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if
          ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1) *
      if
          ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1
case mk
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b } ∈ finPairsLT n
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if
          ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1) *
      if
          ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1
rw [mem_finPairsLT] at hab
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ↑g b < ↑g a
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if
          ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1) *
      if
          ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1

case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if
          ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1) *
      if
          ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1
case mk
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if
          ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1) *
      if
          ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1
by_cases h : g b < g a
no goals
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
⊢ ∀ (b : (_ : Fin n) × Fin n), b ∈ finPairsLT n → ∃ a ha, b = (fun a x => signBijAux g a) a ha
simpa using signBijAux_surj
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ↑g b < ↑g a
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if ↑f { fst := ↑g a, snd := ↑g b }.fst ≤ ↑f { fst := ↑g a, snd := ↑g b }.snd then -1 else 1) *
      if ↑g⁻¹ { fst := ↑g a, snd := ↑g b }.fst ≤ ↑g⁻¹ { fst := ↑g a, snd := ↑g b }.snd then -1 else 1
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ↑g b < ↑g a
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if
          ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1) *
      if
          ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1
rw [dif_pos h]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ↑g b < ↑g a
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    if a ≤ b then -if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1 else if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ↑g b < ↑g a
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if ↑f { fst := ↑g a, snd := ↑g b }.fst ≤ ↑f { fst := ↑g a, snd := ↑g b }.snd then -1 else 1) *
      if ↑g⁻¹ { fst := ↑g a, snd := ↑g b }.fst ≤ ↑g⁻¹ { fst := ↑g a, snd := ↑g b }.snd then -1 else 1
simp only [not_le_of_gt hab, mul_one, mul_ite, mul_neg, Perm.inv_apply_self, if_false]
case pos.inl.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : b < a
h : ↑g b < ↑g a
h₁ : ↑f (↑g a) ≤ ↑f (↑g b)
h₂ : a ≤ b
⊢ -1 = - -1

case pos.inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : b < a
h : ↑g b < ↑g a
h₁ : ¬↑f (↑g a) ≤ ↑f (↑g b)
h₃ : a ≤ b
⊢ 1 = -1
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ↑g b < ↑g a
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    if a ≤ b then -if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1 else if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1
split_ifs with h₁ h₂ h₃ <;> dsimp at *
case pos.inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : b < a
h : ↑g b < ↑g a
h₁ : ¬↑f (↑g a) ≤ ↑f (↑g b)
h₃ : a ≤ b
⊢ 1 = -1
case pos.inl.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : b < a
h : ↑g b < ↑g a
h₁ : ↑f (↑g a) ≤ ↑f (↑g b)
h₂ : a ≤ b
⊢ -1 = - -1

case pos.inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : b < a
h : ↑g b < ↑g a
h₁ : ¬↑f (↑g a) ≤ ↑f (↑g b)
h₃ : a ≤ b
⊢ 1 = -1
. exact absurd hab (not_lt_of_ge h₂)
no goals
case pos.inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : b < a
h : ↑g b < ↑g a
h₁ : ¬↑f (↑g a) ≤ ↑f (↑g b)
h₃ : a ≤ b
⊢ 1 = -1
. exact absurd hab (not_lt_of_ge h₃)
no goals
case pos.inl.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : b < a
h : ↑g b < ↑g a
h₁ : ↑f (↑g a) ≤ ↑f (↑g b)
h₂ : a ≤ b
⊢ -1 = - -1
exact absurd hab (not_lt_of_ge h₂)
no goals
case pos.inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : b < a
h : ↑g b < ↑g a
h₁ : ¬↑f (↑g a) ≤ ↑f (↑g b)
h₃ : a ≤ b
⊢ 1 = -1
exact absurd hab (not_lt_of_ge h₃)
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if ↑f { fst := ↑g b, snd := ↑g a }.fst ≤ ↑f { fst := ↑g b, snd := ↑g a }.snd then -1 else 1) * -1
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if
          ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1) *
      if
          ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1
rw [dif_neg h, inv_apply_self, inv_apply_self, if_pos hab.le]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
h₁ : ↑f (↑g b) ≤ ↑f (↑g a)
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if ↑f { fst := ↑g b, snd := ↑g a }.fst ≤ ↑f { fst := ↑g b, snd := ↑g a }.snd then -1 else 1) * -1

case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
h₁ : ¬↑f (↑g b) ≤ ↑f (↑g a)
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if ↑f { fst := ↑g b, snd := ↑g a }.fst ≤ ↑f { fst := ↑g b, snd := ↑g a }.snd then -1 else 1) * -1
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if ↑f { fst := ↑g b, snd := ↑g a }.fst ≤ ↑f { fst := ↑g b, snd := ↑g a }.snd then -1 else 1) * -1
by_cases h₁ : f (g b) ≤ f (g a)
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
h₁ : ↑f (↑g b) ≤ ↑f (↑g a)
this : ↑f (↑g b) ≠ ↑f (↑g a)
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if ↑f { fst := ↑g b, snd := ↑g a }.fst ≤ ↑f { fst := ↑g b, snd := ↑g a }.snd then -1 else 1) * -1
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
h₁ : ↑f (↑g b) ≤ ↑f (↑g a)
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if ↑f { fst := ↑g b, snd := ↑g a }.fst ≤ ↑f { fst := ↑g b, snd := ↑g a }.snd then -1 else 1) * -1
have : f (g b) ≠ f (g a) := by
  rw [Ne.def, f.injective.eq_iff, g.injective.eq_iff]
  exact ne_of_lt hab
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
h₁ : ↑f (↑g b) ≤ ↑f (↑g a)
this : ↑f (↑g b) ≠ ↑f (↑g a)
⊢ 1 = -1 * -1
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
h₁ : ↑f (↑g b) ≤ ↑f (↑g a)
this : ↑f (↑g b) ≠ ↑f (↑g a)
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if ↑f { fst := ↑g b, snd := ↑g a }.fst ≤ ↑f { fst := ↑g b, snd := ↑g a }.snd then -1 else 1) * -1
rw [if_pos h₁, if_neg (h₁.lt_of_ne this).not_le]
no goals
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
h₁ : ↑f (↑g b) ≤ ↑f (↑g a)
this : ↑f (↑g b) ≠ ↑f (↑g a)
⊢ 1 = -1 * -1
rfl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
h₁ : ↑f (↑g b) ≤ ↑f (↑g a)
⊢ ¬b = a
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
h₁ : ↑f (↑g b) ≤ ↑f (↑g a)
⊢ ↑f (↑g b) ≠ ↑f (↑g a)
rw [Ne.def, f.injective.eq_iff, g.injective.eq_iff]
no goals
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
h₁ : ↑f (↑g b) ≤ ↑f (↑g a)
⊢ ¬b = a
exact ne_of_lt hab
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
h₁ : ¬↑f (↑g b) ≤ ↑f (↑g a)
⊢ -1 = 1 * -1
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
h₁ : ¬↑f (↑g b) ≤ ↑f (↑g a)
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if ↑f { fst := ↑g b, snd := ↑g a }.fst ≤ ↑f { fst := ↑g b, snd := ↑g a }.snd then -1 else 1) * -1
rw [if_neg h₁, if_pos (lt_of_not_ge h₁).le]
no goals
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
h₁ : ¬↑f (↑g b) ≤ ↑f (↑g a)
⊢ -1 = 1 * -1
rfl