α : 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)
α : 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])
rw [iterate_succ', iterate_succ]
no goals
α : 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)
exact ihn.comp hg