case h
α : Type u_1
β : Type ?u.18768
γ : Type ?u.18771
ι : Sort ?u.18774
π : α → Type ?u.18779
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
f : α → α
s : Set α
h : MapsTo f s s
n : ℕ
x : ↑s
⊢ (restrict f s s h^[n]) x = restrict (f^[n]) s s (_ : MapsTo (f^[n]) s s) x
α : Type u_1
β : Type ?u.18768
γ : Type ?u.18771
ι : Sort ?u.18774
π : α → Type ?u.18779
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
f : α → α
s : Set α
h : MapsTo f s s
n : ℕ
⊢ restrict f s s h^[n] = restrict (f^[n]) s s (_ : MapsTo (f^[n]) s s)
funext x
case h
α : Type u_1
β : Type ?u.18768
γ : Type ?u.18771
ι : Sort ?u.18774
π : α → Type ?u.18779
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
f : α → α
s : Set α
h : MapsTo f s s
n : ℕ
x : ↑s
⊢ ↑((restrict f s s h^[n]) x) = (f^[n]) ↑x
case h
α : Type u_1
β : Type ?u.18768
γ : Type ?u.18771
ι : Sort ?u.18774
π : α → Type ?u.18779
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
f : α → α
s : Set α
h : MapsTo f s s
n : ℕ
x : ↑s
⊢ (restrict f s s h^[n]) x = restrict (f^[n]) s s (_ : MapsTo (f^[n]) s s) x
rw [Subtype.ext_iff, MapsTo.val_restrict_apply]
case h.zero
α : Type u_1
β : Type ?u.18768
γ : Type ?u.18771
ι : Sort ?u.18774
π : α → Type ?u.18779
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
f : α → α
s : Set α
h : MapsTo f s s
x✝ x : ↑s
⊢ ↑((restrict f s s h^[Nat.zero]) x) = (f^[Nat.zero]) ↑x

case h.succ
α : Type u_1
β : Type ?u.18768
γ : Type ?u.18771
ι : Sort ?u.18774
π : α → Type ?u.18779
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
f : α → α
s : Set α
h : MapsTo f s s
x✝ : ↑s
n : ℕ
ihn : ∀ (x : ↑s), ↑((restrict f s s h^[n]) x) = (f^[n]) ↑x
x : ↑s
⊢ ↑((restrict f s s h^[Nat.succ n]) x) = (f^[Nat.succ n]) ↑x
case h
α : Type u_1
β : Type ?u.18768
γ : Type ?u.18771
ι : Sort ?u.18774
π : α → Type ?u.18779
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
f : α → α
s : Set α
h : MapsTo f s s
n : ℕ
x : ↑s
⊢ ↑((restrict f s s h^[n]) x) = (f^[n]) ↑x
induction' n with n ihn generalizing x
no goals
case h.zero
α : Type u_1
β : Type ?u.18768
γ : Type ?u.18771
ι : Sort ?u.18774
π : α → Type ?u.18779
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
f : α → α
s : Set α
h : MapsTo f s s
x✝ x : ↑s
⊢ ↑((restrict f s s h^[Nat.zero]) x) = (f^[Nat.zero]) ↑x
rfl
no goals
case h.succ
α : Type u_1
β : Type ?u.18768
γ : Type ?u.18771
ι : Sort ?u.18774
π : α → Type ?u.18779
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
f : α → α
s : Set α
h : MapsTo f s s
x✝ : ↑s
n : ℕ
ihn : ∀ (x : ↑s), ↑((restrict f s s h^[n]) x) = (f^[n]) ↑x
x : ↑s
⊢ ↑((restrict f s s h^[Nat.succ n]) x) = (f^[Nat.succ n]) ↑x
simp [Nat.iterate, ihn]