awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α),
    ∀ ε > 0,
      ∃ U ∈ nhds x₀,
        ∀ x ∈ U,
          ∀ x' ∈ U,
            ∀ (i : (↑A : Type (max u v))),
              dist.{v} (α := β) (((↑i : α →ᵇ β) : (a : α) → β) x : β) (((↑i : α →ᵇ β) : (a : α) → β) x' : β) < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : (x : α) → Set α
hU :
  ∀ (x : α),
    x ∈ U x ∧
      IsOpen (U x) ∧
        ∀ y ∈ U x,
          ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist.{v} (α := β) ((f : (a : α) → β) y : β) ((f : (a : α) → β) z : β) < ε₂
tα : Set α
left : tα ⊆ univ
hfin_1 : tα.Finite
htα : Subset.{u} (α := Set α) univ (⋃ x ∈ tα, U x)
val : Fintype (↑tα : Type u)
tβ : Set β
left_1 : tβ ⊆ univ
hfin : tβ.Finite
htβ : Subset.{v} (α := Set β) univ (⋃ y ∈ tβ, ball y ε₂)
val_1 : Fintype (↑tβ : Type v)
F : (y : β) → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ β
hg : g ∈ A
f_eq_g :
  Eq (α := (↑tα : Type u) → (↑tβ : Type v))
    ((fun (f : (↑A : Type (max u v))) (a : (↑tα : Type u)) ↦
        Subtype.mk (p := fun (x : β) ↦ x ∈ tβ) (F (((↑f : α →ᵇ β) : (a : α) → β) (↑a : α))) ⋯)
      (Subtype.mk (p := fun (x : α →ᵇ β) ↦ x ∈ A) f hf))
    ((fun (f : (↑A : Type (max u v))) (a : (↑tα : Type u)) ↦
        Subtype.mk (p := fun (x : β) ↦ x ∈ tβ) (F (((↑f : α →ᵇ β) : (a : α) → β) (↑a : α))) ⋯)
      (Subtype.mk (p := fun (x : α →ᵇ β) ↦ x ∈ A) g hg))
x x' : α
x'tα : x' ∈ tα
hx' : x ∈ U x'
F_f_g : F ((f : (a : α) → β) x') = F ((g : (a : α) → β) x')
⊢ dist.{v} (α := β) ((f : (a : α) → β) x' : β) ((g : (a : α) → β) x' : β) < ε₁ / 2
have dist : dist ((f : (a : α) → β) x') (F ((f : (a : α) → β) x')) + dist ((g : (a : α) → β) x') (F ((f : (a : α) → β) x')) =
  dist ((f : (a : α) → β) x') (F ((f : (a : α) → β) x')) + dist ((g : (a : α) → β) x') (F ((g : (a : α) → β) x'))
Tactic: calc
          dist (f x') (g x') ≤ dist (f x') (F (f x')) + dist (g x') (F (f x')) :=
            dist_triangle_right _ _ _
          _ = dist (f x') (F (f x')) + dist (g x') (F (g x')) := by rw [F_f_g]
          _ < ε₂ + ε₂ := (add_lt_add (hF (f x')).2 (hF (g x')).2)
          _ = ε₁ / 2 := add_halves _
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α),
    ∀ ε > 0,
      ∃ U ∈ nhds x₀,
        ∀ x ∈ U,
          ∀ x' ∈ U,
            ∀ (i : (↑A : Type (max u v))),
              dist.{v} (α := β) (((↑i : α →ᵇ β) : (a : α) → β) x : β) (((↑i : α →ᵇ β) : (a : α) → β) x' : β) < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : (x : α) → Set α
hU :
  ∀ (x : α),
    x ∈ U x ∧
      IsOpen (U x) ∧
        ∀ y ∈ U x,
          ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist.{v} (α := β) ((f : (a : α) → β) y : β) ((f : (a : α) → β) z : β) < ε₂
tα : Set α
left : tα ⊆ univ
hfin_1 : tα.Finite
htα : Subset.{u} (α := Set α) univ (⋃ x ∈ tα, U x)
val : Fintype (↑tα : Type u)
tβ : Set β
left_1 : tβ ⊆ univ
hfin : tβ.Finite
htβ : Subset.{v} (α := Set β) univ (⋃ y ∈ tβ, ball y ε₂)
val_1 : Fintype (↑tβ : Type v)
F : (y : β) → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ β
hg : g ∈ A
f_eq_g :
  Eq (α := (↑tα : Type u) → (↑tβ : Type v))
    ((fun (f : (↑A : Type (max u v))) (a : (↑tα : Type u)) ↦
        Subtype.mk (p := fun (x : β) ↦ x ∈ tβ) (F (((↑f : α →ᵇ β) : (a : α) → β) (↑a : α))) ⋯)
      (Subtype.mk (p := fun (x : α →ᵇ β) ↦ x ∈ A) f hf))
    ((fun (f : (↑A : Type (max u v))) (a : (↑tα : Type u)) ↦
        Subtype.mk (p := fun (x : β) ↦ x ∈ tβ) (F (((↑f : α →ᵇ β) : (a : α) → β) (↑a : α))) ⋯)
      (Subtype.mk (p := fun (x : α →ᵇ β) ↦ x ∈ A) g hg))
x x' : α
x'tα : x' ∈ tα
hx' : x ∈ U x'
⊢ ε₂ + ε₂ + ε₁ / 2 = ε₁
have rw : ε₁ / 2 + ε₁ / 2 = ε₁
Tactic: rw [add_halves, add_halves]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α),
    ∀ ε > 0,
      ∃ U ∈ nhds x₀,
        ∀ x ∈ U,
          ∀ x' ∈ U,
            ∀ (i : (↑A : Type (max u v))),
              dist.{v} (α := β) (((↑i : α →ᵇ β) : (a : α) → β) x : β) (((↑i : α →ᵇ β) : (a : α) → β) x' : β) < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : (x : α) → Set α
hU :
  ∀ (x : α),
    x ∈ U x ∧
      IsOpen (U x) ∧
        ∀ y ∈ U x,
          ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist.{v} (α := β) ((f : (a : α) → β) y : β) ((f : (a : α) → β) z : β) < ε₂
tα : Set α
left : tα ⊆ univ
hfin_1 : tα.Finite
htα : Subset.{u} (α := Set α) univ (⋃ x ∈ tα, U x)
val : Fintype (↑tα : Type u)
tβ : Set β
left_1 : tβ ⊆ univ
hfin : tβ.Finite
htβ : Subset.{v} (α := Set β) univ (⋃ y ∈ tβ, ball y ε₂)
val_1 : Fintype (↑tβ : Type v)
F : (y : β) → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ β
hg : g ∈ A
f_eq_g :
  Eq (α := (↑tα : Type u) → (↑tβ : Type v))
    ((fun (f : (↑A : Type (max u v))) (a : (↑tα : Type u)) ↦
        Subtype.mk (p := fun (x : β) ↦ x ∈ tβ) (F (((↑f : α →ᵇ β) : (a : α) → β) (↑a : α))) ⋯)
      (Subtype.mk (p := fun (x : α →ᵇ β) ↦ x ∈ A) f hf))
    ((fun (f : (↑A : Type (max u v))) (a : (↑tα : Type u)) ↦
        Subtype.mk (p := fun (x : β) ↦ x ∈ tβ) (F (((↑f : α →ᵇ β) : (a : α) → β) (↑a : α))) ⋯)
      (Subtype.mk (p := fun (x : α →ᵇ β) ↦ x ∈ A) g hg))
x x' : α
x'tα : x' ∈ tα
hx' : x ∈ U x'
rw : ε₁ / 2 + ε₁ / 2 = ε₁
⊢ ε₂ + ε₂ + ε₁ / 2 = ε₁
have rw₁ : ε₁ = ε₁
Tactic: rw [add_halves, add_halves]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α),
    ∀ ε > 0,
      ∃ U ∈ nhds x₀,
        ∀ x ∈ U,
          ∀ x' ∈ U,
            ∀ (i : (↑A : Type (max u v))),
              dist.{v} (α := β) (((↑i : α →ᵇ β) : (a : α) → β) x : β) (((↑i : α →ᵇ β) : (a : α) → β) x' : β) < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : (x : α) → Set α
hU :
  ∀ (x : α),
    x ∈ U x ∧
      IsOpen (U x) ∧
        ∀ y ∈ U x,
          ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist.{v} (α := β) ((f : (a : α) → β) y : β) ((f : (a : α) → β) z : β) < ε₂
tα : Set α
left : tα ⊆ univ
hfin_1 : tα.Finite
htα : Subset.{u} (α := Set α) univ (⋃ x ∈ tα, U x)
val : Fintype (↑tα : Type u)
tβ : Set β
left_1 : tβ ⊆ univ
hfin : tβ.Finite
htβ : Subset.{v} (α := Set β) univ (⋃ y ∈ tβ, ball y ε₂)
val_1 : Fintype (↑tβ : Type v)
F : (y : β) → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ β
hg : g ∈ A
f_eq_g :
  Eq (α := (↑tα : Type u) → (↑tβ : Type v))
    ((fun (f : (↑A : Type (max u v))) (a : (↑tα : Type u)) ↦
        Subtype.mk (p := fun (x : β) ↦ x ∈ tβ) (F (((↑f : α →ᵇ β) : (a : α) → β) (↑a : α))) ⋯)
      (Subtype.mk (p := fun (x : α →ᵇ β) ↦ x ∈ A) f hf))
    ((fun (f : (↑A : Type (max u v))) (a : (↑tα : Type u)) ↦
        Subtype.mk (p := fun (x : β) ↦ x ∈ tβ) (F (((↑f : α →ᵇ β) : (a : α) → β) (↑a : α))) ⋯)
      (Subtype.mk (p := fun (x : α →ᵇ β) ↦ x ∈ A) g hg))
x x' : α
x'tα : x' ∈ tα
hx' : x ∈ U x'
⊢ dist.{v} (α := β) (((↑(Subtype.mk (p := fun (x : α →ᵇ β) ↦ x ∈ A) f hf) : α →ᵇ β) : (a : α) → β) x : β)
      (((↑(Subtype.mk (p := fun (x : α →ᵇ β) ↦ x ∈ A) g hg) : α →ᵇ β) : (a : α) → β) x : β) ≤
    ε₁
have dist : dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) x' : β) +
      dist.{v} (α := β) ((g : (a : α) → β) x : β) ((g : (a : α) → β) x' : β) +
    dist.{v} (α := β) ((f : (a : α) → β) x' : β) ((g : (a : α) → β) x' : β) ≤
  ε₂ + ε₂ + ε₁ / 2
Tactic: calc
    dist (f x) (g x) ≤ dist (f x) (f x') + dist (g x) (g x') + dist (f x') (g x') :=
      dist_triangle4_right _ _ _ _
    _ ≤ ε₂ + ε₂ + ε₁ / 2 := by
      refine le_of_lt (add_lt_add (add_lt_add ?_ ?_) ?_)
      · exact (hU x').2.2 _ hx' _ (hU x').1 hf
      · exact (hU x').2.2 _ hx' _ (hU x').1 hg
      · have F_f_g : F (f x') = F (g x') :=
          (congr_arg (fun f : tα → tβ => (f ⟨x', x'tα⟩ : β)) f_eq_g :)
        calc
          dist (f x') (g x') ≤ dist (f x') (F (f x')) + dist (g x') (F (f x')) :=
            dist_triangle_right _ _ _
          _ = dist (f x') (F (f x')) + dist (g x') (F (g x')) := by rw [F_f_g]
          _ < ε₂ + ε₂ := (add_lt_add (hF (f x')).2 (hF (g x')).2)
          _ = ε₁ / 2 := add_halves _
    _ = ε₁ := by rw [add_halves, add_halves]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α),
    ∀ ε > 0,
      ∃ U ∈ nhds x₀,
        ∀ x ∈ U,
          ∀ x' ∈ U,
            ∀ (i : (↑A : Type (max u v))),
              Dist.dist.{v} (α := β) (((↑i : α →ᵇ β) : (a : α) → β) x : β) (((↑i : α →ᵇ β) : (a : α) → β) x' : β) < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : (x : α) → Set α
hU :
  ∀ (x : α),
    x ∈ U x ∧
      IsOpen (U x) ∧
        ∀ y ∈ U x,
          ∀ z ∈ U x,
            ∀ {f : α →ᵇ β}, f ∈ A → Dist.dist.{v} (α := β) ((f : (a : α) → β) y : β) ((f : (a : α) → β) z : β) < ε₂
tα : Set α
left : tα ⊆ univ
hfin_1 : tα.Finite
htα : Subset.{u} (α := Set α) univ (⋃ x ∈ tα, U x)
val : Fintype (↑tα : Type u)
tβ : Set β
left_1 : tβ ⊆ univ
hfin : tβ.Finite
htβ : Subset.{v} (α := Set β) univ (⋃ y ∈ tβ, ball y ε₂)
val_1 : Fintype (↑tβ : Type v)
F : (y : β) → β
hF : ∀ (y : β), F y ∈ tβ ∧ Dist.dist y (F y) < ε₂
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ β
hg : g ∈ A
f_eq_g :
  Eq (α := (↑tα : Type u) → (↑tβ : Type v))
    ((fun (f : (↑A : Type (max u v))) (a : (↑tα : Type u)) ↦
        Subtype.mk (p := fun (x : β) ↦ x ∈ tβ) (F (((↑f : α →ᵇ β) : (a : α) → β) (↑a : α))) ⋯)
      (Subtype.mk (p := fun (x : α →ᵇ β) ↦ x ∈ A) f hf))
    ((fun (f : (↑A : Type (max u v))) (a : (↑tα : Type u)) ↦
        Subtype.mk (p := fun (x : β) ↦ x ∈ tβ) (F (((↑f : α →ᵇ β) : (a : α) → β) (↑a : α))) ⋯)
      (Subtype.mk (p := fun (x : α →ᵇ β) ↦ x ∈ A) g hg))
x x' : α
x'tα : x' ∈ tα
hx' : x ∈ U x'
dist :
  Dist.dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) x' : β) +
        Dist.dist.{v} (α := β) ((g : (a : α) → β) x : β) ((g : (a : α) → β) x' : β) +
      Dist.dist.{v} (α := β) ((f : (a : α) → β) x' : β) ((g : (a : α) → β) x' : β) ≤
    ε₂ + ε₂ + ε₁ / 2
⊢ Dist.dist.{v} (α := β) (((↑(Subtype.mk (p := fun (x : α →ᵇ β) ↦ x ∈ A) f hf) : α →ᵇ β) : (a : α) → β) x : β)
      (((↑(Subtype.mk (p := fun (x : α →ᵇ β) ↦ x ∈ A) g hg) : α →ᵇ β) : (a : α) → β) x : β) ≤
    ε₁
have dist₁ : ε₂ + ε₂ + ε₁ / 2 = ε₁
Tactic: calc
    dist (f x) (g x) ≤ dist (f x) (f x') + dist (g x) (g x') + dist (f x') (g x') :=
      dist_triangle4_right _ _ _ _
    _ ≤ ε₂ + ε₂ + ε₁ / 2 := by
      refine le_of_lt (add_lt_add (add_lt_add ?_ ?_) ?_)
      · exact (hU x').2.2 _ hx' _ (hU x').1 hf
      · exact (hU x').2.2 _ hx' _ (hU x').1 hg
      · have F_f_g : F (f x') = F (g x') :=
          (congr_arg (fun f : tα → tβ => (f ⟨x', x'tα⟩ : β)) f_eq_g :)
        calc
          dist (f x') (g x') ≤ dist (f x') (F (f x')) + dist (g x') (F (f x')) :=
            dist_triangle_right _ _ _
          _ = dist (f x') (F (f x')) + dist (g x') (F (g x')) := by rw [F_f_g]
          _ < ε₂ + ε₂ := (add_lt_add (hF (f x')).2 (hF (g x')).2)
          _ = ε₁ / 2 := add_halves _
    _ = ε₁ := by rw [add_halves, add_halves]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α),
    ∀ ε > 0,
      ∃ U ∈ nhds x₀,
        ∀ x ∈ U,
          ∀ x' ∈ U,
            ∀ (i : (↑A : Type (max u v))),
              dist.{v} (α := β) (((↑i : α →ᵇ β) : (a : α) → β) x : β) (((↑i : α →ᵇ β) : (a : α) → β) x' : β) < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : (x : α) → Set α
hU :
  ∀ (x : α),
    x ∈ U x ∧
      IsOpen (U x) ∧
        ∀ y ∈ U x,
          ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist.{v} (α := β) ((f : (a : α) → β) y : β) ((f : (a : α) → β) z : β) < ε₂
tα : Set α
left : tα ⊆ univ
hfin_1 : tα.Finite
htα : Subset.{u} (α := Set α) univ (⋃ x ∈ tα, U x)
val : Fintype (↑tα : Type u)
tβ : Set β
left_1 : tβ ⊆ univ
hfin : tβ.Finite
htβ : Subset.{v} (α := Set β) univ (⋃ y ∈ tβ, ball y ε₂)
val_1 : Fintype (↑tβ : Type v)
F : (y : β) → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
⊢ ∃ (β_1 : Type (max u v)) (x : Fintype β_1) (F : (↑A : Type (max u v)) → β_1),
    ∀ (x y : (↑A : Type (max u v))), F x = F y → dist (↑x : α →ᵇ β) (↑y : α →ᵇ β) < ε
have refine : ∀ (x y : (↑A : Type (max u v))),
  Eq (α := (↑tα : Type u) → (↑tβ : Type v))
      ((fun (f : (↑A : Type (max u v))) (a : (↑tα : Type u)) ↦
          Subtype.mk (p := fun (x : β) ↦ x ∈ tβ) (F (((↑f : α →ᵇ β) : (a : α) → β) (↑a : α))) sorry)
        x)
      ((fun (f : (↑A : Type (max u v))) (a : (↑tα : Type u)) ↦
          Subtype.mk (p := fun (x : β) ↦ x ∈ tβ) (F (((↑f : α →ᵇ β) : (a : α) → β) (↑a : α))) sorry)
        y) →
    dist (↑x : α →ᵇ β) (↑y : α →ᵇ β) < ε
Tactic: classical
  refine ⟨tα → tβ, by infer_instance, fun f a => ⟨F (f.1 a), (hF (f.1 a)).1⟩, ?_⟩
  rintro ⟨f, hf⟩ ⟨g, hg⟩ f_eq_g
  -- If two functions have the same approximation, then they are within distance `ε`
  refine lt_of_le_of_lt ((dist_le <| le_of_lt ε₁0).2 fun x => ?_) εε₁
  obtain ⟨x', x'tα, hx'⟩ := mem_iUnion₂.1 (htα (mem_univ x))
  calc
    dist (f x) (g x) ≤ dist (f x) (f x') + dist (g x) (g x') + dist (f x') (g x') :=
      dist_triangle4_right _ _ _ _
    _ ≤ ε₂ + ε₂ + ε₁ / 2 := by
      refine le_of_lt (add_lt_add (add_lt_add ?_ ?_) ?_)
      · exact (hU x').2.2 _ hx' _ (hU x').1 hf
      · exact (hU x').2.2 _ hx' _ (hU x').1 hg
      · have F_f_g : F (f x') = F (g x') :=
          (congr_arg (fun f : tα → tβ => (f ⟨x', x'tα⟩ : β)) f_eq_g :)
        calc
          dist (f x') (g x') ≤ dist (f x') (F (f x')) + dist (g x') (F (f x')) :=
            dist_triangle_right _ _ _
          _ = dist (f x') (F (f x')) + dist (g x') (F (g x')) := by rw [F_f_g]
          _ < ε₂ + ε₂ := (add_lt_add (hF (f x')).2 (hF (g x')).2)
          _ = ε₁ / 2 := add_halves _
    _ = ε₁ := by rw [add_halves, add_halves]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli (hypothesis)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
⊢ IsCompact A
have M : LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))
Tactic: have M : LipschitzWith 1 Subtype.val := LipschitzWith.subtype_val s
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
M : LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))
F : BoundedContinuousFunction.{u, v} α (↑s : Type v) → α →ᵇ β := comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M
⊢ IsCompact A
have refine_1 : IsCompact (F ⁻¹' A)
Tactic: refine IsCompact.of_isClosed_subset ((?_ : IsCompact (F ⁻¹' A)).image (continuous_comp M)) closed
      fun f hf => ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
M : LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))
F : BoundedContinuousFunction.{u, v} α (↑s : Type v) → α →ᵇ β := comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M
refine_1 : IsCompact (F ⁻¹' A)
⊢ IsCompact A
have refine_2 : ∀ (f : α →ᵇ β) (hf : f ∈ A),
  Membership.mem (γ := Set (α →ᵇ β)) (comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M '' F ⁻¹' A) f
Tactic: refine IsCompact.of_isClosed_subset ((?_ : IsCompact (F ⁻¹' A)).image (continuous_comp M)) closed
      fun f hf => ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli (hypothesis)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
M : LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))
F : BoundedContinuousFunction.{u, v} α (↑s : Type v) → α →ᵇ β := comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M
⊢ IsCompact (F ⁻¹' A)
have this : CompactSpace.{v} (↑s : Type v)
Tactic: haveI : CompactSpace s := isCompact_iff_compactSpace.1 hs
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
M : LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))
F : BoundedContinuousFunction.{u, v} α (↑s : Type v) → α →ᵇ β := comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M
this : CompactSpace.{v} (↑s : Type v)
⊢ IsCompact (F ⁻¹' A)
have refine_1 : Equicontinuous (X := α) (α := (↑s : Type v)) fun (x : (↑(F ⁻¹' A) : Type (max u v))) ↦
  (⇑(↑x : α →ᵇ (↑s : Type v)) : (a : α) → (↑s : Type v))
Tactic: refine arzela_ascoli₁ _ (continuous_iff_isClosed.1 (continuous_comp M) _ closed) ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
M : LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))
F : BoundedContinuousFunction.{u, v} α (↑s : Type v) → α →ᵇ β := comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M
this : CompactSpace.{v} (↑s : Type v)
⊢ Equicontinuous (X := α) (α := (↑s : Type v)) fun (x : (↑(F ⁻¹' A) : Type (max u v))) ↦
    (⇑(↑x : α →ᵇ (↑s : Type v)) : (a : α) → (↑s : Type v))
have refine_1 : Equicontinuous (ι := (↑(F ⁻¹' A) : Type (max u v))) (X := α) (α := β)
  ((fun (x : α → { x : β // x ∈ s }) ↦ Subtype.val (p := fun (x : β) ↦ x ∈ s) ∘ x) ∘
    fun (x : (↑(F ⁻¹' A) : Type (max u v))) ↦ (⇑(↑x : α →ᵇ (↑s : Type v)) : (a : α) → (↑s : Type v)))
Tactic: rw [isUniformEmbedding_subtype_val.isUniformInducing.equicontinuous_iff]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
M : LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))
F : BoundedContinuousFunction.{u, v} α (↑s : Type v) → α →ᵇ β := comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M
f : α →ᵇ β
hf : f ∈ A
g : BoundedContinuousFunction.{u, v} α (↑s : Type v) := codRestrict s f ⋯
⊢ f = F g
have h : ∀ (x : α), Eq.{v + 1} (α := β) ((f : (a : α) → β) x : β) ((F g : (a : α) → β) x : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
M : LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))
F : BoundedContinuousFunction.{u, v} α (↑s : Type v) → α →ᵇ β := comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M
f : α →ᵇ β
hf_1 : f ∈ A
g : BoundedContinuousFunction.{u, v} α (↑s : Type v) := codRestrict s f ⋯
hf : F g ∈ A
⊢ f = F g
have h : ∀ (x : α), Eq.{v + 1} (α := β) ((f : (a : α) → β) x : β) ((F g : (a : α) → β) x : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
M : LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))
F : BoundedContinuousFunction.{u, v} α (↑s : Type v) → α →ᵇ β := comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M
f : α →ᵇ β
hf : f ∈ A
g : BoundedContinuousFunction.{u, v} α (↑s : Type v) := codRestrict s f ⋯
⊢ Membership.mem (γ := Set (α →ᵇ β)) (comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M '' F ⁻¹' A) f
have refine_2 : ∀ (hf : F g ∈ A), Membership.mem (γ := Set (α →ᵇ β)) (comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M '' F ⁻¹' A) (F g)
Tactic: rw [show f = F g by ext; rfl] at hf ⊢
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f_1 g_1 : α →ᵇ β
x : α
C : ℝ
f g : α →ᵇ β
h : Eq (α := (a : α) → β) ((fun (f : α →ᵇ β) ↦ f.toFun) f) ((fun (f : α →ᵇ β) ↦ f.toFun) g)
⊢ f = g
have obtain : ∀ (toFun : α → β) (continuous_toFun : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] toFun)
  (map_bounded' :
    ∃ (C : ℝ),
      ∀ (x y : α),
        dist ({ toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun x)
            ({ toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun y) ≤
          C)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : α →ᵇ β) ↦ f.toFun)
        { toFun := toFun, continuous_toFun := continuous_toFun, map_bounded' := map_bounded' })
      ((fun (f : α →ᵇ β) ↦ f.toFun) g)),
  { toFun := toFun, continuous_toFun := continuous_toFun, map_bounded' := map_bounded' : α →ᵇ β } = g
Tactic: obtain ⟨⟨_, _⟩, _⟩ := f
Cleared hypotheses: f, h