Theorem: Nat.iter_mul (GMLInit/Data/Nat/Iter.lean)

State before:
α : Sort u_1
f : α → α
m n : Nat
a : α
⊢ iter f (m * n) a = iter (iter f m) n a
Tactic:
induction n generalizing a with
| zero => rfl
| succ n ih =>
  calc
  _ = iter f (m * n + m) a := rfl
  _ = iter f (m * n) (iter f m a) := by rw [iter_add]
  _ = iter (iter f m) n (iter f m a) := by rw [ih]
  _ = iter (iter f m) (n + 1) a := by rw [iter_succ]
State after:
no goals

State before:
case zero
α : Sort u_1
f : α → α
m : Nat
a : α
⊢ iter f (m * 0) a = iter (iter f m) 0 a
Tactic:
rfl
State after:
no goals

State before:
case succ
α : Sort u_1
f : α → α
m n : Nat
ih : ∀ (a : α), iter f (m * n) a = iter (iter f m) n a
a : α
⊢ iter f (m * (n + 1)) a = iter (iter f m) (n + 1) a
Tactic:
calc
_ = iter f (m * n + m) a := rfl
_ = iter f (m * n) (iter f m a) := by rw [iter_add]
_ = iter (iter f m) n (iter f m a) := by rw [ih]
_ = iter (iter f m) (n + 1) a := by rw [iter_succ]
State after:
no goals

State before:
α : Sort u_1
f : α → α
m n : Nat
ih : ∀ (a : α), iter f (m * n) a = iter (iter f m) n a
a : α
⊢ iter f (m * n + m) a = iter f (m * n) (iter f m a)
Tactic:
rw [iter_add]
State after:
no goals

State before:
α : Sort u_1
f : α → α
m n : Nat
ih : ∀ (a : α), iter f (m * n) a = iter (iter f m) n a
a : α
⊢ iter f (m * n) (iter f m a) = iter (iter f m) n (iter f m a)
Tactic:
rw [ih]
State after:
no goals

State before:
α : Sort u_1
f : α → α
m n : Nat
ih : ∀ (a : α), iter f (m * n) a = iter (iter f m) n a
a : α
⊢ iter (iter f m) n (iter f m a) = iter (iter f m) (n + 1) a
Tactic:
rw [iter_succ]
State after:
no goals