awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
s : β → α
hs : ∀ ε > 0, ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
ε : ℝ≥0∞
ε0 : ε > 0
N : β
hN : ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
⊢ ∀ᶠ (x : β) in atTop, ediam (s '' Ici x) ≤ ε

Tactic:
(eventually_ge_atTop N).mono fun n hn => Metric.ediam_le ?_

Premises used: Filter.Eventually.mono, Metric.ediam_le, Filter.eventually_ge_atTop
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
s : β → α
hs : ∀ ε > 0, ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
ε : ℝ≥0∞
ε0 : ε > 0
N : β
hN : ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
mp : ∀ (n : β) (hn : N ≤ n), ∀ x ∈ s '' Ici n, ∀ y ∈ s '' Ici n, edist x y ≤ ε
⊢ ∀ᶠ (x : β) in atTop, ediam (s '' Ici x) ≤ ε

Tactic:
refine (eventually_ge_atTop N).mono fun n hn => Metric.ediam_le ?_

Premises used: Filter.Eventually.mono, Metric.ediam_le, Filter.eventually_ge_atTop
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
s : β → α
hs : ∀ ε > 0, ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
ε : ℝ≥0∞
ε0 : ε > 0
N : β
hN : ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
n : β
hn : N ≤ n
k : β
hk : k ∈ Ici n
l : β
hl : l ∈ Ici n
⊢ edist (s k) (s l) ≤ ε

Tactic:
(hN _ (hn.trans hk) _ (hn.trans hl)).le

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
s : β → α
hs : ∀ ε > 0, ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
ε : ℝ≥0∞
ε0 : ε > 0
N : β
hN : ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
n : β
hn : N ≤ n
k : β
hk : k ∈ Ici n
l : β
hl : l ∈ Ici n
⊢ edist (s k) (s l) ≤ ε

Tactic:
exact (hN _ (hn.trans hk) _ (hn.trans hl)).le

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
s : β → α
b : β → ℝ≥0∞
b_bound : ∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∀ᶠ (n : β) in atTop, b n < ε

Tactic:
have : ∀ᶠ n in atTop, b n < ε := b_lim.eventually (gt_mem_nhds εpos)
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
s : β → α
b : β → ℝ≥0∞
b_bound : ∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
ε : ℝ≥0∞
εpos : ε > 0
this : ∀ᶠ (n : β) in atTop, b n < ε
mpr : ∀ (N : β) (hN : b N < ε), ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
⊢ ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε

Tactic:
rcases this.exists with ⟨N, hN⟩

Premises used: Filter.Eventually.exists
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
s : β → α
b : β → ℝ≥0∞
b_bound : ∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
ε : ℝ≥0∞
εpos : ε > 0
this : ∀ᶠ (n : β) in atTop, b n < ε
N : β
hN : b N < ε
⊢ ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε

Tactic:
⟨N, fun m hm n hn => ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
s : β → α
b : β → ℝ≥0∞
b_bound : ∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
ε : ℝ≥0∞
εpos : ε > 0
this : ∀ᶠ (n : β) in atTop, b n < ε
N : β
hN : b N < ε
mpr : ∀ (m : β) (hm : N ≤ m) (n : β) (hn : N ≤ n), edist (s m) (s n) < ε
⊢ ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε

Tactic:
refine ⟨N, fun m hm n hn => ?_⟩
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
s : β → α
b : β → ℝ≥0∞
b_bound : ∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
ε : ℝ≥0∞
εpos : ε > 0
this : ∀ᶠ (n : β) in atTop, b n < ε
N : β
hN : b N < ε
m : β
hm : N ≤ m
n : β
hn : N ≤ n
⊢ edist (s m) (s n) ≤ b N

Tactic:
b_bound m n N hm hn
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
s : β → α
b : β → ℝ≥0∞
b_bound : ∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
ε : ℝ≥0∞
εpos : ε > 0
this : ∀ᶠ (n : β) in atTop, b n < ε
N : β
hN : b N < ε
m : β
hm : N ≤ m
n : β
hn : N ≤ n
⊢ b N < ε

Tactic:
hN
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
s : β → α
b : β → ℝ≥0∞
b_bound : ∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
ε : ℝ≥0∞
εpos : ε > 0
this : ∀ᶠ (n : β) in atTop, b n < ε
N : β
hN : b N < ε
m : β
hm : N ≤ m
n : β
hn : N ≤ n
⊢ edist (s m) (s n) < ε

Tactic:
calc edist (s m) (s n) ≤ b N := b_bound m n N hm hn
    _ < ε := hN

Premises used: EDist.edist
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] f

Tactic:
continuous_iff_continuousAt.2 fun x => ENNReal.tendsto_nhds_of_Icc fun ε ε0 => ?_

Premises used: Iff.mpr, continuous_iff_continuousAt, ENNReal.tendsto_nhds_of_Icc
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
refine : ∀ (x : α) (ε : ℝ≥0∞) (ε0 : ε > 0), ∀ᶠ (x_1 : α) in 𝓝 x, f x_1 ∈ Icc (f x - ε) (f x + ε)
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] f

Tactic:
refine continuous_iff_continuousAt.2 fun x => ENNReal.tendsto_nhds_of_Icc fun ε ε0 => ?_

Premises used: Iff.mpr, continuous_iff_continuousAt, ENNReal.tendsto_nhds_of_Icc
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
rcases : ∀ (δ : ℝ≥0) (δ0 : δ > 0) (hδ : (↑δ : ℝ≥0∞) * C < ε), ∀ᶠ (x_1 : α) in 𝓝 x, f x_1 ∈ Icc (f x - ε) (f x + ε)
⊢ ∀ᶠ (x_1 : α) in 𝓝 x, f x_1 ∈ Icc (f x - ε) (f x + ε)

Tactic:
rcases ENNReal.exists_nnreal_pos_mul_lt hC ε0.ne' with ⟨δ, δ0, hδ⟩

Premises used: ENNReal.exists_nnreal_pos_mul_lt, LT.lt.ne'
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : (↑δ : ℝ≥0∞) * C < ε
⊢ C * (↑δ : ℝ≥0∞) < ε

Tactic:
rw [mul_comm] at hδ

Premises used: mul_comm
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * (↑δ : ℝ≥0∞) < ε
h₁ : ∀ (y : α) (hy : y ∈ closedEBall x (↑δ : ℝ≥0∞)), f y ∈ Icc (f x - ε) (f x + ε)
⊢ ∀ᶠ (x_1 : α) in 𝓝 x, f x_1 ∈ Icc (f x - ε) (f x + ε)

Tactic:
filter_upwards [Metric.closedEBall_mem_nhds x (ENNReal.coe_pos.2 δ0)] with y hy

Premises used: Metric.closedEBall_mem_nhds, Iff.mpr, ENNReal.coe_pos
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * (↑δ : ℝ≥0∞) < ε
y : α
hy : y ∈ closedEBall x (↑δ : ℝ≥0∞)
⊢ f y ∈ Icc (f x - ε) (f x + ε)

Tactic:
⟨tsub_le_iff_right.2 <| (h x y).trans ?_, (h y x).trans ?_⟩

Premises used: Iff.mpr, Set.Mem, setOf, tsub_le_iff_right, Set.Icc, And.intro, LE.le.trans
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * (↑δ : ℝ≥0∞) < ε
y : α
hy : y ∈ closedEBall x (↑δ : ℝ≥0∞)
h₁ : f y + C * edist x y ≤ f y + ε
h₂ : f x + C * edist y x ≤ f x + ε
⊢ f y ∈ Icc (f x - ε) (f x + ε)

Tactic:
refine ⟨tsub_le_iff_right.2 <| (h x y).trans ?_, (h y x).trans ?_⟩
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * (↑δ : ℝ≥0∞) < ε
y : α
hy : y ∈ closedEBall x (↑δ : ℝ≥0∞)
h₁ : f y + C * edist x y ≤ f y + C * (↑δ : ℝ≥0∞)
⊢ f y + C * edist x y ≤ f y + ε

Tactic:
grw [← hδ.le]

Premises used: LT.lt.le
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * (↑δ : ℝ≥0∞) < ε
y : α
hy : y ∈ closedEBall x (↑δ : ℝ≥0∞)
h₁ : f x + C * edist y x ≤ f x + C * (↑δ : ℝ≥0∞)
⊢ f x + C * edist y x ≤ f x + ε

Tactic:
grw [← hδ.le]

Premises used: LT.lt.le
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * (↑δ : ℝ≥0∞) < ε
y : α
hy : y ∈ closedEBall x (↑δ : ℝ≥0∞)
h₁ : edist x y ≤ (↑δ : ℝ≥0∞)
⊢ f y + C * edist x y ≤ f y + C * (↑δ : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * (↑δ : ℝ≥0∞) < ε
y : α
hy : y ∈ closedEBall x (↑δ : ℝ≥0∞)
h₁ : edist y x ≤ (↑δ : ℝ≥0∞)
⊢ f x + C * edist y x ≤ f x + C * (↑δ : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * (↑δ : ℝ≥0∞) < ε
y : α
hy : y ∈ closedEBall x (↑δ : ℝ≥0∞)
⊢ edist x y ≤ (↑δ : ℝ≥0∞)

Tactic:
Metric.mem_closedEBall'.1 hy

Premises used: Metric.mem_closedEBall', Iff.mp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * (↑δ : ℝ≥0∞) < ε
y : α
hy : y ∈ closedEBall x (↑δ : ℝ≥0∞)
⊢ edist y x ≤ (↑δ : ℝ≥0∞)

Tactic:
Metric.mem_closedEBall.1 hy

Premises used: Metric.mem_closedEBall, Iff.mp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * (↑δ : ℝ≥0∞) < ε
y : α
hy : y ∈ closedEBall x (↑δ : ℝ≥0∞)
⊢ edist x y ≤ (↑δ : ℝ≥0∞)

Tactic:
exacts [Metric.mem_closedEBall'.1 hy, Metric.mem_closedEBall.1 hy]

Premises used: Metric.mem_closedEBall, Metric.mem_closedEBall', Iff.mp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
⊢ Ne (α := ℝ≥0∞) 2 ∞

Tactic:
decide
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
apply : ∀ (x y : α × α), edist x.1 x.2 ≤ edist y.1 y.2 + 2 * edist x y
⊢ Continuous[instTopologicalSpaceProd, _] fun (p : α × α) ↦ edist p.1 p.2

Tactic:
apply continuous_of_le_add_edist 2 (by decide)

Premises used: continuous_of_le_add_edist, OfNat.ofNat
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x y ≤ edist x x' + edist x' y' + edist y' y

Tactic:
edist_triangle4 _ _ _ _

Premises used: edist_triangle4
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y x' y' : α
rw : edist x x' + edist x' y' + edist y' y = edist x' y' + (edist x x' + edist y' y)
⊢ edist x x' + edist x' y' + edist y' y = edist x' y' + (edist x x' + edist y y')

Tactic:
rw [edist_comm y y']

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x x' + edist x' y' + edist y' y = edist x' y' + (edist x x' + edist y' y)

Tactic:
abel
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y x' y' : α
bc : edist x x' ≤ edist (x, y) (x', y')
bc₁ : edist y y' ≤ edist (x, y) (x', y')
⊢ edist x' y' + (edist x x' + edist y y') ≤ edist x' y' + (edist (x, y) (x', y') + edist (x, y) (x', y'))

Tactic:
gcongr
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x x' ≤ edist (x, y) (x', y')

Tactic:
apply_rules [le_max_left, le_max_right]

Premises used: le_max_right, le_max_left
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y x' y' : α
⊢ edist y y' ≤ edist (x, y) (x', y')

Tactic:
apply_rules [le_max_left, le_max_right]

Premises used: le_max_right, le_max_left
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y x' y' : α
rw : edist x' y' + edist (x, y) (x', y') * 2 = edist x' y' + 2 * edist (x, y) (x', y')
rw₁ rw₂ : edist x' y' + 2 * edist (x, y) (x', y') = edist x' y' + 2 * edist (x, y) (x', y')
⊢ edist x' y' + (edist (x, y) (x', y') + edist (x, y) (x', y')) = edist x' y' + 2 * edist (x, y) (x', y')

Tactic:
rw [← mul_two, mul_comm]

Premises used: mul_comm, mul_two
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y x' y' : α
edist :
  EDist.edist x x' + EDist.edist x' y' + EDist.edist y' y = EDist.edist x' y' + (EDist.edist x x' + EDist.edist y y')
edist₁ :
  EDist.edist x' y' + (EDist.edist x x' + EDist.edist y y') ≤
    EDist.edist x' y' + (EDist.edist (x, y) (x', y') + EDist.edist (x, y) (x', y'))
edist₂ :
  EDist.edist x' y' + (EDist.edist (x, y) (x', y') + EDist.edist (x, y) (x', y')) =
    EDist.edist x' y' + 2 * EDist.edist (x, y) (x', y')
⊢ EDist.edist (x, y).1 (x, y).2 ≤ EDist.edist (x', y').1 (x', y').2 + 2 * EDist.edist (x, y) (x', y')

Tactic:
calc
    edist x y ≤ edist x x' + edist x' y' + edist y' y := edist_triangle4 _ _ _ _
    _ = edist x' y' + (edist x x' + edist y y') := by rw [edist_comm y y']; abel
    _ ≤ edist x' y' + (edist (x, y) (x', y') + edist (x, y) (x', y')) := by
      gcongr <;> apply_rules [le_max_left, le_max_right]
    _ = edist x' y' + 2 * edist (x, y) (x', y') := by rw [← mul_two, mul_comm]

Premises used: Prod.mk, edist_triangle4, HAdd.hAdd, EDist.edist
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
f g : β → α
hf : Continuous[inst_1, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] f
hg : Continuous[inst_1, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] g
⊢ Continuous[inst_1, _] fun (b : β) ↦ EDist.edist (f b) (g b)

Tactic:
continuous_edist.comp (hf.prodMk hg :)

Premises used: Continuous.comp, continuous_edist, Continuous.prodMk
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
f g : β → α
x : Filter β
a b : α
hf : Tendsto f x (𝓝 a)
hg : Tendsto g x (𝓝 b)
⊢ Tendsto (fun (x : β) ↦ EDist.edist (f x) (g x)) x (𝓝 (EDist.edist a b))

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

Premises used: continuous_edist, Prod.mk, Continuous.tendsto, Filter.Tendsto.comp, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
a : α
r : ℝ≥0∞
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (y : α) ↦ edist y a

Tactic:
fun_prop
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s : Set α
⊢ ediam (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = ediam s

Tactic:
le_antisymm (ediam_le fun x hx y hy => ?_) (ediam_mono subset_closure)

Premises used: subset_closure, Metric.ediam_mono, le_antisymm, Metric.ediam_le
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s : Set α
refine :
  ∀ (x : α) (hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) (y : α)
    (hy : y ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s), edist x y ≤ ediam s
⊢ ediam (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = ediam s

Tactic:
refine le_antisymm (ediam_le fun x hx y hy => ?_) (ediam_mono subset_closure)

Premises used: subset_closure, Metric.ediam_mono, le_antisymm, Metric.ediam_le
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s : Set α
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
y : α
hy : y ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ edist x y ∈ closure (Iic (ediam s))

Tactic:
have : edist x y ∈ closure (Iic (ediam s)) :=
    map_mem_closure₂ continuous_edist hx hy fun x hx y hy => edist_le_ediam_of_mem hx hy
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s : Set α
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
y : α
hy : y ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
this : edist x y ∈ closure (Iic (ediam s))
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : edist x y ∈ Iic (ediam s)), edist x y ≤ ediam s
⊢ edist x y ≤ ediam s

Tactic:
rwa [closure_Iic] at this

Premises used: closure_Iic
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
inst : PseudoMetricSpace α
s : Set α
⊢ diam (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) = diam s

Tactic:
simp only [Metric.diam, Metric.ediam_closure]

Premises used: Metric.ediam_closure, Metric.diam
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
simp : IsClosed[Pi.topologicalSpace] (⋂ i ∈ s, ⋂ i_1 ∈ s, {x : α → β | edist (x i) (x i_1) ≤ (↑K : ℝ≥0∞) * edist i i_1})
⊢ IsClosed[Pi.topologicalSpace] {f : α → β | LipschitzOnWith K f s}

Tactic:
simp only [LipschitzOnWith, setOf_forall]

Premises used: LipschitzOnWith, Set.setOf_forall
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
⊢ IsClosed[Pi.topologicalSpace] (⋂ i ∈ s, ⋂ i_1 ∈ s, {x : α → β | edist (x i) (x i_1) ≤ (↑K : ℝ≥0∞) * edist i i_1})

Tactic:
isClosed_biInter fun x _ => isClosed_biInter fun y _ => isClosed_le ?_ ?_

Premises used: isClosed_biInter, isClosed_le
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
refine_1 : ∀ x ∈ s, ∀ y ∈ s, Continuous[Pi.topologicalSpace, _] fun (x_3 : α → β) ↦ edist (x_3 x) (x_3 y)
refine_2 : ∀ x ∈ s, ∀ y ∈ s, Continuous[Pi.topologicalSpace, _] fun (x_3 : α → β) ↦ (↑K : ℝ≥0∞) * edist x y
⊢ IsClosed[Pi.topologicalSpace] (⋂ i ∈ s, ⋂ i_1 ∈ s, {x : α → β | edist (x i) (x i_1) ≤ (↑K : ℝ≥0∞) * edist i i_1})

Tactic:
refine isClosed_biInter fun x _ => isClosed_biInter fun y _ => isClosed_le ?_ ?_

Premises used: isClosed_biInter, isClosed_le
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
x : α
h : x ∈ s
y : α
h_1 : y ∈ s
⊢ Continuous[Pi.topologicalSpace, _] fun (x_1 : α → β) ↦ edist (x_1 x) (x_1 y)

Tactic:
.edist (continuous_apply x) (continuous_apply y)

Premises used: continuous_apply, Continuous.edist
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
x : α
h : x ∈ s
y : α
h_1 : y ∈ s
⊢ Continuous[Pi.topologicalSpace, _] fun (x_1 : α → β) ↦ (↑K : ℝ≥0∞) * edist x y

Tactic:
continuous_const

Premises used: continuous_const
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
x : α
h : x ∈ s
y : α
h_1 : y ∈ s
⊢ Continuous[Pi.topologicalSpace, _] fun (x_1 : α → β) ↦ edist (x_1 x) (x_1 y)

Tactic:
exacts [.edist (continuous_apply x) (continuous_apply y), continuous_const]

Premises used: continuous_const
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
⊢ IsClosed[Pi.topologicalSpace] {f : α → β | LipschitzWith K f}

Tactic:
simp only [← lipschitzOnWith_univ, isClosed_setOf_lipschitzOnWith]

Premises used: isClosed_setOf_lipschitzOnWith, lipschitzOnWith_univ
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
s : Set α
K : ℝ≥0
hcont : ContinuousOn f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
hf : LipschitzOnWith K f s
⊢ Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ (↑K : ℝ≥0∞) * x

Tactic:
have := ENNReal.continuous_const_mul (ENNReal.coe_ne_top (r := K))
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
s : Set α
K : ℝ≥0
hcont : ContinuousOn f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
hf : LipschitzOnWith K f s
this : Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ (↑K : ℝ≥0∞) * x
⊢ LipschitzOnWith K f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)

Tactic:
fun x hx ↦ le_on_closure (fun y hy ↦ le_on_closure (fun x hx ↦ hf hx hy) ?_ ?_ hx) ?_ ?_

Premises used: LipschitzOnWith, le_on_closure
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
s : Set α
K : ℝ≥0
hcont : ContinuousOn f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
hf : LipschitzOnWith K f s
this : Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ (↑K : ℝ≥0∞) * x
refine_1 :
  ∀ (x : α) (hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) (y : α) (hy : y ∈ s),
    ContinuousOn (Y := ℝ≥0∞) (fun (x : α) ↦ edist (f x) (f y))
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
refine_2 :
  ∀ (x : α) (hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) (y : α) (hy : y ∈ s),
    ContinuousOn (Y := ℝ≥0∞) (fun (x : α) ↦ (↑K : ℝ≥0∞) * edist x y)
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
refine_3 :
  ∀ (x : α) (hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s),
    ContinuousOn (Y := ℝ≥0∞) (fun (y : α) ↦ edist (f x) (f y))
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
refine_4 :
  ∀ (x : α) (hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s),
    ContinuousOn (Y := ℝ≥0∞) (fun (y : α) ↦ (↑K : ℝ≥0∞) * edist x y)
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
⊢ LipschitzOnWith K f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)

Tactic:
refine fun x hx ↦ le_on_closure (fun y hy ↦ le_on_closure (fun x hx ↦ hf hx hy) ?_ ?_ hx) ?_ ?_

Premises used: le_on_closure