awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Thickening
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
⊢ min ε₁ ε₂ > 0

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.Thickening
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
hunion : thickening (min ε₁ ε₂) (f '' (V₁ ∪ V₂)) ⊆ U
⊢ ∃ ε > 0, ∃ V ∈ 𝓝ˢ (s ∪ t), thickening ε (f '' V) ⊆ U

Tactic:
refine ⟨min ε₁ ε₂, by positivity, V₁ ∪ V₂, union_mem_nhdsSet hV₁ hV₂, ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Thickening
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
hunion : thickening (min ε₁ ε₂) (f '' V₁) ∪ thickening (min ε₁ ε₂) (f '' V₂) ⊆ U
⊢ thickening (min ε₁ ε₂) (f '' (V₁ ∪ V₂)) ⊆ U

Tactic:
rw [image_union, thickening_union]

Premises used: Metric.thickening_union, Set.image_union
-- Module: Mathlib.Topology.MetricSpace.Thickening
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 ε₁ ε₂ ≤ ε₁
h₂ : min ε₁ ε₂ ≤ ε₂
⊢ thickening (min ε₁ ε₂) (f '' V₁) ∪ thickening (min ε₁ ε₂) (f '' V₂) ⊆
    thickening ε₁ (f '' V₁) ∪ thickening ε₂ (f '' V₂)

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.Thickening
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
⊢ min ε₁ ε₂ ≤ ε₁

Tactic:
norm_num
-- Module: Mathlib.Topology.MetricSpace.Thickening
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
⊢ min ε₁ ε₂ ≤ ε₂

Tactic:
norm_num
-- Module: Mathlib.Topology.MetricSpace.Thickening
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 ε₁ (f '' V₁) ∪ thickening ε₂ (f '' V₂) ⊆ U ∪ U

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.Thickening
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
⊢ U ∪ U = U

Tactic:
union_self _

Premises used: Set.union_self
-- Module: Mathlib.Topology.MetricSpace.Thickening
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₂)
calc₁ : thickening ε₁ (f '' V₁) ∪ thickening ε₂ (f '' V₂) ⊆ U ∪ U
⊢ thickening (min ε₁ ε₂) (f '' V₁) ∪ thickening (min ε₁ ε₂) (f '' V₂) ⊆ 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 _

Premises used: Metric.thickening, Set.image, Set.union_self, Min.min
-- Module: Mathlib.Topology.MetricSpace.Thickening
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
rw : f x ∈ U
⊢ {f x} ⊆ U

Tactic:
rw [singleton_subset_iff]

Premises used: Set.singleton_subset_iff
-- Module: Mathlib.Topology.MetricSpace.Thickening
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

Tactic:
hKU hx
-- Module: Mathlib.Topology.MetricSpace.Thickening
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

Tactic:
exact hKU hx
-- Module: Mathlib.Topology.MetricSpace.Thickening
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

Tactic:
have : {f x} ⊆ U := by rw [singleton_subset_iff]; exact hKU hx
-- Module: Mathlib.Topology.MetricSpace.Thickening
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
hnhds :
  ∀ (δ : ℝ) (hδ : 0 < δ) (hthick : thickening δ {f x} ⊆ U), ∃ t ∈ 𝓝[K] x, ∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ 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

Premises used: isCompact_singleton, IsCompact.exists_thickening_subset_open
-- Module: Mathlib.Topology.MetricSpace.Thickening
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}
a : thickening (δ / 2) {f x} ∈ 𝓝 (f x)
⊢ V ∈ 𝓝 x

Tactic:
apply hf x hx
-- Module: Mathlib.Topology.MetricSpace.Thickening
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}
a : Membership.mem (γ := Set β) (thickening (δ / 2) {f x}) (f x)
⊢ thickening (δ / 2) {f x} ∈ 𝓝 (f x)

Tactic:
apply isOpen_thickening.mem_nhds

Premises used: Metric.isOpen_thickening, IsOpen.mem_nhds
-- Module: Mathlib.Topology.MetricSpace.Thickening
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}
⊢ 0 < δ / 2

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.Thickening
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}
⊢ Membership.mem (γ := Set β) (thickening (δ / 2) {f x}) (f x)

Tactic:
exact (self_subset_thickening (by positivity) _) rfl

Premises used: Metric.self_subset_thickening, rfl
-- Module: Mathlib.Topology.MetricSpace.Thickening
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

Tactic:
have : V ∈ 𝓝 x := by
      apply hf x hx
      apply isOpen_thickening.mem_nhds
      exact (self_subset_thickening (by positivity) _) rfl
-- Module: Mathlib.Topology.MetricSpace.Thickening
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
⊢ δ / 2 > 0

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.Thickening
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
rw : K ∩ interior V ⊆ interior V
⊢ V ∈ 𝓝ˢ (K ∩ interior V)

Tactic:
rw [← subset_interior_iff_mem_nhdsSet]

Premises used: subset_interior_iff_mem_nhdsSet
-- Module: Mathlib.Topology.MetricSpace.Thickening
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
⊢ K ∩ interior V ⊆ interior V

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Thickening
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
hnhds : thickening (δ / 2) (f '' V) ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U

Tactic:
refine ⟨K ∩ (interior V), inter_mem_nhdsWithin K (interior_mem_nhds.mpr this),
      δ / 2, by positivity, V, by rw [← subset_interior_iff_mem_nhdsSet]; simp, ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Thickening
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
⊢ thickening (δ / 2) (f '' V) ⊆ thickening (δ / 2) (thickening (δ / 2) {f x})

Tactic:
thickening_subset_of_subset _ (image_preimage_subset f _)

Premises used: Set.image_preimage_subset, Metric.thickening_subset_of_subset
-- Module: Mathlib.Topology.MetricSpace.Thickening
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
⊢ Subset (α := Set β) (thickening (δ / 2) (thickening (δ / 2) {f x})) (thickening (δ / 2 + δ / 2) {f x})

Tactic:
thickening_thickening_subset (δ / 2) (δ / 2) {f x}

Premises used: HDiv.hDiv, Singleton.singleton, OfNat.ofNat, Metric.thickening_thickening_subset
-- Module: Mathlib.Topology.MetricSpace.Thickening
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
⊢ thickening (δ / 2 + δ / 2) {f x} ⊆ U

Tactic:
simp [hthick]
-- Module: Mathlib.Topology.MetricSpace.Thickening
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
calc : thickening (δ / 2 + δ / 2) {f x} ⊆ U
⊢ thickening (δ / 2) (f '' V) ⊆ U

Tactic:
calc thickening (δ / 2) (f '' V)
      _ ⊆ thickening (δ / 2) (thickening (δ / 2) {f x}) :=
        thickening_subset_of_subset _ (image_preimage_subset f _)
      _ ⊆ thickening ((δ / 2) + (δ / 2)) ({f x}) :=
        thickening_thickening_subset (δ / 2) (δ / 2) {f x}
      _ ⊆ U := by simp [hthick]

Premises used: HDiv.hDiv, Metric.thickening, HAdd.hAdd, Set.image_preimage_subset, Set.image, Metric.thickening_subset_of_subset, Singleton.singleton, OfNat.ofNat, Metric.thickening_thickening_subset
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y z : X
⊢ dist x z ≤ max (dist x y) (dist y z)

Tactic:
IsUltrametricDist.dist_triangle_max x y z

Premises used: IsUltrametricDist.dist_triangle_max
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y z : X
h : dist x y ≠ dist y z
apply : max (dist x y) (dist y z) ≤ dist x z
⊢ dist x z = max (dist x y) (dist y z)

Tactic:
apply le_antisymm (dist_triangle_max x y z)

Premises used: IsUltrametricDist.dist_triangle_max, le_antisymm
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y z : X
h : dist x y ≠ dist y z
inl : ∀ (h : dist x y < dist y z), max (dist x y) (dist y z) ≤ dist x z
inr : ∀ (h : dist y z < dist x y), max (dist x y) (dist y z) ≤ dist x z
⊢ max (dist x y) (dist y z) ≤ dist x z

Tactic:
rcases h.lt_or_gt with h | h

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y z : X
h_1 : dist x y ≠ dist y z
h : dist x y < dist y z
inl : dist y z ≤ dist x z
⊢ max (dist x y) (dist y z) ≤ dist x z

Tactic:
rw [max_eq_right h.le]

Premises used: LT.lt.le, max_eq_right
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y z : X
h_1 : dist x y ≠ dist y z
h : dist x y < dist y z
inl : ¬dist y z ≤ dist y x
⊢ dist y z ≤ dist x z

Tactic:
apply (le_max_iff.mp <| dist_triangle_max y x z).resolve_left

Premises used: IsUltrametricDist.dist_triangle_max, Or.resolve_left, Iff.mp, le_max_iff
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y z : X
h_1 : dist x y ≠ dist y z
h : dist x y < dist y z
⊢ ¬dist y z ≤ dist y x

Tactic:
simpa only [not_le, dist_comm x y] using h

Premises used: not_le, dist_comm
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y z : X
h_1 : dist x y ≠ dist y z
h : dist y z < dist x y
inr : dist y x ≤ dist z x
⊢ max (dist x y) (dist y z) ≤ dist x z

Tactic:
rw [max_eq_left h.le, dist_comm x y, dist_comm x z]

Premises used: LT.lt.le, dist_comm, max_eq_left
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y z : X
h_1 : dist x y ≠ dist y z
h : dist y z < dist x y
inr : ¬dist y x ≤ dist y z
⊢ dist y x ≤ dist z x

Tactic:
apply (le_max_iff.mp <| dist_triangle_max y z x).resolve_left

Premises used: IsUltrametricDist.dist_triangle_max, Or.resolve_left, Iff.mp, le_max_iff
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y z : X
h_1 : dist x y ≠ dist y z
h : dist y z < dist x y
⊢ ¬dist y x ≤ dist y z

Tactic:
simpa only [not_le, dist_comm x y] using h

Premises used: not_le, dist_comm
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y z : X
r s : ℝ
p : X → Prop
x_1 x_2 x_3 : Subtype p
⊢ dist x_1 x_3 ≤ max (dist x_1 x_2) (dist x_2 x_3)

Tactic:
simpa [Subtype.dist_eq] using dist_triangle_max _ _ _

Premises used: IsUltrametricDist.dist_triangle_max, Subtype.dist_eq
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r : ℝ
h : y ∈ ball x r
h₁ : ∀ (a : X), a ∈ ball x r ↔ a ∈ ball y r
⊢ ball x r = ball y r

Tactic:
ext a
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r : ℝ
h : y ∈ ball x r
a : X
⊢ dist y x < r

Tactic:
simp_rw [mem_ball] at h ⊢

Premises used: Metric.mem_ball
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r : ℝ
a : X
h : dist y x < r
h₁ : dist a x < r → dist a y < r
h₂ : dist a y < r → dist a x < r
⊢ dist a x < r ↔ dist a y < r

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r : ℝ
a : X
h : dist y x < r
h' : dist a x < r
⊢ dist a y < r

Tactic:
(dist_triangle_max _ _ _).trans_lt (max_lt h' (dist_comm x _ ▸ h))

Premises used: IsUltrametricDist.dist_triangle_max, Eq.rec, dist_comm, max_lt, Eq.symm, LE.le.trans_lt
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r : ℝ
a : X
h : dist y x < r
h' : dist a x < r
⊢ dist a y < r

Tactic:
exact (dist_triangle_max _ _ _).trans_lt (max_lt h' (dist_comm x _ ▸ h))

Premises used: IsUltrametricDist.dist_triangle_max, max_lt, LE.le.trans_lt
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r : ℝ
a : X
h : dist y x < r
h' : dist a y < r
⊢ dist a x < r

Tactic:
(dist_triangle_max _ _ _).trans_lt (max_lt h' (dist_comm x _ ▸ h))

Premises used: IsUltrametricDist.dist_triangle_max, Eq.rec, dist_comm, max_lt, Eq.symm, LE.le.trans_lt
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r : ℝ
a : X
h : dist y x < r
h' : dist a y < r
⊢ dist a x < r

Tactic:
exact (dist_triangle_max _ _ _).trans_lt (max_lt h' (dist_comm x _ ▸ h))

Premises used: IsUltrametricDist.dist_triangle_max, max_lt, LE.le.trans_lt
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r s : ℝ
inr :
  ∀
    (this :
      ∀ (x y : X) (r s : ℝ) (hrs : r ≤ s), ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s))
    (hrs : s < r), ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)
wlog! : ∀ (x y : X) (r s : ℝ) (hrs : r ≤ s), ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)
⊢ ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)

Tactic:
wlog! hrs : r ≤ s generalizing x y r s
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r s : ℝ
this : ∀ (x y : X) (r s : ℝ) (hrs : r ≤ s), ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)
hrs : s < r
inr : ball y s ⊆ ball x r ∨ ball x r ⊆ ball y s ∨ Disjoint (ball y s) (ball x r)
⊢ ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)

Tactic:
rw [disjoint_comm, ← or_assoc, or_comm (b := _ ⊆ _), or_assoc]

Premises used: disjoint_comm, or_comm, or_assoc
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r s : ℝ
this : ∀ (x y : X) (r s : ℝ) (hrs : r ≤ s), ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)
hrs : s < r
⊢ ball y s ⊆ ball x r ∨ ball x r ⊆ ball y s ∨ Disjoint (ball y s) (ball x r)

Tactic:
this y x s r hrs.le

Premises used: LT.lt.le
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r s : ℝ
this : ∀ (x y : X) (r s : ℝ) (hrs : r ≤ s), ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)
hrs : s < r
⊢ ball y s ⊆ ball x r ∨ ball x r ⊆ ball y s ∨ Disjoint (ball y s) (ball x r)

Tactic:
exact this y x s r hrs.le

Premises used: LT.lt.le
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x_1 y_1 : X
r_1 s_1 : ℝ
x y : X
r s : ℝ
hrs : r ≤ s
⊢ ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)

Tactic:
Set.disjoint_or_nonempty_inter (ball x r) (ball y s) |>.symm.imp (fun h ↦ ?_) (Or.inr ·)

Premises used: Set.disjoint_or_nonempty_inter, Metric.ball, Or.symm, Or.imp, Or.inr