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

Goal state before:
pp: J : Type v'
inst✝⁶ : Category.{u', v'} J
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsUniversalColimit c
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
this✝² : PreservesLimitsOfSize.{?u.146, ?u.145, v_2, v, u_2, u} Gr
this✝¹ : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
this✝ : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.1 ((𝟭 C).obj X)))
this : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
⊢ Nonempty (IsColimit c')

Tactic:
have hc'' : ∀ j, α.app j ≫ Gl.map (c.ι.app j) = c'.ι.app j ≫ f := NatTrans.congr_app h

Goal state after:
J : Type v'
inst✝⁶ : Category.{u', v'} J
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsUniversalColimit c
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
this✝² : PreservesLimitsOfSize.{?u.146, ?u.145, v_2, v, u_2, u} Gr
this✝¹ : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
this✝ : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.1 ((𝟭 C).obj X)))
this : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
hc'' : ∀ (j : J), α.app j ≫ Gl.map (c.ι.app j) = c'.ι.app j ≫ f
⊢ Nonempty (IsColimit c')
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mpr.fac_right
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
⊢ iY ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯) = s.inr

Tactic:
exact H.isColimit.fac _ WalkingSpan.left

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

Goal state before:
pp: 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)
X : C
K : Type s
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
⊢ ∀ {K_1 : K ⥤ Cᵒᵖ ⥤ D}, PreservesLimit K_1 (J.diagramFunctor D X)

Tactic:
by apply preservesLimit_diagramFunctor.{s, t, w, v, u}

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
eq : G.map (adj.unit.app X₁) ≫ adj.counit.app (G.obj X₁) = 𝟙 (G.obj X₁)
⊢ G'.map ((Localization.ε adj L₁ W₁ L₂ G' F').app (L₁.obj X₁)) ≫
      (G'.associator F' G').hom.app (L₁.obj X₁) ≫ (G'.whiskerLeft (Localization.η adj L₁ L₂ W₂ G' F')).app (L₁.obj X₁) =
    (NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X₁)

Tactic:
Localization.ε_app,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
eq : G.map (adj.unit.app X₁) ≫ adj.counit.app (G.obj X₁) = 𝟙 (G.obj X₁)
⊢ G'.map
        (L₁.map (adj.unit.app X₁) ≫
          (CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁) ≫ F'.map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁)) ≫
      (G'.associator F' G').hom.app (L₁.obj X₁) ≫ (G'.whiskerLeft (Localization.η adj L₁ L₂ W₂ G' F')).app (L₁.obj X₁) =
    (NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X₁)
Module: Mathlib.CategoryTheory.Localization.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : adj.unit.app (F.obj X₂) ≫ F.map (adj.counit.app X₂) = 𝟙 (F.obj X₂)
⊢ (𝟭 D₁).map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫
      (Localization.ε adj L₁ W₁ L₂ G' F').app ((F ⋙ L₁).obj X₂) ≫
        F'.map ((CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂)) =
    (NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X₂)

Tactic:
Localization.ε_app,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : adj.unit.app (F.obj X₂) ≫ F.map (adj.counit.app X₂) = 𝟙 (F.obj X₂)
⊢ (𝟭 D₁).map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫
      (L₁.map (adj.unit.app (F.obj X₂)) ≫
          (CatCommSq.iso F L₂ L₁ F').hom.app (G.obj (F.obj X₂)) ≫
            F'.map ((CatCommSq.iso G L₁ L₂ G').hom.app (F.obj X₂))) ≫
        F'.map ((CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂)) =
    (NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X₂)
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
K : GrothendieckTopology C
hJK : J ≤ K
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
h : IsLocallySurjective J f
U✝ : C
s : ToType (G.obj (op U✝))
⊢ imageSieve f s ∈ K U✝

Tactic:
by apply hJK; exact h.1 _

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf

Goal state before:
pp: case refine_1.refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
X Y : Cᵒᵖ
hX : Limits.IsInitial X
hY : Limits.IsInitial Y
φ : X ≅ Y
M : SheafOfModules R
U : Cᵒᵖ
⊢ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.obj.map (hX.to U)))).obj (M.val.obj U) ≅
    (ModuleCat.restrictScalars (RingCat.Hom.hom (R.obj.map φ.hom))).obj
      ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.obj.map (hY.to U)))).obj (M.val.obj U))

Tactic:
refine ModuleCat.restrictScalarsComp'App _ _ _ ?_ _

Goal state after:
case refine_1.refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
X Y : Cᵒᵖ
hX : Limits.IsInitial X
hY : Limits.IsInitial Y
φ : X ≅ Y
M : SheafOfModules R
U : Cᵒᵖ
⊢ RingCat.Hom.hom (R.obj.map (hX.to U)) =
    (RingCat.Hom.hom (R.obj.map (hY.to U))).comp (RingCat.Hom.hom (R.obj.map φ.hom))
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₁
⊢ IsLocallyInjective J (f₁ ≫ f₂) ↔ IsLocallyInjective J f₂

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

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

Goal state before:
pp: case refine_2.uniq.zero
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
j : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone (Discrete.functor F')
α : Discrete.functor F' ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
T : C
f₁ : F' 0 ⟶ T
f₂ : (∐ fun j ↦ (Discrete.functor F').obj { as := j.succ }) ⟶ T
f₃ : (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).pt ⟶ T
m₁ : c.ι.app { as := 0 } ≫ f₃ = f₁
m₂ : (Sigma.desc fun b ↦ c.ι.app { as := b.succ }) ≫ f₃ = f₂
⊢ c.ι.app { as := 0 } ≫ f₃ = Fin.cases f₁ (fun i ↦ Sigma.ι (fun j ↦ F' j.succ) i ≫ f₂) 0

pp: case refine_2.uniq.succ
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
j : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone (Discrete.functor F')
α : Discrete.functor F' ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
T : C
f₁ : F' 0 ⟶ T
f₂ : (∐ fun j ↦ (Discrete.functor F').obj { as := j.succ }) ⟶ T
f₃ : (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).pt ⟶ T
m₁ : c.ι.app { as := 0 } ≫ f₃ = f₁
m₂ : (Sigma.desc fun b ↦ c.ι.app { as := b.succ }) ≫ f₃ = f₂
i✝ : Fin n
a✝ : c.ι.app { as := i✝.castSucc } ≫ f₃ = Fin.cases f₁ (fun i ↦ Sigma.ι (fun j ↦ F' j.succ) i ≫ f₂) i✝.castSucc
⊢ c.ι.app { as := i✝.succ } ≫ f₃ = Fin.cases f₁ (fun i ↦ Sigma.ι (fun j ↦ F' j.succ) i ≫ f₂) i✝.succ

Tactic:
· simp only [Fin.cases_zero, m₁]

Goal state after:
case refine_2.uniq.succ
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
j : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone (Discrete.functor F')
α : Discrete.functor F' ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
T : C
f₁ : F' 0 ⟶ T
f₂ : (∐ fun j ↦ (Discrete.functor F').obj { as := j.succ }) ⟶ T
f₃ : (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).pt ⟶ T
m₁ : c.ι.app { as := 0 } ≫ f₃ = f₁
m₂ : (Sigma.desc fun b ↦ c.ι.app { as := b.succ }) ≫ f₃ = f₂
i✝ : Fin n
a✝ : c.ι.app { as := i✝.castSucc } ≫ f₃ = Fin.cases f₁ (fun i ↦ Sigma.ι (fun j ↦ F' j.succ) i ≫ f₂) i✝.castSucc
⊢ c.ι.app { as := i✝.succ } ≫ f₃ = Fin.cases f₁ (fun i ↦ Sigma.ι (fun j ↦ F' j.succ) i ≫ f₂) i✝.succ
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
R : Cᵒᵖ ⥤ RingCat
F : D ⥤ PresheafOfModules R
inst✝¹ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
c : Cone F
inst✝ : HasLimitsOfShape D AddCommGrpCat
hc : IsLimit c
hF : ∀ (j : D), Presheaf.IsSheaf J (F.obj j).presheaf
⊢ Presheaf.IsSheaf J c.pt.presheaf

Tactic:
let G : D ⥤ Sheaf J AddCommGrpCat.{v} :=
    { obj := fun j => ⟨(F.obj j).presheaf, hF j⟩
      map := fun φ => ⟨(PresheafOfModules.toPresheaf R).map (F.map φ)⟩ }

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
R : Cᵒᵖ ⥤ RingCat
F : D ⥤ PresheafOfModules R
inst✝¹ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
c : Cone F
inst✝ : HasLimitsOfShape D AddCommGrpCat
hc : IsLimit c
hF : ∀ (j : D), Presheaf.IsSheaf J (F.obj j).presheaf
G : D ⥤ Sheaf J AddCommGrpCat :=
  { obj := fun j ↦ { obj := (F.obj j).presheaf, property := ⋯ },
    map := fun {X Y} φ ↦ { hom := (toPresheaf R).map (F.map φ) }, map_id := ⋯, map_comp := ⋯ }
⊢ Presheaf.IsSheaf J c.pt.presheaf
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: case refine_2
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' : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X)
hS : S ∈ J (Opposite.unop X)
r₀ : Presieve.FamilyOfElements (R₀ ⋙ forget RingCat) S.arrows
m₀ : Presieve.FamilyOfElements (M₀.presheaf ⋙ forget Ab) S.arrows
hr₀ : (r₀.map (whiskerRight α (forget RingCat))).IsAmalgamation r
hm₀ : (m₀.map (whiskerRight φ (forget Ab))).IsAmalgamation m
a : ↑(A.obj.obj X)
ha : ((r₀.smul m₀).map (whiskerRight φ (forget Ab))).IsAmalgamation a
Y : Cᵒᵖ
f : X ⟶ Y
a₀ : ↑(R₀.obj Y)
ha₀ : (ConcreteCategory.hom (α.app Y)) a₀ = (ConcreteCategory.hom (R.obj.map f)) r
b₀ : ↑(M₀.obj Y)
hb₀ : (ConcreteCategory.hom (φ.app Y)) b₀ = (ConcreteCategory.hom (A.obj.map f)) m
Z : C
g : Z ⟶ Opposite.unop Y
hg : S.arrows (g ≫ f.unop)
⊢ (ConcreteCategory.hom (A.obj.map (f ≫ g.op))) m =
    (ConcreteCategory.hom (A.obj.map g.op)) ((ConcreteCategory.hom (A.obj.map f)) m)

Tactic:
rw [Functor.map_comp]

Goal state after:
case refine_2
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' : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X)
hS : S ∈ J (Opposite.unop X)
r₀ : Presieve.FamilyOfElements (R₀ ⋙ forget RingCat) S.arrows
m₀ : Presieve.FamilyOfElements (M₀.presheaf ⋙ forget Ab) S.arrows
hr₀ : (r₀.map (whiskerRight α (forget RingCat))).IsAmalgamation r
hm₀ : (m₀.map (whiskerRight φ (forget Ab))).IsAmalgamation m
a : ↑(A.obj.obj X)
ha : ((r₀.smul m₀).map (whiskerRight φ (forget Ab))).IsAmalgamation a
Y : Cᵒᵖ
f : X ⟶ Y
a₀ : ↑(R₀.obj Y)
ha₀ : (ConcreteCategory.hom (α.app Y)) a₀ = (ConcreteCategory.hom (R.obj.map f)) r
b₀ : ↑(M₀.obj Y)
hb₀ : (ConcreteCategory.hom (φ.app Y)) b₀ = (ConcreteCategory.hom (A.obj.map f)) m
Z : C
g : Z ⟶ Opposite.unop Y
hg : S.arrows (g ≫ f.unop)
⊢ (ConcreteCategory.hom (A.obj.map f ≫ A.obj.map g.op)) m =
    (ConcreteCategory.hom (A.obj.map g.op)) ((ConcreteCategory.hom (A.obj.map f)) m)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
ι : Type w'
e : ι ≃ E.I₀
⊢ (E.reindex e).presieve₀ = E.presieve₀

Tactic:
by
  simp [reindex]

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

Goal state before:
pp: case refine_2
C : Type u_2
inst✝ : Category.{v_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS : IsSeparatedFor P S ∧ ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
x : FamilyOfElements P T
hx : x.Compatible
y : FamilyOfElements P S := fun Y g hg ↦ (ConcreteCategory.hom (P.map (i hg).op)) (x (e hg) ⋯)
hy : y.Compatible
left✝ : IsSeparatedFor P S
h2' : ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t
z : P.obj (Opposite.op X)
hz : y.IsAmalgamation z
Y : C
g : Y ⟶ X
hg : T g
R : Presieve Y
hR1 : IsSeparatedFor P R
WW : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → R g → C
ii : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → Z ⟶ WW a
ee : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → WW a ⟶ X
hh1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (a : R g), S (ee a)
hh2 : ∀ ⦃Z : C⦄ ⦃g_1 : Z ⟶ Y⦄ (a : R g_1), ii a ≫ ee a = g_1 ≫ g
Q : C
t : Q ⟶ Y
ht : R t
⊢ (ConcreteCategory.hom (P.map t.op)) ((ConcreteCategory.hom (P.map g.op)) z) =
    (ConcreteCategory.hom (P.map t.op)) (x g hg)

Tactic:
rw [← types_comp_apply (P.map g.op) (P.map t.op), ← P.map_comp, ← op_comp, ← hh2 ht,
    op_comp, P.map_comp, types_comp_apply, hz _ (hh1 _),
    ← types_comp_apply _ (P.map (ii ht).op), ← P.map_comp, ← op_comp]

Goal state after:
case refine_2
C : Type u_2
inst✝ : Category.{v_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS : IsSeparatedFor P S ∧ ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
x : FamilyOfElements P T
hx : x.Compatible
y : FamilyOfElements P S := fun Y g hg ↦ (ConcreteCategory.hom (P.map (i hg).op)) (x (e hg) ⋯)
hy : y.Compatible
left✝ : IsSeparatedFor P S
h2' : ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t
z : P.obj (Opposite.op X)
hz : y.IsAmalgamation z
Y : C
g : Y ⟶ X
hg : T g
R : Presieve Y
hR1 : IsSeparatedFor P R
WW : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → R g → C
ii : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → Z ⟶ WW a
ee : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → WW a ⟶ X
hh1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (a : R g), S (ee a)
hh2 : ∀ ⦃Z : C⦄ ⦃g_1 : Z ⟶ Y⦄ (a : R g_1), ii a ≫ ee a = g_1 ≫ g
Q : C
t : Q ⟶ Y
ht : R t
⊢ (ConcreteCategory.hom (P.map (ii ht ≫ i ⋯).op)) (x (e ⋯) ⋯) = (ConcreteCategory.hom (P.map t.op)) (x g hg)
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
J : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J X
⊢ Sieve.generate S.arrows ∈ J X

Tactic:
rwa [Sieve.generate_sieve S]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
J : Pretopology C
T : C
S : Sieve T
⊢ S ∈ J.toCoverage.toGrothendieck T ↔ S ∈ J.toGrothendieck T

Tactic:
mem_toGrothendieck,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
J : Pretopology C
T : C
S : Sieve T
⊢ S ∈ J.toCoverage.toGrothendieck T ↔ ∃ R ∈ J.coverings T, R ≤ S.arrows
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
J : Pretopology C
⊢ J.toCoverage.toGrothendieck = J.toGrothendieck

Tactic:
ext T S
  rw [mem_toGrothendieck, Coverage.mem_toGrothendieck]
  refine ⟨fun h ↦ ?_, fun ⟨R, hR, hle⟩ ↦ ?_⟩
  · induction h with
    | of X S hS => use S, hS, Sieve.le_generate S
    | top X => use Presieve.singleton (𝟙 X), J.has_isos (𝟙 X), le_top
    | transitive X R S hR hRS hle hfS =>
        obtain ⟨R', hR', hle⟩ := hle
        choose S' hS' hS'le using hfS
        refine ⟨Presieve.bind R' (fun Y f hf ↦ S' (hle _ _ hf)), ?_, fun Z u hu ↦ ?_⟩
        · exact J.transitive R' (fun Y f hf ↦ S' (hle Y _ hf)) hR' fun Y f H ↦ hS' (hle Y _ H)
        · obtain ⟨W, g, w, hw, hg, rfl⟩ := hu
          exact hS'le _ _ _ hg
  · refine Coverage.saturate_of_superset _ ?_ (.of _ _ hR)
    rwa [Sieve.generate_le_iff]

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

Goal state before:
pp: case mpr.h
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ K.coverings X
T : Presieve Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
⊢ ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄,
    (Sieve.pullback f (Sieve.generate S)).arrows f_1 → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong T f_1

Tactic:
intro Z g _

Goal state after:
case mpr.h
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ K.coverings X
T : Presieve Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
Z : C
g : Z ⟶ Y
a✝ : (Sieve.pullback f (Sieve.generate S)).arrows g
⊢ ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong T g
Module: Mathlib.CategoryTheory.Sites.CoverLifting

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.IsCocontinuous J K
⊢ G.IsContinuous K J

Tactic:
have := adj.isRightAdjoint
  apply Functor.isContinuous_of_coverPreserving (compatiblePreservingOfFlat J G)
  rwa [← adj.isCocontinuous_iff_coverPreserving]

Goal state after: