awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
ht : t.Nonempty
this : hausdorffEDist s t ≤ ENNReal.ofReal r
⊢ hausdorffDist s t ≤ r

Tactic:
ENNReal.toReal_le_of_le_ofReal hr this

Premises used: Metric.hausdorffDist, ENNReal.toReal_le_of_le_ofReal
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
ht : t.Nonempty
this : hausdorffEDist s t ≤ ENNReal.ofReal r
⊢ hausdorffDist s t ≤ r

Tactic:
exact ENNReal.toReal_le_of_le_ofReal hr this

Premises used: ENNReal.toReal_le_of_le_ofReal
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
H1₁ : ∀ x ∈ s, infDist x t ≤ r
H2₁ : ∀ x ∈ t, infDist x s ≤ r
⊢ hausdorffDist s t ≤ r

Tactic:
apply hausdorffDist_le_of_infDist hr

Premises used: Metric.hausdorffDist_le_of_infDist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
x : α
xs : x ∈ s
H1₁ : ∀ (y : α) (yt : y ∈ t) (hy : dist x y ≤ r), infDist x t ≤ r
⊢ infDist x t ≤ r

Tactic:
rcases H1 x xs with ⟨y, yt, hy⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
x : α
xs : x ∈ s
y : α
yt : y ∈ t
hy : dist x y ≤ r
⊢ infDist x t ≤ r

Tactic:
le_trans (infDist_le_dist_of_mem yt) hy

Premises used: Metric.infDist_le_dist_of_mem, le_trans
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
x : α
xs : x ∈ s
y : α
yt : y ∈ t
hy : dist x y ≤ r
⊢ infDist x t ≤ r

Tactic:
exact le_trans (infDist_le_dist_of_mem yt) hy

Premises used: Metric.infDist_le_dist_of_mem, le_trans
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
x : α
xt : x ∈ t
H2₁ : ∀ (y : α) (ys : y ∈ s) (hy : dist x y ≤ r), infDist x s ≤ r
⊢ infDist x s ≤ r

Tactic:
rcases H2 x xt with ⟨y, ys, hy⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
x : α
xt : x ∈ t
y : α
ys : y ∈ s
hy : dist x y ≤ r
⊢ infDist x s ≤ r

Tactic:
le_trans (infDist_le_dist_of_mem ys) hy

Premises used: Metric.infDist_le_dist_of_mem, le_trans
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
x : α
xt : x ∈ t
y : α
ys : y ∈ s
hy : dist x y ≤ r
⊢ infDist x s ≤ r

Tactic:
exact le_trans (infDist_le_dist_of_mem ys) hy

Premises used: Metric.infDist_le_dist_of_mem, le_trans
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
hs : s.Nonempty
bs : Bornology.IsBounded s
ht : t.Nonempty
bt : Bornology.IsBounded t
rcases : ∀ (x : α) (xs : x ∈ s), hausdorffDist s t ≤ diam (s ∪ t)
⊢ hausdorffDist s t ≤ diam (s ∪ t)

Tactic:
rcases hs with ⟨x, xs⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
ht : t.Nonempty
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
rcases : ∀ (y : α) (yt : y ∈ t), hausdorffDist s t ≤ diam (s ∪ t)
⊢ hausdorffDist s t ≤ diam (s ∪ t)

Tactic:
rcases ht with ⟨y, yt⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ hausdorffDist s t ≤ diam (s ∪ t)

Tactic:
hausdorffDist_le_of_mem_dist diam_nonneg ?_ ?_

Premises used: Metric.hausdorffDist_le_of_mem_dist, Metric.diam_nonneg
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
refine_1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ diam (s ∪ t)
refine_2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ diam (s ∪ t)
⊢ hausdorffDist s t ≤ diam (s ∪ t)

Tactic:
refine hausdorffDist_le_of_mem_dist diam_nonneg ?_ ?_

Premises used: Metric.hausdorffDist_le_of_mem_dist, Metric.diam_nonneg
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ diam (s ∪ t)

Tactic:
fun z hz => ⟨y, yt, dist_le_diam_of_mem (bs.union bt) (subset_union_left hz)
      (subset_union_right yt)⟩

Premises used: Set.subset_union_right, Set.subset_union_left, Metric.dist_le_diam_of_mem, And.intro, Exists.intro, Bornology.IsBounded.union
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ diam (s ∪ t)

Tactic:
exact fun z hz => ⟨y, yt, dist_le_diam_of_mem (bs.union bt) (subset_union_left hz)
      (subset_union_right yt)⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ diam (s ∪ t)

Tactic:
fun z hz => ⟨x, xs, dist_le_diam_of_mem (bs.union bt) (subset_union_right hz)
      (subset_union_left xs)⟩

Premises used: Set.subset_union_right, Set.subset_union_left, Metric.dist_le_diam_of_mem, And.intro, Exists.intro, Bornology.IsBounded.union
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ diam (s ∪ t)

Tactic:
exact fun z hz => ⟨x, xs, dist_le_diam_of_mem (bs.union bt) (subset_union_right hz)
      (subset_union_left xs)⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
hx : x ∈ s
fin : hausdorffEDist s t ≠ ∞
⊢ infDist x t ≤ hausdorffDist s t

Tactic:
toReal_mono fin (infEDist_le_hausdorffEDist_of_mem hx)

Premises used: Metric.hausdorffDist, Metric.infEDist_le_hausdorffEDist_of_mem, Metric.infDist, ENNReal.toReal_mono
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
⊢ 0 < r

Tactic:
have r0 : 0 < r := lt_of_le_of_lt hausdorffDist_nonneg H
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
rwa :
  ∀ (H : (hausdorffEDist s t).toReal < r) (fin : hausdorffEDist s t ≠ ∞) (r0 : 0 < r),
    hausdorffEDist s t < ENNReal.ofReal r
rwa₁ :
  ∀ (H : (hausdorffEDist s t).toReal < (ENNReal.ofReal r).toReal) (fin : hausdorffEDist s t ≠ ∞) (r0 : 0 < r),
    hausdorffEDist s t < ENNReal.ofReal r
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (H : hausdorffEDist s t < ENNReal.ofReal r) (fin : hausdorffEDist s t ≠ ∞) (r0 : 0 < r),
    hausdorffEDist s t < ENNReal.ofReal r
⊢ hausdorffEDist s t < ENNReal.ofReal r

Tactic:
rwa [hausdorffDist, ← ENNReal.toReal_ofReal (le_of_lt r0),
      ENNReal.toReal_lt_toReal fin ENNReal.ofReal_ne_top] at H

Premises used: Metric.hausdorffDist, le_of_lt, ENNReal.toReal_ofReal, ENNReal.toReal_lt_toReal, ENNReal.ofReal_ne_top
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
⊢ hausdorffEDist s t < ENNReal.ofReal r

Tactic:
have : hausdorffEDist s t < ENNReal.ofReal r := by
    rwa [hausdorffDist, ← ENNReal.toReal_ofReal (le_of_lt r0),
      ENNReal.toReal_lt_toReal fin ENNReal.ofReal_ne_top] at H
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
this : hausdorffEDist s t < ENNReal.ofReal r
rcases : ∀ (y : α) (hy : y ∈ t) (yr : edist x y < ENNReal.ofReal r), ∃ y ∈ t, dist x y < r
⊢ ∃ y ∈ t, dist x y < r

Tactic:
rcases exists_edist_lt_of_hausdorffEDist_lt h this with ⟨y, hy, yr⟩

Premises used: Metric.exists_edist_lt_of_hausdorffEDist_lt
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
this : hausdorffEDist s t < ENNReal.ofReal r
y : α
hy : y ∈ t
yr : edist x y < ENNReal.ofReal r
⊢ dist x y < r

Tactic:
rw [edist_dist, ENNReal.ofReal_lt_ofReal_iff r0] at yr

Premises used: edist_dist, ENNReal.ofReal_lt_ofReal_iff
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
this : hausdorffEDist s t < ENNReal.ofReal r
y : α
hy : y ∈ t
yr : dist x y < r
⊢ ∃ y ∈ t, dist x y < r

Tactic:
⟨y, hy, yr⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
this : hausdorffEDist s t < ENNReal.ofReal r
y : α
hy : y ∈ t
yr : dist x y < r
⊢ ∃ y ∈ t, dist x y < r

Tactic:
exact ⟨y, hy, yr⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
y : α
r : ℝ
h : y ∈ t
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
⊢ hausdorffDist t s < r

Tactic:
rw [hausdorffDist_comm] at H

Premises used: Metric.hausdorffDist_comm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
y : α
r : ℝ
h : y ∈ t
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
H₁ : hausdorffDist t s < r
⊢ hausdorffEDist s t ≠ ∞

Tactic:
rw [hausdorffDist_comm] at H

Premises used: Metric.hausdorffDist_comm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
y : α
r : ℝ
h : y ∈ t
H : hausdorffDist t s < r
fin : hausdorffEDist s t ≠ ∞
⊢ hausdorffEDist t s ≠ ∞

Tactic:
rw [hausdorffEDist_comm] at fin

Premises used: Metric.hausdorffEDist_comm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
y : α
r : ℝ
h : y ∈ t
H : hausdorffDist t s < r
fin : hausdorffEDist t s ≠ ∞
⊢ ∃ x ∈ s, dist x y < r

Tactic:
simpa [dist_comm] using exists_dist_lt_of_hausdorffDist_lt h H fin

Premises used: dist_comm, Metric.exists_dist_lt_of_hausdorffDist_lt
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEDist s t ≠ ∞
⊢ infDist x t ≤ infDist x s + hausdorffDist s t

Tactic:
toReal_le_add' infEDist_le_infEDist_add_hausdorffEDist (fun h ↦ ?_) (flip absurd fin)

Premises used: Metric.hausdorffDist, Metric.infDist, flip, absurd, Metric.infEDist_le_infEDist_add_hausdorffEDist, ENNReal.toReal_le_add'
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEDist s t ≠ ∞
refine : ∀ (h : infEDist x s = ∞), infEDist x t = ∞
⊢ infDist x t ≤ infDist x s + hausdorffDist s t

Tactic:
refine toReal_le_add' infEDist_le_infEDist_add_hausdorffEDist (fun h ↦ ?_) (flip absurd fin)

Premises used: flip, absurd, Metric.infEDist_le_infEDist_add_hausdorffEDist, ENNReal.toReal_le_add'
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEDist s t ≠ ∞
h : infEDist x s = ∞
rw : ∀ (h : ¬s.Nonempty), ¬t.Nonempty
⊢ infEDist x t = ∞

Tactic:
rw [infEDist_eq_top_iff, ← not_nonempty_iff_eq_empty] at h ⊢

Premises used: Set.not_nonempty_iff_eq_empty, Metric.infEDist_eq_top_iff
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEDist s t ≠ ∞
h : ¬s.Nonempty
⊢ hausdorffEDist t s ≠ ∞

Tactic:
rw [hausdorffEDist_comm] at fin

Premises used: Metric.hausdorffEDist_comm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEDist s t ≠ ∞
h : ¬s.Nonempty
fin₁ : hausdorffEDist t s ≠ ∞
⊢ ¬s.Nonempty

Tactic:
rw [hausdorffEDist_comm] at fin

Premises used: Metric.hausdorffEDist_comm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEDist t s ≠ ∞
h : ¬s.Nonempty
⊢ ¬t.Nonempty

Tactic:
mt (nonempty_of_hausdorffEDist_ne_top · fin) h

Premises used: Metric.nonempty_of_hausdorffEDist_ne_top, mt
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEDist t s ≠ ∞
h : ¬s.Nonempty
⊢ ¬t.Nonempty

Tactic:
exact mt (nonempty_of_hausdorffEDist_ne_top · fin) h

Premises used: Metric.nonempty_of_hausdorffEDist_ne_top, mt
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
s t : Set α
Φ : α → β
h : Isometry Φ
⊢ hausdorffDist (Φ '' s) (Φ '' t) = hausdorffDist s t

Tactic:
simp [hausdorffDist, hausdorffEDist_image h]

Premises used: Metric.hausdorffDist, Metric.hausdorffEDist_image
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist s t ≠ ∞
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u

Tactic:
toReal_le_add' hausdorffEDist_triangle (flip absurd fin) (not_imp_not.1 fun h ↦ ?_)

Premises used: Metric.hausdorffDist, flip, absurd, Metric.hausdorffEDist_triangle, Iff.mp, ENNReal.toReal_le_add', not_imp_not
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist s t ≠ ∞
refine : ∀ (h : ¬hausdorffEDist s u = ∞), ¬hausdorffEDist t u = ∞
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u

Tactic:
refine toReal_le_add' hausdorffEDist_triangle (flip absurd fin) (not_imp_not.1 fun h ↦ ?_)

Premises used: flip, absurd, Metric.hausdorffEDist_triangle, Iff.mp, ENNReal.toReal_le_add', not_imp_not
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist s t ≠ ∞
h : ¬hausdorffEDist s u = ∞
⊢ hausdorffEDist t s ≠ ∞

Tactic:
rw [hausdorffEDist_comm] at fin

Premises used: Metric.hausdorffEDist_comm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist s t ≠ ∞
h : ¬hausdorffEDist s u = ∞
fin₁ : hausdorffEDist t s ≠ ∞
⊢ ¬hausdorffEDist s u = ∞

Tactic:
rw [hausdorffEDist_comm] at fin

Premises used: Metric.hausdorffEDist_comm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist t s ≠ ∞
h : ¬hausdorffEDist s u = ∞
⊢ ¬hausdorffEDist t u = ∞

Tactic:
ne_top_of_le_ne_top (add_ne_top.2 ⟨fin, h⟩) hausdorffEDist_triangle

Premises used: Iff.mpr, ne_top_of_le_ne_top, Metric.hausdorffEDist_triangle, And.intro, ENNReal.add_ne_top
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist t s ≠ ∞
h : ¬hausdorffEDist s u = ∞
⊢ ¬hausdorffEDist t u = ∞

Tactic:
exact ne_top_of_le_ne_top (add_ne_top.2 ⟨fin, h⟩) hausdorffEDist_triangle

Premises used: Iff.mpr, ne_top_of_le_ne_top, Metric.hausdorffEDist_triangle, And.intro, ENNReal.add_ne_top
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist t u ≠ ∞
⊢ hausdorffEDist u t ≠ ∞

Tactic:
rw [hausdorffEDist_comm] at fin

Premises used: Metric.hausdorffEDist_comm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist u t ≠ ∞
⊢ hausdorffDist u s ≤ hausdorffDist u t + hausdorffDist t s

Tactic:
have I : hausdorffDist u s ≤ hausdorffDist u t + hausdorffDist t s :=
    hausdorffDist_triangle fin
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist u t ≠ ∞
I : hausdorffDist u s ≤ hausdorffDist u t + hausdorffDist t s
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u

Tactic:
simpa [add_comm, hausdorffDist_comm] using I

Premises used: Metric.hausdorffDist_comm, add_comm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
⊢ hausdorffDist s (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) = 0

Tactic:
simp [hausdorffDist]

Premises used: Metric.hausdorffDist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
⊢ hausdorffDist (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) t = hausdorffDist s t

Tactic:
simp [hausdorffDist]

Premises used: Metric.hausdorffDist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
⊢ hausdorffDist s (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t) = hausdorffDist s t

Tactic:
simp [hausdorffDist]

Premises used: Metric.hausdorffDist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
⊢ hausdorffDist (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)
      (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t) =
    hausdorffDist s t

Tactic:
simp [hausdorffDist]

Premises used: Metric.hausdorffDist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
fin : hausdorffEDist s t ≠ ∞
⊢ hausdorffDist s t = 0 ↔
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s =
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t

Tactic:
simp [← hausdorffEDist_zero_iff_closure_eq_closure, hausdorffDist,
    ENNReal.toReal_eq_zero_iff, fin]

Premises used: Metric.hausdorffDist, Metric.hausdorffEDist_zero_iff_closure_eq_closure, ENNReal.toReal_eq_zero_iff
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
fin : hausdorffEDist s t ≠ ∞
⊢ hausdorffDist s t = 0 ↔ s = t

Tactic:
simp [← _root_.IsClosed.hausdorffEDist_zero_iff hs ht, hausdorffDist, ENNReal.toReal_eq_zero_iff,
    fin]

Premises used: Metric.hausdorffDist, IsClosed.hausdorffEDist_zero_iff, ENNReal.toReal_eq_zero_iff
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
rw : (hausdorffEDist (α := α) {x} {y}).toReal = dist x y
rw₁ : (edist x y).toReal = dist x y
rw₂ rw₃ : (edist x y).toReal = (edist x y).toReal
⊢ hausdorffDist (α := α) {x} {y} = dist x y

Tactic:
rw [hausdorffDist, hausdorffEDist_singleton, dist_edist]

Premises used: Metric.hausdorffDist, Metric.hausdorffEDist_singleton, dist_edist
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
⊢ HolderOnWith C r f ∅

Tactic:
fun _ hx => hx.elim

Premises used: False.elim, HolderOnWith
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
x : X
⊢ HolderOnWith C r f {x}

Tactic:
simp [HolderOnWith]

Premises used: HolderOnWith
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
s : Set X
hs : s.Subsingleton
C r : ℝ≥0
f : X → Y
⊢ HolderOnWith C r f s

Tactic:
hs.induction_on (holderOnWith_empty C r f) (holderOnWith_singleton C r f)

Premises used: Set.Subsingleton.induction_on, holderOnWith_empty, holderOnWith_singleton
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
⊢ HolderOnWith C r f univ ↔ HolderWith C r f

Tactic:
simp only [HolderOnWith, HolderWith, mem_univ, true_imp_iff]

Premises used: true_imp_iff, Set.mem_univ, HolderWith, HolderOnWith
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
C : ℝ≥0
f : X → Y
s : Set X
⊢ HolderOnWith C 1 f s ↔ LipschitzOnWith C f s

Tactic:
simp only [HolderOnWith, LipschitzOnWith, NNReal.coe_one, ENNReal.rpow_one]

Premises used: ENNReal.rpow_one, LipschitzOnWith, HolderOnWith, NNReal.coe_one
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
C : ℝ≥0
f : X → Y
⊢ HolderWith C 1 f ↔ LipschitzWith C f

Tactic:
holderOnWith_univ.symm.trans <| holderOnWith_one.trans lipschitzOnWith_univ

Premises used: holderOnWith_univ, lipschitzOnWith_univ, Iff.trans, holderOnWith_one, Iff.symm
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
⊢ HolderWith.{u_1, u_1} (X := X) 1 1 id

Tactic:
LipschitzWith.id.holderWith

Premises used: LipschitzWith.id, LipschitzWith.holderWith
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
h : HolderWith C r f
s : Set X
⊢ HolderOnWith C r f s

Tactic:
fun x _ y _ => h x y

Premises used: HolderOnWith
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
x y : X
hx : x ∈ s
hy : y ∈ s
⊢ edist (f x) (f y) ≤ (↑C : ℝ≥0∞) * edist x y ^ (↑r : ℝ)

Tactic:
h x hx y hy
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
x y : X
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0∞
hd : edist x y ≤ d
bc : 0 ≤ (↑r : ℝ)
⊢ (↑C : ℝ≥0∞) * edist x y ^ (↑r : ℝ) ≤ (↑C : ℝ≥0∞) * d ^ (↑r : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.Holder
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
inst_2 : PseudoEMetricSpace Z
s : Set X
Cg rg : ℝ≥0
g : Y → Z
t : Set Y
hg : HolderOnWith Cg rg g t
Cf rf : ℝ≥0
f : X → Y
hf : HolderOnWith Cf rf f s
hst : MapsTo f s t
x : X
hx : x ∈ s
y : X
hy : y ∈ s
rw : edist ((g ∘ f) x) ((g ∘ f) y) ≤ (↑Cg : ℝ≥0∞) * ((↑Cf : ℝ≥0∞) * edist x y ^ (↑rf : ℝ)) ^ (↑rg : ℝ)
⊢ edist ((g ∘ f) x) ((g ∘ f) y) ≤ (↑(Cg * Cf ^ (↑rg : ℝ)) : ℝ≥0∞) * edist x y ^ (↑(rg * rf) : ℝ)

Tactic:
rw [ENNReal.coe_mul, mul_comm rg, NNReal.coe_mul, ENNReal.rpow_mul, mul_assoc,
    ENNReal.coe_rpow_of_nonneg _ rg.coe_nonneg, ← ENNReal.mul_rpow_of_nonneg _ _ rg.coe_nonneg]

Premises used: ENNReal.rpow_mul, ENNReal.mul_rpow_of_nonneg, mul_assoc, ENNReal.coe_rpow_of_nonneg, ENNReal.coe_mul, NNReal.coe_nonneg, mul_comm, NNReal.coe_mul