awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
n : ℕ
⊢ edist (f^[n] x) (efixedPoint f hf x hx) ≤ edist x (f x) * (↑K : ℝ≥0∞) ^ n / (1 - (↑K : ℝ≥0∞))

Tactic:
(Classical.choose_spec <| hf.exists_fixedPoint x hx).2.2 n

Premises used: ContractingWith.efixedPoint, ContractingWith.exists_fixedPoint, Classical.choose_spec, And.right
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
⊢ edist (f^[0] x) (efixedPoint f hf x hx) ≤ edist x (f x) * HPow.hPow (β := ℕ) (↑K : ℝ≥0∞) 0 / (1 - (↑K : ℝ≥0∞))

Tactic:
hf.apriori_edist_iterate_efixedPoint_le hx 0

Premises used: OfNat.ofNat, ContractingWith.apriori_edist_iterate_efixedPoint_le
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
h : edist x (f x) = edist x (f x) * HPow.hPow (β := ℕ) (↑K : ℝ≥0∞) 0
⊢ edist x (efixedPoint f hf x hx) ≤ edist x (f x) / (1 - (↑K : ℝ≥0∞))

Tactic:
convert! hf.apriori_edist_iterate_efixedPoint_le hx 0

Premises used: OfNat.ofNat, ContractingWith.apriori_edist_iterate_efixedPoint_le
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
⊢ edist x (f x) = edist x (f x) * HPow.hPow (β := ℕ) (↑K : ℝ≥0∞) 0

Tactic:
simp only [pow_zero, mul_one]

Premises used: pow_zero, mul_one
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
⊢ edist x (efixedPoint f hf x hx) < ∞

Tactic:
(hf.edist_efixedPoint_le 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.one_sub_K_ne_zero, ENNReal.mul_ne_top, Ne.lt_top, LE.le.trans_lt, ContractingWith.edist_efixedPoint_le
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : 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:
(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 : α → α
inst_1 : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
y : α
hy : edist y (f y) ≠ ∞
h : edist x y ≠ ∞
refine_1 : IsFixedPt f (efixedPoint f hf x hx)
refine_2 : IsFixedPt f (efixedPoint f hf y hy)
refine_3 :
  ∀ (h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ∞),
    edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) < ∞
⊢ 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')

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 : α → α
inst_1 : 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 x hx)

Tactic:
apply efixedPoint_isFixedPt

Premises used: ContractingWith.efixedPoint_isFixedPt
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : 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 x 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 : α → α
inst_1 : 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

Premises used: ContractingWith.efixedPoint_isFixedPt
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : 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:
try apply efixedPoint_isFixedPt

Premises used: ContractingWith.efixedPoint_isFixedPt
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : 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) = ∞
refine_3 : (Metric.edistLtTopSetoid : α → α → Prop) (efixedPoint f hf x hx) (efixedPoint f hf y hy)
⊢ edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) < ∞

Tactic:
change Metric.edistLtTopSetoid _ _

Premises used: Setoid.r
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : 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) = ∞
trans : (Metric.edistLtTopSetoid : α → α → Prop) (efixedPoint f hf x hx) x
trans₁ : (Metric.edistLtTopSetoid : α → α → Prop) x (efixedPoint f hf y hy)
⊢ (Metric.edistLtTopSetoid : α → α → Prop) (efixedPoint f hf x hx) (efixedPoint f hf y hy)

Tactic:
trans x
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : 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) = ∞
a : (Metric.edistLtTopSetoid : α → α → Prop) x (efixedPoint f hf x hx)
⊢ (Metric.edistLtTopSetoid : α → α → Prop) (efixedPoint f hf x hx) x

Tactic:
apply Setoid.symm'

Premises used: Setoid.symm'
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : 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) = ∞
⊢ (Metric.edistLtTopSetoid : α → α → Prop) x (efixedPoint f hf x hx)

Tactic:
hf.edist_efixedPoint_lt_top hx

Premises used: ContractingWith.edist_efixedPoint_lt_top
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : 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) = ∞
⊢ (Metric.edistLtTopSetoid : α → α → Prop) x (efixedPoint f hf x hx)

Tactic:
exact hf.edist_efixedPoint_lt_top hx

Premises used: ContractingWith.edist_efixedPoint_lt_top
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : 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) = ∞
trans : (Metric.edistLtTopSetoid : α → α → Prop) x y
trans₁ : (Metric.edistLtTopSetoid : α → α → Prop) y (efixedPoint f hf y hy)
⊢ (Metric.edistLtTopSetoid : α → α → Prop) x (efixedPoint f hf y hy)

Tactic:
trans y
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : 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) = ∞
⊢ (Metric.edistLtTopSetoid : α → α → Prop) x y

Tactic:
lt_top_iff_ne_top.2 h

Premises used: Iff.mpr, lt_top_iff_ne_top
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : 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) = ∞
⊢ (Metric.edistLtTopSetoid : α → α → Prop) y (efixedPoint f hf y hy)

Tactic:
hf.edist_efixedPoint_lt_top hy

Premises used: ContractingWith.edist_efixedPoint_lt_top
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : 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) = ∞
⊢ (Metric.edistLtTopSetoid : α → α → Prop) x y

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

Premises used: Iff.mpr, lt_top_iff_ne_top, ContractingWith.edist_efixedPoint_lt_top
-- 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) ≠ ∞
⊢ CompleteSpace.{u_1} (↑s : Type u_1)

Tactic:
haveI := hsc.completeSpace_coe
-- 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) ≠ ∞
this : CompleteSpace.{u_1} (↑s : Type u_1)
rcases :
  ∀ (y : (↑s : Type u_1)) (hfy : IsFixedPt (MapsTo.restrict f s s hsf) y)
    (h_tendsto :
      Tendsto (fun (n : ℕ) ↦ (MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) atTop (𝓝 y))
    (hle :
      ∀ (n : ℕ),
        edist ((MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) y ≤
          edist (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)
                (MapsTo.restrict f s s hsf (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) *
              (↑K : ℝ≥0∞) ^ n /
            (1 - (↑K : ℝ≥0∞))),
    ∃ y ∈ s,
      IsFixedPt f y ∧
        Tendsto (fun (n : ℕ) ↦ f^[n] x) atTop (𝓝 y) ∧
          ∀ (n : ℕ), edist (f^[n] x) y ≤ edist x (f x) * (↑K : ℝ≥0∞) ^ n / (1 - (↑K : ℝ≥0∞))
⊢ ∃ y ∈ s,
    IsFixedPt f y ∧
      Tendsto (fun (n : ℕ) ↦ f^[n] x) atTop (𝓝 y) ∧
        ∀ (n : ℕ), edist (f^[n] x) y ≤ edist x (f x) * (↑K : ℝ≥0∞) ^ n / (1 - (↑K : ℝ≥0∞))

Tactic:
rcases hf.exists_fixedPoint ⟨x, hxs⟩ hx with ⟨y, hfy, h_tendsto, hle⟩

Premises used: ContractingWith.exists_fixedPoint, Subtype.mk
-- 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) ≠ ∞
this : CompleteSpace.{u_1} (↑s : Type u_1)
y : (↑s : Type u_1)
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto :
  Tendsto (fun (n : ℕ) ↦ (MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) y ≤
      edist (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)
            (MapsTo.restrict f s s hsf (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) *
          (↑K : ℝ≥0∞) ^ n /
        (1 - (↑K : ℝ≥0∞))
⊢ ∃ y ∈ s,
    IsFixedPt f y ∧
      Tendsto (fun (n : ℕ) ↦ f^[n] x) atTop (𝓝 y) ∧
        ∀ (n : ℕ), edist (f^[n] x) y ≤ edist x (f x) * (↑K : ℝ≥0∞) ^ n / (1 - (↑K : ℝ≥0∞))

Tactic:
⟨y, y.2, Subtype.ext_iff.1 hfy, ?_, fun n ↦ ?_⟩

Premises used: Subtype.ext_iff, And.intro, Exists.intro, Iff.mp, Subtype.val, Subtype.property
-- 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) ≠ ∞
this : CompleteSpace.{u_1} (↑s : Type u_1)
y : (↑s : Type u_1)
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto :
  Tendsto (fun (n : ℕ) ↦ (MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) y ≤
      edist (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)
            (MapsTo.restrict f s s hsf (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) *
          (↑K : ℝ≥0∞) ^ n /
        (1 - (↑K : ℝ≥0∞))
refine_1 : Tendsto (fun (n : ℕ) ↦ f^[n] x) atTop (𝓝 (↑y : α))
refine_2 : ∀ (n : ℕ), edist (f^[n] x) (↑y : α) ≤ edist x (f x) * (↑K : ℝ≥0∞) ^ n / (1 - (↑K : ℝ≥0∞))
⊢ ∃ y ∈ s,
    IsFixedPt f y ∧
      Tendsto (fun (n : ℕ) ↦ f^[n] x) atTop (𝓝 y) ∧
        ∀ (n : ℕ), edist (f^[n] x) y ≤ edist x (f x) * (↑K : ℝ≥0∞) ^ n / (1 - (↑K : ℝ≥0∞))

Tactic:
refine ⟨y, y.2, Subtype.ext_iff.1 hfy, ?_, fun n ↦ ?_⟩
-- 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) ≠ ∞
this : CompleteSpace.{u_1} (↑s : Type u_1)
y : (↑s : Type u_1)
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto :
  Tendsto (fun (n : ℕ) ↦ (MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) y ≤
      edist (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)
            (MapsTo.restrict f s s hsf (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) *
          (↑K : ℝ≥0∞) ^ n /
        (1 - (↑K : ℝ≥0∞))
⊢ Tendsto (α := ℕ)
    (comp (β := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) fun (n : ℕ) ↦
      (MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs))
    atTop (𝓝 (↑y : α))

Tactic:
(continuous_subtype_val.tendsto _).comp h_tendsto

Premises used: continuous_subtype_val, Continuous.tendsto, Filter.Tendsto.comp
-- 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) ≠ ∞
this : CompleteSpace.{u_1} (↑s : Type u_1)
y : (↑s : Type u_1)
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto :
  Tendsto (fun (n : ℕ) ↦ (MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) y ≤
      edist (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)
            (MapsTo.restrict f s s hsf (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) *
          (↑K : ℝ≥0∞) ^ n /
        (1 - (↑K : ℝ≥0∞))
h :
  ∀ (x_1 : ℕ),
    f^[x_1] x =
      comp (β := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (fun (n : ℕ) ↦ (MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) x_1
⊢ Tendsto (fun (n : ℕ) ↦ f^[n] x) atTop (𝓝 (↑y : α))

Tactic:
convert! (continuous_subtype_val.tendsto _).comp h_tendsto

Premises used: continuous_subtype_val, Continuous.tendsto, Filter.Tendsto.comp
-- 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) ≠ ∞
this : CompleteSpace.{u_1} (↑s : Type u_1)
y : (↑s : Type u_1)
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto :
  Tendsto (fun (n : ℕ) ↦ (MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) y ≤
      edist (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)
            (MapsTo.restrict f s s hsf (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) *
          (↑K : ℝ≥0∞) ^ n /
        (1 - (↑K : ℝ≥0∞))
x_1 : ℕ
⊢ f^[x_1] x =
    comp (β := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (fun (n : ℕ) ↦ (MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) x_1

Tactic:
simp only [(· ∘ ·), MapsTo.iterate_restrict, MapsTo.val_restrict_apply]

Premises used: Set.MapsTo.iterate_restrict, Set.MapsTo.val_restrict_apply, Function.comp
-- 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) ≠ ∞
this : CompleteSpace.{u_1} (↑s : Type u_1)
y : (↑s : Type u_1)
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto :
  Tendsto (fun (n : ℕ) ↦ (MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) y ≤
      edist (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)
            (MapsTo.restrict f s s hsf (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) *
          (↑K : ℝ≥0∞) ^ n /
        (1 - (↑K : ℝ≥0∞))
n : ℕ
⊢ edist ((MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) y ≤
    edist (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)
          (MapsTo.restrict f s s hsf (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) *
        (↑K : ℝ≥0∞) ^ n /
      (1 - (↑K : ℝ≥0∞))

Tactic:
hle n
-- 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) ≠ ∞
this : CompleteSpace.{u_1} (↑s : Type u_1)
y : (↑s : Type u_1)
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto :
  Tendsto (fun (n : ℕ) ↦ (MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) y ≤
      edist (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)
            (MapsTo.restrict f s s hsf (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) *
          (↑K : ℝ≥0∞) ^ n /
        (1 - (↑K : ℝ≥0∞))
n : ℕ
h : edist (f^[n] x) (↑y : α) = edist ((MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) y
⊢ edist (f^[n] x) (↑y : α) ≤ edist x (f x) * (↑K : ℝ≥0∞) ^ n / (1 - (↑K : ℝ≥0∞))

Tactic:
convert! hle n
-- 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) ≠ ∞
this : CompleteSpace.{u_1} (↑s : Type u_1)
y : (↑s : Type u_1)
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto :
  Tendsto (fun (n : ℕ) ↦ (MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) y ≤
      edist (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)
            (MapsTo.restrict f s s hsf (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) *
          (↑K : ℝ≥0∞) ^ n /
        (1 - (↑K : ℝ≥0∞))
n : ℕ
h : edist (f^[n] x) (↑y : α) = edist (MapsTo.restrict f^[n] s s ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) y
⊢ edist (f^[n] x) (↑y : α) = edist ((MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) y

Tactic:
rw [MapsTo.iterate_restrict]

Premises used: Set.MapsTo.iterate_restrict
-- 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) ≠ ∞
this : CompleteSpace.{u_1} (↑s : Type u_1)
y : (↑s : Type u_1)
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto :
  Tendsto (fun (n : ℕ) ↦ (MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) y ≤
      edist (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)
            (MapsTo.restrict f s s hsf (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) *
          (↑K : ℝ≥0∞) ^ n /
        (1 - (↑K : ℝ≥0∞))
n : ℕ
⊢ edist (f^[n] x) (↑y : α) = edist (MapsTo.restrict f^[n] s s ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) y

Tactic:
rfl
-- 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) ≠ ∞
⊢ efixedPoint' f (s := s) hsc hsf hf x hxs hx ∈ s

Tactic:
(Classical.choose_spec <| hf.exists_fixedPoint' hsc hsf hxs hx).1

Premises used: ContractingWith.efixedPoint', Set.Mem, Classical.choose_spec, And.left, ContractingWith.exists_fixedPoint'
-- 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) ≠ ∞
⊢ IsFixedPt f (efixedPoint' f (s := s) hsc hsf hf x hxs hx)

Tactic:
(Classical.choose_spec <| hf.exists_fixedPoint' hsc hsf hxs hx).2.1

Premises used: ContractingWith.efixedPoint', Classical.choose_spec, And.right, And.left, ContractingWith.exists_fixedPoint'
-- 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) ≠ ∞
⊢ Tendsto (fun (n : ℕ) ↦ f^[n] x) atTop (𝓝 (efixedPoint' f (s := s) hsc hsf hf x hxs hx))

Tactic:
(Classical.choose_spec <| hf.exists_fixedPoint' hsc hsf hxs hx).2.2.1

Premises used: ContractingWith.efixedPoint', Classical.choose_spec, And.right, And.left, ContractingWith.exists_fixedPoint'
-- 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) ≠ ∞
n : ℕ
⊢ edist (f^[n] x) (efixedPoint' f (s := s) hsc hsf hf x hxs hx) ≤ edist x (f x) * (↑K : ℝ≥0∞) ^ n / (1 - (↑K : ℝ≥0∞))

Tactic:
(Classical.choose_spec <| hf.exists_fixedPoint' hsc hsf hxs hx).2.2.2 n

Premises used: ContractingWith.efixedPoint', Classical.choose_spec, And.right, ContractingWith.exists_fixedPoint'
-- 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 (f^[0] x) (efixedPoint' f (s := s) hsc hsf hf x hxs hx) ≤
    edist x (f x) * HPow.hPow (β := ℕ) (↑K : ℝ≥0∞) 0 / (1 - (↑K : ℝ≥0∞))

Tactic:
hf.apriori_edist_iterate_efixedPoint_le' hsc hsf hxs hx 0

Premises used: ContractingWith.apriori_edist_iterate_efixedPoint_le', OfNat.ofNat
-- 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) * HPow.hPow (β := ℕ) (↑K : ℝ≥0∞) 0
⊢ edist x (efixedPoint' f (s := s) hsc hsf hf x hxs hx) ≤ edist x (f x) / (1 - (↑K : ℝ≥0∞))

Tactic:
convert! hf.apriori_edist_iterate_efixedPoint_le' hsc hsf hxs hx 0

Premises used: ContractingWith.apriori_edist_iterate_efixedPoint_le', OfNat.ofNat