awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Module (goal)
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
X Y : ModuleCat R
f : X ⟶ Y
⊢ (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 CompHaus) (ModuleCat R))
          (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) f)).hom
have e_a : Eq (α :=
  Quiver.Hom (V := CompHausᵒᵖ ⥤ ModuleCat R)
    (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))
      (obj (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
        (obj (Functor.const CompHausᵒᵖ)
          ((obj (functor R) X).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj
            (op (CompHaus.of PUnit.{u + 1}))))))
    (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))
      (obj (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R)) (obj (Functor.const CompHausᵒᵖ) Y))))
  (InducedCategory.Hom.hom
    (CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
      (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ)
        (NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map (functor R) f))
            (op (CompHaus.of PUnit.{u + 1})) ≫
          (functorIsoDiscreteAux₁ R Y).inv))))
  (InducedCategory.Hom.hom
    (CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
      (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) ((functorIsoDiscreteAux₁ R X).inv ≫ f))))
Tactic: simp [functorIsoDiscreteAux₂, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Module (hypothesis)
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
M : ModuleCat R
⊢ IsIso (X :=
    obj
      (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
          (CC := ModuleCat.carrier) ⋙
        constantSheaf (coherentTopology LightProfinite) (Type u))
      ((obj (functor R) M).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
        (op (LightProfinite.of PUnit.{u + 1}))))
    (NatTrans.app
      (Adjunction.counit
        (constantSheafAdj (coherentTopology LightProfinite) (Type u)
          (isTerminalPUnit (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)))))
      (obj
        (sheafCompose (coherentTopology LightProfinite)
          (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
            (CC := ModuleCat.carrier)))
        (obj (functor R) M)))
have this : Faithful (D := Sheaf (coherentTopology LightProfinite) (Type u))
  (constantSheaf (coherentTopology LightProfinite) (Type u))
Tactic: have : (constantSheaf (coherentTopology LightProfinite.{u}) (Type u)).Faithful :=
    inferInstanceAs (discrete _).Faithful
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Module (hypothesis)
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
M : ModuleCat R
this :
  Faithful (D := Sheaf (coherentTopology LightProfinite) (Type u))
    (constantSheaf (coherentTopology LightProfinite) (Type u))
⊢ IsIso (X :=
    obj
      (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
          (CC := ModuleCat.carrier) ⋙
        constantSheaf (coherentTopology LightProfinite) (Type u))
      ((obj (functor R) M).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
        (op (LightProfinite.of PUnit.{u + 1}))))
    (NatTrans.app
      (Adjunction.counit
        (constantSheafAdj (coherentTopology LightProfinite) (Type u)
          (isTerminalPUnit (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)))))
      (obj
        (sheafCompose (coherentTopology LightProfinite)
          (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
            (CC := ModuleCat.carrier)))
        (obj (functor R) M)))
have this₁ : Full (D := Sheaf (coherentTopology LightProfinite) (Type u)) (constantSheaf (coherentTopology LightProfinite) (Type u))
Tactic: have : (constantSheaf (coherentTopology LightProfinite.{u}) (Type u)).Full :=
    inferInstanceAs (discrete (Type u)).Full
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Module (goal)
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
M : ModuleCat R
this_1 :
  Faithful (D := Sheaf (coherentTopology LightProfinite) (Type u))
    (constantSheaf (coherentTopology LightProfinite) (Type u))
this :
  Full (D := Sheaf (coherentTopology LightProfinite) (Type u))
    (constantSheaf (coherentTopology LightProfinite) (Type u))
⊢ IsIso (X :=
    obj
      (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
          (CC := ModuleCat.carrier) ⋙
        constantSheaf (coherentTopology LightProfinite) (Type u))
      ((obj (functor R) M).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
        (op (LightProfinite.of PUnit.{u + 1}))))
    (NatTrans.app
      (Adjunction.counit
        (constantSheafAdj (coherentTopology LightProfinite) (Type u)
          (isTerminalPUnit (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)))))
      (obj
        (sheafCompose (coherentTopology LightProfinite)
          (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
            (CC := ModuleCat.carrier)))
        (obj (functor R) M)))
have rw : Sheaf.IsConstant (coherentTopology LightProfinite)
  (obj
    (sheafCompose (coherentTopology LightProfinite)
      (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
        (CC := ModuleCat.carrier)))
    (obj (functor R) M))
Tactic: rw [← Sheaf.isConstant_iff_isIso_counit_app]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Module (goal)
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
M : ModuleCat R
this_1 :
  Faithful (D := Sheaf (coherentTopology LightProfinite) (Type u))
    (constantSheaf (coherentTopology LightProfinite) (Type u))
this :
  Full (D := Sheaf (coherentTopology LightProfinite) (Type u))
    (constantSheaf (coherentTopology LightProfinite) (Type u))
⊢ Sheaf.IsConstant (coherentTopology LightProfinite)
    (obj
      (sheafCompose (coherentTopology LightProfinite)
        (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
          (CC := ModuleCat.carrier)))
      (obj (functor R) M))
have mem_essImage : essImage (constantSheaf (coherentTopology LightProfinite) (Type u))
  (obj
    (sheafCompose (coherentTopology LightProfinite)
      (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
        (CC := ModuleCat.carrier)))
    (obj (functor R) M))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Module (goal)
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
M : ModuleCat R
this_1 :
  Faithful (D := Sheaf (coherentTopology LightProfinite) (Type u))
    (constantSheaf (coherentTopology LightProfinite) (Type u))
this :
  Full (D := Sheaf (coherentTopology LightProfinite) (Type u))
    (constantSheaf (coherentTopology LightProfinite) (Type u))
⊢ essImage (discrete (Type u))
    (obj
      (sheafCompose (coherentTopology LightProfinite)
        (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
          (CC := ModuleCat.carrier)))
      (obj (functor R) M))
have mem_essImage : LightCondSet.LocallyConstant.functor.essImage
  (obj
    (sheafCompose (coherentTopology LightProfinite)
      (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
        (CC := ModuleCat.carrier)))
    (obj (functor R) M))
Tactic: rw [essImage_eq_of_natIso LightCondSet.LocallyConstant.iso.symm]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Module (goal)
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
X Y : ModuleCat R
f : X ⟶ Y
⊢ 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)
have 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
Tactic: rw [Iso.eq_inv_comp, ← Category.assoc, Iso.comp_inv_eq]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Module (goal)
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
X Y : ModuleCat R
f : X ⟶ 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)
have 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)
Tactic: rw [Category.assoc, ← Iso.eq_inv_comp,
      ← (discreteUnderlyingAdj (ModuleCat R)).counit_naturality]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Module (goal)
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
X Y : ModuleCat R
f : X ⟶ 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)
have 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)
Tactic: simp only [← assoc]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Module (goal)
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
X Y : ModuleCat R
f : X ⟶ 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)
have 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
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Module (goal)
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
X Y : ModuleCat R
f : X ⟶ Y
⊢ 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
have 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)
Tactic: rw [← Iso.comp_inv_eq]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Module (goal)
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
X Y : ModuleCat R
f : X ⟶ Y
⊢ 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)
have 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
Tactic: apply Sheaf.hom_ext
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Module (goal)
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
X Y : ModuleCat R
f : X ⟶ Y
⊢ (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
have 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))))
Tactic: simp [functorIsoDiscreteAux₂, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.Condensed.EffectiveEpi (goal)
Goal:
X Y : CompHaus
f : X ⟶ Y
hf : Epi f
⊢ Epi (compHausToCondensed.map f)
have 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')))
Tactic: rw [CondensedSet.epi_iff_locallySurjective_on_compHaus]
-- Lean 4 proof step from Mathlib.Condensed.Explicit (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v_1, u_1} (StructuredArrow X Stonean.toCompHaus.op) A
FA : A → A → Type u_2
CA : A → Type u_3
inst_2 : (X Y : A) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{u_3, v_1, u_1, u_2} A FA (CC := CA)
inst_4 : ReflectsFiniteProducts.{v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget A (FC := FA) (CC := CA))
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} Stoneanᵒᵖ A
inst_5 : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
⊢ IsSheaf (coherentTopology Stonean) F
have apply : IsSheaf (coherentTopology Stonean) (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
Tactic: apply isSheaf_coherent_of_projective_of_comp F (CategoryTheory.forget A)
-- Lean 4 proof step from Mathlib.Condensed.Explicit (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v_1, u_1} (StructuredArrow X profiniteToCompHaus.op) A
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} Profiniteᵒᵖ A
inst_2 : PreservesFiniteProducts F
hF : EqualizerCondition F
⊢ IsSheaf (coherentTopology Profinite) F
have rw : PreservesFiniteProducts F ∧ EqualizerCondition F
Tactic: rw [isSheaf_iff_preservesFiniteProducts_and_equalizerCondition F]
-- Lean 4 proof step from Mathlib.Condensed.Explicit (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v_1, u_1} (StructuredArrow X profiniteToCompHaus.op) A
FA : A → A → Type u_2
CA : A → Type u_3
inst_2 : (X Y : A) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{u_3, v_1, u_1, u_2} A FA (CC := CA)
inst_4 : ReflectsFiniteLimits.{v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget A (FC := FA) (CC := CA))
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} Profiniteᵒᵖ A
inst_5 : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
⊢ IsSheaf (coherentTopology Profinite) F
have apply : IsSheaf (coherentTopology Profinite) (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
Tactic: apply isSheaf_coherent_of_hasPullbacks_of_comp F (CategoryTheory.forget A)
-- Lean 4 proof step from Mathlib.Condensed.Explicit (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v_1, u_1} (StructuredArrow X profiniteToCompHaus.op) A
FA : A → A → Type u_2
CA : A → Type u_3
inst_2 : (X Y : A) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{u_3, v_1, u_1, u_2} A FA (CC := CA)
inst_4 : ReflectsFiniteLimits.{v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget A (FC := FA) (CC := CA))
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} Profiniteᵒᵖ A
inst_5 : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
⊢ IsSheaf (coherentTopology Profinite) (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
have rw : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA)) ∧
  EqualizerCondition (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
Tactic: rw [isSheaf_iff_preservesFiniteProducts_and_equalizerCondition]
-- Lean 4 proof step from Mathlib.Condensed.Explicit (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} CompHausᵒᵖ A
inst_1 : PreservesFiniteProducts F
hF : EqualizerCondition F
⊢ IsSheaf (coherentTopology CompHaus) F
have rw : PreservesFiniteProducts F ∧ EqualizerCondition F
Tactic: rw [isSheaf_iff_preservesFiniteProducts_and_equalizerCondition F]
-- Lean 4 proof step from Mathlib.Condensed.Explicit (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
FA : A → A → Type u_2
CA : A → Type u_3
inst_1 : (X Y : A) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FA X Y) (CA X) (CA Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} A FA (CC := CA)
inst_3 : ReflectsFiniteLimits.{v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget A (FC := FA) (CC := CA))
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} CompHausᵒᵖ A
inst_4 : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
⊢ IsSheaf (coherentTopology CompHaus) F
have apply : IsSheaf (coherentTopology CompHaus) (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
Tactic: apply isSheaf_coherent_of_hasPullbacks_of_comp F (CategoryTheory.forget A)