-- Mathlib/Topology/UniformSpace/AbstractCompletion.lean
theorem compare_comp_eq_compare (γ : Type*) [TopologicalSpace γ]
    [T3Space γ] {f : α → γ} (cont_f : Continuous f) :
    letI := pkg.uniformStruct.toTopologicalSpace
    letI := pkg'.uniformStruct.toTopologicalSpace
    (∀ a : pkg.space,
      Filter.Tendsto f (Filter.comap pkg.coe (𝓝 a)) (𝓝 ((pkg.isDenseInducing.extend f) a))) →
      pkg.isDenseInducing.extend f ∘ pkg'.compare pkg = pkg'.isDenseInducing.extend f

Proof state:
α : Type u_1
inst✝² : UniformSpace α
pkg pkg' : AbstractCompletion α
γ : Type u_3
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
f : α → γ
cont_f : Continuous f
x✝ : UniformSpace pkg'.space := pkg'.uniformStruct
⊢ (∀ (a : pkg.space), Tendsto f (comap pkg.coe (𝓝 a)) (𝓝 (⋯.extend f a))) → ⋯.extend f ∘ pkg'.compare pkg = ⋯.extend f

Tactic:
let _ := pkg.uniformStruct

Result:
α : Type u_1
inst✝² : UniformSpace α
pkg pkg' : AbstractCompletion α
γ : Type u_3
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
f : α → γ
cont_f : Continuous f
x✝¹ : UniformSpace pkg'.space := pkg'.uniformStruct
x✝ : UniformSpace pkg.space := pkg.uniformStruct
⊢ (∀ (a : pkg.space), Tendsto f (comap pkg.coe (𝓝 a)) (𝓝 (⋯.extend f a))) → ⋯.extend f ∘ pkg'.compare pkg = ⋯.extend f

Proof state:
α : Type u_1
inst✝² : UniformSpace α
pkg pkg' : AbstractCompletion α
γ : Type u_3
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
f : α → γ
cont_f : Continuous f
x✝¹ : UniformSpace pkg'.space := pkg'.uniformStruct
x✝ : 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, implies_true]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : UniformSpace α
pkg pkg' : AbstractCompletion α
γ : Type u_3
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
f : α → γ
cont_f : Continuous f
x✝¹ : UniformSpace pkg'.space := pkg'.uniformStruct
x✝ : 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
⊢ ⋯.extend f ∘ pkg'.compare pkg = ⋯.extend f

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

Result:
α : Type u_1
inst✝² : UniformSpace α
pkg pkg' : AbstractCompletion α
γ : Type u_3
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
f : α → γ
cont_f : Continuous f
x✝¹ : UniformSpace pkg'.space := pkg'.uniformStruct
x✝ : 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
⊢ Continuous (⋯.extend f)

Proof state:
α : Type u_1
inst✝² : UniformSpace α
pkg pkg' : AbstractCompletion α
γ : Type u_3
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
f : α → γ
cont_f : Continuous f
x✝¹ : UniformSpace pkg'.space := pkg'.uniformStruct
x✝ : 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
⊢ Continuous (⋯.extend f)

Tactic:
apply IsDenseInducing.continuous_extend

Result:
case hf
α : Type u_1
inst✝² : UniformSpace α
pkg pkg' : AbstractCompletion α
γ : Type u_3
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
f : α → γ
cont_f : Continuous f
x✝¹ : UniformSpace pkg'.space := pkg'.uniformStruct
x✝ : 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
⊢ ∀ (b : pkg.space), ∃ c, Tendsto f (comap pkg.coe (𝓝 b)) (𝓝 c)

Proof state:
α : Type u_1
inst✝² : UniformSpace α
pkg pkg' : AbstractCompletion α
γ : Type u_3
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
f : α → γ
cont_f : Continuous f
x✝¹ : UniformSpace pkg'.space := pkg'.uniformStruct
x✝ : UniformSpace pkg.space := pkg.uniformStruct
⊢ (∀ (a : pkg.space), Tendsto f (comap pkg.coe (𝓝 a)) (𝓝 (⋯.extend f a))) → ⋯.extend f ∘ pkg'.compare pkg = ⋯.extend f

Tactic:
intro h

Result:
α : Type u_1
inst✝² : UniformSpace α
pkg pkg' : AbstractCompletion α
γ : Type u_3
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
f : α → γ
cont_f : Continuous f
x✝¹ : UniformSpace pkg'.space := pkg'.uniformStruct
x✝ : UniformSpace pkg.space := pkg.uniformStruct
h : ∀ (a : pkg.space), Tendsto f (comap pkg.coe (𝓝 a)) (𝓝 (⋯.extend f a))
⊢ ⋯.extend f ∘ pkg'.compare pkg = ⋯.extend f

Proof state:
α : Type u_1
inst✝² : UniformSpace α
pkg pkg' : AbstractCompletion α
γ : Type u_3
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
f : α → γ
cont_f : Continuous f
⊢ (∀ (a : pkg.space), Tendsto f (comap pkg.coe (𝓝 a)) (𝓝 (⋯.extend f a))) → ⋯.extend f ∘ pkg'.compare pkg = ⋯.extend f

Tactic:
let _ := pkg'.uniformStruct

Result:
α : Type u_1
inst✝² : UniformSpace α
pkg pkg' : AbstractCompletion α
γ : Type u_3
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
f : α → γ
cont_f : Continuous f
x✝ : UniformSpace pkg'.space := pkg'.uniformStruct
⊢ (∀ (a : pkg.space), Tendsto f (comap pkg.coe (𝓝 a)) (𝓝 (⋯.extend f a))) → ⋯.extend f ∘ pkg'.compare pkg = ⋯.extend f

Proof state:
case hf
α : Type u_1
inst✝² : UniformSpace α
pkg pkg' : AbstractCompletion α
γ : Type u_3
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
f : α → γ
cont_f : Continuous f
x✝¹ : UniformSpace pkg'.space := pkg'.uniformStruct
x✝ : 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
⊢ ∀ (b : pkg.space), ∃ c, Tendsto f (comap pkg.coe (𝓝 b)) (𝓝 c)

Tactic:
exact fun a ↦ ⟨(pkg.isDenseInducing.extend f) a, h a⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝² : UniformSpace α
pkg pkg' : AbstractCompletion α
γ : Type u_3
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
f : α → γ
cont_f : Continuous f
x✝¹ : UniformSpace pkg'.space := pkg'.uniformStruct
x✝ : UniformSpace pkg.space := pkg.uniformStruct
h : ∀ (a : pkg.space), Tendsto f (comap pkg.coe (𝓝 a)) (𝓝 (⋯.extend f a))
⊢ ⋯.extend f ∘ pkg'.compare pkg = ⋯.extend f

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, implies_true]

Result:
α : Type u_1
inst✝² : UniformSpace α
pkg pkg' : AbstractCompletion α
γ : Type u_3
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
f : α → γ
cont_f : Continuous f
x✝¹ : UniformSpace pkg'.space := pkg'.uniformStruct
x✝ : 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
⊢ ⋯.extend f ∘ pkg'.compare pkg = ⋯.extend f