awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
u : β → α
rw :
  Tendsto (β := ℝ) (fun (x : β × β) ↦ dist (Prod.map u u x).1 (Prod.map u u x).2) atTop (𝓝 0) ↔
    Tendsto (β := ℝ) (fun (n : β × β) ↦ dist (u n.1) (u n.2)) atTop (𝓝 0)
⊢ CauchySeq u ↔ Tendsto (β := ℝ) (fun (n : β × β) ↦ dist (u n.1) (u n.2)) atTop (𝓝 0)

Tactic:
rw [cauchySeq_iff_tendsto, Metric.uniformity_eq_comap_nhds_zero, tendsto_comap_iff,
    Function.comp_def]

Premises used: Filter.tendsto_comap_iff, Function.comp_def, Metric.uniformity_eq_comap_nhds_zero, cauchySeq_iff_tendsto
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
u : β → α
simp_rw :
  Tendsto (β := ℝ) (fun (x : β × β) ↦ dist (u x.1) (Prod.map u u x).2) atTop (𝓝 0) ↔
    Tendsto (β := ℝ) (fun (n : β × β) ↦ dist (u n.1) (u n.2)) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : β × β) ↦ dist (Prod.map u u x).1 (Prod.map u u x).2) atTop (𝓝 0) ↔
    Tendsto (β := ℝ) (fun (n : β × β) ↦ dist (u n.1) (u n.2)) atTop (𝓝 0)

Tactic:
simp_rw [Prod.map_fst, Prod.map_snd]

Premises used: Prod.map_snd, Prod.map_fst
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
β : Type v
α : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
f : β → α
inst_2 : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this : UniformSpace α := pseudoMetrizableSpaceUniformity α
⊢ ∀ (X : Type u_2) [inst : TopologicalSpace X] [h : PseudoMetrizableSpace X], (𝓤 X).IsCountablyGenerated

Tactic:
have := pseudoMetrizableSpaceUniformity_countably_generated
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
β : Type v
α : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
f : β → α
inst_2 : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this_1 : UniformSpace α := pseudoMetrizableSpaceUniformity α
this : ∀ (X : Type u_2) [inst : TopologicalSpace X] [h : PseudoMetrizableSpace X], (𝓤 X).IsCountablyGenerated
⊢ SeparableSpace.{u_2} (↑s : Type u_2)

Tactic:
have : SeparableSpace s := hs.separableSpace
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
β : Type v
α : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
f : β → α
inst_2 : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this_1 : UniformSpace α := pseudoMetrizableSpaceUniformity α
this_2 : ∀ (X : Type u_2) [inst : TopologicalSpace X] [h : PseudoMetrizableSpace X], (𝓤 X).IsCountablyGenerated
this : SeparableSpace.{u_2} (↑s : Type u_2)
⊢ SecondCountableTopology.{u_2} (↑s : Type u_2)

Tactic:
have : SecondCountableTopology s := UniformSpace.secondCountable_of_separable _
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
β : Type v
α : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
f : β → α
inst_2 : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this_1 : UniformSpace α := pseudoMetrizableSpaceUniformity α
this_2 : ∀ (X : Type u_2) [inst : TopologicalSpace X] [h : PseudoMetrizableSpace X], (𝓤 X).IsCountablyGenerated
this_3 : SeparableSpace.{u_2} (↑s : Type u_2)
this : SecondCountableTopology.{u_2} (↑s : Type u_2)
⊢ IsInducing (MapsTo.restrict f (f ⁻¹' s) s ⋯)

Tactic:
have : IsInducing ((mapsTo_preimage f s).restrict _ _ _) :=
    (hf.comp IsInducing.subtypeVal).codRestrict _
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
β : Type v
α : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
f : β → α
inst_2 : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this_1 : UniformSpace α := pseudoMetrizableSpaceUniformity α
this_2 : ∀ (X : Type u_2) [inst : TopologicalSpace X] [h : PseudoMetrizableSpace X], (𝓤 X).IsCountablyGenerated
this_3 : SeparableSpace.{u_2} (↑s : Type u_2)
this_4 : SecondCountableTopology.{u_2} (↑s : Type u_2)
this : IsInducing (MapsTo.restrict f (f ⁻¹' s) s ⋯)
⊢ SecondCountableTopology.{v} (↑(f ⁻¹' s) : Type v)

Tactic:
have := this.secondCountableTopology
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
β : Type v
α : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
f : β → α
inst_2 : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this_1 : UniformSpace α := pseudoMetrizableSpaceUniformity α
this_2 : ∀ (X : Type u_2) [inst : TopologicalSpace X] [h : PseudoMetrizableSpace X], (𝓤 X).IsCountablyGenerated
this_3 : SeparableSpace.{u_2} (↑s : Type u_2)
this_4 : SecondCountableTopology.{u_2} (↑s : Type u_2)
this_5 : IsInducing (MapsTo.restrict f (f ⁻¹' s) s ⋯)
this : SecondCountableTopology.{v} (↑(f ⁻¹' s) : Type v)
⊢ IsSeparable (f ⁻¹' s)

Tactic:
.of_subtype _

Premises used: TopologicalSpace.IsSeparable.of_subtype
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
β : Type v
α : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
f : β → α
inst_2 : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this_1 : UniformSpace α := pseudoMetrizableSpaceUniformity α
this_2 : ∀ (X : Type u_2) [inst : TopologicalSpace X] [h : PseudoMetrizableSpace X], (𝓤 X).IsCountablyGenerated
this_3 : SeparableSpace.{u_2} (↑s : Type u_2)
this_4 : SecondCountableTopology.{u_2} (↑s : Type u_2)
this_5 : IsInducing (MapsTo.restrict f (f ⁻¹' s) s ⋯)
this : SecondCountableTopology.{v} (↑(f ⁻¹' s) : Type v)
⊢ IsSeparable (f ⁻¹' s)

Tactic:
exact .of_subtype _
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
β : Type v
α : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
f : β → α
inst_2 : TopologicalSpace β
hf : IsEmbedding f
s : Set α
hs : IsSeparable s
⊢ IsSeparable (f ⁻¹' s)

Tactic:
hf.isInducing.isSeparable_preimage hs

Premises used: Topology.IsInducing.isSeparable_preimage, Topology.IsEmbedding.isInducing
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
s : Set α
hs : IsCompact s
⊢ IsSeparable s

Tactic:
haveI : CompactSpace s := isCompact_iff_compactSpace.mp hs
  .of_subtype s

Premises used: TopologicalSpace.IsSeparable.of_subtype
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
H : ∀ ε > 0, ∃ (s : Set α), s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
⊢ SecondCountableTopology α

Tactic:
EMetric.secondCountable_of_almost_dense_set fun ε ε0 => ?_

Premises used: EMetric.secondCountable_of_almost_dense_set
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
H : ∀ ε > 0, ∃ (s : Set α), s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
refine : ∀ (ε : ℝ≥0∞) (ε0 : ε > 0), ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, closedEBall x ε) univ
⊢ SecondCountableTopology α

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

Premises used: EMetric.secondCountable_of_almost_dense_set
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
H : ∀ ε > 0, ∃ (s : Set α), s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
rcases :
  ∀ (ε' : ℝ≥0) (ε'0 : 0 < (↑ε' : ℝ≥0∞)) (ε'ε : (↑ε' : ℝ≥0∞) < ε),
    ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, closedEBall x ε) univ
⊢ ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, closedEBall x ε) univ

Tactic:
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 ε0 with ⟨ε', ε'0, ε'ε⟩

Premises used: ENNReal.lt_iff_exists_nnreal_btwn, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
H : ∀ ε > 0, ∃ (s : Set α), s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
ε' : ℝ≥0
ε'0 : 0 < (↑ε' : ℝ≥0∞)
ε'ε : (↑ε' : ℝ≥0∞) < ε
choose :
  ∀ (s : Set α) (hsc : s.Countable) (y : (x : α) → α) (hys : ∀ (x : α), y x ∈ s)
    (hyx : ∀ (x : α), dist x (y x) ≤ (↑ε' : ℝ)),
    ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, closedEBall x ε) univ
⊢ ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, closedEBall x ε) univ

Tactic:
choose s hsc y hys hyx using H ε' (mod_cast ε'0)

Premises used: ENNReal.ofNNReal, congrArg, NNReal.coe_lt_coe._simp_1, cast, ENNReal.coe_lt_coe._simp_1, GT.gt, LT.lt, congrFun', Nat.cast_zero, Eq.symm, NNReal.toReal, Eq.trans
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
H : ∀ ε > 0, ∃ (s : Set α), s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
ε' : ℝ≥0
ε'0 : 0 < (↑ε' : ℝ≥0∞)
ε'ε : (↑ε' : ℝ≥0∞) < ε
s : Set α
hsc : s.Countable
y : (x : α) → α
hys : ∀ (x : α), y x ∈ s
hyx : ∀ (x : α), dist x (y x) ≤ (↑ε' : ℝ)
⊢ ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, closedEBall x ε) univ

Tactic:
⟨s, hsc, iUnion₂_eq_univ_iff.2 fun x => ⟨y x, hys _, le_trans ?_ ε'ε.le⟩⟩

Premises used: Iff.mpr, LT.lt.le, And.intro, Exists.intro, Set.iUnion₂_eq_univ_iff, le_trans
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
H : ∀ ε > 0, ∃ (s : Set α), s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
ε' : ℝ≥0
ε'0 : 0 < (↑ε' : ℝ≥0∞)
ε'ε : (↑ε' : ℝ≥0∞) < ε
s : Set α
hsc : s.Countable
y : (x : α) → α
hys : ∀ (x : α), y x ∈ s
hyx : ∀ (x : α), dist x (y x) ≤ (↑ε' : ℝ)
refine : ∀ (x : α), edist x (y x) ≤ (↑ε' : ℝ≥0∞)
⊢ ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, closedEBall x ε) univ

Tactic:
refine ⟨s, hsc, iUnion₂_eq_univ_iff.2 fun x => ⟨y x, hys _, le_trans ?_ ε'ε.le⟩⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
H : ∀ ε > 0, ∃ (s : Set α), s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
ε' : ℝ≥0
ε'0 : 0 < (↑ε' : ℝ≥0∞)
ε'ε : (↑ε' : ℝ≥0∞) < ε
s : Set α
hsc : s.Countable
y : (x : α) → α
hys : ∀ (x : α), y x ∈ s
hyx : ∀ (x : α), dist x (y x) ≤ (↑ε' : ℝ)
x : α
⊢ edist x (y x) ≤ (↑ε' : ℝ≥0∞)

Tactic:
mod_cast hyx x

Premises used: cast, dist_le_coe._simp_1, edist_le_coe._simp_1, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
H : ∀ ε > 0, ∃ (s : Set α), s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
ε' : ℝ≥0
ε'0 : 0 < (↑ε' : ℝ≥0∞)
ε'ε : (↑ε' : ℝ≥0∞) < ε
s : Set α
hsc : s.Countable
y : (x : α) → α
hys : ∀ (x : α), y x ∈ s
hyx : ∀ (x : α), dist x (y x) ≤ (↑ε' : ℝ)
x : α
⊢ edist x (y x) ≤ (↑ε' : ℝ≥0∞)

Tactic:
exact mod_cast hyx x
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
X : Type u_2
inst : PseudoMetricSpace X
s : Set X
hs : IsCompact s
e : ℝ
he : 0 < e
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, ball x e

Tactic:
let ⟨t, hts, ht⟩ := hs.elim_nhds_subcover _ (fun x _ => ball_mem_nhds x he)
  ⟨t, hts, t.finite_toSet, ht⟩

Premises used: Set.Finite, Exists, Metric.ball, HasSubset.Subset, IsCompact.elim_nhds_subcover, Metric.ball_mem_nhds, And, SetLike.coe, _private.0.finite_cover_balls_of_compact.match_1, And.intro, Exists.intro, Finset.finite_toSet, Set.iUnion
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
X : Type u_2
inst : PseudoMetricSpace X
s : Set X
ε : ℝ
hs : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)
hε : 0 < ε
obtain :
  ∀ (t : Finset (↑s : Type u_2))
    (hst : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ⊆ ⋃ i ∈ t, ball (↑i : X) ε),
    ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, ball x ε
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, ball x ε

Tactic:
obtain ⟨t, hst⟩ := hs.elim_finite_subcover (fun x : s ↦ ball x ε) (fun _ ↦ isOpen_ball) fun x hx ↦
    let ⟨y, hy, hxy⟩ := Metric.mem_closure_iff.1 hx _ hε; mem_iUnion.2 ⟨⟨y, hy⟩, hxy⟩

Premises used: Iff.mpr, Set.mem_iUnion, Membership.mem, Metric.ball, Metric.mem_closure_iff, _private.0.exists_finite_cover_balls_of_isCompact_closure.match_1, Subtype.mk, Metric.isOpen_ball, IsCompact.elim_finite_subcover, Exists.intro, Iff.mp, Subtype.val, Set.iUnion
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
X : Type u_2
inst : PseudoMetricSpace X
s : Set X
ε : ℝ
hs : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)
hε : 0 < ε
t : Finset (↑s : Type u_2)
hst : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ⊆ ⋃ i ∈ t, ball (↑i : X) ε
⊢ (↑(Finset.map { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), inj' := ⋯ : { x : X // x ∈ s } ↪ X } t) : Set X) ⊆ s

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
X : Type u_2
inst : PseudoMetricSpace X
s : Set X
ε : ℝ
hs : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)
hε : 0 < ε
t : Finset (↑s : Type u_2)
hst : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ⊆ ⋃ i ∈ t, ball (↑i : X) ε
refine :
  s ⊆
    ⋃
      x ∈
        (↑(Finset.map { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), inj' := ⋯ : { x : X // x ∈ s } ↪ X } t) :
          Set X),
      ball x ε
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, ball x ε

Tactic:
refine ⟨t.map ⟨Subtype.val, Subtype.val_injective⟩, by simp, Finset.finite_toSet _, ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
X : Type u_2
inst : PseudoMetricSpace X
s : Set X
ε : ℝ
hs : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)
hε : 0 < ε
t : Finset (↑s : Type u_2)
hst : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ⊆ ⋃ i ∈ t, ball (↑i : X) ε
⊢ s ⊆
    ⋃
      x ∈
        (↑(Finset.map { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ s), inj' := ⋯ : { x : X // x ∈ s } ↪ X } t) :
          Set X),
      ball x ε

Tactic:
simpa using subset_closure.trans hst

Premises used: subset_closure, HasSubset.Subset.trans
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
β : Type v
α : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : IsSeparable s
rw : IsSeparable.{v} (α := β) ((fun (x : (↑s : Type u_2)) ↦ f (↑x : α)) '' univ)
⊢ IsSeparable (f '' s)

Tactic:
rw [image_eq_range, ← image_univ]

Premises used: Set.image_univ, Set.image_eq_range
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
β : Type v
α : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : IsSeparable s
⊢ IsSeparable.{v} (α := β) ((fun (x : (↑s : Type u_2)) ↦ f (↑x : α)) '' univ)

Tactic:
(isSeparable_univ_iff.2 hs.separableSpace).image hf.restrict

Premises used: Iff.mpr, TopologicalSpace.IsSeparable.image, ContinuousOn.restrict, TopologicalSpace.IsSeparable.separableSpace, TopologicalSpace.isSeparable_univ_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
β : Type v
α : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : IsSeparable s
⊢ IsSeparable.{v} (α := β) ((fun (x : (↑s : Type u_2)) ↦ f (↑x : α)) '' univ)

Tactic:
exact (isSeparable_univ_iff.2 hs.separableSpace).image hf.restrict

Premises used: Iff.mpr, TopologicalSpace.IsSeparable.image, ContinuousOn.restrict, TopologicalSpace.IsSeparable.separableSpace, TopologicalSpace.isSeparable_univ_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α_1 : Type u_1
β_1 : Type u_2
inst : PseudoMetricSpace α_1
α : Type u_3
β : Type u_4
f : α → β
m : PseudoMetricSpace β
s : Set α
⊢ (f '' sᶜ)ᶜ ∈ cobounded β ↔
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist (f x) (f y) ≤ C} s

Tactic:
simp only [← isBounded_def, isBounded_iff, forall_mem_image, mem_setOf]

Premises used: Bornology.isBounded_def, Metric.isBounded_iff, Set.mem_setOf, Set.forall_mem_image
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
inst : PseudoMetricSpace α
p : α → Prop
x y : Subtype p
⊢ dist x y = dist (↑x : α) (↑y : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
inst : PseudoMetricSpace α
p : α → Prop
x y : Subtype p
⊢ nndist x y = nndist (↑x : α) (↑y : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
inst : PseudoMetricSpace α
p : α → Prop
a : { a : α // p a }
r : ℝ
⊢ val (p := fun (a : α) ↦ p a) ⁻¹' ball (↑a : α) r = ball a r

Tactic:
rfl

Premises used: Set.Mem, setOf, Metric.ball, Set.preimage, rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
inst : PseudoMetricSpace α
p : α → Prop
a : { a : α // p a }
r : ℝ
⊢ val (p := fun (a : α) ↦ p a) ⁻¹' closedBall (↑a : α) r = closedBall a r

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Metric.closedBall, rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
inst : PseudoMetricSpace α
p : α → Prop
a : { a : α // p a }
r : ℝ
rw :
  image (α := { a : α // p a }) (val (p := fun (a : α) ↦ p a)) (val (p := fun (a : α) ↦ p a) ⁻¹' ball (↑a : α) r) =
    ball (↑a : α) r ∩ {a : α | p a}
rw₁ : ball (↑a : α) r ∩ range (ι := { a : α // p a }) (val (p := fun (a : α) ↦ p a)) = ball (↑a : α) r ∩ {a : α | p a}
rw₂ rw₃ : ball (↑a : α) r ∩ {x : α | p x} = ball (↑a : α) r ∩ {a : α | p a}
⊢ val (p := fun (a : α) ↦ p a) '' ball a r = ball (↑a : α) r ∩ {a : α | p a}

Tactic:
rw [← preimage_ball, image_preimage_eq_inter_range, range_val_subtype]

Premises used: Subtype.preimage_ball, Set.image_preimage_eq_inter_range, Subtype.range_val_subtype
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
inst : PseudoMetricSpace α
p : α → Prop
a : { a : α // p a }
r : ℝ
rw :
  image (α := { a : α // p a }) (val (p := fun (a : α) ↦ p a))
      (val (p := fun (a : α) ↦ p a) ⁻¹' closedBall (↑a : α) r) =
    closedBall (↑a : α) r ∩ {a : α | p a}
rw₁ :
  closedBall (↑a : α) r ∩ range (ι := { a : α // p a }) (val (p := fun (a : α) ↦ p a)) =
    closedBall (↑a : α) r ∩ {a : α | p a}
rw₂ rw₃ : closedBall (↑a : α) r ∩ {x : α | p x} = closedBall (↑a : α) r ∩ {a : α | p a}
⊢ val (p := fun (a : α) ↦ p a) '' closedBall a r = closedBall (↑a : α) r ∩ {a : α | p a}

Tactic:
rw [← preimage_closedBall, image_preimage_eq_inter_range, range_val_subtype]

Premises used: Set.image_preimage_eq_inter_range, Subtype.preimage_closedBall, Subtype.range_val_subtype
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
inst : PseudoMetricSpace α
x y : αᵐᵒᵖ
⊢ dist (unop x) (unop y) = dist x y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
inst : PseudoMetricSpace α
x y : α
⊢ dist (op x) (op y) = dist x y

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
inst : PseudoMetricSpace α
x y : αᵐᵒᵖ
⊢ nndist (unop x) (unop y) = nndist x y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
α : Type u_1
inst : PseudoMetricSpace α
x y : α
⊢ nndist (op x) (op y) = nndist x y

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
a b : ℝ≥0
⊢ dist a b = |(↑a : ℝ) - (↑b : ℝ)|

Tactic:
rfl

Premises used: abs, NNReal.toReal, rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
a b x : ℝ≥0
simp : nndist a b ≤ x ↔ a ≤ x + b ∧ b ≤ x + a
⊢ nndist a b ≤ x ↔ max (a - b) (b - a) ≤ x

Tactic:
simp only [max_le_iff, tsub_le_iff_right (α := ℝ≥0)]

Premises used: max_le_iff, tsub_le_iff_right
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
a b x : ℝ≥0
⊢ nndist a b ≤ x ↔ a ≤ x + b ∧ b ≤ x + a

Tactic:
simp only [← NNReal.coe_le_coe, coe_nndist, dist_eq, abs_sub_le_iff,
      tsub_le_iff_right, NNReal.coe_add]

Premises used: NNReal.coe_add, coe_nndist, abs_sub_le_iff, tsub_le_iff_right, NNReal.dist_eq, NNReal.coe_le_coe
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
z : ℝ≥0
⊢ nndist 0 z = z

Tactic:
simp only [NNReal.nndist_eq, max_eq_right, tsub_zero, zero_tsub, zero_le']

Premises used: tsub_zero, max_eq_right, NNReal.nndist_eq, zero_le', zero_tsub
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
z : ℝ≥0
rw : nndist 0 z = z
⊢ nndist z 0 = z

Tactic:
rw [nndist_comm]

Premises used: nndist_comm
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
z : ℝ≥0
⊢ nndist 0 z = z

Tactic:
NNReal.nndist_zero_eq_val z

Premises used: NNReal.nndist_zero_eq_val
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
z : ℝ≥0
⊢ nndist 0 z = z

Tactic:
exact NNReal.nndist_zero_eq_val z

Premises used: NNReal.nndist_zero_eq_val
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
a b : ℝ≥0
this : (↑a : ℝ) ≤ (↑b : ℝ) + dist a b
rwa : (↑a : ℝ) ≤ (↑(b + nndist a b) : ℝ)
rwa₁ : (↑a : ℝ) ≤ (↑b : ℝ) + (↑(nndist a b) : ℝ)
rwa₂ rwa₃ rwa₄ rwa₅ : (↑a : ℝ) ≤ (↑b : ℝ) + dist a b
⊢ a ≤ b + nndist a b

Tactic:
rwa [← NNReal.coe_le_coe, NNReal.coe_add, coe_nndist]

Premises used: NNReal.coe_add, coe_nndist, NNReal.coe_le_coe
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
a b : ℝ≥0
rw : (↑a : ℝ) - (↑b : ℝ) ≤ dist a b
⊢ (↑a : ℝ) ≤ (↑b : ℝ) + dist a b

Tactic:
rw [← sub_le_iff_le_add']

Premises used: sub_le_iff_le_add'
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
a b : ℝ≥0
⊢ (↑a : ℝ) - (↑b : ℝ) ≤ dist a b

Tactic:
le_of_abs_le (dist_eq a b).ge

Premises used: Eq.ge, le_of_abs_le, NNReal.dist_eq
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
a b : ℝ≥0
⊢ (↑a : ℝ) - (↑b : ℝ) ≤ dist a b

Tactic:
exact le_of_abs_le (dist_eq a b).ge

Premises used: Eq.ge, le_of_abs_le, NNReal.dist_eq
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
c : ℝ≥0
h : ∀ (x : ℝ≥0), Membership.mem (γ := Set ℝ≥0) (ball 0 (↑c : ℝ)) x ↔ x ∈ Ico 0 c
⊢ ball 0 (↑c : ℝ) = Ico 0 c

Tactic:
ext x
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
c x : ℝ≥0
⊢ Membership.mem (γ := Set ℝ≥0) (ball 0 (↑c : ℝ)) x ↔ x ∈ Ico 0 c

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
c : ℝ
pos : ∀ (c_pos : 0 < c), ball 0 c = Ico 0 c.toNNReal
neg : ∀ (c_pos : c ≤ 0), ball 0 c = Ico 0 c.toNNReal
⊢ ball 0 c = Ico 0 c.toNNReal

Tactic:
by_cases! c_pos : 0 < c
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
c : ℝ
c_pos : 0 < c
⊢ ball 0 (↑(NNReal.mk c ⋯) : ℝ) = Ico 0 (NNReal.mk c ⋯)

Tactic:
NNReal.ball_zero_eq_Ico' (NNReal.mk c c_pos.le)

Premises used: NNReal.mk, LT.lt.le, NNReal.ball_zero_eq_Ico'
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
c : ℝ
c_pos : 0 < c
h : c.toNNReal = NNReal.mk c ⋯
⊢ ball 0 c = Ico 0 c.toNNReal

Tactic:
convert! NNReal.ball_zero_eq_Ico' (NNReal.mk c c_pos.le)

Premises used: NNReal.mk, LT.lt.le, NNReal.ball_zero_eq_Ico'
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
c : ℝ
c_pos : 0 < c
⊢ c.toNNReal = NNReal.mk c ⋯

Tactic:
simp [Real.toNNReal, c_pos.le]

Premises used: LT.lt.le, Real.toNNReal
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
c : ℝ
c_pos : c ≤ 0
⊢ ball 0 c = Ico 0 c.toNNReal

Tactic:
simp [c_pos]
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
c : ℝ≥0
h : ∀ (x : ℝ≥0), Membership.mem (γ := Set ℝ≥0) (closedBall 0 (↑c : ℝ)) x ↔ x ∈ Icc 0 c
⊢ closedBall 0 (↑c : ℝ) = Icc 0 c

Tactic:
ext x
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
c x : ℝ≥0
⊢ Membership.mem (γ := Set ℝ≥0) (closedBall 0 (↑c : ℝ)) x ↔ x ∈ Icc 0 c

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
c : ℝ
c_nn : 0 ≤ c
⊢ closedBall 0 (↑(NNReal.mk c c_nn) : ℝ) = Icc 0 (NNReal.mk c c_nn)

Tactic:
NNReal.closedBall_zero_eq_Icc' (NNReal.mk c c_nn)

Premises used: NNReal.mk, NNReal.closedBall_zero_eq_Icc'
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
c : ℝ
c_nn : 0 ≤ c
h : c.toNNReal = NNReal.mk c c_nn
⊢ closedBall 0 c = Icc 0 c.toNNReal

Tactic:
convert! NNReal.closedBall_zero_eq_Icc' (NNReal.mk c c_nn)

Premises used: NNReal.mk, NNReal.closedBall_zero_eq_Icc'
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
c : ℝ
c_nn : 0 ≤ c
⊢ c.toNNReal = NNReal.mk c c_nn

Tactic:
simp [Real.toNNReal, c_nn]

Premises used: Real.toNNReal
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions
Goal:
β : Type u_2
inst : PseudoMetricSpace β
x y : ULift.{u_3, u_2} β
⊢ dist x y = dist x.down y.down

Tactic:
rfl

Premises used: rfl