awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.TopPair
Goal:
X Y : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
fst : (F.trans G).symm.fst = (G.symm.trans F.symm).fst
snd : (F.trans G).symm.snd = (G.symm.trans F.symm).snd
⊢ (F.trans G).symm = G.symm.trans F.symm

Tactic:
ext : 1
-- Module: Mathlib.Topology.Category.TopPair
Goal:
X Y : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
⊢ (F.trans G).symm.fst = (G.symm.trans F.symm).fst

Tactic:
ContinuousMap.Homotopy.symm_trans _ _

Premises used: ContinuousMap.Homotopy.symm_trans, ContinuousMap.Homotopy.trans, ContinuousMap.Homotopy.symm
-- Module: Mathlib.Topology.Category.TopPair
Goal:
X Y : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
⊢ (F.trans G).symm.fst = (G.symm.trans F.symm).fst

Tactic:
exact ContinuousMap.Homotopy.symm_trans _ _

Premises used: ContinuousMap.Homotopy.symm_trans
-- Module: Mathlib.Topology.Category.TopPair
Goal:
X Y : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
⊢ (F.trans G).symm.snd = (G.symm.trans F.symm).snd

Tactic:
ContinuousMap.Homotopy.symm_trans _ _

Premises used: ContinuousMap.Homotopy.symm_trans, ContinuousMap.Homotopy.trans, ContinuousMap.Homotopy.symm
-- Module: Mathlib.Topology.Category.TopPair
Goal:
X Y : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
⊢ (F.trans G).symm.snd = (G.symm.trans F.symm).snd

Tactic:
exact ContinuousMap.Homotopy.symm_trans _ _

Premises used: ContinuousMap.Homotopy.symm_trans
-- Module: Mathlib.Topology.Category.TopPair
Goal:
X Y : TopPair
⊢ _root_.Equivalence.{u + 1} (α := X ⟶ Y) Homotopic

Tactic:
⟨fun f ↦ ⟨Homotopy.refl f⟩, fun h ↦ h.map Homotopy.symm, fun h₀ h₁ ↦ h₀.map2 Homotopy.trans h₁⟩

Premises used: TopPair.Homotopy.refl, Nonempty.map2, TopPair.Homotopy.trans, Nonempty.intro, TopPair.Homotopy.symm, Equivalence.mk, Nonempty.map
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X Y : UniformSpaceCat
f : X.Hom Y
hom' :
  {
        hom' :=
          Subtype.mk (p := fun (f : X.carrier → Y.carrier) ↦ UniformContinuous f)
            ((↑f.hom' : X.carrier → Y.carrier) ∘
              (↑(Hom.hom'
                    { hom' := Subtype.mk (p := fun (f : X.carrier → X.carrier) ↦ UniformContinuous f) id ⋯ :
                      X.Hom X }) :
                X.carrier → X.carrier))
            ⋯ :
        X.Hom Y }.hom' =
    f.hom'
⊢ {
      hom' :=
        Subtype.mk (p := fun (f : X.carrier → Y.carrier) ↦ UniformContinuous f)
          ((↑f.hom' : X.carrier → Y.carrier) ∘
            (↑(Hom.hom'
                  { hom' := Subtype.mk (p := fun (f : X.carrier → X.carrier) ↦ UniformContinuous f) id ⋯ : X.Hom X }) :
              X.carrier → X.carrier))
          ⋯ :
      X.Hom Y } =
    f

Tactic:
apply Hom.ext

Premises used: UniformSpaceCat.Hom.ext
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X Y : UniformSpaceCat
f : X.Hom Y
⊢ {
        hom' :=
          Subtype.mk (p := fun (f : X.carrier → Y.carrier) ↦ UniformContinuous f)
            ((↑f.hom' : X.carrier → Y.carrier) ∘
              (↑(Hom.hom'
                    { hom' := Subtype.mk (p := fun (f : X.carrier → X.carrier) ↦ UniformContinuous f) id ⋯ :
                      X.Hom X }) :
                X.carrier → X.carrier))
            ⋯ :
        X.Hom Y }.hom' =
    f.hom'

Tactic:
simp
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X Y : UniformSpaceCat
f : X.Hom Y
hom' :
  {
        hom' :=
          Subtype.mk (p := fun (f : X.carrier → Y.carrier) ↦ UniformContinuous f)
            ((↑(Hom.hom'
                    { hom' := Subtype.mk (p := fun (f : Y.carrier → Y.carrier) ↦ UniformContinuous f) id ⋯ :
                      Y.Hom Y }) :
                Y.carrier → Y.carrier) ∘
              (↑f.hom' : X.carrier → Y.carrier))
            ⋯ :
        X.Hom Y }.hom' =
    f.hom'
⊢ {
      hom' :=
        Subtype.mk (p := fun (f : X.carrier → Y.carrier) ↦ UniformContinuous f)
          ((↑(Hom.hom'
                  { hom' := Subtype.mk (p := fun (f : Y.carrier → Y.carrier) ↦ UniformContinuous f) id ⋯ : Y.Hom Y }) :
              Y.carrier → Y.carrier) ∘
            (↑f.hom' : X.carrier → Y.carrier))
          ⋯ :
      X.Hom Y } =
    f

Tactic:
apply Hom.ext

Premises used: UniformSpaceCat.Hom.ext
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X Y : UniformSpaceCat
f : X.Hom Y
⊢ {
        hom' :=
          Subtype.mk (p := fun (f : X.carrier → Y.carrier) ↦ UniformContinuous f)
            ((↑(Hom.hom'
                    { hom' := Subtype.mk (p := fun (f : Y.carrier → Y.carrier) ↦ UniformContinuous f) id ⋯ :
                      Y.Hom Y }) :
                Y.carrier → Y.carrier) ∘
              (↑f.hom' : X.carrier → Y.carrier))
            ⋯ :
        X.Hom Y }.hom' =
    f.hom'

Tactic:
simp
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
W X Y Z : UniformSpaceCat
f : W.Hom X
g : X.Hom Y
h : Y.Hom Z
hom' :
  {
        hom' :=
          Subtype.mk (p := fun (f : W.carrier → Z.carrier) ↦ UniformContinuous f)
            ((↑h.hom' : Y.carrier → Z.carrier) ∘
              (↑{
                      hom' :=
                        Subtype.mk (p := fun (f : W.carrier → Y.carrier) ↦ UniformContinuous f)
                          ((↑g.hom' : X.carrier → Y.carrier) ∘ (↑f.hom' : W.carrier → X.carrier)) ⋯ :
                      W.Hom Y }.hom' :
                W.carrier → Y.carrier))
            ⋯ }.hom' =
    {
        hom' :=
          Subtype.mk (p := fun (f : W.carrier → Z.carrier) ↦ UniformContinuous f)
            ((↑{
                      hom' :=
                        Subtype.mk (p := fun (f : X.carrier → Z.carrier) ↦ UniformContinuous f)
                          ((↑h.hom' : Y.carrier → Z.carrier) ∘ (↑g.hom' : X.carrier → Y.carrier)) ⋯ :
                      X.Hom Z }.hom' :
                X.carrier → Z.carrier) ∘
              (↑f.hom' : W.carrier → X.carrier))
            ⋯ :
        W.Hom Z }.hom'
⊢ {
      hom' :=
        Subtype.mk (p := fun (f : W.carrier → Z.carrier) ↦ UniformContinuous f)
          ((↑h.hom' : Y.carrier → Z.carrier) ∘
            (↑{
                    hom' :=
                      Subtype.mk (p := fun (f : W.carrier → Y.carrier) ↦ UniformContinuous f)
                        ((↑g.hom' : X.carrier → Y.carrier) ∘ (↑f.hom' : W.carrier → X.carrier)) ⋯ :
                    W.Hom Y }.hom' :
              W.carrier → Y.carrier))
          ⋯ :
      W.Hom Z } =
    {
      hom' :=
        Subtype.mk (p := fun (f : W.carrier → Z.carrier) ↦ UniformContinuous f)
          ((↑{
                    hom' :=
                      Subtype.mk (p := fun (f : X.carrier → Z.carrier) ↦ UniformContinuous f)
                        ((↑h.hom' : Y.carrier → Z.carrier) ∘ (↑g.hom' : X.carrier → Y.carrier)) ⋯ :
                    X.Hom Z }.hom' :
              X.carrier → Z.carrier) ∘
            (↑f.hom' : W.carrier → X.carrier))
          ⋯ }

Tactic:
apply Hom.ext

Premises used: UniformSpaceCat.Hom.ext
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
W X Y Z : UniformSpaceCat
f : W.Hom X
g : X.Hom Y
h : Y.Hom Z
hom' :
  ∀ (x : W.carrier),
    (↑{
                hom' :=
                  Subtype.mk (p := fun (f : W.carrier → Z.carrier) ↦ UniformContinuous f)
                    ((↑h.hom' : Y.carrier → Z.carrier) ∘
                      (↑{
                              hom' :=
                                Subtype.mk (p := fun (f : W.carrier → Y.carrier) ↦ UniformContinuous f)
                                  ((↑g.hom' : X.carrier → Y.carrier) ∘ (↑f.hom' : W.carrier → X.carrier)) ⋯ :
                              W.Hom Y }.hom' :
                        W.carrier → Y.carrier))
                    ⋯ :
                W.Hom Z }.hom' :
          W.carrier → Z.carrier)
        x =
      (↑{
                hom' :=
                  Subtype.mk (p := fun (f : W.carrier → Z.carrier) ↦ UniformContinuous f)
                    ((↑{
                              hom' :=
                                Subtype.mk (p := fun (f : X.carrier → Z.carrier) ↦ UniformContinuous f)
                                  ((↑h.hom' : Y.carrier → Z.carrier) ∘ (↑g.hom' : X.carrier → Y.carrier)) ⋯ :
                              X.Hom Z }.hom' :
                        X.carrier → Z.carrier) ∘
                      (↑f.hom' : W.carrier → X.carrier))
                    ⋯ :
                W.Hom Z }.hom' :
          W.carrier → Z.carrier)
        x
⊢ {
        hom' :=
          Subtype.mk (p := fun (f : W.carrier → Z.carrier) ↦ UniformContinuous f)
            ((↑h.hom' : Y.carrier → Z.carrier) ∘
              (↑{
                      hom' :=
                        Subtype.mk (p := fun (f : W.carrier → Y.carrier) ↦ UniformContinuous f)
                          ((↑g.hom' : X.carrier → Y.carrier) ∘ (↑f.hom' : W.carrier → X.carrier)) ⋯ :
                      W.Hom Y }.hom' :
                W.carrier → Y.carrier))
            ⋯ }.hom' =
    {
        hom' :=
          Subtype.mk (p := fun (f : W.carrier → Z.carrier) ↦ UniformContinuous f)
            ((↑{
                      hom' :=
                        Subtype.mk (p := fun (f : X.carrier → Z.carrier) ↦ UniformContinuous f)
                          ((↑h.hom' : Y.carrier → Z.carrier) ∘ (↑g.hom' : X.carrier → Y.carrier)) ⋯ :
                      X.Hom Z }.hom' :
                X.carrier → Z.carrier) ∘
              (↑f.hom' : W.carrier → X.carrier))
            ⋯ :
        W.Hom Z }.hom'

Tactic:
ext
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
W X Y Z : UniformSpaceCat
f : W.Hom X
g : X.Hom Y
h : Y.Hom Z
x : W.carrier
⊢ (↑{
              hom' :=
                Subtype.mk (p := fun (f : W.carrier → Z.carrier) ↦ UniformContinuous f)
                  ((↑h.hom' : Y.carrier → Z.carrier) ∘
                    (↑{
                            hom' :=
                              Subtype.mk (p := fun (f : W.carrier → Y.carrier) ↦ UniformContinuous f)
                                ((↑g.hom' : X.carrier → Y.carrier) ∘ (↑f.hom' : W.carrier → X.carrier)) ⋯ :
                            W.Hom Y }.hom' :
                      W.carrier → Y.carrier))
                  ⋯ :
              W.Hom Z }.hom' :
        W.carrier → Z.carrier)
      x =
    (↑{
              hom' :=
                Subtype.mk (p := fun (f : W.carrier → Z.carrier) ↦ UniformContinuous f)
                  ((↑{
                            hom' :=
                              Subtype.mk (p := fun (f : X.carrier → Z.carrier) ↦ UniformContinuous f)
                                ((↑h.hom' : Y.carrier → Z.carrier) ∘ (↑g.hom' : X.carrier → Y.carrier)) ⋯ :
                            X.Hom Z }.hom' :
                      X.carrier → Z.carrier) ∘
                    (↑f.hom' : W.carrier → X.carrier))
                  ⋯ :
              W.Hom Z }.hom' :
        W.carrier → Z.carrier)
      x

Tactic:
simp
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X : Type u
inst : UniformSpace X
⊢ { carrier := X, str := inst : UniformSpaceCat.{u} }.carrier = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X Y Z : UniformSpaceCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.hom (f ≫ g) =
    Subtype.mk (p := fun (f : X.carrier → Z.carrier) ↦ UniformContinuous f)
      (Function.comp (β := Y.carrier)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
              { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier) g) :
          (a : Y.carrier) → Z.carrier)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
              { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier) f) :
          (a : X.carrier) → Y.carrier))
      ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X : UniformSpaceCat
⊢ Hom.hom (𝟙 X) = Subtype.mk (p := fun (f : X.carrier → X.carrier) ↦ UniformContinuous f) id ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X Y : Type u
inst : UniformSpace X
inst_1 : UniformSpace Y
f : { f : X → Y // UniformContinuous f }
⊢ Hom.hom (ofHom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X Y Z : UniformSpaceCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := (a : X.carrier) → Z.carrier)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
          { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier) (f ≫ g)) :
      (a : X.carrier) → Z.carrier)
    (Function.comp (β := Y.carrier)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
            { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier) g) :
        (a : Y.carrier) → Z.carrier)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
            { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier) f) :
        (a : X.carrier) → Y.carrier))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X : UniformSpaceCat
⊢ Eq (α := (a : X.carrier) → X.carrier)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
          { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier) (𝟙 X)) :
      (a : X.carrier) → X.carrier)
    id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X Y : UniformSpaceCat
f : X.carrier → Y.carrier
hf : UniformContinuous f
⊢ (⇑{ hom' := Subtype.mk (p := fun (f : X.carrier → Y.carrier) ↦ UniformContinuous f) f hf : X.Hom Y }.hom :
      (a : X.carrier) → Y.carrier) =
    f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X Y : UniformSpaceCat
f g : X ⟶ Y
h :
  Eq (α := (a : X.carrier) → Y.carrier)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
          { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier) f) :
      (a : X.carrier) → Y.carrier)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
          { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier) g) :
      (a : X.carrier) → Y.carrier)
⊢ f = g

Tactic:
Hom.ext (Subtype.ext h)

Premises used: UniformSpaceCat.Hom.ext, Subtype.ext
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X : CpltSepUniformSpace
⊢ CompleteSpace.{u_1} X.toUniformSpace.carrier

Tactic:
CpltSepUniformSpace.isCompleteSpace X

Premises used: CpltSepUniformSpace.isCompleteSpace
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X : CpltSepUniformSpace
⊢ T0Space.{u_1} X.toUniformSpace.carrier

Tactic:
CpltSepUniformSpace.isT0 X

Premises used: CpltSepUniformSpace.isT0
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X : Type u
inst : UniformSpace X
inst_1 : CompleteSpace X
inst_2 : T0Space X
⊢ (of X).α = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X Y Z : CpltSepUniformSpace
f : X ⟶ Y
g : Y ⟶ Z
⊢ ConcreteCategory.hom (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦ { f : x1.α → x2.α // UniformContinuous f })
      (CC := α) (f ≫ g) =
    Subtype.mk (p := fun (f : X.α → Z.α) ↦ UniformContinuous f)
      (Function.comp (β := Y.α)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
              { f : x1.α → x2.α // UniformContinuous f }) (CC := α) g) :
          (a : Y.α) → Z.α)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
              { f : x1.α → x2.α // UniformContinuous f }) (CC := α) f) :
          (a : X.α) → Y.α))
      ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X : CpltSepUniformSpace
⊢ ConcreteCategory.hom (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦ { f : x1.α → x2.α // UniformContinuous f })
      (CC := α) (𝟙 X) =
    Subtype.mk (p := fun (f : X.α → X.α) ↦ UniformContinuous f) id ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X Y : Type u
inst : UniformSpace X
inst_1 : UniformSpace Y
f : { f : X → Y // UniformContinuous f }
⊢ UniformSpaceCat.Hom.hom (UniformSpaceCat.ofHom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
x : UniformSpaceCat
⊢ Eq (α :=
    (a : (CpltSepUniformSpace.of (Completion x.carrier)).toUniformSpace.carrier) →
      (CpltSepUniformSpace.of (Completion x.carrier)).toUniformSpace.carrier)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
          { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier) (X :=
          (CpltSepUniformSpace.of (Completion x.carrier)).toUniformSpace) (Y :=
          (CpltSepUniformSpace.of (Completion x.carrier)).toUniformSpace)
          (InducedCategory.Hom.hom
            (ConcreteCategory.ofHom (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
              { f : x1.α → x2.α // UniformContinuous f }) (CC := α)
              (Subtype.mk (p :=
                fun
                  (f :
                    (CpltSepUniformSpace.of (Completion x.carrier)).α →
                      (CpltSepUniformSpace.of (Completion x.carrier)).α) ↦
                UniformContinuous f) (Completion.map (⇑(Hom.hom' (𝟙 x)) : (a : x.carrier) → x.carrier)) ⋯)))) :
      (a : (CpltSepUniformSpace.of (Completion x.carrier)).toUniformSpace.carrier) →
        (CpltSepUniformSpace.of (Completion x.carrier)).toUniformSpace.carrier)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
          { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier)
          (InducedCategory.Hom.hom (𝟙 (CpltSepUniformSpace.of (Completion x.carrier))))) :
      (a : (CpltSepUniformSpace.of (Completion x.carrier)).toUniformSpace.carrier) →
        (CpltSepUniformSpace.of (Completion x.carrier)).toUniformSpace.carrier)

Tactic:
apply Completion.map_id

Premises used: UniformSpace.Completion.map_id
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X Y Z : UniformSpaceCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    (a : (CpltSepUniformSpace.of (Completion X.carrier)).toUniformSpace.carrier) →
      (CpltSepUniformSpace.of (Completion Z.carrier)).toUniformSpace.carrier)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
          { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier) (X :=
          (CpltSepUniformSpace.of (Completion X.carrier)).toUniformSpace) (Y :=
          (CpltSepUniformSpace.of (Completion Z.carrier)).toUniformSpace)
          (InducedCategory.Hom.hom
            (ConcreteCategory.ofHom (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
              { f : x1.α → x2.α // UniformContinuous f }) (CC := α)
              (Subtype.mk (p :=
                fun
                  (f :
                    (CpltSepUniformSpace.of (Completion X.carrier)).α →
                      (CpltSepUniformSpace.of (Completion Z.carrier)).α) ↦
                UniformContinuous f) (Completion.map (⇑(f ≫ g).hom' : (a : X.carrier) → Z.carrier)) ⋯)))) :
      (a : (CpltSepUniformSpace.of (Completion X.carrier)).toUniformSpace.carrier) →
        (CpltSepUniformSpace.of (Completion Z.carrier)).toUniformSpace.carrier)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
          { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier) (X :=
          (CpltSepUniformSpace.of (Completion X.carrier)).toUniformSpace) (Y :=
          (CpltSepUniformSpace.of (Completion Z.carrier)).toUniformSpace)
          (InducedCategory.Hom.hom
            (CategoryStruct.comp (Y := CpltSepUniformSpace.of (Completion Y.carrier))
              (ConcreteCategory.ofHom (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
                { f : x1.α → x2.α // UniformContinuous f }) (CC := α)
                (Subtype.mk (p :=
                  fun
                    (f :
                      (CpltSepUniformSpace.of (Completion X.carrier)).α →
                        (CpltSepUniformSpace.of (Completion Y.carrier)).α) ↦
                  UniformContinuous f) (Completion.map (⇑f.hom' : (a : X.carrier) → Y.carrier)) ⋯))
              (ConcreteCategory.ofHom (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
                { f : x1.α → x2.α // UniformContinuous f }) (CC := α)
                (Subtype.mk (p :=
                  fun
                    (f :
                      (CpltSepUniformSpace.of (Completion Y.carrier)).α →
                        (CpltSepUniformSpace.of (Completion Z.carrier)).α) ↦
                  UniformContinuous f) (Completion.map (⇑g.hom' : (a : Y.carrier) → Z.carrier)) ⋯))))) :
      (a : (CpltSepUniformSpace.of (Completion X.carrier)).toUniformSpace.carrier) →
        (CpltSepUniformSpace.of (Completion Z.carrier)).toUniformSpace.carrier)

Tactic:
(Completion.map_comp g.hom.property f.hom.property).symm

Premises used: UniformSpace.Completion.map, UniformSpaceCat.Hom.hom, UniformSpace.Completion.map_comp, Quotient, SeparationQuotient, AbstractCompletion.map, Eq.symm, AbstractCompletion.extend, UniformSpace.Completion, Subtype.property, ite
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X Y Z : UniformSpaceCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    (a : (CpltSepUniformSpace.of (Completion X.carrier)).toUniformSpace.carrier) →
      (CpltSepUniformSpace.of (Completion Z.carrier)).toUniformSpace.carrier)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
          { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier) (X :=
          (CpltSepUniformSpace.of (Completion X.carrier)).toUniformSpace) (Y :=
          (CpltSepUniformSpace.of (Completion Z.carrier)).toUniformSpace)
          (InducedCategory.Hom.hom
            (ConcreteCategory.ofHom (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
              { f : x1.α → x2.α // UniformContinuous f }) (CC := α)
              (Subtype.mk (p :=
                fun
                  (f :
                    (CpltSepUniformSpace.of (Completion X.carrier)).α →
                      (CpltSepUniformSpace.of (Completion Z.carrier)).α) ↦
                UniformContinuous f) (Completion.map (⇑(f ≫ g).hom' : (a : X.carrier) → Z.carrier)) ⋯)))) :
      (a : (CpltSepUniformSpace.of (Completion X.carrier)).toUniformSpace.carrier) →
        (CpltSepUniformSpace.of (Completion Z.carrier)).toUniformSpace.carrier)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
          { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier) (X :=
          (CpltSepUniformSpace.of (Completion X.carrier)).toUniformSpace) (Y :=
          (CpltSepUniformSpace.of (Completion Z.carrier)).toUniformSpace)
          (InducedCategory.Hom.hom
            (CategoryStruct.comp (Y := CpltSepUniformSpace.of (Completion Y.carrier))
              (ConcreteCategory.ofHom (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
                { f : x1.α → x2.α // UniformContinuous f }) (CC := α)
                (Subtype.mk (p :=
                  fun
                    (f :
                      (CpltSepUniformSpace.of (Completion X.carrier)).α →
                        (CpltSepUniformSpace.of (Completion Y.carrier)).α) ↦
                  UniformContinuous f) (Completion.map (⇑f.hom' : (a : X.carrier) → Y.carrier)) ⋯))
              (ConcreteCategory.ofHom (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
                { f : x1.α → x2.α // UniformContinuous f }) (CC := α)
                (Subtype.mk (p :=
                  fun
                    (f :
                      (CpltSepUniformSpace.of (Completion Y.carrier)).α →
                        (CpltSepUniformSpace.of (Completion Z.carrier)).α) ↦
                  UniformContinuous f) (Completion.map (⇑g.hom' : (a : Y.carrier) → Z.carrier)) ⋯))))) :
      (a : (CpltSepUniformSpace.of (Completion X.carrier)).toUniformSpace.carrier) →
        (CpltSepUniformSpace.of (Completion Z.carrier)).toUniformSpace.carrier)

Tactic:
exact (Completion.map_comp g.hom.property f.hom.property).symm

Premises used: UniformSpaceCat.Hom.hom, UniformSpace.Completion.map_comp, Eq.symm, Subtype.property