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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category.{t, w} D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Cᵒᵖ ⥤ D
W : (J.Cover X)ᵒᵖ
⊢ ∀ (s : Cone (F ⋙ J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W)) (j : K),
    liftToDiagramLimitObj F s ≫
        ((J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W).mapCone (limit.cone F)).π.app j =
      s.π.app j

Tactic:
by
          intro E k
          dsimp [diagramNatTrans]
          refine Multiequalizer.hom_ext _ _ _ (fun a => ?_)
          simp only [Multiequalizer.lift_ι, Multiequalizer.lift_ι_assoc, Category.assoc,
            liftToDiagramLimitObjAux_fac]

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

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
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : D
f : X ⟶ Y
⊢ isLocal (fun x ↦ x ∈ Set.range F.obj) f ↔ IsIso (G.map f)

Tactic:
have := adj.unit.naturality f

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
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : D
f : X ⟶ Y
this : (𝟭 D).map f ≫ adj.unit.app Y = adj.unit.app X ≫ (G ⋙ F).map f
⊢ isLocal (fun x ↦ x ∈ Set.range F.obj) f ↔ IsIso (G.map f)
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
U : C
s : ToType (G.obj (op U))
V W : C
i : V ⟶ U
t : ToType (F.obj (op V))
ht : (ConcreteCategory.hom (f.app (op V))) t = (ConcreteCategory.hom (G.map i.op)) s
j : W ⟶ V
⊢ (ConcreteCategory.hom (f.app (op W))) ((ConcreteCategory.hom (F.map j.op)) t) =
    (ConcreteCategory.hom (G.map j.op)) ((ConcreteCategory.hom (f.app (op V))) t)

Tactic:
NatTrans.naturality_apply f

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
U : C
s : ToType (G.obj (op U))
V W : C
i : V ⟶ U
t : ToType (F.obj (op V))
ht : (ConcreteCategory.hom (f.app (op V))) t = (ConcreteCategory.hom (G.map i.op)) s
j : W ⟶ V
⊢ (ConcreteCategory.hom (G.map j.op)) ((ConcreteCategory.hom (f.app (op V))) t) =
    (ConcreteCategory.hom (G.map j.op)) ((ConcreteCategory.hom (f.app (op V))) t)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_2.refine_1.isFalse
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 : ι
h✝ : ¬j = i
⊢ initial.to (X i) ≫ eqToHom ⋯ ≫ t.inj i = inv (eqToHom ⋯) ≫ t.inj j

Tactic:
exact initialIsInitial.hom_ext _ _

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S : C
ι : Type u_2
inst✝ : Small.{max w v, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan fun i ↦ uliftYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
e : (Discrete.functor fun i ↦ uliftYoneda.{w, v, u}.obj (X i)) ≅
  Discrete.functor fun i ↦ shrinkYoneda.{max w v, v, u}.obj (X i) :=
  Discrete.natIso fun i ↦ uliftYonedaIsoShrinkYoneda.app (X i.as)
hc' : IsColimit ((Cocone.precompose e.inv).obj c) := (IsColimit.precomposeInvEquiv e c).invFun hc
i : ι
⊢ c.inj i ≫ (Cofan.IsColimit.desc hc fun i ↦ uliftYoneda.{w, v, u}.map (f i)) ≫ uliftYonedaIsoShrinkYoneda.hom.app S =
    c.inj i ≫ Cofan.IsColimit.desc hc' fun i ↦ shrinkYoneda.{max v w, v, u}.map (f i)

Tactic:
rw [Cofan.IsColimit.fac_assoc, NatTrans.naturality,
        ← Cofan.IsColimit.fac hc' (fun i ↦ shrinkYoneda.map (f i)) i]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S : C
ι : Type u_2
inst✝ : Small.{max w v, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan fun i ↦ uliftYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
e : (Discrete.functor fun i ↦ uliftYoneda.{w, v, u}.obj (X i)) ≅
  Discrete.functor fun i ↦ shrinkYoneda.{max w v, v, u}.obj (X i) :=
  Discrete.natIso fun i ↦ uliftYonedaIsoShrinkYoneda.app (X i.as)
hc' : IsColimit ((Cocone.precompose e.inv).obj c) := (IsColimit.precomposeInvEquiv e c).invFun hc
i : ι
⊢ (uliftYonedaIsoShrinkYoneda.hom.app (X i) ≫
      Cofan.inj ((Cocone.precompose e.inv).obj c) i ≫
        Cofan.IsColimit.desc hc' fun i ↦ shrinkYoneda.{max v w, v, u}.map (f i)) =
    c.inj i ≫ Cofan.IsColimit.desc hc' fun i ↦ shrinkYoneda.{max v w, v, u}.map (f i)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: 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₀'))

Tactic:
intro Z g hg
    rw [← NatTrans.naturality_apply (D := Ab), ← NatTrans.naturality_apply (D := Ab)]
    erw [M₀.map_smul, M₀.map_smul, hg.1, hg.2]
    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 Y✝ : Cᵒᵖ
π : X ⟶ Y✝
r r' : ↑(R.obj.obj X)
m m' : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X)
hS : S ∈ J (Opposite.unop X)
r₀ : Presieve.FamilyOfElements (R₀ ⋙ forget RingCat) S.arrows
m₀ : Presieve.FamilyOfElements (M₀.presheaf ⋙ forget Ab) S.arrows
hr₀ : (r₀.map (whiskerRight α (forget RingCat))).IsAmalgamation r
hm₀ : (m₀.map (whiskerRight φ (forget Ab))).IsAmalgamation m
a : ↑(A.obj.obj X)
ha : ((r₀.smul m₀).map (whiskerRight φ (forget Ab))).IsAmalgamation a
Y : Cᵒᵖ
f : X ⟶ Y
a₀ : ↑(R₀.obj Y)
ha₀ : (ConcreteCategory.hom (α.app Y)) a₀ = (ConcreteCategory.hom (R.obj.map f)) r
b₀ : ↑(M₀.obj Y)
hb₀ : (ConcreteCategory.hom (φ.app Y)) b₀ = (ConcreteCategory.hom (A.obj.map f)) m
Z : C
g : Z ⟶ Opposite.unop Y
hg : S.arrows (g ≫ f.unop)
⊢ (ConcreteCategory.hom (A.obj.map f ≫ A.obj.map g.op)) a =
    (ConcreteCategory.hom (A.obj.map g.op)) ((ConcreteCategory.hom (φ.app Y)) (a₀ • b₀))

Tactic:
← A.obj.map_comp,

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

Tactic:
rw [map_smul_eq α φ 0 m f.op 0 (by simp) m₀ hm₀, zero_smul, map_zero,
    (A.obj.map f.op).hom.map_zero]

Goal state after:
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 : Type u
M : SheafOfModules R
f : I → M.sections
i : I
⊢ sectionsMap (M.freeHomEquiv.symm f) (freeSection i) = f i

Tactic:
obtain ⟨f, rfl⟩ := (freeHomEquiv M).surjective f

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : HasWeakSheafify J AddCommGrpCat
inst✝ : J.WEqualsLocallyBijective AddCommGrpCat
I : Type u
M : SheafOfModules R
i : I
f : free I ⟶ M
⊢ sectionsMap (M.freeHomEquiv.symm (M.freeHomEquiv f)) (freeSection i) = M.freeHomEquiv f i
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : Sieve X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
this : J.IsClosed ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ J.close ⊤ = ⊤

Tactic:
J.close_eq_top_iff_mem

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : Sieve X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
this : J.IsClosed ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ⊤ ∈ J Y
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ Presieve.IsSheaf J₂ (Functor.closedSieves J₁).toFunctor

Tactic:
rw [← h]

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ Presieve.IsSheaf J₁ (Functor.closedSieves J₁).toFunctor
Module: Mathlib.CategoryTheory.Sites.Continuous

Goal state before:
pp: case refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
T : D
f : T ⟶ F.obj W
k : (E.map F).I₁ i₁ i₂
u : T ⟶ (E.map F).Y k
hf₁ : f ≫ F.map p₁ = u ≫ (E.map F).p₁ k
hf₂ : f ≫ F.map p₂ = u ≫ (E.map F).p₂ k
l : W ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift p₁ p₂ h
hl₁ : l ≫ pullback.fst (E.f i₁) (E.f i₂) = p₁
hl₂ : l ≫ pullback.snd (E.f i₁) (E.f i₂) = p₂
r : E.Y k ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift (E.p₁ k) (E.p₂ k) ⋯
⊢ (E.sieve₁ p₁ p₂).arrows (pullback.fst l r)

Tactic:
refine ⟨k, pullback.snd _ _, ?_, ?_⟩ <;> simp [← hl₁, ← hl₂, pullback.condition_assoc, r]

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

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

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

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
inst✝³ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝² : G.IsContinuous J K
inst✝¹ : HasWeakSheafify J A
inst✝ : HasWeakSheafify K A
F : Dᵒᵖ ⥤ A
adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A
adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := sheafificationAdjunction K A
adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := G.sheafAdjunctionCocontinuous A J K
eq :
  adj₁.unit.app F ≫
      G.op.ran.map (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F)) ≫
        G.op.ran.map ((sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) =
    adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))
⊢ adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F)) =
    (adj₁.homEquiv F ((sheafToPresheaf J A).obj ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F)))
      (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F))

Tactic:
apply (adj₁.homEquiv _ _).symm.injective

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
inst✝³ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝² : G.IsContinuous J K
inst✝¹ : HasWeakSheafify J A
inst✝ : HasWeakSheafify K A
F : Dᵒᵖ ⥤ A
adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := ⋯
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := ⋯
adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := ⋯
adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := ⋯
eq :
  adj₁.unit.app F ≫
      G.op.ran.map (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F)) ≫
        G.op.ran.map ((sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) =
    adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))
⊢ (adj₁.homEquiv F
          ((sheafToPresheaf J A).obj ((G.sheafPushforwardContinuous A J K).obj ((presheafToSheaf K A).obj F)))).symm
      (adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))) =
    (adj₁.homEquiv F
          ((sheafToPresheaf J A).obj ((G.sheafPushforwardContinuous A J K).obj ((presheafToSheaf K A).obj F)))).symm
      ((adj₁.homEquiv F ((sheafToPresheaf J A).obj ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F)))
        (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F)))
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
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_5)
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₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
V₁ : C
iVW : V₁ ⟶ W
iV₁Y₁ : V₁ ⟶ Y₁
e₁ : G.map iV₁Y₁ = G.map iVW ≫ i ≫ f₁
V₂ : C
iV₂V₁ : V₂ ⟶ V₁
iV₂Y₂ : V₂ ⟶ Y₂
e₂ : G.map iV₂Y₂ = G.map iV₂V₁ ≫ G.map iVW ≫ i ≫ f₂
V₃ : C
iV₃ : V₃ ⟶ V₂
e₄ : iV₃ ≫ iV₂V₁ ≫ iV₁Y₁ ≫ g₁ = iV₃ ≫ iV₂Y₂ ≫ g₂
⊢ (iV₃ ≫ iV₂V₁ ≫ iV₁Y₁) ≫ g₁ = (iV₃ ≫ iV₂Y₂) ≫ g₂

Tactic:
simpa using e₄

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

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
J : GrothendieckTopology C
h : F.IsContinuous J K
P : Sheaf K (Type (max u₁ v₁ u₂ v₂))
⊢ Presieve.IsSheaf J ((fun G ↦ F.op ⋙ G.obj) P)

Tactic:
exact Functor.op_comp_isSheaf_of_types F J K P

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
e✝ : C ≌ D
G : D ⥤ C
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
inst✝ : G.IsEquivalence
U : C
e : C ≌ D := G.asEquivalence.symm
Y : C
f : Y ⟶ U
g : e.inverse.obj (e.functor.obj Y) ⟶ U := e.unitInv.app Y ≫ f
this : (Sieve.coverByImage e.inverse U).arrows (e.unit.app Y ≫ g)
⊢ (Sieve.coverByImage G U).arrows f

Tactic:
simpa [g] using! this

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

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

Tactic:
PreOneHypercover.inv_hom_h₀_assoc

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
⊢ J.CoversTop Y → Sieve.ofObjects Y X ∈ J X

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
⊢ Sieve.ofObjects Y X ∈ J X → J.CoversTop Y

Tactic:
· tauto

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
⊢ Sieve.ofObjects Y X ∈ J X → J.CoversTop Y
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
⊢ Sieve.ofObjects Y X ∈ J X → J.CoversTop Y

Tactic:
intro h W
    apply J.superset_covering _ (J.pullback_stable (hX.from W) h)
    rintro T a ⟨i, ⟨b⟩⟩
    exact ⟨i, ⟨b⟩⟩

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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y
⊢ generate (Presieve.functorPushforward (Over.forget X) R) ≤ (overEquiv Y) (generate R)

Tactic:
rw [generate_le_iff]
    rintro Z g ⟨W, u, v, hu, rfl⟩
    exact (overEquiv_iff _ _).mpr ⟨W, Over.homMk v, u, hu, 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 Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
⊢ (ConcreteCategory.hom (F.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (F.obj.map f₂.op)) (x g₂ hg₂)

Tactic:
let W' : Over X := Over.mk (f₁.left ≫ Y₁.hom)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
⊢ (ConcreteCategory.hom (F.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (F.obj.map f₂.op)) (x g₂ hg₂)
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: case pair.pair.id_pair
C : Type u_1
inst✝² : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
h : F.IsCompatible U sf
G : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ Type u_4 := (Pairwise.diagram U).op ⋙ F
i j : ι
⊢ (ConcreteCategory.hom (((Pairwise.diagram U).op ⋙ F).map (op (Pairwise.Hom.id_pair i j))))
      (objPairwiseOfFamily sf (op (Pairwise.pair i j))) =
    objPairwiseOfFamily sf (op (Pairwise.pair i j))

Tactic:
· exact ConcreteCategory.congr_hom (G.map_id <| op <| Pairwise.pair i j) _

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: case refine_2
X : TopCat
F : Presheaf (Type u_4) X
ι : Type x
U : ι → Opens ↑X
h :
  ∀ (sf : (i : ι) → ToType (F.obj (op (U i)))),
    F.IsCompatible U sf →
      ∃! s,
        ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
          (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app i)) s = objPairwiseOfFamily sf i
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → ((Pairwise.diagram U).op ⋙ F).obj j
hs : s ∈ ((Pairwise.diagram U).op ⋙ F).sections
⊢ ∃! x,
    ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app j)) x = s j

Tactic:
specialize h (fun i ↦ s <| op <| Pairwise.single i) fun i j ↦
      (hs <| op <| Pairwise.Hom.left i j).trans (hs <| op <| Pairwise.Hom.right i j).symm
    convert! h; ext (i | ⟨i, j⟩)
    · rfl
    · exact (hs <| op <| Pairwise.Hom.left i j).symm

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
ι : Type u_4
U : ι → Opens ↑X
s t : ToType (F.obj.obj (op (iSup U)))
h :
  ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s = (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) t
sf : (i : ι) → ToType (F.obj.obj (op (U i))) := fun i ↦ (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s
sf_compatible : IsCompatible F.obj U sf
gl : ToType (F.obj.obj (op (iSup U)))
gl_uniq : ∀ (y : ToType (F.obj.obj (op (iSup U)))), (fun s ↦ IsGluing F.obj U sf s) y → y = gl
i : ι
⊢ (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) t = sf i

Tactic:
rw [← h]

Goal state after: