awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_3
ht : TopologicalSpace X
h : IsCompletelyMetrizableSpace X
⊢ completelyMetrizableMetric X =
    Exists.choose (p := fun (m : MetricSpace X) ↦ UniformSpace.toTopologicalSpace = ht ∧ CompleteSpace X) ⋯

Tactic:
exact MetricSpace.replaceTopology_eq _ _

Premises used: MetricSpace.replaceTopology_eq
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : IsCompletelyMetrizableSpace X
this : UpgradedIsCompletelyMetrizableSpace X := upgradeIsCompletelyMetrizable X
⊢ TopologicalSpace.MetrizableSpace X

Tactic:
infer_instance
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : Countable ι
X : ι → Type u_4
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (i : ι), IsCompletelyMetrizableSpace.{u_4} (X i)
this : (i : ι) → UpgradedIsCompletelyMetrizableSpace (X i) := fun (i : ι) ↦ upgradeIsCompletelyMetrizable (X i)
⊢ IsCompletelyMetrizableSpace ((i : ι) → X i)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
X : ι → Type u_4
inst : (n : ι) → TopologicalSpace (X n)
inst_1 : ∀ (n : ι), IsCompletelyMetrizableSpace.{u_4} (X n)
⊢ IsCompletelyMetrizableSpace ((n : ι) × X n)

Tactic:
letI := fun n ↦ upgradeIsCompletelyMetrizable (X n)
  letI : MetricSpace (Σ n, X n) := Metric.Sigma.metricSpace
  haveI : CompleteSpace (Σ n, X n) := Metric.Sigma.completeSpace
  inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : IsCompletelyMetrizableSpace X
inst_2 : TopologicalSpace Y
inst_3 : IsCompletelyMetrizableSpace Y
⊢ IsCompletelyMetrizableSpace (X × Y)

Tactic:
letI := upgradeIsCompletelyMetrizable X
  letI := upgradeIsCompletelyMetrizable Y
  inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : IsCompletelyMetrizableSpace X
inst_2 : TopologicalSpace Y
inst_3 : IsCompletelyMetrizableSpace Y
⊢ IsCompletelyMetrizableSpace (X ⊕ Y)

Tactic:
letI := upgradeIsCompletelyMetrizable X
  letI := upgradeIsCompletelyMetrizable Y
  inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace.IsCompletelyMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
this_1 : UpgradedIsCompletelyMetrizableSpace Y := upgradeIsCompletelyMetrizable Y
this : MetricSpace X := IsEmbedding.comapMetricSpace f ⋯
rw : IsComplete (range f)
⊢ CompleteSpace X

Tactic:
rw [completeSpace_iff_isComplete_range hf.isEmbedding.to_isometry.isUniformInducing]

Premises used: Topology.IsClosedEmbedding.isEmbedding, Topology.IsEmbedding.to_isometry, Isometry.isUniformInducing, completeSpace_iff_isComplete_range
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : IsCompletelyMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
this_1 : UpgradedIsCompletelyMetrizableSpace Y := upgradeIsCompletelyMetrizable Y
this : MetricSpace X := IsEmbedding.comapMetricSpace f ⋯
⊢ IsComplete (range f)

Tactic:
hf.isClosed_range.isComplete

Premises used: IsClosed.isComplete, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace.IsCompletelyMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
this_1 : UpgradedIsCompletelyMetrizableSpace Y := upgradeIsCompletelyMetrizable Y
this : MetricSpace X := IsEmbedding.comapMetricSpace f ⋯
⊢ IsComplete (range f)

Tactic:
exact hf.isClosed_range.isComplete

Premises used: IsClosed.isComplete, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace.IsCompletelyMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
this_1 : UpgradedIsCompletelyMetrizableSpace Y := upgradeIsCompletelyMetrizable Y
this : MetricSpace X := IsEmbedding.comapMetricSpace f ⋯
⊢ CompleteSpace X

Tactic:
have : CompleteSpace X := by
    rw [completeSpace_iff_isComplete_range hf.isEmbedding.to_isometry.isUniformInducing]
    exact hf.isClosed_range.isComplete
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace.IsCompletelyMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
this_1 : UpgradedIsCompletelyMetrizableSpace Y := upgradeIsCompletelyMetrizable Y
this_2 : MetricSpace X := IsEmbedding.comapMetricSpace f ⋯
this : CompleteSpace X
⊢ TopologicalSpace.IsCompletelyMetrizableSpace X

Tactic:
infer_instance
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
x : X
⊢ Eq (α := ℝ) (if x = x then 0 else 1) 0

Tactic:
simp
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
x y : X
inl : ∀ (h : x = y), Eq (α := ℝ) (if x = y then 0 else 1) (if y = x then 0 else 1)
inr : ∀ (h : x ≠ y), Eq (α := ℝ) (if x = y then 0 else 1) (if y = x then 0 else 1)
⊢ Eq (α := ℝ) (if x = y then 0 else 1) (if y = x then 0 else 1)

Tactic:
obtain h | h := eq_or_ne x y

Premises used: eq_or_ne
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
x y : X
h : x = y
⊢ Eq (α := ℝ) (if x = y then 0 else 1) (if y = x then 0 else 1)

Tactic:
simp [h]
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
x y : X
h : x ≠ y
⊢ Eq (α := ℝ) (if x = y then 0 else 1) (if y = x then 0 else 1)

Tactic:
simp [h, h.symm]

Premises used: Ne.symm
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
x y z : X
pos : x = y → (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)
neg : ¬x = y → (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)
⊢ (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)

Tactic:
by_cases x = y
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
x y z : X
h : x = y
pos : x = z → (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)
neg : ¬x = z → (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)
⊢ (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)

Tactic:
by_cases x = z
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
x y z : X
h : ¬x = y
pos : x = z → (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)
neg : ¬x = z → (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)
⊢ (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)

Tactic:
by_cases x = z
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
x y z : X
h : x = y
h_1 : x = z
pos : y = z → (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)
neg : ¬y = z → (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)
⊢ (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)

Tactic:
by_cases y = z
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
x y z : X
h : x = y
h_1 : ¬x = z
pos : y = z → (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)
neg : ¬y = z → (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)
⊢ (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)

Tactic:
by_cases y = z
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
x y z : X
h : ¬x = y
h_1 : x = z
pos : y = z → (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)
neg : ¬y = z → (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)
⊢ (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)

Tactic:
by_cases y = z
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
x y z : X
h : ¬x = y
h_1 : ¬x = z
pos : y = z → (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)
neg : ¬y = z → (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)
⊢ (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)

Tactic:
by_cases y = z
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
x y z : X
h : x = y
h_1 : x = z
h_2 : y = z
⊢ (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)

Tactic:
simp_all
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
x y z : X
h : x = y
h_1 : x = z
h_2 : ¬y = z
⊢ (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)

Tactic:
simp_all
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
x y z : X
h : x = y
h_1 : ¬x = z
h_2 : y = z
⊢ (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)

Tactic:
simp_all
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
x y z : X
h : x = y
h_1 : ¬x = z
h_2 : ¬y = z
⊢ (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)

Tactic:
simp_all
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
x y z : X
h : ¬x = y
h_1 : x = z
h_2 : y = z
⊢ (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)

Tactic:
simp_all
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
x y z : X
h : ¬x = y
h_1 : x = z
h_2 : ¬y = z
⊢ (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)

Tactic:
simp_all
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
x y z : X
h : ¬x = y
h_1 : ¬x = z
h_2 : y = z
⊢ (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)

Tactic:
simp_all
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
x y z : X
h : ¬x = y
h_1 : ¬x = z
h_2 : ¬y = z
⊢ (if x = z then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = y then 0 else 1) (if y = z then 0 else 1)

Tactic:
simp_all
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
⊢ ∀ {x y : X}, Eq (α := ℝ) (if x = y then 0 else 1) 0 → x = y

Tactic:
simp
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
⊢ IsCompletelyMetrizableSpace X

Tactic:
⟨m, ?_, ?_⟩

Premises used: TopologicalSpace.IsCompletelyMetrizableSpace.mk, And.intro, Exists.intro
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
refine_1 : UniformSpace.toTopologicalSpace = inst
refine_2 : CompleteSpace X
⊢ IsCompletelyMetrizableSpace X

Tactic:
refine ⟨m, ?_, ?_⟩
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
refine_1 : Eq.{u_1 + 1} (α := TopologicalSpace X) UniformSpace.toTopologicalSpace ⊥
⊢ UniformSpace.toTopologicalSpace = inst

Tactic:
rw [DiscreteTopology.eq_bot (α := X)]

Premises used: DiscreteTopology.eq_bot
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
⊢ Eq.{u_1 + 1} (α := TopologicalSpace X) UniformSpace.toTopologicalSpace ⊥

Tactic:
eq_bot_of_singletons_open fun x ↦ ?_

Premises used: eq_bot_of_singletons_open
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
refine_1 : ∀ (x : X), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x}
⊢ Eq.{u_1 + 1} (α := TopologicalSpace X) UniformSpace.toTopologicalSpace ⊥

Tactic:
refine eq_bot_of_singletons_open fun x ↦ ?_

Premises used: eq_bot_of_singletons_open
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
x : X
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Metric.ball x 1)

Tactic:
@Metric.isOpen_ball _ _ x 1

Premises used: Metric.isOpen_ball
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
x : X
h : {x} = Metric.ball x 1
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x}

Tactic:
convert! @Metric.isOpen_ball _ _ x 1

Premises used: Metric.isOpen_ball
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
x : X
⊢ LT.lt (α := ℝ) 0 1

Tactic:
simp
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
x : X
h : ∀ (y : X) (hy : y ∈ Metric.ball x 1), Membership.mem (γ := Set X) {x} y
⊢ {x} = Metric.ball x 1

Tactic:
refine subset_antisymm (singleton_subset_iff.2 (Metric.mem_ball_self (by simp)))
      fun y hy ↦ ?_

Premises used: Iff.mpr, Set.singleton_subset_iff, Metric.mem_ball_self, subset_antisymm
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
x y : X
hy : y ∈ Metric.ball x 1
⊢ dist y x < 1

Tactic:
simp only [Metric.mem_ball, mem_singleton_iff] at *

Premises used: Metric.mem_ball, Set.mem_singleton_iff
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
x y : X
hy : dist y x < 1
h : ∀ (this : ¬y = x), False
⊢ y = x

Tactic:
by_contra
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
x y : X
hy : dist y x < 1
this : ¬y = x
⊢ LT.lt (α := ℝ) (if y = x then 0 else 1) 1

Tactic:
change (if y = x then 0 else 1) < 1 at hy

Premises used: OfNat.ofNat, ite
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
x y : X
this : ¬y = x
hy : LT.lt (α := ℝ) (if y = x then 0 else 1) 1
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
⊢ CompleteSpace X

Tactic:
Metric.complete_of_cauchySeq_tendsto fun u hu ↦ ?_

Premises used: Metric.complete_of_cauchySeq_tendsto
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
refine_2 : ∀ (u : ℕ → X) (hu : CauchySeq u), ∃ (a : X), Tendsto u atTop (𝓝 a)
⊢ CompleteSpace X

Tactic:
refine Metric.complete_of_cauchySeq_tendsto fun u hu ↦ ?_

Premises used: Metric.complete_of_cauchySeq_tendsto
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
u : ℕ → X
hu : CauchySeq u
⊢ ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, dist (u n) (u N) < ε

Tactic:
rw [Metric.cauchySeq_iff'] at hu

Premises used: Metric.cauchySeq_iff'
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
u : ℕ → X
hu : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, dist (u n) (u N) < ε
⊢ GT.gt (α := ℝ) 1 0

Tactic:
simp
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
u : ℕ → X
hu : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, dist (u n) (u N) < ε
refine_2 : ∀ (N : ℕ) (hN : ∀ n ≥ N, dist (u n) (u N) < 1), ∃ (a : X), Tendsto u atTop (𝓝 a)
⊢ ∃ (a : X), Tendsto u atTop (𝓝 a)

Tactic:
obtain ⟨N, hN⟩ := hu 1 (by simp)

Premises used: OfNat.ofNat
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
u : ℕ → X
hu : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, dist (u n) (u N) < ε
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
⊢ ∃ (a : X), Tendsto u atTop (𝓝 a)

Tactic:
⟨u N, @tendsto_atTop_of_eventually_const X UniformSpace.toTopologicalSpace (u N) _ _ _ N
      fun n hn ↦ ?_⟩

Premises used: tendsto_atTop_of_eventually_const, Exists.intro
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
u : ℕ → X
hu : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, dist (u n) (u N) < ε
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
refine_2 : ∀ (n : ℕ) (hn : n ≥ N), u n = u N
⊢ ∃ (a : X), Tendsto u atTop (𝓝 a)

Tactic:
refine ⟨u N, @tendsto_atTop_of_eventually_const X UniformSpace.toTopologicalSpace (u N) _ _ _ N
      fun n hn ↦ ?_⟩
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun (x y : X) ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
u : ℕ → X
hu : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, dist (u n) (u N) < ε
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
n : ℕ
hn : n ≥ N
⊢ dist (u n) (u N) < 1

Tactic:
specialize hN n hn