Theorem: Permutation.powNat_add (Fifteen/Data/Permutation/Basic.lean)

State before:
n : Nat
x : Permutation n
k l : Nat
⊢ x ^ (k + l) = x ^ k * x ^ l
Tactic:
induction k with
| zero =>
  simp only [Nat.zero_eq, Nat.zero_add, powNat_zero, one_mul]
| succ k IH =>
  simp only [Nat.succ_add, powNat_succ]
  rw [mul_assoc, IH]
State after:
no goals

State before:
case zero
n : Nat
x : Permutation n
l : Nat
⊢ x ^ (Nat.zero + l) = x ^ Nat.zero * x ^ l
Tactic:
simp only [Nat.zero_eq, Nat.zero_add, powNat_zero, one_mul]
State after:
no goals

State before:
case succ
n : Nat
x : Permutation n
l k : Nat
IH : x ^ (k + l) = x ^ k * x ^ l
⊢ x ^ (Nat.succ k + l) = x ^ Nat.succ k * x ^ l
Tactic:
simp only [Nat.succ_add, powNat_succ]
State after:
case succ
n : Nat
x : Permutation n
l k : Nat
IH : x ^ (k + l) = x ^ k * x ^ l
⊢ x * x ^ (k + l) = x * x ^ k * x ^ l

State before:
case succ
n : Nat
x : Permutation n
l k : Nat
IH : x ^ (k + l) = x ^ k * x ^ l
⊢ x * x ^ (k + l) = x * x ^ k * x ^ l
Tactic:
rw [mul_assoc, IH]
State after:
no goals