awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (hypothesis)
Goal:
R : Type
inst : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f :
  obj (free R)
      (tensorObj (𝒞 :=
          CompHausLike.category fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
          S ℕ∪{∞}).toCondensed ⟶
    Y
T : LightProfinite
π :
  T ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S ℕ∪{∞}
g : obj (free R) T.toCondensed ⟶ X
hπ : Epi π
comm : CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' :
  T' ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S' ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split :
  SplitEpi (X := LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
    (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' :
  Nonempty
    (↑(S'.toTop (P := fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
      Type)
⊢ ∃ (g' :
    obj (free R)
        (tensorObj (𝒞 :=
            CompHausLike.category fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
            S' ℕ∪{∞}).toCondensed ⟶
      X),
    CategoryTheory.Functor.map (free R) (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p
have this : Mono (X := LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})) (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
Tactic: have : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd _ _)) := by
      rw [CompHausLike.mono_iff_injective]
      exact Subtype.val_injective
-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (hypothesis)
Goal:
R : Type
inst : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f :
  obj (free R)
      (tensorObj (𝒞 :=
          CompHausLike.category fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
          S ℕ∪{∞}).toCondensed ⟶
    Y
T : LightProfinite
π :
  T ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S ℕ∪{∞}
g : obj (free R) T.toCondensed ⟶ X
hπ : Epi π
comm : CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' :
  T' ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S' ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split :
  SplitEpi (X := LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
    (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' :
  Nonempty
    (↑(S'.toTop (P := fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
      Type)
this : Mono (X := LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})) (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
⊢ ∃ (g' :
    obj (free R)
        (tensorObj (𝒞 :=
            CompHausLike.category fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
            S' ℕ∪{∞}).toCondensed ⟶
      X),
    CategoryTheory.Functor.map (free R) (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p
have this₁ : Nonempty
  (↑((LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop (P := fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
    Type)
Tactic: have : Nonempty (LightProfinite.fibre ∞ (π' ≫ snd _ _)) := by
      obtain ⟨x, hx⟩ := (.comp ((fun y ↦ ⟨(Nonempty.some inferInstance, y), rfl⟩))
        ((LightProfinite.epi_iff_surjective _).mp hπ') : ((snd S' ℕ∪{∞}) ∘ π').Surjective) ∞
      exact ⟨x, by simpa using hx⟩
-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (goal)
Goal:
R : Type
inst : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f :
  obj (free R)
      (tensorObj (𝒞 :=
          CompHausLike.category fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
          S ℕ∪{∞}).toCondensed ⟶
    Y
T : LightProfinite
π :
  T ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S ℕ∪{∞}
g : obj (free R) T.toCondensed ⟶ X
hπ : Epi π
comm : CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' :
  T' ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S' ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split :
  SplitEpi (X := LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
    (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' :
  Nonempty
    (↑(S'.toTop (P := fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
      Type)
this_1 : Mono (X := LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})) (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
this :
  Nonempty
    (↑((LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop (P := fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
      Type)
⊢ ∃ (g' :
    obj (free R)
        (tensorObj (𝒞 :=
            CompHausLike.category fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
            S' ℕ∪{∞}).toCondensed ⟶
      X),
    CategoryTheory.Functor.map (free R) (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p
have pos : ∀ (r_inf : T' ⟶ LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
  (hr : LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))),
  ∃ (g' :
    obj (free R)
        (tensorObj (𝒞 :=
            CompHausLike.category fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
            S' ℕ∪{∞}).toCondensed ⟶
      X),
    CategoryTheory.Functor.map (free R) (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p
Tactic: obtain ⟨r_inf, hr⟩ := Injective.factors (𝟙 _) (LightProfinite.fibreIncl ∞ (π' ≫ snd _ _))
-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (hypothesis)
Goal:
R : Type
inst : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f :
  obj (free R)
      (tensorObj (𝒞 :=
          CompHausLike.category fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
          S ℕ∪{∞}).toCondensed ⟶
    Y
T : LightProfinite
π :
  T ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S ℕ∪{∞}
g : obj (free R) T.toCondensed ⟶ X
hπ : Epi π
comm : CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' :
  T' ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S' ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split :
  SplitEpi (X := LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
    (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' :
  Nonempty
    (↑(S'.toTop (P := fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
      Type)
this_1 : Mono (X := LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})) (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
this :
  Nonempty
    (↑((LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop (P := fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
      Type)
r_inf : T' ⟶ LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
hπ'' : RegularEpi (lightProfiniteToLightCondSet.map π') := regularEpiOfEpi (lightProfiniteToLightCondSet.map π')
⊢ ∃ (g' :
    obj (free R)
        (tensorObj (𝒞 :=
            CompHausLike.category fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
            S' ℕ∪{∞}).toCondensed ⟶
      X),
    CategoryTheory.Functor.map (free R) (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p
have this₁ : EffectiveEpi π'
Tactic: have : EffectiveEpi π' := by
      rw [LightProfinite.effectiveEpi_iff_surjective, ← LightProfinite.epi_iff_surjective]
      infer_instance
-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (hypothesis)
Goal:
R : Type
inst : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f :
  obj (free R)
      (tensorObj (𝒞 :=
          CompHausLike.category fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
          S ℕ∪{∞}).toCondensed ⟶
    Y
T : LightProfinite
π :
  T ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S ℕ∪{∞}
g : obj (free R) T.toCondensed ⟶ X
hπ : Epi π
comm : CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' :
  T' ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S' ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split :
  SplitEpi (X := LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
    (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' :
  ¬Nonempty
      (↑(S'.toTop (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
        Type)
⊢ ∃ (g' :
    obj (free R)
        (tensorObj (𝒞 :=
            CompHausLike.category fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
            S' ℕ∪{∞}).toCondensed ⟶
      X),
    CategoryTheory.Functor.map (free R) (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p
have h : IsEmpty
  (tensorObj (𝒞 := types)
    (↑(S'.toTop (P := fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
      Type)
    (↑(ℕ∪{∞}.toTop (P := fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
      Type))
Tactic: have h : IsEmpty (S' ⊗ ℕ∪{∞}) := isEmpty_prod.mpr <| Or.inl <| by simpa using hS'
-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (hypothesis)
Goal:
R : Type
inst : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f :
  obj (free R)
      (tensorObj (𝒞 :=
          CompHausLike.category fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
          S ℕ∪{∞}).toCondensed ⟶
    Y
T : LightProfinite
π :
  T ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S ℕ∪{∞}
g : obj (free R) T.toCondensed ⟶ X
hπ : Epi π
comm : CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' :
  T' ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S' ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split :
  SplitEpi (X := LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
    (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' :
  ¬Nonempty
      (↑(S'.toTop (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
        Type)
h :
  IsEmpty
    (tensorObj (𝒞 := types)
      (↑(S'.toTop (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
        Type)
      (↑(ℕ∪{∞}.toTop (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
        Type))
⊢ ∃ (g' :
    obj (free R)
        (tensorObj (𝒞 :=
            CompHausLike.category fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
            S' ℕ∪{∞}).toCondensed ⟶
      X),
    CategoryTheory.Functor.map (free R) (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p
have this : IsIso π'
Tactic: have : IsIso π' := ⟨ConcreteCategory.ofHom ⟨(h.elim ·), continuous_of_const <| by aesop⟩,
      by ext x; exact h.elim (π' x), by ext x; all_goals exact h.elim x⟩
-- Lean 4 proof step from Mathlib.Condensed.Light.TopCatAdjunction (goal)
Goal:
X : LightCondSet
S : LightProfinite
x : X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)
⊢ Continuous (Y := X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))
    fun
      (a :
        (↑((Sigma.fst (β := fun (S : LightProfinite.{u}) ↦
                  X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S))
                  (Sigma.mk (β := fun (S : LightProfinite.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) S x)).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))
        (Sigma.mk (β := fun (S : LightProfinite.{u}) ↦
          X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) S x)
        a)
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 : LightCondSet
S : LightProfinite
x : X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op 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 : LightCondSet
f : X ⟶ Y
⊢ Continuous (X := X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op (of PUnit.{u + 1})))
    (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).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) ↦ X) (X.obj.obj (Opposite.op (of PUnit.{u + 1})))) →
        (fun (X : Type u) ↦ X) (Y.obj.obj (Opposite.op (of PUnit.{u + 1}))))
have rw : Continuous (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).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) ↦ X) (X.obj.obj (Opposite.op (of PUnit.{u + 1})))) →
        (fun (X : Type u) ↦ X) (Y.obj.obj (Opposite.op (of PUnit.{u + 1})))) ∘
    X.coinducingCoprod)
Tactic: rw [continuous_coinduced_dom]
-- Lean 4 proof step from Mathlib.Condensed.Light.TopCatAdjunction (goal)
Goal:
X Y : LightCondSet
f : X ⟶ Y
⊢ Continuous (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).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) ↦ X) (X.obj.obj (Opposite.op (of PUnit.{u + 1})))) →
          (fun (X : Type u) ↦ X) (Y.obj.obj (Opposite.op (of PUnit.{u + 1})))) ∘
      X.coinducingCoprod)
have hf : ∀ (i : (S : LightProfinite.{u}) × 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 :
        (↑(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)) ↦
    ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op (of PUnit.{u + 1})))) :
          (a : (fun (X : Type u) ↦ X) (X.obj.obj (Opposite.op (of PUnit.{u + 1})))) →
            (fun (X : Type u) ↦ X) (Y.obj.obj (Opposite.op (of PUnit.{u + 1})))) ∘
        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: apply continuous_sigma
-- 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 :
        (↑((Sigma.fst (β := fun (S : LightProfinite.{u}) ↦
                  X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S))
                  (Sigma.mk (β := fun (S : LightProfinite.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) S x)).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 : (fun (X : Type u) ↦ X) (X.obj.obj (Opposite.op (of PUnit.{u + 1})))) →
            (fun (X : Type u) ↦ X) (Y.obj.obj (Opposite.op (of PUnit.{u + 1})))) ∘
        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))
        (Sigma.mk (β := fun (S : LightProfinite.{u}) ↦
          X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) S x)
        a)
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) (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})))
Tactic: simp only [Function.comp_apply, coinducingCoprod]