awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
a : α
⊢ Eq (α := SeparationQuotient β) ((SeparationQuotient.mk ∘ hg.extend i ∘ fwd) (i a)) (SeparationQuotient.mk (i a))

Tactic:
simpa [fwd, hid.extend_eq hgu.uniformContinuous.continuous]
        using hg.inseparable_extend hi.uniformContinuous.continuous.continuousAt

Premises used: UniformContinuous.continuous, Continuous.continuousAt, IsDenseInducing.inseparable_extend, IsUniformInducing.uniformContinuous, IsDenseInducing.extend_eq
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
⊢ Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk

Tactic:
have key : SeparationQuotient.mk ∘ hg.extend i ∘ fwd = SeparationQuotient.mk := by
    ext x
    induction x using isClosed_property hid.dense
    · exact isClosed_eq (SeparationQuotient.continuous_mk.comp (hg'.comp hfwd).continuous)
        SeparationQuotient.continuous_mk
    · simpa [fwd, hid.extend_eq hgu.uniformContinuous.continuous]
        using hg.inseparable_extend hi.uniformContinuous.continuous.continuousAt
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
⊢ IsUniformInducing fwd

Tactic:
IsUniformInducing.of_comp hfwd (SeparationQuotient.uniformContinuous_mk.comp hg') ?_

Premises used: SeparationQuotient.uniformContinuous_mk, IsUniformInducing.of_comp, UniformContinuous.comp
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
refine : IsUniformInducing (β := SeparationQuotient β) ((SeparationQuotient.mk ∘ hg.extend i) ∘ fwd)
⊢ IsUniformInducing fwd

Tactic:
refine IsUniformInducing.of_comp hfwd (SeparationQuotient.uniformContinuous_mk.comp hg') ?_

Premises used: SeparationQuotient.uniformContinuous_mk, IsUniformInducing.of_comp, UniformContinuous.comp
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
rw : IsUniformInducing.{u_2, u_2} (α := β) (β := SeparationQuotient β) SeparationQuotient.mk
⊢ IsUniformInducing (β := SeparationQuotient β) ((SeparationQuotient.mk ∘ hg.extend i) ∘ fwd)

Tactic:
rw [Function.comp_assoc, key]

Premises used: Function.comp_assoc
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
⊢ IsUniformInducing.{u_2, u_2} (α := β) (β := SeparationQuotient β) SeparationQuotient.mk

Tactic:
SeparationQuotient.isUniformInducing_mk

Premises used: SeparationQuotient.isUniformInducing_mk
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
⊢ IsUniformInducing.{u_2, u_2} (α := β) (β := SeparationQuotient β) SeparationQuotient.mk

Tactic:
exact SeparationQuotient.isUniformInducing_mk

Premises used: SeparationQuotient.isUniformInducing_mk
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
⊢ IsUniformInducing fwd

Tactic:
have hfu : IsUniformInducing fwd := by
    refine IsUniformInducing.of_comp hfwd (SeparationQuotient.uniformContinuous_mk.comp hg') ?_
    rw [Function.comp_assoc, key]
    exact SeparationQuotient.isUniformInducing_mk
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
hfu : IsUniformInducing fwd
⊢ Subset (α := Set (SeparationQuotient γ)) (range (SeparationQuotient.mk ∘ hid.extend f))
    (closure (range (SeparationQuotient.mk ∘ f)))

Tactic:
((SeparationQuotient.continuous_mk.comp (uniformContinuous_uniformly_extend hi hid.dense
      h.uniformContinuous).continuous).range_subset_closure_image_dense hid.dense).trans
      (closure_mono (subset_of_eq ?_))

Premises used: SeparationQuotient.continuous_mk, Continuous.range_subset_closure_image_dense, uniformContinuous_uniformly_extend, Continuous.comp, HasSubset.Subset.trans, subset_of_eq, closure_mono, UniformContinuous.continuous, IsDenseInducing.dense, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
hfu : IsUniformInducing fwd
refine :
  Eq (α := Set (SeparationQuotient γ)) (SeparationQuotient.mk ∘ ⋯.extend f '' range i)
    (range (SeparationQuotient.mk ∘ f))
⊢ Subset (α := Set (SeparationQuotient γ)) (range (SeparationQuotient.mk ∘ hid.extend f))
    (closure (range (SeparationQuotient.mk ∘ f)))

Tactic:
refine ((SeparationQuotient.continuous_mk.comp (uniformContinuous_uniformly_extend hi hid.dense
      h.uniformContinuous).continuous).range_subset_closure_image_dense hid.dense).trans
      (closure_mono (subset_of_eq ?_))

Premises used: SeparationQuotient.continuous_mk, Continuous.range_subset_closure_image_dense, uniformContinuous_uniformly_extend, Continuous.comp, HasSubset.Subset.trans, subset_of_eq, closure_mono, UniformContinuous.continuous, IsDenseInducing.dense, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
hfu : IsUniformInducing fwd
rw :
  Eq (α := Set (SeparationQuotient γ)) (range ((SeparationQuotient.mk ∘ ⋯.extend f) ∘ i))
    (range (SeparationQuotient.mk ∘ f))
⊢ Eq (α := Set (SeparationQuotient γ)) (SeparationQuotient.mk ∘ ⋯.extend f '' range i)
    (range (SeparationQuotient.mk ∘ f))

Tactic:
rw [← range_comp]

Premises used: Set.range_comp
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
hfu : IsUniformInducing fwd
apply : Eq (α := α → SeparationQuotient γ) ((SeparationQuotient.mk ∘ ⋯.extend f) ∘ i) (SeparationQuotient.mk ∘ f)
⊢ Eq (α := Set (SeparationQuotient γ)) (range ((SeparationQuotient.mk ∘ ⋯.extend f) ∘ i))
    (range (SeparationQuotient.mk ∘ f))

Tactic:
apply congrArg range

Premises used: congrArg, Set.range
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
hfu : IsUniformInducing fwd
h₁ :
  ∀ (x : α),
    Eq (α := SeparationQuotient γ) (((SeparationQuotient.mk ∘ ⋯.extend f) ∘ i) x) ((SeparationQuotient.mk ∘ f) x)
⊢ Eq (α := α → SeparationQuotient γ) ((SeparationQuotient.mk ∘ ⋯.extend f) ∘ i) (SeparationQuotient.mk ∘ f)

Tactic:
funext x
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
hfu : IsUniformInducing fwd
x : α
⊢ Eq (α := SeparationQuotient γ) (((SeparationQuotient.mk ∘ ⋯.extend f) ∘ i) x) ((SeparationQuotient.mk ∘ f) x)

Tactic:
simpa using (hid.inseparable_extend h.uniformContinuous.continuous.continuousAt)

Premises used: UniformContinuous.continuous, Continuous.continuousAt, IsDenseInducing.inseparable_extend, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
hfu : IsUniformInducing fwd
⊢ Subset (α := Set (SeparationQuotient γ)) (range (SeparationQuotient.mk ∘ hid.extend f))
    (closure (range (SeparationQuotient.mk ∘ f)))

Tactic:
have hrr : range (SeparationQuotient.mk ∘ hid.extend f) ⊆
      closure (range (SeparationQuotient.mk ∘ f)) := by
    refine ((SeparationQuotient.continuous_mk.comp (uniformContinuous_uniformly_extend hi hid.dense
      h.uniformContinuous).continuous).range_subset_closure_image_dense hid.dense).trans
      (closure_mono (subset_of_eq ?_))
    rw [← range_comp]
    apply congrArg range
    funext x
    simpa using (hid.inseparable_extend h.uniformContinuous.continuous.continuousAt)
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this_1 : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
hfu : IsUniformInducing fwd
hrr :
  Subset (α := Set (SeparationQuotient γ)) (range (SeparationQuotient.mk ∘ hid.extend f))
    (closure (range (SeparationQuotient.mk ∘ f)))
this :
  Subtype.val (p := fun (x : SeparationQuotient γ) ↦ x ∈ closure (range sf)) ∘ fwd =
    SeparationQuotient.mk ∘ hid.extend f
rw : IsUniformInducing (Subtype.val (p := fun (x : SeparationQuotient γ) ↦ x ∈ closure (range sf)) ∘ fwd)
⊢ IsUniformInducing (hid.extend f)

Tactic:
rw [← SeparationQuotient.isUniformInducing_mk.of_comp_iff, ← this]

Premises used: SeparationQuotient.isUniformInducing_mk, IsUniformInducing.of_comp_iff
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this_1 : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
hfu : IsUniformInducing fwd
hrr :
  Subset (α := Set (SeparationQuotient γ)) (range (SeparationQuotient.mk ∘ hid.extend f))
    (closure (range (SeparationQuotient.mk ∘ f)))
this :
  Subtype.val (p := fun (x : SeparationQuotient γ) ↦ x ∈ closure (range sf)) ∘ fwd =
    SeparationQuotient.mk ∘ hid.extend f
⊢ IsUniformInducing (Subtype.val (p := fun (x : SeparationQuotient γ) ↦ x ∈ closure (range sf)) ∘ fwd)

Tactic:
(isUniformInducing_val _).comp hfu

Premises used: isUniformInducing_val, IsUniformInducing.comp
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this_1 : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
hfu : IsUniformInducing fwd
hrr :
  Subset (α := Set (SeparationQuotient γ)) (range (SeparationQuotient.mk ∘ hid.extend f))
    (closure (range (SeparationQuotient.mk ∘ f)))
this :
  Subtype.val (p := fun (x : SeparationQuotient γ) ↦ x ∈ closure (range sf)) ∘ fwd =
    SeparationQuotient.mk ∘ hid.extend f
⊢ IsUniformInducing (Subtype.val (p := fun (x : SeparationQuotient γ) ↦ x ∈ closure (range sf)) ∘ fwd)

Tactic:
exact (isUniformInducing_val _).comp hfu

Premises used: isUniformInducing_val, IsUniformInducing.comp