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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
⊢ IsVanKampenColimit c

Tactic:
by
  rw [BinaryCofan.isVanKampen_iff]
  introv hX hY
  constructor
  · rintro ⟨h⟩
    let e := h.coconePointUniqueUpToIso (colimits _ _)
    obtain ⟨hl, hr⟩ := h₁ αX αY (e.inv ≫ f) (by simp [e, hX]) (by simp [e, hY])
    constructor
    · rw [← Category.id_comp αX, ← Iso.hom_inv_id_assoc e f]
      have : IsIso (𝟙 X') := inferInstance
      have : c'.inl ≫ e.hom = 𝟙 X' ≫ (cofans X' Y').inl := by
        dsimp [e]
        simp
      exact (IsPullback.of_vert_isIso ⟨this⟩).paste_vert hl
    · rw [← Category.id_comp αY, ← Iso.hom_inv_id_assoc e f]
      have : IsIso (𝟙 Y') := inferInstance
      have : c'.inr ≫ e.hom = 𝟙 Y' ≫ (cofans X' Y').inr := by
        dsimp [e]
        simp
      exact (IsPullback.of_vert_isIso ⟨this⟩).paste_vert hr
  · rintro ⟨H₁, H₂⟩
    refine ⟨IsColimit.ofIsoColimit ?_ <| (isoBinaryCofanMk _).symm⟩
    let e₁ : X' ≅ _ := H₁.isLimit.conePointUniqueUpToIso (limits _ _)
    let e₂ : Y' ≅ _ := H₂.isLimit.conePointUniqueUpToIso (limits _ _)
    have he₁ : c'.inl = e₁.hom ≫ (cones f c.inl).fst := by simp [e₁]
    have he₂ : c'.inr = e₂.hom ≫ (cones f c.inr).fst := by simp [e₂]
    rw [he₁, he₂]
    exact (BinaryCofan.mk _ _).isColimitCompRightIso e₂.hom
      ((BinaryCofan.mk _ _).isColimitCompLeftIso e₁.hom (h₂ f))

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

Goal state before:
pp: case mpr
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
h : ∀ (P : Cᵒᵖ ⥤ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : IsIso (G₁.map f)
⊢ J.W (whiskerRight f F ≫ whiskerRight (adj₁.unit.app P₂) F)

Tactic:
← whiskerRight_comp

Goal state after:
case mpr
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
h : ∀ (P : Cᵒᵖ ⥤ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : IsIso (G₁.map f)
⊢ J.W (whiskerRight (f ≫ adj₁.unit.app P₂) F)
Module: Mathlib.CategoryTheory.Sites.LocallyInjective

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
X : Cᵒᵖ
x : F.obj X
property✝ : x ∈ G.obj X
⊢ ∀ ⦃a₂ : G.toFunctor.obj X⦄,
    (ConcreteCategory.hom (G.ι.app X)) ⟨x, property✝⟩ = (ConcreteCategory.hom (G.ι.app X)) a₂ → ⟨x, property✝⟩ = a₂

Tactic:
⟨y, _⟩

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
X : Cᵒᵖ
x : F.obj X
property✝¹ : x ∈ G.obj X
y : F.obj X
property✝ : y ∈ G.obj X
⊢ (ConcreteCategory.hom (G.ι.app X)) ⟨x, property✝¹⟩ = (ConcreteCategory.hom (G.ι.app X)) ⟨y, property✝⟩ →
    ⟨x, property✝¹⟩ = ⟨y, property✝⟩
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : LocallySmall.{w, v, u} C
S : C
ι : Type u_2
inst✝ : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan fun i ↦ shrinkYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
hf : Presheaf.IsLocallySurjective J (Cofan.IsColimit.desc hc fun i ↦ shrinkYoneda.{w, v, u}.map (f i))
⊢ Presheaf.imageSieve (Cofan.IsColimit.desc hc fun i ↦ shrinkYoneda.{w, v, u}.map (f i))
      (shrinkYonedaObjObjEquiv.symm (𝟙 S)) ∈
    J S

Tactic:
exact Presheaf.imageSieve_mem J (Cofan.IsColimit.desc hc (fun i ↦ shrinkYoneda.{w}.map (f i)))
      (shrinkYonedaObjObjEquiv.symm (𝟙 S))

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₀ 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₀'
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Y))) (r₀ • m₀) = (ConcreteCategory.hom (φ.app (Opposite.op Y))) (r₀' • m₀')

Tactic:
apply hA _ (Presheaf.equalizerSieve r₀ r₀' ⊓
      Presheaf.equalizerSieve (F := M₀.presheaf) m₀ m₀')

Goal state after:
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))

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.Submodule

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
N✝ : M.Submodule
s : Set M.Submodule
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
N : M.Submodule
hN : N ∈ s
⊢ ⨅ N ∈ s, N.obj X✝ ≤ Submodule.comap (M.restrictₛₗ f) (N.obj Y✝)

Tactic:
refine iInf₂_le_of_le _ hN (N.map _)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ projectiveDimension X = ⊥ ↔ Limits.IsZero X

Tactic:
rw [← hasProjectiveDimensionLT_zero_iff_isZero, ← projectiveDimension_lt_iff,
    Nat.cast_zero, ← WithBot.lt_coe_bot, bot_eq_zero', WithBot.coe_zero]

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

Goal state before:
pp: case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : BiconeHom J (Bicone.diagram j✝) Z✝
⊢ BiconeHom J Bicone.left Z✝

pp: case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : BiconeHom J (Bicone.diagram j✝) Z✝
⊢ BiconeHom J Bicone.right Z✝

pp: case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f : j✝ ⟶ k✝
g : BiconeHom J (Bicone.diagram k✝) Z✝
⊢ BiconeHom J (Bicone.diagram j✝) Z✝

Tactic:
· cases g
      apply BiconeHom.left

Goal state after:
case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : BiconeHom J (Bicone.diagram j✝) Z✝
⊢ BiconeHom J Bicone.right Z✝

case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f : j✝ ⟶ k✝
g : BiconeHom J (Bicone.diagram k✝) Z✝
⊢ BiconeHom J (Bicone.diagram j✝) Z✝
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : HasWeakSheafify J AddCommGrpCat
inst✝ : J.WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
I : Type u
f : I → M.sections
⊢ (fun f i ↦ M.unitHomEquiv (ιFree i ≫ f))
      ((fun s ↦ Cofan.IsColimit.desc (isColimitFreeCofan I) fun i ↦ M.unitHomEquiv.symm (s i)) f) =
    f

Tactic:
by ext1 i; simp [← freeCofan_inj]

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 φ
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
M₀' : PresheafOfModules R₀
A' : Sheaf J AddCommGrpCat
φ' : M₀'.presheaf ⟶ A'.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ'
inst✝ : Presheaf.IsLocallySurjective J φ'
τ₀ : M₀ ⟶ M₀'
τ : A ⟶ A'
fac : (toPresheaf R₀).map τ₀ ≫ φ' = φ ≫ τ.hom
X : Cᵒᵖ
r : ↑(R.obj.obj X)
m : ↑((sheafify α φ).val.obj X)
⊢ Presheaf.IsSheaf J (sheafify α φ').val.presheaf

Tactic:
exact A'.property

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 φ
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
M₀' : PresheafOfModules R₀
A' : Sheaf J AddCommGrpCat
φ' : M₀'.presheaf ⟶ A'.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ'
inst✝ : Presheaf.IsLocallySurjective J φ'
τ₀ : M₀ ⟶ M₀'
τ : A ⟶ A'
fac : (toPresheaf R₀).map τ₀ ≫ φ' = φ ≫ τ.hom
X : Cᵒᵖ
r : ↑(R.obj.obj X)
m : ↑((sheafify α φ).val.obj X)
⊢ (ConcreteCategory.hom (τ.hom.app X)) (r • m) = r • (ConcreteCategory.hom (τ.hom.app X)) m

Tactic:
let f := (sheafifyHomEquiv' α φ (by exact A'.property)).symm (τ₀ ≫ toSheafify α φ')

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 φ
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
M₀' : PresheafOfModules R₀
A' : Sheaf J AddCommGrpCat
φ' : M₀'.presheaf ⟶ A'.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ'
inst✝ : Presheaf.IsLocallySurjective J φ'
τ₀ : M₀ ⟶ M₀'
τ : A ⟶ A'
fac : (toPresheaf R₀).map τ₀ ≫ φ' = φ ≫ τ.hom
X : Cᵒᵖ
r : ↑(R.obj.obj X)
m : ↑((sheafify α φ).val.obj X)
f : (sheafify α φ).val ⟶ (sheafify α φ').val := (sheafifyHomEquiv' α φ ⋯).symm (τ₀ ≫ toSheafify α φ')
⊢ (ConcreteCategory.hom (τ.hom.app X)) (r • m) = r • (ConcreteCategory.hom (τ.hom.app X)) m
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
⊢ Presieve.IsSeparatedFor (Functor.closedSieves J₁).toFunctor S.arrows

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
⊢ ∀ (x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
· rintro x ⟨M, hM⟩ ⟨N, hN⟩ hM₂ hN₂
    dsimp at S M N ⊢
    ext Y f
    dsimp only [Subtype.coe_mk]
    rw [← J₁.covers_iff_mem_of_isClosed hM, ← J₁.covers_iff_mem_of_isClosed hN]
    have q : ∀ ⦃Z : C⦄ (g : Z ⟶ X) (_ : S g), M.pullback g = N.pullback g :=
      fun Z g hg => congr_arg Subtype.val ((hM₂ g hg).trans (hN₂ g hg).symm)
    have MSNS : M ⊓ S = N ⊓ S := by
      ext
      grind [Sieve.inter_apply, Sieve.mem_iff_pullback_eq_top]
    constructor
    · intro hf
      rw [J₁.covers_iff]
      apply J₁.superset_covering (Sieve.pullback_monotone f inf_le_left)
      rw [← MSNS]
      apply J₁.arrow_intersect f M S hf (J₁.pullback_stable _ hS)
    · intro hf
      rw [J₁.covers_iff]
      apply J₁.superset_covering (Sieve.pullback_monotone f inf_le_left)
      rw [MSNS]
      apply J₁.arrow_intersect f N S hf (J₁.pullback_stable _ hS)

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
⊢ ∀ (x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows), x.Compatible → ∃ t, x.IsAmalgamation t
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
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.26
𝒥✝ : SmallCategory J
x✝ : FinCategory J
⊢ autoParam (∀ {K : J ⥤ C}, PreservesLimit K F) PreservesLimitsOfShape.preservesLimit._autoParam

Tactic:
intro K

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.26
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
⊢ PreservesLimit K F
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case refine_1
C : Type u_2
inst✝ : Category.{u_1, u_2} C
J : Precoverage C
⊢ ∀ b ∈ {K | ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ K X}, J.toGrothendieck ≤ b

Tactic:
intro K

Goal state after:
case refine_1
C : Type u_2
inst✝ : Category.{u_1, u_2} C
J : Precoverage C
K : GrothendieckTopology C
⊢ K ∈ {K | ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ K X} → J.toGrothendieck ≤ K
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C D : Type u₁
inst✝¹⁰ : SmallCategory C
inst✝⁹ : SmallCategory D
E : Type u₂
inst✝⁸ : Category.{u₁, u₂} E
FE : E → E → Type u_1
CE : E → Type u₁
inst✝⁷ : (X Y : E) → FunLike (FE X Y) (CE X) (CE Y)
inst✝⁶ : ConcreteCategory E FE
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type u₁
𝒥✝ : SmallCategory J
x✝ : FinCategory J
⊢ ∀ (k : Dᵒᵖ), PreservesLimitsOfShape J (F.op.lan ⋙ (evaluation Dᵒᵖ E).obj k)

Tactic:
intro K

Goal state after:
C D : Type u₁
inst✝¹⁰ : SmallCategory C
inst✝⁹ : SmallCategory D
E : Type u₂
inst✝⁸ : Category.{u₁, u₂} E
FE : E → E → Type u_1
CE : E → Type u₁
inst✝⁷ : (X Y : E) → FunLike (FE X Y) (CE X) (CE Y)
inst✝⁶ : ConcreteCategory E FE
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type u₁
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : Dᵒᵖ
⊢ PreservesLimitsOfShape J (F.op.lan ⋙ (evaluation Dᵒᵖ E).obj K)
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: C : Type u_2
inst✝³ : Category.{v_1, u_2} C
J : Precoverage C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.Small
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), Presieve.IsSheafFor P E.presieve₀
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
E : J.ZeroHypercover X := { toPreZeroHypercover := E₀, mem₀ := hR }
⊢ E.restrictIndexOfSmall.presieve₀ ≤ E₀.presieve₀

Tactic:
simp [E]

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

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
K : Coverage C
P : Cᵒᵖ ⥤ D
⊢ IsSheaf K.toGrothendieck P ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (IsLimit (P.mapCone (Sieve.generate R).arrows.cocone.op))

Tactic:
simp only [Presheaf.IsSheaf, Presieve.isSheaf_coverage, isLimit_iff_isSheafFor,
    ← Presieve.isSheafFor_iff_generate]
  aesop

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve X
E : J.OneHypercover X
hE : H E
le : E.sieve₀ ≤ S
F : Multifork (Cover.index ⟨S, ⋯⟩ P)
inst✝ : H.IsGenerating
Y✝ : C
f : Y✝ ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y✝
Y : C
i : E.I₀
a : Z ⟶ E.X i
fac : a ≫ E.f i = g ≫ f
⊢ F.ι { Y := E.X i, f := E.f i, hf := ⋯ } ≫ P.map a.op = F.ι { Y := Y✝, f := f, hf := hf } ≫ P.map g.op

Tactic:
exact F.condition {
    fst := { hf := le _ (Sieve.ofArrows_mk _ _ _), .. }
    snd := { hf := hf, .. }
    r := { w := fac, .. }
  }

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

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
Z : C
g : Z ⟶ W
⊢ (Sieve.pullback (pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂)).arrows g → (E.sieve₁ p₁ p₂).arrows g

Tactic:
rintro ⟨_, h, w, ⟨j⟩, fac⟩

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
Z : C
g : Z ⟶ W
Y : C
j : E.I₁ i₁ i₂
h : Z ⟶ E.Y j
fac : h ≫ E.toPullback j = g ≫ pullback.lift p₁ p₂ w
⊢ (E.sieve₁ p₁ p₂).arrows g
Module: Mathlib.CategoryTheory.Sites.CoverLifting

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
G : C ⥤ D
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
W : A
f g : W ⟶ R.obj (op X)
h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op
⊢ f = g

Tactic:
apply (hR (op X)).hom_ext
  intro j
  apply hF.hom_ext ⟨_, G.cover_lift J K (K.pullback_stable j.hom.unop S.2)⟩
  intro ⟨W, i, hi⟩
  have eq := h (GrothendieckTopology.Cover.Arrow.mk _ (G.map i ≫ j.hom.unop) hi)
  dsimp at eq ⊢
  simp only [Category.assoc, ← NatTrans.naturality, Functor.comp_map, ← Functor.map_comp_assoc,
    Functor.op_map, Quiver.Hom.unop_op]
  rw [reassoc_of% eq]

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
H : CoverPreserving J K F
U : C
E : J.OneHypercover U
i₁ i₂ : E.I₀
W : D
p₁ : W ⟶ F.obj (E.X i₁)
p₂ : W ⟶ F.obj (E.X i₂)
h : p₁ ≫ F.map (E.f i₁) = p₂ ≫ F.map (E.f i₂)
⊢ (E.map F).sieve₁ p₁ p₂ ∈ K W

Tactic:
let P : C := pullback (E.f i₁) (E.f i₂)

Goal state after:
case refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
H : CoverPreserving J K F
U : C
E : J.OneHypercover U
i₁ i₂ : E.I₀
W : D
p₁ : W ⟶ F.obj (E.X i₁)
p₂ : W ⟶ F.obj (E.X i₂)
h : p₁ ≫ F.map (E.f i₁) = p₂ ≫ F.map (E.f i₂)
P : C := Limits.pullback (E.f i₁) (E.f i₂)
⊢ (E.map F).sieve₁ p₁ p₂ ∈ K W
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

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
E : Type u_3
inst✝⁴ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝³ : Category.{v_4, u_4} A
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ : Sheaf K A
inst✝ : G.IsContinuous J K
ℱ ℱ' : Sheaf K A
α β : ℱ ⟶ ℱ'
e : G.op.whiskerLeft α.hom = G.op.whiskerLeft β.hom
⊢ α.hom = β.hom

Tactic:
rw [← sheafHom_eq G α.hom, ← sheafHom_eq G β.hom, e]

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
K : GrothendieckTopology D
F G : C ⥤ D
e : F ≅ G
⊢ F.inducedTopology K = G.inducedTopology K

Tactic:
by
  refine le_antisymm ?_ ?_ <;> rw [le_inducedTopology_iff]
  · apply Functor.isContinuous_of_iso e
  · apply Functor.isContinuous_of_iso e.symm

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
inst✝ : F.IsContinuous (F.restrictedTopology K) K
⊢ F.inducedTopology K = F.restrictedTopology K

Tactic:
restrictedTopology_eq_inducedTopology

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
inst✝ : F.IsContinuous (F.restrictedTopology K) K
⊢ F.inducedTopology K = F.inducedTopology K
Module: Mathlib.CategoryTheory.Sites.InducedTopology

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
K : Precoverage D
⊢ (comap F K).toGrothendieck ≤ (comap F K.toGrothendieck.toPrecoverage).toGrothendieck

Tactic:
grw [← K.le_toPrecoverage_toGrothendieck]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: case pullback
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S : Sieve X
a✝ : (Precoverage.comap G K.toPrecoverage).Saturate X S
Y : C
f : Y ⟶ X
ih : Sieve.functorPushforward G S ∈ K (G.obj X)
⊢ Sieve.functorPushforward G (Sieve.pullback f S) ∈ K (G.obj Y)

Tactic:
apply K.transitive (LocallyCoverDense.functorPushforward_functorPullback_mem
        ⟨_, K.pullback_stable (G.map f) ih⟩)
      rintro Z _ ⟨U, iUY, iZU, ⟨W, iWX, iUW, hiWX, e₁⟩, rfl⟩
      rw [Sieve.pullback_comp]
      apply K.pullback_stable
      clear iZU Z
      apply K.transitive (G.functorPushforward_imageSieve_mem _ iUW)
      rintro Z _ ⟨U₁, iU₁U, iZU₁, ⟨iU₁W, e₂⟩, rfl⟩
      rw [Sieve.pullback_comp]
      apply K.pullback_stable
      clear iZU₁ Z
      apply K.superset_covering ?_ (G.functorPushforward_equalizer_mem _
        (iU₁U ≫ iUY ≫ f) (iU₁W ≫ iWX) (by simp [e₁, e₂]))
      rintro Z _ ⟨U₂, iU₂U₁, iZU₂, e₃ : _ = _, rfl⟩
      refine ⟨_, iU₂U₁ ≫ iU₁U ≫ iUY, iZU₂, ?_, by simp⟩
      simpa [e₃] using S.downward_closed hiWX (iU₂U₁ ≫ iU₁W)

Goal state after: