awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
β : Type u_2
inst : PseudoMetricSpace β
x y : ULift.{u_3, u_2} β
⊢ nndist x y = nndist x.down y.down

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
β : Type u_2
inst : PseudoMetricSpace β
x y : β
⊢ dist { down := x : ULift.{u_3, u_2} β } { down := y : ULift.{u_3, u_2} β } = dist x y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
β : Type u_2
inst : PseudoMetricSpace β
x y : β
⊢ nndist { down := x : ULift.{u_3, u_2} β } { down := y : ULift.{u_3, u_2} β } = nndist x y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x y : α × β
⊢ LE.le (α := ℝ) 0 ((fun (x y : α × β) ↦ max (dist x.1 y.1) (dist x.2 y.2)) x y)

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x y : α × β
⊢ edist x y = ENNReal.ofReal ((fun (x y : α × β) ↦ max (dist x.1 y.1) (dist x.2 y.2)) x y)

Tactic:
simp only [ENNReal.ofReal_max, Prod.edist_eq, edist_dist]

Premises used: Prod.edist_eq, ENNReal.ofReal_max, edist_dist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
i : PseudoMetricSpace (α × β) :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun (x y : α × β) ↦ max (dist x.1 y.1) (dist x.2 y.2)) ⋯ ⋯
s : Set (α × β)
simp :
  (∀ᶠ (x : ℝ) in atTop,
      ∀ (x_1 : α × β) (x_2 : x_1 ∈ s) (x_3 : α × β) (x_4 : x_3 ∈ s), max (dist x_1.1 x_3.1) (dist x_1.2 x_3.2) ≤ x) ↔
    ∀ᶠ (C : ℝ) in atTop, ∀ ⦃x : α × β⦄, x ∈ s → ∀ ⦃y : α × β⦄, y ∈ s → dist x y ≤ C
⊢ Bornology.IsBounded s ↔ Bornology.IsBounded s

Tactic:
simp only [← isBounded_image_fst_and_snd, isBounded_iff_eventually, forall_mem_image, ←
      eventually_and, ← forall_and, ← max_le_iff]

Premises used: Filter.eventually_and, Metric.isBounded_iff_eventually, max_le_iff, Bornology.isBounded_image_fst_and_snd, Set.forall_mem_image, forall_and
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
i : PseudoMetricSpace (α × β) :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun (x y : α × β) ↦ max (dist x.1 y.1) (dist x.2 y.2)) ⋯ ⋯
s : Set (α × β)
⊢ (∀ᶠ (x : ℝ) in atTop,
      ∀ (x_1 : α × β) (x_2 : x_1 ∈ s) (x_3 : α × β) (x_4 : x_3 ∈ s), max (dist x_1.1 x_3.1) (dist x_1.2 x_3.2) ≤ x) ↔
    ∀ᶠ (C : ℝ) in atTop, ∀ ⦃x : α × β⦄, x ∈ s → ∀ ⦃y : α × β⦄, y ∈ s → dist x y ≤ C

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x y : α × β
⊢ dist x y = max (dist x.1 y.1) (dist x.2 y.2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x : α
y₁ y₂ : β
⊢ dist (x, y₁) (x, y₂) = dist y₁ y₂

Tactic:
simp [Prod.dist_eq]

Premises used: Prod.dist_eq
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x₁ x₂ : α
y : β
⊢ dist (x₁, y) (x₂, y) = dist x₁ x₂

Tactic:
simp [Prod.dist_eq]

Premises used: Prod.dist_eq
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x : α
y : β
r : ℝ
z : α × β
⊢ z ∈ ball x r ×ˢ ball y r ↔ z ∈ ball (x, y) r

Tactic:
simp [Prod.dist_eq]

Premises used: Prod.dist_eq
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x : α
y : β
r : ℝ
z : α × β
⊢ z ∈ closedBall x r ×ˢ closedBall y r ↔ z ∈ closedBall (x, y) r

Tactic:
simp [Prod.dist_eq]

Premises used: Prod.dist_eq
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x : α × β
r : ℝ
inl : ∀ (hr : r < 0), sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r
inr : sphere x 0 = sphere x.1 0 ×ˢ closedBall x.2 0 ∪ closedBall x.1 0 ×ˢ sphere x.2 0
inr₁ : ∀ (hr : 0 < r), sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r
⊢ sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r

Tactic:
obtain hr | rfl | hr := lt_trichotomy r 0

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x : α × β
r : ℝ
hr : r < 0
⊢ sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r

Tactic:
simp [hr]
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x : α × β
inr :
  ∀ (fst : α) (snd : β),
    sphere (fst, snd) 0 =
      sphere (fst, snd).1 0 ×ˢ closedBall (fst, snd).2 0 ∪ closedBall (fst, snd).1 0 ×ˢ sphere (fst, snd).2 0
⊢ sphere x 0 = sphere x.1 0 ×ˢ closedBall x.2 0 ∪ closedBall x.1 0 ×ˢ sphere x.2 0

Tactic:
cases x
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
fst : α
snd : β
inr inr₁ : sphere (fst, snd) 0 = sphere fst 0 ×ˢ closedBall snd 0 ∪ closedBall fst 0 ×ˢ sphere snd 0
inr₂ : closedBall (fst, snd) 0 = closedBall fst 0 ×ˢ closedBall snd 0 ∪ closedBall fst 0 ×ˢ closedBall snd 0
inr₃ : closedBall (fst, snd) 0 = closedBall fst 0 ×ˢ closedBall snd 0
⊢ sphere (fst, snd) 0 =
    sphere (fst, snd).1 0 ×ˢ closedBall (fst, snd).2 0 ∪ closedBall (fst, snd).1 0 ×ˢ sphere (fst, snd).2 0

Tactic:
simp_rw [← closedBall_eq_sphere_of_nonpos le_rfl, union_self, closedBall_prod_same]

Premises used: le_rfl, closedBall_prod_same, Metric.closedBall_eq_sphere_of_nonpos, Set.union_self
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x : α × β
r : ℝ
hr : 0 < r
inr :
  ∀ (x' : α) (y' : β),
    (x', y') ∈ sphere x r ↔ (x', y') ∈ sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r
⊢ sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r

Tactic:
ext ⟨x', y'⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x : α × β
r : ℝ
hr : 0 < r
x' : α
y' : β
inr :
  dist x' x.1 = r ∧ dist y' x.2 ≤ dist x' x.1 ∨ dist y' x.2 = r ∧ dist x' x.1 ≤ dist y' x.2 ↔
    dist x' x.1 = r ∧ dist y' x.2 ≤ r ∨ dist x' x.1 ≤ r ∧ dist y' x.2 = r
⊢ (x', y') ∈ sphere x r ↔ (x', y') ∈ sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r

Tactic:
simp_rw [Set.mem_union, Set.mem_prod, Metric.mem_closedBall, Metric.mem_sphere, Prod.dist_eq,
      max_eq_iff]

Premises used: Set.mem_union, Prod.dist_eq, Metric.mem_sphere, Set.mem_prod, Metric.mem_closedBall, max_eq_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x : α × β
r : ℝ
hr : 0 < r
x' : α
y' : β
⊢ dist x' x.1 = r ∧ dist y' x.2 ≤ dist x' x.1 ∨ dist y' x.2 = r ∧ dist x' x.1 ≤ dist y' x.2 ↔
    dist x' x.1 = r ∧ dist y' x.2 ≤ r ∨ dist x' x.1 ≤ r ∧ dist y' x.2 = r

Tactic:
or_congr (and_congr_right ?_) (and_comm.trans (and_congr_left ?_))

Premises used: or_congr, and_comm, and_congr_right, and_congr_left, Iff.trans
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x : α × β
r : ℝ
hr : 0 < r
x' : α
y' : β
inr : dist x' x.1 = r → (dist y' x.2 ≤ dist x' x.1 ↔ dist y' x.2 ≤ r)
inr₁ : dist y' x.2 = r → (dist x' x.1 ≤ dist y' x.2 ↔ dist x' x.1 ≤ r)
⊢ dist x' x.1 = r ∧ dist y' x.2 ≤ dist x' x.1 ∨ dist y' x.2 = r ∧ dist x' x.1 ≤ dist y' x.2 ↔
    dist x' x.1 = r ∧ dist y' x.2 ≤ r ∨ dist x' x.1 ≤ r ∧ dist y' x.2 = r

Tactic:
refine or_congr (and_congr_right ?_) (and_comm.trans (and_congr_left ?_))

Premises used: or_congr, and_comm, and_congr_right, and_congr_left, Iff.trans
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x : α × β
x' : α
y' : β
hr : 0 < dist x' x.1
⊢ dist y' x.2 ≤ dist x' x.1 ↔ dist y' x.2 ≤ dist x' x.1

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x : α × β
x' : α
y' : β
hr : 0 < dist y' x.2
⊢ dist x' x.1 ≤ dist y' x.2 ↔ dist x' x.1 ≤ dist y' x.2

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
inst : PseudoMetricSpace α
⊢ UniformContinuous (β := ℝ) fun (p : α × α) ↦ dist p.1 p.2

Tactic:
Metric.uniformContinuous_iff.2 fun ε ε0 =>
    ⟨ε / 2, half_pos ε0, fun {a b} h =>
      calc dist (dist a.1 a.2) (dist b.1 b.2) ≤ dist a.1 b.1 + dist a.2 b.2 :=
        dist_dist_dist_le _ _ _ _
      _ ≤ dist a b + dist a b := add_le_add (le_max_left _ _) (le_max_right _ _)
      _ < ε / 2 + ε / 2 := add_lt_add h h
      _ = ε := add_halves ε⟩

Premises used: le_max_right, Iff.mpr, Trans.trans, add_halves, half_pos, Set.Mem, add_le_add, setOf, HDiv.hDiv, Prod.fst, add_lt_add, And.intro, Exists.intro, dist_dist_dist_le, Dist.dist, OfNat.ofNat, le_max_left, Prod.snd, Metric.uniformContinuous_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : UniformSpace β
f g : β → α
hf : UniformContinuous f
hg : UniformContinuous g
⊢ UniformContinuous (β := ℝ) fun (b : β) ↦ dist (f b) (g b)

Tactic:
uniformContinuous_dist.comp (hf.prodMk hg)

Premises used: uniformContinuous_dist, UniformContinuous.prodMk, UniformContinuous.comp
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
inst : PseudoMetricSpace α
⊢ Continuous[instTopologicalSpaceProd, _] fun (p : α × α) ↦ dist p.1 p.2

Tactic:
uniformContinuous_dist.continuous

Premises used: uniformContinuous_dist, setOf, UniformContinuous.continuous
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
f g : β → α
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
⊢ Continuous[inst_1, _] fun (b : β) ↦ dist (f b) (g b)

Tactic:
continuous_dist.comp₂ hf hg

Premises used: Continuous.comp₂, continuous_dist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
f g : β → α
x : Filter β
a b : α
hf : Tendsto f x (𝓝 a)
hg : Tendsto g x (𝓝 b)
⊢ Tendsto (fun (x : β) ↦ dist (f x) (g x)) x (𝓝 (dist a b))

Tactic:
(continuous_dist.tendsto (a, b)).comp (hf.prodMk_nhds hg)

Premises used: continuous_dist, Prod.mk, Continuous.tendsto, Filter.Tendsto.comp, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
f : β → α
⊢ Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ↔
    Continuous[instTopologicalSpaceProd, _] fun (x : β × β) ↦ dist (f x.1) (f x.2)

Tactic:
⟨fun h => h.fst'.dist h.snd', fun h =>
    continuous_iff_continuousAt.2 fun _ => tendsto_iff_dist_tendsto_zero.2 <|
      (h.comp (.prodMk_left _)).tendsto' _ _ <| dist_self _⟩

Premises used: Iff.mpr, Continuous.fst', Continuous.snd', Continuous.comp, Continuous.dist, Prod.mk, Prod.fst, dist_self, Iff.intro, Continuous.tendsto', OfNat.ofNat, Continuous.prodMk_left, tendsto_iff_dist_tendsto_zero, continuous_iff_continuousAt
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
inst : PseudoMetricSpace α
⊢ UniformContinuous (β := ℝ≥0) fun (p : α × α) ↦ nndist p.1 p.2

Tactic:
uniformContinuous_dist.subtype_mk _

Premises used: uniformContinuous_dist, NNReal, UniformContinuous.subtype_mk
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : UniformSpace β
f g : β → α
hf : UniformContinuous f
hg : UniformContinuous g
⊢ UniformContinuous (β := ℝ≥0) fun (b : β) ↦ nndist (f b) (g b)

Tactic:
uniformContinuous_nndist.comp (hf.prodMk hg)

Premises used: uniformContinuous_nndist, UniformContinuous.prodMk, UniformContinuous.comp
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
inst : PseudoMetricSpace α
⊢ Continuous[instTopologicalSpaceProd, _] fun (p : α × α) ↦ nndist p.1 p.2

Tactic:
uniformContinuous_nndist.continuous

Premises used: setOf, uniformContinuous_nndist, UniformContinuous.continuous
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
f g : β → α
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
⊢ Continuous[inst_1, _] fun (b : β) ↦ nndist (f b) (g b)

Tactic:
continuous_nndist.comp₂ hf hg

Premises used: Continuous.comp₂, continuous_nndist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
f g : β → α
x : Filter β
a b : α
hf : Tendsto f x (𝓝 a)
hg : Tendsto g x (𝓝 b)
⊢ Tendsto (fun (x : β) ↦ nndist (f x) (g x)) x (𝓝 (nndist a b))

Tactic:
(continuous_nndist.tendsto (a, b)).comp (hf.prodMk_nhds hg)

Premises used: Prod.mk, Continuous.tendsto, Filter.Tendsto.comp, continuous_nndist, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
ε : ℝ
hε : 0 < ε
⊢ ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε

Tactic:
⟨ε / 2, half_pos hε, fun _x hx _y hy => add_halves ε ▸ add_lt_add hx hy⟩

Premises used: add_halves, half_pos, Eq.rec, HDiv.hDiv, add_lt_add, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} s
t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} t
inl :
  ∀
    (hs :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} ∅),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
      (∅ ∪ t)
inr :
  ∀ (x : α) (hx : x ∈ s),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
      (s ∪ t)
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} (s ∪ t)

Tactic:
rcases s.eq_empty_or_nonempty with rfl | ⟨x, hx⟩

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} t
hs : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} ∅
inl inl₁ inl₂ inl₃ :
  Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} t
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} (∅ ∪ t)

Tactic:
rwa [empty_union]

Premises used: Set.empty_union
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} s
t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} t
x : α
hx : x ∈ s
inr :
  ∀
    (ht :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} ∅),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
      (s ∪ ∅)
inr₁ :
  ∀ (y : α) (hy : y ∈ t),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
      (s ∪ t)
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} (s ∪ t)

Tactic:
rcases t.eq_empty_or_nonempty with rfl | ⟨y, hy⟩

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} s
x : α
hx : x ∈ s
ht : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} ∅
inr inr₁ inr₂ inr₃ :
  Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} s
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} (s ∪ ∅)

Tactic:
rwa [union_empty]

Premises used: Set.union_empty
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} s
t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
inr :
  ∀ (C : ℝ) (hC : ∀ z ∈ s ∪ t, dist x z ≤ C),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
      (s ∪ t)
rsuffices : ∃ (C : ℝ), ∀ z ∈ s ∪ t, dist x z ≤ C
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} (s ∪ t)

Tactic:
rsuffices ⟨C, hC⟩ : ∃ C, ∀ z ∈ s ∪ t, dist x z ≤ C
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} s
t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
C : ℝ
hC : ∀ z ∈ s ∪ t, dist x z ≤ C
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} (s ∪ t)

Tactic:
⟨C + C, fun a ha b hb => (dist_triangle a x b).trans ?_⟩

Premises used: Set.Mem, setOf, HAdd.hAdd, Exists.intro, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} s
t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
C : ℝ
hC : ∀ z ∈ s ∪ t, dist x z ≤ C
inr : ∀ (a : α) (ha : a ∈ s ∪ t) (b : α) (hb : b ∈ s ∪ t), dist a x + dist x b ≤ C + C
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} (s ∪ t)

Tactic:
refine ⟨C + C, fun a ha b hb => (dist_triangle a x b).trans ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} s
t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
C : ℝ
hC : ∀ z ∈ s ∪ t, dist x z ≤ C
a : α
ha : a ∈ s ∪ t
b : α
hb : b ∈ s ∪ t
⊢ dist a x + dist x b ≤ C + C

Tactic:
simpa only [dist_comm] using add_le_add (hC _ ha) (hC _ hb)

Premises used: add_le_add
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} s
t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
rcases : ∀ (Cs : ℝ) (hs : ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ Cs), ∃ (C : ℝ), ∀ z ∈ s ∪ t, dist x z ≤ C
⊢ ∃ (C : ℝ), ∀ z ∈ s ∪ t, dist x z ≤ C

Tactic:
rcases hs with ⟨Cs, hs⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
Cs : ℝ
hs : ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ Cs
rcases : ∀ (Ct : ℝ) (ht : ∀ ⦃x : α⦄, x ∈ t → ∀ ⦃y : α⦄, y ∈ t → dist x y ≤ Ct), ∃ (C : ℝ), ∀ z ∈ s ∪ t, dist x z ≤ C
⊢ ∃ (C : ℝ), ∀ z ∈ s ∪ t, dist x z ≤ C

Tactic:
rcases ht with ⟨Ct, ht⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s t : Set α
x : α
hx : x ∈ s
y : α
hy : y ∈ t
Cs : ℝ
hs : ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ Cs
Ct : ℝ
ht : ∀ ⦃x : α⦄, x ∈ t → ∀ ⦃y : α⦄, y ∈ t → dist x y ≤ Ct
⊢ ∃ (C : ℝ), ∀ z ∈ s ∪ t, dist x z ≤ C

Tactic:
⟨max Cs (dist x y + Ct), fun z hz => hz.elim
        (fun hz => (hs hx hz).trans (le_max_left _ _))
        (fun hz => (dist_triangle x y z).trans <|
          (add_le_add le_rfl (ht hy hz)).trans (le_max_right _ _))⟩

Premises used: le_max_right, le_rfl, add_le_add, HAdd.hAdd, Max.max, Exists.intro, LE.le.trans, Or.elim, le_max_left