-- Mathlib/Topology/MetricSpace/Contracting.lean
theorem isFixedPt_fixedPoint_iterate {n : ℕ} (hf : ContractingWith K f^[n]) :
    IsFixedPt f (hf.fixedPoint f^[n])

Proof state:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
hx : f^[n] x = x
⊢ IsFixedPt f x

Tactic:
have := hf.toLipschitzWith.dist_le_mul x (f x)

Result:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
hx : f^[n] x = x
this : dist (f^[n] x) (f^[n] (f x)) ≤ ↑K * dist x (f x)
⊢ IsFixedPt f x

Proof state:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
hx : f^[n] x = x
this : dist x (f x) ≤ ↑K * dist x (f x)
⊢ IsFixedPt f x

Tactic:
revert this

Result:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
hx : f^[n] x = x
⊢ dist x (f x) ≤ ↑K * dist x (f x) → IsFixedPt f x

Proof state:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
hx : f^[n] x = x
this : ¬IsFixedPt f x
⊢ ↑K * dist x (f x) < dist x (f x)

Tactic:
have := dist_pos.2 (Ne.symm this)

Result:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
hx : f^[n] x = x
this✝ : ¬IsFixedPt f x
this : 0 < dist x (f x)
⊢ ↑K * dist x (f x) < dist x (f x)

Proof state:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
⊢ IsFixedPt f (fixedPoint f^[n] hf)

Tactic:
set x := hf.fixedPoint f^[n]

Result:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
⊢ IsFixedPt f x

Proof state:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
hx : f^[n] x = x
⊢ ¬IsFixedPt f x → ↑K * dist x (f x) < dist x (f x)

Tactic:
intro this

Result:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
hx : f^[n] x = x
this : ¬IsFixedPt f x
⊢ ↑K * dist x (f x) < dist x (f x)

Proof state:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
hx : f^[n] x = x
⊢ dist x (f x) ≤ ↑K * dist x (f x) → IsFixedPt f x

Tactic:
contrapose!

Result:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
hx : f^[n] x = x
⊢ ¬IsFixedPt f x → ↑K * dist x (f x) < dist x (f x)

Proof state:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
hx : f^[n] x = x
this : dist (f^[n] x) (f^[n] (f x)) ≤ ↑K * dist x (f x)
⊢ IsFixedPt f x

Tactic:
rw [← iterate_succ_apply, iterate_succ_apply', hx] at this

Result:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
hx : f^[n] x = x
this : dist x (f x) ≤ ↑K * dist x (f x)
⊢ IsFixedPt f x

Proof state:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
⊢ IsFixedPt f x

Tactic:
have hx : f^[n] x = x := hf.fixedPoint_isFixedPt

Result:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
hx : f^[n] x = x
⊢ IsFixedPt f x

Proof state:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
hx : f^[n] x = x
this✝ : ¬IsFixedPt f x
this : 0 < dist x (f x)
⊢ ↑K * dist x (f x) < dist x (f x)

Tactic:
simpa only [NNReal.coe_one, one_mul, NNReal.val_eq_coe] using (mul_lt_mul_right this).mpr hf.left

Result:
no goals