mathlib-initiative/mathlib-tactics huggingface dataset:
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
    (PushoutCocone.mk ((F.mapCocone (PushoutCocone.mk h i ⋯)).ι.app WalkingSpan.left)
      ((F.mapCocone (PushoutCocone.mk h i ⋯)).ι.app WalkingSpan.right) ⋯)

Tactic:
refine (IsPushout.isVanKampen_iff (H.map F)).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
⊢ ⋯.IsVanKampen
Module: Mathlib.CategoryTheory.Sites.Localization

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
inst✝ : LocallySmall.{w, v_1, u_1} C
X : C
S : Sieve X
hS : S ∈ J X
⊢ J.W (shrinkFunctor.{w, v_1, u_1} S).ι

Tactic:
intro Z hZ

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
inst✝ : LocallySmall.{w, v_1, u_1} C
X : C
S : Sieve X
hS : S ∈ J X
Z : Cᵒᵖ ⥤ Type w
hZ : Presheaf.IsSheaf J Z
⊢ Function.Bijective fun g ↦ (shrinkFunctor.{w, v_1, u_1} S).ι ≫ g
Module: Mathlib.CategoryTheory.Sites.LocallyInjective

Goal state before:
pp: case mp.refine_2
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₂ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
a✝ : IsLocallyInjective J φ
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y) ∈ J (unop X)
S : Sieve (unop X) := equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y)
T : ⦃Y : C⦄ → ⦃f : Y ⟶ unop X⦄ → S.arrows f → Sieve Y :=
  fun Y f x_1 ↦ equalizerSieve ((ConcreteCategory.hom (F₁.map f.op)) x) ((ConcreteCategory.hom (F₁.map f.op)) y)
Y : C
f : Y ⟶ unop X
hf : (equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y)).arrows f
⊢ Sieve.pullback f (Sieve.bind S.arrows T) ∈ J Y

Tactic:
refine J.superset_covering (Sieve.le_pullback_bind S.1 T _ hf)
        (equalizerSieve_mem J φ _ _ ?_)

Goal state after:
case mp.refine_2
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₂ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
a✝ : IsLocallyInjective J φ
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y) ∈ J (unop X)
S : Sieve (unop X) := equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y)
T : ⦃Y : C⦄ → ⦃f : Y ⟶ unop X⦄ → S.arrows f → Sieve Y :=
  fun Y f x_1 ↦ equalizerSieve ((ConcreteCategory.hom (F₁.map f.op)) x) ((ConcreteCategory.hom (F₁.map f.op)) y)
Y : C
f : Y ⟶ unop X
hf : (equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y)).arrows f
⊢ (ConcreteCategory.hom (φ.app (op Y))) ((ConcreteCategory.hom (F₁.map f.op)) x) =
    (ConcreteCategory.hom (φ.app (op Y))) ((ConcreteCategory.hom (F₁.map f.op)) y)
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₃
P : Cᵒᵖ ⥤ Type (max u v)
⊢ IsLocallyInjective J (J.toSheafify P)

Tactic:
by
  dsimp [GrothendieckTopology.toSheafify]
  rw [GrothendieckTopology.plusMap_toPlus]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} 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
U : C
s : ToType (G.obj (op U))
V : C
g✝ : V ⟶ U
W : C
g : W ⟶ V
⊢ (Sieve.pullback g✝ (imageSieve f s)).arrows g ↔ (imageSieve f ((ConcreteCategory.hom (G.map g✝.op)) s)).arrows g

Tactic:
simp [imageSieve]

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

Goal state before:
pp: case refine_2
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✝¹ : IsLocallySurjective J (f₁ ≫ f₂)
inst✝ : IsLocallyInjective J f₂
X : C
x : ToType (F₂.obj (op X))
S : Sieve X := imageSieve (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x)
T : ⦃Y : C⦄ → (f : Y ⟶ X) → S.arrows f → Sieve Y :=
  fun Y f hf ↦
    equalizerSieve
      ((ConcreteCategory.hom (f₁.app (op Y))) (localPreimage (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x) f hf))
      ((ConcreteCategory.hom (F₂.map f.op)) x)
Y : C
f : Y ⟶ unop (op X)
hf : (imageSieve (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x)).arrows f
⊢ (ConcreteCategory.hom (f₂.app (op Y)))
      ((ConcreteCategory.hom (f₁.app (op Y)))
        (localPreimage (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x) f hf)) =
    (ConcreteCategory.hom (f₁.app (op Y) ≫ f₂.app (op Y)))
      (localPreimage (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x) f hf)

Tactic:
ConcreteCategory.comp_apply

Goal state after:
case refine_2
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✝¹ : IsLocallySurjective J (f₁ ≫ f₂)
inst✝ : IsLocallyInjective J f₂
X : C
x : ToType (F₂.obj (op X))
S : Sieve X := imageSieve (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x)
T : ⦃Y : C⦄ → (f : Y ⟶ X) → S.arrows f → Sieve Y :=
  fun Y f hf ↦
    equalizerSieve
      ((ConcreteCategory.hom (f₁.app (op Y))) (localPreimage (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x) f hf))
      ((ConcreteCategory.hom (F₂.map f.op)) x)
Y : C
f : Y ⟶ unop (op X)
hf : (imageSieve (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x)).arrows f
⊢ (ConcreteCategory.hom (f₂.app (op Y)))
      ((ConcreteCategory.hom (f₁.app (op Y)))
        (localPreimage (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x) f hf)) =
    (ConcreteCategory.hom (f₂.app (op Y)))
      ((ConcreteCategory.hom (f₁.app (op Y))) (localPreimage (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x) f hf))
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
P : Cᵒᵖ ⥤ Type (max u v)
⊢ IsLocallySurjective J (J.toSheafify P)

Tactic:
by
  dsimp [GrothendieckTopology.toSheafify]
  rw [GrothendieckTopology.plusMap_toPlus]
  infer_instance

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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
s : (i : ι) → PullbackCone (f i) v
hs : (i : ι) → IsLimit (s i)
t : PullbackCone u v
ht : IsLimit t
d : Cofan fun i ↦ (s i).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
he₁ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.fst = (s i).fst ≫ a.inj i
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd
iso : d ≅ Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht ((s i).fst ≫ a.inj i) (s i).snd ⋯ := Cofan.ext e ⋯
j : Discrete ι
⊢ IsPullback ((Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht ((s i).fst ≫ a.inj i) (s i).snd ⋯).ι.app j)
    ((Discrete.natTrans fun i ↦ (s i.as).fst).app j) t.fst (a.ι.app j)

Tactic:
simp only [Discrete.functor_obj_eq_as, Cofan.mk_pt, Functor.const_obj_obj, Cofan.mk_ι_app,
      Discrete.natTrans_app]
    rw [← Cofan.inj]
    refine IsPullback.of_right ?_ (by simp) (IsPullback.of_isLimit ht).flip
    simpa [hu] using (IsPullback.of_isLimit (hs j.1)).flip

Goal state after:
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
X Y : Cᵒᵖ
f : X ⟶ Y
m : ↥(N.obj X)
⊢ ↑((ConcreteCategory.hom (N.toPresheafOfModules.map f)) m) = (ConcreteCategory.hom (M.map f)) ↑m

Tactic:
by
  rfl

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

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

Tactic:
(A.obj.map f.op).hom.map_zero

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
m : ↑(A.obj.obj X)
Y : C
f : Y ⟶ Opposite.unop X
m₀ : ToType (M₀.presheaf.obj (Opposite.op Y))
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.obj.map f.op)) m
⊢ 0 = 0
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
I J : Type u
⊢ coprod.inr ≫ (freeSumIso I J).hom = freeMap Sum.inr

Tactic:
by
  rw [← dsimp% freeFunctor_map (↾(Sum.inr : J → I ⊕ J))]
  exact IsColimit.comp_coconePointUniqueUpToIso_hom
    (coprodIsCoprod (free (R := R) I) (free J)) _ (.mk .right)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ Dᵒᵖ
inst✝ : ReflectsFiniteCoproducts F
x✝ : ℕ
⊢ ReflectsLimitsOfShape (Discrete (Fin x✝)) F.leftOp

Tactic:
by
    apply +allowSynthFailures reflectsLimitsOfShape_leftOp
    exact reflectsColimitsOfShape_of_equiv (Discrete.opposite _).symm _

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

Tactic:
ConcreteCategory.comp_apply

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✝) :=
  Presheaf.imageSieve α ((ConcreteCategory.hom (R.obj.map π)) r) ⊓
    Presheaf.imageSieve φ ((ConcreteCategory.hom (A.obj.map π)) m)
hS : S ∈ J (Opposite.unop Y✝)
Y : C
f : Y ⟶ Opposite.unop Y✝
r₀ : ToType (R₀.obj (Opposite.op Y))
hr₀ :
  (RingCat.Hom.hom (α.app (Opposite.op Y))) r₀ = (RingCat.Hom.hom (R.obj.map f.op)) ((RingCat.Hom.hom (R.obj.map π)) r)
m₀ : ToType (M₀.presheaf.obj (Opposite.op Y))
hm₀ :
  (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ =
    (ConcreteCategory.hom (A.obj.map f.op)) ((ConcreteCategory.hom (A.obj.map π)) m)
⊢ (ConcreteCategory.hom (A.obj.map f.op)) ((ConcreteCategory.hom (A.obj.map π)) m) =
    (ConcreteCategory.hom (A.obj.map f.op)) ((ConcreteCategory.hom (A.obj.map π)) m)
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝ : RepresentablyFlat F.op
X : D
⊢ IsFiltered (CostructuredArrow F X)

Tactic:
suffices IsCofiltered (CostructuredArrow F X)ᵒᵖ from isFiltered_of_isCofiltered_op _

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝ : RepresentablyFlat F.op
X : D
⊢ IsCofiltered (CostructuredArrow F X)ᵒᵖ
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
⊢ Presieve.IsSheaf J₁ (Functor.closedSieves J₁).toFunctor

Tactic:
by
  intro X S hS
  rw [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]
  refine ⟨?_, ?_⟩
  · 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)
  · intro x hx
    rw [Presieve.compatible_iff_sieveCompatible] at hx
    let M := Sieve.bind S fun Y f hf => (x f hf).1
    have : ∀ ⦃Y⦄ (f : Y ⟶ X) (hf : S f), M.pullback f = (x f hf).1 := by
      intro Y f hf
      apply le_antisymm
      · rintro Z u ⟨W, g, f', hf', hg : (x f' hf').1.1 _, c⟩
        rw [Sieve.mem_iff_pullback_eq_top,
          ← show (x (u ≫ f) _).1 = (x f hf).1.pullback u from congr_arg Subtype.val (hx f u hf)]
        conv_lhs => congr; congr; rw [← c] -- Porting note: Originally `simp_rw [← c]`
        rw [show (x (g ≫ f') _).1 = _ from congr_arg Subtype.val (hx f' g hf')]
        apply Sieve.pullback_eq_top_of_mem _ hg
      · apply Sieve.le_pullback_bind S fun Y f hf => (x f hf).1
    refine ⟨⟨_, J₁.close_isClosed M⟩, ?_⟩
    intro Y f hf
    dsimp
    ext1
    dsimp
    rw [← J₁.pullback_close, this _ hf]
    apply le_antisymm (J₁.le_close_of_isClosed le_rfl (x f hf).2) (J₁.le_close _)

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

Goal state before:
pp: case mk.mk
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
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 ≫ F.f (s₀✝¹ i) = E.f i
s₀✝ : E.I₀ → F.I₀
h₀✝ : (i : E.I₀) → E.X i ⟶ F.X (s₀✝ i)
w₀✝ : ∀ (i : E.I₀), h₀✝ i ≫ F.f (s₀✝ i) = E.f i
hs : { s₀ := s₀✝¹, h₀ := h₀✝¹, w₀ := w₀✝¹ }.s₀ = { s₀ := s₀✝, h₀ := h₀✝, w₀ := w₀✝ }.s₀
hh : ∀ (i : E.I₀), { s₀ := s₀✝¹, h₀ := h₀✝¹, w₀ := w₀✝¹ }.h₀ i = { s₀ := s₀✝, h₀ := h₀✝, w₀ := w₀✝ }.h₀ i ≫ eqToHom ⋯
⊢ { s₀ := s₀✝¹, h₀ := h₀✝¹, w₀ := w₀✝¹ } = { s₀ := s₀✝, h₀ := h₀✝, w₀ := w₀✝ }

Tactic:
simp only at hs

Goal state after:
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
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 ≫ F.f (s₀✝¹ i) = E.f i
s₀✝ : E.I₀ → F.I₀
h₀✝ : (i : E.I₀) → E.X i ⟶ F.X (s₀✝ i)
w₀✝ : ∀ (i : E.I₀), h₀✝ i ≫ F.f (s₀✝ i) = E.f i
hs : s₀✝¹ = s₀✝
hh : ∀ (i : E.I₀), { s₀ := s₀✝¹, h₀ := h₀✝¹, w₀ := w₀✝¹ }.h₀ i = { s₀ := s₀✝, h₀ := h₀✝, w₀ := w₀✝ }.h₀ i ≫ eqToHom ⋯
⊢ { s₀ := s₀✝¹, h₀ := h₀✝¹, w₀ := w₀✝¹ } = { s₀ := s₀✝, h₀ := h₀✝, w₀ := w₀✝ }
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasIsos
X : C
E F : PreZeroHypercover X
e : E ≅ F
hE : E.presieve₀ ∈ K.coverings X
⊢ F.presieve₀ ∈ K.coverings X

Tactic:
have : F.presieve₀ =
      Presieve.ofArrows (fun (i : Σ (_ : F.I₀), Unit) ↦ _) (fun i ↦ e.inv.h₀ i.1 ≫ E.f _) := by
    simp only [Hom.w₀]
    refine le_antisymm ?_ ?_
    · rw [Presieve.ofArrows_le_iff]
      intro i
      exact .mk (⟨i, ⟨⟩⟩ : Σ (_ : F.I₀), Unit)
    · simp [Presieve.ofArrows_le_iff]
  rw [this]
  refine K.comp_mem_coverings (fun i ↦ E.f (e.inv.s₀ i)) ?_ (fun i (k : Unit) ↦ e.inv.h₀ i) ?_
  · rwa [← E.presieve₀_reindex (PreZeroHypercover.equivOfIso e.symm)] at hE
  · intro i
    rw [Presieve.ofArrows_pUnit]
    exact K.mem_coverings_of_isIso _

Goal state after:
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✝
S T : C
f : S ⟶ T
E : PreZeroHypercover T
inst✝¹ : ∀ (i : E.I₀), HasPullback f (E.f i)
inst✝ : ∀ (i : E.I₀), HasPullback (E.f i) f
⊢ { s₀ := id, h₀ := fun i ↦ (pullbackSymmetry f (E.f i)).hom, w₀ := ⋯ } ≫
      { s₀ := id, h₀ := fun i ↦ (pullbackSymmetry f (E.f i)).inv, w₀ := ⋯ } =
    𝟙 (pullback₁ f E)

Tactic:
by
    apply Hom.ext (by rfl)
    simp only [heq_eq_eq]
    ext i
    simp

Goal state after:
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✝
S T : C
f : S ⟶ T
E : PreZeroHypercover T
inst✝¹ : ∀ (i : E.I₀), HasPullback f (E.f i)
inst✝ : ∀ (i : E.I₀), HasPullback (E.f i) f
⊢ { s₀ := id, h₀ := fun i ↦ (pullbackSymmetry f (E.f i)).inv, w₀ := ⋯ } ≫
      { s₀ := id, h₀ := fun i ↦ (pullbackSymmetry f (E.f i)).hom, w₀ := ⋯ } =
    𝟙 (pullback₂ f E)

Tactic:
by
    apply Hom.ext (by rfl)
    simp only [heq_eq_eq]
    ext i
    simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
E F : PreZeroHypercover S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
⊢ F.presieve₀ ∈ J.coverings S

Tactic:
by
  refine Precoverage.RespectsIso.of_forall_exists_iso ?_ ?_ hE
  · intro Z _ ⟨i⟩
    use F.X (e.hom.s₀ i), (asIso (e.hom.h₀ i)).symm
    simp
  · intro Z _ ⟨i⟩
    use E.X (e.inv.s₀ i), (asIso (e.inv.h₀ i)).symm
    simp

Goal state after:
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.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
i : F.I₀
⊢ F.X i ⟶ E.X (e.inv.s₀ i)

pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
⊢ ∀ (i : F.I₀), IsPullback (F.f i) ?refine_2 (𝟙 S) (E.f (e.inv.s₀ i))

Tactic:
· exact e.inv.h₀ i

Goal state after:
case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
⊢ ∀ (i : F.I₀), IsPullback (F.f i) (e.inv.h₀ i) (𝟙 S) (E.f (e.inv.s₀ i))
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
this : G.IsRightAdjoint
⊢ G.IsContinuous K J

Tactic:
apply Functor.isContinuous_of_coverPreserving (compatiblePreservingOfFlat J G)

Goal state after:
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
this : G.IsRightAdjoint
⊢ CoverPreserving K J G
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
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X : C
⊢ mapPreimage K G F (𝟙 (G.obj X)) = 𝟙 (F.obj.obj (op X))

Tactic:
rw [← G.map_id, mapPreimage_map, op_id, map_id]

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 : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
i : E.I₀
⊢ F.X (g.s₀ i) = F.X (f.s₀ i)

Tactic:
by simp [hs₀]

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 : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
hh₀ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
i j : E.I₀
k : E.I₁ i j
⊢ g.s₀ i = f.s₀ i

Tactic:
by simp [hs₀]

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 : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
hh₀ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
i j : E.I₀
k : E.I₁ i j
⊢ g.s₀ j = f.s₀ j

Tactic:
by simp [hs₀]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
X✝ : C
J✝ J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
⊢ Presheaf.IsSheaf J (CategoryTheory.yoneda.obj X)

Tactic:
rw [isSheaf_iff_isSheaf_of_type]
    apply Subcanonical.isSheaf_of_isRepresentable

Goal state after: