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

State before:
m n : Nat
x : Permutation n
k : Int
h : sign x = false
⊢ sign (x ^ k) = false
Tactic:
rcases k with ⟨k⟩ | ⟨k⟩
State after:
case ofNat
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (x ^ Int.ofNat k) = false

case negSucc
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (x ^ Int.negSucc k) = false

State before:
case ofNat
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (x ^ Int.ofNat k) = false

case negSucc
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (x ^ Int.negSucc k) = false
Tactic:
. show sign (x ^ (k : Nat)) = false
  exact sign_powNat_of_even x k h
State after:
case negSucc
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (x ^ Int.negSucc k) = false

State before:
case negSucc
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (x ^ Int.negSucc k) = false
Tactic:
. show sign (x.inv ^ (k+1 : Nat)) = false
  apply sign_powNat_of_even
  rewrite [x.sign_inv]
  exact h
State after:
no goals

State before:
case ofNat
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (x ^ Int.ofNat k) = false
Tactic:
show sign (x ^ (k : Nat)) = false
State after:
case ofNat
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (x ^ k) = false

State before:
case ofNat
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (x ^ k) = false
Tactic:
exact sign_powNat_of_even x k h
State after:
no goals

State before:
case negSucc
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (x ^ Int.negSucc k) = false
Tactic:
show sign (x.inv ^ (k+1 : Nat)) = false
State after:
case negSucc
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (inv x ^ (k + 1)) = false

State before:
case negSucc
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (inv x ^ (k + 1)) = false
Tactic:
apply sign_powNat_of_even
State after:
case negSucc.h
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (inv x) = false

State before:
case negSucc.h
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (inv x) = false
Tactic:
rewrite [x.sign_inv]
State after:
case negSucc.h
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign x = false

State before:
case negSucc.h
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign x = false
Tactic:
exact h
State after:
no goals