awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
ι : Type u_1
X_1 : Type u_2
Y : Type u_3
A : ι → Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst_4 : TopologicalSpace X
inst_5 : LindelofSpace X
inst_6 : PseudoMetrizableSpace X
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : (n : ℕ) → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), Eq.{u_5 + 1} (α := Set X) (⋃ x ∈ U n, ball x (V n)) univ
⊢ SeparableSpace X

Tactic:
⟨Set.iUnion U, Set.countable_iUnion hUc, fun x => ?_⟩

Premises used: Set.countable_iUnion, And.intro, Exists.intro, TopologicalSpace.SeparableSpace.mk, Set.iUnion
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
ι : Type u_1
X_1 : Type u_2
Y : Type u_3
A : ι → Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst_4 : TopologicalSpace X
inst_5 : LindelofSpace X
inst_6 : PseudoMetrizableSpace X
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : (n : ℕ) → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), Eq.{u_5 + 1} (α := Set X) (⋃ x ∈ U n, ball x (V n)) univ
refine : ∀ (x : X), x ∈ closure[inst_4] (iUnion U)
⊢ SeparableSpace X

Tactic:
refine ⟨Set.iUnion U, Set.countable_iUnion hUc, fun x => ?_⟩
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
ι : Type u_1
X_1 : Type u_2
Y : Type u_3
A : ι → Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst_4 : TopologicalSpace X
inst_5 : LindelofSpace X
inst_6 : PseudoMetrizableSpace X
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : (n : ℕ) → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), Eq.{u_5 + 1} (α := Set X) (⋃ x ∈ U n, ball x (V n)) univ
x : X
rw : ∀ (i : ℕ), True → ∃ x_1 ∈ V i, ∃ (a : X), (x, a) = x_1 ∧ a ∈ iUnion U
⊢ x ∈ closure[inst_4] (iUnion U)

Tactic:
rw [mem_closure_iff_frequently, nhds_eq_comap_uniformity, frequently_comap, hVb.frequently_iff]

Premises used: Filter.HasAntitoneBasis.toHasBasis, mem_closure_iff_frequently, Filter.frequently_comap, Filter.HasBasis.frequently_iff, nhds_eq_comap_uniformity
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
ι : Type u_1
X_1 : Type u_2
Y : Type u_3
A : ι → Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst_4 : TopologicalSpace X
inst_5 : LindelofSpace X
inst_6 : PseudoMetrizableSpace X
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : (n : ℕ) → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), Eq.{u_5 + 1} (α := Set X) (⋃ x ∈ U n, ball x (V n)) univ
x : X
n : ℕ
_ : True → ∃ x_1 ∈ V n, ∃ (a : X), (x, a) = x_1 ∧ a ∈ iUnion U
⊢ True → ∃ x_1 ∈ V n, ∃ (a : X), (x, a) = x_1 ∧ a ∈ iUnion U

Tactic:
_
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
ι : Type u_1
X_1 : Type u_2
Y : Type u_3
A : ι → Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst_4 : TopologicalSpace X
inst_5 : LindelofSpace X
inst_6 : PseudoMetrizableSpace X
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : (n : ℕ) → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), Eq.{u_5 + 1} (α := Set X) (⋃ x ∈ U n, ball x (V n)) univ
x : X
n : ℕ
h : True
obtain : ∀ (i : X) (hi : i ∈ U n) (hx : x ∈ ball i (V n)), ∃ x_1 ∈ V n, ∃ (a : X), (x, a) = x_1 ∧ a ∈ iUnion U
⊢ ∃ x_1 ∈ V n, ∃ (a : X), (x, a) = x_1 ∧ a ∈ iUnion U

Tactic:
obtain ⟨i, hi, hx⟩ := Set.mem_iUnion₂.1 (Set.eq_univ_iff_forall.1 (hUu n) x)

Premises used: Set.eq_univ_iff_forall, Set.mem_iUnion₂, Iff.mp
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
ι : Type u_1
X_1 : Type u_2
Y : Type u_3
A : ι → Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst_4 : TopologicalSpace X
inst_5 : LindelofSpace X
inst_6 : PseudoMetrizableSpace X
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : (n : ℕ) → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), Eq.{u_5 + 1} (α := Set X) (⋃ x ∈ U n, ball x (V n)) univ
x : X
n : ℕ
h : True
i : X
hi : i ∈ U n
hx : x ∈ ball i (V n)
⊢ Membership.mem (γ := Set X) {y : X | (y, i) ∈ V n} x

Tactic:
rw [ball_eq_of_symmetry] at hx

Premises used: UniformSpace.ball_eq_of_symmetry
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
ι : Type u_1
X_1 : Type u_2
Y : Type u_3
A : ι → Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst_4 : TopologicalSpace X
inst_5 : LindelofSpace X
inst_6 : PseudoMetrizableSpace X
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : (n : ℕ) → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), Eq.{u_5 + 1} (α := Set X) (⋃ x ∈ U n, ball x (V n)) univ
x : X
n : ℕ
h : True
i : X
hi : i ∈ U n
hx : Membership.mem (γ := Set X) {y : X | (y, i) ∈ V n} x
⊢ ∃ x_1 ∈ V n, ∃ (a : X), (x, a) = x_1 ∧ a ∈ iUnion U

Tactic:
⟨(x, i), hx, i, rfl, Set.mem_iUnion_of_mem n hi⟩

Premises used: Prod.mk, And.intro, Set.mem_iUnion_of_mem, Exists.intro, rfl
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
ι : Type u_1
X_1 : Type u_2
Y : Type u_3
A : ι → Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst_4 : TopologicalSpace X
inst_5 : LindelofSpace X
inst_6 : PseudoMetrizableSpace X
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : (n : ℕ) → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), Eq.{u_5 + 1} (α := Set X) (⋃ x ∈ U n, ball x (V n)) univ
x : X
n : ℕ
h : True
i : X
hi : i ∈ U n
hx : Membership.mem (γ := Set X) {y : X | (y, i) ∈ V n} x
⊢ ∃ x_1 ∈ V n, ∃ (a : X), (x, a) = x_1 ∧ a ∈ iUnion U

Tactic:
exact ⟨(x, i), hx, i, rfl, Set.mem_iUnion_of_mem n hi⟩
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
this : UniformSpace X := pseudoMetrizableSpaceUniformity X
⊢ (𝓤 X).IsCountablyGenerated

Tactic:
have := pseudoMetrizableSpaceUniformity_countably_generated X
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
hs₁ : ∀ U ∈ 𝓤 X, ∃ (t : Set X), t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[inst] t

Tactic:
apply subset_countable_closure_of_almost_dense_set

Premises used: UniformSpace.subset_countable_closure_of_almost_dense_set
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
U : Set (X × X)
hU : U ∈ 𝓤 X
hs₁ : ∀ (t : Set X) (htc : t.Countable) (hst : s ⊆ closure[inst] t), ∃ (t : Set X), t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U
⊢ ∃ (t : Set X), t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U

Tactic:
obtain ⟨t, htc, hst⟩ := hs
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
U : Set (X × X)
hU : U ∈ 𝓤 X
t : Set X
htc : t.Countable
hst : s ⊆ closure[inst] t
⊢ ∃ (t : Set X), t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U

Tactic:
⟨t, htc, fun x hx => ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
U : Set (X × X)
hU : U ∈ 𝓤 X
t : Set X
htc : t.Countable
hst : s ⊆ closure[inst] t
hs : ∀ (x : X) (hx : x ∈ s), Membership.mem (γ := Set X) (⋃ x ∈ t, ball x U) x
⊢ ∃ (t : Set X), t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U

Tactic:
refine ⟨t, htc, fun x hx => ?_⟩
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
U : Set (X × X)
hU : U ∈ 𝓤 X
t : Set X
htc : t.Countable
hst : s ⊆ closure[inst] t
x : X
hx : x ∈ s
hs : ∀ (y : X) (hyx : y ∈ ball x (symmetrize U)) (hyt : y ∈ t), Membership.mem (γ := Set X) (⋃ x ∈ t, ball x U) x
⊢ Membership.mem (γ := Set X) (⋃ x ∈ t, ball x U) x

Tactic:
obtain ⟨y, hyx, hyt⟩ := mem_closure_iff_ball.1 (hst hx) (symmetrize_mem_uniformity hU)

Premises used: symmetrize_mem_uniformity, UniformSpace.mem_closure_iff_ball, Iff.mp
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
U : Set (X × X)
hU : U ∈ 𝓤 X
t : Set X
htc : t.Countable
hst : s ⊆ closure[inst] t
x : X
hx : x ∈ s
y : X
hyx : y ∈ ball x (symmetrize U)
hyt : y ∈ t
⊢ Membership.mem (γ := Set X) (⋃ x ∈ t, ball x U) x

Tactic:
mem_biUnion hyt (ball_mono SetRel.symmetrize_subset_inv x hyx)

Premises used: UniformSpace.ball_mono, Set.mem_biUnion, SetRel.symmetrize_subset_inv
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
U : Set (X × X)
hU : U ∈ 𝓤 X
t : Set X
htc : t.Countable
hst : s ⊆ closure[inst] t
x : X
hx : x ∈ s
y : X
hyx : y ∈ ball x (symmetrize U)
hyt : y ∈ t
⊢ Membership.mem (γ := Set X) (⋃ x ∈ t, ball x U) x

Tactic:
exact mem_biUnion hyt (ball_mono SetRel.symmetrize_subset_inv x hyx)

Premises used: UniformSpace.ball_mono, Set.mem_biUnion, SetRel.symmetrize_subset_inv
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
rcases :
  ∀ (t : Set X) (hts : t ⊆ s) (htc : t.Countable) (hst : s ⊆ closure[inst] t), SeparableSpace.{u_2} (↑s : Type u_2)
⊢ SeparableSpace.{u_2} (↑s : Type u_2)

Tactic:
rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, hst⟩

Premises used: TopologicalSpace.IsSeparable.exists_countable_dense_subset
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
t : Set X
hts : t ⊆ s
htc : t.Countable
hst : s ⊆ closure[inst] t
⊢ ∀ x ∈ t, x ∈ s

Tactic:
hts

Premises used: Set.Subset
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
t : Set X
hts : t ⊆ s
htc : t.Countable
hst : s ⊆ closure[inst] t
lift :
  ∀ (t : Set (↑s : Type u_2)) (htc : (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t).Countable)
    (hst : s ⊆ closure[inst] (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t)), SeparableSpace.{u_2} (↑s : Type u_2)
⊢ SeparableSpace.{u_2} (↑s : Type u_2)

Tactic:
lift t to Set s using hts

Premises used: Set.Elem, Set
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
t : Set (↑s : Type u_2)
htc : (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t).Countable
hst : s ⊆ closure[inst] (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t)
⊢ SeparableSpace.{u_2} (↑s : Type u_2)

Tactic:
⟨⟨t, countable_of_injective_of_countable_image Subtype.coe_injective.injOn htc, ?_⟩⟩

Premises used: Function.Injective.injOn, Subtype.coe_injective, Set.countable_of_injective_of_countable_image, And.intro, Exists.intro, TopologicalSpace.SeparableSpace.mk
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
t : Set (↑s : Type u_2)
htc : (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t).Countable
hst : s ⊆ closure[inst] (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t)
refine : Dense t
⊢ SeparableSpace.{u_2} (↑s : Type u_2)

Tactic:
refine ⟨⟨t, countable_of_injective_of_countable_image Subtype.coe_injective.injOn htc, ?_⟩⟩
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
t : Set (↑s : Type u_2)
htc : (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t).Countable
hst : s ⊆ closure[inst] (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t)
rwa : ∀ (x : { x : X // x ∈ s }), (↑x : X) ∈ closure[inst] (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (a : X) (b : a ∈ s),
    (↑(Subtype.mk (p := fun (a : X) ↦ a ∈ s) a b) : X) ∈ closure[inst] (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t)
⊢ Dense t

Tactic:
rwa [IsInducing.subtypeVal.dense_iff, Subtype.forall]

Premises used: Subtype.forall, Topology.IsInducing.dense_iff, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : CompleteSpace X
⊢ IsCompletelyPseudoMetrizableSpace X

Tactic:
⟨⟨‹_›, rfl, ‹_›⟩⟩

Premises used: TopologicalSpace.IsCompletelyPseudoMetrizableSpace.mk, And.intro, Exists.intro
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_3
ht : TopologicalSpace X
h : IsCompletelyPseudoMetrizableSpace X
⊢ CompleteSpace X

Tactic:
h.complete.choose_spec.2

Premises used: Exists.choose_spec, TopologicalSpace.IsCompletelyPseudoMetrizableSpace.complete, And.right
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_3
ht : TopologicalSpace X
h : IsCompletelyPseudoMetrizableSpace X
h₁ :
  completelyPseudoMetrizableMetric X =
    Exists.choose (p := fun (m : PseudoMetricSpace X) ↦ UniformSpace.toTopologicalSpace = ht ∧ CompleteSpace X) ⋯
⊢ CompleteSpace X

Tactic:
convert! h.complete.choose_spec.2

Premises used: Exists.choose_spec, TopologicalSpace.IsCompletelyPseudoMetrizableSpace.complete, And.right
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_3
ht : TopologicalSpace X
h : IsCompletelyPseudoMetrizableSpace X
⊢ completelyPseudoMetrizableMetric X =
    Exists.choose (p := fun (m : PseudoMetricSpace X) ↦ UniformSpace.toTopologicalSpace = ht ∧ CompleteSpace X) ⋯

Tactic:
PseudoMetricSpace.replaceTopology_eq _ _

Premises used: PseudoMetricSpace.replaceTopology_eq
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_3
ht : TopologicalSpace X
h : IsCompletelyPseudoMetrizableSpace X
⊢ completelyPseudoMetrizableMetric X =
    Exists.choose (p := fun (m : PseudoMetricSpace X) ↦ UniformSpace.toTopologicalSpace = ht ∧ CompleteSpace X) ⋯

Tactic:
exact PseudoMetricSpace.replaceTopology_eq _ _

Premises used: PseudoMetricSpace.replaceTopology_eq
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
this : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
⊢ TopologicalSpace.PseudoMetrizableSpace 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 : ι), IsCompletelyPseudoMetrizableSpace.{u_4} (X i)
this : (i : ι) → UpgradedIsCompletelyPseudoMetrizableSpace (X i) :=
  fun (i : ι) ↦ upgradeIsCompletelyPseudoMetrizable (X i)
⊢ IsCompletelyPseudoMetrizableSpace ((i : ι) → X i)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
inst_2 : TopologicalSpace Y
inst_3 : IsCompletelyPseudoMetrizableSpace Y
⊢ IsCompletelyPseudoMetrizableSpace (X × Y)

Tactic:
letI := upgradeIsCompletelyPseudoMetrizable X
  letI := upgradeIsCompletelyPseudoMetrizable Y
  inferInstance

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

Tactic:
letI := upgradeIsCompletelyPseudoMetrizable X
  letI := upgradeIsCompletelyPseudoMetrizable 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.IsCompletelyPseudoMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
this_1 : UpgradedIsCompletelyPseudoMetrizableSpace Y := upgradeIsCompletelyPseudoMetrizable Y
this : PseudoMetricSpace X := IsInducing.comapPseudoMetricSpace.{u_1, u_2} (β := Y) (f := 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 : IsCompletelyPseudoMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
this_1 : UpgradedIsCompletelyPseudoMetrizableSpace Y := upgradeIsCompletelyPseudoMetrizable Y
this : PseudoMetricSpace X := IsInducing.comapPseudoMetricSpace.{u_1, u_2} (β := Y) (f := 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.IsCompletelyPseudoMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
this_1 : UpgradedIsCompletelyPseudoMetrizableSpace Y := upgradeIsCompletelyPseudoMetrizable Y
this : PseudoMetricSpace X := IsInducing.comapPseudoMetricSpace.{u_1, u_2} (β := Y) (f := 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.IsCompletelyPseudoMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
this_1 : UpgradedIsCompletelyPseudoMetrizableSpace Y := upgradeIsCompletelyPseudoMetrizable Y
this : PseudoMetricSpace X := IsInducing.comapPseudoMetricSpace.{u_1, u_2} (β := Y) (f := 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.IsCompletelyPseudoMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
this_1 : UpgradedIsCompletelyPseudoMetrizableSpace Y := upgradeIsCompletelyPseudoMetrizable Y
this_2 : PseudoMetricSpace X := IsInducing.comapPseudoMetricSpace.{u_1, u_2} (β := Y) (f := f) ⋯
this : CompleteSpace X
⊢ TopologicalSpace.IsCompletelyPseudoMetrizableSpace X

Tactic:
infer_instance
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
s : Set X
hs : IsClosed[inst] s
⊢ IsCompletelyPseudoMetrizableSpace.{u_1} (↑s : Type u_1)

Tactic:
hs.isClosedEmbedding_subtypeVal.IsCompletelyPseudoMetrizableSpace

Premises used: Topology.IsClosedEmbedding.IsCompletelyPseudoMetrizableSpace, IsClosed.isClosedEmbedding_subtypeVal
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : IsCompletelyMetrizableSpace X
obtain :
  ∀ (m : MetricSpace X), UniformSpace.toTopologicalSpace = inst ∧ CompleteSpace X → IsCompletelyPseudoMetrizableSpace X
⊢ IsCompletelyPseudoMetrizableSpace X

Tactic:
obtain ⟨m, _⟩ := ‹_›
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : IsCompletelyMetrizableSpace X
m : MetricSpace X
h_1 : UniformSpace.toTopologicalSpace = inst ∧ CompleteSpace X
w : PseudoMetricSpace X
h : UniformSpace.toTopologicalSpace = inst ∧ CompleteSpace X
⊢ IsCompletelyPseudoMetrizableSpace X

Tactic:
use m.toPseudoMetricSpace

Premises used: MetricSpace.toPseudoMetricSpace
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
inst_2 : T0Space X
this : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
h : UniformSpace.toTopologicalSpace = inst ∧ CompleteSpace X
⊢ IsCompletelyMetrizableSpace X

Tactic:
use MetricSpace.ofT0PseudoMetricSpace X

Premises used: MetricSpace.ofT0PseudoMetricSpace
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
inst_2 : T0Space X
this : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
⊢ CompleteSpace X

Tactic:
infer_instance
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
inst_2 : T0Space X
this : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
⊢ UniformSpace.toTopologicalSpace = inst ∧ CompleteSpace X

Tactic:
exact ⟨rfl, by infer_instance⟩
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : CompleteSpace X
⊢ IsCompletelyMetrizableSpace X

Tactic:
⟨⟨‹_›, rfl, ‹_›⟩⟩

Premises used: TopologicalSpace.IsCompletelyMetrizableSpace.mk, And.intro, Exists.intro
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_3
ht : TopologicalSpace X
h : IsCompletelyMetrizableSpace X
⊢ CompleteSpace X

Tactic:
h.complete.choose_spec.2

Premises used: Exists.choose_spec, And.right, TopologicalSpace.IsCompletelyMetrizableSpace.complete
-- Module: Mathlib.Topology.Metrizable.CompletelyMetrizable
Goal:
X : Type u_3
ht : TopologicalSpace X
h : IsCompletelyMetrizableSpace X
h₁ :
  completelyMetrizableMetric X =
    Exists.choose (p := fun (m : MetricSpace X) ↦ UniformSpace.toTopologicalSpace = ht ∧ CompleteSpace X) ⋯
⊢ CompleteSpace X

Tactic:
convert! h.complete.choose_spec.2

Premises used: Exists.choose_spec, And.right, TopologicalSpace.IsCompletelyMetrizableSpace.complete
-- 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:
MetricSpace.replaceTopology_eq _ _

Premises used: MetricSpace.replaceTopology_eq