awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.AbsoluteValue
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
R : Type u_2
inst_3 : CommRing R
abv : AbsoluteValue R 𝕜
⊢ (𝓤 R).HasBasis (fun (x : 𝕜) ↦ 0 < x) fun (ε : 𝕜) ↦ {p : R × R | (abv : (a : R) → 𝕜) (p.2 - p.1) < ε}

Tactic:
UniformSpace.hasBasis_ofFun (exists_gt _) _ _ _ _ _

Premises used: UniformSpace.hasBasis_ofFun, NoMaxOrder.exists_gt
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
⊢ closure (range pkg.coe) = univ

Tactic:
pkg.dense.closure_range

Premises used: AbstractCompletion.dense, DenseRange.closure_range
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
⊢ IsDenseInducing pkg.coe

Tactic:
⟨pkg.isUniformInducing.isInducing, pkg.dense⟩

Premises used: AbstractCompletion.dense, IsDenseInducing.mk, IsUniformInducing.isInducing, AbstractCompletion.isUniformInducing
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
⊢ UniformContinuous pkg.coe

Tactic:
IsUniformInducing.uniformContinuous pkg.isUniformInducing

Premises used: AbstractCompletion.isUniformInducing, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
⊢ Continuous pkg.coe

Tactic:
pkg.uniformContinuous_coe.continuous

Premises used: AbstractCompletion.uniformContinuous_coe, UniformContinuous.continuous
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
p : pkg.space → Prop
a : pkg.space
hp : IsClosed.{vα} (X := pkg.space) {a : pkg.space | p a}
ih : ∀ (a : α), p (pkg.coe a)
⊢ p a

Tactic:
isClosed_property pkg.dense hp ih a

Premises used: AbstractCompletion.dense, isClosed_property
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : TopologicalSpace β
inst_2 : T2Space β
f g : pkg.space → β
hf : Continuous f
hg : Continuous g
h : ∀ (a : α), f (pkg.coe a) = g (pkg.coe a)
⊢ f = g

Tactic:
funext fun a => pkg.induction_on a (isClosed_eq hf hg) h

Premises used: funext, AbstractCompletion.induction_on
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
hf : UniformContinuous f
⊢ pkg.extend f = ⋯.extend f

Tactic:
if_pos hf

Premises used: if_pos, AbstractCompletion.extend
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
hf : UniformContinuous f
x : α
rw : Inseparable (⋯.extend f (pkg.coe x)) (f x)
⊢ Inseparable (pkg.extend f (pkg.coe x)) (f x)

Tactic:
rw [extend_def _ hf]

Premises used: AbstractCompletion.extend_def
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
hf : UniformContinuous f
x : α
⊢ Inseparable (⋯.extend f (pkg.coe x)) (f x)

Tactic:
pkg.isDenseInducing.inseparable_extend hf.continuous.continuousAt

Premises used: UniformContinuous.continuous, Continuous.continuousAt, IsDenseInducing.inseparable_extend, AbstractCompletion.isDenseInducing
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
hf : UniformContinuous f
x : α
⊢ Inseparable (⋯.extend f (pkg.coe x)) (f x)

Tactic:
exact pkg.isDenseInducing.inseparable_extend hf.continuous.continuousAt

Premises used: UniformContinuous.continuous, Continuous.continuousAt, IsDenseInducing.inseparable_extend, AbstractCompletion.isDenseInducing
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
inst_2 : T2Space β
hf : UniformContinuous f
a : α
rw : ⋯.extend f (pkg.coe a) = f a
⊢ pkg.extend f (pkg.coe a) = f a

Tactic:
rw [pkg.extend_def hf]

Premises used: AbstractCompletion.extend_def
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
inst_2 : T2Space β
hf : UniformContinuous f
a : α
⊢ ⋯.extend f (pkg.coe a) = f a

Tactic:
pkg.isDenseInducing.extend_eq hf.continuous a

Premises used: UniformContinuous.continuous, AbstractCompletion.isDenseInducing, IsDenseInducing.extend_eq
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
inst_2 : T2Space β
hf : UniformContinuous f
a : α
⊢ ⋯.extend f (pkg.coe a) = f a

Tactic:
exact pkg.isDenseInducing.extend_eq hf.continuous a

Premises used: UniformContinuous.continuous, AbstractCompletion.isDenseInducing, IsDenseInducing.extend_eq
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
inst_2 : CompleteSpace β
pos : ∀ (hf : UniformContinuous f), UniformContinuous (pkg.extend f)
neg : ∀ (hf : ¬UniformContinuous f), UniformContinuous (pkg.extend f)
⊢ UniformContinuous (pkg.extend f)

Tactic:
by_cases hf : UniformContinuous f

Premises used: UniformContinuous
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
inst_2 : CompleteSpace β
hf : UniformContinuous f
pos : UniformContinuous (⋯.extend f)
⊢ UniformContinuous (pkg.extend f)

Tactic:
rw [pkg.extend_def hf]

Premises used: AbstractCompletion.extend_def
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
inst_2 : CompleteSpace β
hf : UniformContinuous f
⊢ UniformContinuous (⋯.extend f)

Tactic:
uniformContinuous_uniformly_extend pkg.isUniformInducing pkg.dense hf

Premises used: AbstractCompletion.dense, uniformContinuous_uniformly_extend, AbstractCompletion.isUniformInducing
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
inst_2 : CompleteSpace β
hf : UniformContinuous f
⊢ UniformContinuous (⋯.extend f)

Tactic:
exact uniformContinuous_uniformly_extend pkg.isUniformInducing pkg.dense hf

Premises used: AbstractCompletion.dense, uniformContinuous_uniformly_extend, AbstractCompletion.isUniformInducing
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
inst_2 : CompleteSpace β
hf : ¬UniformContinuous f
neg : UniformContinuous.{vα, uβ} (β := β) fun (x : pkg.space) ↦ f (⋯.some x)
⊢ UniformContinuous (if UniformContinuous f then ⋯.extend f else fun (x : pkg.space) ↦ f (⋯.some x))

Tactic:
rw [if_neg hf]

Premises used: if_neg
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
inst_2 : CompleteSpace β
hf : ¬UniformContinuous f
a b : pkg.space
⊢ f (⋯.some a) = f (⋯.some b)

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

Tactic:
exact uniformContinuous_of_const fun a b => by congr 1

Premises used: uniformContinuous_of_const
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
inst_2 : CompleteSpace β
⊢ Continuous (pkg.extend f)

Tactic:
pkg.uniformContinuous_extend.continuous

Premises used: UniformContinuous.continuous, AbstractCompletion.uniformContinuous_extend
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
inst_2 : CompleteSpace β
h : IsUniformInducing f
rw : IsUniformInducing (⋯.extend f)
⊢ IsUniformInducing (pkg.extend f)

Tactic:
rw [extend_def _ h.uniformContinuous]

Premises used: AbstractCompletion.extend_def, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
inst_2 : CompleteSpace β
h : IsUniformInducing f
⊢ IsUniformInducing (⋯.extend f)

Tactic:
pkg.isDenseInducing.isUniformInducing_extend pkg.isUniformInducing h

Premises used: IsDenseInducing.isUniformInducing_extend, AbstractCompletion.isUniformInducing, AbstractCompletion.isDenseInducing
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
inst_2 : CompleteSpace β
h : IsUniformInducing f
⊢ IsUniformInducing (⋯.extend f)

Tactic:
exact pkg.isDenseInducing.isUniformInducing_extend pkg.isUniformInducing h

Premises used: IsDenseInducing.isUniformInducing_extend, AbstractCompletion.isUniformInducing, AbstractCompletion.isDenseInducing
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
inst_2 : CompleteSpace β
inst_3 : T0Space β
hf : UniformContinuous f
g : pkg.space → β
hg : UniformContinuous g
h : ∀ (a : α), f a = g (pkg.coe a)
apply : ∀ (a : α), pkg.extend f (pkg.coe a) = g (pkg.coe a)
⊢ pkg.extend f = g

Tactic:
apply pkg.funext pkg.continuous_extend hg.continuous

Premises used: AbstractCompletion.funext, UniformContinuous.continuous, AbstractCompletion.continuous_extend
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
inst_2 : CompleteSpace β
inst_3 : T0Space β
hf : UniformContinuous f
g : pkg.space → β
hg : UniformContinuous g
h : ∀ (a : α), f a = g (pkg.coe a)
⊢ ∀ (a : α), pkg.extend f (pkg.coe a) = g (pkg.coe a)

Tactic:
simpa only [pkg.extend_coe hf] using h

Premises used: AbstractCompletion.extend_coe
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
inst_2 : CompleteSpace β
inst_3 : T0Space β
f : pkg.space → β
hf : UniformContinuous f
⊢ pkg.extend (f ∘ pkg.coe) = f

Tactic:
funext fun x =>
    pkg.induction_on x (isClosed_eq pkg.continuous_extend hf.continuous) fun y =>
      pkg.extend_coe (hf.comp <| pkg.uniformContinuous_coe) y

Premises used: funext, AbstractCompletion.induction_on
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
⊢ UniformContinuous (pkg.map pkg' f)

Tactic:
pkg.uniformContinuous_extend

Premises used: AbstractCompletion.uniformContinuous_extend, AbstractCompletion.map
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
⊢ Continuous (pkg.map pkg' f)

Tactic:
pkg.continuous_extend

Premises used: AbstractCompletion.map, AbstractCompletion.continuous_extend
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
hf : UniformContinuous f
a : α
⊢ pkg.map pkg' f (pkg.coe a) = pkg'.coe (f a)

Tactic:
pkg.extend_coe (pkg'.uniformContinuous_coe.comp hf) a

Premises used: AbstractCompletion.uniformContinuous_coe, AbstractCompletion.extend_coe, UniformContinuous.comp, AbstractCompletion.map
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
a : α
simp_rw : pkg.extend (fun (x : α) ↦ (g ∘ pkg.coe) x) (pkg.coe a) = (g ∘ pkg.coe) a
⊢ pkg.extend (pkg'.coe ∘ f) (pkg.coe a) = g (pkg.coe a)

Tactic:
simp_rw [Function.comp_def, h, ← comp_apply (f := g)]

Premises used: Function.comp_def, Function.comp_apply
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
a : α
rw rw₁ : (g ∘ pkg.coe) a = (g ∘ pkg.coe) a
⊢ pkg.extend (fun (x : α) ↦ (g ∘ pkg.coe) x) (pkg.coe a) = (g ∘ pkg.coe) a

Tactic:
rw [pkg.extend_coe (hg.comp pkg.uniformContinuous_coe)]

Premises used: AbstractCompletion.uniformContinuous_coe, AbstractCompletion.extend_coe, UniformContinuous.comp
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
⊢ pkg.map pkg id = id

Tactic:
pkg.map_unique pkg uniformContinuous_id fun _ => rfl

Premises used: uniformContinuous_id, AbstractCompletion.map_unique, rfl
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst_2 : UniformSpace γ
inst_3 : CompleteSpace γ
inst_4 : T0Space γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
rw : f (g a) = (f ∘ g) a
⊢ (pkg'.extend f ∘ pkg.map pkg' g) (pkg.coe a) = pkg.extend (f ∘ g) (pkg.coe a)

Tactic:
rw [pkg.extend_coe (hf.comp hg), comp_apply, pkg.map_coe pkg' hg, pkg'.extend_coe hf]

Premises used: AbstractCompletion.extend_coe, AbstractCompletion.map_coe, UniformContinuous.comp, Function.comp_apply
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst_2 : UniformSpace γ
inst_3 : CompleteSpace γ
inst_4 : T0Space γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
⊢ f (g a) = (f ∘ g) a

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst_2 : UniformSpace γ
pkg'' : AbstractCompletion.{vγ, uγ} γ
g : β → γ
f : α → β
hg : UniformContinuous g
hf : UniformContinuous f
⊢ pkg'.map pkg'' g ∘ pkg.map pkg' f = pkg.map pkg'' (g ∘ f)

Tactic:
pkg.extend_map pkg' (pkg''.uniformContinuous_coe.comp hg) hf

Premises used: AbstractCompletion.extend_map, AbstractCompletion.uniformContinuous_coe, UniformContinuous.comp, AbstractCompletion.map
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
γ : Type uγ
inst_2 : UniformSpace γ
pkg'' : AbstractCompletion.{vγ, uγ} γ
e : α ≃ᵤ β
⊢ pkg'.map pkg (⇑e.symm : (a : β) → α) ∘ pkg.map pkg' (⇑e : (a : α) → β) = id

Tactic:
simp [map_comp _ _ _ e.symm.uniformContinuous e.uniformContinuous]

Premises used: UniformEquiv.symm, UniformEquiv.uniformContinuous, AbstractCompletion.map_comp
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
γ : Type uγ
inst_2 : UniformSpace γ
pkg'' : AbstractCompletion.{vγ, uγ} γ
e : α ≃ᵤ β
⊢ pkg.map pkg' (⇑e : (a : α) → β) ∘ pkg'.map pkg (⇑e.symm : (a : β) → α) = id

Tactic:
simp [map_comp _ _ _ e.uniformContinuous e.symm.uniformContinuous]

Premises used: UniformEquiv.symm, UniformEquiv.uniformContinuous, AbstractCompletion.map_comp
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
e : α ≃ᵤ β
⊢ (pkg.mapEquiv pkg' e).symm = pkg'.mapEquiv pkg e.symm

Tactic:
rfl

Premises used: AbstractCompletion.mapEquiv, UniformEquiv.symm, AbstractCompletion.map, Equiv.symm, AbstractCompletion.extend, rfl, ite
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
e : α ≃ᵤ β
a : α
⊢ (pkg.mapEquiv pkg' e : (a : pkg.space) → pkg'.space) (pkg.coe a) = pkg'.coe ((e : (a : α) → β) a)

Tactic:
pkg.map_coe pkg' e.uniformContinuous _

Premises used: AbstractCompletion.map_coe, UniformEquiv.uniformContinuous, AbstractCompletion.map, AbstractCompletion.extend, ite
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
⊢ UniformContinuous (pkg.compare pkg')

Tactic:
pkg.uniformContinuous_extend

Premises used: AbstractCompletion.uniformContinuous_extend, AbstractCompletion.compare
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
a : α
⊢ pkg.compare pkg' (pkg.coe a) = pkg'.coe a

Tactic:
pkg.extend_coe pkg'.uniformContinuous_coe a

Premises used: AbstractCompletion.uniformContinuous_coe, AbstractCompletion.extend_coe, AbstractCompletion.compare
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
⊢ UniformContinuous (pkg.compare pkg')

Tactic:
have uc := pkg.uniformContinuous_compare pkg'
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
uc : UniformContinuous (pkg.compare pkg')
⊢ UniformContinuous (pkg'.compare pkg)

Tactic:
have uc' := pkg'.uniformContinuous_compare pkg
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
uc : UniformContinuous (pkg.compare pkg')
uc' : UniformContinuous (pkg'.compare pkg)
apply : ∀ (a : α), (pkg.compare pkg' ∘ pkg'.compare pkg) (pkg'.coe a) = id (pkg'.coe a)
⊢ pkg.compare pkg' ∘ pkg'.compare pkg = id

Tactic:
apply pkg'.funext (uc.comp uc').continuous continuous_id

Premises used: AbstractCompletion.funext, UniformContinuous.comp, UniformContinuous.continuous, continuous_id
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
uc : UniformContinuous (pkg.compare pkg')
uc' : UniformContinuous (pkg'.compare pkg)
a : α
rw : pkg'.coe a = id (pkg'.coe a)
⊢ (pkg.compare pkg' ∘ pkg'.compare pkg) (pkg'.coe a) = id (pkg'.coe a)

Tactic:
rw [comp_apply, pkg'.compare_coe pkg, pkg.compare_coe pkg']

Premises used: AbstractCompletion.compare_coe, Function.comp_apply
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
uc : UniformContinuous (pkg.compare pkg')
uc' : UniformContinuous (pkg'.compare pkg)
a : α
⊢ pkg'.coe a = id (pkg'.coe a)

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
⊢ UniformContinuous.{vα, vα'} (α := pkg.space) (β := pkg'.space)
    (⇑(pkg.compareEquiv pkg') : (a : pkg.space) → pkg'.space)

Tactic:
pkg.uniformContinuous_compare pkg'

Premises used: AbstractCompletion.uniformContinuous_compare, AbstractCompletion.compare, AbstractCompletion.extend, ite
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
⊢ UniformContinuous.{vα', vα} (α := pkg'.space) (β := pkg.space)
    (⇑(pkg.compareEquiv pkg').symm : (a : pkg'.space) → pkg.space)

Tactic:
pkg'.uniformContinuous_compare pkg

Premises used: AbstractCompletion.uniformContinuous_compare, AbstractCompletion.compare, AbstractCompletion.extend, ite
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
γ : Type uγ
inst_1 : TopologicalSpace γ
inst_2 : T3Space γ
f : α → γ
cont_f : Continuous[inst.toTopologicalSpace, inst_1] f
x_1 : UniformSpace pkg'.space := pkg'.uniformStruct
x_2 : UniformSpace pkg.space := pkg.uniformStruct
h : ∀ (a : pkg.space), Tendsto f (comap pkg.coe (𝓝 a)) (𝓝 (⋯.extend f a))
x : α
⊢ (⋯.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x

Tactic:
simp only [Function.comp_apply, compare_coe, IsDenseInducing.extend_eq _ cont_f]

Premises used: AbstractCompletion.compare_coe, Function.comp_apply, IsDenseInducing.extend_eq
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
γ : Type uγ
inst_1 : TopologicalSpace γ
inst_2 : T3Space γ
f : α → γ
cont_f : Continuous[inst.toTopologicalSpace, inst_1] f
x : UniformSpace pkg'.space := pkg'.uniformStruct
x_1 : UniformSpace pkg.space := pkg.uniformStruct
h : ∀ (a : pkg.space), Tendsto f (comap pkg.coe (𝓝 a)) (𝓝 (⋯.extend f a))
⊢ ∀ (x : α), (⋯.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x

Tactic:
have (x : α) : (pkg.isDenseInducing.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x := by
    simp only [Function.comp_apply, compare_coe, IsDenseInducing.extend_eq _ cont_f]
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
γ : Type uγ
inst_1 : TopologicalSpace γ
inst_2 : T3Space γ
f : α → γ
cont_f : Continuous[inst.toTopologicalSpace, inst_1] f
x : UniformSpace pkg'.space := pkg'.uniformStruct
x_1 : UniformSpace pkg.space := pkg.uniformStruct
h : ∀ (a : pkg.space), Tendsto f (comap pkg.coe (𝓝 a)) (𝓝 (⋯.extend f a))
this : ∀ (x : α), (⋯.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x
apply : Continuous[_, inst_1] (⋯.extend f)
⊢ ⋯.extend f ∘ pkg'.compare pkg = ⋯.extend f

Tactic:
apply (IsDenseInducing.extend_unique (AbstractCompletion.isDenseInducing _) this
    (Continuous.comp _ (uniformContinuous_compare pkg' pkg).continuous)).symm

Premises used: AbstractCompletion.uniformContinuous_compare, Continuous.comp, IsDenseInducing.extend_unique, UniformContinuous.continuous, Eq.symm, AbstractCompletion.isDenseInducing