α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
this : CompleteSpace ↑s
⊢ ∃ y,
    y ∈ s ∧
      IsFixedPt f y ∧
        Tendsto (fun n => (f^[n]) x) atTop (𝓝 y) ∧ ∀ (n : ℕ), edist ((f^[n]) x) y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
⊢ ∃ y,
    y ∈ s ∧
      IsFixedPt f y ∧
        Tendsto (fun n => (f^[n]) x) atTop (𝓝 y) ∧ ∀ (n : ℕ), edist ((f^[n]) x) y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
haveI := hsc.completeSpace_coe
case intro.intro.intro
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n => (MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) y ≤
      edist { val := x, property := hxs } (MapsTo.restrict f s s hsf { val := x, property := hxs }) * ↑K ^ n / (1 - ↑K)
⊢ ∃ y,
    y ∈ s ∧
      IsFixedPt f y ∧
        Tendsto (fun n => (f^[n]) x) atTop (𝓝 y) ∧ ∀ (n : ℕ), edist ((f^[n]) x) y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
this : CompleteSpace ↑s
⊢ ∃ y,
    y ∈ s ∧
      IsFixedPt f y ∧
        Tendsto (fun n => (f^[n]) x) atTop (𝓝 y) ∧ ∀ (n : ℕ), edist ((f^[n]) x) y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
rcases hf.exists_fixedPoint ⟨x, hxs⟩ hx with ⟨y, hfy, h_tendsto, hle⟩
case intro.intro.intro.refine'_1
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n => (MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) y ≤
      edist { val := x, property := hxs } (MapsTo.restrict f s s hsf { val := x, property := hxs }) * ↑K ^ n / (1 - ↑K)
⊢ Tendsto (fun n => (f^[n]) x) atTop (𝓝 ↑y)

case intro.intro.intro.refine'_2
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n => (MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) y ≤
      edist { val := x, property := hxs } (MapsTo.restrict f s s hsf { val := x, property := hxs }) * ↑K ^ n / (1 - ↑K)
n : ℕ
⊢ edist ((f^[n]) x) ↑y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
case intro.intro.intro
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n => (MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) y ≤
      edist { val := x, property := hxs } (MapsTo.restrict f s s hsf { val := x, property := hxs }) * ↑K ^ n / (1 - ↑K)
⊢ ∃ y,
    y ∈ s ∧
      IsFixedPt f y ∧
        Tendsto (fun n => (f^[n]) x) atTop (𝓝 y) ∧ ∀ (n : ℕ), edist ((f^[n]) x) y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
refine' ⟨y, y.2, Subtype.ext_iff_val.1 hfy, _, fun n ↦ _⟩
case h.e'_3.h
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n => (MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) y ≤
      edist { val := x, property := hxs } (MapsTo.restrict f s s hsf { val := x, property := hxs }) * ↑K ^ n / (1 - ↑K)
x✝ : ℕ
⊢ (f^[x✝]) x = (Subtype.val ∘ fun n => (MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) x✝
case intro.intro.intro.refine'_1
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n => (MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) y ≤
      edist { val := x, property := hxs } (MapsTo.restrict f s s hsf { val := x, property := hxs }) * ↑K ^ n / (1 - ↑K)
⊢ Tendsto (fun n => (f^[n]) x) atTop (𝓝 ↑y)
convert (continuous_subtype_val.tendsto _).comp h_tendsto
case h.e'_3
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n => (MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) y ≤
      edist { val := x, property := hxs } (MapsTo.restrict f s s hsf { val := x, property := hxs }) * ↑K ^ n / (1 - ↑K)
n : ℕ
⊢ edist ((f^[n]) x) ↑y = edist ((MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) y
case intro.intro.intro.refine'_2
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n => (MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) y ≤
      edist { val := x, property := hxs } (MapsTo.restrict f s s hsf { val := x, property := hxs }) * ↑K ^ n / (1 - ↑K)
n : ℕ
⊢ edist ((f^[n]) x) ↑y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
convert hle n
case h.e'_3
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n => (MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) y ≤
      edist { val := x, property := hxs } (MapsTo.restrict f s s hsf { val := x, property := hxs }) * ↑K ^ n / (1 - ↑K)
n : ℕ
⊢ edist ((f^[n]) x) ↑y = edist (MapsTo.restrict (f^[n]) s s (_ : MapsTo (f^[n]) s s) { val := x, property := hxs }) y
case h.e'_3
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n => (MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) y ≤
      edist { val := x, property := hxs } (MapsTo.restrict f s s hsf { val := x, property := hxs }) * ↑K ^ n / (1 - ↑K)
n : ℕ
⊢ edist ((f^[n]) x) ↑y = edist ((MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) y
rw [MapsTo.iterate_restrict]
no goals
case h.e'_3
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n => (MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf^[n]) { val := x, property := hxs }) y ≤
      edist { val := x, property := hxs } (MapsTo.restrict f s s hsf { val := x, property := hxs }) * ↑K ^ n / (1 - ↑K)
n : ℕ
⊢ edist ((f^[n]) x) ↑y = edist (MapsTo.restrict (f^[n]) s s (_ : MapsTo (f^[n]) s s) { val := x, property := hxs }) y
rfl