awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
x : α × β
⊢ Membership.mem (γ := Set (α × β)) (Metric.ball 0 (dist x 0 + 1)) x

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
x : α × β
⊢ Metric.ball 0 (dist x 0 + 1) ∈ 𝓝 x

Tactic:
exact Metric.isOpen_ball.mem_nhds (by simp)

Premises used: Metric.isOpen_ball, IsOpen.mem_nhds
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
⊢ UniformContinuousConstSMul α β

Tactic:
⟨fun c => ((lipschitzWith_iff_dist_le_mul (K := nndist c 0)).2 fun _ _ =>
    dist_smul_pair c _ _).uniformContinuous⟩

Premises used: Iff.mpr, UniformContinuousConstSMul.mk, LipschitzWith.uniformContinuous, lipschitzWith_iff_dist_le_mul, dist_smul_pair
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
h : AntilipschitzWith K f
x y : α
⊢ edist x y < ∞

Tactic:
(h x y).trans_lt <| ENNReal.mul_lt_top ENNReal.coe_lt_top (edist_lt_top _ _)

Premises used: ENNReal.mul_lt_top, edist_lt_top, LE.le.trans_lt, ENNReal.coe_lt_top
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
h : AntilipschitzWith K f
x y : α
⊢ edist x y ≠ ∞

Tactic:
(h.edist_lt_top x y).ne

Premises used: AntilipschitzWith.edist_lt_top, LT.lt.ne
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
simp :
  (∀ (x y : α), (↑(nndist x y) : ℝ≥0∞) ≤ (↑K : ℝ≥0∞) * (↑(nndist (f x) (f y)) : ℝ≥0∞)) ↔
    ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)
⊢ AntilipschitzWith K f ↔ ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)

Tactic:
simp only [AntilipschitzWith, edist_nndist]

Premises used: edist_nndist, AntilipschitzWith
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  (∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)) ↔ ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)
⊢ (∀ (x y : α), (↑(nndist x y) : ℝ≥0∞) ≤ (↑K : ℝ≥0∞) * (↑(nndist (f x) (f y)) : ℝ≥0∞)) ↔
    ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)

Tactic:
norm_cast
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
simp :
  (∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)) ↔
    ∀ (x y : α), (↑(nndist x y) : ℝ) ≤ (↑K : ℝ) * (↑(nndist (f x) (f y)) : ℝ)
⊢ AntilipschitzWith K f ↔ ∀ (x y : α), dist x y ≤ (↑K : ℝ) * dist (f x) (f y)

Tactic:
simp only [antilipschitzWith_iff_le_mul_nndist, dist_nndist]

Premises used: antilipschitzWith_iff_le_mul_nndist, dist_nndist
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  (∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)) ↔ ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)
⊢ (∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)) ↔
    ∀ (x y : α), (↑(nndist x y) : ℝ) ≤ (↑K : ℝ) * (↑(nndist (f x) (f y)) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ K⁻¹ * nndist x y ≤ nndist (f x) (f y)

Tactic:
simpa only [div_eq_inv_mul] using NNReal.div_le_of_le_mul' (hf.le_mul_nndist x y)

Premises used: AntilipschitzWith.le_mul_nndist, NNReal.div_le_of_le_mul', div_eq_inv_mul
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ (↑K⁻¹ : ℝ) * dist x y ≤ dist (f x) (f y)

Tactic:
mod_cast hf.mul_le_nndist x y

Premises used: AntilipschitzWith.mul_le_nndist, HMul.hMul, cast, LE.le, Inv.inv, Eq.refl, Dist.dist, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_4
β : Type u_5
inst : EMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
h : f x = f y
⊢ x = y

Tactic:
simpa only [h, edist_self, mul_zero, edist_le_zero] using hf x y

Premises used: PseudoEMetricSpace.edist_self, MulZeroClass.mul_zero, edist_le_zero
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
rw : edist x y / (↑K : ℝ≥0∞) ≤ edist (f x) (f y)
⊢ (↑K : ℝ≥0∞)⁻¹ * edist x y ≤ edist (f x) (f y)

Tactic:
rw [mul_comm, ← div_eq_mul_inv]

Premises used: div_eq_mul_inv, mul_comm
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ edist x y / (↑K : ℝ≥0∞) ≤ edist (f x) (f y)

Tactic:
ENNReal.div_le_of_le_mul' (hf x y)

Premises used: ENNReal.div_le_of_le_mul'
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ edist x y / (↑K : ℝ≥0∞) ≤ edist (f x) (f y)

Tactic:
exact ENNReal.div_le_of_le_mul' (hf x y)

Premises used: ENNReal.div_le_of_le_mul'
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
s : Set β
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
grw : (↑K : ℝ≥0∞) * edist (f x) (f y) ≤ (↑K : ℝ≥0∞) * ediam s
grw₁ grw₂ : (↑K : ℝ≥0∞) * ediam s ≤ (↑K : ℝ≥0∞) * ediam s
⊢ edist x y ≤ (↑K : ℝ≥0∞) * ediam s

Tactic:
grw [hf x y, edist_le_ediam_of_mem (mem_preimage.1 hx) hy]

Premises used: Metric.edist_le_ediam_of_mem, Iff.mp, Set.mem_preimage
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
s : Set α
⊢ ediam s ≤ (↑K : ℝ≥0∞) * ediam (f '' s)

Tactic:
(ediam_mono (subset_preimage_image _ _)).trans (hf.ediam_preimage_le (f '' s))

Premises used: Metric.ediam_mono, Set.image, LE.le.trans, Set.subset_preimage_image, AntilipschitzWith.ediam_preimage_le
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y : α
⊢ edist x y ≤ (↑1 : ℝ≥0∞) * edist (id x) (id y)

Tactic:
simp only [ENNReal.coe_one, one_mul, id, le_refl]

Premises used: le_refl, id, ENNReal.coe_one, one_mul
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
Kg : ℝ≥0
g : β → γ
hg : AntilipschitzWith Kg g
Kf : ℝ≥0
f : α → β
hf : AntilipschitzWith Kf f
x y : α
rw :
  (↑Kf : ℝ≥0∞) * ((↑Kg : ℝ≥0∞) * edist (g (f x)) (g (f y))) =
    (↑Kf : ℝ≥0∞) * ((↑Kg : ℝ≥0∞) * edist ((g ∘ f) x) ((g ∘ f) y))
⊢ (↑Kf : ℝ≥0∞) * ((↑Kg : ℝ≥0∞) * edist (g (f x)) (g (f y))) = (↑(Kf * Kg) : ℝ≥0∞) * edist ((g ∘ f) x) ((g ∘ f) y)

Tactic:
rw [ENNReal.coe_mul, mul_assoc]

Premises used: mul_assoc, ENNReal.coe_mul
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
Kg : ℝ≥0
g : β → γ
hg : AntilipschitzWith Kg g
Kf : ℝ≥0
f : α → β
hf : AntilipschitzWith Kf f
x y : α
⊢ (↑Kf : ℝ≥0∞) * ((↑Kg : ℝ≥0∞) * edist (g (f x)) (g (f y))) =
    (↑Kf : ℝ≥0∞) * ((↑Kg : ℝ≥0∞) * edist ((g ∘ f) x) ((g ∘ f) y))

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
s : Set α
⊢ AntilipschitzWith K (s.restrict (π := fun (a : α) ↦ β) f)

Tactic:
fun x y => hf x y

Premises used: Set.restrict, Subtype.val, AntilipschitzWith
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
s : Set β
hs : ∀ (x : α), f x ∈ s
⊢ AntilipschitzWith K (Set.codRestrict f s hs)

Tactic:
fun x y => hf x y

Premises used: AntilipschitzWith
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
s : Set α
hf : AntilipschitzWith K (s.restrict (π := fun (a : α) ↦ β) f)
g : β → α
t : Set β
g_maps : MapsTo g t s
g_inv : RightInvOn g f t
x y : (↑t : Type u_2)
⊢ edist (t.restrict (π := fun (a : β) ↦ α) g x) (t.restrict (π := fun (a : β) ↦ α) g y) ≤ (↑K : ℝ≥0∞) * edist x y

Tactic:
simpa only [restrict_apply, g_inv x.mem, g_inv y.mem, Subtype.edist_mk_mk]
    using hf ⟨g x, g_maps x.mem⟩ ⟨g y, g_maps y.mem⟩

Premises used: Set.restrict_apply, Subtype.mk, Subtype.mem, Subtype.edist_mk_mk, Subtype.val
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
g : β → α
t : Set β
h : RightInvOn g f t
⊢ LipschitzWith K (t.restrict (π := fun (a : β) ↦ α) g)

Tactic:
(hf.restrict univ).to_rightInvOn' (mapsTo_univ g t) h

Premises used: Set.mapsTo_univ, Set.univ, AntilipschitzWith.to_rightInvOn', AntilipschitzWith.restrict
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
g : β → α
hg : Function.RightInverse g f
x y : β
⊢ edist (g x) (g y) ≤ (↑K : ℝ≥0∞) * edist (f (g x)) (f (g y))

Tactic:
have := hf (g x) (g y)
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
g : β → α
hg : Function.RightInverse g f
x y : β
this : edist (g x) (g y) ≤ (↑K : ℝ≥0∞) * edist (f (g x)) (f (g y))
rwa : ∀ (this : edist (g x) (g y) ≤ (↑K : ℝ≥0∞) * edist x (f (g y))), edist (g x) (g y) ≤ (↑K : ℝ≥0∞) * edist x y
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : edist (g x) (g y) ≤ (↑K : ℝ≥0∞) * edist x y), edist (g x) (g y) ≤ (↑K : ℝ≥0∞) * edist x y
⊢ edist (g x) (g y) ≤ (↑K : ℝ≥0∞) * edist x y

Tactic:
rwa [hg x, hg y] at this
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
⊢ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α

Tactic:
((uniformity_basis_edist.comap _).le_basis_iff uniformity_basis_edist).2 fun ε h₀ => ?_

Premises used: Iff.mpr, uniformity_basis_edist, Filter.HasBasis.le_basis_iff, Filter.HasBasis.comap
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
refine :
  ∀ (ε : ℝ≥0∞) (h₀ : 0 < ε),
    ∃ (i : ℝ≥0∞), 0 < i ∧ Prod.map f f ⁻¹' {p : β × β | edist p.1 p.2 < i} ⊆ {p : α × α | edist p.1 p.2 < ε}
⊢ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α

Tactic:
refine ((uniformity_basis_edist.comap _).le_basis_iff uniformity_basis_edist).2 fun ε h₀ => ?_

Premises used: Iff.mpr, uniformity_basis_edist, Filter.HasBasis.le_basis_iff, Filter.HasBasis.comap
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
⊢ ∃ (i : ℝ≥0∞), 0 < i ∧ Prod.map f f ⁻¹' {p : β × β | edist p.1 p.2 < i} ⊆ {p : α × α | edist p.1 p.2 < ε}

Tactic:
⟨(↑K)⁻¹ * ε, ENNReal.mul_pos (ENNReal.inv_ne_zero.2 ENNReal.coe_ne_top) h₀.ne', ?_⟩

Premises used: Iff.mpr, HMul.hMul, ENNReal.mul_pos, LT.lt.ne', ENNReal.inv_ne_zero, Inv.inv, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
refine : Prod.map f f ⁻¹' {p : β × β | edist p.1 p.2 < (↑K : ℝ≥0∞)⁻¹ * ε} ⊆ {p : α × α | edist p.1 p.2 < ε}
⊢ ∃ (i : ℝ≥0∞), 0 < i ∧ Prod.map f f ⁻¹' {p : β × β | edist p.1 p.2 < i} ⊆ {p : α × α | edist p.1 p.2 < ε}

Tactic:
refine ⟨(↑K)⁻¹ * ε, ENNReal.mul_pos (ENNReal.inv_ne_zero.2 ENNReal.coe_ne_top) h₀.ne', ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
⊢ Prod.map f f ⁻¹' {p : β × β | edist p.1 p.2 < (↑K : ℝ≥0∞)⁻¹ * ε} ⊆ {p : α × α | edist p.1 p.2 < ε}

Tactic:
fun x hx => (hf x.1 x.2).trans_lt ?_

Premises used: Set.Mem, setOf, Set.Subset, Prod.fst, LE.le.trans_lt, Prod.snd
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
refine :
  ∀ (x : α × α) (hx : x ∈ Prod.map f f ⁻¹' {p : β × β | edist p.1 p.2 < (↑K : ℝ≥0∞)⁻¹ * ε}),
    (↑K : ℝ≥0∞) * edist (f x.1) (f x.2) < ε
⊢ Prod.map f f ⁻¹' {p : β × β | edist p.1 p.2 < (↑K : ℝ≥0∞)⁻¹ * ε} ⊆ {p : α × α | edist p.1 p.2 < ε}

Tactic:
refine fun x hx => (hf x.1 x.2).trans_lt ?_

Premises used: LE.le.trans_lt
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
x : α × α
hx : x ∈ Prod.map f f ⁻¹' {p : β × β | edist p.1 p.2 < (↑K : ℝ≥0∞)⁻¹ * ε}
⊢ x ∈ Prod.map f f ⁻¹' {p : β × β | edist p.1 p.2 < ε / (↑K : ℝ≥0∞)}

Tactic:
rw [mul_comm, ← div_eq_mul_inv] at hx

Premises used: div_eq_mul_inv, mul_comm
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
x : α × α
hx : x ∈ Prod.map f f ⁻¹' {p : β × β | edist p.1 p.2 < ε / (↑K : ℝ≥0∞)}
rw : edist (f x.1) (f x.2) * (↑K : ℝ≥0∞) < ε
⊢ (↑K : ℝ≥0∞) * edist (f x.1) (f x.2) < ε

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
x : α × α
hx : x ∈ Prod.map f f ⁻¹' {p : β × β | edist p.1 p.2 < ε / (↑K : ℝ≥0∞)}
⊢ edist (f x.1) (f x.2) * (↑K : ℝ≥0∞) < ε

Tactic:
ENNReal.mul_lt_of_lt_div hx

Premises used: ENNReal.mul_lt_of_lt_div
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
x : α × α
hx : x ∈ Prod.map f f ⁻¹' {p : β × β | edist p.1 p.2 < ε / (↑K : ℝ≥0∞)}
⊢ edist (f x.1) (f x.2) * (↑K : ℝ≥0∞) < ε

Tactic:
exact ENNReal.mul_lt_of_lt_div hx

Premises used: ENNReal.mul_lt_of_lt_div
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
hfc : UniformContinuous f
⊢ IsUniformInducing f

Tactic:
⟨le_antisymm hf.comap_uniformity_le hfc.le_comap⟩

Premises used: Filter.Tendsto.le_comap, le_antisymm, IsUniformInducing.mk, AntilipschitzWith.comap_uniformity_le
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_4
β : Type u_5
inst : EMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
hfc : UniformContinuous f
⊢ IsUniformEmbedding f

Tactic:
⟨hf.isUniformInducing hfc, hf.injective⟩

Premises used: AntilipschitzWith.isUniformInducing, AntilipschitzWith.injective, IsUniformEmbedding.mk
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x : α
simp : comap f (comap (Prod.mk (f x)) (𝓤 β)) ≤ comap (Prod.mk x) (𝓤 α)
⊢ comap f (𝓝 (f x)) ≤ 𝓝 x

Tactic:
simp only [nhds_eq_comap_uniformity]

Premises used: nhds_eq_comap_uniformity
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x : α
grw : comap f (comap (Prod.mk (f x)) (𝓤 β)) ≤ comap (Prod.mk x) (comap (Prod.map f f) (𝓤 β))
⊢ comap f (comap (Prod.mk (f x)) (𝓤 β)) ≤ comap (Prod.mk x) (𝓤 α)

Tactic:
grw [← hf.comap_uniformity_le]

Premises used: AntilipschitzWith.comap_uniformity_le
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x : α
⊢ comap f (comap (Prod.mk (f x)) (𝓤 β)) ≤ comap (Prod.mk x) (comap (Prod.map f f) (𝓤 β))

Tactic:
simp [comap_comap, Function.comp_def]

Premises used: Function.comp_def, Filter.comap_comap
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
hfc :
  Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    f
⊢ IsInducing f

Tactic:
isInducing_iff_nhds.mpr fun x ↦ le_antisymm (hfc.tendsto x).le_comap <| hf.comap_nhds_le _

Premises used: Iff.mpr, Filter.Tendsto.le_comap, Continuous.tendsto, le_antisymm, Topology.isInducing_iff_nhds, AntilipschitzWith.comap_nhds_le
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_4
β : Type u_5
inst : EMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
hfc :
  Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    f
⊢ IsEmbedding f

Tactic:
hf.isInducing hfc |>.isEmbedding

Premises used: AntilipschitzWith.isInducing, Topology.IsInducing.isEmbedding
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
inst_2 : CompleteSpace α
hf : AntilipschitzWith K f
hfc : UniformContinuous f
⊢ IsComplete (range f)

Tactic:
(hf.isUniformInducing hfc).isComplete_range

Premises used: AntilipschitzWith.isUniformInducing, IsUniformInducing.isComplete_range
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : EMetricSpace β
inst_2 : CompleteSpace α
f : α → β
K : ℝ≥0
hf : AntilipschitzWith K f
hfc : UniformContinuous f
⊢ IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (range f)

Tactic:
(hf.isComplete_range hfc).isClosed

Premises used: IsComplete.isClosed, AntilipschitzWith.isComplete_range
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_4
β : Type u_5
inst : EMetricSpace α
inst_1 : EMetricSpace β
K : ℝ≥0
f : α → β
inst_2 : CompleteSpace α
hf : AntilipschitzWith K f
hfc : UniformContinuous f
⊢ IsClosedEmbedding f

Tactic:
{ (hf.isUniformEmbedding hfc).isEmbedding with isClosed_range := hf.isClosed_range hfc }

Premises used: AntilipschitzWith.isClosed_range, AntilipschitzWith.isUniformEmbedding, IsUniformEmbedding.isEmbedding, Topology.IsClosedEmbedding.mk
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s : Set α
⊢ AntilipschitzWith.{u_1, u_1} (α := { x : α // x ∈ s }) 1 (Subtype.val (p := fun (x : α) ↦ x ∈ s))

Tactic:
AntilipschitzWith.id.restrict s

Premises used: AntilipschitzWith.id, AntilipschitzWith.restrict, Set.restrict
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
inst_2 : Subsingleton α
K : ℝ≥0
x y : α
⊢ edist x y ≤ (↑K : ℝ≥0∞) * edist (f x) (f y)

Tactic:
simp only [Subsingleton.elim x y, edist_self, zero_le]

Premises used: zero_le, PseudoEMetricSpace.edist_self, Subsingleton.elim
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_4
β : Type u_5
inst : EMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
h : AntilipschitzWith 0 f
⊢ Subsingleton α

Tactic:
⟨fun x y => edist_le_zero.1 <| (h x y).trans_eq <| zero_mul _⟩

Premises used: LE.le.trans_eq, MulZeroClass.zero_mul, Subsingleton.intro, edist_le_zero, Iff.mp, EDist.edist
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
β : Type u_2
inst : PseudoEMetricSpace β
K : ℝ≥0
α : Type u_4
inst_1 : EMetricSpace α
inst_2 : Nontrivial α
f : α → β
hf : AntilipschitzWith K f
by_contra! : ∀ (h₀ : K ≤ 0), False
⊢ 0 < K

Tactic:
by_contra! h₀
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
β : Type u_2
inst : PseudoEMetricSpace β
K : ℝ≥0
α : Type u_4
inst_1 : EMetricSpace α
inst_2 : Nontrivial α
f : α → β
hf : AntilipschitzWith K f
h₀ : K ≤ 0
rwa rwa₁ rwa₂ rwa₃ : ∀ (h₀ : K = 0), K = 0
⊢ K = 0

Tactic:
rwa [le_zero_iff] at h₀

Premises used: le_zero_iff
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
β : Type u_2
inst : PseudoEMetricSpace β
K : ℝ≥0
α : Type u_4
inst_1 : EMetricSpace α
inst_2 : Nontrivial α
f : α → β
hf : AntilipschitzWith K f
h₀ : K ≤ 0
⊢ AntilipschitzWith 0 f

Tactic:
obtain rfl : K = 0 := by rwa [le_zero_iff] at h₀

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
β : Type u_2
inst : PseudoEMetricSpace β
K : ℝ≥0
α : Type u_4
inst_1 : EMetricSpace α
inst_2 : Nontrivial α
f : α → β
hf : AntilipschitzWith K f
h₀ : K ≤ 0
hf₁ : AntilipschitzWith 0 f
⊢ LE.le (α := ℝ≥0) 0 0

Tactic:
obtain rfl : K = 0 := by rwa [le_zero_iff] at h₀

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
β : Type u_2
inst : PseudoEMetricSpace β
α : Type u_4
inst_1 : EMetricSpace α
inst_2 : Nontrivial α
f : α → β
hf : AntilipschitzWith 0 f
h₀ : LE.le (α := ℝ≥0) 0 0
⊢ False

Tactic:
not_subsingleton α hf.subsingleton

Premises used: AntilipschitzWith.subsingleton, not_subsingleton
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
β : Type u_2
inst : PseudoEMetricSpace β
α : Type u_4
inst_1 : EMetricSpace α
inst_2 : Nontrivial α
f : α → β
hf : AntilipschitzWith 0 f
h₀ : LE.le (α := ℝ≥0) 0 0
⊢ False

Tactic:
exact not_subsingleton α hf.subsingleton

Premises used: AntilipschitzWith.subsingleton, not_subsingleton
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
s : Set β
hs : Bornology.IsBounded s
⊢ Bornology.IsBounded (f ⁻¹' s)

Tactic:
isBounded_iff_ediam_ne_top.2 <| ne_top_of_le_ne_top
    (ENNReal.mul_ne_top ENNReal.coe_ne_top hs.ediam_ne_top) (hf.ediam_preimage_le _)

Premises used: Iff.mpr, Metric.isBounded_iff_ediam_ne_top, Bornology.IsBounded.ediam_ne_top, ENNReal.mul_ne_top, ne_top_of_le_ne_top, AntilipschitzWith.ediam_preimage_le, ENNReal.coe_ne_top
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
⊢ Tendsto f (cobounded α) (cobounded β)

Tactic:
compl_surjective.forall.2 fun _ ↦ hf.isBounded_preimage

Premises used: Iff.mpr, Function.Surjective.forall, AntilipschitzWith.isBounded_preimage, compl_surjective, Filter.Tendsto