awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
ι : Type u_3
inst : Countable ι
u : (i : ι) → UniformSpace α
hcomp : ∀ (i : ι), CompleteSpace α
hcount : ∀ (i : ι), (𝓤 α).IsCountablyGenerated
ht₀ :
  ∃ (t₀ : TopologicalSpace α),
    T2Space α ∧ ∀ (i : ι), (fun (i : ι) ↦ (UniformSpace.toTopologicalSpace : TopologicalSpace α)) i ≤ t₀
hut :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace
      ((fun (i : ι) ↦ (UniformSpace.toTopologicalSpace : TopologicalSpace α)) i)
refine : (𝓤 α).IsCountablyGenerated
⊢ ∃ (u_1 : UniformSpace α),
    CompleteSpace α ∧
      (𝓤 α).IsCountablyGenerated ∧
        Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace
          (⨅ (i : ι), (fun (i : ι) ↦ (UniformSpace.toTopologicalSpace : TopologicalSpace α)) i)

Tactic:
refine ⟨⨅ i, u i, .iInf hcomp ht₀, ?_, UniformSpace.toTopologicalSpace_iInf⟩
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
ι : Type u_3
inst : Countable ι
u : (i : ι) → UniformSpace α
hcomp : ∀ (i : ι), CompleteSpace α
hcount : ∀ (i : ι), (𝓤 α).IsCountablyGenerated
ht₀ :
  ∃ (t₀ : TopologicalSpace α),
    T2Space α ∧ ∀ (i : ι), (fun (i : ι) ↦ (UniformSpace.toTopologicalSpace : TopologicalSpace α)) i ≤ t₀
hut :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace
      ((fun (i : ι) ↦ (UniformSpace.toTopologicalSpace : TopologicalSpace α)) i)
rw : IsCountablyGenerated.{u_1} (α := α × α) (⨅ (i : ι), 𝓤 α)
⊢ (𝓤 α).IsCountablyGenerated

Tactic:
rw [iInf_uniformity]

Premises used: iInf_uniformity
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
ι : Type u_3
inst : Countable ι
u : (i : ι) → UniformSpace α
hcomp : ∀ (i : ι), CompleteSpace α
hcount : ∀ (i : ι), (𝓤 α).IsCountablyGenerated
ht₀ :
  ∃ (t₀ : TopologicalSpace α),
    T2Space α ∧ ∀ (i : ι), (fun (i : ι) ↦ (UniformSpace.toTopologicalSpace : TopologicalSpace α)) i ≤ t₀
hut :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace
      ((fun (i : ι) ↦ (UniformSpace.toTopologicalSpace : TopologicalSpace α)) i)
⊢ IsCountablyGenerated.{u_1} (α := α × α) (⨅ (i : ι), 𝓤 α)

Tactic:
infer_instance
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
ι : Type u_3
inst : Countable ι
t : ι → TopologicalSpace α
ht₀ : ∃ (i₀ : ι), ∀ (i : ι), t i ≤ t i₀
ht : ∀ (i : ι), PolishSpace α
rcases : ∀ (i₀ : ι) (hi₀ : ∀ (i : ι), t i ≤ t i₀), PolishSpace α
⊢ PolishSpace α

Tactic:
rcases ht₀ with ⟨i₀, hi₀⟩
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
ι : Type u_3
inst : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), PolishSpace α
i₀ : ι
hi₀ : ∀ (i : ι), t i ≤ t i₀
rcases :
  ∀ (u : UniformSpace α) (hcomp : CompleteSpace α) (hcount : (𝓤 α).IsCountablyGenerated)
    (htop : Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace (⨅ (i : ι), t i)), PolishSpace α
⊢ PolishSpace α

Tactic:
rcases CompletePseudometrizable.iInf ⟨t i₀, letI := t i₀; haveI := ht i₀; inferInstance, hi₀⟩
    fun i ↦
      letI := t i; haveI := ht i; letI := upgradeIsCompletelyMetrizable α
      ⟨inferInstance, inferInstance, inferInstance, rfl⟩
    with ⟨u, hcomp, hcount, htop⟩

Premises used: inferInstance, CompletePseudometrizable.iInf, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
ι : Type u_3
inst : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), PolishSpace α
i₀ : ι
hi₀ : ∀ (i : ι), t i ≤ t i₀
u : UniformSpace α
hcomp : CompleteSpace α
hcount : (𝓤 α).IsCountablyGenerated
htop : Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace (⨅ (i : ι), t i)
rw : PolishSpace α
⊢ PolishSpace α

Tactic:
rw [← htop]
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
ι : Type u_3
inst : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), PolishSpace α
i₀ : ι
hi₀ : ∀ (i : ι), t i ≤ t i₀
u : UniformSpace α
hcomp : CompleteSpace α
hcount : (𝓤 α).IsCountablyGenerated
htop : Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace (⨅ (i : ι), t i)
⊢ SecondCountableTopology α

Tactic:
have : @SecondCountableTopology α u.toTopologicalSpace :=
    htop.symm ▸ secondCountableTopology_iInf fun i ↦ letI := t i; (ht i).toSecondCountableTopology
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
ι : Type u_3
inst : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), PolishSpace α
i₀ : ι
hi₀ : ∀ (i : ι), t i ≤ t i₀
u : UniformSpace α
hcomp : CompleteSpace α
hcount : (𝓤 α).IsCountablyGenerated
htop : Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace (⨅ (i : ι), t i)
this_1 : SecondCountableTopology α
this : TopologicalSpace α := t i₀
⊢ PolishSpace α

Tactic:
haveI := ht i₀
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
ι : Type u_3
inst : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), PolishSpace α
i₀ : ι
hi₀ : ∀ (i : ι), t i ≤ t i₀
u : UniformSpace α
hcomp : CompleteSpace α
hcount : (𝓤 α).IsCountablyGenerated
htop : Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace (⨅ (i : ι), t i)
this_1 : SecondCountableTopology α
this_2 : TopologicalSpace α := t i₀
this : PolishSpace α
⊢ T1Space α

Tactic:
infer_instance
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
ι : Type u_3
inst : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), PolishSpace α
i₀ : ι
hi₀ : ∀ (i : ι), t i ≤ t i₀
u : UniformSpace α
hcomp : CompleteSpace α
hcount : (𝓤 α).IsCountablyGenerated
htop : Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace (⨅ (i : ι), t i)
this : SecondCountableTopology α
⊢ T1Space α

Tactic:
have : @T1Space α u.toTopologicalSpace :=
    htop.symm ▸ t1Space_antitone (iInf_le _ i₀) (by letI := t i₀; haveI := ht i₀; infer_instance)
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
ι : Type u_3
inst : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), PolishSpace α
i₀ : ι
hi₀ : ∀ (i : ι), t i ≤ t i₀
u : UniformSpace α
hcomp : CompleteSpace α
hcount : (𝓤 α).IsCountablyGenerated
htop : Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace (⨅ (i : ι), t i)
this_1 : SecondCountableTopology α
this : T1Space α
⊢ PolishSpace α

Tactic:
infer_instance
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
ι : Type u_3
inst : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
⊢ ∃ (t' : TopologicalSpace α), (∀ (n : ι), t' ≤ m n) ∧ t' ≤ t ∧ PolishSpace α

Tactic:
⟨⨅ i : Option ι, i.elim t m, fun i ↦ iInf_le _ (some i), iInf_le _ none,
    .iInf ⟨none, Option.forall.2 ⟨le_rfl, hm⟩⟩ <| Option.forall.2 ⟨p, h'm⟩⟩

Premises used: Iff.mpr, iInf, le_rfl, Option.some, Option.forall, Option.none, And.intro, Exists.intro, Option.elim, PolishSpace.iInf, iInf_le
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
⊢ PolishSpace ENNReal

Tactic:
ENNReal.orderIsoUnitIntervalBirational.toHomeomorph.isClosedEmbedding.polishSpace

Premises used: ENNReal.orderIsoUnitIntervalBirational, OrderIso.toHomeomorph, Topology.IsClosedEmbedding.polishSpace, Homeomorph.isClosedEmbedding
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
inst : MetricSpace α
s : Opens α
x y : s.CompleteCopy
⊢ dist x y = dist (↑x : α) (↑y : α) + |1 / infDist (↑x : α) (↑s : Set α)ᶜ - 1 / infDist (↑y : α) (↑s : Set α)ᶜ|

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
inst : MetricSpace α
s : Opens α
x y : s.CompleteCopy
⊢ dist (↑x : α) (↑y : α) ≤ dist x y

Tactic:
le_add_of_nonneg_right (abs_nonneg _)

Premises used: le_add_of_nonneg_right, abs_nonneg
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
inst_1 : SecondCountableTopology α
⊢ SecondCountableTopology.{u_1} s.CompleteCopy

Tactic:
inferInstanceAs (SecondCountableTopology s)

Premises used: _private.0.TopologicalSpace.Opens.CompleteCopy.instSecondCountableTopology._proof_1
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
⊢ T0Space.{u_1} s.CompleteCopy

Tactic:
inferInstanceAs (T0Space s)

Premises used: _private.0.TopologicalSpace.Opens.CompleteCopy.instT0Space._proof_1
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
refine_1 : ∀ (x : s.CompleteCopy), dist x x = 0
refine_2 : ∀ (x x_1 : s.CompleteCopy), dist x x_1 = dist x_1 x
refine_3 : ∀ (x y z : s.CompleteCopy), dist x z ≤ dist x y + dist y z
refine_4 : ∀ (t : Set s.CompleteCopy), IsOpen t ↔ ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
⊢ MetricSpace s.CompleteCopy

Tactic:
refine @MetricSpace.ofT0PseudoMetricSpace (CompleteCopy s)
    (.ofDistTopology dist (fun _ ↦ ?_) (fun _ _ ↦ ?_) (fun x y z ↦ ?_) fun t ↦ ?_) _

Premises used: TopologicalSpace.Opens.CompleteCopy, MetricSpace.ofT0PseudoMetricSpace
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
x : s.CompleteCopy
⊢ dist x x = 0

Tactic:
simp only [dist_eq, dist_self, one_div, sub_self, abs_zero, add_zero]

Premises used: TopologicalSpace.Opens.CompleteCopy.dist_eq, sub_self, dist_self, abs_zero, one_div, add_zero
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
x x_1 : s.CompleteCopy
⊢ dist x x_1 = dist x_1 x

Tactic:
simp only [dist_eq, dist_comm, abs_sub_comm]

Premises used: TopologicalSpace.Opens.CompleteCopy.dist_eq, dist_comm, abs_sub_comm
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
x y z : s.CompleteCopy
⊢ dist x z = dist (↑x : α) (↑z : α) + |1 / infDist (↑x : α) (↑s : Set α)ᶜ - 1 / infDist (↑z : α) (↑s : Set α)ᶜ|

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
x y z : s.CompleteCopy
⊢ dist (↑x : α) (↑z : α) + |1 / infDist (↑x : α) (↑s : Set α)ᶜ - 1 / infDist (↑z : α) (↑s : Set α)ᶜ| ≤
    dist (↑x : α) (↑y : α) + dist (↑y : α) (↑z : α) +
      (|1 / infDist (↑x : α) (↑s : Set α)ᶜ - 1 / infDist (↑y : α) (↑s : Set α)ᶜ| +
        |1 / infDist (↑y : α) (↑s : Set α)ᶜ - 1 / infDist (↑z : α) (↑s : Set α)ᶜ|)

Tactic:
add_le_add (dist_triangle _ _ _) (dist_triangle (1 / infDist _ _) _ _)

Premises used: dist_triangle, add_le_add, Metric.infDist, HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
x y z : s.CompleteCopy
⊢ dist (↑x : α) (↑y : α) + dist (↑y : α) (↑z : α) +
      (|1 / infDist (↑x : α) (↑s : Set α)ᶜ - 1 / infDist (↑y : α) (↑s : Set α)ᶜ| +
        |1 / infDist (↑y : α) (↑s : Set α)ᶜ - 1 / infDist (↑z : α) (↑s : Set α)ᶜ|) =
    dist x y + dist y z

Tactic:
add_add_add_comm ..

Premises used: add_add_add_comm
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
x y z : s.CompleteCopy
⊢ dist x z ≤ dist x y + dist y z

Tactic:
calc
      dist x z = dist x.1 z.1 + |1 / infDist x.1 sᶜ - 1 / infDist z.1 sᶜ| := rfl
      _ ≤ dist x.1 y.1 + dist y.1 z.1 + (|1 / infDist x.1 sᶜ - 1 / infDist y.1 sᶜ| +
            |1 / infDist y.1 sᶜ - 1 / infDist z.1 sᶜ|) :=
        add_le_add (dist_triangle _ _ _) (dist_triangle (1 / infDist _ _) _ _)
      _ = dist x y + dist y z := add_add_add_comm ..

Premises used: dist_triangle, abs, Compl.compl, add_le_add, HSub.hSub, Metric.infDist, HDiv.hDiv, SetLike.coe, HAdd.hAdd, add_add_add_comm, Dist.dist, OfNat.ofNat, Subtype.val, rfl
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
⊢ IsOpen t ↔ ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t

Tactic:
⟨fun h x hx ↦ ?_, fun h ↦ isOpen_iff_mem_nhds.2 fun x hx ↦ ?_⟩

Premises used: Iff.mpr, Iff.intro, isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
refine_4 : ∀ (h : IsOpen t) (x : s.CompleteCopy) (hx : x ∈ t), ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
refine_4₁ :
  ∀ (h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t) (x : s.CompleteCopy) (hx : x ∈ t), t ∈ 𝓝 x
⊢ IsOpen t ↔ ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h ↦ isOpen_iff_mem_nhds.2 fun x hx ↦ ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : IsOpen t
x : s.CompleteCopy
hx : x ∈ t
refine_4 : ∀ (ε : ℝ) (ε0 : ε > 0) (hε : ball x ε ⊆ t), ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
⊢ ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t

Tactic:
rcases (Metric.isOpen_iff (α := s)).1 h x hx with ⟨ε, ε0, hε⟩

Premises used: Metric.isOpen_iff, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : IsOpen t
x : s.CompleteCopy
hx : x ∈ t
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ t
⊢ ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t

Tactic:
⟨ε, ε0, fun y hy ↦ hε <| (dist_comm _ _).trans_lt <| (dist_val_le_dist _ _).trans_lt hy⟩

Premises used: TopologicalSpace.Opens.CompleteCopy.dist_val_le_dist, dist_comm, And.intro, Exists.intro, Eq.trans_lt, LE.le.trans_lt
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : IsOpen t
x : s.CompleteCopy
hx : x ∈ t
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ t
⊢ ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t

Tactic:
exact ⟨ε, ε0, fun y hy ↦ hε <| (dist_comm _ _).trans_lt <| (dist_val_le_dist _ _).trans_lt hy⟩
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
refine_4 : ∀ (ε : ℝ) (ε0 : ε > 0) (hε : ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t), t ∈ 𝓝 x
⊢ t ∈ 𝓝 x

Tactic:
rcases h x hx with ⟨ε, ε0, hε⟩
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
ε : ℝ
ε0 : ε > 0
hε : ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
⊢ ∀ (y : s.CompleteCopy),
    dist (↑x : α) (↑y : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹| < ε → y ∈ t

Tactic:
simp only [dist_eq, one_div] at hε

Premises used: TopologicalSpace.Opens.CompleteCopy.dist_eq, one_div
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
ε : ℝ
ε0 : ε > 0
hε :
  ∀ (y : s.CompleteCopy),
    dist (↑x : α) (↑y : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹| < ε → y ∈ t
⊢ Tendsto
    (fun (y : ↥s) ↦ dist (↑x : α) (↑y : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹|)
    (𝓝 x) (𝓝 (dist (↑x : α) (↑x : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹|))

Tactic:
(tendsto_const_nhds.dist continuous_subtype_val.continuousAt).add
          (tendsto_const_nhds.sub <| ?_).abs

Premises used: continuous_subtype_val, tendsto_const_nhds, Filter.Tendsto.abs, Filter.Tendsto.dist, Continuous.continuousAt, Filter.Tendsto.add, Filter.Tendsto.sub
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
ε : ℝ
ε0 : ε > 0
hε :
  ∀ (y : s.CompleteCopy),
    dist (↑x : α) (↑y : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹| < ε → y ∈ t
refine : Tendsto (fun (y : ↥s) ↦ (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹) (𝓝 x) (𝓝 (infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹)
⊢ Tendsto
    (fun (y : ↥s) ↦ dist (↑x : α) (↑y : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹|)
    (𝓝 x) (𝓝 (dist (↑x : α) (↑x : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹|))

Tactic:
refine (tendsto_const_nhds.dist continuous_subtype_val.continuousAt).add
          (tendsto_const_nhds.sub <| ?_).abs

Premises used: continuous_subtype_val, tendsto_const_nhds, Filter.Tendsto.abs, Filter.Tendsto.dist, Continuous.continuousAt, Filter.Tendsto.add, Filter.Tendsto.sub
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
ε : ℝ
ε0 : ε > 0
hε :
  ∀ (y : s.CompleteCopy),
    dist (↑x : α) (↑y : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹| < ε → y ∈ t
⊢ Tendsto (fun (y : ↥s) ↦ (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹) (𝓝 x) (𝓝 (infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹)

Tactic:
(continuousAt_inv_infDist_pt ?_).comp continuous_subtype_val.continuousAt

Premises used: continuous_subtype_val, Metric.continuousAt_inv_infDist_pt, ContinuousAt, Continuous.continuousAt, ContinuousAt.comp
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
ε : ℝ
ε0 : ε > 0
hε :
  ∀ (y : s.CompleteCopy),
    dist (↑x : α) (↑y : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹| < ε → y ∈ t
refine : (↑x : α) ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set α)ᶜ
⊢ Tendsto (fun (y : ↥s) ↦ (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹) (𝓝 x) (𝓝 (infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹)

Tactic:
refine (continuousAt_inv_infDist_pt ?_).comp continuous_subtype_val.continuousAt

Premises used: continuous_subtype_val, Metric.continuousAt_inv_infDist_pt, Continuous.continuousAt, ContinuousAt.comp
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
ε : ℝ
ε0 : ε > 0
hε :
  ∀ (y : s.CompleteCopy),
    dist (↑x : α) (↑y : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹| < ε → y ∈ t
rw : (↑x : α) ∈ (↑s : Set α)
⊢ (↑x : α) ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set α)ᶜ

Tactic:
rw [s.isOpen.isClosed_compl.closure_eq, mem_compl_iff, not_not]

Premises used: Classical.not_not, IsClosed.closure_eq, IsOpen.isClosed_compl, TopologicalSpace.Opens.isOpen, Set.mem_compl_iff
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
ε : ℝ
ε0 : ε > 0
hε :
  ∀ (y : s.CompleteCopy),
    dist (↑x : α) (↑y : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹| < ε → y ∈ t
⊢ (↑x : α) ∈ (↑s : Set α)

Tactic:
x.2

Premises used: Subtype.property
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
ε : ℝ
ε0 : ε > 0
hε :
  ∀ (y : s.CompleteCopy),
    dist (↑x : α) (↑y : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹| < ε → y ∈ t
⊢ (↑x : α) ∈ (↑s : Set α)

Tactic:
exact x.2

Premises used: Subtype.property
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
ε : ℝ
ε0 : ε > 0
hε :
  ∀ (y : s.CompleteCopy),
    dist (↑x : α) (↑y : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹| < ε → y ∈ t
⊢ Tendsto
    (fun (y : ↥s) ↦ dist (↑x : α) (↑y : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹|)
    (𝓝 x) (𝓝 (dist (↑x : α) (↑x : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹|))

Tactic:
have : Tendsto (fun y : s ↦ dist x.1 y.1 + |(infDist x.1 sᶜ)⁻¹ - (infDist y.1 sᶜ)⁻¹|)
          (𝓝 x) (𝓝 (dist x.1 x.1 + |(infDist x.1 sᶜ)⁻¹ - (infDist x.1 sᶜ)⁻¹|)) := by
        refine (tendsto_const_nhds.dist continuous_subtype_val.continuousAt).add
          (tendsto_const_nhds.sub <| ?_).abs
        refine (continuousAt_inv_infDist_pt ?_).comp continuous_subtype_val.continuousAt
        rw [s.isOpen.isClosed_compl.closure_eq, mem_compl_iff, not_not]
        exact x.2
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
ε : ℝ
ε0 : ε > 0
hε :
  ∀ (y : s.CompleteCopy),
    dist (↑x : α) (↑y : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹| < ε → y ∈ t
this :
  Tendsto
    (fun (y : ↥s) ↦ dist (↑x : α) (↑y : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹|)
    (𝓝 x) (𝓝 (dist (↑x : α) (↑x : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹|))
⊢ Tendsto (β := ℝ)
    (fun (y : ↥s) ↦ dist (↑x : α) (↑y : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹|)
    (𝓝 x) (𝓝 0)

Tactic:
simp only [dist_self, sub_self, abs_zero, zero_add] at this

Premises used: sub_self, zero_add, dist_self, abs_zero
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
ε : ℝ
ε0 : ε > 0
hε :
  ∀ (y : s.CompleteCopy),
    dist (↑x : α) (↑y : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹| < ε → y ∈ t
this :
  Tendsto (β := ℝ)
    (fun (y : ↥s) ↦ dist (↑x : α) (↑y : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹|)
    (𝓝 x) (𝓝 0)
⊢ t ∈ 𝓝 x

Tactic:
mem_of_superset (this <| gt_mem_nhds ε0) hε

Premises used: gt_mem_nhds, Filter.mem_of_superset
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
ε : ℝ
ε0 : ε > 0
hε :
  ∀ (y : s.CompleteCopy),
    dist (↑x : α) (↑y : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹| < ε → y ∈ t
this :
  Tendsto (β := ℝ)
    (fun (y : ↥s) ↦ dist (↑x : α) (↑y : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹|)
    (𝓝 x) (𝓝 0)
⊢ t ∈ 𝓝 x

Tactic:
exact mem_of_superset (this <| gt_mem_nhds ε0) hε
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
inst_1 : CompleteSpace α
⊢ ∀ (n : ℕ), LT.lt (α := ℝ) 0 ((fun (x : ℕ) ↦ (1 / 2) ^ x) n)

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
inst_1 : CompleteSpace α
refine :
  ∀ (u : ℕ → s.CompleteCopy) (hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (x : ℕ) ↦ (1 / 2) ^ x) N),
    ∃ (x : s.CompleteCopy), Tendsto u atTop (𝓝 x)
⊢ CompleteSpace.{u_1} s.CompleteCopy

Tactic:
refine Metric.complete_of_convergent_controlled_sequences ((1 / 2) ^ ·) (by simp) fun u hu ↦ ?_

Premises used: Metric.complete_of_convergent_controlled_sequences, HDiv.hDiv, HPow.hPow, OfNat.ofNat