Theorem: Permutation.sign_mul (Fifteen/Data/Permutation/Sign.lean)

State before:
m n : Nat
x y : Permutation n
this :
  (fun x => x % 2) (inversionNum x + inversionNum y) =
    (fun x => x % 2)
      (inversionNum (x * y) +
        2 * BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd])
⊢ sign (x * y) = (sign x != sign y)
Tactic:
conv at this =>
  dsimp; rw [Nat.add_mul_mod_self_left, Nat.add_mod]
State after:
m n : Nat
x y : Permutation n
this : (inversionNum x % 2 + inversionNum y % 2) % 2 = inversionNum (x * y) % 2
⊢ sign (x * y) = (sign x != sign y)

State before:
m n : Nat
x y : Permutation n
this : (inversionNum x % 2 + inversionNum y % 2) % 2 = inversionNum (x * y) % 2
⊢ sign (x * y) = (sign x != sign y)
Tactic:
dsimp [sign]
State after:
m n : Nat
x y : Permutation n
this : (inversionNum x % 2 + inversionNum y % 2) % 2 = inversionNum (x * y) % 2
⊢ (inversionNum (x * y) % 2 == 1) = ((inversionNum x % 2 == 1) != (inversionNum y % 2 == 1))

State before:
m n : Nat
x y : Permutation n
this : (inversionNum x % 2 + inversionNum y % 2) % 2 = inversionNum (x * y) % 2
⊢ (inversionNum (x * y) % 2 == 1) = ((inversionNum x % 2 == 1) != (inversionNum y % 2 == 1))
Tactic:
rw [← this]
State after:
m n : Nat
x y : Permutation n
this : (inversionNum x % 2 + inversionNum y % 2) % 2 = inversionNum (x * y) % 2
⊢ ((inversionNum x % 2 + inversionNum y % 2) % 2 == 1) = ((inversionNum x % 2 == 1) != (inversionNum y % 2 == 1))

State before:
m n : Nat
x y : Permutation n
this : (inversionNum x % 2 + inversionNum y % 2) % 2 = inversionNum (x * y) % 2
⊢ ((inversionNum x % 2 + inversionNum y % 2) % 2 == 1) = ((inversionNum x % 2 == 1) != (inversionNum y % 2 == 1))
Tactic:
clear this
State after:
m n : Nat
x y : Permutation n
⊢ ((inversionNum x % 2 + inversionNum y % 2) % 2 == 1) = ((inversionNum x % 2 == 1) != (inversionNum y % 2 == 1))

State before:
m n : Nat
x y : Permutation n
⊢ ((inversionNum x % 2 + inversionNum y % 2) % 2 == 1) = ((inversionNum x % 2 == 1) != (inversionNum y % 2 == 1))
Tactic:
generalize x.inversionNum = m
State after:
m✝ n : Nat
x y : Permutation n
m : Nat
⊢ ((m % 2 + inversionNum y % 2) % 2 == 1) = ((m % 2 == 1) != (inversionNum y % 2 == 1))

State before:
m✝ n : Nat
x y : Permutation n
m : Nat
⊢ ((m % 2 + inversionNum y % 2) % 2 == 1) = ((m % 2 == 1) != (inversionNum y % 2 == 1))
Tactic:
generalize y.inversionNum = n
State after:
m✝ n✝ : Nat
x y : Permutation n✝
m n : Nat
⊢ ((m % 2 + n % 2) % 2 == 1) = ((m % 2 == 1) != (n % 2 == 1))

State before:
m✝ n✝ : Nat
x y : Permutation n✝
m n : Nat
⊢ ((m % 2 + n % 2) % 2 == 1) = ((m % 2 == 1) != (n % 2 == 1))
Tactic:
cases m.mod_two_eq_zero_or_one
  <;> cases n.mod_two_eq_zero_or_one
  <;> rename_i hm hn
  <;> simp only [hm, hn]
State after:
no goals