awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
E : EqOn f g s
inr : ∀ (x y : α), g x ≤ g y + (↑K : ℝ) * dist x y
⊢ ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn f g s

Tactic:
refine ⟨g, LipschitzWith.of_le_add_mul K fun x y => ?_, E⟩
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
E : EqOn f g s
x y : α
inr : g x - (↑K : ℝ) * dist x y ≤ g y
⊢ g x ≤ g y + (↑K : ℝ) * dist x y

Tactic:
rw [← sub_le_iff_le_add]

Premises used: sub_le_iff_le_add
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
E : EqOn f g s
x y : α
⊢ g x - (↑K : ℝ) * dist x y ≤ g y

Tactic:
le_ciInf fun z => ?_

Premises used: le_ciInf
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
E : EqOn f g s
x y : α
inr : ∀ (z : (↑s : Type u)), g x - (↑K : ℝ) * dist x y ≤ f (↑z : α) + (↑K : ℝ) * dist y (↑z : α)
⊢ g x - (↑K : ℝ) * dist x y ≤ g y

Tactic:
refine le_ciInf fun z => ?_

Premises used: le_ciInf
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
E : EqOn f g s
x y : α
z : (↑s : Type u)
inr : g x ≤ f (↑z : α) + (↑K : ℝ) * dist y (↑z : α) + (↑K : ℝ) * dist x y
⊢ g x - (↑K : ℝ) * dist x y ≤ f (↑z : α) + (↑K : ℝ) * dist y (↑z : α)

Tactic:
rw [sub_le_iff_le_add]

Premises used: sub_le_iff_le_add
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
E : EqOn f g s
x y : α
z : (↑s : Type u)
⊢ g x ≤ f (↑z : α) + (↑K : ℝ) * dist x (↑z : α)

Tactic:
ciInf_le (B x) _

Premises used: ciInf_le
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
E : EqOn f g s
x y : α
z : (↑s : Type u)
rw : f (↑z : α) + (↑K : ℝ) * dist x (↑z : α) ≤ f (↑z : α) + (↑K : ℝ) * (dist x y + dist y (↑z : α))
⊢ f (↑z : α) + (↑K : ℝ) * dist x (↑z : α) ≤ f (↑z : α) + (↑K : ℝ) * dist y (↑z : α) + (↑K : ℝ) * dist x y

Tactic:
rw [add_assoc, ← mul_add, add_comm (dist y z)]

Premises used: add_assoc, add_comm, mul_add, Dist.dist, Subtype.val
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
E : EqOn f g s
x y : α
z : (↑s : Type u)
bc : dist x (↑z : α) ≤ dist x y + dist y (↑z : α)
⊢ f (↑z : α) + (↑K : ℝ) * dist x (↑z : α) ≤ f (↑z : α) + (↑K : ℝ) * (dist x y + dist y (↑z : α))

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
E : EqOn f g s
x y : α
z : (↑s : Type u)
⊢ dist x (↑z : α) ≤ dist x y + dist y (↑z : α)

Tactic:
apply dist_triangle

Premises used: dist_triangle
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
E : EqOn f g s
x y : α
z : (↑s : Type u)
g₁ : f (↑z : α) + (↑K : ℝ) * dist x (↑z : α) ≤ f (↑z : α) + (↑K : ℝ) * dist y (↑z : α) + (↑K : ℝ) * dist x y
⊢ g x ≤ f (↑z : α) + (↑K : ℝ) * dist y (↑z : α) + (↑K : ℝ) * dist x y

Tactic:
calc
    g x ≤ f z + K * dist x z := ciInf_le (B x) _
    _ ≤ f z + K * dist y z + K * dist x y := by
      rw [add_assoc, ← mul_add, add_comm (dist y z)]
      gcongr
      apply dist_triangle

Premises used: ciInf_le, Dist.dist, Subtype.val
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
ι : Type x
inst : PseudoMetricSpace α
inst_1 : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
i : ι
⊢ LipschitzOnWith (β := ℝ) K (fun (x : α) ↦ f x i) s

Tactic:
have : LipschitzOnWith K (fun x : α => f x i) s :=
      LipschitzOnWith.of_dist_le_mul fun x hx y hy =>
        (dist_le_pi_dist _ _ i).trans (hf.dist_le_mul x hx y hy)
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
ι : Type x
inst : PseudoMetricSpace α
inst_1 : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
i : ι
this : LipschitzOnWith (β := ℝ) K (fun (x : α) ↦ f x i) s
⊢ ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn (fun (x : α) ↦ f x i) g s

Tactic:
this.extend_real

Premises used: LipschitzOnWith.extend_real
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
ι : Type x
inst : PseudoMetricSpace α
inst_1 : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
i : ι
this : LipschitzOnWith (β := ℝ) K (fun (x : α) ↦ f x i) s
⊢ ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn (fun (x : α) ↦ f x i) g s

Tactic:
exact this.extend_real

Premises used: LipschitzOnWith.extend_real
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
ι : Type x
inst : PseudoMetricSpace α
inst_1 : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
⊢ ∀ (i : ι), ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn (fun (x : α) ↦ f x i) g s

Tactic:
have : ∀ i, ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn (fun x => f x i) g s := fun i => by
    have : LipschitzOnWith K (fun x : α => f x i) s :=
      LipschitzOnWith.of_dist_le_mul fun x hx y hy =>
        (dist_le_pi_dist _ _ i).trans (hf.dist_le_mul x hx y hy)
    exact this.extend_real
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
ι : Type x
inst : PseudoMetricSpace α
inst_1 : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : ∀ (i : ι), ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn (fun (x : α) ↦ f x i) g s
choose :
  ∀ (g : (i : ι) → α → ℝ) (hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun (x : α) ↦ f x i) (g i) s),
    ∃ (g : α → ι → ℝ), LipschitzWith K g ∧ EqOn f g s
⊢ ∃ (g : α → ι → ℝ), LipschitzWith K g ∧ EqOn f g s

Tactic:
choose g hg using this
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
ι : Type x
inst : PseudoMetricSpace α
inst_1 : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : (i : ι) → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun (x : α) ↦ f x i) (g i) s
⊢ ∃ (g : α → ι → ℝ), LipschitzWith K g ∧ EqOn f g s

Tactic:
⟨fun x i => g i x, LipschitzWith.of_dist_le_mul fun x y => ?_, fun x hx ↦ ?_⟩

Premises used: And.intro, Exists.intro, LipschitzWith.of_dist_le_mul
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
ι : Type x
inst : PseudoMetricSpace α
inst_1 : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : (i : ι) → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun (x : α) ↦ f x i) (g i) s
refine_1 : ∀ (x y : α), (dist.{x} (α := ι → ℝ) (fun (i : ι) ↦ g i x) fun (i : ι) ↦ g i y) ≤ (↑K : ℝ) * dist x y
refine_2 : ∀ (x : α) (hx : x ∈ s), f x = (fun (x : α) (i : ι) ↦ g i x) x
⊢ ∃ (g : α → ι → ℝ), LipschitzWith K g ∧ EqOn f g s

Tactic:
refine ⟨fun x i => g i x, LipschitzWith.of_dist_le_mul fun x y => ?_, fun x hx ↦ ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
ι : Type x
inst : PseudoMetricSpace α
inst_1 : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : (i : ι) → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun (x : α) ↦ f x i) (g i) s
x y : α
⊢ (dist.{x} (α := ι → ℝ) (fun (i : ι) ↦ g i x) fun (i : ι) ↦ g i y) ≤ (↑K : ℝ) * dist x y

Tactic:
(dist_pi_le_iff (mul_nonneg K.2 dist_nonneg)).2 fun i => (hg i).1.dist_le_mul x y

Premises used: Iff.mpr, mul_nonneg, LipschitzWith.dist_le_mul, dist_nonneg, dist_pi_le_iff, And.left, NNReal.toReal, Subtype.property
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
ι : Type x
inst : PseudoMetricSpace α
inst_1 : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : (i : ι) → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun (x : α) ↦ f x i) (g i) s
x y : α
⊢ (dist.{x} (α := ι → ℝ) (fun (i : ι) ↦ g i x) fun (i : ι) ↦ g i y) ≤ (↑K : ℝ) * dist x y

Tactic:
exact (dist_pi_le_iff (mul_nonneg K.2 dist_nonneg)).2 fun i => (hg i).1.dist_le_mul x y

Premises used: Iff.mpr, mul_nonneg, LipschitzWith.dist_le_mul, dist_nonneg, dist_pi_le_iff, And.left, Subtype.property
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
ι : Type x
inst : PseudoMetricSpace α
inst_1 : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : (i : ι) → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun (x : α) ↦ f x i) (g i) s
x : α
hx : x ∈ s
refine_2 : ∀ (i : ι), f x i = (fun (x : α) (i : ι) ↦ g i x) x i
⊢ f x = (fun (x : α) (i : ι) ↦ g i x) x

Tactic:
ext1 i
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
ι : Type x
inst : PseudoMetricSpace α
inst_1 : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : (i : ι) → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun (x : α) ↦ f x i) (g i) s
x : α
hx : x ∈ s
i : ι
⊢ f x i = (fun (x : α) (i : ι) ↦ g i x) x i

Tactic:
(hg i).2 hx

Premises used: And.right
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
ι : Type x
inst : PseudoMetricSpace α
inst_1 : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : (i : ι) → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun (x : α) ↦ f x i) (g i) s
x : α
hx : x ∈ s
i : ι
⊢ f x i = (fun (x : α) (i : ι) ↦ g i x) x i

Tactic:
exact (hg i).2 hx

Premises used: And.right
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s : Set X
ε : ℝ≥0∞
⊢ IsSeparated ε s ↔
    SetRel.IsSeparated
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => edist x y ≤ ε}
      s

Tactic:
simp [IsSeparated, SetRel.IsSeparated]

Premises used: SetRel.IsSeparated, Metric.IsSeparated
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0∞
⊢ IsSeparated.{u_1} (X := X) ε ∅

Tactic:
pairwise_empty _

Premises used: Set.pairwise_empty, Metric.IsSeparated
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0∞
x : X
⊢ IsSeparated (X := X) ε {x}

Tactic:
pairwise_singleton ..

Premises used: Set.pairwise_singleton, Metric.IsSeparated
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s : Set X
ε : ℝ≥0∞
hs : s.Subsingleton
⊢ IsSeparated ε s

Tactic:
hs.pairwise _

Premises used: Set.Subsingleton.pairwise, Metric.IsSeparated
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s : Set X
ε δ : ℝ≥0∞
hεδ : ε ≤ δ
hs : IsSeparated δ s
⊢ IsSeparated ε s

Tactic:
hs.mono' fun _ _ ↦ hεδ.trans_lt

Premises used: Set.Pairwise.mono', LE.le.trans_lt, Metric.IsSeparated
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t : Set X
ε : ℝ≥0∞
hst : s ⊆ t
hs : IsSeparated ε t
⊢ IsSeparated ε s

Tactic:
hs.mono hst

Premises used: Set.Pairwise.mono, Metric.IsSeparated
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s : Set X
ε : ℝ≥0∞
x x_1 x_2 : X
⊢ ε < edist x_1 x_2 → ε < edist x_2 x_1

Tactic:
simp [edist_comm]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s : Set X
ε : ℝ≥0∞
x : X
hx : x ∉ s
x_1 x_2 : X
⊢ ε < edist x_1 x_2 → ε < edist x_2 x_1

Tactic:
simp [edist_comm]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s : Set X
ε : ℝ≥0∞
x : X
hs : IsSeparated ε s
h : ∀ y ∈ s, x ≠ y → ε < edist x y
⊢ IsSeparated ε (insert x s)

Tactic:
isSeparated_insert.2 ⟨hs, h⟩

Premises used: Iff.mpr, Metric.isSeparated_insert, And.intro
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_3
inst : EMetricSpace X
s : Set X
⊢ IsSeparated 0 s

Tactic:
simp [IsSeparated, Set.Pairwise]

Premises used: Set.Pairwise, Metric.IsSeparated
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
s : Set X
ε K₁ : ℝ≥0
f : X → Y
hs : IsSeparated (↑ε : ℝ≥0∞) s
hf : AntilipschitzWith K₁ f
hK₁ : 0 < K₁
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hne : f x ≠ f y
⊢ x ≠ y

Tactic:
grind
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
s : Set X
ε K₁ : ℝ≥0
f : X → Y
hs : IsSeparated (↑ε : ℝ≥0∞) s
hf : AntilipschitzWith K₁ f
hK₁ : 0 < K₁
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hne : f x ≠ f y
rw : edist x y ≤ (↑K₁ : ℝ≥0∞) * edist (f x) (f y)
⊢ edist x y ≤ edist (f x) (f y) * (↑K₁ : ℝ≥0∞)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
s : Set X
ε K₁ : ℝ≥0
f : X → Y
hs : IsSeparated (↑ε : ℝ≥0∞) s
hf : AntilipschitzWith K₁ f
hK₁ : 0 < K₁
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hne : f x ≠ f y
⊢ edist x y ≤ (↑K₁ : ℝ≥0∞) * edist (f x) (f y)

Tactic:
hf x y
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
s : Set X
ε K₁ : ℝ≥0
f : X → Y
hs : IsSeparated (↑ε : ℝ≥0∞) s
hf : AntilipschitzWith K₁ f
hK₁ : 0 < K₁
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hne : f x ≠ f y
⊢ edist x y ≤ (↑K₁ : ℝ≥0∞) * edist (f x) (f y)

Tactic:
exact hf x y
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
s : Set X
ε K₁ : ℝ≥0
f : X → Y
hs : IsSeparated (↑ε : ℝ≥0∞) s
hf : AntilipschitzWith K₁ f
hK₁ : 0 < K₁
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hne : f x ≠ f y
⊢ (↑ε : ℝ≥0∞) < edist (f x) (f y) * (↑K₁ : ℝ≥0∞)

Tactic:
have hmul : (↑ε : ℝ≥0∞) < edist (f x) (f y) * ↑K₁ :=
    lt_of_lt_of_le (hs hx hy (by grind)) (by rw [mul_comm]; exact hf x y)
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
s : Set X
ε K₁ : ℝ≥0
f : X → Y
hs : IsSeparated (↑ε : ℝ≥0∞) s
hf : AntilipschitzWith K₁ f
hK₁ : 0 < K₁
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hne : f x ≠ f y
hmul : (↑ε : ℝ≥0∞) < edist (f x) (f y) * (↑K₁ : ℝ≥0∞)
⊢ (↑(ε / K₁) : ℝ≥0∞) < edist (f x) (f y)

Tactic:
ENNReal.coe_div hK₁.ne' ▸ ENNReal.div_lt_of_lt_mul hmul

Premises used: Eq.rec, LT.lt.ne', ENNReal.div_lt_of_lt_mul, Eq.symm, ENNReal.coe_div
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
s : Set X
ε K₁ : ℝ≥0
f : X → Y
hs : IsSeparated (↑ε : ℝ≥0∞) s
hf : AntilipschitzWith K₁ f
hK₁ : 0 < K₁
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hne : f x ≠ f y
hmul : (↑ε : ℝ≥0∞) < edist (f x) (f y) * (↑K₁ : ℝ≥0∞)
⊢ (↑(ε / K₁) : ℝ≥0∞) < edist (f x) (f y)

Tactic:
exact ENNReal.coe_div hK₁.ne' ▸ ENNReal.div_lt_of_lt_mul hmul
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t : Set X
h : AreSeparated s t
⊢ AreSeparated t s

Tactic:
let ⟨r, r0, hr⟩ := h
  ⟨r, r0, fun y hy x hx => edist_comm x y ▸ hr x hx y hy⟩

Premises used: PseudoEMetricSpace.edist_comm, Eq.rec, And.intro, Exists.intro, _private.0.Metric.AreSeparated.symm.match_1, Metric.AreSeparated
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t : Set X
⊢ AreSeparated s t ↔ AreSeparated t s

Tactic:
⟨symm, symm⟩

Premises used: Metric.AreSeparated.symm, Iff.intro
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s : Set X
⊢ AreSeparated ∅ s

Tactic:
⟨1, one_ne_zero, fun _x => False.elim⟩

Premises used: False.elim, And.intro, Exists.intro, one_ne_zero, OfNat.ofNat, Metric.AreSeparated
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s : Set X
⊢ AreSeparated s ∅

Tactic:
(empty_left s).symm

Premises used: Metric.AreSeparated.symm, Metric.AreSeparated.empty_left
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t : Set X
h : AreSeparated s t
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
x : X
hx1 : x ∈ s
hx2 : x ∈ t
⊢ r = 0

Tactic:
simpa using hr x hx1 x hx2
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t : Set X
h : AreSeparated s t
⊢ s ⊆ tᶜ

Tactic:
fun _ hs ht =>
  h.disjoint.le_bot ⟨hs, ht⟩

Premises used: Disjoint.le_bot, Set.Mem, setOf, Set.Subset, Metric.AreSeparated.disjoint, And.intro, Not
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t s' t' : Set X
hs : s ⊆ s'
ht : t ⊆ t'
⊢ AreSeparated s' t' → AreSeparated s t

Tactic:
fun ⟨r, r0, hr⟩ =>
  ⟨r, r0, fun x hx y hy => hr x (hs hx) y (ht hy)⟩

Premises used: And.intro, Exists.intro, _private.0.Metric.AreSeparated.symm.match_1, Metric.AreSeparated
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t s' : Set X
h' : AreSeparated s' t
hs : s ⊆ s'
⊢ AreSeparated s t

Tactic:
h'.mono hs Subset.rfl

Premises used: Set.Subset.rfl, Metric.AreSeparated.mono
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t t' : Set X
h' : AreSeparated s t'
ht : t ⊆ t'
⊢ AreSeparated s t

Tactic:
h'.mono Subset.rfl ht

Premises used: Set.Subset.rfl, Metric.AreSeparated.mono
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t s' : Set X
h : AreSeparated s t
h' : AreSeparated s' t
rcases :
  ∀ (r : ℝ≥0∞) (r0 : r ≠ 0) (hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y) (r' : ℝ≥0∞) (r0' : r' ≠ 0)
    (hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y), AreSeparated (s ∪ s') t
⊢ AreSeparated (s ∪ s') t

Tactic:
rcases h, h' with ⟨⟨r, r0, hr⟩, ⟨r', r0', hr'⟩⟩
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
⊢ AreSeparated (s ∪ s') t

Tactic:
⟨min r r', ?_, fun x hx y hy => hx.elim ?_ ?_⟩

Premises used: And.intro, Exists.intro, Or.elim, Min.min, Metric.AreSeparated
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
refine_1 : min r r' ≠ 0
refine_2 : ∀ (x : X) (hx : x ∈ s ∪ s') (y : X) (hy : y ∈ t), x ∈ s → min r r' ≤ edist x y
refine_3 : ∀ (x : X) (hx : x ∈ s ∪ s') (y : X) (hy : y ∈ t), x ∈ s' → min r r' ≤ edist x y
⊢ AreSeparated (s ∪ s') t

Tactic:
refine ⟨min r r', ?_, fun x hx y hy => hx.elim ?_ ?_⟩
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
refine_1 :
  ∀ (r0 : 0 < r) (hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y) (r' : ℝ≥0∞) (r0' : 0 < r')
    (hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y), 0 < min r r'
⊢ min r r' ≠ 0

Tactic:
rw [← pos_iff_ne_zero] at r0 r0' ⊢

Premises used: pos_iff_ne_zero
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : 0 < r
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : 0 < r'
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
⊢ 0 < min r r'

Tactic:
lt_min r0 r0'

Premises used: lt_min
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : 0 < r
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : 0 < r'
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
⊢ 0 < min r r'

Tactic:
exact lt_min r0 r0'

Premises used: lt_min
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
x : X
hx : x ∈ s ∪ s'
y : X
hy : y ∈ t
⊢ x ∈ s → min r r' ≤ edist x y

Tactic:
fun hx => (min_le_left _ _).trans (hr _ hx _ hy)

Premises used: min_le_left, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
x : X
hx : x ∈ s ∪ s'
y : X
hy : y ∈ t
⊢ x ∈ s → min r r' ≤ edist x y

Tactic:
exact fun hx => (min_le_left _ _).trans (hr _ hx _ hy)

Premises used: min_le_left, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
x : X
hx : x ∈ s ∪ s'
y : X
hy : y ∈ t
⊢ x ∈ s' → min r r' ≤ edist x y

Tactic:
fun hx => (min_le_right _ _).trans (hr' _ hx _ hy)

Premises used: min_le_right, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
x : X
hx : x ∈ s ∪ s'
y : X
hy : y ∈ t
⊢ x ∈ s' → min r r' ≤ edist x y

Tactic:
exact fun hx => (min_le_right _ _).trans (hr' _ hx _ hy)

Premises used: min_le_right, LE.le.trans