awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
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) ≠ ∞
h : edist x (f x) = edist x (f x) * 1
h₁ h₂ : edist x (f x) = edist x (f x)
⊢ edist x (f x) = edist x (f x) * HPow.hPow (β := ℕ) (↑K : ℝ≥0∞) 0

Tactic:
rw [pow_zero, mul_one]

Premises used: pow_zero, mul_one
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
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) ≠ ∞
⊢ edist x (efixedPoint' f (s := s) hsc hsf hf x hxs hx) < ∞

Tactic:
(hf.edist_efixedPoint_le' hsc hsf hxs hx).trans_lt
    (ENNReal.mul_ne_top hx <| ENNReal.inv_ne_top.2 hf.one_sub_K_ne_zero).lt_top

Premises used: Iff.mpr, ENNReal.inv_ne_top, ContractingWith.edist_efixedPoint_le', ContractingWith.one_sub_K_ne_zero, ENNReal.mul_ne_top, Ne.lt_top, LE.le.trans_lt
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
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 (s := s) hsc hsf hfs x hxs hx = efixedPoint' f (s := t) htc htf hft y hyt hy

Tactic:
(hf.eq_or_edist_eq_top_of_fixedPoints ?_ ?_).elim id fun h' ↦ False.elim (ne_of_lt ?_ h')

Premises used: False.elim, id, ContractingWith.eq_or_edist_eq_top_of_fixedPoints, Or.elim, ne_of_lt
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
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 ≠ ∞
refine_1 : IsFixedPt f (efixedPoint' f (s := s) hsc hsf hfs x hxs hx)
refine_2 : IsFixedPt f (efixedPoint' f (s := t) htc htf hft y hyt hy)
refine_3 :
  ∀ (h' : edist (efixedPoint' f (s := s) hsc hsf hfs x hxs hx) (efixedPoint' f (s := t) htc htf hft y hyt hy) = ∞),
    edist (efixedPoint' f (s := s) hsc hsf hfs x hxs hx) (efixedPoint' f (s := t) htc htf hft y hyt hy) < ∞
⊢ efixedPoint' f (s := s) hsc hsf hfs x hxs hx = efixedPoint' f (s := t) htc htf hft y hyt hy

Tactic:
refine (hf.eq_or_edist_eq_top_of_fixedPoints ?_ ?_).elim id fun h' ↦ False.elim (ne_of_lt ?_ h')

Premises used: False.elim, id, ContractingWith.eq_or_edist_eq_top_of_fixedPoints, Or.elim, ne_of_lt
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
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 ≠ ∞
⊢ IsFixedPt f (efixedPoint' f (s := s) hsc hsf hfs x hxs hx)

Tactic:
apply efixedPoint_isFixedPt'

Premises used: ContractingWith.efixedPoint_isFixedPt'
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
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 ≠ ∞
⊢ IsFixedPt f (efixedPoint' f (s := s) hsc hsf hfs x hxs hx)

Tactic:
try apply efixedPoint_isFixedPt'

Premises used: ContractingWith.efixedPoint_isFixedPt'
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
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 ≠ ∞
⊢ IsFixedPt f (efixedPoint' f (s := t) htc htf hft y hyt hy)

Tactic:
apply efixedPoint_isFixedPt'

Premises used: ContractingWith.efixedPoint_isFixedPt'
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
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 ≠ ∞
⊢ IsFixedPt f (efixedPoint' f (s := t) htc htf hft y hyt hy)

Tactic:
try apply efixedPoint_isFixedPt'

Premises used: ContractingWith.efixedPoint_isFixedPt'
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
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 (s := s) hsc hsf hfs x hxs hx) (efixedPoint' f (s := t) htc htf hft y hyt hy) = ∞
refine_3 :
  (Metric.edistLtTopSetoid : α → α → Prop) (efixedPoint' f (s := s) hsc hsf hfs x hxs hx)
    (efixedPoint' f (s := t) htc htf hft y hyt hy)
⊢ edist (efixedPoint' f (s := s) hsc hsf hfs x hxs hx) (efixedPoint' f (s := t) htc htf hft y hyt hy) < ∞

Tactic:
change Metric.edistLtTopSetoid _ _

Premises used: Setoid.r
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
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 (s := s) hsc hsf hfs x hxs hx) (efixedPoint' f (s := t) htc htf hft y hyt hy) = ∞
trans : (Metric.edistLtTopSetoid : α → α → Prop) (efixedPoint' f (s := s) hsc hsf hfs x hxs hx) x
trans₁ : (Metric.edistLtTopSetoid : α → α → Prop) x (efixedPoint' f (s := t) htc htf hft y hyt hy)
⊢ (Metric.edistLtTopSetoid : α → α → Prop) (efixedPoint' f (s := s) hsc hsf hfs x hxs hx)
    (efixedPoint' f (s := t) htc htf hft y hyt hy)

Tactic:
trans x
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
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 (s := s) hsc hsf hfs x hxs hx) (efixedPoint' f (s := t) htc htf hft y hyt hy) = ∞
a : (Metric.edistLtTopSetoid : α → α → Prop) x (efixedPoint' f (s := s) hsc hsf hfs x hxs hx)
⊢ (Metric.edistLtTopSetoid : α → α → Prop) (efixedPoint' f (s := s) hsc hsf hfs x hxs hx) x

Tactic:
apply Setoid.symm'

Premises used: Setoid.symm'
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
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 (s := s) hsc hsf hfs x hxs hx) (efixedPoint' f (s := t) htc htf hft y hyt hy) = ∞
⊢ (Metric.edistLtTopSetoid : α → α → Prop) x (efixedPoint' f (s := s) hsc hsf hfs x hxs hx)

Tactic:
apply edist_efixedPoint_lt_top'

Premises used: ContractingWith.edist_efixedPoint_lt_top'
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
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 (s := s) hsc hsf hfs x hxs hx) (efixedPoint' f (s := t) htc htf hft y hyt hy) = ∞
trans : (Metric.edistLtTopSetoid : α → α → Prop) x y
trans₁ : (Metric.edistLtTopSetoid : α → α → Prop) y (efixedPoint' f (s := t) htc htf hft y hyt hy)
⊢ (Metric.edistLtTopSetoid : α → α → Prop) x (efixedPoint' f (s := t) htc htf hft y hyt hy)

Tactic:
trans y
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
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 (s := s) hsc hsf hfs x hxs hx) (efixedPoint' f (s := t) htc htf hft y hyt hy) = ∞
⊢ (Metric.edistLtTopSetoid : α → α → Prop) x y

Tactic:
lt_top_iff_ne_top.2 hxy

Premises used: Iff.mpr, lt_top_iff_ne_top
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
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 (s := s) hsc hsf hfs x hxs hx) (efixedPoint' f (s := t) htc htf hft y hyt hy) = ∞
⊢ (Metric.edistLtTopSetoid : α → α → Prop) x y

Tactic:
exact lt_top_iff_ne_top.2 hxy

Premises used: Iff.mpr, lt_top_iff_ne_top
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
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 (s := s) hsc hsf hfs x hxs hx) (efixedPoint' f (s := t) htc htf hft y hyt hy) = ∞
⊢ (Metric.edistLtTopSetoid : α → α → Prop) y (efixedPoint' f (s := t) htc htf hft y hyt hy)

Tactic:
apply edist_efixedPoint_lt_top'

Premises used: ContractingWith.edist_efixedPoint_lt_top'
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
⊢ 0 < 1 - (↑K : ℝ)

Tactic:
sub_pos.2 hf.1

Premises used: Iff.mpr, sub_pos, And.left
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
⊢ dist (f x) (f y) ≤ (↑K : ℝ) * dist x y

Tactic:
hf.toLipschitzWith.dist_le_mul x y

Premises used: LipschitzWith.dist_le_mul, ContractingWith.toLipschitzWith
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
grw grw₁ : dist x (f x) + dist y (f y) + (↑K : ℝ) * dist x y ≤ dist x (f x) + dist y (f y) + (↑K : ℝ) * dist x y
⊢ dist x (f x) + dist y (f y) + dist (f x) (f y) ≤ dist x (f x) + dist y (f y) + (↑K : ℝ) * dist x y

Tactic:
grw [hf.dist_le_mul]

Premises used: ContractingWith.dist_le_mul
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
this : dist x y ≤ dist x (f x) + dist y (f y) + (↑K : ℝ) * dist x y
rwa : dist x y * (1 - (↑K : ℝ)) ≤ dist x (f x) + dist y (f y)
rwa₁ : (1 - (↑K : ℝ)) * dist x y ≤ dist x (f x) + dist y (f y)
rwa₂ : 1 * dist x y - (↑K : ℝ) * dist x y ≤ dist x (f x) + dist y (f y)
rwa₃ : dist x y - (↑K : ℝ) * dist x y ≤ dist x (f x) + dist y (f y)
rwa₄ rwa₅ rwa₆ rwa₇ : dist x y ≤ dist x (f x) + dist y (f y) + (↑K : ℝ) * dist x y
⊢ dist x y ≤ (dist x (f x) + dist y (f y)) / (1 - (↑K : ℝ))

Tactic:
rwa [le_div_iff₀ hf.one_sub_K_pos, mul_comm, _root_.sub_mul, one_mul, sub_le_iff_le_add]

Premises used: sub_le_iff_le_add, sub_mul, ContractingWith.one_sub_K_pos, mul_comm, le_div_iff₀, one_mul
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
hy : IsFixedPt f y
⊢ dist x y ≤ dist x (f x) / (1 - (↑K : ℝ))

Tactic:
simpa only [hy.eq, dist_self, add_zero] using hf.dist_inequality x y

Premises used: dist_self, ContractingWith.dist_inequality, Function.IsFixedPt.eq, add_zero
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
hx : IsFixedPt f x
hy : IsFixedPt f y
⊢ x = y

Tactic:
(hf.eq_or_edist_eq_top_of_fixedPoints hx hy).resolve_right (edist_ne_top _ _)

Premises used: edist_ne_top, ContractingWith.eq_or_edist_eq_top_of_fixedPoints, Or.resolve_right
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
g : α → α
x y : α
hx : IsFixedPt f x
hy : IsFixedPt g y
C : ℝ
hfg : ∀ (z : α), dist (f z) (g z) ≤ C
rw : dist y (f y) / (1 - (↑K : ℝ)) = dist (f y) y / (1 - (↑K : ℝ))
rw₁ rw₂ : dist (f y) y / (1 - (↑K : ℝ)) = dist (f y) y / (1 - (↑K : ℝ))
⊢ dist y (f y) / (1 - (↑K : ℝ)) = dist (f y) (g y) / (1 - (↑K : ℝ))

Tactic:
rw [hy.eq, dist_comm]

Premises used: dist_comm, Function.IsFixedPt.eq
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst_1 : Nonempty α
inst_2 : CompleteSpace α
⊢ IsFixedPt f (fixedPoint f hf)

Tactic:
hf.efixedPoint_isFixedPt _

Premises used: ContractingWith.fixedPoint, ContractingWith.efixedPoint_isFixedPt
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst_1 : Nonempty α
inst_2 : CompleteSpace α
x : α
hx : IsFixedPt f x
⊢ x = fixedPoint f hf

Tactic:
hf.fixedPoint_unique' hx hf.fixedPoint_isFixedPt

Premises used: ContractingWith.fixedPoint_unique', ContractingWith.fixedPoint_isFixedPt
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst_1 : Nonempty α
inst_2 : CompleteSpace α
x : α
⊢ dist x (fixedPoint f hf) ≤ dist x (f x) / (1 - (↑K : ℝ))

Tactic:
hf.dist_le_of_fixedPoint x hf.fixedPoint_isFixedPt

Premises used: ContractingWith.dist_le_of_fixedPoint, ContractingWith.fixedPoint_isFixedPt
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst_1 : Nonempty α
inst_2 : CompleteSpace α
x : α
n : ℕ
rw : dist (f^[n] x) (fixedPoint f hf) ≤ dist (f^[n] x) ((f ∘ f^[n]) x) / (1 - (↑K : ℝ))
⊢ dist (f^[n] x) (fixedPoint f hf) ≤ dist (f^[n] x) (f^[n + 1] x) / (1 - (↑K : ℝ))

Tactic:
rw [iterate_succ']

Premises used: Function.iterate_succ'
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst_1 : Nonempty α
inst_2 : CompleteSpace α
x : α
n : ℕ
⊢ dist (f^[n] x) (fixedPoint f hf) ≤ dist (f^[n] x) ((f ∘ f^[n]) x) / (1 - (↑K : ℝ))

Tactic:
apply hf.dist_fixedPoint_le

Premises used: ContractingWith.dist_fixedPoint_le
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst_1 : Nonempty α
inst_2 : CompleteSpace α
x : α
n : ℕ
hc : 0 ≤ 1 - (↑K : ℝ)
hab : dist (f^[n] x) (f^[n + 1] x) ≤ dist x (f x) * (↑K : ℝ) ^ n
⊢ dist (f^[n] x) (f^[n + 1] x) / (1 - (↑K : ℝ)) ≤ dist x (f x) * (↑K : ℝ) ^ n / (1 - (↑K : ℝ))

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst_1 : Nonempty α
inst_2 : CompleteSpace α
x : α
n : ℕ
⊢ 0 ≤ 1 - (↑K : ℝ)

Tactic:
hf.one_sub_K_pos.le

Premises used: LT.lt.le, ContractingWith.one_sub_K_pos
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst_1 : Nonempty α
inst_2 : CompleteSpace α
x : α
n : ℕ
⊢ dist (f^[n] x) (f^[n + 1] x) ≤ dist x (f x) * (↑K : ℝ) ^ n

Tactic:
hf.toLipschitzWith.dist_iterate_succ_le_geometric x n

Premises used: LipschitzWith.dist_iterate_succ_le_geometric, ContractingWith.toLipschitzWith
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst_1 : Nonempty α
inst_2 : CompleteSpace α
x : α
n : ℕ
⊢ 0 ≤ 1 - (↑K : ℝ)

Tactic:
exacts [hf.one_sub_K_pos.le, hf.toLipschitzWith.dist_iterate_succ_le_geometric x n]

Premises used: LT.lt.le, LipschitzWith.dist_iterate_succ_le_geometric, ContractingWith.toLipschitzWith, ContractingWith.one_sub_K_pos
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst_1 : Nonempty α
inst_2 : CompleteSpace α
x : α
⊢ Tendsto (fun (n : ℕ) ↦ f^[n] x) atTop (𝓝 (efixedPoint f hf x ⋯))

Tactic:
tendsto_iterate_efixedPoint hf (edist_ne_top x _)

Premises used: ContractingWith.tendsto_iterate_efixedPoint, edist_ne_top
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst_1 : Nonempty α
inst_2 : CompleteSpace α
x : α
h : fixedPoint f hf = efixedPoint f hf x ⋯
⊢ Tendsto (fun (n : ℕ) ↦ f^[n] x) atTop (𝓝 (fixedPoint f hf))

Tactic:
convert! tendsto_iterate_efixedPoint hf (edist_ne_top x _)

Premises used: ContractingWith.tendsto_iterate_efixedPoint, edist_ne_top
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst_1 : Nonempty α
inst_2 : CompleteSpace α
x : α
⊢ fixedPoint f hf = efixedPoint f hf x ⋯

Tactic:
(fixedPoint_unique _ ?_).symm

Premises used: ContractingWith.fixedPoint_unique, Eq.symm
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst_1 : Nonempty α
inst_2 : CompleteSpace α
x : α
h : IsFixedPt f (efixedPoint f hf x ⋯)
⊢ fixedPoint f hf = efixedPoint f hf x ⋯

Tactic:
refine (fixedPoint_unique _ ?_).symm

Premises used: ContractingWith.fixedPoint_unique, Eq.symm
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst_1 : Nonempty α
inst_2 : CompleteSpace α
x : α
⊢ IsFixedPt f (efixedPoint f hf x ⋯)

Tactic:
apply efixedPoint_isFixedPt

Premises used: ContractingWith.efixedPoint_isFixedPt
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst_1 : Nonempty α
inst_2 : CompleteSpace α
g : α → α
hg : ContractingWith K g
C : ℝ
hfg : ∀ (z : α), dist (f z) (g z) ≤ C
⊢ dist (fixedPoint f hf) (fixedPoint g hg) ≤ C / (1 - (↑K : ℝ))

Tactic:
hf.dist_fixedPoint_fixedPoint_of_dist_le' g hf.fixedPoint_isFixedPt hg.fixedPoint_isFixedPt hfg

Premises used: ContractingWith.fixedPoint_isFixedPt, ContractingWith.dist_fixedPoint_fixedPoint_of_dist_le'
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
inst_1 : Nonempty α
inst_2 : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
set :
  let x := fixedPoint f^[n] hf;
  IsFixedPt f x
⊢ IsFixedPt f (fixedPoint f^[n] hf)

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

Premises used: Nat.iterate, ContractingWith.fixedPoint
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
inst_1 : Nonempty α
inst_2 : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
⊢ f^[n] x = x

Tactic:
have hx : f^[n] x = x := hf.fixedPoint_isFixedPt
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
inst_1 : Nonempty α
inst_2 : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
hx : f^[n] x = x
⊢ dist (f^[n] x) (f^[n] (f x)) ≤ (↑K : ℝ) * dist x (f x)

Tactic:
have := hf.toLipschitzWith.dist_le_mul x (f x)
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
inst_1 : Nonempty α
inst_2 : 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)
⊢ dist x (f x) ≤ (↑K : ℝ) * dist x (f x)

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

Premises used: Function.iterate_succ_apply', Function.iterate_succ_apply
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
inst_1 : Nonempty α
inst_2 : 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)
contrapose! : ∀ (this : ¬IsFixedPt f x), (↑K : ℝ) * dist x (f x) < dist x (f x)
⊢ IsFixedPt f x

Tactic:
contrapose! this
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
inst_1 : Nonempty α
inst_2 : 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:
simpa using mul_lt_mul_of_pos_right (NNReal.coe_lt_one.2 hf.left) <| dist_pos.2 (Ne.symm this)

Premises used: Iff.mpr, Ne.symm, NNReal.coe_lt_one, mul_lt_mul_of_pos_right, And.left, dist_pos
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
ε δ : ℝ≥0
s t N N₁ N₂ : Set X
x : X
⊢ ∀ (a : X),
    Membership.mem (γ := SetRel X X)
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => edist x y ≤ (↑ε : ENNReal)}
      (a, a)

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
ε δ : ℝ≥0
s t N N₁ N₂ : Set X
x : X
⊢ ∀ (a b : X),
    Membership.mem (γ := SetRel X X)
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => edist x y ≤ (↑ε : ENNReal)}
        (a, b) →
      Membership.mem (γ := SetRel X X)
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => edist x y ≤ (↑ε : ENNReal)}
        (b, a)

Tactic:
simp [edist_comm]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
N : Set X
⊢ IsCover ε ∅ N

Tactic:
.empty

Premises used: Metric.IsCover, SetRel.IsCover.empty
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
⊢ IsCover ε s ∅ ↔ s = ∅

Tactic:
SetRel.isCover_empty_right

Premises used: Metric.IsCover, SetRel.isCover_empty_right
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s N : Set X
hsN : IsCover ε s N
hs : s.Nonempty
⊢ N.Nonempty

Tactic:
hsN.nonempty hs

Premises used: SetRel.IsCover.nonempty