awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify J AddCommGrpCat
inst_2 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_3 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
X Y : Type u
f : X ⟶ Y
⊢ Eq (α := Quiver.Hom (V := SheafOfModules R) (free X) (free Y))
    (CategoryTheory.Functor.map freeFunctor f :
      Quiver.Hom (V := SheafOfModules R) (Functor.obj freeFunctor X) (Functor.obj freeFunctor Y))
    (freeMap (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X) → Y))

Tactic:
Cofan.IsColimit.hom_ext (isColimitFreeCofan _) _ _
    (fun i ↦ (Sigma.ι_desc _ _).trans (ιFree_freeMap f i).symm)

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.Sigma.ι, SheafOfModules.unit, SheafOfModules.ιFree_freeMap, CategoryTheory.Limits.Cofan.IsColimit.hom_ext, CategoryTheory.Limits.colimit, CategoryTheory.Discrete.natTrans, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.Sigma.ι_desc, SheafOfModules.free, SheafOfModules.isColimitFreeCofan, SheafOfModules.ιFree, Eq.symm, DFunLike.coe, Eq.trans, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify J AddCommGrpCat
inst_2 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_3 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
⊢ PreservesColimitsOfSize.{v₂, u₂, u, max u u₁, u + 1, max (max (u + 1) u₁) v₁} (D := SheafOfModules R) freeFunctor

Tactic:
inferInstanceAs (PreservesColimitsOfSize.{v₂, u₂} (sigmaConst.obj _))

Premises used: _private.0.SheafOfModules.instPreservesColimitsOfSizeFreeFunctor._proof_1
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J_1 : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J_1 RingCat
inst_1 : HasWeakSheafify J_1 AddCommGrpCat
inst_2 :
  J_1.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_3 :
  J_1.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
I J : Type u
rw :
  Eq (α := Quiver.Hom (V := SheafOfModules R) (free I) (free (I ⊕ J))) (coprod.inl ≫ Iso.hom (freeSumIso I J))
    (CategoryTheory.Functor.map freeFunctor (↾Sum.inl))
⊢ Eq (α := Quiver.Hom (V := SheafOfModules R) (free I) (free (I ⊕ J))) (coprod.inl ≫ Iso.hom (freeSumIso I J))
    (freeMap Sum.inl)

Tactic:
rw [← dsimp% freeFunctor_map (↾(Sum.inl : I → I ⊕ J))]

Premises used: TypeCat.ofHom, Sum.inl, SheafOfModules.freeFunctor_map
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J_1 : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J_1 RingCat
inst_1 : HasWeakSheafify J_1 AddCommGrpCat
inst_2 :
  J_1.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_3 :
  J_1.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
I J : Type u
⊢ Eq (α := Quiver.Hom (V := SheafOfModules R) (free I) (free (I ⊕ J))) (coprod.inl ≫ Iso.hom (freeSumIso I J))
    (CategoryTheory.Functor.map freeFunctor (↾Sum.inl))

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_hom
    (coprodIsCoprod (free (R := R) I) (free J)) _ (.mk .left)

Premises used: CategoryTheory.Limits.coprodIsCoprod, CategoryTheory.Discrete.functor, CategoryTheory.Limits.colimit, CategoryTheory.Discrete.mk, CategoryTheory.Limits.pair, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.colimit.desc, SheafOfModules.free, CategoryTheory.Limits.Sigma.map', CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J_1 : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J_1 RingCat
inst_1 : HasWeakSheafify J_1 AddCommGrpCat
inst_2 :
  J_1.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_3 :
  J_1.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
I J : Type u
⊢ Eq (α := Quiver.Hom (V := SheafOfModules R) (free I) (free (I ⊕ J))) (coprod.inl ≫ Iso.hom (freeSumIso I J))
    (CategoryTheory.Functor.map freeFunctor (↾Sum.inl))

Tactic:
exact IsColimit.comp_coconePointUniqueUpToIso_hom
    (coprodIsCoprod (free (R := R) I) (free J)) _ (.mk .left)

Premises used: CategoryTheory.Limits.coprodIsCoprod, CategoryTheory.Discrete.mk, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, SheafOfModules.free, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J_1 : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J_1 RingCat
inst_1 : HasWeakSheafify J_1 AddCommGrpCat
inst_2 :
  J_1.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_3 :
  J_1.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
I J : Type u
rw :
  Eq (α := Quiver.Hom (V := SheafOfModules R) (free J) (free (I ⊕ J))) (coprod.inr ≫ Iso.hom (freeSumIso I J))
    (CategoryTheory.Functor.map freeFunctor (↾Sum.inr))
⊢ Eq (α := Quiver.Hom (V := SheafOfModules R) (free J) (free (I ⊕ J))) (coprod.inr ≫ Iso.hom (freeSumIso I J))
    (freeMap Sum.inr)

Tactic:
rw [← dsimp% freeFunctor_map (↾(Sum.inr : J → I ⊕ J))]

Premises used: TypeCat.ofHom, SheafOfModules.freeFunctor_map, Sum.inr
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J_1 : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J_1 RingCat
inst_1 : HasWeakSheafify J_1 AddCommGrpCat
inst_2 :
  J_1.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_3 :
  J_1.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
I J : Type u
⊢ Eq (α := Quiver.Hom (V := SheafOfModules R) (free J) (free (I ⊕ J))) (coprod.inr ≫ Iso.hom (freeSumIso I J))
    (CategoryTheory.Functor.map freeFunctor (↾Sum.inr))

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_hom
    (coprodIsCoprod (free (R := R) I) (free J)) _ (.mk .right)

Premises used: CategoryTheory.Limits.coprodIsCoprod, CategoryTheory.Discrete.functor, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Limits.colimit, CategoryTheory.Discrete.mk, CategoryTheory.Limits.pair, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.colimit.desc, SheafOfModules.free, CategoryTheory.Limits.Sigma.map'
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J_1 : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J_1 RingCat
inst_1 : HasWeakSheafify J_1 AddCommGrpCat
inst_2 :
  J_1.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_3 :
  J_1.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
I J : Type u
⊢ Eq (α := Quiver.Hom (V := SheafOfModules R) (free J) (free (I ⊕ J))) (coprod.inr ≫ Iso.hom (freeSumIso I J))
    (CategoryTheory.Functor.map freeFunctor (↾Sum.inr))

Tactic:
exact IsColimit.comp_coconePointUniqueUpToIso_hom
    (coprodIsCoprod (free (R := R) I) (free J)) _ (.mk .right)

Premises used: CategoryTheory.Limits.coprodIsCoprod, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, SheafOfModules.free
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify J AddCommGrpCat
inst_2 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_3 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
C' : Type u₂
inst_4 : Category.{v₂, u₂} C'
J' : GrothendieckTopology.{v₂, u₂} C'
S : Sheaf J' RingCat
inst_5 : HasSheafify J' AddCommGrpCat
inst_6 :
  J'.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_7 :
  J'.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
F : SheafOfModules R ⥤ SheafOfModules S
I : Type u
η : unit S ⟶ F.obj (unit R)
i : I
⊢ Eq (α := unit S ⟶ F.obj (free I))
    (CategoryStruct.comp (Y := free I) (ιFree i : unit S ⟶ free I) (mapFree F I η : free I ⟶ F.obj (free I)))
    (η ≫ F.map (ιFree i))

Tactic:
IsColimit.ι_map (isColimitFreeCofan I) (F.mapCocone (freeCofan I))
    (Discrete.natTrans fun _ ↦ η) (Discrete.mk i)

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.Limits.IsColimit.ι_map, SheafOfModules.unit, CategoryTheory.Limits.colimit, CategoryTheory.Discrete.natTrans, SheafOfModules.freeCofan, CategoryTheory.Discrete.mk, SheafOfModules.free, SheafOfModules.isColimitFreeCofan, SheafOfModules.ιFree, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify J AddCommGrpCat
inst_2 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_3 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
C' : Type u₂
inst_4 : Category.{v₂, u₂} C'
J' : GrothendieckTopology.{v₂, u₂} C'
S : Sheaf J' RingCat
inst_5 : HasSheafify J' AddCommGrpCat
inst_6 :
  J'.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_7 :
  J'.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
F : SheafOfModules R ⥤ SheafOfModules S
I : Type u
inst_8 : PreservesColimitsOfShape (Discrete I) F
η : unit S ≅ F.obj (unit R)
⊢ Eq (α := free I ⟶ F.obj (free I)) (Iso.hom (mapFreeIso F I η) : free I ⟶ F.obj (free I))
    (mapFree F I η.hom : free I ⟶ F.obj (free I))

Tactic:
rfl

Premises used: SheafOfModules.mapFree, CategoryTheory.Discrete.natTrans, CategoryTheory.Limits.IsColimit.map, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify J AddCommGrpCat
inst_2 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_3 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
C' : Type u₂
inst_4 : Category.{v₂, u₂} C'
J' : GrothendieckTopology.{v₂, u₂} C'
S : Sheaf J' RingCat
inst_5 : HasSheafify J' AddCommGrpCat
inst_6 :
  J'.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_7 :
  J'.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
F : SheafOfModules R ⥤ SheafOfModules S
I : Type u
inst_8 : PreservesColimitsOfShape (Discrete I) F
η : unit S ≅ F.obj (unit R)
i : I
⊢ Eq (α := unit S ⟶ F.obj (free I))
    (CategoryStruct.comp (Y := free I) (ιFree i : unit S ⟶ free I)
      (Iso.hom (mapFreeIso F I η) : free I ⟶ F.obj (free I)))
    (η.hom ≫ F.map (ιFree i))

Tactic:
ιFree_mapFree _ _ _ _

Premises used: CategoryTheory.Discrete.natTrans, SheafOfModules.ιFree_mapFree
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify J AddCommGrpCat
inst_2 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_3 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
C' : Type u₂
inst_4 : Category.{v₂, u₂} C'
J' : GrothendieckTopology.{v₂, u₂} C'
S : Sheaf J' RingCat
inst_5 : HasSheafify J' AddCommGrpCat
inst_6 :
  J'.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_7 :
  J'.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
F : SheafOfModules R ⥤ SheafOfModules S
I : Type u
inst_8 : PreservesColimitsOfShape (Discrete I) F
η : unit S ≅ F.obj (unit R)
i : I
⊢ Eq (α := F.obj (unit R) ⟶ free I)
    (CategoryStruct.comp (Y := F.obj (free I)) (F.map (ιFree i)) (Iso.inv (mapFreeIso F I η)) : F.obj (unit R) ⟶ free I)
    (η.inv ≫ ιFree i : F.obj (unit R) ⟶ free I)

Tactic:
IsColimit.ι_map (isColimitOfPreserves F (isColimitFreeCofan I)) (freeCofan I)
    (Discrete.natTrans fun _ ↦ η.inv) (Discrete.mk i)

Premises used: CategoryTheory.Limits.IsColimit.ι_map, SheafOfModules.unit, CategoryTheory.Limits.colimit, CategoryTheory.Discrete.natTrans, SheafOfModules.freeCofan, CategoryTheory.Discrete.mk, SheafOfModules.free, SheafOfModules.isColimitFreeCofan, SheafOfModules.ιFree, CategoryTheory.Iso.inv, CategoryTheory.Limits.isColimitOfPreserves, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify J AddCommGrpCat
inst_2 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_3 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
M N P : SheafOfModules R
σ : M.GeneratingSections
p : M ⟶ N
inst_4 : Epi p
rw :
  Epi (X := free σ.I) (Y := N)
    ((Equiv.symm M.freeHomEquiv : (a : σ.I → M.sections) → free σ.I ⟶ M) σ.s ≫ p : free σ.I ⟶ N)
⊢ Epi (C := SheafOfModules R) (X := free σ.I) (Y := N)
    ((Equiv.symm N.freeHomEquiv : (a : σ.I → N.sections) → free σ.I ⟶ N) fun (i : σ.I) ↦ sectionsMap p (σ.s i))

Tactic:
rw [← freeHomEquiv_symm_comp]

Premises used: SheafOfModules.freeHomEquiv_symm_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify J AddCommGrpCat
inst_2 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_3 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
M N P : SheafOfModules R
σ : M.GeneratingSections
p : M ⟶ N
inst_4 : Epi p
⊢ Epi (X := free σ.I) (Y := N)
    ((Equiv.symm M.freeHomEquiv : (a : σ.I → M.sections) → free σ.I ⟶ M) σ.s ≫ p : free σ.I ⟶ N)

Tactic:
apply epi_comp

Premises used: CategoryTheory.epi_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify J AddCommGrpCat
inst_2 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_3 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
M : SheafOfModules R
σ : M.GeneratingSections
⊢ σ.ofEpi (𝟙 M) = σ

Tactic:
rfl

Premises used: PresheafOfModules.sectionsMk, PresheafOfModules.sectionsMap, SheafOfModules.GeneratingSections.ofEpi, rfl, PresheafOfModules.sections
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify J AddCommGrpCat
inst_2 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_3 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
M N P : SheafOfModules R
σ : M.GeneratingSections
p : M ⟶ N
q : N ⟶ P
inst_4 : Epi p
inst_5 : Epi q
⊢ σ.ofEpi (p ≫ q) = (σ.ofEpi p).ofEpi q

Tactic:
rfl

Premises used: PresheafOfModules.sectionsMap, SheafOfModules.GeneratingSections.ofEpi, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify J AddCommGrpCat
inst_2 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_3 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
M N : SheafOfModules R
σ : M.GeneratingSections
p : M ⟶ N
inst_4 : Epi p
⊢ (σ.ofEpi p).π = σ.π ≫ p

Tactic:
simp [ofEpi, freeHomEquiv_symm_comp]

Premises used: SheafOfModules.freeHomEquiv_symm_comp, SheafOfModules.GeneratingSections.ofEpi
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify J AddCommGrpCat
inst_2 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_3 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
M N P : SheafOfModules R
e : M ≅ N
σ : M.GeneratingSections
⊢ (σ.ofEpi e.hom).ofEpi e.inv = σ

Tactic:
simp only [← opEpi_comp, e.hom_inv_id, opEpi_id]

Premises used: SheafOfModules.GeneratingSections.opEpi_comp, CategoryTheory.Iso.hom_inv_id, SheafOfModules.GeneratingSections.opEpi_id
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify J AddCommGrpCat
inst_2 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_3 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
M N P : SheafOfModules R
e : M ≅ N
σ : N.GeneratingSections
⊢ (σ.ofEpi e.inv).ofEpi e.hom = σ

Tactic:
simp only [← opEpi_comp, e.inv_hom_id, opEpi_id]

Premises used: CategoryTheory.Iso.inv_hom_id, SheafOfModules.GeneratingSections.opEpi_comp, SheafOfModules.GeneratingSections.opEpi_id