awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
X Y : ModuleCat R
f : X ⟶ Y
rw :
  (functorIsoDiscreteComponents R X).hom ≫ CategoryTheory.Functor.map (functor R) f =
    CategoryTheory.Functor.map (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R))
        (CategoryTheory.Functor.map (Functor.const LightProfiniteᵒᵖ) f) ≫
      (functorIsoDiscreteComponents R Y).hom
⊢ CategoryTheory.Functor.map (functor R) f ≫ (functorIsoDiscreteComponents R Y).inv =
    (functorIsoDiscreteComponents R X).inv ≫
      CategoryTheory.Functor.map (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R))
        (CategoryTheory.Functor.map (Functor.const LightProfiniteᵒᵖ) f)

Tactic:
rw [Iso.eq_inv_comp, ← Category.assoc, Iso.comp_inv_eq]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
X Y : ModuleCat R
f : X ⟶ Y
rw :
  CategoryTheory.Functor.map (discrete (ModuleCat R))
        (CategoryTheory.Functor.map (underlying (ModuleCat R)) (CategoryTheory.Functor.map (functor R) f)) ≫
      NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (ModuleCat R))) (obj (functor R) Y) =
    (functorIsoDiscreteAux₂ R X).inv ≫
      CategoryTheory.Functor.map (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R))
          (CategoryTheory.Functor.map (Functor.const LightProfiniteᵒᵖ) f) ≫
        (functorIsoDiscreteAux₂ R Y).hom ≫
          NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (ModuleCat R))) (obj (functor R) Y)
⊢ ((functorIsoDiscreteAux₂ R X).hom ≫
        NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (ModuleCat R))) (obj (functor R) X)) ≫
      CategoryTheory.Functor.map (functor R) f =
    CategoryTheory.Functor.map (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R))
        (CategoryTheory.Functor.map (Functor.const LightProfiniteᵒᵖ) f) ≫
      (functorIsoDiscreteAux₂ R Y).hom ≫
        NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (ModuleCat R))) (obj (functor R) Y)

Tactic:
rw [Category.assoc, ← Iso.eq_inv_comp,
      ← (discreteUnderlyingAdj (ModuleCat R)).counit_naturality]

Premises used: CategoryTheory.Category.assoc, ModuleCat, CategoryTheory.Adjunction.counit_naturality, LightCondensed.discreteUnderlyingAdj, CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
X Y : ModuleCat R
f : X ⟶ Y
simp :
  CategoryTheory.Functor.map (discrete (ModuleCat R))
        (CategoryTheory.Functor.map (underlying (ModuleCat R)) (CategoryTheory.Functor.map (functor R) f)) ≫
      NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (ModuleCat R))) (obj (functor R) Y) =
    (((functorIsoDiscreteAux₂ R X).inv ≫
          CategoryTheory.Functor.map (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R))
            (CategoryTheory.Functor.map (Functor.const LightProfiniteᵒᵖ) f)) ≫
        (functorIsoDiscreteAux₂ R Y).hom) ≫
      NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (ModuleCat R))) (obj (functor R) Y)
⊢ CategoryTheory.Functor.map (discrete (ModuleCat R))
        (CategoryTheory.Functor.map (underlying (ModuleCat R)) (CategoryTheory.Functor.map (functor R) f)) ≫
      NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (ModuleCat R))) (obj (functor R) Y) =
    (functorIsoDiscreteAux₂ R X).inv ≫
      CategoryTheory.Functor.map (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R))
          (CategoryTheory.Functor.map (Functor.const LightProfiniteᵒᵖ) f) ≫
        (functorIsoDiscreteAux₂ R Y).hom ≫
          NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (ModuleCat R))) (obj (functor R) Y)

Tactic:
simp only [← assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
X Y : ModuleCat R
f : X ⟶ Y
e_a :
  CategoryTheory.Functor.map (discrete (ModuleCat R))
      (CategoryTheory.Functor.map (underlying (ModuleCat R)) (CategoryTheory.Functor.map (functor R) f)) =
    ((functorIsoDiscreteAux₂ R X).inv ≫
        CategoryTheory.Functor.map (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R))
          (CategoryTheory.Functor.map (Functor.const LightProfiniteᵒᵖ) f)) ≫
      (functorIsoDiscreteAux₂ R Y).hom
⊢ CategoryTheory.Functor.map (discrete (ModuleCat R))
        (CategoryTheory.Functor.map (underlying (ModuleCat R)) (CategoryTheory.Functor.map (functor R) f)) ≫
      NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (ModuleCat R))) (obj (functor R) Y) =
    (((functorIsoDiscreteAux₂ R X).inv ≫
          CategoryTheory.Functor.map (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R))
            (CategoryTheory.Functor.map (Functor.const LightProfiniteᵒᵖ) f)) ≫
        (functorIsoDiscreteAux₂ R Y).hom) ≫
      NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (ModuleCat R))) (obj (functor R) Y)

Tactic:
congr 1
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
X Y : ModuleCat R
f : X ⟶ Y
e_a :
  CategoryTheory.Functor.map (discrete (ModuleCat R))
        (CategoryTheory.Functor.map (underlying (ModuleCat R)) (CategoryTheory.Functor.map (functor R) f)) ≫
      (functorIsoDiscreteAux₂ R Y).inv =
    (functorIsoDiscreteAux₂ R X).inv ≫
      CategoryTheory.Functor.map (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R))
        (CategoryTheory.Functor.map (Functor.const LightProfiniteᵒᵖ) f)
⊢ CategoryTheory.Functor.map (discrete (ModuleCat R))
      (CategoryTheory.Functor.map (underlying (ModuleCat R)) (CategoryTheory.Functor.map (functor R) f)) =
    ((functorIsoDiscreteAux₂ R X).inv ≫
        CategoryTheory.Functor.map (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R))
          (CategoryTheory.Functor.map (Functor.const LightProfiniteᵒᵖ) f)) ≫
      (functorIsoDiscreteAux₂ R Y).hom

Tactic:
rw [← Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
X Y : ModuleCat R
f : X ⟶ Y
e_a :
  (CategoryTheory.Functor.map (discrete (ModuleCat R))
          (CategoryTheory.Functor.map (underlying (ModuleCat R)) (CategoryTheory.Functor.map (functor R) f)) ≫
        (functorIsoDiscreteAux₂ R Y).inv).hom =
    ((functorIsoDiscreteAux₂ R X).inv ≫
        CategoryTheory.Functor.map (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R))
          (CategoryTheory.Functor.map (Functor.const LightProfiniteᵒᵖ) f)).hom
⊢ CategoryTheory.Functor.map (discrete (ModuleCat R))
        (CategoryTheory.Functor.map (underlying (ModuleCat R)) (CategoryTheory.Functor.map (functor R) f)) ≫
      (functorIsoDiscreteAux₂ R Y).inv =
    (functorIsoDiscreteAux₂ R X).inv ≫
      CategoryTheory.Functor.map (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R))
        (CategoryTheory.Functor.map (Functor.const LightProfiniteᵒᵖ) f)

Tactic:
apply Sheaf.hom_ext

Premises used: CategoryTheory.Sheaf.hom_ext
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
X Y : ModuleCat R
f : X ⟶ Y
e_a :
  Eq (α :=
    Quiver.Hom (V := LightProfiniteᵒᵖ ⥤ ModuleCat R)
      (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite))
        (obj (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R))
          (obj (Functor.const LightProfiniteᵒᵖ)
            ((obj (functor R) X).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
              (op (LightProfinite.of PUnit.{u + 1}))))))
      (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite))
        (obj (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R))
          (obj (Functor.const LightProfiniteᵒᵖ) Y))))
    (InducedCategory.Hom.hom
      (CategoryTheory.Functor.map (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R))
        (CategoryTheory.Functor.map (Functor.const LightProfiniteᵒᵖ)
          (NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map (functor R) f))
              (op (LightProfinite.of PUnit.{u + 1})) ≫
            (functorIsoDiscreteAux₁ R Y).inv))))
    (InducedCategory.Hom.hom
      (CategoryTheory.Functor.map (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R))
        (CategoryTheory.Functor.map (Functor.const LightProfiniteᵒᵖ) ((functorIsoDiscreteAux₁ R X).inv ≫ f))))
⊢ (CategoryTheory.Functor.map (discrete (ModuleCat R))
          (CategoryTheory.Functor.map (underlying (ModuleCat R)) (CategoryTheory.Functor.map (functor R) f)) ≫
        (functorIsoDiscreteAux₂ R Y).inv).hom =
    ((functorIsoDiscreteAux₂ R X).inv ≫
        CategoryTheory.Functor.map (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R))
          (CategoryTheory.Functor.map (Functor.const LightProfiniteᵒᵖ) f)).hom

Tactic:
simp [functorIsoDiscreteAux₂, ← Functor.map_comp]

Premises used: LightCondMod.LocallyConstant.functorIsoDiscreteAux₂, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
X Y : ModuleCat R
f : X ⟶ Y
⊢ Eq (α :=
    Quiver.Hom (V := LightProfiniteᵒᵖ ⥤ ModuleCat R)
      (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite))
        (obj (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R))
          (obj (Functor.const LightProfiniteᵒᵖ)
            ((obj (functor R) X).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
              (op (LightProfinite.of PUnit.{u + 1}))))))
      (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite))
        (obj (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R))
          (obj (Functor.const LightProfiniteᵒᵖ) Y))))
    (InducedCategory.Hom.hom
      (CategoryTheory.Functor.map (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R))
        (CategoryTheory.Functor.map (Functor.const LightProfiniteᵒᵖ)
          (NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map (functor R) f))
              (op (LightProfinite.of PUnit.{u + 1})) ≫
            (functorIsoDiscreteAux₁ R Y).inv))))
    (InducedCategory.Hom.hom
      (CategoryTheory.Functor.map (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R))
        (CategoryTheory.Functor.map (Functor.const LightProfiniteᵒᵖ) ((functorIsoDiscreteAux₁ R X).inv ≫ f))))

Tactic:
rfl
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
⊢ Faithful (C := ModuleCat R) (functor R)

Tactic:
(fullyFaithfulFunctor R).faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, LightCondMod.LocallyConstant.fullyFaithfulFunctor
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
⊢ Full (C := ModuleCat R) (functor R)

Tactic:
(fullyFaithfulFunctor R).full

Premises used: CategoryTheory.Functor.FullyFaithful.full, LightCondMod.LocallyConstant.fullyFaithfulFunctor
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
⊢ Faithful.{u, u + 1, u + 1, u + 1} (C := ModuleCat R) (discrete (ModuleCat R))

Tactic:
Functor.Faithful.of_iso (functorIsoDiscrete R)

Premises used: CategoryTheory.Functor.Faithful.of_iso, LightCondMod.LocallyConstant.functorIsoDiscrete
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
⊢ Faithful (C := ModuleCat R) (D := Sheaf (coherentTopology LightProfinite) (ModuleCat R))
    (constantSheaf (coherentTopology LightProfinite) (ModuleCat R))

Tactic:
inferInstanceAs (discrete.{u} (ModuleCat R)).Faithful

Premises used: _private.0.LightCondMod.LocallyConstant.instFaithfulModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf._proof_1
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
⊢ Full.{u, u + 1, u + 1, u + 1} (C := ModuleCat R) (discrete (ModuleCat R))

Tactic:
Functor.Full.of_iso (functorIsoDiscrete R)

Premises used: CategoryTheory.Functor.Full.of_iso, LightCondMod.LocallyConstant.functorIsoDiscrete
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
⊢ Full (C := ModuleCat R) (D := Sheaf (coherentTopology LightProfinite) (ModuleCat R))
    (constantSheaf (coherentTopology LightProfinite) (ModuleCat R))

Tactic:
inferInstanceAs (discrete.{u} (ModuleCat.{u} R)).Full

Premises used: _private.0.LightCondMod.LocallyConstant.instFullModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf._proof_1
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
⊢ Faithful (D := Sheaf (coherentTopology LightProfinite) (Type u))
    (constantSheaf (coherentTopology LightProfinite) (Type u))

Tactic:
inferInstanceAs (discrete (Type u)).Faithful

Premises used: _private.0.LightCondMod.LocallyConstant.instIsIsoLightCondSetMapForgetAppLightCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor._proof_1
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
⊢ Full (D := Sheaf (coherentTopology LightProfinite) (Type u))
    (constantSheaf (coherentTopology LightProfinite) (Type u))

Tactic:
inferInstanceAs (discrete (Type u)).Full

Premises used: _private.0.LightCondMod.LocallyConstant.instIsIsoLightCondSetMapForgetAppLightCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor._proof_2
-- Module: Mathlib.Condensed.EffectiveEpi
Goal:
X Y : CompHaus
f : X ⟶ Y
hf : Epi f
rw :
  ∀ (S : CompHaus.{u_1})
    (y : (compHausToCondensed.obj Y).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)),
    ∃ (S' : CompHaus.{u_1}) (φ : S' ⟶ S) (_ :
      Function.Surjective (α :=
        (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
          S')
        (β :=
        (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
          S)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
              C((↑(x1.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
                (↑(x2.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)))
              (CC := fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
              (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) φ) :
          (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) S') →
            (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) S))
      (x : (compHausToCondensed.obj X).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S')),
      Eq (α :=
        (fun (X : Type (u_1 + 1)) ↦ X)
          ((compHausToCondensed.obj Y).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((compHausToCondensed.map f).hom.app (Opposite.op S')) :
              (a : (fun (X : Type (u_1 + 1)) ↦ X) ((compHausToCondensed.obj X).obj.obj (Opposite.op S'))) →
                (fun (X : Type (u_1 + 1)) ↦ X) ((compHausToCondensed.obj Y).obj.obj (Opposite.op S')))
            x :
          (fun (X : Type (u_1 + 1)) ↦ X)
            ((compHausToCondensed.obj Y).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((compHausToCondensed.obj Y).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map
                  (Opposite.op φ)) :
              (a : (fun (X : Type (u_1 + 1)) ↦ X) ((compHausToCondensed.obj Y).obj.obj (Opposite.op S))) →
                (fun (X : Type (u_1 + 1)) ↦ X) ((compHausToCondensed.obj Y).obj.obj (Opposite.op S')))
            y :
          (fun (X : Type (u_1 + 1)) ↦ X)
            ((compHausToCondensed.obj Y).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S')))
⊢ Epi (compHausToCondensed.map f)

Tactic:
rw [CondensedSet.epi_iff_locallySurjective_on_compHaus]

Premises used: CondensedSet.epi_iff_locallySurjective_on_compHaus
-- Module: Mathlib.Condensed.EffectiveEpi
Goal:
X Y : CompHaus
f : X ⟶ Y
hf : Epi f
S : CompHaus
g : (compHausToCondensed.obj Y).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)
⊢ ∃ (S' : CompHaus.{u_1}) (φ : S' ⟶ S) (_ :
    Function.Surjective (α :=
      (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
        S')
      (β :=
      (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
        S)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
            C((↑(x1.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
              (↑(x2.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)))
            (CC := fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) φ) :
        (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) S') →
          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) S))
    (x : (compHausToCondensed.obj X).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S')),
    Eq (α :=
      (fun (X : Type (u_1 + 1)) ↦ X)
        ((compHausToCondensed.obj Y).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((compHausToCondensed.map f).hom.app (Opposite.op S')) :
            (a : (fun (X : Type (u_1 + 1)) ↦ X) ((compHausToCondensed.obj X).obj.obj (Opposite.op S'))) →
              (fun (X : Type (u_1 + 1)) ↦ X) ((compHausToCondensed.obj Y).obj.obj (Opposite.op S')))
          x :
        (fun (X : Type (u_1 + 1)) ↦ X)
          ((compHausToCondensed.obj Y).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((compHausToCondensed.obj Y).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map
                (Opposite.op φ)) :
            (a : (fun (X : Type (u_1 + 1)) ↦ X) ((compHausToCondensed.obj Y).obj.obj (Opposite.op S))) →
              (fun (X : Type (u_1 + 1)) ↦ X) ((compHausToCondensed.obj Y).obj.obj (Opposite.op S')))
          g :
        (fun (X : Type (u_1 + 1)) ↦ X)
          ((compHausToCondensed.obj Y).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S')))

Tactic:
⟨pullback f g.down, pullback.snd _ _, fun y ↦ ?_, ⟨pullback.fst _ _⟩,
      ULift.ext _ _ <| pullback.condition _ _⟩

Premises used: CompHausLike.pullback.condition, ULift.ext, CompHausLike.pullback.fst, CompHausLike.pullback, Exists.intro, CompHausLike.pullback.snd, ULift.up, ULift.down
-- Module: Mathlib.Condensed.EffectiveEpi
Goal:
⊢ IsRegularEpiCategory CondensedSet

Tactic:
inferInstanceAs <| IsRegularEpiCategory (Sheaf _ _)

Premises used: _private.0.instIsRegularEpiCategoryCondensedSet._proof_1
-- Module: Mathlib.Condensed.EffectiveEpi
Goal:
⊢ compHausToCondensed.PreservesEffectiveEpis

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Condensed.Epi
Goal:
X Y : CondensedSet
f : X ⟶ Y
⊢ Epi f ↔
    ∀ (S : CompHaus.{u}) (y : Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S)),
      ∃ (S' : CompHaus.{u}) (φ : S' ⟶ S) (_ :
        Function.Surjective (α :=
          (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
              (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
            S')
          (β :=
          (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
              (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
            S)
          (⇑(hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
                  (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
                (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) φ) :
            (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) S') →
              (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) S))
        (x : X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S')),
        Eq (α := (fun (X : Type (u + 1)) ↦ X) (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S')))
          ((hom (FC := TypeCat.Fun) (f.hom.app (op S')) :
                (a : (fun (X : Type (u + 1)) ↦ X) (X.obj.obj (op S'))) →
                  (fun (X : Type (u + 1)) ↦ X) (Y.obj.obj (op S')))
              x :
            (fun (X : Type (u + 1)) ↦ X) (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S')))
          ((hom (FC := TypeCat.Fun) (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map (op φ)) :
                (a : (fun (X : Type (u + 1)) ↦ X) (Y.obj.obj (op S))) →
                  (fun (X : Type (u + 1)) ↦ X) (Y.obj.obj (op S')))
              y :
            (fun (X : Type (u + 1)) ↦ X) (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S')))

Tactic:
Condensed.epi_iff_locallySurjective_on_compHaus _ f

Premises used: Condensed.epi_iff_locallySurjective_on_compHaus
-- Module: Mathlib.Condensed.Epi
Goal:
X Y : CondensedSet
f : X ⟶ Y
⊢ Epi f ↔
    ∀ (S : Stonean.{u}),
      Function.Surjective (α :=
        (fun (X : Type (u + 1)) ↦ X) (X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S.compHaus)))
        (β :=
        (fun (X : Type (u + 1)) ↦ X) (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S.compHaus)))
        (⇑(hom (FC := TypeCat.Fun) (f.hom.app (op S.compHaus))) :
          (a : (fun (X : Type (u + 1)) ↦ X) (X.obj.obj (op S.compHaus))) →
            (fun (X : Type (u + 1)) ↦ X) (Y.obj.obj (op S.compHaus)))

Tactic:
Condensed.epi_iff_surjective_on_stonean _ f

Premises used: Condensed.epi_iff_surjective_on_stonean