awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Condensed.Light.TopCatAdjunction (goal)
Goal:
X Y : LightCondSet
f : X ⟶ Y
S : LightProfinite
x : X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)
⊢ Continuous (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))
    fun
      (a :
        (↑(S.toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
          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 LightProfinite)).map
                (CompHausLike.const (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                    (of PUnit.{u + 1}) a).op) :
            (a : X.obj.obj (Opposite.op S)) → X.obj.obj (Opposite.op (of PUnit.{u + 1})))
          x :
        X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))
have hf : Continuous (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))
  fun
    (a :
      (↑(S.toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
        Type u)) ↦
  (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map
          (CompHausLike.const (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) (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 :
      Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S))
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]
-- Lean 4 proof step from Mathlib.Condensed.Light.TopCatAdjunction (goal)
Goal:
X_1 Y : LightCondSet
f : X_1 ⟶ Y
X : TopCat
⊢ Continuous (Y := (↑X : Type u))
    fun
      (x :
        X.toLightCondSet.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
          (Opposite.op (of PUnit.{u + 1}))) ↦
    x.toFun PUnit.unit
have rw : Continuous.{u + 1, u} (X :=
  (i :
    (S : LightProfinite.{u}) ×
      X.toLightCondSet.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) ×
    (↑(i.fst (β := fun (S : LightProfinite.{u}) ↦
              X.toLightCondSet.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)).toTop
          (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u))
  (Y := (↑X : Type u))
  ((fun
        (x :
          X.toLightCondSet.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
            (Opposite.op (of PUnit.{u + 1}))) ↦
      x.toFun PUnit.unit) ∘
    X.toLightCondSet.coinducingCoprod)
Tactic: rw [continuous_coinduced_dom]
-- Lean 4 proof step from Mathlib.Condensed.Light.TopCatAdjunction (goal)
Goal:
X_1 Y : LightCondSet
f : X_1 ⟶ Y
X : LightCondSet
S : LightProfiniteᵒᵖ
x : X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj S
⊢ Continuous (Y := (↑X.toTopCat : Type u))
    fun
      (s :
        (↑(Functor.obj
              (CompHausLike.compHausLikeToTop fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
              (Opposite.unop S)) :
          Type u)) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map
            (CompHausLike.const (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                (of PUnit.{u + 1}) s).op) :
        (a : (fun (X : Type u) ↦ X) (X.obj.obj (Opposite.op (Opposite.unop S)))) →
          (fun (X : Type u) ↦ X) (X.obj.obj (Opposite.op (of PUnit.{u + 1}))))
      x
have suffices : ∀ (i : (T : LightProfinite.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op T)),
  Continuous (Y := X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))
    fun
      (a :
        (↑(i.fst (β := fun (T : LightProfinite.{u}) ↦
                  X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op T)).toTop
              (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
          Type u)) ↦
    X.coinducingCoprod
      (Sigma.mk (β :=
        fun
          (i :
            (S : LightProfinite.{u}) ×
              X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) ↦
        (↑(i.fst (β := fun (S : LightProfinite.{u}) ↦
                  X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)).toTop
              (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
          Type u))
        i a)
Tactic: suffices ∀ (i : (T : LightProfinite.{u}) × X.obj.obj ⟨T⟩),
          Continuous (fun (a : i.fst) ↦ X.coinducingCoprod ⟨i, a⟩) from this ⟨_, _⟩
-- Lean 4 proof step from Mathlib.Condensed.Light.TopCatAdjunction (goal)
Goal:
X_1 Y : LightCondSet
f : X_1 ⟶ Y
X : LightCondSet
S : LightProfiniteᵒᵖ
x : X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj S
⊢ ∀
    (i :
      (T : LightProfinite.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op T)),
    Continuous (Y :=
      X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))
      fun
        (a :
          (↑(i.fst (β := fun (T : LightProfinite.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op T)).toTop
                (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u)) ↦
      X.coinducingCoprod
        (Sigma.mk (β :=
          fun
            (i :
              (S : LightProfinite.{u}) ×
                X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) ↦
          (↑(i.fst (β := fun (S : LightProfinite.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)).toTop
                (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
          i a)
have rw : Continuous X.coinducingCoprod
Tactic: rw [← continuous_sigma_iff]
-- Lean 4 proof step from Mathlib.Condensed.Light.TopCatAdjunction (goal)
Goal:
X Y_1 : LightCondSet
f : X ⟶ Y_1
Y : LightCondSet
⊢ Eq (α := lightCondSetToTopCat.obj Y ⟶ lightCondSetToTopCat.obj Y)
    (CategoryStruct.comp (Y := lightCondSetToTopCat.obj (topCatToLightCondSet.obj (lightCondSetToTopCat.obj Y)))
        (lightCondSetToTopCat.map
          (NatTrans.app { app := topCatAdjunctionUnit, naturality := topCatAdjunction._proof_2 } Y))
        (NatTrans.app { app := topCatAdjunctionCounit, naturality := topCatAdjunction._proof_3 }
          (lightCondSetToTopCat.obj Y)) :
      lightCondSetToTopCat.obj Y ⟶ lightCondSetToTopCat.obj Y)
    (𝟙 (lightCondSetToTopCat.obj Y) : lightCondSetToTopCat.obj Y ⟶ lightCondSetToTopCat.obj Y)
have w : ∀ (x : (↑(lightCondSetToTopCat.obj Y) : Type u)),
  Eq (α := (↑(lightCondSetToTopCat.obj Y) : Type u))
    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (X := lightCondSetToTopCat.obj Y) (Y := lightCondSetToTopCat.obj Y)
              (CategoryStruct.comp (Y :=
                  lightCondSetToTopCat.obj (topCatToLightCondSet.obj (lightCondSetToTopCat.obj Y)))
                  (lightCondSetToTopCat.map
                    (NatTrans.app { app := topCatAdjunctionUnit, naturality := topCatAdjunction._proof_2 } Y))
                  (NatTrans.app { app := topCatAdjunctionCounit, naturality := topCatAdjunction._proof_3 }
                    (lightCondSetToTopCat.obj Y)) :
                lightCondSetToTopCat.obj Y ⟶ lightCondSetToTopCat.obj Y) :
            C((↑(lightCondSetToTopCat.obj Y) : Type u), (↑(lightCondSetToTopCat.obj Y) : Type u))) :
          (a : (↑(lightCondSetToTopCat.obj Y) : Type u)) → (↑(lightCondSetToTopCat.obj Y) : Type u))
        x :
      (↑(lightCondSetToTopCat.obj Y) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (𝟙 (lightCondSetToTopCat.obj Y)) :
          (a : (↑(lightCondSetToTopCat.obj Y) : Type u)) → (↑(lightCondSetToTopCat.obj Y) : Type u))
        x :
      (↑(lightCondSetToTopCat.obj Y) : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Condensed.Light.TopCatAdjunction (goal)
Goal:
X Y_1 : LightCondSet
f : X ⟶ Y_1
Y : LightCondSet
x : (↑(lightCondSetToTopCat.obj Y) : Type u)
⊢ Eq (α := (↑(lightCondSetToTopCat.obj Y) : Type u))
    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (X := lightCondSetToTopCat.obj Y) (Y := lightCondSetToTopCat.obj Y)
              (CategoryStruct.comp (Y :=
                  lightCondSetToTopCat.obj (topCatToLightCondSet.obj (lightCondSetToTopCat.obj Y)))
                  (lightCondSetToTopCat.map
                    (NatTrans.app { app := topCatAdjunctionUnit, naturality := topCatAdjunction._proof_2 } Y))
                  (NatTrans.app { app := topCatAdjunctionCounit, naturality := topCatAdjunction._proof_3 }
                    (lightCondSetToTopCat.obj Y)) :
                lightCondSetToTopCat.obj Y ⟶ lightCondSetToTopCat.obj Y) :
            C((↑(lightCondSetToTopCat.obj Y) : Type u), (↑(lightCondSetToTopCat.obj Y) : Type u))) :
          (a : (↑(lightCondSetToTopCat.obj Y) : Type u)) → (↑(lightCondSetToTopCat.obj Y) : Type u))
        x :
      (↑(lightCondSetToTopCat.obj Y) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (𝟙 (lightCondSetToTopCat.obj Y)) :
          (a : (↑(lightCondSetToTopCat.obj Y) : Type u)) → (↑(lightCondSetToTopCat.obj Y) : Type u))
        x :
      (↑(lightCondSetToTopCat.obj Y) : Type u))
have w : Eq (α :=
  (fun (X : Type u) ↦ X)
    (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
      (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1}))))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map
            (𝟙 (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1})))))) :
        (a : (fun (X : Type u) ↦ X) (Y.obj.obj (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1})))))) →
          (fun (X : Type u) ↦ X) (Y.obj.obj (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1}))))))
      x :
    (fun (X : Type u) ↦ X)
      (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
        (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1}))))))
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (𝟙 (lightCondSetToTopCat.obj Y)) :
        (a : (↑(lightCondSetToTopCat.obj Y) : Type u)) → (↑(lightCondSetToTopCat.obj Y) : Type u))
      x :
    (↑(lightCondSetToTopCat.obj Y) : Type u))
Tactic: change Y.obj.map (𝟙 _) _ = _
-- Lean 4 proof step from Mathlib.Condensed.Light.TopCatAdjunction (goal)
Goal:
X_1 Y : LightCondSet
f : X_1 ⟶ Y
X : TopCat
⊢ Epi (topCatAdjunction.counit.app X)
have rw : Function.Surjective (α := (↑((topCatToLightCondSet ⋙ lightCondSetToTopCat).obj X) : Type u_1)) (β :=
  (↑(Functor.obj (𝟭 TopCat) 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)
        (topCatAdjunction.counit.app X)) :
    (a : (↑((topCatToLightCondSet ⋙ lightCondSetToTopCat).obj X) : Type u_1)) → (↑((𝟭 TopCat).obj X) : Type u_1))
Tactic: rw [TopCat.epi_iff_surjective]
-- Lean 4 proof step from Mathlib.Condensed.Light.TopCatAdjunction (goal)
Goal:
X_1 Y : LightCondSet
f : X_1 ⟶ Y
X : TopCat
inst : SequentialSpace (↑X : Type)
⊢ Continuous (topCatAdjunctionCounitEquiv X).invFun
have hf : SeqContinuous (topCatAdjunctionCounitEquiv X).invFun
Tactic: apply SeqContinuous.continuous
-- Lean 4 proof step from Mathlib.Condensed.Light.TopCatAdjunction (goal)
Goal:
X_1 Y : LightCondSet
f_1 : X_1 ⟶ Y
X : TopCat
inst : SequentialSpace (↑X : Type)
f : ℕ → (↑X : Type)
p : (↑X : Type)
h : Filter.Tendsto f Filter.atTop (nhds p)
g : OnePoint ℕ → (↑X.toLightCondSet.toTopCat : Type) :=
  (topCatAdjunctionCounitEquiv X).invFun ∘ (⇑(OnePoint.continuousMapMkNat f p h) : (a : OnePoint ℕ) → (↑X : Type))
⊢ Filter.Tendsto ((topCatAdjunctionCounitEquiv X).invFun ∘ f) Filter.atTop
    (nhds ((topCatAdjunctionCounitEquiv X).invFun p))
have hf : Filter.Tendsto (fun (n : ℕ) ↦ g (↑n : OnePoint ℕ)) Filter.atTop (nhds ((topCatAdjunctionCounitEquiv X).invFun p))
Tactic: change Filter.Tendsto (fun n : ℕ ↦ g n) _ _
-- Lean 4 proof step from Mathlib.Condensed.Light.TopCatAdjunction (goal)
Goal:
X_1 Y : LightCondSet
f_1 : X_1 ⟶ Y
X : TopCat
inst : SequentialSpace (↑X : Type)
f : ℕ → (↑X : Type)
p : (↑X : Type)
h : Filter.Tendsto f Filter.atTop (nhds p)
g : OnePoint ℕ → (↑X.toLightCondSet.toTopCat : Type) :=
  (topCatAdjunctionCounitEquiv X).invFun ∘ (⇑(OnePoint.continuousMapMkNat f p h) : (a : OnePoint ℕ) → (↑X : Type))
⊢ Filter.Tendsto (fun (n : ℕ) ↦ g (↑n : OnePoint ℕ)) Filter.atTop (nhds ((topCatAdjunctionCounitEquiv X).invFun p))
have hf : Continuous g
Tactic: erw [← OnePoint.continuous_iff_from_nat]
-- Lean 4 proof step from Mathlib.Condensed.Light.TopCatAdjunction (goal)
Goal:
X Y : LightCondSet
f : X ⟶ Y
⊢ IsIso sequentialAdjunction.counit
have rw : ∀ (X : Sequential.{0}), IsIso (sequentialAdjunction.counit.app X)
Tactic: rw [NatTrans.isIso_iff_isIso_app]
-- Lean 4 proof step from Mathlib.Condensed.TopCatAdjunction (goal)
Goal:
X : CondensedSet
S : CompHaus
x : X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)
⊢ Continuous (Y := X.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)) ↦
    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)
have 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)
Tactic: suffices ∀ (i : (T : CompHaus.{u}) × X.obj.obj ⟨T⟩),
      Continuous (fun (a : i.fst) ↦ X.coinducingCoprod ⟨i, a⟩) from this ⟨_, _⟩
-- Lean 4 proof step from Mathlib.Condensed.TopCatAdjunction (goal)
Goal:
X : CondensedSet
S : CompHaus
x : X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)
⊢ ∀ (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)
have rw : Continuous X.coinducingCoprod
Tactic: rw [← continuous_sigma_iff]
-- Lean 4 proof step from Mathlib.Condensed.TopCatAdjunction (goal)
Goal:
X Y : CondensedSet
f : X ⟶ Y
⊢ 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}))))
have 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)
Tactic: rw [continuous_coinduced_dom]
-- Lean 4 proof step from Mathlib.Condensed.TopCatAdjunction (goal)
Goal:
X Y : CondensedSet
f : X ⟶ Y
⊢ 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)
have 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)
Tactic: apply continuous_sigma
-- Lean 4 proof step from Mathlib.Condensed.TopCatAdjunction (goal)
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 :
        (↑((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)
have 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)
Tactic: simp only [Function.comp_apply, coinducingCoprod]