awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
refine : ∀ (h : (ball x r ∩ ball y s).Nonempty), 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:
refine 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
-- 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
h : (ball x r ∩ ball y s).Nonempty
⊢ h.some (s := ball x r ∩ ball y s) ∈ ball x r

Tactic:
obtain ⟨hxz, hyz⟩ := (Set.mem_inter_iff _ _ _).mp h.some_mem

Premises used: Set.mem_inter_iff, Set.Nonempty.some_mem, Iff.mp
-- 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
h : (ball x r ∩ ball y s).Nonempty
hxz : h.some (s := ball x r ∩ ball y s) ∈ ball x r
⊢ h.some (s := ball x r ∩ ball y s) ∈ ball y s

Tactic:
obtain ⟨hxz, hyz⟩ := (Set.mem_inter_iff _ _ _).mp h.some_mem

Premises used: Set.mem_inter_iff, Set.Nonempty.some_mem, Iff.mp
-- 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
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 x s

Tactic:
have hx := ball_subset_ball hrs (x := x)
-- 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
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
hx : ball x r ⊆ ball x s
rwa rwa₁ rwa₂ rwa₃ : ball x r ⊆ ball x s
⊢ ball x r ⊆ ball y s

Tactic:
rwa [ball_eq_of_mem hyz |>.trans (ball_eq_of_mem <| hx hxz).symm]

Premises used: IsUltrametricDist.ball_eq_of_mem, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
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)

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

Premises used: Set.disjoint_or_nonempty_inter, id, Metric.ball, Or.symm, Or.imp
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r : ℝ
refine : ∀ (h : (ball x r ∩ ball y r).Nonempty), ball x r = ball y r
⊢ ball x r = ball y r ∨ Disjoint (ball x r) (ball y r)

Tactic:
refine Set.disjoint_or_nonempty_inter (ball x r) (ball y r) |>.symm.imp (fun h ↦ ?_) id

Premises used: Set.disjoint_or_nonempty_inter, id, Metric.ball, Or.symm, Or.imp
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
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 (h.some (s := ball x r ∩ ball y r)) r

Tactic:
have h₁ := ball_eq_of_mem <| Set.inter_subset_left h.some_mem
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
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 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
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
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
h₂ : ball y r = ball (h.some (s := ball x r ∩ ball y r)) r
⊢ ball x r = ball y r

Tactic:
h₁.trans h₂.symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
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
h₂ : ball y r = ball (h.some (s := ball x r ∩ ball y r)) r
⊢ ball x r = ball y r

Tactic:
exact h₁.trans h₂.symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r : ℝ
h : y ∈ closedBall x r
h₁ : ∀ (x_1 : X), x_1 ∈ closedBall x r ↔ x_1 ∈ closedBall y r
⊢ closedBall x r = closedBall y r

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

Tactic:
simp_rw [mem_closedBall] at h ⊢

Premises used: Metric.mem_closedBall
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
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
h₂ : dist x_1 y ≤ r → dist x_1 x ≤ r
⊢ dist x_1 x ≤ r ↔ dist x_1 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 : ℝ
x_1 : X
h : dist y x ≤ r
h' : dist x_1 x ≤ r
⊢ dist x_1 y ≤ r

Tactic:
(dist_triangle_max _ _ _).trans (max_le h' (dist_comm x _ ▸ h))

Premises used: IsUltrametricDist.dist_triangle_max, Eq.rec, dist_comm, max_le, LE.le.trans, Eq.symm
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
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

Tactic:
exact (dist_triangle_max _ _ _).trans (max_le h' (dist_comm x _ ▸ h))

Premises used: IsUltrametricDist.dist_triangle_max, max_le, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
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 y ≤ r
⊢ dist x_1 x ≤ r

Tactic:
(dist_triangle_max _ _ _).trans (max_le h' (dist_comm x _ ▸ h))

Premises used: IsUltrametricDist.dist_triangle_max, Eq.rec, dist_comm, max_le, LE.le.trans, Eq.symm
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
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 y ≤ r
⊢ dist x_1 x ≤ r

Tactic:
exact (dist_triangle_max _ _ _).trans (max_le h' (dist_comm x _ ▸ h))

Premises used: IsUltrametricDist.dist_triangle_max, max_le, LE.le.trans
-- 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),
        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)
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)
⊢ 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
-- 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),
    closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)
hrs : s < r
inr : closedBall y s ⊆ closedBall x r ∨ closedBall x r ⊆ closedBall y s ∨ Disjoint (closedBall y s) (closedBall x r)
⊢ closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall 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),
    closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)
hrs : s < r
⊢ closedBall y s ⊆ closedBall x r ∨ closedBall x r ⊆ closedBall y s ∨ Disjoint (closedBall y s) (closedBall 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),
    closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)
hrs : s < r
⊢ closedBall y s ⊆ closedBall x r ∨ closedBall x r ⊆ closedBall y s ∨ Disjoint (closedBall y s) (closedBall 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
⊢ closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)

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

Premises used: Set.disjoint_or_nonempty_inter, Or.symm, Metric.closedBall, Or.imp, Or.inr
-- 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
refine : ∀ (h : (closedBall x r ∩ closedBall y s).Nonempty), 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)

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

Premises used: Set.disjoint_or_nonempty_inter, Or.symm, Metric.closedBall, Or.imp, Or.inr
-- 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
h : (closedBall x r ∩ closedBall y s).Nonempty
⊢ h.some (s := closedBall x r ∩ closedBall y s) ∈ closedBall x r

Tactic:
obtain ⟨hxz, hyz⟩ := (Set.mem_inter_iff _ _ _).mp h.some_mem

Premises used: Set.mem_inter_iff, Set.Nonempty.some_mem, Iff.mp
-- 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
h : (closedBall x r ∩ closedBall y s).Nonempty
hxz : h.some (s := closedBall x r ∩ closedBall y s) ∈ closedBall x r
⊢ h.some (s := closedBall x r ∩ closedBall y s) ∈ closedBall y s

Tactic:
obtain ⟨hxz, hyz⟩ := (Set.mem_inter_iff _ _ _).mp h.some_mem

Premises used: Set.mem_inter_iff, Set.Nonempty.some_mem, Iff.mp
-- 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
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 x s

Tactic:
have hx := closedBall_subset_closedBall hrs (x := x)
-- 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
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
hx : closedBall x r ⊆ closedBall x s
rwa rwa₁ rwa₂ rwa₃ : closedBall x r ⊆ closedBall x s
⊢ closedBall x r ⊆ closedBall y s

Tactic:
rwa [closedBall_eq_of_mem hyz |>.trans (closedBall_eq_of_mem <| hx hxz).symm]

Premises used: IsUltrametricDist.closedBall_eq_of_mem, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
hr : r ≤ 0
⊢ IsClosed (ball x r)

Tactic:
simp [ball_eq_empty.mpr hr]

Premises used: Iff.mpr, Metric.ball_eq_empty
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
inr : ∀ x_1 ∈ (ball x r)ᶜ, ∃ ε > 0, ball x_1 ε ⊆ (ball x r)ᶜ
⊢ IsClosed (ball x r)

Tactic:
rw [← isOpen_compl_iff, isOpen_iff]

Premises used: Metric.isOpen_iff, isOpen_compl_iff
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
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
⊢ y ∉ ball y r

Tactic:
rw [hd] at hy
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
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
hy₁ : y ∉ ball y r
⊢ ball x r = ball y r

Tactic:
rw [hd] at hy
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
y : X
hy : y ∉ ball y r
hd : ball x r = ball y r
⊢ ∃ ε > 0, ball y ε ⊆ (ball x r)ᶜ

Tactic:
simp [h.not_ge] at hy

Premises used: LT.lt.not_ge
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
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)
h₁ : r > 0 ∧ ball y r ⊆ (ball x r)ᶜ
⊢ ∃ ε > 0, ball y ε ⊆ (ball x r)ᶜ

Tactic:
use r
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
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)
⊢ r > 0 ∧ ball y r ⊆ (ball x r)ᶜ

Tactic:
simp [h, ← Set.le_iff_subset, le_compl_iff_disjoint_left, hd]

Premises used: le_compl_iff_disjoint_left, Set.le_iff_subset
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
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
⊢ 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]

Premises used: IsUltrametricDist.ball_eq_or_disjoint, le_compl_iff_disjoint_left, Set.le_iff_subset, LT.lt.not_ge
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
⊢ 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]

Premises used: le_or_gt, Metric.isOpen_iff, le_compl_iff_disjoint_left, Set.le_iff_subset, OfNat.ofNat, isOpen_compl_iff
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
⊢ IsClopen (ball x r)

Tactic:
⟨isClosed_ball x r, isOpen_ball⟩

Premises used: Metric.isOpen_ball, And.intro, IsClopen, IsUltrametricDist.isClosed_ball
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
⊢ frontier (ball x r) = ∅

Tactic:
isClopen_iff_frontier_eq_empty.mp (isClopen_ball x r)

Premises used: Iff.mp, isClopen_iff_frontier_eq_empty, IsUltrametricDist.isClopen_ball
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
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)

Tactic:
Set.disjoint_or_nonempty_inter (closedBall x r) (closedBall y r) |>.symm.imp
    (fun h ↦ ?_) id

Premises used: Set.disjoint_or_nonempty_inter, id, Or.symm, Metric.closedBall, Or.imp
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x y : X
r : ℝ
refine : ∀ (h : (closedBall x r ∩ closedBall y r).Nonempty), closedBall x r = closedBall y r
⊢ closedBall x r = closedBall y r ∨ Disjoint (closedBall x r) (closedBall y r)

Tactic:
refine Set.disjoint_or_nonempty_inter (closedBall x r) (closedBall y r) |>.symm.imp
    (fun h ↦ ?_) id

Premises used: Set.disjoint_or_nonempty_inter, id, Or.symm, Metric.closedBall, Or.imp
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
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 (h.some (s := closedBall x r ∩ closedBall y r)) r

Tactic:
have h₁ := closedBall_eq_of_mem <| Set.inter_subset_left h.some_mem
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
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 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
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
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
h₂ : closedBall y r = closedBall (h.some (s := closedBall x r ∩ closedBall y r)) r
⊢ closedBall x r = closedBall y r

Tactic:
h₁.trans h₂.symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
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
h₂ : closedBall y r = closedBall (h.some (s := closedBall x r ∩ closedBall y r)) r
⊢ closedBall x r = closedBall y r

Tactic:
exact h₁.trans h₂.symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
h : r < 0
⊢ IsOpen (closedBall x r)

Tactic:
simp [closedBall_eq_empty.mpr h]

Premises used: Iff.mpr, Metric.closedBall_eq_empty
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
h : 0 < r
inr : ∀ x_1 ∈ closedBall x r, ∃ ε > 0, ball x_1 ε ⊆ closedBall x r
⊢ IsOpen (closedBall x r)

Tactic:
rw [isOpen_iff]

Premises used: Metric.isOpen_iff
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
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
h₁ : 0 < r ∧ ball y r ⊆ closedBall x r
⊢ ∃ (ε : ℝ), 0 < ε ∧ ball y ε ⊆ closedBall x r

Tactic:
use r
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
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 < r ∧ ball y r ⊆ closedBall x r

Tactic:
simp [h, hd, ball_subset_closedBall]

Premises used: Metric.ball_subset_closedBall
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
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 : Disjoint (closedBall x r) (closedBall y r)
⊢ ∃ (ε : ℝ), 0 < ε ∧ ball y ε ⊆ closedBall x r

Tactic:
simp [closedBall_eq_of_mem hy, h.not_gt] at hd

Premises used: IsUltrametricDist.closedBall_eq_of_mem, LT.lt.not_gt
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
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
⊢ 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

Premises used: Metric.ball_subset_closedBall, IsUltrametricDist.closedBall_eq_of_mem, LT.lt.not_gt, IsUltrametricDist.closedBall_eq_or_disjoint
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
⊢ 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

Premises used: lt_or_gt_of_ne, Metric.ball_subset_closedBall, Metric.isOpen_iff, gt_iff_lt
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
⊢ IsClopen (closedBall x r)

Tactic:
⟨Metric.isClosed_closedBall, isOpen_closedBall x hr⟩

Premises used: Metric.isClosed_closedBall, IsUltrametricDist.isOpen_closedBall, And.intro, IsClopen
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
⊢ frontier (closedBall x r) = ∅

Tactic:
isClopen_iff_frontier_eq_empty.mp (isClopen_closedBall x hr)

Premises used: Iff.mp, isClopen_iff_frontier_eq_empty, IsUltrametricDist.isClopen_closedBall
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
rw : IsOpen (closedBall x r ⊓ (ball x r)ᶜ)
⊢ IsOpen (sphere x r)

Tactic:
rw [← closedBall_diff_ball, sdiff_eq]

Premises used: sdiff_eq, Metric.closedBall_diff_ball
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
⊢ IsOpen (closedBall x r ⊓ (ball x r)ᶜ)

Tactic:
(isOpen_closedBall x hr).inter (isClosed_ball x r).isOpen_compl

Premises used: IsClosed.isOpen_compl, IsUltrametricDist.isOpen_closedBall, IsOpen.inter
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
⊢ IsOpen (closedBall x r ⊓ (ball x r)ᶜ)

Tactic:
exact (isOpen_closedBall x hr).inter (isClosed_ball x r).isOpen_compl

Premises used: IsClosed.isOpen_compl, IsUltrametricDist.isOpen_closedBall, IsOpen.inter
-- Module: Mathlib.Topology.MetricSpace.Ultra.Basic
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
⊢ IsClopen (sphere x r)

Tactic:
⟨Metric.isClosed_sphere, isOpen_sphere x hr⟩

Premises used: IsUltrametricDist.isOpen_sphere, Metric.isClosed_sphere, And.intro, IsClopen
-- Module: Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : MetricSpace Y
inst_3 : IsUltrametricDist Y
dist_triangle_max : ∀ (x y z : C(X, Y)), dist x z ≤ max (dist x y) (dist y z)
⊢ IsUltrametricDist C(X, Y)

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps
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)
⊢ 0 ≤ max (dist f g) (dist g h)

Tactic:
positivity