-- Mathlib/GroupTheory/Perm/Sign.lean
theorem signAux_mul {n : ℕ} (f g : Perm (Fin n)) : signAux (f * g) = signAux f * signAux g

Proof state:
case mk
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩ ∈ finPairsLT n
⊢ (if (f * g) a ≤ (f * g) b then -1 else 1) =
    (if
          f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1) *
      if
          g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1

Tactic:
rw [mul_apply, mul_apply]

Result:
case mk
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩ ∈ finPairsLT n
⊢ (if f (g a) ≤ f (g b) then -1 else 1) =
    (if
          f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1) *
      if
          g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1

Proof state:
n : ℕ
f g : Perm (Fin n)
⊢ (f * g).signAux = f.signAux * g.signAux

Tactic:
rw [← signAux_inv g]

Result:
n : ℕ
f g : Perm (Fin n)
⊢ (f * g).signAux = f.signAux * g⁻¹.signAux

Proof state:
n : ℕ
f g : Perm (Fin n)
⊢ (∏ x ∈ finPairsLT n, if (f * g) x.fst ≤ (f * g) x.snd then -1 else 1) =
    ∏ x ∈ finPairsLT n, (if f x.fst ≤ f x.snd then -1 else 1) * if g⁻¹ x.fst ≤ g⁻¹ x.snd then -1 else 1

Tactic:
refine prod_nbij (signBijAux g) signBijAux_mem signBijAux_injOn signBijAux_surj ?_

Result:
n : ℕ
f g : Perm (Fin n)
⊢ ∀ a ∈ finPairsLT n,
    (if (f * g) a.fst ≤ (f * g) a.snd then -1 else 1) =
      (if f (g.signBijAux a).fst ≤ f (g.signBijAux a).snd then -1 else 1) *
        if g⁻¹ (g.signBijAux a).fst ≤ g⁻¹ (g.signBijAux a).snd then -1 else 1

Proof state:
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩.snd < ⟨a, b⟩.fst
h : ¬g b < g a
h₁ : f (g b) ≤ f (g a)
⊢ ¬b = a

Tactic:
exact ne_of_lt hab

Result:
no goals

Proof state:
case pos
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩.snd < ⟨a, 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 ⟨g b, g a⟩.fst ≤ f ⟨g b, g a⟩.snd then -1 else 1) * -1

Tactic:
have : f (g b) ≠ f (g a) := by
  rw [Ne, f.injective.eq_iff, g.injective.eq_iff]
  exact ne_of_lt hab

Result:
case pos
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩.snd < ⟨a, 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 ⟨g b, g a⟩.fst ≤ f ⟨g b, g a⟩.snd then -1 else 1) * -1

Proof state:
n : ℕ
f g : Perm (Fin n)
⊢ (∏ x ∈ finPairsLT n, if (f * g) x.fst ≤ (f * g) x.snd then -1 else 1) =
    (∏ x ∈ finPairsLT n, if f x.fst ≤ f x.snd then -1 else 1) *
      ∏ x ∈ finPairsLT n, if g⁻¹ x.fst ≤ g⁻¹ x.snd then -1 else 1

Tactic:
rw [← prod_mul_distrib]

Result:
n : ℕ
f g : Perm (Fin n)
⊢ (∏ x ∈ finPairsLT n, if (f * g) x.fst ≤ (f * g) x.snd then -1 else 1) =
    ∏ x ∈ finPairsLT n, (if f x.fst ≤ f x.snd then -1 else 1) * if g⁻¹ x.fst ≤ g⁻¹ x.snd then -1 else 1

Proof state:
case neg
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩.snd < ⟨a, 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 ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1) *
      if
          g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1

Tactic:
rw [dif_neg h, inv_apply_self, inv_apply_self, if_pos hab.le]

Result:
case neg
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩.snd < ⟨a, b⟩.fst
h : ¬g b < g a
⊢ (if f (g a) ≤ f (g b) then -1 else 1) = (if f ⟨g b, g a⟩.fst ≤ f ⟨g b, g a⟩.snd then -1 else 1) * -1

Proof state:
case neg
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩.snd < ⟨a, b⟩.fst
h : ¬g b < g a
⊢ (if f (g a) ≤ f (g b) then -1 else 1) = (if f ⟨g b, g a⟩.fst ≤ f ⟨g b, g a⟩.snd then -1 else 1) * -1

Tactic:
by_cases h₁ : f (g b) ≤ f (g a)

Result:
case pos
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩.snd < ⟨a, 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 ⟨g b, g a⟩.fst ≤ f ⟨g b, g a⟩.snd then -1 else 1) * -1

case neg
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩.snd < ⟨a, 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 ⟨g b, g a⟩.fst ≤ f ⟨g b, g a⟩.snd then -1 else 1) * -1

Proof state:
case pos
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩.snd < ⟨a, b⟩.fst
h : ¬g b < g a
h₁ : f (g b) ≤ f (g a)
this : f (g b) ≠ f (g a)
⊢ 1 = -1 * -1

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
f g : Perm (Fin n)
⊢ (f * g).signAux = f.signAux * g⁻¹.signAux

Tactic:
unfold signAux

Result:
n : ℕ
f g : Perm (Fin n)
⊢ (∏ x ∈ finPairsLT n, if (f * g) x.fst ≤ (f * g) x.snd then -1 else 1) =
    (∏ x ∈ finPairsLT n, if f x.fst ≤ f x.snd then -1 else 1) *
      ∏ x ∈ finPairsLT n, if g⁻¹ x.fst ≤ g⁻¹ x.snd then -1 else 1

Proof state:
case mk
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩ ∈ finPairsLT n
⊢ (if f (g a) ≤ f (g b) then -1 else 1) =
    (if
          f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1) *
      if
          g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1

Tactic:
rw [mem_finPairsLT] at hab

Result:
case mk
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩.snd < ⟨a, b⟩.fst
⊢ (if f (g a) ≤ f (g b) then -1 else 1) =
    (if
          f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1) *
      if
          g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1

Proof state:
case pos
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩.snd < ⟨a, b⟩.fst
h : g b < g a
⊢ (if f (g a) ≤ f (g b) then -1 else 1) =
    (if f ⟨g a, g b⟩.fst ≤ f ⟨g a, g b⟩.snd then -1 else 1) * if g⁻¹ ⟨g a, g b⟩.fst ≤ g⁻¹ ⟨g a, g b⟩.snd then -1 else 1

Tactic:
simp only [not_le_of_gt hab, mul_one, mul_ite, mul_neg, Perm.inv_apply_self, if_false]

Result:
no goals

Proof state:
case neg
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩.snd < ⟨a, b⟩.fst
h : ¬g b < g a
h₁ : ¬f (g b) ≤ f (g a)
⊢ -1 = 1 * -1

Tactic:
rfl

Result:
no goals

Proof state:
case mk
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩ ∈ finPairsLT n
⊢ (if (f * g) ⟨a, b⟩.fst ≤ (f * g) ⟨a, b⟩.snd then -1 else 1) =
    (if f (g.signBijAux ⟨a, b⟩).fst ≤ f (g.signBijAux ⟨a, b⟩).snd then -1 else 1) *
      if g⁻¹ (g.signBijAux ⟨a, b⟩).fst ≤ g⁻¹ (g.signBijAux ⟨a, b⟩).snd then -1 else 1

Tactic:
dsimp only [signBijAux]

Result:
case mk
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩ ∈ finPairsLT n
⊢ (if (f * g) a ≤ (f * g) b then -1 else 1) =
    (if
          f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1) *
      if
          g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1

Proof state:
case neg
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩.snd < ⟨a, 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 ⟨g b, g a⟩.fst ≤ f ⟨g b, g a⟩.snd then -1 else 1) * -1

Tactic:
rw [if_neg h₁, if_pos (lt_of_not_ge h₁).le]

Result:
case neg
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩.snd < ⟨a, b⟩.fst
h : ¬g b < g a
h₁ : ¬f (g b) ≤ f (g a)
⊢ -1 = 1 * -1