awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
δ : ℝ
α : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
E : Set α
hE : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E
hδ : 0 ≤ δ
rw :
  Eq.{u_2 + 1} (α := Set α) (⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ)
    (⋃ x ∈ E, closedBall x δ)
⊢ cthickening δ E = ⋃ x ∈ E, closedBall x δ
have rw₁ : Eq.{u_2 + 1} (α := Set α) (⋃ x ∈ E, closedBall x δ) (⋃ x ∈ E, closedBall x δ)
Tactic: rw [cthickening_eq_biUnion_closedBall E hδ, hE.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
⊢ infEDist x s ≤ infEDist x (cthickening δ s) + ENNReal.ofReal δ
have refine : ∀ (r : ℝ≥0∞) (h : infEDist x (cthickening δ s) + ENNReal.ofReal δ < r), infEDist x s < r
Tactic: refine le_of_forall_gt fun r h => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
r : ℝ≥0∞
h : infEDist x (cthickening δ s) + ENNReal.ofReal δ < r
⊢ infEDist x s < r
have h₁ : ∃ (y : α), infEDist y s ≤ ENNReal.ofReal δ ∧ edist x y < r - ENNReal.ofReal δ
Tactic: simp_rw [← lt_tsub_iff_right, infEDist_lt_iff, mem_cthickening_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
r : ℝ≥0∞
h : ∃ (y : α), infEDist y s ≤ ENNReal.ofReal δ ∧ edist x y < r - ENNReal.ofReal δ
⊢ infEDist x s < r
have obtain : ∀ (y : α) (hy : infEDist y s ≤ ENNReal.ofReal δ) (hxy : edist x y < r - ENNReal.ofReal δ), infEDist x s < r
Tactic: obtain ⟨y, hy, hxy⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
⊢ infEDist x (cthickening δ s) + ENNReal.ofReal δ ≤ infEDist x (thickening δ s) + ENNReal.ofReal δ
have bc : thickening δ s ⊆ cthickening δ s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
have inl : ∀ (hε : ε ≤ 0), thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
Tactic: obtain hε | hε := le_total ε 0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
inl : ∀ (hε : ε ≤ 0), thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
have inr : ∀ (hε : 0 ≤ ε), thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
Tactic: obtain hε | hε := le_total ε 0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
have inr : ∀ (hδ : δ ≤ 0), thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
Tactic: obtain hδ | hδ := le_total δ 0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
inr : ∀ (hδ : δ ≤ 0), thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
have inr₁ : ∀ (hδ : 0 ≤ δ), thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
Tactic: obtain hδ | hδ := le_total δ 0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
hδ : 0 ≤ δ
x : α
⊢ x ∈ thickening ε (thickening δ s) → x ∈ thickening (ε + δ) s
have inr : (∃ (z : α), (∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal δ) ∧ edist x z < ENNReal.ofReal ε) →
  ∃ z ∈ s, edist x z < ENNReal.ofReal ε + ENNReal.ofReal δ
Tactic: simp_rw [mem_thickening_iff_exists_edist_lt, ENNReal.ofReal_add hε hδ]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
⊢ thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s
have inl : ∀ (hε : ε ≤ 0), thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s
Tactic: obtain hε | hε := le_total ε 0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
inl : ∀ (hε : ε ≤ 0), thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s
⊢ thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s
have inr : ∀ (hε : 0 ≤ ε), thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s
Tactic: obtain hε | hε := le_total ε 0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x : α
⊢ x ∈ thickening ε (cthickening δ s) → x ∈ thickening (ε + δ) s
have inr : (∃ (z : α), infEDist z s ≤ ENNReal.ofReal δ ∧ edist x z < ENNReal.ofReal ε) →
  infEDist x s < ENNReal.ofReal ε + ENNReal.ofReal δ
Tactic: simp_rw [mem_thickening_iff_exists_edist_lt, mem_cthickening_iff, ← infEDist_lt_iff,
    ENNReal.ofReal_add hε hδ]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε : ℝ
hε : 0 ≤ ε
δ : ℝ
s : Set α
⊢ cthickening ε (thickening δ s) ⊆ cthickening (ε + δ) s
have inl : ∀ (hδ : δ ≤ 0), cthickening ε (thickening δ s) ⊆ cthickening (ε + δ) s
Tactic: obtain hδ | hδ := le_total δ 0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε : ℝ
hε : 0 ≤ ε
δ : ℝ
s : Set α
inl : ∀ (hδ : δ ≤ 0), cthickening ε (thickening δ s) ⊆ cthickening (ε + δ) s
⊢ cthickening ε (thickening δ s) ⊆ cthickening (ε + δ) s
have inr : ∀ (hδ : 0 ≤ δ), cthickening ε (thickening δ s) ⊆ cthickening (ε + δ) s
Tactic: obtain hδ | hδ := le_total δ 0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε : ℝ
hε : 0 ≤ ε
δ : ℝ
s : Set α
hδ : 0 ≤ δ
x : α
⊢ x ∈ cthickening ε (thickening δ s) → x ∈ cthickening (ε + δ) s
have inr : infEDist x (thickening δ s) ≤ ENNReal.ofReal ε → infEDist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ
Tactic: simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε : ℝ
hε : 0 ≤ ε
δ : ℝ
s : Set α
hδ : 0 ≤ δ
x : α
hx : infEDist x (thickening δ s) ≤ ENNReal.ofReal ε
⊢ infEDist x (thickening δ s) + ENNReal.ofReal δ ≤ ENNReal.ofReal ε + ENNReal.ofReal δ
have grw : ENNReal.ofReal ε + ENNReal.ofReal δ ≤ ENNReal.ofReal ε + ENNReal.ofReal δ
Tactic: grw [hx]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
x : α
⊢ x ∈ cthickening ε (cthickening δ s) → x ∈ cthickening (ε + δ) s
have simp_rw : infEDist x (cthickening δ s) ≤ ENNReal.ofReal ε → infEDist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ
Tactic: simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
x : α
hx : infEDist x (cthickening δ s) ≤ ENNReal.ofReal ε
⊢ infEDist x (cthickening δ s) + ENNReal.ofReal δ ≤ ENNReal.ofReal ε + ENNReal.ofReal δ
have grw : ENNReal.ofReal ε + ENNReal.ofReal δ ≤ ENNReal.ofReal ε + ENNReal.ofReal δ
Tactic: grw [hx]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
ε δ : ℝ
⊢ thickening ε (ball x δ) ⊆ ball x (ε + δ)
have rw : Subset (α := Set α) (thickening ε (thickening δ {x})) (thickening (ε + δ) {x})
Tactic: rw [← thickening_singleton, ← thickening_singleton]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u_2
β : Type u_3
inst : PseudoMetricSpace α
l : Filter β
s : Set α
f : β → α
hs₁ : IsCompact s
hs₂ : s.Nonempty
⊢ Tendsto f l (𝓝ˢ s) ↔ ∀ ε > 0, ∀ᶠ (x : β) in l, infDist (f x) s < ε
have rw : (∀ (i : ℝ), 0 < i → ∀ᶠ (x : β) in l, f x ∈ thickening i s) ↔ ∀ ε > 0, ∀ᶠ (x : β) in l, infDist (f x) s < ε
Tactic: rw [(hasBasis_nhdsSet_thickening hs₁).tendsto_right_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u_2
β : Type u_3
inst : PseudoMetricSpace α
l : Filter β
s : Set α
f : β → α
hs₁ : IsCompact s
hs₂ : s.Nonempty
⊢ (∀ (i : ℝ), 0 < i → ∀ᶠ (x : β) in l, f x ∈ thickening i s) ↔ ∀ ε > 0, ∀ᶠ (x : β) in l, infDist (f x) s < ε
have a : ∀ (ε : ℝ) (hε : 0 < ε), (∀ᶠ (x : β) in l, f x ∈ thickening ε s) ↔ ∀ᶠ (x : β) in l, infDist (f x) s < ε
Tactic: congrm (∀ ε hε, ?_)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
s t : Set α
hs : IsCompact s
⊢ t ∈ 𝓝ˢ s ↔ ∃ ε > 0, thickening ε s ⊆ t
have rw : (∃ (i : ℝ), 0 < i ∧ thickening i s ⊆ t) ↔ ∃ ε > 0, thickening ε s ⊆ t
Tactic: rw [(hasBasis_nhdsSet_thickening hs).mem_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
δ : ℝ
hδ : 0 < δ
hs : thickening δ s ⊆ s
⊢ IsClopen s
have hs₁ : thickening δ s = s
Tactic: replace hs : thickening δ s = s := le_antisymm hs (self_subset_thickening hδ s)
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
δ : ℝ
hδ : 0 < δ
hs : thickening δ s = s
⊢ IsClopen s
have refine : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
Tactic: refine ⟨?_, hs ▸ isOpen_thickening⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
δ : ℝ
hδ : 0 < δ
hs : thickening δ s = s
⊢ IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
have rw : ⋂ (δ : ℝ), ⋂ (_ : 0 < δ), thickening δ s ⊆ s
Tactic: rw [← closure_subset_iff_isClosed, closure_eq_iInter_thickening]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
⊢ ∃ ε > 0, ∃ V ∈ 𝓝ˢ K, thickening ε (f '' V) ⊆ U
have he : ∃ ε > 0, ∃ (V : Set α), Membership.mem (γ := Filter α) (𝓝ˢ ∅) V ∧ thickening ε (f '' V) ⊆ U
Tactic: apply hK.induction_on (p := fun K ↦ ∃ ε > 0, ∃ V ∈ 𝓝ˢ K, thickening ε (f '' V) ⊆ U)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
he : ∃ ε > 0, ∃ (V : Set α), Membership.mem (γ := Filter α) (𝓝ˢ ∅) V ∧ thickening ε (f '' V) ⊆ U
⊢ ∃ ε > 0, ∃ V ∈ 𝓝ˢ K, thickening ε (f '' V) ⊆ U
have hmono : ∀ ⦃s t : Set α⦄,
  s ⊆ t → (∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U) → ∃ ε > 0, ∃ V ∈ 𝓝ˢ s, thickening ε (f '' V) ⊆ U
Tactic: apply hK.induction_on (p := fun K ↦ ∃ ε > 0, ∃ V ∈ 𝓝ˢ K, thickening ε (f '' V) ⊆ U)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
he : ∃ ε > 0, ∃ (V : Set α), Membership.mem (γ := Filter α) (𝓝ˢ ∅) V ∧ thickening ε (f '' V) ⊆ U
hmono :
  ∀ ⦃s t : Set α⦄,
    s ⊆ t → (∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U) → ∃ ε > 0, ∃ V ∈ 𝓝ˢ s, thickening ε (f '' V) ⊆ U
⊢ ∃ ε > 0, ∃ V ∈ 𝓝ˢ K, thickening ε (f '' V) ⊆ U
have hunion : ∀ ⦃s t : Set α⦄,
  (∃ ε > 0, ∃ V ∈ 𝓝ˢ s, thickening ε (f '' V) ⊆ U) →
    (∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U) → ∃ ε > 0, ∃ V ∈ 𝓝ˢ (s ∪ t), thickening ε (f '' V) ⊆ U
Tactic: apply hK.induction_on (p := fun K ↦ ∃ ε > 0, ∃ V ∈ 𝓝ˢ K, thickening ε (f '' V) ⊆ U)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
he : ∃ ε > 0, ∃ (V : Set α), Membership.mem (γ := Filter α) (𝓝ˢ ∅) V ∧ thickening ε (f '' V) ⊆ U
hmono :
  ∀ ⦃s t : Set α⦄,
    s ⊆ t → (∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U) → ∃ ε > 0, ∃ V ∈ 𝓝ˢ s, thickening ε (f '' V) ⊆ U
hunion :
  ∀ ⦃s t : Set α⦄,
    (∃ ε > 0, ∃ V ∈ 𝓝ˢ s, thickening ε (f '' V) ⊆ U) →
      (∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U) → ∃ ε > 0, ∃ V ∈ 𝓝ˢ (s ∪ t), thickening ε (f '' V) ⊆ U
⊢ ∃ ε > 0, ∃ V ∈ 𝓝ˢ K, thickening ε (f '' V) ⊆ U
have hnhds : ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U
Tactic: apply hK.induction_on (p := fun K ↦ ∃ ε > 0, ∃ V ∈ 𝓝ˢ K, thickening ε (f '' V) ⊆ U)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
⊢ ∃ ε > 0, ∃ (V : Set α), Membership.mem (γ := Filter α) (𝓝ˢ ∅) V ∧ thickening ε (f '' V) ⊆ U
have w : ℝ
Tactic: use 1, by positivity, ∅, by simp, by simp
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
w : ℝ
⊢ ∃ ε > 0, ∃ (V : Set α), Membership.mem (γ := Filter α) (𝓝ˢ ∅) V ∧ thickening ε (f '' V) ⊆ U
have left : GT.gt (α := ℝ) 1 0
Tactic: use 1, by positivity, ∅, by simp, by simp
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
w : ℝ
left : GT.gt (α := ℝ) 1 0
w₁ : Set α
⊢ ∃ ε > 0, ∃ (V : Set α), Membership.mem (γ := Filter α) (𝓝ˢ ∅) V ∧ thickening ε (f '' V) ⊆ U
have left₁ : Membership.mem (γ := Filter α) (𝓝ˢ ∅) ∅
Tactic: use 1, by positivity, ∅, by simp, by simp
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
w : ℝ
left : GT.gt (α := ℝ) 1 0
w₁ : Set α
left₁ : Membership.mem (γ := Filter α) (𝓝ˢ ∅) ∅
⊢ ∃ ε > 0, ∃ (V : Set α), Membership.mem (γ := Filter α) (𝓝ˢ ∅) V ∧ thickening ε (f '' V) ⊆ U
have right : thickening 1 (f '' ∅) ⊆ U
Tactic: use 1, by positivity, ∅, by simp, by simp
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
s t : Set α
ε₁ : ℝ
hε₁ : ε₁ > 0
V₁ : Set α
hV₁ : V₁ ∈ 𝓝ˢ s
hV₁thickening : thickening ε₁ (f '' V₁) ⊆ U
ε₂ : ℝ
hε₂ : ε₂ > 0
V₂ : Set α
hV₂ : V₂ ∈ 𝓝ˢ t
hV₂thickening : thickening ε₂ (f '' V₂) ⊆ U
⊢ ∃ ε > 0, ∃ V ∈ 𝓝ˢ (s ∪ t), thickening ε (f '' V) ⊆ U
have hunion : thickening (min ε₁ ε₂) (f '' (V₁ ∪ V₂)) ⊆ U
Tactic: refine ⟨min ε₁ ε₂, by positivity, V₁ ∪ V₂, union_mem_nhdsSet hV₁ hV₂, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
s t : Set α
ε₁ : ℝ
hε₁ : ε₁ > 0
V₁ : Set α
hV₁ : V₁ ∈ 𝓝ˢ s
hV₁thickening : thickening ε₁ (f '' V₁) ⊆ U
ε₂ : ℝ
hε₂ : ε₂ > 0
V₂ : Set α
hV₂ : V₂ ∈ 𝓝ˢ t
hV₂thickening : thickening ε₂ (f '' V₂) ⊆ U
⊢ thickening (min ε₁ ε₂) (f '' (V₁ ∪ V₂)) ⊆ U
have hunion : thickening (min ε₁ ε₂) (f '' V₁) ∪ thickening (min ε₁ ε₂) (f '' V₂) ⊆ U
Tactic: rw [image_union, thickening_union]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
s t : Set α
ε₁ : ℝ
hε₁ : ε₁ > 0
V₁ : Set α
hV₁ : V₁ ∈ 𝓝ˢ s
hV₁thickening : thickening ε₁ (f '' V₁) ⊆ U
ε₂ : ℝ
hε₂ : ε₂ > 0
V₂ : Set α
hV₂ : V₂ ∈ 𝓝ˢ t
hV₂thickening : thickening ε₂ (f '' V₂) ⊆ U
⊢ thickening (min ε₁ ε₂) (f '' V₁) ∪ thickening (min ε₁ ε₂) (f '' V₂) ⊆
    thickening ε₁ (f '' V₁) ∪ thickening ε₂ (f '' V₂)
have h₁ : min ε₁ ε₂ ≤ ε₁
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
s t : Set α
ε₁ : ℝ
hε₁ : ε₁ > 0
V₁ : Set α
hV₁ : V₁ ∈ 𝓝ˢ s
hV₁thickening : thickening ε₁ (f '' V₁) ⊆ U
ε₂ : ℝ
hε₂ : ε₂ > 0
V₂ : Set α
hV₂ : V₂ ∈ 𝓝ˢ t
hV₂thickening : thickening ε₂ (f '' V₂) ⊆ U
h₁ : min ε₁ ε₂ ≤ ε₁
⊢ thickening (min ε₁ ε₂) (f '' V₁) ∪ thickening (min ε₁ ε₂) (f '' V₂) ⊆
    thickening ε₁ (f '' V₁) ∪ thickening ε₂ (f '' V₂)
have h₂ : min ε₁ ε₂ ≤ ε₂
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
s t : Set α
ε₁ : ℝ
hε₁ : ε₁ > 0
V₁ : Set α
hV₁ : V₁ ∈ 𝓝ˢ s
hV₁thickening : thickening ε₁ (f '' V₁) ⊆ U
ε₂ : ℝ
hε₂ : ε₂ > 0
V₂ : Set α
hV₂ : V₂ ∈ 𝓝ˢ t
hV₂thickening : thickening ε₂ (f '' V₂) ⊆ U
⊢ thickening (min ε₁ ε₂) (f '' V₁) ∪ thickening (min ε₁ ε₂) (f '' V₂) ⊆ U
have calc : thickening (min ε₁ ε₂) (f '' V₁) ∪ thickening (min ε₁ ε₂) (f '' V₂) ⊆ thickening ε₁ (f '' V₁) ∪ thickening ε₂ (f '' V₂)
Tactic: calc thickening (ε₁ ⊓ ε₂) (f '' V₁) ∪ thickening (ε₁ ⊓ ε₂) (f '' V₂)
      _ ⊆ thickening ε₁ (f '' V₁) ∪ thickening ε₂ (f '' V₂) := by gcongr <;> norm_num
      _ ⊆ U ∪ U := by gcongr
      _ = U := union_self _
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
s t : Set α
ε₁ : ℝ
hε₁ : ε₁ > 0
V₁ : Set α
hV₁ : V₁ ∈ 𝓝ˢ s
hV₁thickening : thickening ε₁ (f '' V₁) ⊆ U
ε₂ : ℝ
hε₂ : ε₂ > 0
V₂ : Set α
hV₂ : V₂ ∈ 𝓝ˢ t
hV₂thickening : thickening ε₂ (f '' V₂) ⊆ U
calc :
  thickening (min ε₁ ε₂) (f '' V₁) ∪ thickening (min ε₁ ε₂) (f '' V₂) ⊆
    thickening ε₁ (f '' V₁) ∪ thickening ε₂ (f '' V₂)
⊢ thickening (min ε₁ ε₂) (f '' V₁) ∪ thickening (min ε₁ ε₂) (f '' V₂) ⊆ U
have calc₁ : thickening ε₁ (f '' V₁) ∪ thickening ε₂ (f '' V₂) ⊆ U ∪ U
Tactic: calc thickening (ε₁ ⊓ ε₂) (f '' V₁) ∪ thickening (ε₁ ⊓ ε₂) (f '' V₂)
      _ ⊆ thickening ε₁ (f '' V₁) ∪ thickening ε₂ (f '' V₂) := by gcongr <;> norm_num
      _ ⊆ U ∪ U := by gcongr
      _ = U := union_self _
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
x : α
hx : x ∈ K
⊢ {f x} ⊆ U
have rw : f x ∈ U
Tactic: rw [singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
x : α
hx : x ∈ K
⊢ ∃ t ∈ 𝓝[K] x, ∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U
have this : {f x} ⊆ U
Tactic: have : {f x} ⊆ U := by rw [singleton_subset_iff]; exact hKU hx
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
x : α
hx : x ∈ K
this : {f x} ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U
have hnhds : ∀ (δ : ℝ) (hδ : 0 < δ) (hthick : thickening δ {f x} ⊆ U), ∃ t ∈ 𝓝[K] x, ∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U
Tactic: obtain ⟨δ, hδ, hthick⟩ := (isCompact_singleton (x := f x)).exists_thickening_subset_open ho this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
x : α
hx : x ∈ K
this : {f x} ⊆ U
δ : ℝ
hδ : 0 < δ
hthick : thickening δ {f x} ⊆ U
V : Set α := f ⁻¹' thickening (δ / 2) {f x}
⊢ V ∈ 𝓝 x
have a : thickening (δ / 2) {f x} ∈ 𝓝 (f x)
Tactic: apply hf x hx
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
x : α
hx : x ∈ K
this : {f x} ⊆ U
δ : ℝ
hδ : 0 < δ
hthick : thickening δ {f x} ⊆ U
V : Set α := f ⁻¹' thickening (δ / 2) {f x}
⊢ thickening (δ / 2) {f x} ∈ 𝓝 (f x)
have a : Membership.mem (γ := Set β) (thickening (δ / 2) {f x}) (f x)
Tactic: apply isOpen_thickening.mem_nhds
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
x : α
hx : x ∈ K
this : {f x} ⊆ U
δ : ℝ
hδ : 0 < δ
hthick : thickening δ {f x} ⊆ U
V : Set α := f ⁻¹' thickening (δ / 2) {f x}
⊢ ∃ t ∈ 𝓝[K] x, ∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U
have this₁ : V ∈ 𝓝 x
Tactic: have : V ∈ 𝓝 x := by
      apply hf x hx
      apply isOpen_thickening.mem_nhds
      exact (self_subset_thickening (by positivity) _) rfl
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
x : α
hx : x ∈ K
this_1 : {f x} ⊆ U
δ : ℝ
hδ : 0 < δ
hthick : thickening δ {f x} ⊆ U
V : Set α := f ⁻¹' thickening (δ / 2) {f x}
this : V ∈ 𝓝 x
⊢ V ∈ 𝓝ˢ (K ∩ interior V)
have rw : K ∩ interior V ⊆ interior V
Tactic: rw [← subset_interior_iff_mem_nhdsSet]