awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R R' : CategoryTheory.Functor.{v', u, u', u + 1} Cᵒᵖ RingCat
α : R ⟶ R'
M₁ M₂ : PresheafOfModules.{v, v', u', u} R'
hM₂ : Presheaf.IsSheaf J M₂.presheaf
inst_1 :
  Presheaf.IsLocallySurjective J (FA := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CA :=
    RingCat.carrier) α
g : (restrictScalars α).obj M₁ ⟶ (restrictScalars α).obj M₂
X : Cᵒᵖ
r' : (↑(R'.obj X) : Type u)
m : (↑(M₁.obj X) : Type v)
a :
  ∀ (Y : C) (f : Y ⟶ Opposite.unop X),
    (Presheaf.imageSieve (FA := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CA := RingCat.carrier) α
            r').arrows
        f →
      Eq (α := (↑(M₂.presheaf.obj (Opposite.op Y)) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) (M₂.presheaf.map f.op) :
              (a : (↑(M₂.presheaf.obj (Opposite.op (Opposite.unop X))) : Type v)) →
                (↑(M₂.presheaf.obj (Opposite.op Y)) : Type v))
            ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                    AddCommGrpCat.carrier) (((toPresheaf R).map g).app X) :
                  (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v))
                (r' • m) :
              (↑(M₂.presheaf.obj X) : Type v)) :
          (↑(M₂.presheaf.obj (Opposite.op Y)) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) (M₂.presheaf.map f.op) :
              (a : (↑(M₂.presheaf.obj (Opposite.op (Opposite.unop X))) : Type v)) →
                (↑(M₂.presheaf.obj (Opposite.op Y)) : Type v))
            (HSMul.hSMul (β := (↑(M₂.presheaf.obj X) : Type v)) r'
              ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                      AddCommGrpCat.carrier) (((toPresheaf R).map g).app X) :
                    (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v))
                  m :
                (↑(M₂.presheaf.obj X) : Type v))) :
          (↑(M₂.presheaf.obj (Opposite.op Y)) : Type v))
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier) (((toPresheaf R).map g).app X) :
        (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v))
      (r' • m) =
    HSMul.hSMul (β := (↑(M₂.presheaf.obj X) : Type v)) r'
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              AddCommGrpCat.carrier) (((toPresheaf R).map g).app X) :
            (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v))
          m :
        (↑(M₂.presheaf.obj X) : Type v))

Tactic:
apply hM₂.isSeparated _ _ (Presheaf.imageSieve_mem J α r')

Premises used: CategoryTheory.Presheaf.IsSheaf.isSeparated, CategoryTheory.Presheaf.imageSieve_mem
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits
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.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CA := AddCommGrpCat.carrier)
K : Type w
inst_3 : Category.{w', w} K
inst_4 : HasColimitsOfShape K (PresheafOfModules.{v, v', u', u} (R.obj (P := Presheaf.IsSheaf J)))
F : K ⥤ SheafOfModules.{v, v', u', u} R
e : F ≅ (F ⋙ forget R) ⋙ PresheafOfModules.sheafification (𝟙 (R.obj (P := Presheaf.IsSheaf J))) :=
  F.isoWhiskerLeft
    (Iso.symm
      (asIso (Adjunction.counit (PresheafOfModules.sheafificationAdjunction (𝟙 (R.obj (P := Presheaf.IsSheaf J)))))))
⊢ HasColimit F

Tactic:
hasColimit_of_iso e

Premises used: CategoryTheory.Limits.hasColimit_of_iso
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits
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.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CA := AddCommGrpCat.carrier)
K : Type w
inst_3 : Category.{w', w} K
inst_4 : HasColimitsOfShape K (PresheafOfModules.{v, v', u', u} (R.obj (P := Presheaf.IsSheaf J)))
F : K ⥤ SheafOfModules.{v, v', u', u} R
e : F ≅ (F ⋙ forget R) ⋙ PresheafOfModules.sheafification (𝟙 (R.obj (P := Presheaf.IsSheaf J))) :=
  F.isoWhiskerLeft
    (Iso.symm
      (asIso (Adjunction.counit (PresheafOfModules.sheafificationAdjunction (𝟙 (R.obj (P := Presheaf.IsSheaf J)))))))
⊢ HasColimit F

Tactic:
exact hasColimit_of_iso e

Premises used: CategoryTheory.Limits.hasColimit_of_iso
-- 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))
I : Type u
i : I
⊢ Eq (α := unit R ⟶ Cocone.pt (F := Discrete.functor fun (x : I) ↦ unit R) (freeCofan I))
    (Cofan.inj (C := SheafOfModules R) (f := fun (x : I) ↦ unit R) (freeCofan I) i :
      unit R ⟶ Cocone.pt (F := Discrete.functor fun (x : I) ↦ unit R) (freeCofan I))
    (ιFree i : unit R ⟶ free I)

Tactic:
rfl

Premises used: SheafOfModules.ιFree, rfl, 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))
M : SheafOfModules R
I : Type u
s : free I ⟶ M
i : I
⊢ CategoryStruct.comp (Y := Cocone.pt (F := Discrete.functor fun (x : I) ↦ unit R) (freeCofan I))
      (Cofan.inj (C := SheafOfModules R) (f := fun (x : I) ↦ unit R) (freeCofan I) i)
      ((fun (s : I → M.sections) ↦
          (Cofan.IsColimit.desc (isColimitFreeCofan I) fun (i : I) ↦
              (Equiv.symm M.unitHomEquiv : (a : M.sections) → unit R ⟶ M) (s i) :
            Cocone.pt (F := Discrete.functor fun (x : I) ↦ unit R) (freeCofan I) ⟶ M))
        ((fun (f : free I ⟶ M) (i : I) ↦ ((M.unitHomEquiv : (a : unit R ⟶ M) → M.sections) (ιFree i ≫ f) : M.sections))
          s)) =
    Cofan.inj (C := SheafOfModules R) (f := fun (x : I) ↦ unit R) (freeCofan I) i ≫ s

Tactic:
simp [← freeCofan_inj]

Premises used: SheafOfModules.freeCofan_inj
-- 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))
M : SheafOfModules R
I : Type u
f : I → M.sections
h :
  ∀ (i : I),
    (fun (f : free I ⟶ M) (i : I) ↦ ((M.unitHomEquiv : (a : unit R ⟶ M) → M.sections) (ιFree i ≫ f) : M.sections))
        ((fun (s : I → M.sections) ↦
            (Cofan.IsColimit.desc (isColimitFreeCofan I) fun (i : I) ↦
                (Equiv.symm M.unitHomEquiv : (a : M.sections) → unit R ⟶ M) (s i) :
              Cocone.pt (F := Discrete.functor fun (x : I) ↦ unit R) (freeCofan I) ⟶ M))
          f)
        i =
      f i
⊢ (fun (f : free I ⟶ M) (i : I) ↦ ((M.unitHomEquiv : (a : unit R ⟶ M) → M.sections) (ιFree i ≫ f) : M.sections))
      ((fun (s : I → M.sections) ↦
          (Cofan.IsColimit.desc (isColimitFreeCofan I) fun (i : I) ↦
              (Equiv.symm M.unitHomEquiv : (a : M.sections) → unit R ⟶ M) (s i) :
            Cocone.pt (F := Discrete.functor fun (x : I) ↦ unit R) (freeCofan I) ⟶ M))
        f) =
    f

Tactic:
ext1 i
-- 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))
M : SheafOfModules R
I : Type u
f : I → M.sections
i : I
⊢ (fun (f : free I ⟶ M) (i : I) ↦ ((M.unitHomEquiv : (a : unit R ⟶ M) → M.sections) (ιFree i ≫ f) : M.sections))
      ((fun (s : I → M.sections) ↦
          (Cofan.IsColimit.desc (isColimitFreeCofan I) fun (i : I) ↦
              (Equiv.symm M.unitHomEquiv : (a : M.sections) → unit R ⟶ M) (s i) :
            Cocone.pt (F := Discrete.functor fun (x : I) ↦ unit R) (freeCofan I) ⟶ M))
        f)
      i =
    f i

Tactic:
simp [← freeCofan_inj]

Premises used: SheafOfModules.freeCofan_inj
-- 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))
M N : SheafOfModules R
I : Type u
f : free I ⟶ M
p : M ⟶ N
i : I
⊢ (N.freeHomEquiv : (a : free I ⟶ N) → I → N.sections) (f ≫ p) i =
    sectionsMap p ((M.freeHomEquiv : (a : free I ⟶ M) → I → M.sections) f i)

Tactic:
rfl

Premises used: PresheafOfModules.sectionsMk, PresheafOfModules.sectionsMap, 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))
M N : SheafOfModules R
I : Type u
s : I → M.sections
p : M ⟶ N
h :
  ∀ (x : I) (X : Cᵒᵖ),
    Eq.{u + 1} (α :=
      (N.val.presheaf ⋙
            CategoryTheory.forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier)).obj
        X)
      ((↑((N.freeHomEquiv : (a : free I ⟶ N) → I → N.sections)
              ((Equiv.symm M.freeHomEquiv : (a : I → M.sections) → free I ⟶ M) s ≫ p : free I ⟶ N) x) :
          (j : Cᵒᵖ) → (N.val.presheaf ⋙ CategoryTheory.forget Ab).obj j)
        X)
      ((↑((N.freeHomEquiv : (a : free I ⟶ N) → I → N.sections)
              ((Equiv.symm N.freeHomEquiv : (a : I → N.sections) → free I ⟶ N) fun (i : I) ↦ sectionsMap p (s i)) x) :
          (j : Cᵒᵖ) → (N.val.presheaf ⋙ CategoryTheory.forget Ab).obj j)
        X)
⊢ Eq (α := I → N.sections)
    ((N.freeHomEquiv : (a : free I ⟶ N) → I → N.sections)
        ((Equiv.symm M.freeHomEquiv : (a : I → M.sections) → free I ⟶ M) s ≫ p : free I ⟶ N) :
      I → N.sections)
    ((N.freeHomEquiv : (a : free I ⟶ N) → I → N.sections)
        ((Equiv.symm N.freeHomEquiv : (a : I → N.sections) → free I ⟶ N) fun (i : I) ↦ sectionsMap p (s i)) :
      I → N.sections)

Tactic:
ext
-- 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))
M N : SheafOfModules R
I : Type u
s : I → M.sections
p : M ⟶ N
x : I
X : Cᵒᵖ
⊢ Eq.{u + 1} (α :=
    (N.val.presheaf ⋙
          CategoryTheory.forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier)).obj
      X)
    ((↑((N.freeHomEquiv : (a : free I ⟶ N) → I → N.sections)
            ((Equiv.symm M.freeHomEquiv : (a : I → M.sections) → free I ⟶ M) s ≫ p : free I ⟶ N) x) :
        (j : Cᵒᵖ) → (N.val.presheaf ⋙ CategoryTheory.forget Ab).obj j)
      X)
    ((↑((N.freeHomEquiv : (a : free I ⟶ N) → I → N.sections)
            ((Equiv.symm N.freeHomEquiv : (a : I → N.sections) → free I ⟶ N) fun (i : I) ↦ sectionsMap p (s i)) x) :
        (j : Cᵒᵖ) → (N.val.presheaf ⋙ CategoryTheory.forget Ab).obj j)
      X)

Tactic:
simp [freeHomEquiv_comp_apply]

Premises used: SheafOfModules.freeHomEquiv_comp_apply
-- 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))
M : SheafOfModules R
I : Type u
f : free I ⟶ M
i : I
⊢ (M.freeHomEquiv : (a : free I ⟶ M) → I → M.sections) f i = sectionsMap f (freeSection i)

Tactic:
rfl

Premises used: PresheafOfModules.sectionsMk, PresheafOfModules.sectionsMap, 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))
I : Type u
M : SheafOfModules R
f : free I ⟶ M
i : I
⊢ (Equiv.symm M.unitHomEquiv : (a : M.sections) → unit R ⟶ M)
      ((M.freeHomEquiv : (a : free I ⟶ M) → I → M.sections) f i) =
    ιFree i ≫ f

Tactic:
simp [freeHomEquiv]

Premises used: SheafOfModules.freeHomEquiv
-- 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
f : I → J
simp :
  Eq (α := Quiver.Hom (V := SheafOfModules R) (free I) (free J)) (freeMap f)
    ((Equiv.symm (freeHomEquiv (free J)) : (a : I → (free J).sections) → free I ⟶ free J) (freeSection ∘ f))
⊢ Eq (α := Quiver.Hom (V := SheafOfModules R) (free I) (free J))
    ((Equiv.symm (freeHomEquiv (free J)) : (a : I → (free J).sections) → free I ⟶ free J)
        ((freeHomEquiv (free J) : (a : free I ⟶ free J) → I → (free J).sections) (freeMap f)) :
      Quiver.Hom (V := SheafOfModules R) (free I) (free J))
    ((Equiv.symm (freeHomEquiv (free J)) : (a : I → (free J).sections) → free I ⟶ free J) (freeSection ∘ f) :
      Quiver.Hom (V := SheafOfModules R) (free I) (free J))

Tactic:
simp
-- 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
f : I → J
⊢ Eq (α := Quiver.Hom (V := SheafOfModules R) (free I) (free J)) (freeMap f)
    ((Equiv.symm (freeHomEquiv (free J)) : (a : I → (free J).sections) → free I ⟶ free J) (freeSection ∘ f))

Tactic:
rfl
-- 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
f : I → J
i : I
⊢ Eq (α := sections.{u, v₁, u₁, u} (C := C) (J := J_1) (R := R) (free J)) (sectionsMap (freeMap f) (freeSection i))
    (freeSection (f i))

Tactic:
simp [← freeHomEquiv_comp_apply]

Premises used: SheafOfModules.freeHomEquiv_comp_apply
-- 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))
I : Type u
M : SheafOfModules R
f : I → M.sections
i : I
obtain :
  ∀ (f : free I ⟶ M),
    Eq (α := M.sections)
      (sectionsMap (M := free I)
        ((Equiv.symm M.freeHomEquiv : (a : I → M.sections) → free I ⟶ M)
          ((M.freeHomEquiv : (a : free I ⟶ M) → I → M.sections) f))
        (freeSection i))
      ((M.freeHomEquiv : (a : free I ⟶ M) → I → M.sections) f i)
⊢ sectionsMap (M := free I) ((Equiv.symm M.freeHomEquiv : (a : I → M.sections) → free I ⟶ M) f) (freeSection i) = f i

Tactic:
obtain ⟨f, rfl⟩ := (freeHomEquiv M).surjective f

Premises used: SheafOfModules.freeHomEquiv, Equiv.surjective, rfl
-- 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
f : I → J
i : I
rw :
  Eq (α := unit R ⟶ free J)
    ((Equiv.symm (unitHomEquiv (free J)) : (a : (free J).sections) → unit R ⟶ free J) ((freeSection ∘ f) i) :
      unit R ⟶ free J)
    (ιFree (f i) : unit R ⟶ free J)
⊢ Eq (α := unit R ⟶ free J) (ιFree i ≫ freeMap f) (ιFree (f i))

Tactic:
rw [← unitHomEquiv_symm_freeHomEquiv_apply, freeHomEquiv_freeMap]

Premises used: SheafOfModules.freeHomEquiv_freeMap, SheafOfModules.unitHomEquiv_symm_freeHomEquiv_apply
-- 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
f : I → J
i : I
rw : Eq (α := unit R ⟶ free J) (ιFree (f i) ≫ 𝟙 (free J)) (ιFree (f i))
rw₁ rw₂ : Eq (α := unit R ⟶ free J) (ιFree (f i)) (ιFree (f i))
⊢ Eq (α := unit R ⟶ free J)
    ((Equiv.symm (unitHomEquiv (free J)) : (a : (free J).sections) → unit R ⟶ free J)
        ((freeHomEquiv (free J) : (a : free J ⟶ free J) → J → (free J).sections) (𝟙 (free J)) (f i)) :
      unit R ⟶ free J)
    (ιFree (f i) : unit R ⟶ free J)

Tactic:
rw [unitHomEquiv_symm_freeHomEquiv_apply, Category.comp_id]

Premises used: SheafOfModules.unitHomEquiv_symm_freeHomEquiv_apply, CategoryTheory.Category.comp_id
-- 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 : Type u
⊢ Eq (α := SheafOfModules R) (Functor.obj freeFunctor X) (free X)

Tactic:
rfl

Premises used: CategoryTheory.Limits.colimit, SheafOfModules.free, rfl