awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.TotallySeparated (goal)
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : IsUltrametricDist X
x y : X
h : x ≠ y
r : ℝ
hr : 0 < r
hr' : r < dist x y
refine_1 : x ∈ ball x r
⊢ ∃ (U : Set X), IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ
have refine_2 : y ∈ (ball x r)ᶜ
Tactic: refine ⟨_, IsUltrametricDist.isClopen_ball x r, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
⊢ Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β))
    (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : (α →ᵤ β) × (α →ᵤ β) | edist p.1 p.2 < ε})
have suffices : Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β))
  (comap (β := ℝ≥0∞) (fun (x : (α →ᵤ β) × (α →ᵤ β)) ↦ edist x.1 x.2) (𝓝 0))
Tactic: suffices 𝓤 (α →ᵤ β) = comap (fun x ↦ edist x.1 x.2) (𝓝 0) by
      simp [this, ENNReal.nhds_zero_basis.comap _ |>.eq_biInf, Set.Iio]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
⊢ Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β))
    (comap (β := ℝ≥0∞) (fun (x : (α →ᵤ β) × (α →ᵤ β)) ↦ edist x.1 x.2) (𝓝 0))
have rw : Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β))
  (⨅ (i : ℝ≥0∞), ⨅ (_ : 0 < i), 𝓟 ((fun (x : (α →ᵤ β) × (α →ᵤ β)) ↦ edist x.1 x.2) ⁻¹' Set.Iic i))
Tactic: rw [ENNReal.nhds_zero_basis_Iic.comap _ |>.eq_biInf]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
⊢ Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β))
    (⨅ (i : ℝ≥0∞), ⨅ (_ : 0 < i), 𝓟 ((fun (x : (α →ᵤ β) × (α →ᵤ β)) ↦ edist x.1 x.2) ⁻¹' Set.Iic i))
have rw : Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β)))
  (⨅ (i : ℝ≥0∞), ⨅ (_ : 0 < i), 𝓟 ((UniformFun.gen α β ∘ fun (ε : ℝ≥0∞) ↦ {p : β × β | edist p.1 p.2 ≤ ε}) i))
  (⨅ (i : ℝ≥0∞), ⨅ (_ : 0 < i), 𝓟 ((fun (x : (α →ᵤ β) × (α →ᵤ β)) ↦ edist x.1 x.2) ⁻¹' Set.Iic i))
Tactic: rw [UniformFun.hasBasis_uniformity_of_basis α β uniformity_basis_edist_le |>.eq_biInf]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
f : α → γ → β
K : ℝ≥0
h : ∀ (c : α), LipschitzWith K (f c)
⊢ UniformEquicontinuous f
have rw : UniformContinuous (β := α →ᵤ β) ((⇑ofFun : (a : α → β) → α →ᵤ β) ∘ Function.swap (φ := fun (a : α) (a_1 : γ) ↦ β) f)
Tactic: rw [uniformEquicontinuous_iff_uniformContinuous]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
f : α → γ → β
K : ℝ≥0
h : ∀ (c : α), LipschitzWith K (f c)
⊢ UniformContinuous (β := α →ᵤ β) ((⇑ofFun : (a : α → β) → α →ᵤ β) ∘ Function.swap (φ := fun (a : α) (a_1 : γ) ↦ β) f)
have h₁ : LipschitzWith (β := α →ᵤ β) K fun (x : γ) ↦ (ofFun : (a : α → β) → α →ᵤ β) fun (c : α) ↦ f c x
Tactic: rw [← lipschitzWith_ofFun_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
f : γ → α →ᵤ β
K : ℝ≥0
s : Set γ
⊢ LipschitzOnWith K f s ↔
    ∀ (c : α), LipschitzOnWith.{u_3, u_2} (β := β) K (fun (x : γ) ↦ (toFun : (a : α →ᵤ β) → α → β) (f x) c) s
have simp : (∀ (c : α),
    LipschitzWith.{u_3, u_2} (β := β) K fun (x : (↑s : Type u_3)) ↦ (toFun : (a : α →ᵤ β) → α → β) (f (↑x : γ)) c) ↔
  ∀ (c : α),
    LipschitzWith.{u_3, u_2} (α := (↑s : Type u_3)) (β := β) K
      (s.restrict (π := fun (a : γ) ↦ β) fun (x : γ) ↦ (toFun : (a : α →ᵤ β) → α → β) (f x) c)
Tactic: simp [lipschitzOnWith_iff_restrict, lipschitzWith_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
f : α → γ → β
K : ℝ≥0
s : Set γ
h : ∀ (c : α), LipschitzOnWith K (f c) s
⊢ UniformEquicontinuousOn f s
have rw : UniformContinuousOn (β := α →ᵤ β) ((⇑ofFun : (a : α → β) → α →ᵤ β) ∘ Function.swap (φ := fun (a : α) (a_1 : γ) ↦ β) f) s
Tactic: rw [uniformEquicontinuousOn_iff_uniformContinuousOn]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
f : α → γ → β
K : ℝ≥0
s : Set γ
h : ∀ (c : α), LipschitzOnWith K (f c) s
⊢ UniformContinuousOn (β := α →ᵤ β) ((⇑ofFun : (a : α → β) → α →ᵤ β) ∘ Function.swap (φ := fun (a : α) (a_1 : γ) ↦ β) f)
    s
have h₁ : LipschitzOnWith (β := α →ᵤ β) K (fun (x : γ) ↦ (ofFun : (a : α → β) → α →ᵤ β) fun (c : α) ↦ f c x) s
Tactic: rw [← lipschitzOnWith_ofFun_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoMetricSpace β
inst_2 : BoundedSpace β
f g : α →ᵤ β
⊢ edist f g =
    ENNReal.ofReal
      ((fun (f g : α →ᵤ β) ↦
          (⨆ (x : α),
              dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β) :
            ℝ))
        f g)
have inl : IsEmpty α →
  edist f g =
    ENNReal.ofReal
      ((fun (f g : α →ᵤ β) ↦
          (⨆ (x : α),
              dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β) :
            ℝ))
        f g)
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoMetricSpace β
inst_2 : BoundedSpace β
f g : α →ᵤ β
inl :
  IsEmpty α →
    edist f g =
      ENNReal.ofReal
        ((fun (f g : α →ᵤ β) ↦
            (⨆ (x : α),
                dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β) :
              ℝ))
          f g)
⊢ edist f g =
    ENNReal.ofReal
      ((fun (f g : α →ᵤ β) ↦
          (⨆ (x : α),
              dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β) :
            ℝ))
        f g)
have inr : Nonempty α →
  edist f g =
    ENNReal.ofReal
      ((fun (f g : α →ᵤ β) ↦
          (⨆ (x : α),
              dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β) :
            ℝ))
        f g)
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoMetricSpace β
inst_2 : BoundedSpace β
f g : α →ᵤ β
h : Nonempty α
⊢ BddAbove (α := ℝ)
    (Set.range fun (x : α) ↦
      dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β))
have h : Membership.mem (γ := Set ℝ)
  (upperBounds
    (Set.range fun (x : α) ↦
      dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β)))
  (Metric.ediam.{u_2} (X := β) Set.univ).toReal
Tactic: use (Metric.ediam (.univ : Set β)).toReal
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoMetricSpace β
inst_2 : BoundedSpace β
f g : α →ᵤ β
h : Nonempty α
⊢ edist f g =
    ENNReal.ofReal
      ((fun (f g : α →ᵤ β) ↦
          (⨆ (x : α),
              dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β) :
            ℝ))
        f g)
have this : BddAbove (α := ℝ)
  (Set.range fun (x : α) ↦
    dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β))
Tactic: have : BddAbove <| .range fun x ↦ dist (toFun f x) (toFun g x) := by
        use (Metric.ediam (.univ : Set β)).toReal
        simp +contextual [mem_upperBounds, eq_comm (a := dist _ _), ← edist_dist,
          ← ENNReal.ofReal_le_iff_le_toReal BoundedSpace.bounded_univ.ediam_ne_top,
          Metric.edist_le_ediam_of_mem]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace β
inst_1 : BoundedSpace β
f g : α →ᵤ β
C : ℝ
hC : 0 ≤ C
⊢ dist f g ≤ C ↔
    ∀ (x : α), dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β) ≤ C
have simp_rw : (edist f g).toReal ≤ C ↔
  ∀ (x : α),
    (edist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β)).toReal ≤ C
Tactic: simp_rw [dist_edist, ← ENNReal.le_ofReal_iff_toReal_le (edist_ne_top _ _) hC, edist_le]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace β
inst_1 : BoundedSpace β
f g : α →ᵤ β
C : ℝ
hC : 0 ≤ C
simp_rw :
  (edist f g).toReal ≤ C ↔
    ∀ (x : α),
      (edist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β)).toReal ≤
        C
⊢ dist f g ≤ C ↔
    ∀ (x : α), dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β) ≤ C
have simp_rw₁ : edist f g ≤ ENNReal.ofReal C ↔
  ∀ (x : α),
    edist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β) ≤
      ENNReal.ofReal C
Tactic: simp_rw [dist_edist, ← ENNReal.le_ofReal_iff_toReal_le (edist_ne_top _ _) hC, edist_le]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoMetricSpace β
inst_2 : BoundedSpace β
⊢ Bornology.IsBounded (α := α →ᵤ β) Set.univ
have rw : Metric.ediam (X := α →ᵤ β) Set.univ < ∞
Tactic: rw [Metric.isBounded_iff_ediam_ne_top, ← lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoMetricSpace β
inst_2 : BoundedSpace β
⊢ Metric.ediam (X := α →ᵤ β) Set.univ < ∞
have refine : Metric.ediam (X := α →ᵤ β) Set.univ ≤ Metric.ediam.{u_2} (X := β) Set.univ
Tactic: refine lt_of_le_of_lt ?_ <| BoundedSpace.bounded_univ (α := β) |>.ediam_ne_top.lt_top
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoMetricSpace β
inst_2 : BoundedSpace β
⊢ Metric.ediam (X := α →ᵤ β) Set.univ ≤ Metric.ediam.{u_2} (X := β) Set.univ
have simp : ∀ (x y : α →ᵤ β) (x_1 : α),
  edist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) x x_1 : β) ((toFun : (a : α →ᵤ β) → α → β) y x_1 : β) ≤
    Metric.ediam.{u_2} (X := β) Set.univ
Tactic: simp only [Metric.ediam_le_iff, Set.mem_univ, edist_le, forall_const]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
𝔖 : Set (Set α)
inst_1 : PseudoEMetricSpace β
f : γ → α →ᵤ[𝔖] β
K : Set α → ℝ≥0
h : ∀ s ∈ 𝔖, ∀ c ∈ s, LipschitzWith.{u_3, u_2} (β := β) (K s) fun (x : γ) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, topologicalSpace α β 𝔖] f
have rw : ∀ s ∈ 𝔖,
  Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, UniformFun.topologicalSpace (↑s : Type u_1) β]
    (Function.comp (β := (↑s : Type u_1) → β)
      ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
        (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
      (Function.comp (β := α → β) (s.restrict (π := fun (a : α) ↦ β)) ((⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) ∘ f) :
        γ → (↑s : Type u_1) → β))
Tactic: rw [UniformOnFun.continuous_rng_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
𝔖 : Set (Set α)
inst_1 : PseudoEMetricSpace β
f : γ → α →ᵤ[𝔖] β
K : Set α → ℝ≥0
h : ∀ s ∈ 𝔖, ∀ c ∈ s, LipschitzWith.{u_3, u_2} (β := β) (K s) fun (x : γ) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c
⊢ ∀ s ∈ 𝔖,
    Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, UniformFun.topologicalSpace (↑s : Type u_1) β]
      (Function.comp (β := (↑s : Type u_1) → β)
        ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
          (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
        (Function.comp (β := α → β) (s.restrict (π := fun (a : α) ↦ β)) ((⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) ∘ f) :
          γ → (↑s : Type u_1) → β))
have refine : ∀ (s : Set α) (hs : s ∈ 𝔖),
  LipschitzWith (β := UniformFun.{u_1, u_2} (↑s : Type u_1) β) (K s)
    (Function.comp (β := (↑s : Type u_1) → β)
      ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
        (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
      (Function.comp (β := α → β) (s.restrict (π := fun (a : α) ↦ β)) ((⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) ∘ f) :
        γ → (↑s : Type u_1) → β))
Tactic: refine fun s hs ↦ LipschitzWith.continuous (K := K s) ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
𝔖 : Set (Set α)
inst_1 : PseudoEMetricSpace β
f : γ → α →ᵤ[𝔖] β
K : Set α → ℝ≥0
h : ∀ s ∈ 𝔖, ∀ c ∈ s, LipschitzWith.{u_3, u_2} (β := β) (K s) fun (x : γ) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c
s : Set α
hs : s ∈ 𝔖
⊢ LipschitzWith (β := UniformFun.{u_1, u_2} (↑s : Type u_1) β) (K s)
    (Function.comp (β := (↑s : Type u_1) → β)
      ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
        (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
      (Function.comp (β := α → β) (s.restrict (π := fun (a : α) ↦ β)) ((⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) ∘ f) :
        γ → (↑s : Type u_1) → β))
have rw : ∀ (c : (↑s : Type u_1)),
  LipschitzWith.{u_3, u_2} (β := β) (K s) fun (x : γ) ↦
    (UniformFun.toFun : (a : (↑s : Type u_1) →ᵤ β) → (↑s : Type u_1) → β)
      (Function.comp (β := (↑s : Type u_1) → β)
        ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
          (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
        (Function.comp (β := α → β) (s.restrict (π := fun (a : α) ↦ β)) ((⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) ∘ f) :
          γ → (↑s : Type u_1) → β)
        x)
      c
Tactic: rw [UniformFun.lipschitzWith_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst : PseudoEMetricSpace β
inst_1 : Fintype (↑𝔖 : Type u_1)
f g : α →ᵤ[𝔖] β
⊢ edist f g =
    edist (α := (s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β)
      (fun (s : (↑𝔖 : Type u_1)) ↦
        (UniformFun.ofFun : (a : (↑(↑s : Set α) : Type u_1) → β) → (↑(↑s : Set α) : Type u_1) →ᵤ β)
          ((↑s : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f)))
      fun (s : (↑𝔖 : Type u_1)) ↦
      (UniformFun.ofFun : (a : (↑(↑s : Set α) : Type u_1) → β) → (↑(↑s : Set α) : Type u_1) →ᵤ β)
        ((↑s : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g))
have simp_rw : Eq (α := ℝ≥0∞)
  (⨆ (x : Subtype (Membership.mem 𝔖)),
    ⨆ (x_1 : Subtype (Membership.mem (↑x : Set α))),
      edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f (↑x_1 : α) : β)
        ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g (↑x_1 : α) : β))
  (⨆ (b : (↑𝔖 : Type u_1)),
    edist (α := UniformFun.{u_1, u_2} (↑(↑b : Set α) : Type u_1) β)
      ((UniformFun.ofFun : (a : (↑(↑b : Set α) : Type u_1) → β) → (↑(↑b : Set α) : Type u_1) →ᵤ β)
          ((↑b : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f)) :
        UniformFun.{u_1, u_2} (↑(↑b : Set α) : Type u_1) β)
      ((UniformFun.ofFun : (a : (↑(↑b : Set α) : Type u_1) → β) → (↑(↑b : Set α) : Type u_1) →ᵤ β)
          ((↑b : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g)) :
        UniformFun.{u_1, u_2} (↑(↑b : Set α) : Type u_1) β))
Tactic: simp_rw [edist_def', iSup_subtype', edist_pi_def, Finset.sup_univ_eq_iSup]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst_1 : PseudoEMetricSpace β
inst_2 : Finite.{u_1 + 1} (↑𝔖 : Type u_1)
x : Fintype (↑𝔖 : Type u_1) := Fintype.ofFinite (↑𝔖 : Type u_1)
⊢ Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) (𝓤 (α →ᵤ[𝔖] β))
    (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) | edist p.1 p.2 < ε})
have simp_rw : Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
  (comap (β :=
    ((s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β) ×
      ((s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β))
    (fun (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) ↦
      (fun (s : (↑𝔖 : Type u_1)) ↦
        (UniformFun.ofFun : (a : (↑(↑s : Set α) : Type u_1) → β) → (↑(↑s : Set α) : Type u_1) →ᵤ β)
          ((↑s : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.1)),
        fun (s : (↑𝔖 : Type u_1)) ↦
        (UniformFun.ofFun : (a : (↑(↑s : Set α) : Type u_1) → β) → (↑(↑s : Set α) : Type u_1) →ᵤ β)
          ((↑s : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.2))))
    (𝓤 ((s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β)))
  (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) | edist p.1 p.2 < ε})
Tactic: simp_rw [← isUniformInducing_pi_restrict.comap_uniformity,
      PseudoEMetricSpace.uniformity_edist, comap_iInf, comap_principal, edist_eq_pi_restrict,
      Set.preimage_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst_1 : PseudoEMetricSpace β
inst_2 : Finite.{u_1 + 1} (↑𝔖 : Type u_1)
x : Fintype (↑𝔖 : Type u_1) := Fintype.ofFinite (↑𝔖 : Type u_1)
simp_rw :
  Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
    (comap (β :=
      ((s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β) ×
        ((s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β))
      (fun (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) ↦
        (fun (s : (↑𝔖 : Type u_1)) ↦
          (UniformFun.ofFun : (a : (↑(↑s : Set α) : Type u_1) → β) → (↑(↑s : Set α) : Type u_1) →ᵤ β)
            ((↑s : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.1)),
          fun (s : (↑𝔖 : Type u_1)) ↦
          (UniformFun.ofFun : (a : (↑(↑s : Set α) : Type u_1) → β) → (↑(↑s : Set α) : Type u_1) →ᵤ β)
            ((↑s : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.2))))
      (𝓤 ((s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β)))
    (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) | edist p.1 p.2 < ε})
⊢ Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) (𝓤 (α →ᵤ[𝔖] β))
    (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) | edist p.1 p.2 < ε})
have simp_rw₁ : Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
  (comap (β :=
    ((s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β) ×
      ((s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β))
    (fun (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) ↦
      (fun (s : (↑𝔖 : Type u_1)) ↦
        (UniformFun.ofFun : (a : (↑(↑s : Set α) : Type u_1) → β) → (↑(↑s : Set α) : Type u_1) →ᵤ β)
          ((↑s : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.1)),
        fun (s : (↑𝔖 : Type u_1)) ↦
        (UniformFun.ofFun : (a : (↑(↑s : Set α) : Type u_1) → β) → (↑(↑s : Set α) : Type u_1) →ᵤ β)
          ((↑s : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.2))))
    (⨅ (ε : ℝ≥0∞),
      ⨅ (_ : ε > 0),
        𝓟
          {p :
            ((s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β) ×
              ((s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β) |
            edist p.1 p.2 < ε}))
  (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) | edist p.1 p.2 < ε})
Tactic: simp_rw [← isUniformInducing_pi_restrict.comap_uniformity,
      PseudoEMetricSpace.uniformity_edist, comap_iInf, comap_principal, edist_eq_pi_restrict,
      Set.preimage_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
𝔖 : Set (Set α)
inst_1 : PseudoEMetricSpace β
inst_2 : Finite.{u_1 + 1} (↑𝔖 : Type u_1)
f : γ → α →ᵤ[𝔖] β
K : ℝ≥0
⊢ LipschitzWith K f ↔
    ∀ c ∈ ⋃₀ 𝔖, LipschitzWith.{u_3, u_2} (β := β) K fun (x : γ) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c
have simp : (∀ (x y : γ) (x_1 : α),
    ∀ x_2 ∈ 𝔖,
      x_1 ∈ x_2 →
        edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) x_1 : β)
            ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) x_1 : β) ≤
          (↑K : ℝ≥0∞) * edist x y) ↔
  ∀ (c : α),
    ∀ x ∈ 𝔖,
      c ∈ x →
        ∀ (x y : γ),
          edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c : β)
              ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) c : β) ≤
            (↑K : ℝ≥0∞) * edist x y
Tactic: simp [LipschitzWith, edist_le]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
𝔖 : Set (Set α)
inst_1 : PseudoEMetricSpace β
inst_2 : Finite.{u_1 + 1} (↑𝔖 : Type u_1)
f : γ → α →ᵤ[𝔖] β
K : ℝ≥0
⊢ (∀ (x y : γ) (x_1 : α),
      ∀ x_2 ∈ 𝔖,
        x_1 ∈ x_2 →
          edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) x_1 : β)
              ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) x_1 : β) ≤
            (↑K : ℝ≥0∞) * edist x y) ↔
    ∀ (c : α),
      ∀ x ∈ 𝔖,
        c ∈ x →
          ∀ (x y : γ),
            edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c : β)
                ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) c : β) ≤
              (↑K : ℝ≥0∞) * edist x y
have mp : (∀ (x y : γ) (x_1 : α),
    ∀ x_2 ∈ 𝔖,
      x_1 ∈ x_2 →
        edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) x_1 : β)
            ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) x_1 : β) ≤
          (↑K : ℝ≥0∞) * edist x y) →
  ∀ (c : α),
    ∀ x ∈ 𝔖,
      c ∈ x →
        ∀ (x y : γ),
          edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c : β)
              ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) c : β) ≤
            (↑K : ℝ≥0∞) * edist x y
Tactic: tauto