awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
β : Type u_2
inst_1 : UniformSpace β
f : α → β
g : Completion α → Completion β
hg : UniformContinuous g
h : ∀ (a : α), (↑(f a) : Completion β) = g (↑a : Completion α)
⊢ Completion.map f = g

Tactic:
cPkg.map_unique cPkg hg h

Premises used: UniformSpace.Completion.map, Quotient, SeparationQuotient, AbstractCompletion.map_unique, UniformSpace.Completion.cPkg, UniformSpace.Completion
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
⊢ Eq.{u_1 + 1} (α := Completion α → Completion α) (Completion.map id) id

Tactic:
cPkg.map_id

Premises used: UniformSpace.Completion.map, Quotient, SeparationQuotient, UniformSpace.Completion.cPkg, UniformSpace.Completion, AbstractCompletion.map_id
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace γ
inst_4 : T0Space γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
⊢ ∀ (a : α),
    Function.comp (α := Completion α) (β := Completion β) (Completion.extension f) (Completion.map g)
        (↑a : Completion α) =
      Completion.extension (f ∘ g) (↑a : Completion α)

Tactic:
simp [hf, hg, hf.comp hg, map_coe, extension_coe]

Premises used: UniformSpace.Completion.extension_coe, UniformSpace.Completion.map_coe, UniformContinuous.comp
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
g : β → γ
f : α → β
hg : UniformContinuous g
hf : UniformContinuous f
⊢ Eq (α := Completion α → Completion γ) (Function.comp (β := Completion β) (Completion.map g) (Completion.map f))
    (Completion.map (g ∘ f))

Tactic:
extension_map ((uniformContinuous_coe _).comp hg) hf

Premises used: UniformSpace.Completion.map, UniformSpace.Completion.extension_map, UniformContinuous.comp, Quotient, SeparationQuotient, UniformSpace.Completion.uniformContinuous_coe, AbstractCompletion.map, UniformSpace.Completion
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
β : Type u_2
inst_1 : UniformSpace β
e : α ≃ᵤ β
⊢ (mapEquiv e).symm = mapEquiv e.symm

Tactic:
cPkg.mapEquiv_symm cPkg e

Premises used: UniformSpace.Completion.mapEquiv, AbstractCompletion.mapEquiv_symm, Quotient, SeparationQuotient, UniformSpace.Completion.cPkg, UniformSpace.Completion
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
β : Type u_2
inst_1 : UniformSpace β
e : α ≃ᵤ β
a : α
⊢ Eq.{u_2 + 1} (α := Completion β) ((mapEquiv e : (a : Completion α) → Completion β) (↑a : Completion α) : Completion β)
    ((↑((e : (a : α) → β) a) : Completion β) : Completion β)

Tactic:
cPkg.mapEquiv_coe cPkg e a

Premises used: AbstractCompletion.mapEquiv_coe, UniformSpace.Completion.coe', Quotient, SeparationQuotient, SeparationQuotient.mk, UniformSpace.Completion.cPkg, UniformSpace.Completion
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α_1 : Type u_1
inst : UniformSpace α_1
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
α : Type u
inst_3 : UniformSpace α
refine_1 :
  ∀ (a : Completion (SeparationQuotient α)),
    Completion.map SeparationQuotient.mk (Completion.extension (lift' coe') a) = a
refine_2 :
  ∀ (a : Completion α),
    Completion.extension (α := SeparationQuotient α) (lift' coe') (Completion.map SeparationQuotient.mk a) = a
⊢ Completion (SeparationQuotient α) ≃ Completion α

Tactic:
refine ⟨Completion.extension (lift' ((↑) : α → Completion α)),
    Completion.map SeparationQuotient.mk, fun a ↦ ?_, fun a ↦ ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α_1 : Type u_1
inst : UniformSpace α_1
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
α : Type u
inst_3 : UniformSpace α
a : Completion (SeparationQuotient α)
⊢ Completion.map SeparationQuotient.mk (Completion.extension (lift' coe') a) = a

Tactic:
induction_on a (isClosed_eq (continuous_map.comp continuous_extension) continuous_id) ?_

Premises used: UniformSpace.Completion.induction_on
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α_1 : Type u_1
inst : UniformSpace α_1
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
α : Type u
inst_3 : UniformSpace α
a : Completion (SeparationQuotient α)
refine_1 :
  ∀ (a : SeparationQuotient α),
    Eq (α := Completion (SeparationQuotient α))
      (Completion.map SeparationQuotient.mk
        (Completion.extension (lift' coe') (↑a : Completion (SeparationQuotient α))))
      (↑a : Completion (SeparationQuotient α))
⊢ Completion.map SeparationQuotient.mk (Completion.extension (lift' coe') a) = a

Tactic:
refine induction_on a (isClosed_eq (continuous_map.comp continuous_extension) continuous_id) ?_
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α_1 : Type u_1
inst : UniformSpace α_1
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
α : Type u
inst_3 : UniformSpace α
a : Completion (SeparationQuotient α)
⊢ ∀ (a : SeparationQuotient α),
    Eq (α := Completion (SeparationQuotient α))
      (Completion.map SeparationQuotient.mk
        (Completion.extension (lift' coe') (↑a : Completion (SeparationQuotient α))))
      (↑a : Completion (SeparationQuotient α))

Tactic:
SeparationQuotient.surjective_mk.forall.2 fun a ↦ ?_

Premises used: Iff.mpr, Function.Surjective.forall, SeparationQuotient.surjective_mk
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α_1 : Type u_1
inst : UniformSpace α_1
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
α : Type u
inst_3 : UniformSpace α
a : Completion (SeparationQuotient α)
refine_1 :
  ∀ (a : α),
    Eq (α := Completion (SeparationQuotient α))
      (Completion.map SeparationQuotient.mk
        (Completion.extension (α := SeparationQuotient α) (lift' coe')
          (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α))))
      (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α))
⊢ ∀ (a : SeparationQuotient α),
    Eq (α := Completion (SeparationQuotient α))
      (Completion.map SeparationQuotient.mk
        (Completion.extension (lift' coe') (↑a : Completion (SeparationQuotient α))))
      (↑a : Completion (SeparationQuotient α))

Tactic:
refine SeparationQuotient.surjective_mk.forall.2 fun a ↦ ?_

Premises used: Iff.mpr, Function.Surjective.forall, SeparationQuotient.surjective_mk
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α_1 : Type u_1
inst : UniformSpace α_1
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
α : Type u
inst_3 : UniformSpace α
a_1 : Completion (SeparationQuotient α)
a : α
refine_1 :
  Eq (α := Completion (SeparationQuotient α))
    (Completion.map SeparationQuotient.mk (lift' coe' (SeparationQuotient.mk a)))
    (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α))
refine_1₁ :
  Eq (α := Completion (SeparationQuotient α)) (Completion.map SeparationQuotient.mk (↑a : Completion α))
    (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α))
refine_1₂ refine_1₃ :
  Eq (α := Completion (SeparationQuotient α)) (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α))
    (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α))
⊢ Eq (α := Completion (SeparationQuotient α))
    (Completion.map SeparationQuotient.mk
      (Completion.extension (α := SeparationQuotient α) (lift' coe')
        (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α))))
    (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α))

Tactic:
rw [extension_coe (uniformContinuous_lift' _), lift'_mk (uniformContinuous_coe α),
      map_coe uniformContinuous_mk]

Premises used: SeparationQuotient.uniformContinuous_mk, UniformSpace.Completion.extension_coe, SeparationQuotient.uniformContinuous_lift', UniformSpace.Completion.map_coe, SeparationQuotient.lift'_mk, UniformSpace.Completion.uniformContinuous_coe
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α_1 : Type u_1
inst : UniformSpace α_1
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
α : Type u
inst_3 : UniformSpace α
a : Completion α
⊢ Completion.extension (α := SeparationQuotient α) (lift' coe') (Completion.map SeparationQuotient.mk a) = a

Tactic:
induction_on a
      (isClosed_eq (continuous_extension.comp continuous_map) continuous_id) fun a ↦ ?_

Premises used: UniformSpace.Completion.induction_on
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α_1 : Type u_1
inst : UniformSpace α_1
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
α : Type u
inst_3 : UniformSpace α
a : Completion α
refine_2 :
  ∀ (a : α),
    Eq (α := Completion α)
      (Completion.extension (α := SeparationQuotient α) (lift' coe')
        (Completion.map SeparationQuotient.mk (↑a : Completion α)))
      (↑a : Completion α)
⊢ Completion.extension (α := SeparationQuotient α) (lift' coe') (Completion.map SeparationQuotient.mk a) = a

Tactic:
refine induction_on a
      (isClosed_eq (continuous_extension.comp continuous_map) continuous_id) fun a ↦ ?_
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α_1 : Type u_1
inst : UniformSpace α_1
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
α : Type u
inst_3 : UniformSpace α
a_1 : Completion α
a : α
refine_2 :
  Eq (α := Completion α)
    (Completion.extension (α := SeparationQuotient α) (lift' coe')
      (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α)))
    (↑a : Completion α)
refine_2₁ : Eq (α := Completion α) (lift' coe' (SeparationQuotient.mk a)) (↑a : Completion α)
refine_2₂ refine_2₃ : Eq (α := Completion α) (↑a : Completion α) (↑a : Completion α)
⊢ Eq (α := Completion α)
    (Completion.extension (α := SeparationQuotient α) (lift' coe')
      (Completion.map SeparationQuotient.mk (↑a : Completion α)))
    (↑a : Completion α)

Tactic:
rw [map_coe uniformContinuous_mk, extension_coe (uniformContinuous_lift' _),
      lift'_mk (uniformContinuous_coe _)]

Premises used: SeparationQuotient.uniformContinuous_mk, UniformSpace.Completion.extension_coe, SeparationQuotient.uniformContinuous_lift', UniformSpace.Completion.map_coe, SeparationQuotient.lift'_mk, UniformSpace.Completion.uniformContinuous_coe
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
⊢ UniformContinuous (α := Completion (SeparationQuotient α)) (β := Completion α)
    (⇑(completionSeparationQuotientEquiv α) : (a : Completion (SeparationQuotient α)) → Completion α)

Tactic:
uniformContinuous_extension

Premises used: UniformSpace.Completion.uniformContinuous_extension, UniformSpace.Completion.extension, AbstractCompletion.extend, ite
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
⊢ UniformContinuous (α := Completion α) (β := Completion (SeparationQuotient α))
    (⇑(Equiv.symm (completionSeparationQuotientEquiv α)) : (a : Completion α) → Completion (SeparationQuotient α))

Tactic:
uniformContinuous_map

Premises used: UniformSpace.Completion.map, AbstractCompletion.map, AbstractCompletion.extend, UniformSpace.Completion.uniformContinuous_map, ite
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
f : α → β → γ
inst_3 : T0Space γ
hf : UniformContinuous₂ f
a : α
b : β
⊢ Completion.extension₂ f (↑a : Completion α) (↑b : Completion β) = f a b

Tactic:
cPkg.extension₂_coe_coe cPkg hf a b

Premises used: UniformSpace.Completion.coe', UniformSpace.Completion.extension₂, AbstractCompletion.extension₂_coe_coe, SeparationQuotient.mk, UniformSpace.Completion.cPkg
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
f : α → β → γ
inst_3 : CompleteSpace γ
⊢ UniformContinuous₂ (α := Completion α) (β := Completion β) (Completion.extension₂ f)

Tactic:
cPkg.uniformContinuous_extension₂ cPkg f

Premises used: UniformSpace.Completion.extension₂, Quotient, SeparationQuotient, UniformSpace.Completion.cPkg, AbstractCompletion.uniformContinuous_extension₂, UniformSpace.Completion
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
f : α → β → γ
⊢ UniformContinuous₂ (α := Completion α) (β := Completion β) (γ := Completion γ) (Completion.map₂ f)

Tactic:
cPkg.uniformContinuous_map₂ cPkg cPkg f

Premises used: AbstractCompletion.uniformContinuous_map₂, UniformSpace.Completion.map₂, Quotient, SeparationQuotient, UniformSpace.Completion.cPkg, UniformSpace.Completion
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
δ : Type u_4
inst_3 : TopologicalSpace δ
f : α → β → γ
a : δ → Completion α
b : δ → Completion β
ha : Continuous[inst_3, _] a
hb : Continuous[inst_3, _] b
⊢ Continuous[inst_3, _] fun (d : δ) ↦ Completion.map₂ f (a d) (b d)

Tactic:
cPkg.continuous_map₂ cPkg cPkg ha hb

Premises used: UniformSpace.Completion.map₂, AbstractCompletion.continuous_map₂, Quotient, SeparationQuotient, UniformSpace.Completion.cPkg, UniformSpace.Completion
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
a : α
b : β
f : α → β → γ
hf : UniformContinuous₂ f
⊢ Eq (α := Completion γ) (Completion.map₂ f (↑a : Completion α) (↑b : Completion β)) (↑(f a b) : Completion γ)

Tactic:
cPkg.map₂_coe_coe cPkg cPkg a b f hf

Premises used: UniformSpace.Completion.coe', UniformSpace.Completion.map₂, Quotient, SeparationQuotient, SeparationQuotient.mk, AbstractCompletion.map₂_coe_coe, UniformSpace.Completion.cPkg, UniformSpace.Completion
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
R : SetRel α α
f g : Filter α
inst : R.IsSymm
rw : R.inv ∈ f ×ˢ g ↔ R.inv ∈ g ×ˢ f
rw₁ : Prod.swap ⁻¹' R ∈ f ×ˢ g ↔ Prod.swap ⁻¹' R ∈ g ×ˢ f
rw₂ : R ∈ map Prod.swap (f ×ˢ g) ↔ Prod.swap ⁻¹' R ∈ g ×ˢ f
rw₃ : R ∈ g ×ˢ f ↔ Prod.swap ⁻¹' R ∈ g ×ˢ f
rw₄ : R ∈ g ×ˢ f ↔ R.inv ∈ g ×ˢ f
rw₅ rw₆ : R ∈ g ×ˢ f ↔ R ∈ g ×ˢ f
⊢ R ∈ f ×ˢ g ↔ R ∈ g ×ˢ f

Tactic:
rw [← R.inv_eq_self, SetRel.inv, ← mem_map, ← prod_comm, ← SetRel.inv, R.inv_eq_self]

Premises used: SetRel.inv, Filter.prod_comm, SetRel.inv_eq_self, Filter.mem_map
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
c : Core α
s : SetRel α α
hs : s ∈ c.uniformity
⊢ ∃ t ∈ c.uniformity, t ○ t ⊆ s

Tactic:
(mem_lift'_sets <| monotone_id.relComp monotone_id).mp <| c.comp hs

Premises used: monotone_id, Monotone.relComp, Filter.mem_lift'_sets, Iff.mp, UniformSpace.Core.comp
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type u
u : Core α
x : α
hpure : ∀ (a : α), ∀ i ∈ u.uniformity, a ∈ Prod.mk a ⁻¹' id i
hopen :
  ∀ (a : α),
    ∀ i ∈ u.uniformity,
      ∀ᶠ (x : α) in comap (Prod.mk a) u.uniformity, Prod.mk a ⁻¹' id i ∈ comap (Prod.mk x) u.uniformity
⊢ 𝓝 x = comap (Prod.mk x) u.uniformity

Tactic:
apply TopologicalSpace.nhds_mkOfNhds_of_hasBasis (fun _ ↦ (basis_sets _).comap _)

Premises used: TopologicalSpace.nhds_mkOfNhds_of_hasBasis, Filter.HasBasis.comap, Filter.basis_sets
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type u
u : Core α
x : α
⊢ ∀ (a : α), ∀ i ∈ u.uniformity, a ∈ Prod.mk a ⁻¹' id i

Tactic:
fun a U hU ↦ u.refl hU rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl, UniformSpace.Core.refl
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type u
u : Core α
x : α
⊢ ∀ (a : α), ∀ i ∈ u.uniformity, a ∈ Prod.mk a ⁻¹' id i

Tactic:
exact fun a U hU ↦ u.refl hU rfl

Premises used: UniformSpace.Core.refl
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type u
u : Core α
x a : α
U : Set (α × α)
hU : U ∈ u.uniformity
hopen :
  ∀ (V : Set (α × α)) (hV : V ∈ u.uniformity) (hVU : V ○ V ⊆ U),
    ∀ᶠ (x : α) in comap (Prod.mk a) u.uniformity, Prod.mk a ⁻¹' id U ∈ comap (Prod.mk x) u.uniformity
⊢ ∀ᶠ (x : α) in comap (Prod.mk a) u.uniformity, Prod.mk a ⁻¹' id U ∈ comap (Prod.mk x) u.uniformity

Tactic:
rcases u.comp_mem_uniformity_sets hU with ⟨V, hV, hVU⟩

Premises used: UniformSpace.Core.comp_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type u
u : Core α
x a : α
U : Set (α × α)
hU : U ∈ u.uniformity
V : Set (α × α)
hV : V ∈ u.uniformity
hVU : V ○ V ⊆ U
h : ∀ (b : α) (hb : b ∈ Prod.mk a ⁻¹' V), Prod.mk a ⁻¹' id U ∈ comap (Prod.mk b) u.uniformity
⊢ ∀ᶠ (x : α) in comap (Prod.mk a) u.uniformity, Prod.mk a ⁻¹' id U ∈ comap (Prod.mk x) u.uniformity

Tactic:
filter_upwards [preimage_mem_comap hV] with b hb

Premises used: Filter.preimage_mem_comap
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type u
u : Core α
x a : α
U : Set (α × α)
hU : U ∈ u.uniformity
V : Set (α × α)
hV : V ∈ u.uniformity
hVU : V ○ V ⊆ U
b : α
hb : b ∈ Prod.mk a ⁻¹' V
h : ∀ (c : α) (hc : c ∈ Prod.mk b ⁻¹' V), c ∈ Prod.mk a ⁻¹' id U
⊢ Prod.mk a ⁻¹' id U ∈ comap (Prod.mk b) u.uniformity

Tactic:
filter_upwards [preimage_mem_comap hV] with c hc

Premises used: Filter.preimage_mem_comap
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type u
u : Core α
x a : α
U : Set (α × α)
hU : U ∈ u.uniformity
V : Set (α × α)
hV : V ∈ u.uniformity
hVU : V ○ V ⊆ U
b : α
hb : b ∈ Prod.mk a ⁻¹' V
c : α
hc : c ∈ Prod.mk b ⁻¹' V
⊢ c ∈ Prod.mk a ⁻¹' id U

Tactic:
hVU ⟨b, hb, hc⟩

Premises used: Set.Mem, setOf, Set.preimage, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type u
u : Core α
x a : α
U : Set (α × α)
hU : U ∈ u.uniformity
V : Set (α × α)
hV : V ∈ u.uniformity
hVU : V ○ V ⊆ U
b : α
hb : b ∈ Prod.mk a ⁻¹' V
c : α
hc : c ∈ Prod.mk b ⁻¹' V
⊢ c ∈ Prod.mk a ⁻¹' id U

Tactic:
exact hVU ⟨b, hb, hc⟩
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α_1 : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
α : Type u
u : Core α
t : TopologicalSpace α
h : t = u.toTopologicalSpace
x : α
rw : 𝓝 x = comap (Prod.mk x) u.uniformity
rw₁ rw₂ : comap (Prod.mk x) u.uniformity = comap (Prod.mk x) u.uniformity
⊢ 𝓝 x = comap (Prod.mk x) u.uniformity

Tactic:
rw [h, u.nhds_toTopologicalSpace]

Premises used: UniformSpace.Core.nhds_toTopologicalSpace
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u : UniformSpace α
U : Set (α × α)
hU : Membership.mem (γ := Filter (α × α)) UniformSpace.uniformity U
x : α
rw : Prod.mk x ⁻¹' U ∈ comap (Prod.mk x) UniformSpace.uniformity
⊢ Prod.mk x ⁻¹' U ∈ 𝓝 x

Tactic:
rw [UniformSpace.nhds_eq_comap_uniformity]

Premises used: UniformSpace.nhds_eq_comap_uniformity
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u : UniformSpace α
U : Set (α × α)
hU : Membership.mem (γ := Filter (α × α)) UniformSpace.uniformity U
x : α
⊢ Prod.mk x ⁻¹' U ∈ comap (Prod.mk x) UniformSpace.uniformity

Tactic:
preimage_mem_comap hU

Premises used: Filter.preimage_mem_comap
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u : UniformSpace α
U : Set (α × α)
hU : Membership.mem (γ := Filter (α × α)) UniformSpace.uniformity U
x : α
⊢ Prod.mk x ⁻¹' U ∈ comap (Prod.mk x) UniformSpace.uniformity

Tactic:
exact preimage_mem_comap hU

Premises used: Filter.preimage_mem_comap
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u : UniformSpace α
U : Set (α × α)
hU : Membership.mem (γ := Filter (α × α)) UniformSpace.uniformity U
x : α
⊢ Prod.mk x ⁻¹' U ∈ 𝓝 x

Tactic:
have : Prod.mk x ⁻¹' U ∈ 𝓝 x := by
      rw [UniformSpace.nhds_eq_comap_uniformity]
      exact preimage_mem_comap hU
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u : UniformSpace α
U : Set (α × α)
hU : Membership.mem (γ := Filter (α × α)) UniformSpace.uniformity U
x : α
this : Prod.mk x ⁻¹' U ∈ 𝓝 x
⊢ x ∈ Prod.mk x ⁻¹' U

Tactic:
mem_of_mem_nhds this

Premises used: mem_of_mem_nhds
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u : UniformSpace α
U : Set (α × α)
hU : Membership.mem (γ := Filter (α × α)) UniformSpace.uniformity U
x : α
this : Prod.mk x ⁻¹' U ∈ 𝓝 x
⊢ (x, x) ∈ U

Tactic:
convert! mem_of_mem_nhds this

Premises used: mem_of_mem_nhds
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
u : UniformSpace α
a : α
rw : 𝓝 a = comap (Prod.mk a) UniformSpace.uniformity
rw₁ rw₂ : comap (Prod.mk a) u.toCore.uniformity = comap (Prod.mk a) UniformSpace.uniformity
⊢ 𝓝 a = 𝓝 a

Tactic:
rw [u.nhds_eq_comap_uniformity, u.toCore.nhds_toTopologicalSpace]

Premises used: UniformSpace.toCore, UniformSpace.nhds_eq_comap_uniformity, UniformSpace.Core.nhds_toTopologicalSpace
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
u : Core α
s : SetRel α α
⊢ s ∈ 𝓤 α ↔ s ∈ u.uniformity

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
u₁ u₂ : UniformSpace α
h : 𝓤 α = 𝓤 α
x : α
rw : comap (Prod.mk x) UniformSpace.uniformity = comap (Prod.mk x) UniformSpace.uniformity
⊢ 𝓝 x = 𝓝 x

Tactic:
rw [u₁.nhds_eq_comap_uniformity, u₂.nhds_eq_comap_uniformity]

Premises used: UniformSpace.nhds_eq_comap_uniformity
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
u₁ u₂ : UniformSpace α
h : 𝓤 α = 𝓤 α
x : α
⊢ comap (Prod.mk x) UniformSpace.uniformity = comap (Prod.mk x) UniformSpace.uniformity

Tactic:
congr_arg (comap _) h

Premises used: congr_arg, Filter.comap
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
u₁ u₂ : UniformSpace α
h : 𝓤 α = 𝓤 α
x : α
⊢ comap (Prod.mk x) UniformSpace.uniformity = comap (Prod.mk x) UniformSpace.uniformity

Tactic:
exact congr_arg (comap _) h

Premises used: congr_arg, Filter.comap
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
u₁ u₂ : UniformSpace α
h : 𝓤 α = 𝓤 α
⊢ Eq.{ua + 1} (α := TopologicalSpace α) toTopologicalSpace toTopologicalSpace

Tactic:
have : u₁.toTopologicalSpace = u₂.toTopologicalSpace := TopologicalSpace.ext_nhds fun x ↦ by
    rw [u₁.nhds_eq_comap_uniformity, u₂.nhds_eq_comap_uniformity]
    exact congr_arg (comap _) h
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
u₁ u₂ : UniformSpace α
h : 𝓤 α = 𝓤 α
this : Eq.{ua + 1} (α := TopologicalSpace α) toTopologicalSpace toTopologicalSpace
mk :
  ∀ [toTopologicalSpace : TopologicalSpace α] (uniformity : Filter (α × α))
    (symm : Tendsto Prod.swap uniformity uniformity)
    (comp : (uniformity.lift' fun (s : Set (α × α)) ↦ s ○ s) ≤ uniformity)
    (nhds_eq_comap_uniformity : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity) (h : 𝓤 α = 𝓤 α)
    (this : Eq.{ua + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace UniformSpace.toTopologicalSpace),
    { toTopologicalSpace := toTopologicalSpace, uniformity := uniformity, symm := symm, comp := comp,
        nhds_eq_comap_uniformity := nhds_eq_comap_uniformity : UniformSpace α } =
      u₂
⊢ u₁ = u₂

Tactic:
cases u₁