mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f c.inl h i
hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY c.inl
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))
hc₃ :
  IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inl (pullback.snd αY c.inr) αZ
    (BinaryCofan.mk (c.inr ≫ i) h).inl
hc₄✝ :
  IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inr αX αZ
    (BinaryCofan.mk (c.inr ≫ i) h).inr
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY ⋯
e₁ : (g' ≫ cmp) ≫ pullback.snd αZ i = αW ≫ c.inl
e₂ : (pullback.fst αY c.inr ≫ cmp) ≫ pullback.snd αZ i = pullback.snd αY c.inr ≫ c.inr
hc₄ : IsColimit (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))
this : cmp = (hc₂.coconePointUniqueUpToIso hc₄).hom
⊢ i' ≫ 𝟙 Z' = (hc₂.coconePointUniqueUpToIso hc₄).hom ≫ pullback.fst αZ i

Tactic:
← this,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f c.inl h i
hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY c.inl
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))
hc₃ :
  IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inl (pullback.snd αY c.inr) αZ
    (BinaryCofan.mk (c.inr ≫ i) h).inl
hc₄✝ :
  IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inr αX αZ
    (BinaryCofan.mk (c.inr ≫ i) h).inr
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY ⋯
e₁ : (g' ≫ cmp) ≫ pullback.snd αZ i = αW ≫ c.inl
e₂ : (pullback.fst αY c.inr ≫ cmp) ≫ pullback.snd αZ i = pullback.snd αY c.inr ≫ c.inr
hc₄ : IsColimit (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))
this : cmp = (hc₂.coconePointUniqueUpToIso hc₄).hom
⊢ i' ≫ 𝟙 Z' = cmp ≫ pullback.fst αZ i
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case e'_8.e
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
e_3✝ :
  (∐ fun p ↦ pullback (f p.1) (g p.2)) =
    (Cofan.mk (∐ fun p ↦ pullback (f p.1) (g p.2)) (Sigma.ι fun p ↦ pullback (f p.1) (g p.2))).pt
e_5✝ : ∐ Y = (Cofan.mk (∐ Y) fun i ↦ Sigma.ι Y i).pt
⊢ @Sigma.desc (ι × ι') C inst✝⁴ (fun p ↦ pullback (f p.1) (g p.2)) ⋯ =
    @Cofan.IsColimit.desc (ι × ι') C inst✝⁴ (fun b ↦ pullback (f b.1) (g b.2))
      (Cofan.mk (∐ fun p ↦ pullback (f p.1) (g p.2)) (Sigma.ι fun p ↦ pullback (f p.1) (g p.2)))
      (coproductIsCoproduct fun p ↦ pullback (f p.1) (g p.2))

pp: case convert_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
⊢ IsUniversalColimit (Cofan.mk (∐ X) fun i ↦ Sigma.ι X i)

pp: case convert_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
⊢ IsUniversalColimit (Cofan.mk (∐ Y) fun i ↦ Sigma.ι Y i)

Tactic:
· ext
    simp [Cofan.IsColimit.desc, Sigma.ι, coproductIsCoproduct]

Goal state after:
case convert_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
⊢ IsUniversalColimit (Cofan.mk (∐ X) fun i ↦ Sigma.ι X i)

case convert_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
⊢ IsUniversalColimit (Cofan.mk (∐ Y) fun i ↦ Sigma.ι Y i)
Module: Mathlib.CategoryTheory.Sites.LeftExact

Goal state before:
pp: case refine_2
C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹¹ : Category.{t, w} D
inst✝¹⁰ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁸ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁷ : ConcreteCategory D FD
inst✝⁶ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁵ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type t
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : Cᵒᵖ
⊢ ∀ (s : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X))
    (m : s.pt ⟶ ((J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X).mapCone (limit.cone F)).pt),
    (∀ (j : K), m ≫ ((J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X).mapCone (limit.cone F)).π.app j = s.π.app j) →
      m = liftToPlusObjLimitObj F (unop X) s

Tactic:
· intro S m hm
    dsimp [liftToPlusObjLimitObj]
    simp_rw [← Category.assoc, Iso.eq_comp_inv, ← Iso.comp_inv_eq]
    refine limit.hom_ext (fun k => ?_)
    simp only [limit.lift_π, Category.assoc, ← hm]
    congr 1
    refine colimit.hom_ext (fun k => ?_)
    dsimp [plusMap, plusObj]
    erw [colimit.ι_map, colimit.ι_desc_assoc, limit.lift_π]
    conv_lhs => dsimp
    simp only [Category.assoc]
    rw [ι_colimitLimitIso_limit_π_assoc]
    simp only [colimitObjIsoColimitCompEvaluation_ι_app_hom]
    conv_lhs =>
      dsimp [IsLimit.conePointUniqueUpToIso]
    rw [← Category.assoc, ← NatTrans.comp_app, limit.lift_π]
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : G.Full
inst✝ : G.Faithful
X Y : C
f : X ⟶ Y
this : G.map (F.map f) ≫ adj.counit.app Y = adj.counit.app X ≫ f
⊢ isColocal (fun x ↦ x ∈ Set.range G.obj) (adj.counit.app X ≫ f) ↔ IsIso (F.map f)

Tactic:
← this,

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : G.Full
inst✝ : G.Faithful
X Y : C
f : X ⟶ Y
this : G.map (F.map f) ≫ adj.counit.app Y = adj.counit.app X ≫ f
⊢ isColocal (fun x ↦ x ∈ Set.range G.obj) (G.map (F.map f) ≫ adj.counit.app Y) ↔ IsIso (F.map f)
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S : C
ι : Type u_2
inst✝ : Small.{max w v, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan fun i ↦ uliftYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
e : (Discrete.functor fun i ↦ uliftYoneda.{w, v, u}.obj (X i)) ≅
  Discrete.functor fun i ↦ shrinkYoneda.{max w v, v, u}.obj (X i) :=
  Discrete.natIso fun i ↦ uliftYonedaIsoShrinkYoneda.app (X i.as)
hc' : IsColimit ((Cocone.precompose e.inv).obj c) := (IsColimit.precomposeInvEquiv e c).invFun hc
this :
  (Cofan.IsColimit.desc hc fun i ↦ uliftYoneda.{w, v, u}.map (f i)) ≫ uliftYonedaIsoShrinkYoneda.hom.app S =
    Cofan.IsColimit.desc hc' fun i ↦ shrinkYoneda.{max v w, v, u}.map (f i)
⊢ Presheaf.IsLocallySurjective J (Cofan.IsColimit.desc hc' fun i ↦ shrinkYoneda.{max w v, v, u}.map (f i)) ↔
    Presheaf.IsLocallySurjective J (Cofan.IsColimit.desc hc fun i ↦ uliftYoneda.{w, v, u}.map (f i))

Tactic:
← this,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S : C
ι : Type u_2
inst✝ : Small.{max w v, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan fun i ↦ uliftYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
e : (Discrete.functor fun i ↦ uliftYoneda.{w, v, u}.obj (X i)) ≅
  Discrete.functor fun i ↦ shrinkYoneda.{max w v, v, u}.obj (X i) :=
  Discrete.natIso fun i ↦ uliftYonedaIsoShrinkYoneda.app (X i.as)
hc' : IsColimit ((Cocone.precompose e.inv).obj c) := (IsColimit.precomposeInvEquiv e c).invFun hc
this :
  (Cofan.IsColimit.desc hc fun i ↦ uliftYoneda.{w, v, u}.map (f i)) ≫ uliftYonedaIsoShrinkYoneda.hom.app S =
    Cofan.IsColimit.desc hc' fun i ↦ shrinkYoneda.{max v w, v, u}.map (f i)
⊢ Presheaf.IsLocallySurjective J
      ((Cofan.IsColimit.desc hc fun i ↦ uliftYoneda.{w, v, u}.map (f i)) ≫ uliftYonedaIsoShrinkYoneda.hom.app S) ↔
    Presheaf.IsLocallySurjective J (Cofan.IsColimit.desc hc fun i ↦ uliftYoneda.{w, v, u}.map (f i))
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: case x
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
Y : C
r₀ r₀' : ↑(R₀.obj (Opposite.op Y))
m₀ m₀' : ↑(M₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀'
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀'
⊢ Presheaf.equalizerSieve r₀ r₀' ⊓ Presheaf.equalizerSieve m₀ m₀' ∈ J (Opposite.unop (Opposite.op Y))

pp: case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
Y : C
r₀ r₀' : ↑(R₀.obj (Opposite.op Y))
m₀ m₀' : ↑(M₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀'
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀'
⊢ ∀ (Y_1 : C) (f : Y_1 ⟶ Opposite.unop (Opposite.op Y)),
    (Presheaf.equalizerSieve r₀ r₀' ⊓ Presheaf.equalizerSieve m₀ m₀').arrows f →
      (ConcreteCategory.hom (A.map f.op)) ((ConcreteCategory.hom (φ.app (Opposite.op Y))) (r₀ • m₀)) =
        (ConcreteCategory.hom (A.map f.op)) ((ConcreteCategory.hom (φ.app (Opposite.op Y))) (r₀' • m₀'))

Tactic:
· apply J.intersection_covering
    · exact Presheaf.equalizerSieve_mem J α _ _ hr₀
    · exact Presheaf.equalizerSieve_mem J φ _ _ hm₀

Goal state after:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
Y : C
r₀ r₀' : ↑(R₀.obj (Opposite.op Y))
m₀ m₀' : ↑(M₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀'
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀'
⊢ ∀ (Y_1 : C) (f : Y_1 ⟶ Opposite.unop (Opposite.op Y)),
    (Presheaf.equalizerSieve r₀ r₀' ⊓ Presheaf.equalizerSieve m₀ m₀').arrows f →
      (ConcreteCategory.hom (A.map f.op)) ((ConcreteCategory.hom (φ.app (Opposite.op Y))) (r₀ • m₀)) =
        (ConcreteCategory.hom (A.map f.op)) ((ConcreteCategory.hom (φ.app (Opposite.op Y))) (r₀' • m₀'))
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification

Goal state before:
pp: C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
P₀ Q₀ : PresheafOfModules R₀
N : SheafOfModules R
f : P₀ ⟶ Q₀
g : Q₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj N
⊢ (SheafOfModules.toSheaf R).map ((sheafificationHomEquiv α).symm (f ≫ g)) =
    (SheafOfModules.toSheaf R).map ((sheafification α).map f) ≫
      (SheafOfModules.toSheaf R).map ((sheafificationHomEquiv α).symm g)

Tactic:
rw [toSheaf_map_sheafificationHomEquiv_symm α (f ≫ g),
          toSheaf_map_sheafificationHomEquiv_symm α g, Functor.map_comp]

Goal state after:
C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
P₀ Q₀ : PresheafOfModules R₀
N : SheafOfModules R
f : P₀ ⟶ Q₀
g : Q₀ ⟶ (SheafOfModules.forget R ⋙ restrictScalars α).obj N
⊢ ((CategoryTheory.sheafificationAdjunction J AddCommGrpCat).homEquiv P₀.presheaf
          ((SheafOfModules.toSheaf R).obj N)).symm
      ((toPresheaf R₀).map f ≫ (toPresheaf R₀).map g) =
    (SheafOfModules.toSheaf R).map ((sheafification α).map f) ≫
      ((CategoryTheory.sheafificationAdjunction J AddCommGrpCat).homEquiv Q₀.presheaf
            ((SheafOfModules.toSheaf R).obj N)).symm
        ((toPresheaf R₀).map g)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
X : C
r : ↑(R.obj (Opposite.op X))
m : ↑(A.obj (Opposite.op X))
P : Presieve X
r₀ : FamilyOfElements (R₀ ⋙ forget RingCat) P
m₀ : FamilyOfElements (M₀.presheaf ⋙ forget Ab) P
hr₀ : (r₀.map (whiskerRight α (forget RingCat))).IsAmalgamation r
hm₀ : (m₀.map (whiskerRight φ (forget Ab))).IsAmalgamation m
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : P f₁
h₂ : P f₂
fac : g₁ ≫ f₁ = g₂ ≫ f₂
a₁ : (R₀ ⋙ forget RingCat).obj (Opposite.op Y₁) := r₀ f₁ h₁
b₁ : (M₀.presheaf ⋙ forget Ab).obj (Opposite.op Y₁) := m₀ f₁ h₁
a₂ : (R₀ ⋙ forget RingCat).obj (Opposite.op Y₂) := r₀ f₂ h₂
b₂ : (M₀.presheaf ⋙ forget Ab).obj (Opposite.op Y₂) := m₀ f₂ h₂
a₀ : ↑(R₀.obj (Opposite.op Z)) := (ConcreteCategory.hom (R₀.map g₁.op)) a₁
b₀ : ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R₀.map g₁.op))).obj (M₀.obj (Opposite.op Z))) :=
  (ConcreteCategory.hom (M₀.map g₁.op)) b₁
ha₁ : (ConcreteCategory.hom (α.app (Opposite.op Y₁))) a₁ = (ConcreteCategory.hom (R.map f₁.op)) r
ha₂ : (ConcreteCategory.hom (α.app (Opposite.op Y₂))) a₂ = (ConcreteCategory.hom (R.map f₂.op)) r
hb₁ : (ConcreteCategory.hom (φ.app (Opposite.op Y₁))) b₁ = (ConcreteCategory.hom (A.map f₁.op)) m
hb₂ : (ConcreteCategory.hom (φ.app (Opposite.op Y₂))) b₂ = (ConcreteCategory.hom (A.map f₂.op)) m
ha₀ : (ConcreteCategory.hom (α.app (Opposite.op Z))) a₀ = (ConcreteCategory.hom (R.map (f₁.op ≫ g₁.op))) r
hb₀ : (ConcreteCategory.hom (φ.app (Opposite.op Z))) b₀ = (ConcreteCategory.hom (A.map (f₁.op ≫ g₁.op))) m
⊢ (ConcreteCategory.hom (α.app (Opposite.op Z))) a₀ = (ConcreteCategory.hom (R.map (f₂.op ≫ g₂.op))) r

Tactic:
rw [ha₀, ← op_comp, fac, op_comp]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
m : ↑(A.obj.obj X)
⊢ smul α φ 1 m = m

Tactic:
apply A.isSeparated _ _ (Presheaf.imageSieve_mem J φ m)

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
m : ↑(A.obj.obj X)
⊢ ∀ (Y : C) (f : Y ⟶ Opposite.unop X),
    (Presheaf.imageSieve φ m).arrows f →
      (ConcreteCategory.hom (A.obj.map f.op)) (smul α φ 1 m) = (ConcreteCategory.hom (A.obj.map f.op)) m
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
m : ↑(A.obj.obj X)
⊢ smul α φ 0 m = 0

Tactic:
apply A.isSeparated _ _ (Presheaf.imageSieve_mem J φ m)

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
m : ↑(A.obj.obj X)
⊢ ∀ (Y : C) (f : Y ⟶ Opposite.unop X),
    (Presheaf.imageSieve φ m).arrows f →
      (ConcreteCategory.hom (A.obj.map f.op)) (smul α φ 0 m) = (ConcreteCategory.hom (A.obj.map f.op)) 0
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y✝ : Cᵒᵖ
π : X ⟶ Y✝
r : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop Y✝) :=
  Presheaf.imageSieve α ((ConcreteCategory.hom (R.obj.map π)) r) ⊓
    Presheaf.imageSieve φ ((ConcreteCategory.hom (A.obj.map π)) m)
hS : S ∈ J (Opposite.unop Y✝)
Y : C
f : Y ⟶ Opposite.unop Y✝
r₀ : ToType (R₀.obj (Opposite.op Y))
hr₀ :
  (RingCat.Hom.hom (α.app (Opposite.op Y))) r₀ = (RingCat.Hom.hom (R.obj.map f.op)) ((RingCat.Hom.hom (R.obj.map π)) r)
m₀ : ToType (M₀.presheaf.obj (Opposite.op Y))
hm₀ :
  (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ =
    (ConcreteCategory.hom (A.obj.map f.op)) ((ConcreteCategory.hom (A.obj.map π)) m)
⊢ (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.obj.map (π ≫ f.op))) r

Tactic:
by rw [hr₀, Functor.map_comp, RingCat.comp_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : RepresentablyFlat F
inst✝ : RepresentablyFlat G
X : E
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
H : J ⥤ StructuredArrow X (F ⋙ G)
c₁ : Cone (H ⋙ StructuredArrow.pre X F G)
H₂ : J ⥤ StructuredArrow c₁.pt.right F :=
  { obj := fun j ↦ StructuredArrow.mk (StructuredArrow.Hom.right (c₁.π.app j)),
    map := fun {j j'} f ↦ StructuredArrow.homMk (StructuredArrow.Hom.right (H.map f)) ⋯, map_id := ⋯, map_comp := ⋯ }
c₂ :
  Cone
    { obj := fun j ↦ StructuredArrow.mk (StructuredArrow.Hom.right (c₁.π.app j)),
      map := fun {j j'} f ↦ StructuredArrow.homMk (StructuredArrow.Hom.right (H.map f)) ⋯, map_id := ⋯, map_comp := ⋯ }
⊢ Nonempty (Cone H)

Tactic:
exact ⟨⟨StructuredArrow.mk (c₁.pt.hom ≫ G.map c₂.pt.hom),
    ⟨fun j => StructuredArrow.homMk (c₂.π.app j).right (by simp [← G.map_comp]),
     fun j j' f => by simpa using (c₂.w f).symm⟩⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
hS : J₁.IsClosed S
Z : C
g : Z ⟶ Y
hg : J₁.Covers (Sieve.pullback f S) g
⊢ J₁.Covers S (g ≫ f)

Tactic:
rwa [J₁.covers_iff, Sieve.pullback_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
j k : Bicone J
⊢ Fintype (j ⟶ k)

Tactic:
cases j <;> cases k
  · exact
      { elems := {BiconeHom.left_id}
        complete := fun f => by cases f; simp }
  · exact
    { elems := ∅
      complete := fun f => by cases f }
  · exact
    { elems := {BiconeHom.left _}
      complete := fun f => by cases f; simp }
  · exact
    { elems := ∅
      complete := fun f => by cases f }
  · exact
      { elems := {BiconeHom.right_id}
        complete := fun f => by cases f; simp }
  · exact
    { elems := {BiconeHom.right _}
      complete := fun f => by cases f; simp }
  · exact
    { elems := ∅
      complete := fun f => by cases f }
  · exact
    { elems := ∅
      complete := fun f => by cases f }
  · exact
    { elems := Finset.image BiconeHom.diagram Fintype.elems
      complete := fun f => by
        rcases f with (_ | _ | _ | _ | f)
        simp only [Finset.mem_image]
        use f
        simpa using Fintype.complete _ }

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
⊢ Presieve.ofArrows (E.sum F).X (E.sum F).f ≤ Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f

Tactic:
intro Z g ⟨i⟩
    cases i
    · exact Or.inl (.mk _)
    · exact Or.inr (.mk _)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
T : C
f : T ⟶ S
⊢ (E.add f).presieve₀ = E.presieve₀ ⊔ Presieve.singleton f

Tactic:
simp [add, presieve₀_reindex, presieve₀_sum]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
f : E.Hom F
⊢ E.sieve₀ ≤ F.sieve₀

Tactic:
rw [Sieve.generate_le_iff, Presieve.ofArrows_le_iff]
  intro i
  rw [← f.w₀ i]
  apply Sieve.downward_closed
  exact Sieve.le_generate _ _ _ ⟨f.s₀ i⟩

Goal state after: