awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Condensed.Discrete.LocallyConstant (hypothesis)
Goal:
P : TopCat.{u} → Prop
inst : ∀ (S : CompHausLike P) (p : (↑(S.toTop (P := P)) : Type u) → Prop), HasProp P (Subtype p)
inst_1 : HasProp P PUnit.{u + 1}
inst_2 : HasExplicitFiniteCoproducts P
inst_3 : HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
inst_4 : HasExplicitFiniteCoproducts P
X : Type (max u w)
S : CompHausLike P
f : LocallyConstant (↑(S.toTop (P := P)) : Type u) X
⊢ ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (NatTrans.app
              (InducedCategory.Hom.hom
                (ObjectProperty.homMk (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
                  (counitApp (P := P)
                    (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
                      (Functor.obj
                          (functor.{u, w} P hs :
                            Type (max u w) ⥤
                              Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
                          X :
                        Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))))))
              (op S)) :
          TypeCat.Fun (LocallyConstant (↑(S.toTop (P := P)) : Type u) (LocallyConstant PUnit.{u + 1} X))
            (LocallyConstant (↑(S.toTop (P := P)) : Type u) X)) :
        (a : LocallyConstant (↑S.toTop : Type u) (LocallyConstant PUnit.{u + 1} X)) →
          LocallyConstant (↑S.toTop : Type u) X)
      (map (fun (x : X) ↦ LocallyConstant.const PUnit.{u + 1} x) f) =
    f
have this : Preregular.{u, u + 1} (CompHausLike P)
Tactic: have := CompHausLike.preregular hs
-- Lean 4 proof step from Mathlib.Condensed.Discrete.LocallyConstant (goal)
Goal:
P : TopCat.{u} → Prop
inst : ∀ (S : CompHausLike P) (p : (↑(S.toTop (P := P)) : Type u) → Prop), HasProp P (Subtype p)
inst_1 : HasProp P PUnit.{u + 1}
inst_2 : HasExplicitFiniteCoproducts P
inst_3 : HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
inst_4 : HasExplicitFiniteCoproducts P
X : Type (max u w)
S : CompHausLike P
f : LocallyConstant (↑(S.toTop (P := P)) : Type u) X
this : Preregular.{u, u + 1} (CompHausLike P)
⊢ ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (NatTrans.app
              (InducedCategory.Hom.hom
                (ObjectProperty.homMk (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
                  (counitApp (P := P)
                    (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
                      (Functor.obj
                          (functor.{u, w} P hs :
                            Type (max u w) ⥤
                              Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
                          X :
                        Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))))))
              (op S)) :
          TypeCat.Fun (LocallyConstant (↑(S.toTop (P := P)) : Type u) (LocallyConstant PUnit.{u + 1} X))
            (LocallyConstant (↑(S.toTop (P := P)) : Type u) X)) :
        (a : LocallyConstant (↑S.toTop : Type u) (LocallyConstant PUnit.{u + 1} X)) →
          LocallyConstant (↑S.toTop : Type u) X)
      (map (fun (x : X) ↦ LocallyConstant.const PUnit.{u + 1} x) f) =
    f
have w : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: apply presheaf_ext
    (X := ((functor P hs).obj X).obj) (Y := ((functor.{u, w} P hs).obj X).obj)
      (f.map ((unit P hs).app X))
-- Lean 4 proof step from Mathlib.Condensed.Discrete.LocallyConstant (hypothesis)
Goal:
P : TopCat.{u} → Prop
inst : ∀ (S : CompHausLike P) (p : (↑(S.toTop (P := P)) : Type u) → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_1 : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑(S.toTop (P := P)) : Type u) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
X_1 : TopCat
inst_2 : HasExplicitFiniteCoproducts P
inst_3 : HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
inst_4 : HasExplicitFiniteCoproducts P
X : Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))
x : X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj (op (of P PUnit.{u + 1}))
⊢ ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (NatTrans.app (InducedCategory.Hom.hom (NatTrans.app (counit P hs) X)) (op (of P PUnit.{u + 1}))) :
          TypeCat.Fun
            (LocallyConstant PUnit.{u + 1}
              (X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj (op (of P PUnit.{u + 1}))))
            (X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj (op (of P PUnit.{u + 1})))) :
        (a : LocallyConstant PUnit.{u + 1} (X.obj.obj (op (of P PUnit.{u + 1})))) → X.obj.obj (op (of P PUnit.{u + 1})))
      (LocallyConstant.const PUnit.{u + 1} x) =
    x
have this : Preregular.{u, u + 1} (CompHausLike P)
Tactic: have := CompHausLike.preregular hs
-- Lean 4 proof step from Mathlib.Condensed.Discrete.LocallyConstant (goal)
Goal:
P : TopCat.{u} → Prop
inst : ∀ (S : CompHausLike P) (p : (↑(S.toTop (P := P)) : Type u) → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_1 : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑(S.toTop (P := P)) : Type u) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
X_1 : TopCat
inst_2 : HasExplicitFiniteCoproducts P
inst_3 : HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
inst_4 : HasExplicitFiniteCoproducts P
X : Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))
x : X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj (op (of P PUnit.{u + 1}))
this_1 : Preregular.{u, u + 1} (CompHausLike P)
this : PreservesFiniteProducts (Functor.obj (sheafToPresheaf (coherentTopology (CompHausLike P)) (Type (max u w))) X) :=
  ⋯
⊢ ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (NatTrans.app (InducedCategory.Hom.hom (NatTrans.app (counit P hs) X)) (op (of P PUnit.{u + 1}))) :
          TypeCat.Fun
            (LocallyConstant PUnit.{u + 1}
              (X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj (op (of P PUnit.{u + 1}))))
            (X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj (op (of P PUnit.{u + 1})))) :
        (a : LocallyConstant PUnit.{u + 1} (X.obj.obj (op (of P PUnit.{u + 1})))) → X.obj.obj (op (of P PUnit.{u + 1})))
      (LocallyConstant.const PUnit.{u + 1} x) =
    x
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: apply presheaf_ext ((unit P hs).app _ x)
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Module (hypothesis)
Goal:
P : TopCat.{u} → Prop
R : Type (max u w)
inst : Ring R
inst_1 : HasExplicitFiniteCoproducts P
inst_2 : HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
X : ModuleCat R
⊢ Presheaf.IsSheaf (C := CompHausLike P) (coherentTopology (CompHausLike P))
    (obj (functorToPresheaves.{w, u} (P := P) R) X)
have this : Preregular.{u, u + 1} (CompHausLike P)
Tactic: have := CompHausLike.preregular hs
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Module (goal)
Goal:
P : TopCat.{u} → Prop
R : Type (max u w)
inst : Ring R
inst_1 : HasExplicitFiniteCoproducts P
inst_2 : HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
X : ModuleCat R
this : Preregular.{u, u + 1} (CompHausLike P)
⊢ Presheaf.IsSheaf (C := CompHausLike P) (coherentTopology (CompHausLike P))
    (obj (functorToPresheaves.{w, u} (P := P) R) X)
have hF : Presheaf.IsSheaf (C := CompHausLike P) (coherentTopology (CompHausLike P))
  (obj (functorToPresheaves.{w, u} (P := P) R) X ⋙
    forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u w)) →ₗ[R] (↑x2 : Type (max u w))) (CC :=
      ModuleCat.carrier))
Tactic: apply Presheaf.isSheaf_coherent_of_hasPullbacks_of_comp
      (s := CategoryTheory.forget (ModuleCat R))
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Module (hypothesis)
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
M : ModuleCat R
⊢ IsIso (X :=
    obj
      (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
          (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier) ⋙
        constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
      ((obj (functor R) M).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj
        (op (CompHaus.of PUnit.{u + 1}))))
    (NatTrans.app
      (Adjunction.counit (constantSheafAdj (coherentTopology CompHaus) (Type (u + 1)) CompHaus.isTerminalPUnit))
      (obj
        (sheafCompose (coherentTopology CompHaus)
          (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
            (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier)))
        (obj (functor R) M)))
have this : Faithful (D := Sheaf (coherentTopology CompHaus) (Type (u + 1)))
  (constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
Tactic: have : (constantSheaf (coherentTopology CompHaus) (Type (u + 1))).Faithful :=
    inferInstanceAs (discrete _).Faithful
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Module (hypothesis)
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
M : ModuleCat R
this :
  Faithful (D := Sheaf (coherentTopology CompHaus) (Type (u + 1)))
    (constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
⊢ IsIso (X :=
    obj
      (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
          (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier) ⋙
        constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
      ((obj (functor R) M).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj
        (op (CompHaus.of PUnit.{u + 1}))))
    (NatTrans.app
      (Adjunction.counit (constantSheafAdj (coherentTopology CompHaus) (Type (u + 1)) CompHaus.isTerminalPUnit))
      (obj
        (sheafCompose (coherentTopology CompHaus)
          (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
            (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier)))
        (obj (functor R) M)))
have this₁ : Full (D := Sheaf (coherentTopology CompHaus) (Type (u + 1))) (constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
Tactic: have : (constantSheaf (coherentTopology CompHaus) (Type (u + 1))).Full :=
    inferInstanceAs (discrete _).Full
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Module (goal)
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
M : ModuleCat R
this_1 :
  Faithful (D := Sheaf (coherentTopology CompHaus) (Type (u + 1)))
    (constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
this :
  Full (D := Sheaf (coherentTopology CompHaus) (Type (u + 1)))
    (constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
⊢ IsIso (X :=
    obj
      (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
          (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier) ⋙
        constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
      ((obj (functor R) M).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj
        (op (CompHaus.of PUnit.{u + 1}))))
    (NatTrans.app
      (Adjunction.counit (constantSheafAdj (coherentTopology CompHaus) (Type (u + 1)) CompHaus.isTerminalPUnit))
      (obj
        (sheafCompose (coherentTopology CompHaus)
          (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
            (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier)))
        (obj (functor R) M)))
have rw : Sheaf.IsConstant (coherentTopology CompHaus)
  (obj
    (sheafCompose (coherentTopology CompHaus)
      (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
        (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (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 + 1)
inst : Ring R
M : ModuleCat R
this_1 :
  Faithful (D := Sheaf (coherentTopology CompHaus) (Type (u + 1)))
    (constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
this :
  Full (D := Sheaf (coherentTopology CompHaus) (Type (u + 1)))
    (constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
⊢ Sheaf.IsConstant (coherentTopology CompHaus)
    (obj
      (sheafCompose (coherentTopology CompHaus)
        (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
          (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier)))
      (obj (functor R) M))
have mem_essImage : essImage (constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
  (obj
    (sheafCompose (coherentTopology CompHaus)
      (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
        (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (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 + 1)
inst : Ring R
M : ModuleCat R
this_1 :
  Faithful (D := Sheaf (coherentTopology CompHaus) (Type (u + 1)))
    (constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
this :
  Full (D := Sheaf (coherentTopology CompHaus) (Type (u + 1)))
    (constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
⊢ essImage (discrete (Type (u + 1)))
    (obj
      (sheafCompose (coherentTopology CompHaus)
        (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
          (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier)))
      (obj (functor R) M))
have mem_essImage : CondensedSet.LocallyConstant.functor.essImage
  (obj
    (sheafCompose (coherentTopology CompHaus)
      (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
        (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier)))
    (obj (functor R) M))
Tactic: rw [essImage_eq_of_natIso CondensedSet.LocallyConstant.iso.symm]
-- 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 (functor R) f ≫ (functorIsoDiscreteComponents R Y).inv =
    (functorIsoDiscreteComponents R X).inv ≫
      CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
        (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) f)
have rw : (functorIsoDiscreteComponents R X).hom ≫ CategoryTheory.Functor.map (functor R) f =
  CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
      (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) 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 + 1)
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 CompHaus) (ModuleCat R))
        (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) 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 CompHaus) (ModuleCat R))
        (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) f) ≫
      (functorIsoDiscreteAux₂ R Y).hom ≫
        NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (ModuleCat R))) (obj (functor R) Y)
Tactic: rw [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 + 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)) ≫
      NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (ModuleCat R))) (obj (functor R) Y) =
    (functorIsoDiscreteAux₂ R X).inv ≫
      CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
          (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) 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 CompHaus) (ModuleCat R))
          (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) 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 + 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)) ≫
      NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (ModuleCat R))) (obj (functor R) Y) =
    (((functorIsoDiscreteAux₂ R X).inv ≫
          CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
            (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) 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 CompHaus) (ModuleCat R))
        (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) 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 + 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 X).inv ≫
        CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
          (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) 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 CompHaus) (ModuleCat R))
      (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) 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 + 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 =
    (functorIsoDiscreteAux₂ R X).inv ≫
      CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
        (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) 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 CompHaus) (ModuleCat R))
        (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) f)).hom
Tactic: apply Sheaf.hom_ext