awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
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 : tα.Finite
htα : Subset.{u} (α := Set α) univ (⋃ x ∈ tα, U x)
rcases :
  ∀ (val : Fintype (↑tα : Type u)),
    ∃ (β_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 : α →ᵇ β) < ε
⊢ ∃ (β_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 : α →ᵇ β) < ε

Tactic:
rcases hfin.nonempty_fintype with ⟨_⟩

Premises used: Set.Finite.nonempty_fintype
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
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 : tα.Finite
htα : Subset.{u} (α := Set α) univ (⋃ x ∈ tα, U x)
val : Fintype (↑tα : Type u)
obtain :
  ∀ tβ ⊆ univ,
    ∀ (hfin : tβ.Finite) (htβ : Subset.{v} (α := Set β) univ (⋃ y ∈ tβ, ball 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 : α →ᵇ β) < ε
⊢ ∃ (β_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 : α →ᵇ β) < ε

Tactic:
obtain ⟨tβ : Set β, _, hfin, htβ : univ ⊆ ⋃ y ∈ tβ, ball y ε₂⟩ :=
    @finite_cover_balls_of_compact β _ _ isCompact_univ _ ε₂0

Premises used: Set.univ, finite_cover_balls_of_compact, isCompact_univ, Set
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
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 ε₂)
rcases :
  ∀ (val : Fintype (↑tβ : Type v)),
    ∃ (β_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 : α →ᵇ β) < ε
⊢ ∃ (β_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 : α →ᵇ β) < ε

Tactic:
rcases hfin.nonempty_fintype with ⟨_⟩

Premises used: Set.Finite.nonempty_fintype
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
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)
y : β
⊢ ∃ z ∈ tβ, dist y z < ε₂

Tactic:
simpa using htβ (mem_univ y)

Premises used: Set.mem_univ
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
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)
choose :
  ∀ (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 : α →ᵇ β) < ε
⊢ ∃ (β_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 : α →ᵇ β) < ε

Tactic:
choose F hF using fun y => show ∃ z ∈ tβ, dist y z < ε₂ by simpa using htβ (mem_univ y)
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
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) < ε₂
⊢ Fintype ((↑tα : Type u) → (↑tβ : Type v))

Tactic:
infer_instance
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
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) < ε₂
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 : α))) ⋯)
          x)
        ((fun (f : (↑A : Type (max u v))) (a : (↑tα : Type u)) ↦
            Subtype.mk (p := fun (x : β) ↦ x ∈ tβ) (F (((↑f : α →ᵇ β) : (a : α) → β) (↑a : α))) ⋯)
          y) →
      dist (↑x : α →ᵇ β) (↑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 : α →ᵇ β) < ε

Tactic:
refine ⟨tα → tβ, by infer_instance, fun f a => ⟨F (f.1 a), (hF (f.1 a)).1⟩, ?_⟩
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
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))
⊢ dist (↑(Subtype.mk (p := fun (x : α →ᵇ β) ↦ x ∈ A) f hf) : α →ᵇ β)
      (↑(Subtype.mk (p := fun (x : α →ᵇ β) ↦ x ∈ A) g hg) : α →ᵇ β) <
    ε

Tactic:
lt_of_le_of_lt ((dist_le <| le_of_lt ε₁0).2 fun x => ?_) εε₁

Premises used: Iff.mpr, lt_of_le_of_lt, BoundedContinuousFunction.dist_le, le_of_lt
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
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))
refine :
  ∀ (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 : β) ≤
      ε₁
⊢ dist (↑(Subtype.mk (p := fun (x : α →ᵇ β) ↦ x ∈ A) f hf) : α →ᵇ β)
      (↑(Subtype.mk (p := fun (x : α →ᵇ β) ↦ x ∈ A) g hg) : α →ᵇ β) <
    ε

Tactic:
refine lt_of_le_of_lt ((dist_le <| le_of_lt ε₁0).2 fun x => ?_) εε₁

Premises used: Iff.mpr, lt_of_le_of_lt, BoundedContinuousFunction.dist_le, le_of_lt
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
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 : α
obtain :
  ∀ (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 : β) ≤
      ε₁
⊢ dist.{v} (α := β) (((↑(Subtype.mk (p := fun (x : α →ᵇ β) ↦ x ∈ A) f hf) : α →ᵇ β) : (a : α) → β) x : β)
      (((↑(Subtype.mk (p := fun (x : α →ᵇ β) ↦ x ∈ A) g hg) : α →ᵇ β) : (a : α) → β) x : β) ≤
    ε₁

Tactic:
obtain ⟨x', x'tα, hx'⟩ := mem_iUnion₂.1 (htα (mem_univ x))

Premises used: Set.mem_iUnion₂, Iff.mp, Set.mem_univ
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
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} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤
    dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) x' : β) +
        dist.{v} (α := β) ((g : (a : α) → β) x : β) ((g : (a : α) → β) x' : β) +
      dist.{v} (α := β) ((f : (a : α) → β) x' : β) ((g : (a : α) → β) x' : β)

Tactic:
dist_triangle4_right _ _ _ _

Premises used: dist_triangle4_right
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
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} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) x' : β) +
        dist.{v} (α := β) ((g : (a : α) → β) x : β) ((g : (a : α) → β) x' : β) +
      dist.{v} (α := β) ((f : (a : α) → β) x' : β) ((g : (a : α) → β) x' : β) ≤
    ε₂ + ε₂ + ε₁ / 2

Tactic:
le_of_lt (add_lt_add (add_lt_add ?_ ?_) ?_)

Premises used: le_of_lt, add_lt_add
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
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'
refine_1 : dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) x' : β) < ε₂
refine_2 : dist.{v} (α := β) ((g : (a : α) → β) x : β) ((g : (a : α) → β) x' : β) < ε₂
refine_3 : dist.{v} (α := β) ((f : (a : α) → β) x' : β) ((g : (a : α) → β) x' : β) < ε₁ / 2
⊢ 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:
refine le_of_lt (add_lt_add (add_lt_add ?_ ?_) ?_)

Premises used: le_of_lt, add_lt_add