awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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) (efixedPoint f hf x hx) x
have a : (Metric.edistLtTopSetoid : α → α → Prop) x (efixedPoint f hf x hx)
Tactic: apply Setoid.symm'
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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 y hy)
have trans : (Metric.edistLtTopSetoid : α → α → Prop) x y
Tactic: trans y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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
⊢ (Metric.edistLtTopSetoid : α → α → Prop) x (efixedPoint f hf y hy)
have trans₁ : (Metric.edistLtTopSetoid : α → α → Prop) y (efixedPoint f hf y hy)
Tactic: trans y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (hypothesis)
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) ≠ ∞
⊢ ∃ 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∞))
have this : CompleteSpace.{u_1} (↑s : Type u_1)
Tactic: haveI := hsc.completeSpace_coe
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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,
    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∞))
have 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∞))
Tactic: rcases hf.exists_fixedPoint ⟨x, hxs⟩ hx with ⟨y, hfy, h_tendsto, hle⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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∞))
have refine_1 : Tendsto (fun (n : ℕ) ↦ f^[n] x) atTop (𝓝 (↑y : α))
Tactic: refine ⟨y, y.2, Subtype.ext_iff.1 hfy, ?_, fun n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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 : α))
⊢ ∃ 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∞))
have refine_2 : ∀ (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 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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 (fun (n : ℕ) ↦ f^[n] x) atTop (𝓝 (↑y : α))
have 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
Tactic: convert! (continuous_subtype_val.tendsto _).comp h_tendsto
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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 x (f x) * (↑K : ℝ≥0∞) ^ n / (1 - (↑K : ℝ≥0∞))
have h : edist (f^[n] x) (↑y : α) = edist ((MapsTo.restrict f s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) y
Tactic: convert! hle n
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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 s s hsf)^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) y
have h : edist (f^[n] x) (↑y : α) = edist (MapsTo.restrict f^[n] s s sorry (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxs)) y
Tactic: rw [MapsTo.iterate_restrict]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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) ≤ edist x (f x) / (1 - (↑K : ℝ≥0∞))
have h : edist x (f x) = edist x (f x) * HPow.hPow (β := ℕ) (↑K : ℝ≥0∞) 0
Tactic: convert! hf.apriori_edist_iterate_efixedPoint_le' hsc hsf hxs hx 0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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 (f x) = edist x (f x) * HPow.hPow (β := ℕ) (↑K : ℝ≥0∞) 0
have h : edist x (f x) = edist x (f x) * 1
Tactic: rw [pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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
⊢ edist x (f x) = edist x (f x) * HPow.hPow (β := ℕ) (↑K : ℝ≥0∞) 0
have h₁ : edist x (f x) = edist x (f x)
Tactic: rw [pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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
have refine_1 : IsFixedPt f (efixedPoint' f (s := s) hsc hsf hfs x hxs hx)
Tactic: refine (hf.eq_or_edist_eq_top_of_fixedPoints ?_ ?_).elim id fun h' ↦ False.elim (ne_of_lt ?_ h')
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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)
⊢ efixedPoint' f (s := s) hsc hsf hfs x hxs hx = efixedPoint' f (s := t) htc htf hft y hyt hy
have refine_2 : IsFixedPt f (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')
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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)
⊢ efixedPoint' f (s := s) hsc hsf hfs x hxs hx = efixedPoint' f (s := t) htc htf hft y hyt hy
have 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) < ∞
Tactic: refine (hf.eq_or_edist_eq_top_of_fixedPoints ?_ ?_).elim id fun h' ↦ False.elim (ne_of_lt ?_ h')
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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) = ∞
⊢ edist (efixedPoint' f (s := s) hsc hsf hfs x hxs hx) (efixedPoint' f (s := t) htc htf hft y hyt hy) < ∞
have 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)
Tactic: change Metric.edistLtTopSetoid _ _
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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) (efixedPoint' f (s := s) hsc hsf hfs x hxs hx)
    (efixedPoint' f (s := t) htc htf hft y hyt hy)
have trans : (Metric.edistLtTopSetoid : α → α → Prop) (efixedPoint' f (s := s) hsc hsf hfs x hxs hx) x
Tactic: trans x
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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
⊢ (Metric.edistLtTopSetoid : α → α → Prop) (efixedPoint' f (s := s) hsc hsf hfs x hxs hx)
    (efixedPoint' f (s := t) htc htf hft y hyt hy)
have trans₁ : (Metric.edistLtTopSetoid : α → α → Prop) x (efixedPoint' f (s := t) htc htf hft y hyt hy)
Tactic: trans x
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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) (efixedPoint' f (s := s) hsc hsf hfs x hxs hx) x
have a : (Metric.edistLtTopSetoid : α → α → Prop) x (efixedPoint' f (s := s) hsc hsf hfs x hxs hx)
Tactic: apply Setoid.symm'
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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 := t) htc htf hft y hyt hy)
have trans : (Metric.edistLtTopSetoid : α → α → Prop) x y
Tactic: trans y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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
⊢ (Metric.edistLtTopSetoid : α → α → Prop) x (efixedPoint' f (s := t) htc htf hft y hyt hy)
have trans₁ : (Metric.edistLtTopSetoid : α → α → Prop) y (efixedPoint' f (s := t) htc htf hft y hyt hy)
Tactic: trans y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
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
have 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
Tactic: grw [hf.dist_le_mul]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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
⊢ dist x y ≤ (dist x (f x) + dist y (f y)) / (1 - (↑K : ℝ))
have rwa : dist x y * (1 - (↑K : ℝ)) ≤ dist x (f x) + dist y (f y)
Tactic: rwa [le_div_iff₀ hf.one_sub_K_pos, mul_comm, _root_.sub_mul, one_mul, sub_le_iff_le_add]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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)
⊢ dist x y ≤ (dist x (f x) + dist y (f y)) / (1 - (↑K : ℝ))
have rwa₁ : (1 - (↑K : ℝ)) * dist x y ≤ dist x (f x) + dist y (f y)
Tactic: rwa [le_div_iff₀ hf.one_sub_K_pos, mul_comm, _root_.sub_mul, one_mul, sub_le_iff_le_add]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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)
⊢ dist x y ≤ (dist x (f x) + dist y (f y)) / (1 - (↑K : ℝ))
have rwa₂ : 1 * dist x y - (↑K : ℝ) * dist x y ≤ dist x (f x) + dist y (f y)
Tactic: rwa [le_div_iff₀ hf.one_sub_K_pos, mul_comm, _root_.sub_mul, one_mul, sub_le_iff_le_add]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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)
⊢ dist x y ≤ (dist x (f x) + dist y (f y)) / (1 - (↑K : ℝ))
have rwa₃ : dist x y - (↑K : ℝ) * dist x y ≤ dist x (f x) + dist y (f y)
Tactic: rwa [le_div_iff₀ hf.one_sub_K_pos, mul_comm, _root_.sub_mul, one_mul, sub_le_iff_le_add]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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
⊢ dist y (f y) / (1 - (↑K : ℝ)) = dist (f y) (g y) / (1 - (↑K : ℝ))
have rw : dist y (f y) / (1 - (↑K : ℝ)) = dist (f y) y / (1 - (↑K : ℝ))
Tactic: rw [hy.eq, dist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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 : ℝ))
⊢ dist y (f y) / (1 - (↑K : ℝ)) = dist (f y) (g y) / (1 - (↑K : ℝ))
have rw₁ : dist (f y) y / (1 - (↑K : ℝ)) = dist (f y) y / (1 - (↑K : ℝ))
Tactic: rw [hy.eq, dist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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^[n + 1] x) / (1 - (↑K : ℝ))
have rw : dist (f^[n] x) (fixedPoint f hf) ≤ dist (f^[n] x) ((f ∘ f^[n]) x) / (1 - (↑K : ℝ))
Tactic: rw [iterate_succ']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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) / (1 - (↑K : ℝ)) ≤ dist x (f x) * (↑K : ℝ) ^ n / (1 - (↑K : ℝ))
have hc : 0 ≤ 1 - (↑K : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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 : ℝ)
⊢ dist (f^[n] x) (f^[n + 1] x) / (1 - (↑K : ℝ)) ≤ dist x (f x) * (↑K : ℝ) ^ n / (1 - (↑K : ℝ))
have hab : dist (f^[n] x) (f^[n + 1] x) ≤ dist x (f x) * (↑K : ℝ) ^ n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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 (𝓝 (fixedPoint f hf))
have h : fixedPoint f hf = efixedPoint f hf x sorry
Tactic: convert! tendsto_iterate_efixedPoint hf (edist_ne_top x _)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
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 ⋯
have h : IsFixedPt f (efixedPoint f hf x sorry)
Tactic: refine (fixedPoint_unique _ ?_).symm
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (hypothesis)
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
⊢ IsFixedPt f x
have hx : f^[n] x = x
Tactic: have hx : f^[n] x = x := hf.fixedPoint_isFixedPt
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (hypothesis)
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
⊢ IsFixedPt f x
have this : dist (f^[n] x) (f^[n] (f x)) ≤ (↑K : ℝ) * dist x (f x)
Tactic: have := hf.toLipschitzWith.dist_le_mul x (f x)