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_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' : β) < ε₂

Tactic:
(hU x').2.2 _ hx' _ (hU x').1 hf

Premises used: And.right, And.left
-- 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' : β) < ε₂

Tactic:
exact (hU x').2.2 _ hx' _ (hU x').1 hf

Premises used: And.right, And.left
-- 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} (α := β) ((g : (a : α) → β) x : β) ((g : (a : α) → β) x' : β) < ε₂

Tactic:
(hU x').2.2 _ hx' _ (hU x').1 hg

Premises used: And.right, And.left
-- 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} (α := β) ((g : (a : α) → β) x : β) ((g : (a : α) → β) x' : β) < ε₂

Tactic:
exact (hU x').2.2 _ hx' _ (hU x').1 hg

Premises used: And.right, And.left
-- 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'
⊢ F ((f : (a : α) → β) x') = F ((g : (a : α) → β) x')

Tactic:
have F_f_g : F (f x') = F (g x') :=
          (congr_arg (fun f : tα → tβ => (f ⟨x', x'tα⟩ : β)) f_eq_g :)
-- 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'
F_f_g : F ((f : (a : α) → β) x') = F ((g : (a : α) → β) x')
⊢ dist.{v} (α := β) ((f : (a : α) → β) x' : β) ((g : (a : α) → β) x' : β) ≤
    dist ((f : (a : α) → β) x') (F ((f : (a : α) → β) x')) + dist ((g : (a : α) → β) x') (F ((f : (a : α) → β) x'))

Tactic:
dist_triangle_right _ _ _

Premises used: dist_triangle_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'
F_f_g : F ((f : (a : α) → β) x') = F ((g : (a : α) → β) x')
rw rw₁ :
  dist ((f : (a : α) → β) x') (F ((g : (a : α) → β) x')) + dist ((g : (a : α) → β) x') (F ((g : (a : α) → β) x')) =
    dist ((f : (a : α) → β) x') (F ((g : (a : α) → β) x')) + dist ((g : (a : α) → β) x') (F ((g : (a : α) → β) x'))
⊢ 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:
rw [F_f_g]
-- 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'
F_f_g : F ((f : (a : α) → β) x') = F ((g : (a : α) → β) x')
⊢ dist ((f : (a : α) → β) x') (F ((f : (a : α) → β) x')) + dist ((g : (a : α) → β) x') (F ((g : (a : α) → β) x')) <
    ε₂ + ε₂

Tactic:
(add_lt_add (hF (f x')).2 (hF (g x')).2)

Premises used: add_lt_add, And.right, DFunLike.coe
-- 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'
F_f_g : F ((f : (a : α) → β) x') = F ((g : (a : α) → β) x')
⊢ ε₂ + ε₂ = ε₁ / 2

Tactic:
add_halves _

Premises used: add_halves
-- 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.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'
F_f_g : F ((f : (a : α) → β) x') = F ((g : (a : α) → β) x')
dist :
  Dist.dist ((f : (a : α) → β) x') (F ((f : (a : α) → β) x')) +
      Dist.dist ((g : (a : α) → β) x') (F ((f : (a : α) → β) x')) =
    Dist.dist ((f : (a : α) → β) x') (F ((f : (a : α) → β) x')) +
      Dist.dist ((g : (a : α) → β) x') (F ((g : (a : α) → β) x'))
⊢ Dist.dist.{v} (α := β) ((f : (a : α) → β) x' : β) ((g : (a : α) → β) x' : β) < ε₁ / 2

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 _

Premises used: add_halves, dist_triangle_right, add_lt_add, And.right, Dist.dist, DFunLike.coe
-- 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'
rw : ε₁ / 2 + ε₁ / 2 = ε₁
rw₁ rw₂ : ε₁ = ε₁
⊢ ε₂ + ε₂ + ε₁ / 2 = ε₁

Tactic:
rw [add_halves, add_halves]

Premises used: add_halves
-- 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.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₁ : ε₂ + ε₂ + ε₁ / 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 : β) ≤
    ε₁

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]

Premises used: dist_triangle4_right, Dist.dist, DFunLike.coe