awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
c : CauchyFilter α
this : Membership.mem (γ := Set (CauchyFilter α)) (closure (range pureCauchy)) c
w : CauchyFilter α
left : Membership.mem (γ := Set (CauchyFilter α)) univ w
a : α
h : pureCauchy a = w
⊢ Nonempty α

Tactic:
⟨a⟩

Premises used: Nonempty.intro
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
c : CauchyFilter α
this : Membership.mem (γ := Set (CauchyFilter α)) (closure (range pureCauchy)) c
w : CauchyFilter α
left : Membership.mem (γ := Set (CauchyFilter α)) univ w
a : α
h : pureCauchy a = w
⊢ Nonempty α

Tactic:
exact ⟨a⟩
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
c : α
⊢ Nonempty.{u + 1} (CauchyFilter α)

Tactic:
⟨pureCauchy c⟩

Premises used: CauchyFilter.pureCauchy, Nonempty.intro
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
c : α
⊢ Nonempty.{u + 1} (CauchyFilter α)

Tactic:
exact ⟨pureCauchy c⟩
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
β : Type v
γ : Type w
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : Filter α
hf : Cauchy f
f' : CauchyFilter α := Subtype.mk (p := fun (f : Filter α) ↦ Cauchy f) f hf
this : map pureCauchy f ≤ Filter.lift' (𝓤 (CauchyFilter α)) (preimage (Prod.mk f'))
⊢ map pureCauchy f ≤ 𝓝 f'

Tactic:
simpa [nhds_eq_uniformity]

Premises used: nhds_eq_uniformity
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
β : Type v
γ : Type w
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
h : Nonempty α
⊢ Nonempty.{u + 1} (CauchyFilter α)

Tactic:
h.recOn fun a => Nonempty.intro <| CauchyFilter.pureCauchy a

Premises used: Nonempty.recOn
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
β : Type v
inst_1 : UniformSpace β
inst_2 : T0Space β
f : α → β
hf : UniformContinuous f
a : α
rw : IsDenseInducing.extend (β := CauchyFilter α) ⋯ f (pureCauchy a) = f a
⊢ extend f (pureCauchy a) = f a

Tactic:
rw [extend, if_pos hf]

Premises used: if_pos, CauchyFilter.extend
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
β : Type v
inst_1 : UniformSpace β
inst_2 : T0Space β
f : α → β
hf : UniformContinuous f
a : α
⊢ IsDenseInducing.extend (β := CauchyFilter α) ⋯ f (pureCauchy a) = f a

Tactic:
uniformly_extend_of_ind isUniformInducing_pureCauchy denseRange_pureCauchy hf _

Premises used: CauchyFilter.isUniformInducing_pureCauchy, CauchyFilter.denseRange_pureCauchy, uniformly_extend_of_ind
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
β : Type v
inst_1 : UniformSpace β
inst_2 : T0Space β
f : α → β
hf : UniformContinuous f
a : α
⊢ IsDenseInducing.extend (β := CauchyFilter α) ⋯ f (pureCauchy a) = f a

Tactic:
exact uniformly_extend_of_ind isUniformInducing_pureCauchy denseRange_pureCauchy hf _

Premises used: CauchyFilter.isUniformInducing_pureCauchy, CauchyFilter.denseRange_pureCauchy, uniformly_extend_of_ind
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
β : Type v
inst_1 : UniformSpace β
inst_2 : CompleteSpace β
f : α → β
pos : ∀ (hf : UniformContinuous f), UniformContinuous (α := CauchyFilter α) (extend f)
neg : ∀ (hf : ¬UniformContinuous f), UniformContinuous (α := CauchyFilter α) (extend f)
⊢ UniformContinuous (α := CauchyFilter α) (extend f)

Tactic:
by_cases hf : UniformContinuous f

Premises used: UniformContinuous
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
β : Type v
inst_1 : UniformSpace β
inst_2 : CompleteSpace β
f : α → β
hf : UniformContinuous f
pos : UniformContinuous (α := CauchyFilter α) (IsDenseInducing.extend ⋯ f)
⊢ UniformContinuous (α := CauchyFilter α) (extend f)

Tactic:
rw [extend, if_pos hf]

Premises used: if_pos, CauchyFilter.extend
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
β : Type v
inst_1 : UniformSpace β
inst_2 : CompleteSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (α := CauchyFilter α) (IsDenseInducing.extend ⋯ f)

Tactic:
uniformContinuous_uniformly_extend isUniformInducing_pureCauchy denseRange_pureCauchy hf

Premises used: CauchyFilter.isUniformInducing_pureCauchy, uniformContinuous_uniformly_extend, CauchyFilter.denseRange_pureCauchy
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
β : Type v
inst_1 : UniformSpace β
inst_2 : CompleteSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (α := CauchyFilter α) (IsDenseInducing.extend ⋯ f)

Tactic:
exact uniformContinuous_uniformly_extend isUniformInducing_pureCauchy denseRange_pureCauchy hf

Premises used: CauchyFilter.isUniformInducing_pureCauchy, uniformContinuous_uniformly_extend, CauchyFilter.denseRange_pureCauchy
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
β : Type v
inst_1 : UniformSpace β
inst_2 : CompleteSpace β
f : α → β
hf : ¬UniformContinuous f
neg : UniformContinuous.{u, v} (β := β) fun (x : CauchyFilter α) ↦ f ⋯.some
⊢ UniformContinuous (α := CauchyFilter α) (extend f)

Tactic:
rw [extend, if_neg hf]

Premises used: if_neg, CauchyFilter.extend
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
β : Type v
inst_1 : UniformSpace β
inst_2 : CompleteSpace β
f : α → β
hf : ¬UniformContinuous f
a _b : CauchyFilter α
⊢ f ⋯.some = f ⋯.some

Tactic:
congr
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
β : Type v
inst_1 : UniformSpace β
inst_2 : CompleteSpace β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous.{u, v} (β := β) fun (x : CauchyFilter α) ↦ f ⋯.some

Tactic:
exact uniformContinuous_of_const fun a _b => by congr

Premises used: uniformContinuous_of_const
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
f g : CauchyFilter α
⊢ Inseparable f g ↔ (↑f : Filter α) ×ˢ (↑g : Filter α) ≤ 𝓤 α

Tactic:
(basis_uniformity (basis_sets _)).inseparable_iff_uniformity

Premises used: Set.Mem, setOf, CauchyFilter.basis_uniformity, Filter.basis_sets, CauchyFilter.gen, Filter.HasBasis.inseparable_iff_uniformity
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
f g : CauchyFilter α
a b : α
ha : (↑f : Filter α) ≤ 𝓝 a
hb : (↑g : Filter α) ≤ 𝓝 b
⊢ Tendsto id (↑f : Filter α) (𝓝 a)

Tactic:
rw [← tendsto_id'] at ha hb

Premises used: Filter.tendsto_id'
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
f g : CauchyFilter α
a b : α
ha : (↑f : Filter α) ≤ 𝓝 a
hb : (↑g : Filter α) ≤ 𝓝 b
ha₁ : Tendsto id (↑f : Filter α) (𝓝 a)
⊢ Tendsto id (↑g : Filter α) (𝓝 b)

Tactic:
rw [← tendsto_id'] at ha hb

Premises used: Filter.tendsto_id'
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
f g : CauchyFilter α
a b : α
ha : Tendsto id (↑f : Filter α) (𝓝 a)
hb : Tendsto id (↑g : Filter α) (𝓝 b)
rw :
  Tendsto (fun (x : α × α) ↦ ((id ∘ Prod.fst) x, (id ∘ Prod.snd) x)) ((↑f : Filter α) ×ˢ (↑g : Filter α)) (𝓤 α) ↔
    (↑f : Filter α) ×ˢ (↑g : Filter α) ≤ 𝓤 α
⊢ Inseparable a b ↔ Inseparable f g

Tactic:
rw [inseparable_iff, (ha.comp tendsto_fst).inseparable_iff_uniformity (hb.comp tendsto_snd)]

Premises used: CauchyFilter.inseparable_iff, Filter.Tendsto.comp, Filter.Tendsto.inseparable_iff_uniformity, Filter.tendsto_snd, Filter.tendsto_fst
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
f g : CauchyFilter α
a b : α
ha : Tendsto id (↑f : Filter α) (𝓝 a)
hb : Tendsto id (↑g : Filter α) (𝓝 b)
⊢ Tendsto (fun (x : α × α) ↦ ((id ∘ Prod.fst) x, (id ∘ Prod.snd) x)) ((↑f : Filter α) ×ˢ (↑g : Filter α)) (𝓤 α) ↔
    (↑f : Filter α) ×ˢ (↑g : Filter α) ≤ 𝓤 α

Tactic:
simp only [Function.comp_apply, id_eq, Prod.mk.eta, ← Function.id_def, tendsto_id']

Premises used: Function.id_def, Filter.tendsto_id', Prod.mk.eta, Function.comp_apply, id_eq
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
inst_1 : CompleteSpace α
f g : CauchyFilter α
⊢ Inseparable (↑f : Filter α).lim (↑g : Filter α).lim ↔ Inseparable f g

Tactic:
inseparable_iff_of_le_nhds f.2.le_nhds_lim g.2.le_nhds_lim

Premises used: Cauchy.le_nhds_lim, CauchyFilter.inseparable_iff_of_le_nhds, Subtype.property
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : CompleteSpace α
inst_2 : T0Space α
f g : CauchyFilter α
rw : Inseparable (↑f : Filter α).lim (↑g : Filter α).lim ↔ Inseparable f g
rw₁ rw₂ : Inseparable f g ↔ Inseparable f g
⊢ (↑f : Filter α).lim = (↑g : Filter α).lim ↔ Inseparable f g

Tactic:
rw [← inseparable_iff_eq, inseparable_lim_iff]

Premises used: inseparable_iff_eq, CauchyFilter.inseparable_lim_iff
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T0Space α
⊢ Function.Injective (β := SeparationQuotient (CauchyFilter α)) fun (a : α) ↦ SeparationQuotient.mk (pureCauchy a)

Tactic:
fun a b h ↦
  Inseparable.eq <| (inseparable_iff_of_le_nhds (pure_le_nhds a) (pure_le_nhds b)).2 <|
    SeparationQuotient.mk_eq_mk.1 h

Premises used: Iff.mpr, SeparationQuotient.mk_eq_mk, Inseparable.eq, Iff.mp, CauchyFilter.inseparable_iff_of_le_nhds, Function.Injective
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
⊢ CompleteSpace.{u_1} (Completion α)

Tactic:
SeparationQuotient.instCompleteSpace

Premises used: SeparationQuotient.instCompleteSpace, 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 γ
⊢ T0Space.{u_1} (Completion α)

Tactic:
SeparationQuotient.instT0Space

Premises used: SeparationQuotient.instT0Space, UniformSpace.Completion
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
⊢ Eq.{u_1 + 1} (α := α → Completion α) coe' (SeparationQuotient.mk ∘ pureCauchy)

Tactic:
rfl

Premises used: UniformSpace.Completion.coe', rfl
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
⊢ IsUniformInducing.{u_1, u_1} (α := α) (β := Completion α) coe'

Tactic:
SeparationQuotient.isUniformInducing_mk.comp isUniformInducing_pureCauchy

Premises used: UniformSpace.Completion.coe', CauchyFilter.isUniformInducing_pureCauchy, SeparationQuotient.isUniformInducing_mk, IsUniformInducing.comp, UniformSpace.Completion
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
⊢ Filter.comap (β := Completion α × Completion α) (fun (p : α × α) ↦ ((↑p.1 : Completion α), (↑p.2 : Completion α)))
      (𝓤 (Completion α)) =
    𝓤 α

Tactic:
(isUniformInducing_coe _).1

Premises used: IsUniformInducing.comap_uniformity, UniformSpace.Completion.isUniformInducing_coe
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
⊢ DenseRange.{u_1, u_1} (X := Completion α) coe'

Tactic:
SeparationQuotient.surjective_mk.denseRange.comp denseRange_pureCauchy
    SeparationQuotient.continuous_mk

Premises used: UniformSpace.Completion.coe', SeparationQuotient.continuous_mk, Function.Surjective.denseRange, CauchyFilter.denseRange_pureCauchy, SeparationQuotient.surjective_mk, DenseRange.comp, 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_4
inst_3 : UniformSpace α
⊢ UniformSpace (Completion α)

Tactic:
infer_instance
-- 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_4
inst_3 : UniformSpace α
⊢ CompleteSpace.{u_4} (Completion α)

Tactic:
infer_instance
-- 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_4
inst_3 : UniformSpace α
⊢ T0Space.{u_4} (Completion α)

Tactic:
infer_instance
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
⊢ Nonempty.{u_1 + 1} (Completion α) ↔ Nonempty α

Tactic:
cPkg.dense.nonempty_iff.symm

Premises used: AbstractCompletion.dense, DenseRange.nonempty_iff, Quotient, SeparationQuotient, UniformSpace.Completion.cPkg, Iff.symm, UniformSpace.Completion
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
⊢ UniformContinuous.{u_1, u_1} (α := α) (β := Completion α) coe'

Tactic:
cPkg.uniformContinuous_coe

Premises used: UniformSpace.Completion.coe', AbstractCompletion.uniformContinuous_coe, Quotient, SeparationQuotient, SeparationQuotient.mk, UniformSpace.Completion.cPkg, UniformSpace.Completion
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
⊢ Continuous[inst.toTopologicalSpace, _] coe'

Tactic:
cPkg.continuous_coe

Premises used: UniformSpace.Completion.coe', AbstractCompletion.continuous_coe, Quotient, SeparationQuotient, SeparationQuotient.mk, UniformSpace.Completion.cPkg, UniformSpace.Completion
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T0Space α
⊢ IsUniformEmbedding.{u_1, u_1} (α := α) (β := Completion α) coe'

Tactic:
{ comap_uniformity := comap_coe_eq_uniformity α
    injective := separated_pureCauchy_injective }

Premises used: CauchyFilter.separated_pureCauchy_injective, IsUniformEmbedding.mk, IsUniformInducing.mk, UniformSpace.Completion.comap_coe_eq_uniformity
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T0Space α
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := α) (β := Completion α) coe'

Tactic:
IsUniformEmbedding.injective (isUniformEmbedding_coe _)

Premises used: IsUniformEmbedding.injective, UniformSpace.Completion.isUniformEmbedding_coe
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T0Space α
a b : α
⊢ Eq (α := Completion α) (↑a : Completion α) (↑b : Completion α) ↔ a = b

Tactic:
(coe_injective _).eq_iff

Premises used: Function.Injective.eq_iff, UniformSpace.Completion.coe_injective
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
⊢ IsDenseInducing.{u_1, u_1} (α := α) (β := Completion α) coe'

Tactic:
{ (isUniformInducing_coe α).isInducing with dense := denseRange_coe }

Premises used: IsDenseInducing.mk, IsUniformInducing.isInducing, UniformSpace.Completion.denseRange_coe, UniformSpace.Completion.isUniformInducing_coe
-- 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 : SeparableSpace α
⊢ SeparableSpace.{u_1} (Completion α)

Tactic:
Completion.isDenseInducing_coe.separableSpace

Premises used: IsDenseInducing.separableSpace, UniformSpace.Completion.isDenseInducing_coe
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T0Space α
⊢ IsDenseEmbedding.{u_1, u_1} (α := α) (β := Completion α) coe'

Tactic:
{ isDenseInducing_coe with injective := separated_pureCauchy_injective }

Premises used: IsDenseEmbedding.mk, CauchyFilter.separated_pureCauchy_injective, UniformSpace.Completion.isDenseInducing_coe
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
β : Type u_2
inst_1 : UniformSpace β
⊢ DenseRange (X := Prod.{u_1, u_2} (Completion α) (Completion β)) fun (x : α × β) ↦
    ((↑x.1 : Completion α), (↑x.2 : Completion β))

Tactic:
denseRange_coe.prodMap denseRange_coe

Premises used: DenseRange.prodMap, UniformSpace.Completion.denseRange_coe, Prod.map
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
⊢ DenseRange (X := Completion α × Prod.{u_2, u_3} (Completion β) (Completion γ)) fun (x : α × β × γ) ↦
    ((↑x.1 : Completion α), (↑x.2.1 : Completion β), (↑x.2.2 : Completion γ))

Tactic:
denseRange_coe.prodMap denseRange_coe₂

Premises used: DenseRange.prodMap, UniformSpace.Completion.denseRange_coe, Prod.map, UniformSpace.Completion.denseRange_coe₂
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
p : Completion α → Prop
a : Completion α
hp : IsClosed.{u_1} (X := Completion α) {a : Completion α | p a}
ih : ∀ (a : α), p (↑a : Completion α)
⊢ p a

Tactic:
isClosed_property denseRange_coe hp ih a

Premises used: UniformSpace.Completion.denseRange_coe, isClosed_property
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
β : Type u_2
inst_1 : UniformSpace β
p : Completion α → Completion β → Prop
a : Completion α
b : Completion β
hp :
  IsClosed (X := Prod.{u_1, u_2} (Completion α) (Completion β))
    {x : Prod.{u_1, u_2} (Completion α) (Completion β) | p x.1 x.2}
ih : ∀ (a : α) (b : β), p (↑a : Completion α) (↑b : Completion β)
⊢ p a b

Tactic:
have : ∀ x : Completion α × Completion β, p x.1 x.2 :=
    isClosed_property denseRange_coe₂ hp fun ⟨a, b⟩ => ih a b
  this (a, b)

Premises used: UniformSpace.Completion.coe', Prod.mk, _private.0.UniformSpace.Completion.induction_on₂.match_1, Prod.fst, isClosed_property, UniformSpace.Completion.denseRange_coe₂, Prod.snd
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
p : Completion α → Completion β → Completion γ → Prop
a : Completion α
b : Completion β
c : Completion γ
hp :
  IsClosed (X := Completion α × Prod.{u_2, u_3} (Completion β) (Completion γ))
    {x : Completion α × Prod.{u_2, u_3} (Completion β) (Completion γ) | p x.1 x.2.1 x.2.2}
ih : ∀ (a : α) (b : β) (c : γ), p (↑a : Completion α) (↑b : Completion β) (↑c : Completion γ)
⊢ p a b c

Tactic:
have : ∀ x : Completion α × Completion β × Completion γ, p x.1 x.2.1 x.2.2 :=
    isClosed_property denseRange_coe₃ hp fun ⟨a, b, c⟩ => ih a b c
  this (a, b, c)

Premises used: UniformSpace.Completion.coe', Prod.mk, Prod.fst, _private.0.UniformSpace.Completion.induction_on₃.match_1, UniformSpace.Completion.denseRange_coe₃, isClosed_property, Prod.snd
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
Y : Type u_4
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
f g : Completion α → Y
hf : Continuous[_, inst_1] f
hg : Continuous[_, inst_1] g
h : ∀ (a : α), f (↑a : Completion α) = g (↑a : Completion α)
⊢ f = g

Tactic:
cPkg.funext hf hg h

Premises used: AbstractCompletion.funext, Quotient, SeparationQuotient, UniformSpace.Completion.cPkg, UniformSpace.Completion
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
Y : Type u_4
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
f g : Completion α → Y
hf : Continuous[_, inst_1] f
hg : Continuous[_, inst_1] g
h : ∀ (a : α), f (↑a : Completion α) = g (↑a : Completion α)
a : Completion α
⊢ f a = g a

Tactic:
congr_fun (ext hf hg h) a

Premises used: UniformSpace.Completion.ext, congr_fun
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
β : Type u_2
inst_1 : UniformSpace β
f : α → β
inst_2 : CompleteSpace β
⊢ UniformContinuous (α := Completion α) (Completion.extension f)

Tactic:
cPkg.uniformContinuous_extend

Premises used: AbstractCompletion.uniformContinuous_extend, Quotient, SeparationQuotient, UniformSpace.Completion.extension, UniformSpace.Completion.cPkg, UniformSpace.Completion
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
β : Type u_2
inst_1 : UniformSpace β
f : α → β
inst_2 : CompleteSpace β
⊢ Continuous[_, inst_1.toTopologicalSpace] (Completion.extension f)

Tactic:
cPkg.continuous_extend

Premises used: Quotient, SeparationQuotient, UniformSpace.Completion.extension, UniformSpace.Completion.cPkg, UniformSpace.Completion, AbstractCompletion.continuous_extend
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
β : Type u_2
inst_1 : UniformSpace β
f : α → β
inst_2 : T0Space β
hf : UniformContinuous f
a : α
⊢ Completion.extension f (↑a : Completion α) = f a

Tactic:
cPkg.extend_coe hf a

Premises used: UniformSpace.Completion.coe', AbstractCompletion.extend_coe, SeparationQuotient.mk, UniformSpace.Completion.extension, UniformSpace.Completion.cPkg
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
β : Type u_2
inst_1 : UniformSpace β
f : α → β
hf : UniformContinuous f
x : α
⊢ Inseparable (Completion.extension f (↑x : Completion α)) (f x)

Tactic:
cPkg.inseparable_extend_coe hf x

Premises used: UniformSpace.Completion.coe', AbstractCompletion.inseparable_extend_coe, SeparationQuotient.mk, UniformSpace.Completion.extension, UniformSpace.Completion.cPkg
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
β : Type u_2
inst_1 : UniformSpace β
f : α → β
inst_2 : CompleteSpace β
h : IsUniformInducing f
⊢ IsUniformInducing (α := Completion α) (Completion.extension f)

Tactic:
cPkg.isUniformInducing_extend h

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

Tactic:
cPkg.extend_unique hf hg h

Premises used: Quotient, SeparationQuotient, UniformSpace.Completion.extension, AbstractCompletion.extend_unique, UniformSpace.Completion.cPkg, UniformSpace.Completion
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
β : Type u_2
inst_1 : UniformSpace β
inst_2 : T0Space β
inst_3 : CompleteSpace β
f : Completion α → β
hf : UniformContinuous f
⊢ Completion.extension (f ∘ coe') = f

Tactic:
cPkg.extend_comp_coe hf

Premises used: UniformSpace.Completion.coe', AbstractCompletion.extend_comp_coe, Quotient, SeparationQuotient, SeparationQuotient.mk, UniformSpace.Completion.extension, UniformSpace.Completion.cPkg, UniformSpace.Completion
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
β : Type u_2
inst_1 : UniformSpace β
f : α → β
⊢ UniformContinuous (α := Completion α) (β := Completion β) (Completion.map f)

Tactic:
cPkg.uniformContinuous_map cPkg f

Premises used: UniformSpace.Completion.map, Quotient, SeparationQuotient, AbstractCompletion.uniformContinuous_map, UniformSpace.Completion.cPkg, UniformSpace.Completion
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u_1
inst : UniformSpace α
β : Type u_2
inst_1 : UniformSpace β
f : α → β
⊢ Continuous (X := Completion α) (Y := Completion β) (Completion.map f)

Tactic:
cPkg.continuous_map cPkg f

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

Tactic:
cPkg.map_coe cPkg hf a

Premises used: UniformSpace.Completion.map, UniformSpace.Completion.coe', AbstractCompletion.map_coe, Quotient, SeparationQuotient, SeparationQuotient.mk, UniformSpace.Completion.cPkg, UniformSpace.Completion