awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X : CondensedSet
S : CompHaus
x : X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)
⊢ Continuous X.coinducingCoprod

Tactic:
apply continuous_coinduced_rng

Premises used: continuous_coinduced_rng
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X Y : CondensedSet
f : X ⟶ Y
rw :
  Continuous (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1})))
    ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op (of PUnit.{u + 1})))) :
        (a : (fun (X : Type (u + 1)) ↦ X) (X.obj.obj (Opposite.op (of PUnit.{u + 1})))) →
          (fun (X : Type (u + 1)) ↦ X) (Y.obj.obj (Opposite.op (of PUnit.{u + 1})))) ∘
      X.coinducingCoprod)
⊢ Continuous (X := X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1}))) (Y :=
    Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1})))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op (of PUnit.{u + 1})))) :
      (a : (fun (X : Type (u + 1)) ↦ X) (X.obj.obj (Opposite.op (of PUnit.{u + 1})))) →
        (fun (X : Type (u + 1)) ↦ X) (Y.obj.obj (Opposite.op (of PUnit.{u + 1}))))

Tactic:
rw [continuous_coinduced_dom]

Premises used: continuous_coinduced_dom
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X Y : CondensedSet
f : X ⟶ Y
hf :
  ∀ (i : (S : CompHaus.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)),
    Continuous (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1})))
      fun
        (a :
          (↑(i.fst (β := fun (S : CompHaus.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u)) ↦
      ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op (of PUnit.{u + 1})))) :
            (a : (fun (X : Type (u + 1)) ↦ X) (X.obj.obj (Opposite.op (of PUnit.{u + 1})))) →
              (fun (X : Type (u + 1)) ↦ X) (Y.obj.obj (Opposite.op (of PUnit.{u + 1})))) ∘
          X.coinducingCoprod)
        (Sigma.mk (β :=
          fun (i : (S : CompHaus.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)) ↦
          (↑(i.fst (β := fun (S : CompHaus.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u))
          i a)
⊢ Continuous (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1})))
    ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op (of PUnit.{u + 1})))) :
        (a : (fun (X : Type (u + 1)) ↦ X) (X.obj.obj (Opposite.op (of PUnit.{u + 1})))) →
          (fun (X : Type (u + 1)) ↦ X) (Y.obj.obj (Opposite.op (of PUnit.{u + 1})))) ∘
      X.coinducingCoprod)

Tactic:
apply continuous_sigma

Premises used: continuous_sigma
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X Y : CondensedSet
f : X ⟶ Y
S : CompHaus
x : X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)
hf :
  Continuous (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1})))
    fun (a : (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op (of PUnit.{u + 1}))) :
        (a : X.obj.obj (Opposite.op (of PUnit.{u + 1}))) → Y.obj.obj (Opposite.op (of PUnit.{u + 1})))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map
              (CompHausLike.const (P := fun (x : TopCat.{u}) ↦ True) (of PUnit.{u + 1}) a).op) :
          (a : X.obj.obj (Opposite.op S)) → X.obj.obj (Opposite.op (of PUnit.{u + 1})))
        x)
⊢ Continuous (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1})))
    fun
      (a :
        (↑((Sigma.fst (β := fun (S : CompHaus.{u}) ↦
                  X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S))
                  (Sigma.mk (β := fun (S : CompHaus.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)) S x)).toTop
              (P := fun (x : TopCat.{u}) ↦ True)) :
          Type u)) ↦
    ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op (of PUnit.{u + 1})))) :
          (a : (fun (X : Type (u + 1)) ↦ X) (X.obj.obj (Opposite.op (of PUnit.{u + 1})))) →
            (fun (X : Type (u + 1)) ↦ X) (Y.obj.obj (Opposite.op (of PUnit.{u + 1})))) ∘
        X.coinducingCoprod)
      (Sigma.mk (β :=
        fun (i : (S : CompHaus.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)) ↦
        (↑(i.fst (β := fun (S : CompHaus.{u}) ↦
                  X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)).toTop
              (P := fun (x : TopCat.{u}) ↦ True)) :
          Type u))
        (Sigma.mk (β := fun (S : CompHaus.{u}) ↦
          X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)) S x)
        a)

Tactic:
simp only [Function.comp_apply, coinducingCoprod]

Premises used: Function.comp_apply, _private.0.CondensedSet.coinducingCoprod
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X Y : CondensedSet
f : X ⟶ Y
S : CompHaus
x : X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)
hf :
  Continuous (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1})))
    fun (a : (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map
            (CompHausLike.const (P := fun (x : TopCat.{u}) ↦ True) (of PUnit.{u + 1}) a).op) :
        (a : Y.obj.obj (Opposite.op S)) → Y.obj.obj (Opposite.op (of PUnit.{u + 1})))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op S)) :
          (a : X.obj.obj (Opposite.op S)) → Y.obj.obj (Opposite.op S))
        x)
⊢ Continuous (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1})))
    fun (a : (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op (of PUnit.{u + 1}))) :
        (a : X.obj.obj (Opposite.op (of PUnit.{u + 1}))) → Y.obj.obj (Opposite.op (of PUnit.{u + 1})))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map
              (CompHausLike.const (P := fun (x : TopCat.{u}) ↦ True) (of PUnit.{u + 1}) a).op) :
          (a : X.obj.obj (Opposite.op S)) → X.obj.obj (Opposite.op (of PUnit.{u + 1})))
        x)

Tactic:
rw [show (fun (a : S) ↦
          f.hom.app ⟨of PUnit⟩ (X.obj.map ((of PUnit.{u + 1}).const a).op x)) = _
        from funext fun a ↦ NatTrans.naturality_apply f.hom ((of PUnit.{u + 1}).const a).op x]
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X Y : CondensedSet
f : X ⟶ Y
S : CompHaus
x : X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)
⊢ Continuous (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1})))
    fun (a : (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map
            (CompHausLike.const (P := fun (x : TopCat.{u}) ↦ True) (of PUnit.{u + 1}) a).op) :
        (a : Y.obj.obj (Opposite.op S)) → Y.obj.obj (Opposite.op (of PUnit.{u + 1})))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op S)) :
          (a : X.obj.obj (Opposite.op S)) → Y.obj.obj (Opposite.op S))
        x)

Tactic:
continuous_coinducingCoprod Y _

Premises used: CondensedSet.continuous_coinducingCoprod, _private.0.CondensedSet.coinducingCoprod
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X Y : CondensedSet
f : X ⟶ Y
S : CompHaus
x : X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)
⊢ Continuous (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1})))
    fun (a : (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map
            (CompHausLike.const (P := fun (x : TopCat.{u}) ↦ True) (of PUnit.{u + 1}) a).op) :
        (a : Y.obj.obj (Opposite.op S)) → Y.obj.obj (Opposite.op (of PUnit.{u + 1})))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op S)) :
          (a : X.obj.obj (Opposite.op S)) → Y.obj.obj (Opposite.op S))
        x)

Tactic:
exact continuous_coinducingCoprod Y _

Premises used: CondensedSet.continuous_coinducingCoprod
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X_1 : CondensedSet
X : TopCat
rw :
  Continuous.{u + 1, u + 1} (X :=
    (i :
      (S : CompHaus.{u}) ×
        X.toCondensedSet.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)) ×
      (↑(i.fst (β := fun (S : CompHaus.{u}) ↦
                X.toCondensedSet.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)).toTop
            (P := fun (x : TopCat.{u}) ↦ True)) :
        Type u))
    (Y := (↑X : Type (u + 1)))
    ((fun
          (x :
            X.toCondensedSet.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj
              (Opposite.op (of PUnit.{u + 1}))) ↦
        x.toFun PUnit.unit) ∘
      X.toCondensedSet.coinducingCoprod)
⊢ Continuous (Y := (↑X : Type (u + 1)))
    fun
      (x :
        X.toCondensedSet.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1}))) ↦
    x.toFun PUnit.unit

Tactic:
rw [continuous_coinduced_dom]

Premises used: continuous_coinduced_dom
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X_1 : CondensedSet
X : TopCat
⊢ Continuous.{u + 1, u + 1} (X :=
    (i :
      (S : CompHaus.{u}) ×
        X.toCondensedSet.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)) ×
      (↑(i.fst (β := fun (S : CompHaus.{u}) ↦
                X.toCondensedSet.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)).toTop
            (P := fun (x : TopCat.{u}) ↦ True)) :
        Type u))
    (Y := (↑X : Type (u + 1)))
    ((fun
          (x :
            X.toCondensedSet.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj
              (Opposite.op (of PUnit.{u + 1}))) ↦
        x.toFun PUnit.unit) ∘
      X.toCondensedSet.coinducingCoprod)

Tactic:
continuity
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X : TopCat
x : C(PUnit.{u_1 + 1}, (↑X : Type (u_1 + 1)))
⊢ Eq (α := (↑X : Type (u_1 + 1)))
    ((TopCat.Hom.hom (topCatAdjunctionCounit X) :
          (a : C(PUnit.{u_1 + 1}, (↑X : Type (u_1 + 1)))) → (↑X : Type (u_1 + 1)))
        x :
      (↑X : Type (u_1 + 1)))
    ((x : (a : PUnit.{u_1 + 1}) → (↑X : Type (u_1 + 1))) PUnit.unit : (↑X : Type (u_1 + 1)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X : TopCat
⊢ Function.Bijective (α := (↑X.toCondensedSet.toTopCat : Type (u + 1))) (β := (↑X : Type (u + 1)))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u + 1}) ↦ C((↑X : Type (u + 1)), (↑Y : Type (u + 1)))) (CC :=
          TopCat.carrier) (topCatAdjunctionCounit X)) :
      (a : (↑X.toCondensedSet.toTopCat : Type (u + 1))) → (↑X : Type (u + 1)))

Tactic:
(topCatAdjunctionCounitEquiv X).bijective

Premises used: Equiv.bijective, CondensedSet.topCatAdjunctionCounitEquiv
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X_1 X : CondensedSet
S : CompHausᵒᵖ
x : X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj S
suffices :
  ∀ (i : (T : CompHaus.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op T)),
    Continuous (Y := X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1})))
      fun
        (a :
          (↑(i.fst (β := fun (T : CompHaus.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op T)).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u)) ↦
      X.coinducingCoprod
        (Sigma.mk (β :=
          fun (i : (S : CompHaus.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)) ↦
          (↑(i.fst (β := fun (S : CompHaus.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u))
          i a)
⊢ Continuous (Y := (↑X.toTopCat : Type (u + 1)))
    fun (s : (↑(Functor.obj (CompHausLike.compHausLikeToTop fun (x : TopCat.{u}) ↦ True) (Opposite.unop S)) : Type u)) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map
            (CompHausLike.const (P := fun (x : TopCat.{u}) ↦ True) (of PUnit.{u + 1}) s).op) :
        (a : (fun (X : Type (u + 1)) ↦ X) (X.obj.obj (Opposite.op (Opposite.unop S)))) →
          (fun (X : Type (u + 1)) ↦ X) (X.obj.obj (Opposite.op (of PUnit.{u + 1}))))
      x

Tactic:
suffices ∀ (i : (T : CompHaus.{u}) × X.obj.obj ⟨T⟩),
          Continuous (fun (a : i.fst) ↦ X.coinducingCoprod ⟨i, a⟩) from this ⟨_, _⟩
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X_1 X : CondensedSet
S : CompHausᵒᵖ
x : X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj S
rw : Continuous X.coinducingCoprod
⊢ ∀ (i : (T : CompHaus.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op T)),
    Continuous (Y := X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1})))
      fun
        (a :
          (↑(i.fst (β := fun (T : CompHaus.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op T)).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u)) ↦
      X.coinducingCoprod
        (Sigma.mk (β :=
          fun (i : (S : CompHaus.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)) ↦
          (↑(i.fst (β := fun (S : CompHaus.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u))
          i a)

Tactic:
rw [← continuous_sigma_iff]

Premises used: continuous_sigma_iff
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X_1 X : CondensedSet
S : CompHausᵒᵖ
x : X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj S
⊢ Continuous X.coinducingCoprod

Tactic:
apply continuous_coinduced_rng

Premises used: continuous_coinduced_rng
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X_1 X : CondensedSet
x x_1 : CompHausᵒᵖ
x_2 : x ⟶ x_1
x_3 : X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj x
⊢ {
      toFun :=
        fun
          (s :
            (↑(Functor.obj (CompHausLike.compHausLikeToTop fun (x : TopCat.{u}) ↦ True) (Opposite.unop x_1)) :
              Type u)) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map
                (x_2 ≫ (CompHausLike.const (P := fun (x : TopCat.{u}) ↦ True) (of PUnit.{u + 1}) s).op)) :
            (a : X.obj.obj x) → X.obj.obj (Opposite.op (of PUnit.{u + 1})))
          x_3,
      continuous_toFun := ⋯ :
      C((↑(Functor.obj (CompHausLike.compHausLikeToTop fun (x : TopCat.{u}) ↦ True) (Opposite.unop x_1)) : Type u),
        X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1}))) } =
    {
          toFun :=
            fun
              (s :
                (↑(Functor.obj (CompHausLike.compHausLikeToTop fun (x : TopCat.{u}) ↦ True) (Opposite.unop x)) :
                  Type u)) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map
                    (CompHausLike.const (P := fun (x : TopCat.{u}) ↦ True) (of PUnit.{u + 1}) s).op) :
                (a : X.obj.obj (Opposite.op (Opposite.unop x))) → X.obj.obj (Opposite.op (of PUnit.{u + 1})))
              x_3,
          continuous_toFun := ⋯ :
          C((↑(Functor.obj (CompHausLike.compHausLikeToTop fun (x : TopCat.{u}) ↦ True) (Opposite.unop x)) : Type u),
            X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1}))) }.comp
      (TopCat.Hom.hom x_2.unop.hom)

Tactic:
rfl
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X Y : CondensedSet
w :
  ∀ (x : (↑(condensedSetToTopCat.obj Y) : Type (u + 1))),
    Eq (α := (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))
      (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u + 1}) ↦ C((↑X : Type (u + 1)), (↑Y : Type (u + 1)))) (CC :=
                TopCat.carrier) (X := condensedSetToTopCat.obj Y) (Y := condensedSetToTopCat.obj Y)
                (CategoryStruct.comp (Y :=
                    condensedSetToTopCat.obj (topCatToCondensedSet.obj (condensedSetToTopCat.obj Y)))
                    (condensedSetToTopCat.map
                      (NatTrans.app { app := topCatAdjunctionUnit, naturality := topCatAdjunction._proof_2 } Y))
                    (NatTrans.app { app := topCatAdjunctionCounit, naturality := topCatAdjunction._proof_3 }
                      (condensedSetToTopCat.obj Y)) :
                  condensedSetToTopCat.obj Y ⟶ condensedSetToTopCat.obj Y) :
              C((↑(condensedSetToTopCat.obj Y) : Type (u + 1)), (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))) :
            (a : (↑(condensedSetToTopCat.obj Y) : Type (u + 1))) → (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))
          x :
        (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u + 1}) ↦ C((↑X : Type (u + 1)), (↑Y : Type (u + 1)))) (CC :=
              TopCat.carrier) (𝟙 (condensedSetToTopCat.obj Y)) :
            (a : (↑(condensedSetToTopCat.obj Y) : Type (u + 1))) → (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))
          x :
        (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))
⊢ Eq (α := condensedSetToTopCat.obj Y ⟶ condensedSetToTopCat.obj Y)
    (CategoryStruct.comp (Y := condensedSetToTopCat.obj (topCatToCondensedSet.obj (condensedSetToTopCat.obj Y)))
        (condensedSetToTopCat.map
          (NatTrans.app { app := topCatAdjunctionUnit, naturality := topCatAdjunction._proof_2 } Y))
        (NatTrans.app { app := topCatAdjunctionCounit, naturality := topCatAdjunction._proof_3 }
          (condensedSetToTopCat.obj Y)) :
      condensedSetToTopCat.obj Y ⟶ condensedSetToTopCat.obj Y)
    (𝟙 (condensedSetToTopCat.obj Y) : condensedSetToTopCat.obj Y ⟶ condensedSetToTopCat.obj Y)

Tactic:
ext
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X Y : CondensedSet
x : (↑(condensedSetToTopCat.obj Y) : Type (u + 1))
w :
  Eq (α :=
    (fun (X : Type (u + 1)) ↦ X)
      (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj
        (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1}))))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map
              (𝟙 (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1})))))) :
          (a :
              (fun (X : Type (u + 1)) ↦ X) (Y.obj.obj (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1})))))) →
            (fun (X : Type (u + 1)) ↦ X) (Y.obj.obj (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1}))))))
        x :
      (fun (X : Type (u + 1)) ↦ X)
        (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj
          (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1}))))))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u + 1}) ↦ C((↑X : Type (u + 1)), (↑Y : Type (u + 1)))) (CC :=
            TopCat.carrier) (𝟙 (condensedSetToTopCat.obj Y)) :
          (a : (↑(condensedSetToTopCat.obj Y) : Type (u + 1))) → (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))
        x :
      (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))
⊢ Eq (α := (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))
    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u + 1}) ↦ C((↑X : Type (u + 1)), (↑Y : Type (u + 1)))) (CC :=
              TopCat.carrier) (X := condensedSetToTopCat.obj Y) (Y := condensedSetToTopCat.obj Y)
              (CategoryStruct.comp (Y :=
                  condensedSetToTopCat.obj (topCatToCondensedSet.obj (condensedSetToTopCat.obj Y)))
                  (condensedSetToTopCat.map
                    (NatTrans.app { app := topCatAdjunctionUnit, naturality := topCatAdjunction._proof_2 } Y))
                  (NatTrans.app { app := topCatAdjunctionCounit, naturality := topCatAdjunction._proof_3 }
                    (condensedSetToTopCat.obj Y)) :
                condensedSetToTopCat.obj Y ⟶ condensedSetToTopCat.obj Y) :
            C((↑(condensedSetToTopCat.obj Y) : Type (u + 1)), (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))) :
          (a : (↑(condensedSetToTopCat.obj Y) : Type (u + 1))) → (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))
        x :
      (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u + 1}) ↦ C((↑X : Type (u + 1)), (↑Y : Type (u + 1)))) (CC :=
            TopCat.carrier) (𝟙 (condensedSetToTopCat.obj Y)) :
          (a : (↑(condensedSetToTopCat.obj Y) : Type (u + 1))) → (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))
        x :
      (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))

Tactic:
change Y.obj.map (𝟙 _) _ = _

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.CategoryStruct.id, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map, DFunLike.coe
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X Y : CondensedSet
x : (↑(condensedSetToTopCat.obj Y) : Type (u + 1))
⊢ Eq (α :=
    (fun (X : Type (u + 1)) ↦ X)
      (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj
        (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1}))))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map
              (𝟙 (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1})))))) :
          (a :
              (fun (X : Type (u + 1)) ↦ X) (Y.obj.obj (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1})))))) →
            (fun (X : Type (u + 1)) ↦ X) (Y.obj.obj (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1}))))))
        x :
      (fun (X : Type (u + 1)) ↦ X)
        (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj
          (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1}))))))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u + 1}) ↦ C((↑X : Type (u + 1)), (↑Y : Type (u + 1)))) (CC :=
            TopCat.carrier) (𝟙 (condensedSetToTopCat.obj Y)) :
          (a : (↑(condensedSetToTopCat.obj Y) : Type (u + 1))) → (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))
        x :
      (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))

Tactic:
simp
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X_1 : CondensedSet
X : TopCat
rw :
  Function.Surjective (α := (↑((topCatToCondensedSet ⋙ condensedSetToTopCat).obj X) : Type (u_1 + 1))) (β :=
    (↑(Functor.obj (𝟭 TopCat) X) : Type (u_1 + 1)))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1 + 1}) ↦ C((↑X : Type (u_1 + 1)), (↑Y : Type (u_1 + 1))))
          (CC := TopCat.carrier) (topCatAdjunction.counit.app X)) :
      (a : (↑((topCatToCondensedSet ⋙ condensedSetToTopCat).obj X) : Type (u_1 + 1))) →
        (↑((𝟭 TopCat).obj X) : Type (u_1 + 1)))
⊢ Epi (topCatAdjunction.counit.app X)

Tactic:
rw [TopCat.epi_iff_surjective]

Premises used: TopCat.epi_iff_surjective