mathlib-initiative/mathlib-tactics huggingface dataset:
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 G : Cᵒᵖ ⥤ A
f : F ⟶ G
⊢ IsLocallySurjective J f ↔ IsLocallySurjective J (whiskerRight f (forget A))

Tactic:
simp only [isLocallySurjective_iff_range_sheafify_eq_top]

Goal state after:
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 G : Cᵒᵖ ⥤ A
f : F ⟶ G
⊢ Subfunctor.sheafify J (Subfunctor.range (whiskerRight f (forget A))) = ⊤ ↔
    Subfunctor.sheafify J (Subfunctor.range (whiskerRight (whiskerRight f (forget A)) (forget (Type w')))) = ⊤
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: case refine_1
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 : Sieve.ofArrows X f ∈ J S
U : C
u : ToType ((shrinkYoneda.{w, v, u}.obj S).obj (op U))
⊢ Presheaf.imageSieve (Cofan.IsColimit.desc hc fun i ↦ shrinkYoneda.{w, v, u}.map (f i)) u ∈ J U

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))
⊢ Sieve.ofArrows X f ∈ J S

Tactic:
· obtain ⟨u, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective u
    replace hf := J.pullback_stable u hf
    rwa [← Presheaf.imageSieve_cofanIsColimitDesc_shrinkYoneda_map f hc u] at hf

Goal state after:
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))
⊢ Sieve.ofArrows X f ∈ J S
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_2.refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j : ι
inst✝ : DecidableEq ι
⊢ ∀ (t : Cofan fun k ↦ if k = i then X i else ⊥_ C) (j : ι),
    (Cofan.mk (X i) fun k ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).inj j ≫ eqToHom ⋯ ≫ t.inj i =
      t.inj j

Tactic:
intro t j

Goal state after:
case refine_2.refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j✝ : ι
inst✝ : DecidableEq ι
t : Cofan fun k ↦ if k = i then X i else ⊥_ C
j : ι
⊢ (Cofan.mk (X i) fun k ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).inj j ≫ eqToHom ⋯ ≫ t.inj i =
    t.inj j
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ Projective X ↔ HasProjectiveDimensionLT X 1

Tactic:
by
  let := HasExt.standard C
  exact ⟨fun _ ↦ inferInstance, fun _ ↦ projective_iff_subsingleton_ext_one.2
    (HasProjectiveDimensionLT.subsingleton X 1 1 (by rfl))⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₂ : HasProjectiveDimensionLT S.X₂ n
h₃ : HasProjectiveDimensionLT S.X₃ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₂ : Ext S.X₂ Y i
⊢ (Ext.mk₀ S.f).comp x₂ ⋯ = 0

Tactic:
rw [x₂.eq_zero_of_hasProjectiveDimensionLT n (by lia), Ext.comp_zero]

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 φ
⊢ IsLocallySurjective J (toSheafify α φ)

Tactic:
by
  dsimp [IsLocallySurjective]; infer_instance

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

Goal state before:
pp: case h
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
E F : PreZeroHypercover S
e : E ≅ F
i : E.I₀
⊢ e.hom.h₀ i ≫ e.inv.h₀ (e.hom.s₀ i) ≫ eqToHom ⋯ = 𝟙 (E.X i) ∧
    (e.inv.h₀ (e.hom.s₀ i) ≫ eqToHom ⋯) ≫ e.hom.h₀ i = 𝟙 (F.X (e.hom.s₀ i))

Tactic:
hom_inv_h₀_assoc,

Goal state after:
case h
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
E F : PreZeroHypercover S
e : E ≅ F
i : E.I₀
⊢ eqToHom ⋯ ≫ eqToHom ⋯ = 𝟙 (E.X i) ∧ (e.inv.h₀ (e.hom.s₀ i) ≫ eqToHom ⋯) ≫ e.hom.h₀ i = 𝟙 (F.X (e.hom.s₀ i))
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ (↑j).fst) (fun j ↦ YT (↑j).snd ⋯) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (↑i).snd
      | Sum.inr i => (eT (↑i).snd ⋯).hom ≫ (↑i).snd }
F : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ YR (↑j).snd ⋯) (fun j ↦ (↑j).fst) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (eR (↑i).snd ⋯).hom ≫ (↑i).snd
      | Sum.inr i => (↑i).snd }
i : E.I₀
⊢ (match i with
        | Sum.inl i => id (eR (↑i).snd ⋯).symm
        | Sum.inr i => id (eT (↑i).snd ⋯)).hom ≫
      F.f ((Equiv.refl E.I₀) i) =
    E.f i

Tactic:
cases i <;> simp [E, F]

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
hS : K.Saturate X S
⊢ K.Saturate X S

Tactic:
· induction hS <;> grind [Saturate]

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
⊢ lift hP hE le F ≫ P.map f.op = F.ι { Y := Y, f := f, hf := hf }

Tactic:
apply hom_ext H P hP _ (J.pullback_stable f E.mem₀)

Goal state after:
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
⊢ ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y),
    (Sieve.pullback f E.sieve₀).arrows f_1 →
      (lift hP hE le F ≫ P.map f.op) ≫ P.map f_1.op = F.ι { Y := Y, f := f, hf := hf } ≫ P.map f_1.op
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.HasIsos
X : C
S : Sieve X
⊢ S ∈ J.toGrothendieck X ↔ ∃ R ∈ J.coverings X, R ≤ S.arrows

Tactic:
refine ⟨fun hS ↦ ?_, fun ⟨R, hR, hle⟩ ↦ ?_⟩
  · induction hS with
    | of X R hR =>
      use R, hR
      exact Sieve.le_generate R
    | top X =>
      exact ⟨Presieve.singleton (𝟙 X), mem_coverings_of_isIso (𝟙 X), by simp⟩
    | pullback X S hS Y f h =>
      obtain ⟨R, hR, hle⟩ := h
      have : R.HasPullbacks f := J.hasPullbacks_of_mem f hR
      refine ⟨R.pullbackArrows f, pullbackArrows_mem f hR, ?_⟩
      rw [← Sieve.generate_le_iff, Sieve.pullbackArrows_comm]
      apply Sieve.pullback_monotone
      rwa [Sieve.generate_le_iff]
    | transitive X S T hS hT hleS hleT =>
      obtain ⟨R, hR, hle⟩ := hleS
      rw [mem_iff_exists_zeroHypercover] at hR
      obtain ⟨E, rfl⟩ := hR
      replace hleT (i : E.I₀) : ∃ (F : J.ZeroHypercover (E.X i)),
          F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows := by
        obtain ⟨R', hR', hle'⟩ := hleT (hle _ _ ⟨i⟩)
        rw [mem_iff_exists_zeroHypercover] at hR'
        obtain ⟨F, rfl⟩ := hR'
        use F
      choose F hle' using hleT
      refine ⟨(E.bind F).presieve₀, (E.bind F).mem₀, ?_⟩
      rw [Presieve.ofArrows_le_iff]
      intro i
      exact hle' _ _ _ ⟨i.snd⟩
  · rw [← Sieve.generate_le_iff] at hle
    apply GrothendieckTopology.superset_covering _ hle
    exact generate_mem_toGrothendieck hR

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cone.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
⊢ (ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)

Tactic:
have eq₁ : f₁ = (c'.pt.hom ≫ G.map (c'.π.app left).right) ≫ eqToHom (by simp) := by simp [c]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cone.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ : f₁ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app left))) ≫ eqToHom ⋯
⊢ (ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)
Module: Mathlib.CategoryTheory.Sites.CoverPreserving

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cone.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ : f₁ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app left))) ≫ eqToHom ⋯
eq₂ : f₂ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app right))) ≫ eqToHom ⋯
| (ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)

Tactic:
eq₂

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cone.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ : f₁ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app left))) ≫ eqToHom ⋯
eq₂ : f₂ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app right))) ≫ eqToHom ⋯
| (ConcreteCategory.hom (ℱ.obj.map ((c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app right))) ≫ eqToHom ⋯).op))
    (x g₂ hg₂)
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 ≤ F.restrictedTopology K.toGrothendieck

Tactic:
by
  rw [Functor.restrictedTopology]
  grw [← K.le_toPrecoverage_toGrothendieck]

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ K.W = ObjectProperty.isLocal fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj

Tactic:
rw [W_eq_isLocal_range_sheafToPresheaf_obj, ← ObjectProperty.isoClosure_isLocal]

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ (ObjectProperty.isoClosure fun x ↦ x ∈ Set.range (sheafToPresheaf K A).obj).isLocal =
    ObjectProperty.isLocal fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
x✝ : E.multicospanShape.R
⊢ x✝ = ⟨(f.inv.s₀ (f.hom.s₀ x✝.fst.1), f.inv.s₀ (f.hom.s₀ x✝.fst.2)), f.inv.s₁ (f.hom.s₁ x✝.snd)⟩

Tactic:
apply PreOneHypercover.I₁'.ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Connected

Goal state before:
pp: J α : Type u_1
F : WidePullbackShape J → α
H : ∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂
⊢ ∀ (j j' : WidePullbackShape J), F j = F j'

Tactic:
suffices ∀ i, F i = F none from fun j j' ↦ (this j).trans (this j').symm

Goal state after:
J α : Type u_1
F : WidePullbackShape J → α
H : ∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂
⊢ ∀ (i : WidePullbackShape J), F i = F none
Module: Mathlib.CategoryTheory.Limits.Shapes.Connected

Goal state before:
pp: J α : Type u_1
F : WidePushoutShape J → α
H : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂
⊢ ∀ (j j' : WidePushoutShape J), F j = F j'

Tactic:
suffices ∀ i, F i = F none from fun j j' ↦ (this j).trans (this j').symm

Goal state after:
J α : Type u_1
F : WidePushoutShape J → α
H : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂
⊢ ∀ (i : WidePushoutShape J), F i = F none
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case w
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
x✝ : E.multicospanShape.R
⊢ x✝ = ⟨(f.inv.s₀ (f.hom.s₀ x✝.fst.1), f.inv.s₀ (f.hom.s₀ x✝.fst.2)), f.inv.s₁ (f.hom.s₁ x✝.snd)⟩

Tactic:
apply PreOneHypercover.I₁'.ext <;> simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
x✝ : F.multicospanShape.R
⊢ ⟨(f.hom.s₀ (f.inv.s₀ x✝.fst.1), f.hom.s₀ (f.inv.s₀ x✝.fst.2)), f.hom.s₁ (f.inv.s₁ x✝.snd)⟩ = x✝

Tactic:
apply PreOneHypercover.I₁'.ext <;> simp

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

Goal state before:
pp: case w
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
x✝ : F.multicospanShape.R
⊢ ⟨(f.hom.s₀ (f.inv.s₀ x✝.fst.1), f.hom.s₀ (f.inv.s₀ x✝.fst.2)), f.hom.s₁ (f.inv.s₁ x✝.snd)⟩ = x✝

Tactic:
apply PreOneHypercover.I₁'.ext <;> simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over X := Over.mk (b ≫ W.hom)
⊢ g ≫ Y₁.hom = T.hom

Tactic:
dsimp [T]; rw [← Over.w a, ← reassoc_of% w, Over.w f]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
i j : E.I₀
⊢ E.toPreOneHypercover.sieve₁' i j = ⊤

Tactic:
by
  rw [eq_top_iff]
  intro Y f _
  refine ⟨pullback (E.f i) (E.f j), f, 𝟙 _, ?_, by simp⟩
  refine Presieve.ofArrows.mk' ⟨⟩ rfl ?_
  apply pullback.hom_ext <;> simp [PreOneHypercover.toPullback]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
Y : Over X
S : Sieve Y
hS : S ∈ ⇑(Sieve.overEquiv Y) ⁻¹' J Y.left
R : Sieve Y
hR : ∀ ⦃Y_1 : Over X⦄ ⦃f : Y_1 ⟶ Y⦄, S.arrows f → Sieve.pullback f R ∈ ⇑(Sieve.overEquiv Y_1) ⁻¹' J Y_1.left
Z : C
f : Z ⟶ Y.left
hf : ((Sieve.overEquiv Y) S).arrows f
⊢ Sieve.pullback f ((Sieve.overEquiv Y) R) ∈ J Z

Tactic:
specialize hR ((Sieve.overEquiv_iff _ _).1 hf)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
Y : Over X
S : Sieve Y
hS : S ∈ ⇑(Sieve.overEquiv Y) ⁻¹' J Y.left
R : Sieve Y
Z : C
f : Z ⟶ Y.left
hR : Sieve.pullback (Over.homMk f ⋯) R ∈ ⇑(Sieve.overEquiv (Over.mk (f ≫ Y.hom))) ⁻¹' J (Over.mk (f ≫ Y.hom)).left
hf : ((Sieve.overEquiv Y) S).arrows f
⊢ Sieve.pullback f ((Sieve.overEquiv Y) R) ∈ J Z
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
K : GrothendieckTopology D
F : C ⥤ D
X : C
h : CoverPreserving J K F
U : Over X
S : Sieve U
hS : (Sieve.overEquiv U) S ∈ J U.left
⊢ Sieve.functorPushforward F ((Sieve.overEquiv U) S) ∈ K ((Over.post F).obj U).left

Tactic:
exact h.cover_preserve hS

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

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
s : Y ⟶ X
R : Sieve Y
hR :
  (Sieve.overEquiv { left := Y, right := right, hom := s }).symm R ∈
    (K.toGrothendieck.over X) { left := Y, right := right, hom := s }
⊢ (Sieve.overEquiv { left := Y, right := right, hom := s }).symm R ∈
    (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Y, right := right, hom := s }

Tactic:
simp only [GrothendieckTopology.mem_over_iff, OrderIso.apply_symm_apply,
      ← Precoverage.toGrothendieck_toCoverage, Coverage.mem_toGrothendieck,
      Over.left] at hR

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
s : Y ⟶ X
R : Sieve Y
hR : K.toCoverage.Saturate Y R
⊢ (Sieve.overEquiv { left := Y, right := right, hom := s }).symm R ∈
    (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Y, right := right, hom := s }
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.obj
he : ∀ (i : ι), α.app (op (B i)) = β.app (op (B i))
i : (InducedCategory (Opens ↑X) B)ᵒᵖ
⊢ ((restrictHomEquivHom F F' h).symm α).app i = ((restrictHomEquivHom F F' h).symm β).app i

Tactic:
exact he i.unop

Goal state after: