case zero
α : Type u_1
β : Type ?u.11434
γ : Type ?u.11437
ι : Sort ?u.11440
ι' : Sort ?u.11443
f✝ : α → β
g : β → γ
f : α → α
⊢ preimage (f^[Nat.zero]) = preimage f^[Nat.zero]

case succ
α : Type u_1
β : Type ?u.11434
γ : Type ?u.11437
ι : Sort ?u.11440
ι' : Sort ?u.11443
f✝ : α → β
g : β → γ
f : α → α
n : ℕ
ih : preimage (f^[n]) = preimage f^[n]
⊢ preimage (f^[Nat.succ n]) = preimage f^[Nat.succ n]
α : Type u_1
β : Type ?u.11434
γ : Type ?u.11437
ι : Sort ?u.11440
ι' : Sort ?u.11443
f✝ : α → β
g : β → γ
f : α → α
n : ℕ
⊢ preimage (f^[n]) = preimage f^[n]
induction' n with n ih
no goals
case succ
α : Type u_1
β : Type ?u.11434
γ : Type ?u.11437
ι : Sort ?u.11440
ι' : Sort ?u.11443
f✝ : α → β
g : β → γ
f : α → α
n : ℕ
ih : preimage (f^[n]) = preimage f^[n]
⊢ preimage (f^[Nat.succ n]) = preimage f^[Nat.succ n]
rw [iterate_succ, iterate_succ', Set.preimage_comp_eq, ih]
no goals
case zero
α : Type u_1
β : Type ?u.11434
γ : Type ?u.11437
ι : Sort ?u.11440
ι' : Sort ?u.11443
f✝ : α → β
g : β → γ
f : α → α
⊢ preimage (f^[Nat.zero]) = preimage f^[Nat.zero]
simp