mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
s : Meq (J.plusObj P) S
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
II : (S.bind T).Relation
⊢ (ConcreteCategory.hom ((J.plusObj P).map II.r.g₁.op))
      ((ConcreteCategory.hom ((J.toPlus P).app (op II.fst.Y))) ((fun I ↦ ↑(t I.fromMiddle) I.toMiddle) II.fst)) =
    (ConcreteCategory.hom ((J.plusObj P).map II.r.g₂.op))
      ((ConcreteCategory.hom ((J.toPlus P).app (op II.snd.Y))) ((fun I ↦ ↑(t I.fromMiddle) I.toMiddle) II.snd))

Tactic:
toPlus_apply (T II.fst.fromMiddle) (t II.fst.fromMiddle) II.fst.toMiddle,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
s : Meq (J.plusObj P) S
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
II : (S.bind T).Relation
⊢ (ConcreteCategory.hom ((J.plusObj P).map II.r.g₁.op))
      ((ConcreteCategory.hom ((J.plusObj P).map II.fst.toMiddle.f.op)) (mk (t II.fst.fromMiddle))) =
    (ConcreteCategory.hom ((J.plusObj P).map II.r.g₂.op))
      ((ConcreteCategory.hom ((J.toPlus P).app (op II.snd.Y))) ((fun I ↦ ↑(t I.fromMiddle) I.toMiddle) II.snd))
Module: Mathlib.Topology.Category.TopCat.EpiMono

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
this : Mono f ↔ Mono ((forget TopCat).map f)
⊢ Mono f ↔ Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
rw [this, CategoryTheory.mono_iff_injective]

Goal state after:
X Y : TopCat
f : X ⟶ Y
this : Mono f ↔ Mono ((forget TopCat).map f)
⊢ Function.Injective ⇑(ConcreteCategory.hom ((forget TopCat).map f)) ↔ Function.Injective ⇑(ConcreteCategory.hom f)
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
S : Cone F
x : ↑S.1
i✝ j✝ : J
f : i✝ ⟶ j✝
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (S.π.app i✝)) x) = (ConcreteCategory.hom (S.π.app j✝)) x

Tactic:
rw [← S.w f]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
S : Cone F
x : ↑S.1
i✝ j✝ : J
f : i✝ ⟶ j✝
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (S.π.app i✝)) x) =
    (ConcreteCategory.hom (S.π.app i✝ ≫ F.map f)) x
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
S : Cone F
x : ↑S.1
i j : J
f : i ⟶ j
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (S.π.app i)) x) = (ConcreteCategory.hom (S.π.app j)) x

Tactic:
rw [← S.w f]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
S : Cone F
x : ↑S.1
i j : J
f : i ⟶ j
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (S.π.app i)) x) =
    (ConcreteCategory.hom (S.π.app i ≫ F.map f)) x
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case mp
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : ↑(Y ⨯ Z)
⊢ x ∈ range ⇑(ConcreteCategory.hom (prod.map f g)) →
    x ∈
      ⇑(ConcreteCategory.hom prod.fst) ⁻¹' range ⇑(ConcreteCategory.hom f) ∩
        ⇑(ConcreteCategory.hom prod.snd) ⁻¹' range ⇑(ConcreteCategory.hom g)

pp: case mpr
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : ↑(Y ⨯ Z)
⊢ x ∈
      ⇑(ConcreteCategory.hom prod.fst) ⁻¹' range ⇑(ConcreteCategory.hom f) ∩
        ⇑(ConcreteCategory.hom prod.snd) ⁻¹' range ⇑(ConcreteCategory.hom g) →
    x ∈ range ⇑(ConcreteCategory.hom (prod.map f g))

Tactic:
· rintro ⟨y, rfl⟩
    simp_rw [Set.mem_inter_iff, Set.mem_preimage, Set.mem_range, ← ConcreteCategory.comp_apply,
      Limits.prod.map_fst, Limits.prod.map_snd, ConcreteCategory.comp_apply, exists_apply_eq_apply,
      and_self_iff]

Goal state after:
case mpr
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : ↑(Y ⨯ Z)
⊢ x ∈
      ⇑(ConcreteCategory.hom prod.fst) ⁻¹' range ⇑(ConcreteCategory.hom f) ∩
        ⇑(ConcreteCategory.hom prod.snd) ⁻¹' range ⇑(ConcreteCategory.hom g) →
    x ∈ range ⇑(ConcreteCategory.hom (prod.map f g))
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
hf : IsEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
H : Set.range ⇑(ConcreteCategory.hom g) ⊆ Set.range ⇑(ConcreteCategory.hom f)
x : ↑Y
⊢ x ∈ {y | ∃ x, (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y}

Tactic:
exact ⟨_, (H (Set.mem_range_self x)).choose_spec⟩

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case mpr.zero
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
h : IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U)
⊢ IsOpen (⇑(ConcreteCategory.hom (c.ι.app WalkingParallelPair.zero)) ⁻¹' U)

Tactic:
← c.w .left

Goal state after:
case mpr.zero
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
h : IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U)
⊢ IsOpen
    (⇑(ConcreteCategory.hom ((parallelPair f g).map WalkingParallelPairHom.left ≫ c.ι.app WalkingParallelPair.one)) ⁻¹'
      U)
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
K : Type u_3
inst✝ : Category.{v_3, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
⊢ (e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι = (Cocone.whisker e.inverse c').ι ≫ (const K).map f

Tactic:
ext k
    simpa using congr_app e' (e.inverse.obj k)

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp
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
⊢ Nonempty (IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)) → IsPushout f c.inl iY fE

Tactic:
rintro ⟨h⟩
    refine ⟨H, ⟨Limits.PushoutCocone.isColimitAux' _ ?_⟩⟩
    intro s
    dsimp
    refine ⟨BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl,
        BinaryCofan.IsColimit.inr_desc h _ _, ?_, ?_⟩
    · apply BinaryCofan.IsColimit.hom_ext hc
      · rw [← H.w_assoc]; erw [h.fac _ ⟨WalkingPair.right⟩]; exact s.condition
      · rw [← Category.assoc]; exact h.fac _ ⟨WalkingPair.left⟩
    · intro m e₁ e₂
      apply BinaryCofan.IsColimit.hom_ext h
      · dsimp
        rw [Category.assoc, e₂, eq_comm]; exact h.fac _ ⟨WalkingPair.left⟩
      · refine e₁.trans (Eq.symm ?_); exact h.fac _ _

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryPreExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)} (hc : IsColimit c), IsUniversalColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ IsUniversalColimit c

Tactic:
refine IsUniversalColimit.of_iso (@isUniversalColimit_extendCofan _ _ _ _ _ _
      (IH _ (coproductIsCoproduct _)) (FinitaryPreExtensive.universal' _ (coprodIsCoprod _ _)) ?_)
      ((extendCofanIsColimit f (coproductIsCoproduct _) (coprodIsCoprod _ _)).uniqueUpToIso hc)
    · dsimp
      infer_instance

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

Goal state before:
pp: 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₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
⊢ IsUniversalColimit (extendCofan c₁ c₂)

Tactic:
intro F c α i e hα H

Goal state after:
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₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : 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 α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
⊢ Nonempty (IsColimit c)
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
inst✝ : IsIso f
⊢ IsLocallySurjective J f

Tactic:
by
  apply isLocallySurjective_of_surjective
  intro U
  apply Function.Bijective.surjective
  rw [bijective_iff_isIso_ofHom]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows :=
  fun Y g hg ↦ Presheaf.localPreimage f.hom s g hg
Y₁ Y₂ W : C
g₁ : W ⟶ Y₁
g₂ : W ⟶ Y₂
f₁ : Y₁ ⟶ Opposite.unop X
f₂ : Y₂ ⟶ Opposite.unop X
⊢ ∀ (h₁ : (Presheaf.imageSieve f.hom s).arrows f₁) (h₂ : (Presheaf.imageSieve f.hom s).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (F.obj.map g₁.op)) (t f₁ h₁) = (ConcreteCategory.hom (F.obj.map g₂.op)) (t f₂ h₂)

Tactic:
hf₁

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows :=
  fun Y g hg ↦ Presheaf.localPreimage f.hom s g hg
Y₁ Y₂ W : C
g₁ : W ⟶ Y₁
g₂ : W ⟶ Y₂
f₁ : Y₁ ⟶ Opposite.unop X
f₂ : Y₂ ⟶ Opposite.unop X
hf₁ : (Presheaf.imageSieve f.hom s).arrows f₁
⊢ ∀ (h₂ : (Presheaf.imageSieve f.hom s).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (F.obj.map g₁.op)) (t f₁ hf₁) = (ConcreteCategory.hom (F.obj.map g₂.op)) (t f₂ h₂)
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: case mp
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:
intro
    exact isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective J f₁ f₂

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

Tactic:
rw [_root_.map_add, _root_.map_add, hr₀, hr₀']

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
R T : Presieve S
hTR : ∀ ⦃Z : C⦄ (g : Z ⟶ S), T g → ∃ Y e, R (e.hom ≫ g)
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)
⊢ T ∈ J.coverings S

Tactic:
choose YT eT hReg using hTR

Goal state after:
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)
⊢ T ∈ J.coverings S
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
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 }
e : E ≅ F :=
  PreZeroHypercover.isoMk (Equiv.refl E.I₀)
    (fun i ↦
      match i with
      | Sum.inl i => id (eR (↑i).snd ⋯).symm
      | Sum.inr i => id (eT (↑i).snd ⋯))
    ⋯
⊢ T ∈ J.coverings S

Tactic:
have hER : E.presieve₀ = R := by
    refine le_antisymm ?_ fun Y g hg ↦ .mk (Sum.inl (⟨⟨Y, g⟩, hg⟩ : R.uncurry))
    rintro - - ⟨i⟩
    match i with
    | .inl i => exact i.2
    | .inr i => apply hReg

Goal state after:
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 }
e : E ≅ F :=
  PreZeroHypercover.isoMk (Equiv.refl E.I₀)
    (fun i ↦
      match i with
      | Sum.inl i => id (eR (↑i).snd ⋯).symm
      | Sum.inr i => id (eT (↑i).snd ⋯))
    ⋯
hER : E.presieve₀ = R
⊢ T ∈ J.coverings S
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case refine_1
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K : Precoverage C
J : GrothendieckTopology C
h : K.toGrothendieck ≤ J
X : C
R : Presieve X
hR : R ∈ K.coverings X
⊢ R ∈ J.toPrecoverage.coverings X

Tactic:
rw [GrothendieckTopology.mem_toPrecoverage_iff]

Goal state after:
case refine_1
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K : Precoverage C
J : GrothendieckTopology C
h : K.toGrothendieck ≤ J
X : C
R : Presieve X
hR : R ∈ K.coverings X
⊢ Sieve.generate R ∈ J X
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
hG : CompatiblePreserving K G
ℱ : Sheaf K (Type w)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
h : x.Compatible
⊢ (FamilyOfElements.functorPushforward G x).Compatible

Tactic:
by
  rintro Z₁ Z₂ W g₁ g₂ f₁' f₂' H₁ H₂ eq
  unfold FamilyOfElements.functorPushforward
  rcases getFunctorPushforwardStructure H₁ with ⟨X₁, f₁, h₁, hf₁, rfl⟩
  rcases getFunctorPushforwardStructure H₂ with ⟨X₂, f₂, h₂, hf₂, rfl⟩
  suffices ℱ.obj.map (g₁ ≫ h₁).op (x f₁ hf₁) = ℱ.obj.map (g₂ ≫ h₂).op (x f₂ hf₂) by
    simpa using this
  apply hG.compatible ℱ h _ _ hf₁ hf₂
  simpa using eq

Goal state after:
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
s : Multifork (S.index R)
i : S.Arrow
⊢ lift hF hR s ≫ R.map i.f.op = s.ι i

Tactic:
apply (hR (op i.Y)).hom_ext

Goal state after:
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
s : Multifork (S.index R)
i : S.Arrow
⊢ ∀ (j : StructuredArrow (op i.Y) G.op),
    (lift hF hR s ≫ R.map i.f.op) ≫ ((Functor.RightExtension.mk R α).coneAt (op i.Y)).π.app j =
      s.ι i ≫ ((Functor.RightExtension.mk R α).coneAt (op i.Y)).π.app j
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
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝ : G.IsLocallyFull K
X Y : C
i : G.obj X ⟶ G.obj Y
x : (fun X ↦ X) ((G.op ⋙ ℱ).obj (op Y))
⊢ (ConcreteCategory.hom (ℱ'.obj.map i.op)) ((ConcreteCategory.hom (α.app (op Y))) x) =
    (ConcreteCategory.hom (α.app (op X))) ((ConcreteCategory.hom (ℱ.map i.op)) x)

Tactic:
have {X Y} (i : X ⟶ Y) (x) :
      ℱ'.1.map (G.map i).op (α.app _ x) = α.app _ (ℱ.map (G.map i).op x) := by
    exact ConcreteCategory.congr_hom (α.naturality i.op).symm x
  refine IsLocallyFull.ext G _ i fun V iVX iVY e ↦ ?_
  simp only [← Functor.map_comp_apply, ← op_comp, ← e, this]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
⊢ Sieve.generate (Presieve.ofArrows (trivial S).X (trivial S).f) = ⊤

Tactic:
← PreZeroHypercover.presieve₀

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S : C
⊢ Sieve.generate (trivial S).presieve₀ = ⊤
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

Goal state before:
pp: case left
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
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
⊢ Function.Injective ⇑(ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X)))

Tactic:
intro f₁ f₂ e
    refine (isPointwiseRightKanExtensionRanCounit G.op Y.1 (.op (G.obj U))).hom_ext (fun g ↦ ?_)
    obtain ⟨⟨W⟩, ⟨g : G.obj W ⟶ G.obj U⟩, rfl⟩ := g.mk_surjective
    refine (Y.2 X _ (IsDenseSubsite.imageSieve_mem J K G g)).isSeparatedFor.ext
      (fun V iVW ⟨iVU, h⟩ ↦ ?_)
    have := congr($e ≫ Y.1.map iVU.op)
    dsimp at this ⊢
    simp only [Category.assoc, ← NatTrans.naturality] at this ⊢
    simpa [h] using! this

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Presieve Y
R : Presieve Y.left := fun Z g ↦ S (Over.homMk g ⋯)
Z : C
fZ : Z ⟶ X
f : Over.mk fZ ⟶ Y
⊢ functorPullback (Over.forget X) R f = S f

Tactic:
obtain ⟨g : Z ⟶ Y.left, rfl : g ≫ Y.hom = fZ, rfl⟩ := Over.homMk_surjective f

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Presieve Y
R : Presieve Y.left := fun Z g ↦ S (Over.homMk g ⋯)
Z : C
g : Z ⟶ Y.left
⊢ functorPullback (Over.forget X) R (Over.homMk g ⋯) = S (Over.homMk g ⋯)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Presieve Y
⊢ functorPullback (Over.forget X) (map (Over.forget X) S) = S

Tactic:
let R : Presieve Y.left := fun Z g ↦ S (Over.homMk g : Over.mk (g ≫ Y.hom) ⟶ Y)
  suffices hR : (R.functorPullback (Over.forget X)) = S by
    rw [← hR, functorPullback_map_functorPullback]
  funext Z f
  obtain ⟨Z, fZ, rfl⟩ := Z.mk_surjective
  obtain ⟨g : Z ⟶ Y.left, rfl : g ≫ Y.hom = fZ, rfl⟩ := Over.homMk_surjective f
  rfl

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)
    rwa [Set.mem_preimage, Sieve.overEquiv_pullback] at hR

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroMorphisms C
D : Type u_1
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : HasZeroMorphisms D
F : C ⥤ D
inst✝⁴ : F.PreservesMonomorphisms
inst✝³ : F.PreservesZeroMorphisms
inst✝² : F.ReflectsIsomorphisms
inst✝¹ : F.Faithful
X : C
inst✝ : Simple (F.obj X)
Y : C
g : Y ⟶ X
x✝ : Mono g
⊢ F.map g ≠ 0 ↔ g ≠ 0

Tactic:
ne_eq,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroMorphisms C
D : Type u_1
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : HasZeroMorphisms D
F : C ⥤ D
inst✝⁴ : F.PreservesMonomorphisms
inst✝³ : F.PreservesZeroMorphisms
inst✝² : F.ReflectsIsomorphisms
inst✝¹ : F.Faithful
X : C
inst✝ : Simple (F.obj X)
Y : C
g : Y ⟶ X
x✝ : Mono g
⊢ ¬F.map g = 0 ↔ g ≠ 0