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))

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))
α : 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))
induction' n with n ihn generalizing k
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)
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))
rw [Nat.zero_add]
no goals
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)
exact id_left
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)))
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))
rw [Nat.succ_eq_add_one, Nat.add_right_comm, Nat.add_assoc]
no goals
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)))
exact (H k).comp_left (ihn (k + 1))