-- Mathlib/Topology/MetricSpace/Contracting.lean
theorem efixedPoint_eq_of_edist_lt_top (hf : ContractingWith K f) {x : α} (hx : edist x (f x) ≠ ∞)
    {y : α} (hy : edist y (f y) ≠ ∞) (h : edist x y ≠ ∞) :
    efixedPoint f hf x hx = efixedPoint f hf y hy

Proof state:
case refine_2
α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
⊢ IsFixedPt f (efixedPoint f hf y hy)

Tactic:
apply efixedPoint_isFixedPt

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤
⊢ edistLtTopSetoid x y

α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤
⊢ edistLtTopSetoid y (efixedPoint f hf y hy)

Tactic:
exacts [lt_top_iff_ne_top.2 h, hf.edist_efixedPoint_lt_top hy]

Result:
no goals

Proof state:
case refine_3
α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤
⊢ edistLtTopSetoid (efixedPoint f hf x hx) (efixedPoint f hf y hy)

Tactic:
trans x

Result:
α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤
⊢ edistLtTopSetoid (efixedPoint f hf x hx) x

α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤
⊢ edistLtTopSetoid x (efixedPoint f hf y hy)

Proof state:
α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
⊢ efixedPoint f hf x hx = efixedPoint f hf y hy

Tactic:
refine (hf.eq_or_edist_eq_top_of_fixedPoints ?_ ?_).elim id fun h' ↦ False.elim (ne_of_lt ?_ h')
  <;> try apply efixedPoint_isFixedPt

Result:
case refine_3
α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤
⊢ edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) < ⊤

Proof state:
case refine_3
α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤
⊢ edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) < ⊤

Tactic:
change edistLtTopSetoid _ _

Result:
case refine_3
α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤
⊢ edistLtTopSetoid (efixedPoint f hf x hx) (efixedPoint f hf y hy)

Proof state:
case a
α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤
⊢ edistLtTopSetoid x (efixedPoint f hf x hx)

Tactic:
exact hf.edist_efixedPoint_lt_top hx

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤
⊢ edistLtTopSetoid x (efixedPoint f hf y hy)

Tactic:
trans y

Result:
α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤
⊢ edistLtTopSetoid x y

α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤
⊢ edistLtTopSetoid y (efixedPoint f hf y hy)

Proof state:
α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤
⊢ edistLtTopSetoid (efixedPoint f hf x hx) x

Tactic:
apply Setoid.symm'

Result:
case a
α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤
⊢ edistLtTopSetoid x (efixedPoint f hf x hx)