awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ∃ t ∈ 𝓝[K] x, ∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U
have hnhds : thickening (δ / 2) (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, ?_⟩
-- 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
⊢ thickening (δ / 2) (f '' V) ⊆ U
have calc : thickening (δ / 2 + δ / 2) {f x} ⊆ 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]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y z : X
h : dist x y ≠ dist y z
⊢ dist x z = max (dist x y) (dist y z)
have apply : max (dist x y) (dist y z) ≤ dist x z
Tactic: apply le_antisymm (dist_triangle_max x y z)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y z : X
h : dist x y ≠ dist y z
⊢ max (dist x y) (dist y z) ≤ dist x z
have inl : ∀ (h : dist x y < dist y z), max (dist x y) (dist y z) ≤ dist x z
Tactic: rcases h.lt_or_gt with h | h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
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
⊢ max (dist x y) (dist y z) ≤ dist x z
have inr : ∀ (h : dist y z < dist x y), max (dist x y) (dist y z) ≤ dist x z
Tactic: rcases h.lt_or_gt with h | h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
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
⊢ max (dist x y) (dist y z) ≤ dist x z
have inl : dist y z ≤ dist x z
Tactic: rw [max_eq_right h.le]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
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 x z
have inl : ¬dist y z ≤ dist y x
Tactic: apply (le_max_iff.mp <| dist_triangle_max y x z).resolve_left
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
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
⊢ max (dist x y) (dist y z) ≤ dist x z
have inr : dist y x ≤ dist z x
Tactic: rw [max_eq_left h.le, dist_comm x y, dist_comm x z]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
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 z x
have inr : ¬dist y x ≤ dist y z
Tactic: apply (le_max_iff.mp <| dist_triangle_max y z x).resolve_left
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r : ℝ
h : y ∈ ball x r
⊢ ball x r = ball y r
have h₁ : ∀ (a : X), a ∈ ball x r ↔ a ∈ ball y r
Tactic: ext a
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (hypothesis)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r : ℝ
h : y ∈ ball x r
a : X
⊢ a ∈ ball x r ↔ a ∈ ball y r
have h₁ : dist y x < r
Tactic: simp_rw [mem_ball] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r : ℝ
a : X
h : dist y x < r
⊢ dist a x < r ↔ dist a y < r
have h₁ : dist a x < r → dist a y < r
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
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
⊢ dist a x < r ↔ dist a y < r
have h₂ : dist a y < r → dist a x < r
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r s : ℝ
⊢ ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)
have 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)
Tactic: wlog! hrs : r ≤ s generalizing x y r s
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
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)
⊢ ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)
have 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)
Tactic: wlog! hrs : r ≤ s generalizing x y r s
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
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 x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)
have inr : ball y s ⊆ ball x r ∨ ball x r ⊆ ball y s ∨ Disjoint (ball y s) (ball x r)
Tactic: rw [disjoint_comm, ← or_assoc, or_comm (b := _ ⊆ _), or_assoc]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
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)
have refine : ∀ (h : (ball x r ∩ ball y s).Nonempty), ball x r ⊆ ball y s
Tactic: refine Set.disjoint_or_nonempty_inter (ball x r) (ball y s) |>.symm.imp (fun h ↦ ?_) (Or.inr ·)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (hypothesis)
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
h : (ball x r ∩ ball y s).Nonempty
⊢ ball x r ⊆ ball y s
have hxz : h.some (s := ball x r ∩ ball y s) ∈ ball x r
Tactic: obtain ⟨hxz, hyz⟩ := (Set.mem_inter_iff _ _ _).mp h.some_mem
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (hypothesis)
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
h : (ball x r ∩ ball y s).Nonempty
hxz : h.some (s := ball x r ∩ ball y s) ∈ ball x r
⊢ ball x r ⊆ ball y s
have hyz : h.some (s := ball x r ∩ ball y s) ∈ ball y s
Tactic: obtain ⟨hxz, hyz⟩ := (Set.mem_inter_iff _ _ _).mp h.some_mem
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (hypothesis)
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
h : (ball x r ∩ ball y s).Nonempty
hxz : h.some (s := ball x r ∩ ball y s) ∈ ball x r
hyz : h.some (s := ball x r ∩ ball y s) ∈ ball y s
⊢ ball x r ⊆ ball y s
have hx : ball x r ⊆ ball x s
Tactic: have hx := ball_subset_ball hrs (x := x)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r : ℝ
⊢ ball x r = ball y r ∨ Disjoint (ball x r) (ball y r)
have refine : ∀ (h : (ball x r ∩ ball y r).Nonempty), ball x r = ball y r
Tactic: refine Set.disjoint_or_nonempty_inter (ball x r) (ball y r) |>.symm.imp (fun h ↦ ?_) id
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (hypothesis)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r : ℝ
h : (ball x r ∩ ball y r).Nonempty
⊢ ball x r = ball y r
have h₁ : ball x r = ball (h.some (s := ball x r ∩ ball y r)) r
Tactic: have h₁ := ball_eq_of_mem <| Set.inter_subset_left h.some_mem
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (hypothesis)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r : ℝ
h : (ball x r ∩ ball y r).Nonempty
h₁ : ball x r = ball (h.some (s := ball x r ∩ ball y r)) r
⊢ ball x r = ball y r
have h₂ : ball y r = ball (h.some (s := ball x r ∩ ball y r)) r
Tactic: have h₂ := ball_eq_of_mem <| Set.inter_subset_right h.some_mem
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r : ℝ
h : y ∈ closedBall x r
⊢ closedBall x r = closedBall y r
have h₁ : ∀ (x_1 : X), x_1 ∈ closedBall x r ↔ x_1 ∈ closedBall y r
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (hypothesis)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r : ℝ
h : y ∈ closedBall x r
x_1 : X
⊢ x_1 ∈ closedBall x r ↔ x_1 ∈ closedBall y r
have h₁ : dist y x ≤ r
Tactic: simp_rw [mem_closedBall] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r : ℝ
x_1 : X
h : dist y x ≤ r
⊢ dist x_1 x ≤ r ↔ dist x_1 y ≤ r
have h₁ : dist x_1 x ≤ r → dist x_1 y ≤ r
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r : ℝ
x_1 : X
h : dist y x ≤ r
h₁ : dist x_1 x ≤ r → dist x_1 y ≤ r
⊢ dist x_1 x ≤ r ↔ dist x_1 y ≤ r
have h₂ : dist x_1 y ≤ r → dist x_1 x ≤ r
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r s : ℝ
⊢ closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)
have inr : ∀
  (this :
    ∀ (x y : X) (r s : ℝ) (hrs : r ≤ s),
      closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s))
  (hrs : s < r),
  closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)
Tactic: wlog! hrs : r ≤ s generalizing x y r s
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
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),
        closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s))
    (hrs : s < r),
    closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)
⊢ closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)
have wlog! : ∀ (x y : X) (r s : ℝ) (hrs : r ≤ s),
  closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)
Tactic: wlog! hrs : r ≤ s generalizing x y r s
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
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),
    closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)
hrs : s < r
⊢ closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)
have inr : closedBall y s ⊆ closedBall x r ∨ closedBall x r ⊆ closedBall y s ∨ Disjoint (closedBall y s) (closedBall x r)
Tactic: rw [disjoint_comm, ← or_assoc, or_comm (b := _ ⊆ _), or_assoc]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
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
⊢ closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)
have refine : ∀ (h : (closedBall x r ∩ closedBall y s).Nonempty), closedBall x r ⊆ closedBall y s
Tactic: refine Set.disjoint_or_nonempty_inter (closedBall x r) (closedBall y s) |>.symm.imp
      (fun h ↦ ?_) (Or.inr ·)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (hypothesis)
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
h : (closedBall x r ∩ closedBall y s).Nonempty
⊢ closedBall x r ⊆ closedBall y s
have hxz : h.some (s := closedBall x r ∩ closedBall y s) ∈ closedBall x r
Tactic: obtain ⟨hxz, hyz⟩ := (Set.mem_inter_iff _ _ _).mp h.some_mem
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (hypothesis)
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
h : (closedBall x r ∩ closedBall y s).Nonempty
hxz : h.some (s := closedBall x r ∩ closedBall y s) ∈ closedBall x r
⊢ closedBall x r ⊆ closedBall y s
have hyz : h.some (s := closedBall x r ∩ closedBall y s) ∈ closedBall y s
Tactic: obtain ⟨hxz, hyz⟩ := (Set.mem_inter_iff _ _ _).mp h.some_mem
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (hypothesis)
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
h : (closedBall x r ∩ closedBall y s).Nonempty
hxz : h.some (s := closedBall x r ∩ closedBall y s) ∈ closedBall x r
hyz : h.some (s := closedBall x r ∩ closedBall y s) ∈ closedBall y s
⊢ closedBall x r ⊆ closedBall y s
have hx : closedBall x r ⊆ closedBall x s
Tactic: have hx := closedBall_subset_closedBall hrs (x := x)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
⊢ IsClosed (ball x r)
have inr : ∀ x_1 ∈ (ball x r)ᶜ, ∃ ε > 0, ball x_1 ε ⊆ (ball x r)ᶜ
Tactic: rw [← isOpen_compl_iff, isOpen_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (hypothesis)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
y : X
hy : y ∉ ball x r
hd : ball x r = ball y r
⊢ ∃ ε > 0, ball y ε ⊆ (ball x r)ᶜ
have hy₁ : y ∉ ball y r
Tactic: rw [hd] at hy
Cleared hypotheses: hy, hd
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
y : X
hy : y ∉ ball x r
hd : Disjoint (ball x r) (ball y r)
⊢ ∃ ε > 0, ball y ε ⊆ (ball x r)ᶜ
have h₁ : r > 0 ∧ ball y r ⊆ (ball x r)ᶜ
Tactic: use r
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (hypothesis)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
y : X
hy : y ∉ ball x r
⊢ ∃ ε > 0, ball y ε ⊆ (ball x r)ᶜ
have x₁ : ball x r = ball y r ∨ Disjoint (ball x r) (ball y r)
Tactic: cases ball_eq_or_disjoint x y r with
    | inl hd =>
      rw [hd] at hy
      simp [h.not_ge] at hy
    | inr hd =>
      use r
      simp [h, ← Set.le_iff_subset, le_compl_iff_disjoint_left, hd]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (hypothesis)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
⊢ IsClosed (ball x r)
have x₁ : r ≤ 0 ∨ 0 < r
Tactic: cases le_or_gt r 0 with
  | inl hr =>
    simp [ball_eq_empty.mpr hr]
  | inr h =>
    rw [← isOpen_compl_iff, isOpen_iff]
    push _ ∈ _
    intro y hy
    cases ball_eq_or_disjoint x y r with
    | inl hd =>
      rw [hd] at hy
      simp [h.not_ge] at hy
    | inr hd =>
      use r
      simp [h, ← Set.le_iff_subset, le_compl_iff_disjoint_left, hd]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r : ℝ
⊢ closedBall x r = closedBall y r ∨ Disjoint (closedBall x r) (closedBall y r)
have refine : ∀ (h : (closedBall x r ∩ closedBall y r).Nonempty), closedBall x r = closedBall y r
Tactic: refine Set.disjoint_or_nonempty_inter (closedBall x r) (closedBall y r) |>.symm.imp
    (fun h ↦ ?_) id
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (hypothesis)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r : ℝ
h : (closedBall x r ∩ closedBall y r).Nonempty
⊢ closedBall x r = closedBall y r
have h₁ : closedBall x r = closedBall (h.some (s := closedBall x r ∩ closedBall y r)) r
Tactic: have h₁ := closedBall_eq_of_mem <| Set.inter_subset_left h.some_mem
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (hypothesis)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r : ℝ
h : (closedBall x r ∩ closedBall y r).Nonempty
h₁ : closedBall x r = closedBall (h.some (s := closedBall x r ∩ closedBall y r)) r
⊢ closedBall x r = closedBall y r
have h₂ : closedBall y r = closedBall (h.some (s := closedBall x r ∩ closedBall y r)) r
Tactic: have h₂ := closedBall_eq_of_mem <| Set.inter_subset_right h.some_mem
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
h : 0 < r
⊢ IsOpen (closedBall x r)
have inr : ∀ x_1 ∈ closedBall x r, ∃ ε > 0, ball x_1 ε ⊆ closedBall x r
Tactic: rw [isOpen_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
h : 0 < r
y : X
hy : y ∈ closedBall x r
hd : closedBall x r = closedBall y r
⊢ ∃ (ε : ℝ), 0 < ε ∧ ball y ε ⊆ closedBall x r
have h₁ : 0 < r ∧ ball y r ⊆ closedBall x r
Tactic: use r
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (hypothesis)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
h : 0 < r
y : X
hy : y ∈ closedBall x r
⊢ ∃ (ε : ℝ), 0 < ε ∧ ball y ε ⊆ closedBall x r
have x₁ : closedBall x r = closedBall y r ∨ Disjoint (closedBall x r) (closedBall y r)
Tactic: cases closedBall_eq_or_disjoint x y r with
    | inl hd =>
      use r
      simp [h, hd, ball_subset_closedBall]
    | inr hd =>
      simp [closedBall_eq_of_mem hy, h.not_gt] at hd
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (hypothesis)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
⊢ IsOpen (closedBall x r)
have x₁ : r < 0 ∨ 0 < r
Tactic: cases lt_or_gt_of_ne hr with
  | inl h =>
    simp [closedBall_eq_empty.mpr h]
  | inr h =>
    rw [isOpen_iff]
    simp only [gt_iff_lt]
    intro y hy
    cases closedBall_eq_or_disjoint x y r with
    | inl hd =>
      use r
      simp [h, hd, ball_subset_closedBall]
    | inr hd =>
      simp [closedBall_eq_of_mem hy, h.not_gt] at hd
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
⊢ IsOpen (sphere x r)
have rw : IsOpen (closedBall x r ⊓ (ball x r)ᶜ)
Tactic: rw [← closedBall_diff_ball, sdiff_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : MetricSpace Y
inst_3 : IsUltrametricDist Y
⊢ IsUltrametricDist C(X, Y)
have dist_triangle_max : ∀ (x y z : C(X, Y)), dist x z ≤ max (dist x y) (dist y z)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : MetricSpace Y
inst_3 : IsUltrametricDist Y
f g h : C(X, Y)
⊢ dist f h ≤ max (dist f g) (dist g h)
have dist_triangle_max : ∀ (x : X), dist.{u_2} (α := Y) ((f : (a : X) → Y) x : Y) ((h : (a : X) → Y) x : Y) ≤ max (dist f g) (dist g h)
Tactic: rw [ContinuousMap.dist_le (by positivity)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : MetricSpace Y
inst_3 : IsUltrametricDist Y
f g h : C(X, Y)
⊢ ∀ (x : X), dist.{u_2} (α := Y) ((f : (a : X) → Y) x : Y) ((h : (a : X) → Y) x : Y) ≤ max (dist f g) (dist g h)
have dist_triangle_max : ∀ (x : X), dist.{u_2} (α := Y) ((f : (a : X) → Y) x : Y) ((g : (a : X) → Y) x : Y) ≤ dist f g
Tactic: refine fun x ↦ (dist_triangle_max (f x) (g x) (h x)).trans (max_le_max ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : MetricSpace Y
inst_3 : IsUltrametricDist Y
f g h : C(X, Y)
dist_triangle_max : ∀ (x : X), dist.{u_2} (α := Y) ((f : (a : X) → Y) x : Y) ((g : (a : X) → Y) x : Y) ≤ dist f g
⊢ ∀ (x : X), dist.{u_2} (α := Y) ((f : (a : X) → Y) x : Y) ((h : (a : X) → Y) x : Y) ≤ max (dist f g) (dist g h)
have dist_triangle_max₁ : ∀ (x : X), dist.{u_2} (α := Y) ((g : (a : X) → Y) x : Y) ((h : (a : X) → Y) x : Y) ≤ dist g h
Tactic: refine fun x ↦ (dist_triangle_max (f x) (g x) (h x)).trans (max_le_max ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Pi (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → PseudoMetricSpace (X i)
inst_2 : ∀ (i : ι), IsUltrametricDist.{u_2} (X i)
⊢ IsUltrametricDist ((i : ι) → X i)
have dist_triangle_max : ∀ (x y z : (i : ι) → X i), dist x z ≤ max (dist x y) (dist y z)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Ultra.Pi (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → PseudoMetricSpace (X i)
inst_2 : ∀ (i : ι), IsUltrametricDist.{u_2} (X i)
f g h : (i : ι) → X i
⊢ dist f h ≤ max (dist f g) (dist g h)
have dist_triangle_max : LE.le (α := NNReal) (Finset.sup Finset.univ fun (b : ι) ↦ nndist (f b) (h b))
  (Finset.sup.{0, u_1} (β := ι) Finset.univ ((fun (b : ι) ↦ nndist (f b) (g b)) ⊔ fun (b : ι) ↦ nndist (g b) (h b)))
Tactic: simp only [dist_pi_def, ← NNReal.coe_max, NNReal.coe_le_coe, ← Finset.sup_sup]
-- 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
⊢ (fun (x1 x2 : X) ↦ ∃ (U : Set X), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ) x y
have obtain : ∀ (r : ℝ) (hr : 0 < r) (hr' : r < dist x y), ∃ (U : Set X), IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ
Tactic: obtain ⟨r, hr, hr'⟩ := exists_between (dist_pos.mpr h)
-- 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
⊢ ∃ (U : Set X), IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ
have refine_1 : x ∈ ball x r
Tactic: refine ⟨_, IsUltrametricDist.isClopen_ball x r, ?_, ?_⟩