[GOAL]
α : Type u
β : Type v
f : α → α
n✝ n : ℕ
ihn : id^[n] = id
⊢ id^[Nat.succ n] = id
[PROOFSTEP]
rw [iterate_succ, ihn, comp.left_id]
[GOAL]
α : Type u
β : Type v
f : α → α
m n : ℕ
⊢ f^[m + Nat.succ n] = f^[m] ∘ f^[Nat.succ n]
[PROOFSTEP]
rw [Nat.add_succ, iterate_succ, iterate_succ, iterate_add m n]
[GOAL]
α : Type u
β : Type v
f : α → α
m n : ℕ
⊢ (f^[m] ∘ f^[n]) ∘ f = f^[m] ∘ f^[n] ∘ f
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
f : α → α
m n : ℕ
x : α
⊢ f^[m + n] x = f^[m] (f^[n] x)
[PROOFSTEP]
rw [iterate_add f m n]
[GOAL]
α : Type u
β : Type v
f : α → α
m n : ℕ
x : α
⊢ (f^[m] ∘ f^[n]) x = f^[m] (f^[n] x)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
f : α → α
m : ℕ
⊢ f^[m * 0] = f^[m]^[0]
[PROOFSTEP]
simp only [Nat.mul_zero, iterate_zero]
[GOAL]
α : Type u
β : Type v
f : α → α
m n : ℕ
⊢ f^[m * (n + 1)] = f^[m]^[n + 1]
[PROOFSTEP]
simp only [Nat.mul_succ, Nat.mul_one, iterate_one, iterate_add, iterate_mul m n]
[GOAL]
α : Type u
β : Type v
f : α → α
x : α
h : f x = x
n✝ n : ℕ
ihn : f^[n] x = x
⊢ f^[Nat.succ n] x = x
[PROOFSTEP]
rw [iterate_succ_apply, h, ihn]
[GOAL]
α : Type u
β : Type v
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
n k : ℕ
⊢ Semiconj f^[n] (g k) (g (n + k))
[PROOFSTEP]
induction' n with n ihn generalizing k
[GOAL]
case zero
α : Type u
β : Type v
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
k✝ k : ℕ
⊢ Semiconj f^[Nat.zero] (g k) (g (Nat.zero + k))
[PROOFSTEP]
rw [Nat.zero_add]
[GOAL]
case zero
α : Type u
β : Type v
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
k✝ k : ℕ
⊢ Semiconj f^[Nat.zero] (g k) (g k)
[PROOFSTEP]
exact id_left
[GOAL]
case succ
α : Type u
β : Type v
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
k✝ n : ℕ
ihn : ∀ (k : ℕ), Semiconj f^[n] (g k) (g (n + k))
k : ℕ
⊢ Semiconj f^[Nat.succ n] (g k) (g (Nat.succ n + k))
[PROOFSTEP]
rw [Nat.succ_eq_add_one, Nat.add_right_comm, Nat.add_assoc]
[GOAL]
case succ
α : Type u
β : Type v
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
k✝ n : ℕ
ihn : ∀ (k : ℕ), Semiconj f^[n] (g k) (g (n + k))
k : ℕ
⊢ Semiconj f^[n + 1] (g k) (g (n + (k + 1)))
[PROOFSTEP]
exact (H k).comp_left (ihn (k + 1))
[GOAL]
α : Type u
β : Type v
f g : α → α
h : Commute f g
n✝ : ℕ
x : α
hx : f x = g x
n : ℕ
ihn : f^[n] x = g^[n] x
⊢ f^[Nat.succ n] x = g^[Nat.succ n] x
[PROOFSTEP]
simp only [iterate_succ_apply, hx, (h.iterate_left n).eq, ihn, ((refl g).iterate_right n).eq]
[GOAL]
α : Type u
β : Type v
f g : α → α
h : Commute f g
n : ℕ
⊢ (f ∘ g)^[n] = f^[n] ∘ g^[n]
[PROOFSTEP]
induction' n with n ihn
[GOAL]
case zero
α : Type u
β : Type v
f g : α → α
h : Commute f g
⊢ (f ∘ g)^[Nat.zero] = f^[Nat.zero] ∘ g^[Nat.zero]
[PROOFSTEP]
rfl
[GOAL]
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]
[PROOFSTEP]
funext x
[GOAL]
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
[PROOFSTEP]
simp only [ihn, (h.iterate_right n).eq, iterate_succ, comp_apply]
[GOAL]
α : Type u
β : Type v
f : α → α
n : ℕ
⊢ f^[Nat.succ n] = f ∘ f^[n]
[PROOFSTEP]
rw [iterate_succ, (Commute.self_iterate f n).comp_eq]
[GOAL]
α : Type u
β : Type v
f : α → α
n : ℕ
x : α
⊢ f^[Nat.succ n] x = f (f^[n] x)
[PROOFSTEP]
rw [iterate_succ']
[GOAL]
α : Type u
β : Type v
f : α → α
n : ℕ
x : α
⊢ (f ∘ f^[n]) x = f (f^[n] x)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
f : α → α
n : ℕ
hn : 0 < n
⊢ f^[Nat.pred n] ∘ f = f^[n]
[PROOFSTEP]
rw [← iterate_succ, Nat.succ_pred_eq_of_pos hn]
[GOAL]
α : Type u
β : Type v
f : α → α
n : ℕ
hn : 0 < n
⊢ f ∘ f^[Nat.pred n] = f^[n]
[PROOFSTEP]
rw [← iterate_succ', Nat.succ_pred_eq_of_pos hn]
[GOAL]
α : Type u
β : Type v
f : α → α
m n✝¹ : ℕ
a : α
g : α → α
hg : LeftInverse g f
n✝ n : ℕ
ihn : LeftInverse g^[n] f^[n]
⊢ LeftInverse g^[Nat.succ n] f^[Nat.succ n]
[PROOFSTEP]
rw [iterate_succ', iterate_succ]
[GOAL]
α : Type u
β : Type v
f : α → α
m n✝¹ : ℕ
a : α
g : α → α
hg : LeftInverse g f
n✝ n : ℕ
ihn : LeftInverse g^[n] f^[n]
⊢ LeftInverse (g ∘ g^[n]) (f^[n] ∘ f)
[PROOFSTEP]
exact ihn.comp hg
[GOAL]
α : Type u
β : Type v
f✝ : α → α
m✝ n✝ : ℕ
a : α
f : α → α
m n : ℕ
⊢ f^[n * m] = f^[m * n]
[PROOFSTEP]
rw [Nat.mul_comm]
[GOAL]
α : Type u
β : Type v
f : α → α
m n : ℕ
a : α
hf : Injective f
⊢ f^[m + n] a = f^[n] a ↔ f^[n] (f^[m] a) = f^[n] a
[PROOFSTEP]
rw [← iterate_add_apply, Nat.add_comm]
[GOAL]
α : Type u
β : Type v
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
⊢ f^[m - n] a = a
[PROOFSTEP]
obtain h | h := le_total m n
[GOAL]
case inl
α : Type u
β : Type v
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : m ≤ n
⊢ f^[m - n] a = a
case inr
α : Type u
β : Type v
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m - n] a = a
[PROOFSTEP]
{simp [Nat.sub_eq_zero_of_le h]
}
[GOAL]
case inl
α : Type u
β : Type v
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : m ≤ n
⊢ f^[m - n] a = a
[PROOFSTEP]
simp [Nat.sub_eq_zero_of_le h]
[GOAL]
case inr
α : Type u
β : Type v
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m - n] a = a
[PROOFSTEP]
{exact iterate_cancel_of_add hf (by rwa [Nat.sub_add_cancel h])
}
[GOAL]
case inr
α : Type u
β : Type v
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m - n] a = a
[PROOFSTEP]
exact iterate_cancel_of_add hf (by rwa [Nat.sub_add_cancel h])
[GOAL]
α : Type u
β : Type v
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m - n + ?m.6123] a = f^[?m.6123] a
[PROOFSTEP]
rwa [Nat.sub_add_cancel h]
[GOAL]
α : Type u
β : Type v
f : α → α
a : α
l : List β
⊢ foldl (fun b x => f b) a l = f^[length l] a
[PROOFSTEP]
induction' l with b l H generalizing a
[GOAL]
case nil
α : Type u
β : Type v
f : α → α
a✝ a : α
⊢ foldl (fun b x => f b) a [] = f^[length []] a
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type v
f : α → α
a✝ : α
b : β
l : List β
H : ∀ (a : α), foldl (fun b x => f b) a l = f^[length l] a
a : α
⊢ foldl (fun b x => f b) a (b :: l) = f^[length (b :: l)] a
[PROOFSTEP]
rw [length_cons, foldl, iterate_succ_apply, H]
[GOAL]
α : Type u
β : Type v
f : β → β
b : β
a : α
l : List α
⊢ foldr (fun x => f) b (a :: l) = f^[length (a :: l)] b
[PROOFSTEP]
rw [length_cons, foldr, foldr_const f b l, iterate_succ_apply']
