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 : β) < ε₂
⊢ ∃ (β_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 obtain : ∀ tα ⊆ univ,
  ∀ (hfin : tα.Finite) (htα : Subset.{u} (α := Set α) univ (⋃ x ∈ tα, U x)),
    ∃ (β_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 ⊆ ⋃ x ∈ tα, U x⟩ :=
    isCompact_univ.elim_finite_subcover_image (fun x _ => (hU x).2.1) fun x _ =>
      mem_biUnion (mem_univ _) (hU x).1
-- 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 : tα.Finite
htα : Subset.{u} (α := Set α) univ (⋃ x ∈ tα, U x)
⊢ ∃ (β_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 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 : α →ᵇ β) < ε
Tactic: rcases hfin.nonempty_fintype with ⟨_⟩
-- 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 : tα.Finite
htα : Subset.{u} (α := Set α) univ (⋃ x ∈ tα, U x)
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 : α →ᵇ β) < ε
have 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 : α →ᵇ β) < ε
Tactic: obtain ⟨tβ : Set β, _, hfin, htβ : univ ⊆ ⋃ y ∈ tβ, ball y ε₂⟩ :=
    @finite_cover_balls_of_compact β _ _ isCompact_univ _ ε₂0
-- 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 ε₂)
⊢ ∃ (β_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 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 : α →ᵇ β) < ε
Tactic: rcases hfin.nonempty_fintype with ⟨_⟩
-- 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)
⊢ ∃ (β_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 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 : α →ᵇ β) < ε
Tactic: choose F hF using fun y => show ∃ z ∈ tβ, dist y z < ε₂ by simpa using htβ (mem_univ y)
-- 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: refine ⟨tα → tβ, by infer_instance, fun f a => ⟨F (f.1 a), (hF (f.1 a)).1⟩, ?_⟩
-- 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))
⊢ dist (↑(Subtype.mk (p := fun (x : α →ᵇ β) ↦ x ∈ A) f hf) : α →ᵇ β)
      (↑(Subtype.mk (p := fun (x : α →ᵇ β) ↦ x ∈ A) g hg) : α →ᵇ β) <
    ε
have 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 : β) ≤
    ε₁
Tactic: refine lt_of_le_of_lt ((dist_le <| le_of_lt ε₁0).2 fun x => ?_) εε₁
-- 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 : α
⊢ 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 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 : β) ≤
    ε₁
Tactic: obtain ⟨x', x'tα, hx'⟩ := mem_iUnion₂.1 (htα (mem_univ x))
-- 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} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) x' : β) +
        dist.{v} (α := β) ((g : (a : α) → β) x : β) ((g : (a : α) → β) x' : β) +
      dist.{v} (α := β) ((f : (a : α) → β) x' : β) ((g : (a : α) → β) x' : β) ≤
    ε₂ + ε₂ + ε₁ / 2
have refine_1 : dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) x' : β) < ε₂
Tactic: refine le_of_lt (add_lt_add (add_lt_add ?_ ?_) ?_)
-- 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'
refine_1 : dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (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' : β) ≤
    ε₂ + ε₂ + ε₁ / 2
have refine_2 : dist.{v} (α := β) ((g : (a : α) → β) x : β) ((g : (a : α) → β) x' : β) < ε₂
Tactic: refine le_of_lt (add_lt_add (add_lt_add ?_ ?_) ?_)
-- 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'
refine_1 : dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) x' : β) < ε₂
refine_2 : dist.{v} (α := β) ((g : (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' : β) ≤
    ε₂ + ε₂ + ε₁ / 2
have refine_3 : dist.{v} (α := β) ((f : (a : α) → β) x' : β) ((g : (a : α) → β) x' : β) < ε₁ / 2
Tactic: refine le_of_lt (add_lt_add (add_lt_add ?_ ?_) ?_)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli (hypothesis)
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' : β) < ε₁ / 2
have F_f_g : 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 :)
-- 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 ((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'))
have 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'))
Tactic: rw [F_f_g]