case refine'_3
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) < ⊤
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
⊢ efixedPoint' f hsc hsf hfs x hxs hx = efixedPoint' f htc htf hft y hyt hy
refine' (hf.eq_or_edist_eq_top_of_fixedPoints _ _).elim id fun h' ↦ False.elim (ne_of_lt _ h')
  <;> try apply efixedPoint_isFixedPt'
case refine'_3
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy)
case refine'_3
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) < ⊤
change edistLtTopSetoid.Rel _ _
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid (efixedPoint' f hsc hsf hfs x hxs hx) x

α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid x (efixedPoint' f htc htf hft y hyt hy)
case refine'_3
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy)
trans x
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid x y

α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid y (efixedPoint' f htc htf hft y hyt hy)
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid x (efixedPoint' f htc htf hft y hyt hy)
trans y
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid y (efixedPoint' f htc htf hft y hyt hy)
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid x y

α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid y (efixedPoint' f htc htf hft y hyt hy)
exact lt_top_iff_ne_top.2 hxy
no goals
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid y (efixedPoint' f htc htf hft y hyt hy)
apply edist_efixedPoint_lt_top'
case refine'_3
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) < ⊤
case refine'_3
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) < ⊤
apply efixedPoint_isFixedPt'
case a
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid x (efixedPoint' f hsc hsf hfs x hxs hx)
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid (efixedPoint' f hsc hsf hfs x hxs hx) x
apply Setoid.symm'
no goals
case a
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid x (efixedPoint' f hsc hsf hfs x hxs hx)
apply edist_efixedPoint_lt_top'