awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α_1 : Type u
β_1 : Type v
X : Type u_1
inst : PseudoEMetricSpace α_1
γ : Type w
inst_1 : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
x : α
r : ℝ≥0∞
u : Set β
hu : IsOpen[n] u
uy :
  Eq (α := Set { x_1 : β // x_1 ∈ Metric.eball (f x) ∞ })
    (Subtype.val (p := fun (x_1 : β) ↦ x_1 ∈ Metric.eball (f x) ∞) ⁻¹' u) (Metric.eball (f x) ∞ ↓∩ Metric.eball (f x) r)
⊢ IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r)

Tactic:
exact ⟨f ⁻¹' u, isOpen_induced hu, by aesop (add simp [Set.ext_iff])⟩
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u_2
inst : TopologicalSpace α
m m' : WeakEMetricSpace α
h :
  Eq.{u_2 + 1} (α := EDist α) (WeakPseudoEMetricSpace.toEDist (τ := inst)) (WeakPseudoEMetricSpace.toEDist (τ := inst))
mk :
  ∀ [toWeakPseudoEMetricSpace : WeakPseudoEMetricSpace α] (eq_of_edist_eq_zero : ∀ {x y : α}, edist x y = 0 → x = y)
    (h :
      Eq.{u_2 + 1} (α := EDist α) (WeakPseudoEMetricSpace.toEDist (τ := inst))
        (WeakPseudoEMetricSpace.toEDist (τ := inst))),
    { toWeakPseudoEMetricSpace := toWeakPseudoEMetricSpace, eq_of_edist_eq_zero := @eq_of_edist_eq_zero :
        WeakEMetricSpace α } =
      m'
⊢ m = m'

Tactic:
cases m
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u_2
inst : TopologicalSpace α
m' : WeakEMetricSpace α
toWeakPseudoEMetricSpace : WeakPseudoEMetricSpace α
eq_of_edist_eq_zero : ∀ {x y : α}, edist x y = 0 → x = y
h :
  Eq.{u_2 + 1} (α := EDist α) (WeakPseudoEMetricSpace.toEDist (τ := inst)) (WeakPseudoEMetricSpace.toEDist (τ := inst))
mk :
  ∀ [toWeakPseudoEMetricSpace_1 : WeakPseudoEMetricSpace α] (eq_of_edist_eq_zero_1 : ∀ {x y : α}, edist x y = 0 → x = y)
    (h :
      Eq.{u_2 + 1} (α := EDist α) (WeakPseudoEMetricSpace.toEDist (τ := inst))
        (WeakPseudoEMetricSpace.toEDist (τ := inst))),
    { toWeakPseudoEMetricSpace := toWeakPseudoEMetricSpace, eq_of_edist_eq_zero := @eq_of_edist_eq_zero :
        WeakEMetricSpace α } =
      { toWeakPseudoEMetricSpace := toWeakPseudoEMetricSpace_1, eq_of_edist_eq_zero := @eq_of_edist_eq_zero_1 }
⊢ { toWeakPseudoEMetricSpace := toWeakPseudoEMetricSpace, eq_of_edist_eq_zero := @eq_of_edist_eq_zero :
      WeakEMetricSpace α } =
    m'

Tactic:
cases m'
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u_2
inst : TopologicalSpace α
toWeakPseudoEMetricSpace : WeakPseudoEMetricSpace α
eq_of_edist_eq_zero : ∀ {x y : α}, edist x y = 0 → x = y
toWeakPseudoEMetricSpace_1 : WeakPseudoEMetricSpace α
eq_of_edist_eq_zero_1 : ∀ {x y : α}, edist x y = 0 → x = y
h :
  Eq.{u_2 + 1} (α := EDist α) (WeakPseudoEMetricSpace.toEDist (τ := inst)) (WeakPseudoEMetricSpace.toEDist (τ := inst))
mk : toWeakPseudoEMetricSpace = toWeakPseudoEMetricSpace_1
⊢ { toWeakPseudoEMetricSpace := toWeakPseudoEMetricSpace, eq_of_edist_eq_zero := @eq_of_edist_eq_zero :
      WeakEMetricSpace α } =
    { toWeakPseudoEMetricSpace := toWeakPseudoEMetricSpace_1, eq_of_edist_eq_zero := @eq_of_edist_eq_zero_1 }

Tactic:
congr
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u_2
inst : TopologicalSpace α
toWeakPseudoEMetricSpace : WeakPseudoEMetricSpace α
eq_of_edist_eq_zero : ∀ {x y : α}, edist x y = 0 → x = y
toWeakPseudoEMetricSpace_1 : WeakPseudoEMetricSpace α
eq_of_edist_eq_zero_1 : ∀ {x y : α}, edist x y = 0 → x = y
h :
  Eq.{u_2 + 1} (α := EDist α) (WeakPseudoEMetricSpace.toEDist (τ := inst)) (WeakPseudoEMetricSpace.toEDist (τ := inst))
mk :
  Eq.{u_2 + 1} (α := EDist α) (WeakPseudoEMetricSpace.toEDist (τ := inst)) (WeakPseudoEMetricSpace.toEDist (τ := inst))
⊢ toWeakPseudoEMetricSpace = toWeakPseudoEMetricSpace_1

Tactic:
ext1
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u_2
inst : TopologicalSpace α
toWeakPseudoEMetricSpace : WeakPseudoEMetricSpace α
eq_of_edist_eq_zero : ∀ {x y : α}, edist x y = 0 → x = y
toWeakPseudoEMetricSpace_1 : WeakPseudoEMetricSpace α
eq_of_edist_eq_zero_1 : ∀ {x y : α}, edist x y = 0 → x = y
h :
  Eq.{u_2 + 1} (α := EDist α) (WeakPseudoEMetricSpace.toEDist (τ := inst)) (WeakPseudoEMetricSpace.toEDist (τ := inst))
⊢ Eq.{u_2 + 1} (α := EDist α) (WeakPseudoEMetricSpace.toEDist (τ := inst)) (WeakPseudoEMetricSpace.toEDist (τ := inst))

Tactic:
assumption
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
inst : PseudoEMetricSpace X
s : Set X
⊢ ediam s = sSup (image2 edist s s)

Tactic:
sSup_image2.symm

Premises used: sSup_image2, Metric.ediam, Eq.symm
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s : Set X
inst : PseudoEMetricSpace X
d : ℝ≥0∞
⊢ ediam s ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d

Tactic:
simp only [ediam, iSup_le_iff]

Premises used: Metric.ediam, iSup_le_iff
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
α : Type u_1
X : Type u_2
inst : PseudoEMetricSpace X
d : ℝ≥0∞
f : α → X
s : Set α
⊢ ediam (f '' s) ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) ≤ d

Tactic:
simp only [ediam_le_iff, forall_mem_image]

Premises used: Metric.ediam_le_iff, Set.forall_mem_image
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s : Set X
x y : X
inst : PseudoEMetricSpace X
d : ℝ≥0∞
hx : x ∈ s
hy : y ∈ s
hd : ediam s ≤ d
⊢ edist x y ≤ d

Tactic:
ediam_le_iff.1 hd x hx y hy

Premises used: Iff.mp, Metric.ediam_le_iff
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s : Set X
x y : X
inst : PseudoEMetricSpace X
hx : x ∈ s
hy : y ∈ s
⊢ edist x y ≤ ediam s

Tactic:
edist_le_of_ediam_le hx hy le_rfl

Premises used: le_rfl, Metric.edist_le_of_ediam_le
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s : Set X
inst : PseudoEMetricSpace X
d : ℝ≥0∞
h : ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d
⊢ ediam s ≤ d

Tactic:
ediam_le_iff.2 h

Premises used: Iff.mpr, Metric.ediam_le_iff
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s : Set X
inst : PseudoEMetricSpace X
hs : s.Subsingleton
⊢ ediam s = 0

Tactic:
nonpos_iff_eq_zero.1 <| ediam_le fun _x hx y hy => (hs hx hy).symm ▸ edist_self y ▸ le_rfl

Premises used: le_rfl, Eq.rec, PseudoEMetricSpace.edist_self, Metric.ediam_le, Iff.mp, Eq.symm, nonpos_iff_eq_zero
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
inst : PseudoEMetricSpace X
⊢ ediam.{u_2} (X := X) ∅ = 0

Tactic:
ediam_subsingleton subsingleton_empty

Premises used: Metric.ediam_subsingleton, Set.subsingleton_empty
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
x : X
inst : PseudoEMetricSpace X
⊢ ediam (X := X) {x} = 0

Tactic:
ediam_subsingleton subsingleton_singleton

Premises used: Metric.ediam_subsingleton, Set.subsingleton_singleton
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
inst : PseudoEMetricSpace X
inst_1 : One X
⊢ ediam.{u_2} (X := X) 1 = 0

Tactic:
ediam_singleton

Premises used: Metric.ediam_singleton
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
inst : PseudoEMetricSpace X
ι : Type u_3
o : Option ι
s : ι → Set X
none :
  ediam.{u_2} (X := X) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Option ι) Option.none i), s i) =
    ⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Option ι) Option.none i), ediam (s i)
some : ∀ (val : ι), ediam.{u_2} (X := X) (⋃ i ∈ Option.some val, s i) = ⨆ i ∈ Option.some val, ediam (s i)
⊢ ediam.{u_2} (X := X) (⋃ i ∈ o, s i) = ⨆ i ∈ o, ediam (s i)

Tactic:
cases o
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
inst : PseudoEMetricSpace X
ι : Type u_3
s : ι → Set X
⊢ ediam.{u_2} (X := X) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Option ι) none i), s i) =
    ⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Option ι) none i), ediam (s i)

Tactic:
simp
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
inst : PseudoEMetricSpace X
ι : Type u_3
s : ι → Set X
val : ι
⊢ ediam.{u_2} (X := X) (⋃ i ∈ some val, s i) = ⨆ i ∈ some val, ediam (s i)

Tactic:
simp
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s : Set X
x : X
inst : PseudoEMetricSpace X
d : ℝ≥0∞
⊢ ediam (insert x s) ≤ d ↔ max (⨆ y ∈ s, edist x y) (ediam s) ≤ d

Tactic:
simp +contextual [ediam_le_iff, edist_comm]

Premises used: PseudoEMetricSpace.edist_comm, Metric.ediam_le_iff
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
x y : X
inst : PseudoEMetricSpace X
⊢ ediam (X := X) {x, y} = edist x y

Tactic:
simp [ediam_insert]

Premises used: Metric.ediam_insert
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
x y z : X
inst : PseudoEMetricSpace X
⊢ ediam (X := X) {x, y, z} = max (max (edist x y) (edist x z)) (edist y z)

Tactic:
simp only [ediam_insert, iSup_insert, iSup_singleton, ediam_singleton, max_zero]

Premises used: iSup_insert, max_zero, iSup_singleton, Metric.ediam_singleton, Metric.ediam_insert
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
inst : PseudoEMetricSpace X
h : s ⊆ t
⊢ ediam s ≤ ediam t

Tactic:
ediam_le fun _x hx _y hy => edist_le_ediam_of_mem (h hx) (h hy)

Premises used: Metric.edist_le_ediam_of_mem, Metric.ediam_le
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
a : X
ha : a ∈ s
b : X
hb : b ∈ t
h₁ : edist a x ≤ ediam s
h₂ : edist y b ≤ ediam t
⊢ edist a x + edist x y + edist y b ≤ ediam s + edist x y + ediam t

Tactic:
gcongr
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
a : X
ha : a ∈ s
b : X
hb : b ∈ t
⊢ edist a x ≤ ediam s

Tactic:
edist_le_ediam_of_mem ha xs

Premises used: Metric.edist_le_ediam_of_mem
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
a : X
ha : a ∈ s
b : X
hb : b ∈ t
⊢ edist y b ≤ ediam t

Tactic:
edist_le_ediam_of_mem yt hb

Premises used: Metric.edist_le_ediam_of_mem
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
a : X
ha : a ∈ s
b : X
hb : b ∈ t
⊢ edist a x ≤ ediam s

Tactic:
exacts [edist_le_ediam_of_mem ha xs, edist_le_ediam_of_mem yt hb]

Premises used: Metric.edist_le_ediam_of_mem
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
⊢ ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t

Tactic:
have A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t := fun a ha b hb =>
    calc
      edist a b ≤ edist a x + edist x y + edist y b := edist_triangle4 _ _ _ _
      _ ≤ ediam s + edist x y + ediam t := by
        gcongr
        exacts [edist_le_ediam_of_mem ha xs, edist_le_ediam_of_mem yt hb]
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
⊢ ediam (s ∪ t) ≤ ediam s + edist x y + ediam t

Tactic:
ediam_le fun a ha b hb => ?_

Premises used: Metric.ediam_le
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
refine : ∀ (a : X) (ha : a ∈ s ∪ t) (b : X) (hb : b ∈ s ∪ t), edist a b ≤ ediam s + edist x y + ediam t
⊢ ediam (s ∪ t) ≤ ediam s + edist x y + ediam t

Tactic:
refine ediam_le fun a ha b hb => ?_

Premises used: Metric.ediam_le
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a : X
ha : a ∈ s ∪ t
b : X
hb : b ∈ s ∪ t
rw : ∀ (ha : a ∈ s ∨ a ∈ t) (b : X) (hb : b ∈ s ∨ b ∈ t), edist a b ≤ ediam s + edist x y + ediam t
⊢ edist a b ≤ ediam s + edist x y + ediam t

Tactic:
rw [mem_union] at ha hb

Premises used: Set.mem_union
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a : X
ha : a ∈ s ∨ a ∈ t
b : X
hb : b ∈ s ∨ b ∈ t
inl : ∀ (h'a : a ∈ s), edist a b ≤ ediam s + edist x y + ediam t
inr : ∀ (h'a : a ∈ t), edist a b ≤ ediam s + edist x y + ediam t
⊢ edist a b ≤ ediam s + edist x y + ediam t

Tactic:
rcases ha with h'a | h'a
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
hb : b ∈ s ∨ b ∈ t
h'a : a ∈ s
inl : ∀ (h'b : b ∈ s), edist a b ≤ ediam s + edist x y + ediam t
inl₁ : ∀ (h'b : b ∈ t), edist a b ≤ ediam s + edist x y + ediam t
⊢ edist a b ≤ ediam s + edist x y + ediam t

Tactic:
rcases hb with h'b | h'b
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
hb : b ∈ s ∨ b ∈ t
h'a : a ∈ t
inr : ∀ (h'b : b ∈ s), edist a b ≤ ediam s + edist x y + ediam t
inr₁ : ∀ (h'b : b ∈ t), edist a b ≤ ediam s + edist x y + ediam t
⊢ edist a b ≤ ediam s + edist x y + ediam t

Tactic:
rcases hb with h'b | h'b
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ s
h'b : b ∈ s
⊢ edist a b ≤ ediam s

Tactic:
edist_le_ediam_of_mem h'a h'b

Premises used: Metric.edist_le_ediam_of_mem
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ s
h'b : b ∈ s
⊢ ediam s ≤ ediam s + (edist x y + ediam t)

Tactic:
le_self_add

Premises used: le_self_add
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ s
h'b : b ∈ s
⊢ ediam s + (edist x y + ediam t) = ediam s + edist x y + ediam t

Tactic:
(add_assoc _ _ _).symm

Premises used: add_assoc, Eq.symm
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ s
h'b : b ∈ s
⊢ edist a b ≤ ediam s + edist x y + ediam t

Tactic:
calc
      edist a b ≤ ediam s := edist_le_ediam_of_mem h'a h'b
      _ ≤ ediam s + (edist x y + ediam t) := le_self_add
      _ = ediam s + edist x y + ediam t := (add_assoc _ _ _).symm

Premises used: add_assoc, Metric.edist_le_ediam_of_mem, Metric.ediam, HAdd.hAdd, EDist.edist, Eq.symm, le_self_add
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ s
h'b : b ∈ t
⊢ edist a b ≤ ediam s + edist x y + ediam t

Tactic:
A a h'a b h'b
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ s
h'b : b ∈ t
⊢ edist a b ≤ ediam s + edist x y + ediam t

Tactic:
exact A a h'a b h'b
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ t
h'b : b ∈ s
⊢ edist b a ≤ ediam s + edist x y + ediam t

Tactic:
have Z := A b h'b a h'a
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ t
h'b : b ∈ s
Z : edist b a ≤ ediam s + edist x y + ediam t
inr inr₁ inr₂ inr₃ : ∀ (Z : edist a b ≤ ediam s + edist x y + ediam t), edist a b ≤ ediam s + edist x y + ediam t
⊢ edist a b ≤ ediam s + edist x y + ediam t

Tactic:
rwa [edist_comm] at Z

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ t
h'b : b ∈ t
⊢ edist a b ≤ ediam t

Tactic:
edist_le_ediam_of_mem h'a h'b

Premises used: Metric.edist_le_ediam_of_mem
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ t
h'b : b ∈ t
⊢ ediam t ≤ ediam s + edist x y + ediam t

Tactic:
le_add_self

Premises used: le_add_self
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ t
h'b : b ∈ t
⊢ edist a b ≤ ediam s + edist x y + ediam t

Tactic:
calc
      edist a b ≤ ediam t := edist_le_ediam_of_mem h'a h'b
      _ ≤ ediam s + edist x y + ediam t := le_add_self

Premises used: Metric.edist_le_ediam_of_mem, Metric.ediam, EDist.edist, le_add_self
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
inst : PseudoEMetricSpace X
h : (s ∩ t).Nonempty
let : ∀ (x : X) (xs : x ∈ s) (xt : x ∈ t), ediam (s ∪ t) ≤ ediam s + ediam t
⊢ ediam (s ∪ t) ≤ ediam s + ediam t

Tactic:
let ⟨x, ⟨xs, xt⟩⟩ := h
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s t : Set X
inst : PseudoEMetricSpace X
h : (s ∩ t).Nonempty
x : X
xs : x ∈ s
xt : x ∈ t
⊢ ediam (s ∪ t) ≤ ediam s + ediam t

Tactic:
simpa using ediam_union_le_add_edist xs xt

Premises used: Metric.ediam_union_le_add_edist
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
x : X
inst : PseudoEMetricSpace X
r : ℝ≥0∞
⊢ ediam (closedEBall x r) ≤ 2 * r

Tactic:
ediam_le fun a ha b hb =>
    calc
      edist a b ≤ edist a x + edist b x := edist_triangle_right _ _ _
      _ ≤ r + r := add_le_add ha hb
      _ = 2 * r := (two_mul r).symm

Premises used: Trans.trans, add_le_add, two_mul, edist_triangle_right, Metric.ediam_le, Eq.symm
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
x : X
inst : PseudoEMetricSpace X
r : ℝ≥0∞
⊢ ediam (eball x r) ≤ 2 * r

Tactic:
le_trans (ediam_mono eball_subset_closedEBall) ediam_closedEBall_le

Premises used: Metric.ediam_closedEBall_le, Metric.eball_subset_closedEBall, Metric.ediam_mono, le_trans
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
ι : Type u_3
X : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → PseudoEMetricSpace (X i)
s : (i : ι) → Set (X i)
c : ℝ≥0∞
h : ∀ (b : ι), ediam (s b) ≤ c
⊢ ediam (Set.pi (α := X) univ s) ≤ c

Tactic:
ediam_le fun x hx y hy => edist_pi_le_iff.mpr ?_

Premises used: Iff.mpr, Metric.ediam_le, edist_pi_le_iff
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
ι : Type u_3
X : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → PseudoEMetricSpace (X i)
s : (i : ι) → Set (X i)
c : ℝ≥0∞
h : ∀ (b : ι), ediam (s b) ≤ c
refine :
  ∀ (x : (i : ι) → X i) (hx : x ∈ Set.pi (α := X) univ s) (y : (i : ι) → X i) (hy : y ∈ Set.pi (α := X) univ s) (b : ι),
    edist (x b) (y b) ≤ c
⊢ ediam (Set.pi (α := X) univ s) ≤ c

Tactic:
refine ediam_le fun x hx y hy => edist_pi_le_iff.mpr ?_

Premises used: Metric.ediam_le
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
ι : Type u_3
X : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → PseudoEMetricSpace (X i)
s : (i : ι) → Set (X i)
c : ℝ≥0∞
h : ∀ (b : ι), ediam (s b) ≤ c
x : (i : ι) → X i
hx : x ∈ Set.pi (α := X) univ s
y : (i : ι) → X i
hy : y ∈ Set.pi (α := X) univ s
rw : ∀ (hx : ∀ (i : ι), x i ∈ s i) (y : (i : ι) → X i) (hy : ∀ (i : ι), y i ∈ s i) (b : ι), edist (x b) (y b) ≤ c
⊢ ∀ (b : ι), edist (x b) (y b) ≤ c

Tactic:
rw [mem_univ_pi] at hx hy

Premises used: Set.mem_univ_pi
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
ι : Type u_3
X : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → PseudoEMetricSpace (X i)
s : (i : ι) → Set (X i)
c : ℝ≥0∞
h : ∀ (b : ι), ediam (s b) ≤ c
x : (i : ι) → X i
hx : ∀ (i : ι), x i ∈ s i
y : (i : ι) → X i
hy : ∀ (i : ι), y i ∈ s i
⊢ ∀ (b : ι), edist (x b) (y b) ≤ c

Tactic:
fun b => ediam_le_iff.1 (h b) (x b) (hx b) (y b) (hy b)

Premises used: Iff.mp, Metric.ediam_le_iff
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
ι : Type u_3
X : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → PseudoEMetricSpace (X i)
s : (i : ι) → Set (X i)
c : ℝ≥0∞
h : ∀ (b : ι), ediam (s b) ≤ c
x : (i : ι) → X i
hx : ∀ (i : ι), x i ∈ s i
y : (i : ι) → X i
hy : ∀ (i : ι), y i ∈ s i
⊢ ∀ (b : ι), edist (x b) (y b) ≤ c

Tactic:
exact fun b => ediam_le_iff.1 (h b) (x b) (hx b) (y b) (hy b)

Premises used: Iff.mp, Metric.ediam_le_iff
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s : Set X
inst : EMetricSpace X
⊢ ediam s = 0 ↔ s.Subsingleton

Tactic:
⟨fun h _x hx _y hy => edist_le_zero.1 <| h ▸ edist_le_ediam_of_mem hx hy, ediam_subsingleton⟩

Premises used: Metric.ediam_subsingleton, edist_le_zero, Iff.intro, Iff.mp
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s : Set X
inst : EMetricSpace X
⊢ 0 < ediam s ↔ s.Nontrivial

Tactic:
simp only [pos_iff_ne_zero, Ne, ediam_eq_zero_iff, Set.not_subsingleton_iff]

Premises used: Set.not_subsingleton_iff, Ne, Metric.ediam_eq_zero_iff, pos_iff_ne_zero
-- Module: Mathlib.Topology.EMetricSpace.Diam
Goal:
X : Type u_2
s : Set X
inst : EMetricSpace X
⊢ 0 < ediam s ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y

Tactic:
simp only [ediam_pos_iff, Set.Nontrivial]

Premises used: Metric.ediam_pos_iff, Set.Nontrivial
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
⊢ LipschitzOnWith K f ∅

Tactic:
fun _ => False.elim

Premises used: Set.Mem, False.elim, LipschitzOnWith
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
⊢ LocallyLipschitzOn ∅ f

Tactic:
fun _ ↦ False.elim

Premises used: Set.Mem, False.elim, LocallyLipschitzOn
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
s t : Set α
f : α → β
hf : LipschitzOnWith K f t
h : s ⊆ t
⊢ LipschitzOnWith K f s

Tactic:
fun _x x_in _y y_in => hf (h x_in) (h y_in)

Premises used: LipschitzOnWith
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
s t : Set α
f : α → β
hf : LocallyLipschitzOn t f
h : s ⊆ t
x : α
hx : x ∈ s
obtain :
  ∀ (K : ℝ≥0) (u : Set α) (hu : u ∈ 𝓝[t] x) (hfu : LipschitzOnWith K f u),
    ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
obtain ⟨K, u, hu, hfu⟩ := hf (h hx)
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
s t : Set α
f : α → β
hf : LocallyLipschitzOn t f
h : s ⊆ t
x : α
hx : x ∈ s
K : ℝ≥0
u : Set α
hu : u ∈ 𝓝[t] x
hfu : LipschitzOnWith K f u
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
⟨K, u, nhdsWithin_mono _ h hu, hfu⟩

Premises used: And.intro, Exists.intro, nhdsWithin_mono
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
s t : Set α
f : α → β
hf : LocallyLipschitzOn t f
h : s ⊆ t
x : α
hx : x ∈ s
K : ℝ≥0
u : Set α
hu : u ∈ 𝓝[t] x
hfu : LipschitzOnWith K f u
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
exact ⟨K, u, nhdsWithin_mono _ h hu, hfu⟩
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
⊢ LipschitzOnWith K f univ ↔ LipschitzWith K f

Tactic:
simp [LipschitzOnWith, LipschitzWith]

Premises used: LipschitzWith, LipschitzOnWith