case zero
α : Type u
β : Type v
f g : α → α
h : Commute f g
⊢ (f ∘ g)^[Nat.zero] = f^[Nat.zero] ∘ g^[Nat.zero]

case succ
α : Type u
β : Type v
f g : α → α
h : Commute f g
n : ℕ
ihn : (f ∘ g)^[n] = f^[n] ∘ g^[n]
⊢ (f ∘ g)^[Nat.succ n] = f^[Nat.succ n] ∘ g^[Nat.succ n]
α : Type u
β : Type v
f g : α → α
h : Commute f g
n : ℕ
⊢ (f ∘ g)^[n] = f^[n] ∘ g^[n]
induction' n with n ihn
case succ.h
α : Type u
β : Type v
f g : α → α
h : Commute f g
n : ℕ
ihn : (f ∘ g)^[n] = f^[n] ∘ g^[n]
x : α
⊢ ((f ∘ g)^[Nat.succ n]) x = (f^[Nat.succ n] ∘ g^[Nat.succ n]) x
case succ
α : Type u
β : Type v
f g : α → α
h : Commute f g
n : ℕ
ihn : (f ∘ g)^[n] = f^[n] ∘ g^[n]
⊢ (f ∘ g)^[Nat.succ n] = f^[Nat.succ n] ∘ g^[Nat.succ n]
funext x
no goals
case succ.h
α : Type u
β : Type v
f g : α → α
h : Commute f g
n : ℕ
ihn : (f ∘ g)^[n] = f^[n] ∘ g^[n]
x : α
⊢ ((f ∘ g)^[Nat.succ n]) x = (f^[Nat.succ n] ∘ g^[Nat.succ n]) x
simp only [ihn, (h.iterate_right n).eq, iterate_succ, comp_apply]
no goals
case zero
α : Type u
β : Type v
f g : α → α
h : Commute f g
⊢ (f ∘ g)^[Nat.zero] = f^[Nat.zero] ∘ g^[Nat.zero]
rfl