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

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 (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_pos h]

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
⊢ (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

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)
⊢ (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_pos h₁, if_neg (h₁.lt_of_ne this).not_le]

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)
⊢ 1 = -1 * -1

Proof state:
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

Tactic:
by_cases h : g b < 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
⊢ (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

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

Proof state:
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

Tactic:
rintro ⟨a, b⟩ hab

Result:
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

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)
⊢ f (g b) ≠ f (g a)

Tactic:
rw [Ne, f.injective.eq_iff, g.injective.eq_iff]

Result:
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