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

State before:
m n : Nat
x : Permutation n
k : Nat
h : sign x = false
⊢ sign (x ^ k) = false
Tactic:
induction k with
| zero => rw [powNat_zero, sign_one]
| succ k IH =>
  rewrite [powNat_succ, sign_mul, h, IH]
  decide
State after:
no goals

State before:
case zero
m n : Nat
x : Permutation n
h : sign x = false
⊢ sign (x ^ Nat.zero) = false
Tactic:
rw [powNat_zero, sign_one]
State after:
no goals

State before:
case succ
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
IH : sign (x ^ k) = false
⊢ sign (x ^ Nat.succ k) = false
Tactic:
rewrite [powNat_succ, sign_mul, h, IH]
State after:
case succ
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
IH : sign (x ^ k) = false
⊢ (false != false) = false

State before:
case succ
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
IH : sign (x ^ k) = false
⊢ (false != false) = false
Tactic:
decide
State after:
no goals