awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
β : Type u_2
inst : PseudoMetricSpace β
α : Type u_4
inst_1 : MetricSpace α
K : ℝ≥0
f : α → β
inst_2 : ProperSpace α
hK : AntilipschitzWith K f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
⊢ ProperSpace β

Tactic:
⟨fun x₀ r => ?_⟩

Premises used: ProperSpace.mk
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
β : Type u_2
inst : PseudoMetricSpace β
α : Type u_4
inst_1 : MetricSpace α
K : ℝ≥0
f : α → β
inst_2 : ProperSpace α
hK : AntilipschitzWith K f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
refine : ∀ (x₀ : β) (r : ℝ), IsCompact (closedBall x₀ r)
⊢ ProperSpace β

Tactic:
refine ⟨fun x₀ r => ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
β : Type u_2
inst : PseudoMetricSpace β
α : Type u_4
inst_1 : MetricSpace α
K_1 : ℝ≥0
f : α → β
inst_2 : ProperSpace α
hK : AntilipschitzWith K_1 f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K

Tactic:
have A : IsClosed K := isClosed_closedBall.preimage f_cont
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
β : Type u_2
inst : PseudoMetricSpace β
α : Type u_4
inst_1 : MetricSpace α
K_1 : ℝ≥0
f : α → β
inst_2 : ProperSpace α
hK : AntilipschitzWith K_1 f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K
⊢ Bornology.IsBounded K

Tactic:
have B : IsBounded K := hK.isBounded_preimage isBounded_closedBall
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
β : Type u_2
inst : PseudoMetricSpace β
α : Type u_4
inst_1 : MetricSpace α
K_1 : ℝ≥0
f : α → β
inst_2 : ProperSpace α
hK : AntilipschitzWith K_1 f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K
B : Bornology.IsBounded K
⊢ IsCompact K

Tactic:
have : IsCompact K := isCompact_iff_isClosed_bounded.2 ⟨A, B⟩
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
β : Type u_2
inst : PseudoMetricSpace β
α : Type u_4
inst_1 : MetricSpace α
K_1 : ℝ≥0
f : α → β
inst_2 : ProperSpace α
hK : AntilipschitzWith K_1 f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K
B : Bornology.IsBounded K
this : IsCompact K
⊢ IsCompact (f '' K)

Tactic:
this.image f_cont

Premises used: IsCompact.image
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
β : Type u_2
inst : PseudoMetricSpace β
α : Type u_4
inst_1 : MetricSpace α
K_1 : ℝ≥0
f : α → β
inst_2 : ProperSpace α
hK : AntilipschitzWith K_1 f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K
B : Bornology.IsBounded K
this : IsCompact K
h : closedBall x₀ r = f '' K
⊢ IsCompact (closedBall x₀ r)

Tactic:
convert! this.image f_cont

Premises used: IsCompact.image
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
β : Type u_2
inst : PseudoMetricSpace β
α : Type u_4
inst_1 : MetricSpace α
K_1 : ℝ≥0
f : α → β
inst_2 : ProperSpace α
hK : AntilipschitzWith K_1 f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K
B : Bornology.IsBounded K
this : IsCompact K
⊢ closedBall x₀ r = f '' K

Tactic:
(hf.image_preimage _).symm

Premises used: Function.Surjective.image_preimage, Eq.symm
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
β : Type u_2
inst : PseudoMetricSpace β
α : Type u_4
inst_1 : MetricSpace α
K_1 : ℝ≥0
f : α → β
inst_2 : ProperSpace α
hK : AntilipschitzWith K_1 f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K
B : Bornology.IsBounded K
this : IsCompact K
⊢ closedBall x₀ r = f '' K

Tactic:
exact (hf.image_preimage _).symm

Premises used: Function.Surjective.image_preimage, Eq.symm
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith.{u_1, u_3} (β := γ) K₁ fun (a : α) ↦ f a b
s : Set α
t : Set β
hst : Bornology.IsBounded (image2 f s t)
contrapose! : ∀ (hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t), ¬Bornology.IsBounded (image2 f s t)
⊢ Bornology.IsBounded s ∨ Bornology.IsBounded t

Tactic:
contrapose! hst
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith.{u_1, u_3} (β := γ) K₁ fun (a : α) ↦ f a b
s : Set α
t : Set β
hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t
⊢ t.Nonempty

Tactic:
nonempty_of_not_isBounded hst.2

Premises used: Bornology.nonempty_of_not_isBounded, And.right
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith.{u_1, u_3} (β := γ) K₁ fun (a : α) ↦ f a b
s : Set α
t : Set β
hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t
obtain : ∀ (b : β) (hb : b ∈ t), ¬Bornology.IsBounded (image2 f s t)
⊢ ¬Bornology.IsBounded (image2 f s t)

Tactic:
obtain ⟨b, hb⟩ : t.Nonempty := nonempty_of_not_isBounded hst.2

Premises used: Set.Nonempty, Bornology.nonempty_of_not_isBounded, And.right
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith.{u_1, u_3} (β := γ) K₁ fun (a : α) ↦ f a b
s : Set α
t : Set β
hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t
b : β
hb : b ∈ t
h : Bornology.IsBounded (image2 f s {b})
apply : Bornology.IsBounded s
⊢ False

Tactic:
apply hst.1

Premises used: And.left
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith.{u_1, u_3} (β := γ) K₁ fun (a : α) ↦ f a b
s : Set α
t : Set β
hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t
b : β
hb : b ∈ t
h : Bornology.IsBounded (image2 f s {b})
⊢ Bornology.IsBounded.{u_3} (α := γ) ((fun (a : α) ↦ f a b) '' s)

Tactic:
rw [Set.image2_singleton_right] at h

Premises used: Set.image2_singleton_right
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith.{u_1, u_3} (β := γ) K₁ fun (a : α) ↦ f a b
s : Set α
t : Set β
hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t
b : β
hb : b ∈ t
h : Bornology.IsBounded.{u_3} (α := γ) ((fun (a : α) ↦ f a b) '' s)
⊢ Bornology.IsBounded.{u_1} (α := α) (preimage.{u_1, u_3} (β := γ) (fun (a : α) ↦ f a b) ((fun (a : α) ↦ f a b) '' s))

Tactic:
replace h := (hf b).isBounded_preimage h
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith.{u_1, u_3} (β := γ) K₁ fun (a : α) ↦ f a b
s : Set α
t : Set β
hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t
b : β
hb : b ∈ t
h : Bornology.IsBounded.{u_1} (α := α) (preimage.{u_1, u_3} (β := γ) (fun (a : α) ↦ f a b) ((fun (a : α) ↦ f a b) '' s))
⊢ Bornology.IsBounded s

Tactic:
h.subset (subset_preimage_image _ _)

Premises used: Bornology.IsBounded.subset, Set.subset_preimage_image
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith.{u_1, u_3} (β := γ) K₁ fun (a : α) ↦ f a b
s : Set α
t : Set β
hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t
b : β
hb : b ∈ t
h : Bornology.IsBounded.{u_1} (α := α) (preimage.{u_1, u_3} (β := γ) (fun (a : α) ↦ f a b) ((fun (a : α) ↦ f a b) '' s))
⊢ Bornology.IsBounded s

Tactic:
exact h.subset (subset_preimage_image _ _)

Premises used: Bornology.IsBounded.subset, Set.subset_preimage_image
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith.{u_1, u_3} (β := γ) K₁ fun (a : α) ↦ f a b
s : Set α
t : Set β
hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t
b : β
hb : b ∈ t
⊢ ¬Bornology.IsBounded (image2 f s {b})

Tactic:
have : ¬IsBounded (Set.image2 f s {b}) := by
    intro h
    apply hst.1
    rw [Set.image2_singleton_right] at h
    replace h := (hf b).isBounded_preimage h
    exact h.subset (subset_preimage_image _ _)
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith.{u_1, u_3} (β := γ) K₁ fun (a : α) ↦ f a b
s : Set α
t : Set β
hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t
b : β
hb : b ∈ t
this : ¬Bornology.IsBounded (image2 f s {b})
⊢ ¬Bornology.IsBounded (image2 f s t)

Tactic:
mt (IsBounded.subset · (image2_subset subset_rfl (singleton_subset_iff.mpr hb))) this

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.image2_subset, mt, Bornology.IsBounded.subset, subset_rfl
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith.{u_1, u_3} (β := γ) K₁ fun (a : α) ↦ f a b
s : Set α
t : Set β
hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t
b : β
hb : b ∈ t
this : ¬Bornology.IsBounded (image2 f s {b})
⊢ ¬Bornology.IsBounded (image2 f s t)

Tactic:
exact mt (IsBounded.subset · (image2_subset subset_rfl (singleton_subset_iff.mpr hb))) this

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.image2_subset, mt, Bornology.IsBounded.subset, subset_rfl
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f : α → β → γ
K₂ : ℝ≥0
hf : ∀ (a : α), AntilipschitzWith K₂ (f a)
s : Set α
t : Set β
hst : Bornology.IsBounded (image2 f s t)
⊢ Bornology.IsBounded s ∨ Bornology.IsBounded t

Tactic:
Or.symm <| isBounded_of_image2_left (flip f) hf <| image2_swap f s t ▸ hst

Premises used: AntilipschitzWith.isBounded_of_image2_left, Eq.rec, flip, Or.symm, Set.image2_swap
-- Module: Mathlib.Topology.MetricSpace.Antilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
g : β → α
hg : Function.RightInverse g f
x y : β
⊢ edist x y ≤ (↑K : ℝ≥0∞) * edist (g x) (g y)

Tactic:
simpa only [hg _] using hf (g x) (g y)
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
β : Type v
γ : Type w
inst : MetricSpace γ
inst_1 : PseudoMetricSpace β
f : γ → β
rw :
  IsUniformInducing f ↔
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ
rw₁ :
  (UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ) ↔
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ
rw₂ rw₃ :
  ((∀ ε > 0, ∃ δ > 0, ∀ ⦃a b : γ⦄, dist a b < δ → dist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ) ↔
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ
⊢ IsUniformEmbedding f ↔
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ

Tactic:
rw [isUniformEmbedding_iff_isUniformInducing, isUniformInducing_iff, uniformContinuous_iff]

Premises used: Metric.isUniformInducing_iff, isUniformEmbedding_iff_isUniformInducing, Metric.uniformContinuous_iff
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
γ : Type w
inst : MetricSpace γ
s : Set γ
ε : ℝ
hε : 0 < ε
hs : s.Pairwise fun (x y : γ) ↦ ε ≤ dist x y
⊢ s.Pairwise fun (x y : γ) ↦ (x, y) ∉ {p : γ × γ | dist p.1 p.2 < ε}

Tactic:
simpa using hs
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
γ : Type w
inst : MetricSpace γ
α : Type u_2
inst_1 : TopologicalSpace α
inst_2 : DiscreteTopology α
ε : ℝ
hε : 0 < ε
f : α → γ
hf : Pairwise fun (x y : α) ↦ ε ≤ dist (f x) (f y)
⊢ Pairwise fun (x y : α) ↦ (f x, f y) ∉ {p : γ × γ | dist p.1 p.2 < ε}

Tactic:
simpa using hf
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β_1 : Type v
X : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
x : γ
s : Set γ
β : Type u_2
ε : ℝ
hε : 0 < ε
f : β → α
hf : Pairwise fun (x y : β) ↦ ε ≤ dist (f x) (f y)
⊢ UniformSpace α

Tactic:
infer_instance
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
β : Type u_2
ε : ℝ
hε : 0 < ε
f : β → α
hf : Pairwise fun (x y : β) ↦ ε ≤ dist (f x) (f y)
⊢ Pairwise fun (x y : β) ↦ (f x, f y) ∉ {p : α × α | dist p.1 p.2 < ε}

Tactic:
simpa using hf
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α_1 : Type u
β : Type v
X : Type u_1
inst : PseudoMetricSpace α_1
γ : Type w
inst_1 : MetricSpace γ
α : Type u
inst_2 : EMetricSpace α
h : ∀ (x y : α), edist x y ≠ ⊤
⊢ ∀ (x y : α), LE.le (α := ℝ) 0 ((fun (x1 x2 : α) ↦ (edist x1 x2).toReal) x y)

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α_1 : Type u
β : Type v
X : Type u_1
inst : PseudoMetricSpace α_1
γ : Type w
inst_1 : MetricSpace γ
α : Type u
inst_2 : EMetricSpace α
h : ∀ (x y : α), edist x y ≠ ⊤
⊢ ∀ (x y : α), edist x y = ENNReal.ofReal ((fun (x1 x2 : α) ↦ (edist x1 x2).toReal) x y)

Tactic:
simp [h]
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
⊢ IsUniformEmbedding toReal

Tactic:
isUniformEmbedding_subtype_val

Premises used: NNReal, NNReal.toReal, isUniformEmbedding_subtype_val
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
⊢ IsEmbedding toReal

Tactic:
isUniformEmbedding_coe.isEmbedding

Premises used: NNReal.isUniformEmbedding_coe, IsUniformEmbedding.isEmbedding
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
⊢ IsClosedEmbedding toReal

Tactic:
isClosed_Ici.isClosedEmbedding_subtypeVal

Premises used: Set.Ici, Set.Mem, NNReal, IsClosed.isClosedEmbedding_subtypeVal, NNReal.toReal, isClosed_Ici
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
H : ∀ ε > 0, ∃ (β : Type u_2) (x : Encodable β) (F : α → β), ∀ (x y : α), F x = F y → dist x y ≤ ε
⊢ SecondCountableTopology α

Tactic:
secondCountable_of_almost_dense_set fun ε ε0 => ?_

Premises used: Metric.secondCountable_of_almost_dense_set
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
H : ∀ ε > 0, ∃ (β : Type u_2) (x : Encodable β) (F : α → β), ∀ (x y : α), F x = F y → dist x y ≤ ε
refine : ∀ (ε : ℝ) (ε0 : ε > 0), ∃ (s : Set α), s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
⊢ SecondCountableTopology α

Tactic:
refine secondCountable_of_almost_dense_set fun ε ε0 => ?_

Premises used: Metric.secondCountable_of_almost_dense_set
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
H : ∀ ε > 0, ∃ (β : Type u_2) (x : Encodable β) (F : α → β), ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
rcases :
  ∀ (β : Type u_2) (fβ : Encodable β) (F : α → β) (hF : ∀ (x y : α), F x = F y → dist x y ≤ ε),
    ∃ (s : Set α), s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
⊢ ∃ (s : Set α), s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε

Tactic:
rcases H ε ε0 with ⟨β, fβ, F, hF⟩
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
H : ∀ ε > 0, ∃ (β : Type u_2) (x : Encodable β) (F : α → β), ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_2
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : (↑(range F) : Type u_2) → α := rangeSplitting F
⊢ ∃ (s : Set α), s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε

Tactic:
⟨range Finv, ⟨countable_range _, fun x => ?_⟩⟩

Premises used: Set.countable_range, And.intro, Exists.intro, Set.range
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
H : ∀ ε > 0, ∃ (β : Type u_2) (x : Encodable β) (F : α → β), ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_2
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : (↑(range F) : Type u_2) → α := rangeSplitting F
refine : ∀ (x : α), ∃ y ∈ range Finv, dist x y ≤ ε
⊢ ∃ (s : Set α), s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε

Tactic:
refine ⟨range Finv, ⟨countable_range _, fun x => ?_⟩⟩
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
H : ∀ ε > 0, ∃ (β : Type u_2) (x : Encodable β) (F : α → β), ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_2
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : (↑(range F) : Type u_2) → α := rangeSplitting F
x : α
x' : α := Finv (Subtype.mk (p := fun (x : β) ↦ x ∈ range F) (F x) ⋯)
⊢ F x' = F x

Tactic:
have : F x' = F x := apply_rangeSplitting F _
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
H : ∀ ε > 0, ∃ (β : Type u_2) (x : Encodable β) (F : α → β), ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_2
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : (↑(range F) : Type u_2) → α := rangeSplitting F
x : α
x' : α := Finv (Subtype.mk (p := fun (x : β) ↦ x ∈ range F) (F x) ⋯)
this : F x' = F x
⊢ ∃ y ∈ range Finv, dist x y ≤ ε

Tactic:
⟨x', mem_range_self _, hF _ _ this.symm⟩

Premises used: Set.mem_range_self, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
H : ∀ ε > 0, ∃ (β : Type u_2) (x : Encodable β) (F : α → β), ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_2
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : (↑(range F) : Type u_2) → α := rangeSplitting F
x : α
x' : α := Finv (Subtype.mk (p := fun (x : β) ↦ x ∈ range F) (F x) ⋯)
this : F x' = F x
⊢ ∃ y ∈ range Finv, dist x y ≤ ε

Tactic:
exact ⟨x', mem_range_self _, hF _ _ this.symm⟩
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α_1 : Type u
β : Type v
X : Type u_1
inst : PseudoMetricSpace α_1
γ : Type w
inst_1 : MetricSpace γ
α : Type u
inst_2 : PseudoMetricSpace α
x y x' y' : α
hx : Inseparable x x'
hy : Inseparable y y'
rw : (edist x y).toReal = dist x' y'
rw₁ : (edist x y).toReal = (edist x' y').toReal
rw₂ : (edist (α := SeparationQuotient α) (mk x) (mk y)).toReal = (edist x' y').toReal
rw₃ :
  (edist (α := SeparationQuotient α) (mk x) (mk y)).toReal = (edist (α := SeparationQuotient α) (mk x') (mk y')).toReal
rw₄ :
  (edist (α := SeparationQuotient α) (mk x') (mk y)).toReal = (edist (α := SeparationQuotient α) (mk x') (mk y')).toReal
rw₅ rw₆ :
  (edist (α := SeparationQuotient α) (mk x') (mk y')).toReal =
    (edist (α := SeparationQuotient α) (mk x') (mk y')).toReal
⊢ dist x y = dist x' y'

Tactic:
rw [dist_edist, dist_edist, ← edist_mk x,
    ← edist_mk x', mk_eq_mk.2 hx, mk_eq_mk.2 hy]

Premises used: Iff.mpr, SeparationQuotient.mk_eq_mk, SeparationQuotient.edist_mk, dist_edist
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
p q : α
⊢ dist (α := SeparationQuotient α) (mk p) (mk q) = dist p q

Tactic:
rfl

Premises used: SeparationQuotient.lift₂, rfl, Quotient.liftOn₂'
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
X : Type u_2
m : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ ∀ (x : X), d x x = 0

Tactic:
simp [hd]
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
X : Type u_2
m : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ ∀ (x y : X), d x y = d y x

Tactic:
simp [hd, edist_comm]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
X : Type u_2
m : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ ∀ (x y z : X), d x z ≤ d x y + d y z

Tactic:
simp [hd, edist_triangle]

Premises used: PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
X : Type u_2
m : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ 𝓤 X = ⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : X × X | d p.1 p.2 < ε}

Tactic:
simp [hd, uniformity_edist]

Premises used: PseudoEMetricSpace.uniformity_edist
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
X : Type u_2
m : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
h : Eq.{u_2 + 1} (α := X → X → ℝ≥0∞) edist edist
⊢ m.replaceEDist d hd = m

Tactic:
ext : 2
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
X : Type u_2
m : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ Eq.{u_2 + 1} (α := X → X → ℝ≥0∞) edist edist

Tactic:
hd
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
X : Type u_2
m : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ Eq.{u_2 + 1} (α := X → X → ℝ≥0∞) edist edist

Tactic:
exact hd
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
X : Type u_2
m : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ Eq.{u_2 + 1} (α := UniformSpace X) toUniformSpace toUniformSpace

Tactic:
dsimp +instances [replaceEDist]

Premises used: PseudoEMetricSpace.replaceEDist
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ (x : X), d x x = 0

Tactic:
simp [hd]
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ (x y : X), d x y = d y x

Tactic:
simp [hd, dist_comm]

Premises used: PseudoMetricSpace.dist_comm