mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j)
O : Finset K := (Finset.univ.biUnion fun j ↦ Finset.univ.biUnion fun j' ↦ Finset.image kf Finset.univ) ∪ {k'}
kfO : ∀ {j j' : J} (f : j ⟶ j'), kf f ∈ O
k'O : k' ∈ O
H : Finset ((X : K) ×' (Y : K) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun j ↦
    Finset.univ.biUnion fun j' ↦
      Finset.univ.biUnion fun f ↦ {⟨k', ⟨kf f, ⟨k'O, ⟨⋯, gf f⟩⟩⟩⟩, ⟨k', ⟨kf f, ⟨k'O, ⟨⋯, hf f⟩⟩⟩⟩}
k'' : K
i' : {X : K} → X ∈ O → (X ⟶ k'')
s' : ∀ {X Y : K} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H → f ≫ i' mY = i' mX
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k'' := fun {j j'} f ↦ i' ⋯
j₁ j₂ j₃ j₄ : J
f : j₁ ⟶ j₂
f' : j₃ ⟶ j₄
⊢ gf f = gf f ∨ ⟨k', ⟨kf f, ⟨k'O, ⟨⋯, gf f⟩⟩⟩⟩ ∈ {⟨k', ⟨kf f, ⟨k'O, ⟨⋯, hf f⟩⟩⟩⟩}

Tactic:
Finset.mem_singleton,

Goal state after:
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j)
O : Finset K := (Finset.univ.biUnion fun j ↦ Finset.univ.biUnion fun j' ↦ Finset.image kf Finset.univ) ∪ {k'}
kfO : ∀ {j j' : J} (f : j ⟶ j'), kf f ∈ O
k'O : k' ∈ O
H : Finset ((X : K) ×' (Y : K) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun j ↦
    Finset.univ.biUnion fun j' ↦
      Finset.univ.biUnion fun f ↦ {⟨k', ⟨kf f, ⟨k'O, ⟨⋯, gf f⟩⟩⟩⟩, ⟨k', ⟨kf f, ⟨k'O, ⟨⋯, hf f⟩⟩⟩⟩}
k'' : K
i' : {X : K} → X ∈ O → (X ⟶ k'')
s' : ∀ {X Y : K} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H → f ≫ i' mY = i' mX
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k'' := fun {j j'} f ↦ i' ⋯
j₁ j₂ j₃ j₄ : J
f : j₁ ⟶ j₂
f' : j₃ ⟶ j₄
⊢ gf f = gf f ∨ ⟨k', ⟨kf f, ⟨k'O, ⟨⋯, gf f⟩⟩⟩⟩ = ⟨k', ⟨kf f, ⟨k'O, ⟨⋯, hf f⟩⟩⟩⟩
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: J : Type v'
inst✝⁵ : Category.{u', v'} J
C : Type u
inst✝⁴ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ : C
f✝ : W✝ ⟶ X✝
g✝ : W✝ ⟶ Y✝
h✝ : X✝ ⟶ Z✝
i✝ : Y✝ ⟶ Z✝
D : Type u''
inst✝³ : Category.{v'', u''} D
inst✝² : Adhesive C
inst✝¹ : HasPullbacks C
inst✝ : HasPushouts C
W X Y Z : D ⥤ C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
x : D
⊢ IsVanKampenColimit (((evaluation D C).obj x).mapCocone (PushoutCocone.mk h i ⋯))

Tactic:
refine (IsVanKampenColimit.precompose_isIso_iff (diagramIsoSpan _).inv).mp ?_

Goal state after:
J : Type v'
inst✝⁵ : Category.{u', v'} J
C : Type u
inst✝⁴ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ : C
f✝ : W✝ ⟶ X✝
g✝ : W✝ ⟶ Y✝
h✝ : X✝ ⟶ Z✝
i✝ : Y✝ ⟶ Z✝
D : Type u''
inst✝³ : Category.{v'', u''} D
inst✝² : Adhesive C
inst✝¹ : HasPullbacks C
inst✝ : HasPushouts C
W X Y Z : D ⥤ C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
x : D
⊢ IsVanKampenColimit
    ((Cocone.precompose (diagramIsoSpan (span f g ⋙ (evaluation D C).obj x)).inv).obj
      (((evaluation D C).obj x).mapCocone (PushoutCocone.mk h i ⋯)))
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u''
inst✝⁵ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁴ : Adhesive D
H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [Mono f], HasPullback f g
H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
inst✝³ : PreservesLimitsOfShape WalkingCospan F
inst✝² : ReflectsLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape WalkingSpan F
inst✝ : ReflectsColimitsOfShape WalkingSpan F
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
⊢ IsVanKampenColimit (F.mapCocone (PushoutCocone.mk h i ⋯))

Tactic:
refine (IsVanKampenColimit.precompose_isIso_iff (diagramIsoSpan _).inv).mp ?_

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u''
inst✝⁵ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁴ : Adhesive D
H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [Mono f], HasPullback f g
H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
inst✝³ : PreservesLimitsOfShape WalkingCospan F
inst✝² : ReflectsLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape WalkingSpan F
inst✝ : ReflectsColimitsOfShape WalkingSpan F
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
⊢ IsVanKampenColimit
    ((Cocone.precompose (diagramIsoSpan (span f g ⋙ F)).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯)))
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
D : Type u''
inst✝⁷ : Category.{v'', u''} D
inst✝⁶ : HasPullbacks D
inst✝⁵ : Adhesive C
inst✝⁴ : HasPullbacks C
inst✝³ : HasPushouts C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝² : Gr.Full
inst✝¹ : Gr.Faithful
inst✝ : PreservesLimitsOfShape WalkingCospan Gl
this✝ : PreservesColimitsOfSize.{?u.95, ?u.94, v, v'', u, u''} Gl
this : PreservesLimitsOfSize.{?u.102, ?u.101, v'', v, u'', u} Gr
⊢ Adhesive D

Tactic:
apply Adhesive.mk (hasPushout_of_mono_left := H₂)

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
D : Type u''
inst✝⁷ : Category.{v'', u''} D
inst✝⁶ : HasPullbacks D
inst✝⁵ : Adhesive C
inst✝⁴ : HasPullbacks C
inst✝³ : HasPushouts C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝² : Gr.Full
inst✝¹ : Gr.Faithful
inst✝ : PreservesLimitsOfShape WalkingCospan Gl
this✝ : PreservesColimitsOfSize.{?u.95, ?u.94, v, v'', u, u''} Gl
this : PreservesLimitsOfSize.{?u.102, ?u.101, v'', v, u'', u} Gr
⊢ ∀ {W X Y Z : D} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [Mono f] (H : IsPushout f g h i), H.IsVanKampen
Module: Mathlib.CategoryTheory.Sites.Localization

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_3
inst✝¹ : Category.{v_3, u_3} D
K : GrothendieckTopology D
inst✝ : LocallySmall.{w, v_1, u_1} C
F : C ⥤ D
H : (Cᵒᵖ ⥤ Type w) ⥤ Dᵒᵖ ⥤ Type w
adj : H ⊣ (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type w)).obj F.op
h : ∀ ⦃X : C⦄ ⦃S : Sieve X⦄, S ∈ J X → K.W (H.map (Sieve.shrinkFunctor.{w, v_1, u_1} S).ι)
G : Dᵒᵖ ⥤ Type w
hG : IsSheaf K G
X : C
S : Sieve X
hS : S ∈ J X
⊢ IsSheafFor (F.op ⋙ G) S.arrows

Tactic:
Presieve.isSheafFor_iff_bijective_shrinkFunctor_ι_comp,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_3
inst✝¹ : Category.{v_3, u_3} D
K : GrothendieckTopology D
inst✝ : LocallySmall.{w, v_1, u_1} C
F : C ⥤ D
H : (Cᵒᵖ ⥤ Type w) ⥤ Dᵒᵖ ⥤ Type w
adj : H ⊣ (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type w)).obj F.op
h : ∀ ⦃X : C⦄ ⦃S : Sieve X⦄, S ∈ J X → K.W (H.map (Sieve.shrinkFunctor.{w, v_1, u_1} S).ι)
G : Dᵒᵖ ⥤ Type w
hG : IsSheaf K G
X : C
S : Sieve X
hS : S ∈ J X
⊢ Function.Bijective fun g ↦ (Sieve.shrinkFunctor.{w, v_1, u_1} S).ι ≫ g
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝ : J.HasSheafCompose F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ ((whiskeringRight Cᵒᵖ A B).obj F ⋙ G₂).map f ≫
      (adj₂.homEquiv (((whiskeringRight Cᵒᵖ A B).obj F).obj Q) ((G₁ ⋙ sheafCompose J F).obj Q)).symm
        (whiskerRight (adj₁.unit.app Q) F) =
    (adj₂.homEquiv (((whiskeringRight Cᵒᵖ A B).obj F).obj P) ((G₁ ⋙ sheafCompose J F).obj P)).symm
        (whiskerRight (adj₁.unit.app P) F) ≫
      (G₁ ⋙ sheafCompose J F).map f

Tactic:
by
    dsimp
    erw [← adj₂.homEquiv_naturality_left_symm,
      ← adj₂.homEquiv_naturality_right_symm]
    congr 1
    ext X
    have := NatTrans.congr_app (adj₁.unit.naturality f) X
    dsimp at this ⊢
    grind

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallyInjective J f₂
inst✝ : IsLocallySurjective J f₂
⊢ IsLocallySurjective J (f₁ ≫ f₂) ↔ IsLocallySurjective J f₁

Tactic:
constructor
  · intro
    exact isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective J f₁ f₂
  · intro
    infer_instance

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 Y : Cᵒᵖ
π : X ⟶ Y
r r' : ↑(R.obj.obj X)
m m' x₁ : ↑(A.obj.obj X)
h₁ :
  ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
    (ConcreteCategory.hom (α.app Y)) r₀ = (ConcreteCategory.hom (R.obj.map f)) r →
      ∀ (m₀ : ↑(M₀.obj Y)),
        (ConcreteCategory.hom (φ.app Y)) m₀ = (ConcreteCategory.hom (A.obj.map f)) m →
          (ConcreteCategory.hom (A.obj.map f)) x₁ = (ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)
x₂ : ↑(A.obj.obj X)
h₂ :
  ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
    (ConcreteCategory.hom (α.app Y)) r₀ = (ConcreteCategory.hom (R.obj.map f)) r →
      ∀ (m₀ : ↑(M₀.obj Y)),
        (ConcreteCategory.hom (φ.app Y)) m₀ = (ConcreteCategory.hom (A.obj.map f)) m →
          (ConcreteCategory.hom (A.obj.map f)) x₂ = (ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m
hS : S ∈ J (Opposite.unop X)
⊢ x₁ = x₂

Tactic:
apply A.isSeparated _ _ hS

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 Y : Cᵒᵖ
π : X ⟶ Y
r r' : ↑(R.obj.obj X)
m m' x₁ : ↑(A.obj.obj X)
h₁ :
  ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
    (ConcreteCategory.hom (α.app Y)) r₀ = (ConcreteCategory.hom (R.obj.map f)) r →
      ∀ (m₀ : ↑(M₀.obj Y)),
        (ConcreteCategory.hom (φ.app Y)) m₀ = (ConcreteCategory.hom (A.obj.map f)) m →
          (ConcreteCategory.hom (A.obj.map f)) x₁ = (ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)
x₂ : ↑(A.obj.obj X)
h₂ :
  ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
    (ConcreteCategory.hom (α.app Y)) r₀ = (ConcreteCategory.hom (R.obj.map f)) r →
      ∀ (m₀ : ↑(M₀.obj Y)),
        (ConcreteCategory.hom (φ.app Y)) m₀ = (ConcreteCategory.hom (A.obj.map f)) m →
          (ConcreteCategory.hom (A.obj.map f)) x₂ = (ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)
S : Sieve (Opposite.unop X) := ⋯
hS : S ∈ J (Opposite.unop X)
⊢ ∀ (Y : C) (f : Y ⟶ Opposite.unop X),
    S.arrows f → (ConcreteCategory.hom (A.obj.map f.op)) x₁ = (ConcreteCategory.hom (A.obj.map f.op)) x₂
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ᵒᵖ
r : ↑(R.obj.obj X)
m m' : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m ⊓ Presheaf.imageSieve φ m'
hS : S ∈ J (Opposite.unop X)
⊢ smul α φ r (m + m') = smul α φ r m + smul α φ r m'

Tactic:
apply A.isSeparated _ _ hS

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ᵒᵖ
r : ↑(R.obj.obj X)
m m' : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := ⋯
hS : S ∈ J (Opposite.unop X)
⊢ ∀ (Y : C) (f : Y ⟶ Opposite.unop X),
    S.arrows f →
      (ConcreteCategory.hom (A.obj.map f.op)) (smul α φ r (m + m')) =
        (ConcreteCategory.hom (A.obj.map f.op)) (smul α φ r m + smul α φ r 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ᵒᵖ
r r' : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m
hS : S ∈ J (Opposite.unop X)
⊢ smul α φ (r + r') m = smul α φ r m + smul α φ r' m

Tactic:
apply A.isSeparated _ _ hS

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ᵒᵖ
r r' : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := ⋯
hS : S ∈ J (Opposite.unop X)
⊢ ∀ (Y : C) (f : Y ⟶ Opposite.unop X),
    S.arrows f →
      (ConcreteCategory.hom (A.obj.map f.op)) (smul α φ (r + r') m) =
        (ConcreteCategory.hom (A.obj.map f.op)) (smul α φ r m + smul α φ r' 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ᵒᵖ
r r' : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m
hS : S ∈ J (Opposite.unop X)
⊢ smul α φ (r * r') m = smul α φ r (smul α φ r' m)

Tactic:
apply A.isSeparated _ _ hS

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ᵒᵖ
r r' : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := ⋯
hS : S ∈ J (Opposite.unop X)
⊢ ∀ (Y : C) (f : Y ⟶ Opposite.unop X),
    S.arrows f →
      (ConcreteCategory.hom (A.obj.map f.op)) (smul α φ (r * r') m) =
        (ConcreteCategory.hom (A.obj.map f.op)) (smul α φ r (smul α φ r' 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ᵒᵖ
r r' : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m
hS : S ∈ J (Opposite.unop X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ↑(R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.obj.map f.op)) r
r₀' : ↑(R₀.obj (Opposite.op Y))
hr₀' : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀' = (ConcreteCategory.hom (R.obj.map f.op)) r'
m₀ : ↑(M₀.obj (Opposite.op Y))
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.obj.map f.op)) m
⊢ (ConcreteCategory.hom (α.app (Opposite.op Y))) (r₀ * r₀') = (ConcreteCategory.hom (R.obj.map f.op)) (r * r')

Tactic:
map_mul,

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ᵒᵖ
r r' : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m
hS : S ∈ J (Opposite.unop X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ↑(R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.obj.map f.op)) r
r₀' : ↑(R₀.obj (Opposite.op Y))
hr₀' : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀' = (ConcreteCategory.hom (R.obj.map f.op)) r'
m₀ : ↑(M₀.obj (Opposite.op Y))
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.obj.map f.op)) m
⊢ (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ * (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀' =
    (ConcreteCategory.hom (R.obj.map f.op)) (r * r')
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ᵒᵖ
r r' : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m
hS : S ∈ J (Opposite.unop X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ↑(R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.obj.map f.op)) r
r₀' : ↑(R₀.obj (Opposite.op Y))
hr₀' : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀' = (ConcreteCategory.hom (R.obj.map f.op)) r'
m₀ : ↑(M₀.obj (Opposite.op Y))
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.obj.map f.op)) m
⊢ (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ * (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀' =
    (ConcreteCategory.hom (R.obj.map f.op)) (r * r')

Tactic:
map_mul,

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ᵒᵖ
r r' : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m
hS : S ∈ J (Opposite.unop X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ↑(R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.obj.map f.op)) r
r₀' : ↑(R₀.obj (Opposite.op Y))
hr₀' : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀' = (ConcreteCategory.hom (R.obj.map f.op)) r'
m₀ : ↑(M₀.obj (Opposite.op Y))
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.obj.map f.op)) m
⊢ (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ * (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀' =
    (ConcreteCategory.hom (R.obj.map f.op)) r * (ConcreteCategory.hom (R.obj.map f.op)) r'
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)
⊢ (ConcreteCategory.hom (A.obj.map π)) (smul α φ r m) =
    smul α φ ((ConcreteCategory.hom (R.obj.map π)) r) ((ConcreteCategory.hom (A.obj.map π)) m)

Tactic:
apply A.isSeparated _ _ hS

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 Y : Cᵒᵖ
π : X ⟶ Y
r : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop Y) := ⋯
hS : S ∈ J (Opposite.unop Y)
⊢ ∀ (Y_1 : C) (f : Y_1 ⟶ Opposite.unop Y),
    S.arrows f →
      (ConcreteCategory.hom (A.obj.map f.op)) ((ConcreteCategory.hom (A.obj.map π)) (smul α φ r m)) =
        (ConcreteCategory.hom (A.obj.map f.op))
          (smul α φ ((ConcreteCategory.hom (R.obj.map π)) r) ((ConcreteCategory.hom (A.obj.map π)) m))
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S✝ T : C
E✝¹ : PreZeroHypercover S✝
F✝¹ : PreZeroHypercover S✝
E✝ : PreZeroHypercover S✝
F✝ : PreZeroHypercover S✝
G : PreZeroHypercover S✝
S : C
E F : PreZeroHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
i : E.I₀
⊢ (eqToHom ⋯ ≫ (h₀ (s₀.symm (s₀ i))).inv) ≫ E.f (s₀.symm (s₀ i)) = F.f (s₀ i)

Tactic:
simp only [← cancel_epi (h₀ i).hom, w₀, Category.assoc, Equiv.symm_apply_apply,
      eqToHom_iso_hom_naturality_assoc, Iso.hom_inv_id_assoc]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S✝ T : C
E✝¹ : PreZeroHypercover S✝
F✝¹ : PreZeroHypercover S✝
E✝ : PreZeroHypercover S✝
F✝ : PreZeroHypercover S✝
G : PreZeroHypercover S✝
S : C
E F : PreZeroHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
i : E.I₀
⊢ eqToHom ⋯ ≫ E.f (s₀.symm (s₀ i)) = E.f i