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

Goal state before:
pp: case refine_1.of
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
J : Pretopology C
T : C
S✝ : Sieve T
X : C
S : Presieve X
hS : S ∈ J.toCoverage.coverings X
⊢ ∃ R ∈ J.coverings X, R ≤ (Sieve.generate S).arrows

Tactic:
| of X S hS =>

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

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
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
inst✝ : H.IsGenerating
⊢ Presheaf.IsSheaf J P → ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))

Tactic:
intro hP X E _

Goal state after:
case mp
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
inst✝ : H.IsGenerating
hP : Presheaf.IsSheaf J P
X : C
E : J.OneHypercover X
x✝ : H E
⊢ Nonempty (IsLimit (E.multifork P))
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} B
inst✝³ : Category.{v_3, u_3} C
inst✝² : Category.{v_4, u_4} D
G : B ⥤ D
F : A ⥤ B
L : A ⥤ C
inst✝¹ : G.PreservesLeftKanExtension F L
inst✝ : L.HasLeftKanExtension F
⊢ whiskerRight (L.leftKanExtensionUnit F) G ≫
      (L.associator (L.leftKanExtension F) G).hom ≫ L.whiskerLeft (G.leftKanExtensionCompIsoOfPreserves F L).hom =
    L.leftKanExtensionUnit (F ⋙ G)

Tactic:
simpa [leftKanExtensionCompIsoOfPreserves] using
    descOfIsLeftKanExtension_fac
      (α := whiskerRight (L.leftKanExtensionUnit F) G ≫ (Functor.associator _ _ _).hom)
      (β := L.leftKanExtensionUnit (F ⋙ G))

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

Goal state before:
pp: case refine_2.of
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K : Precoverage C
J : GrothendieckTopology C
h : K ≤ J.toPrecoverage
X✝ : C
R : Sieve X✝
X : C
S : Presieve X
hS : S ∈ K.coverings X
⊢ Sieve.generate S ∈ J X

Tactic:
| of X S hS =>

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
X : D
S : K.Cover X
s : Multifork (S.index R)
Y : C
f : G.obj Y ⟶ X
W : C
g : W ⟶ Y
i : S.Arrow
h : G.obj W ⟶ i.Y
w : h ≫ i.f = G.map g ≫ f
⊢ s.ι { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ } ≫ α.app (op W) = s.ι i ≫ R.map h.op ≫ α.app (op W)

Tactic:
simp only [← Category.assoc]

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
X : D
S : K.Cover X
s : Multifork (S.index R)
Y : C
f : G.obj Y ⟶ X
W : C
g : W ⟶ Y
i : S.Arrow
h : G.obj W ⟶ i.Y
w : h ≫ i.f = G.map g ≫ f
⊢ s.ι { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ } ≫ α.app (op W) = (s.ι i ≫ R.map h.op) ≫ α.app (op W)
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 := ⋯
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 := ⋯
⊢ (adj₁.homEquiv F ((sheafToPresheaf J A).obj ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F)))
      (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F) ≫
        (sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app 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:
have eq := (adj₁.comp adj₂).unit_leftAdjointUniq_hom_app (adj₃.comp adj₄) 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
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₁.comp adj₂).unit.app F ≫
      (sheafToPresheaf J A ⋙ G.op.ran).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F) =
    (adj₃.comp adj₄).unit.app F
⊢ (adj₁.homEquiv F ((sheafToPresheaf J A).obj ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F)))
      (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F) ≫
        (sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app 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))
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
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
W : D
Z : C
iWZ : W ⟶ G.obj Z
iZY : G.obj Z ⟶ Y
⊢ Sieve.pullback (iWZ ≫ iZY) (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T))) ∈ K W

Tactic:
rw [Sieve.pullback_comp]

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
K : GrothendieckTopology D
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
W : D
Z : C
iWZ : W ⟶ G.obj Z
iZY : G.obj Z ⟶ Y
⊢ Sieve.pullback iWZ
      (Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T)))) ∈
    K W
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.obj ≅ G.op ⋙ ℱ'.obj
⊢ ℱ.obj ≅ ℱ'.obj

Tactic:
have : ∀ X : Dᵒᵖ, IsIso ((sheafHom i.hom).app X) := by
    intro X
    rw [← isIso_iff_of_reflects_iso _ yoneda]
    use (sheafYonedaHom i.inv).app X
    constructor <;> ext x : 2 <;>
      simp only [sheafHom, NatTrans.comp_app, NatTrans.id_app, Functor.map_preimage]
    · exact ((Types.presheafIso (isoOver i (unop x))).app X).hom_inv_id
    · exact ((Types.presheafIso (isoOver i (unop x))).app X).inv_hom_id

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
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.obj ≅ G.op ⋙ ℱ'.obj
this : ∀ (X : Dᵒᵖ), IsIso ((sheafHom i.hom).app X)
⊢ ℱ.obj ≅ ℱ'.obj
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
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
f : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
𝒢' : Sheaf K A
g : ℱ' ⟶ 𝒢'
⊢ restrictHomEquivHom.symm (restrictHomEquivHom (f ≫ G.op.whiskerLeft g.hom)) =
    restrictHomEquivHom.symm (restrictHomEquivHom f ≫ g.hom)

Tactic:
simpa only [Equiv.symm_apply_apply] using
    (restrictHomEquivHom_naturality_right_symm (G := G) (restrictHomEquivHom f) g).symm

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

Goal state before:
pp: case refine_2
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
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
W₁ : C
g₁ : G.obj W₁ ⟶ G.obj U
W₂ : C
i : W₂ ⟶ W₁
hi : (StructuredArrow.mk (op g₁)).hom ≫ G.op.map (op i) = (StructuredArrow.mk (op (G.map i ≫ g₁))).hom
⊢ ∀ (I : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve (G.map i ≫ g₁), ⋯⟩),
    ⋯.amalgamate ⟨G.imageSieve (G.map i ≫ g₁), ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y W₂ U I.f (G.map i ≫ g₁) ⋯).op) ⋯ ≫
        Y.obj.map I.f.op =
      (⋯.amalgamate ⟨G.imageSieve g₁, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y W₁ U I.f g₁ ⋯).op) ⋯ ≫ Y.obj.map (op i)) ≫
        Y.obj.map I.f.op

Tactic:
intro I

Goal state after:
case refine_2
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
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
W₁ : C
g₁ : G.obj W₁ ⟶ G.obj U
W₂ : C
i : W₂ ⟶ W₁
hi : (StructuredArrow.mk (op g₁)).hom ≫ G.op.map (op i) = (StructuredArrow.mk (op (G.map i ≫ g₁))).hom
I : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve (G.map i ≫ g₁), ⋯⟩
⊢ ⋯.amalgamate ⟨G.imageSieve (G.map i ≫ g₁), ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y W₂ U I.f (G.map i ≫ g₁) ⋯).op) ⋯ ≫
      Y.obj.map I.f.op =
    (⋯.amalgamate ⟨G.imageSieve g₁, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y W₁ U I.f g₁ ⋯).op) ⋯ ≫ Y.obj.map (op i)) ≫
      Y.obj.map I.f.op
Module: Mathlib.CategoryTheory.Sites.InducedTopology

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

Tactic:
by
  refine le_antisymm ?_ inducedTopology_le_restrictedTopology
  rw [le_inducedTopology_iff]
  infer_instance

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

Goal state before:
pp: case of
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S : Presieve X
hS : S ∈ (Precoverage.comap G K.toPrecoverage).coverings X
⊢ Sieve.functorPushforward G (Sieve.generate S) ∈ K (G.obj X)

Tactic:
| of X S hS =>

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

Goal state before:
pp: case pullback
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S : Sieve X
a✝ : (Precoverage.comap G K.toPrecoverage).Saturate X S
Y : C
f : Y ⟶ X
ih : Sieve.functorPushforward G S ∈ K (G.obj X)
Z : D
U : C
iUY : U ⟶ Y
iZU : Z ⟶ G.obj U
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map f = iUW ≫ G.map iWX
⊢ Sieve.pullback (iZU ≫ G.map iUY) (Sieve.functorPushforward G (Sieve.pullback f S)) ∈ K Z

Tactic:
rw [Sieve.pullback_comp]

Goal state after:
case pullback
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S : Sieve X
a✝ : (Precoverage.comap G K.toPrecoverage).Saturate X S
Y : C
f : Y ⟶ X
ih : Sieve.functorPushforward G S ∈ K (G.obj X)
Z : D
U : C
iUY : U ⟶ Y
iZU : Z ⟶ G.obj U
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map f = iUW ≫ G.map iWX
⊢ Sieve.pullback iZU (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback f S))) ∈ K Z
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: case pullback
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S : Sieve X
a✝ : (Precoverage.comap G K.toPrecoverage).Saturate X S
Y : C
f : Y ⟶ X
ih : Sieve.functorPushforward G S ∈ K (G.obj X)
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map f = iUW ≫ G.map iWX
Z : D
U₁ : C
iU₁U : U₁ ⟶ U
iZU₁ : Z ⟶ G.obj U₁
iU₁W : U₁ ⟶ W
e₂ : G.map iU₁W = G.map iU₁U ≫ iUW
⊢ Sieve.pullback (iZU₁ ≫ G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback f S))) ∈
    K Z

Tactic:
rw [Sieve.pullback_comp]

Goal state after:
case pullback
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S : Sieve X
a✝ : (Precoverage.comap G K.toPrecoverage).Saturate X S
Y : C
f : Y ⟶ X
ih : Sieve.functorPushforward G S ∈ K (G.obj X)
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map f = iUW ≫ G.map iWX
Z : D
U₁ : C
iU₁U : U₁ ⟶ U
iZU₁ : Z ⟶ G.obj U₁
iU₁W : U₁ ⟶ W
e₂ : G.map iU₁W = G.map iU₁U ≫ iUW
⊢ Sieve.pullback iZU₁
      (Sieve.pullback (G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback f S)))) ∈
    K Z
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: case transitive
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S R : Sieve X
a✝¹ : (Precoverage.comap G K.toPrecoverage).Saturate X S
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → (Precoverage.comap G K.toPrecoverage).Saturate Y (Sieve.pullback f R)
hS : Sieve.functorPushforward G S ∈ K (G.obj X)
H' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.functorPushforward G (Sieve.pullback f R) ∈ K (G.obj Y)
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg : S.arrows g
⊢ Sieve.pullback (i ≫ G.map g) (Sieve.functorPushforward G R) ∈ K Y

Tactic:
rw [Sieve.pullback_comp]

Goal state after:
case transitive
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S R : Sieve X
a✝¹ : (Precoverage.comap G K.toPrecoverage).Saturate X S
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → (Precoverage.comap G K.toPrecoverage).Saturate Y (Sieve.pullback f R)
hS : Sieve.functorPushforward G S ∈ K (G.obj X)
H' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.functorPushforward G (Sieve.pullback f R) ∈ K (G.obj Y)
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg : S.arrows g
⊢ Sieve.pullback i (Sieve.pullback (G.map g) (Sieve.functorPushforward G R)) ∈ K Y
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
X : C
i : I
f : X ⟶ Y i
h : (ConcreteCategory.hom (F.map (𝟙 X).op)) (⋯.amalgamate (x.familyOfElements X) ⋯) = x.familyOfElements X (𝟙 X) ⋯
⊢ s X = (ConcreteCategory.hom (F.map f.op)) (x i)

Tactic:
simp only [op_id, F.map_id, types_id_apply] at h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
X : C
i : I
f : X ⟶ Y i
h : ⋯.amalgamate (x.familyOfElements X) ⋯ = x.familyOfElements X (𝟙 X) ⋯
⊢ s X = (ConcreteCategory.hom (F.map f.op)) (x i)
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₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
⊢ (Iso.refl ((Over.map f).obj W').left).hom ≫ W.hom = ((Over.map f).obj W').hom

Tactic:
simpa [W'] using! (Over.w f₁).symm

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

Goal state before:
pp: case refine_1.transitive
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X Y✝ : C
R✝ : Sieve Y✝
Y : C
R S : Sieve Y
hR : K.toCoverage.Saturate Y R
H : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → K.toCoverage.Saturate Y_1 (Sieve.pullback f S)
s : Y ⟶ X
Z : Over X
ih :
  ∀ (s : Y ⟶ X),
    (Sieve.overEquiv { left := Y, right := Z.right, hom := s }).symm R ∈
      (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Y, right := Z.right, hom := s }
ih' :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f →
      ∀ (s : Y_1 ⟶ X),
        (Sieve.overEquiv { left := Y_1, right := Z.right, hom := s }).symm (Sieve.pullback f S) ∈
          (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Y_1, right := Z.right, hom := s }
g : Z ⟶ { left := Y, right := Z.right, hom := s }
hg : ((Sieve.overEquiv { left := Y, right := Z.right, hom := s }).symm R).arrows g
⊢ Sieve.pullback g ((Sieve.overEquiv { left := Y, right := Z.right, hom := s }).symm S) ∈
    (Precoverage.comap (Over.forget X) K).toGrothendieck Z

Tactic:
rw [← Sieve.overEquiv_symm_pullback]

Goal state after:
case refine_1.transitive
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X Y✝ : C
R✝ : Sieve Y✝
Y : C
R S : Sieve Y
hR : K.toCoverage.Saturate Y R
H : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → K.toCoverage.Saturate Y_1 (Sieve.pullback f S)
s : Y ⟶ X
Z : Over X
ih :
  ∀ (s : Y ⟶ X),
    (Sieve.overEquiv { left := Y, right := Z.right, hom := s }).symm R ∈
      (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Y, right := Z.right, hom := s }
ih' :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f →
      ∀ (s : Y_1 ⟶ X),
        (Sieve.overEquiv { left := Y_1, right := Z.right, hom := s }).symm (Sieve.pullback f S) ∈
          (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Y_1, right := Z.right, hom := s }
g : Z ⟶ { left := Y, right := Z.right, hom := s }
hg : ((Sieve.overEquiv { left := Y, right := Z.right, hom := s }).symm R).arrows g
⊢ (Sieve.overEquiv Z).symm (Sieve.pullback (Over.Hom.left g) S) ∈ (Precoverage.comap (Over.forget X) K).toGrothendieck Z
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: case refine_1
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
s₁ s₂ : ↑P.sections
h : F.sectionsPrecomp s₁ = F.sectionsPrecomp s₂
Y : D
X : CostructuredArrow F Y := Classical.arbitrary (CostructuredArrow F Y)
this : ↑(F.sectionsPrecomp s₁) X.left = ↑(F.sectionsPrecomp s₂) X.left
h₁ : (ConcreteCategory.hom (P.map X.hom)) (↑s₁ (F.obj X.left)) = ↑s₁ Y
h₂ : (ConcreteCategory.hom (P.map X.hom)) (↑s₂ (F.obj X.left)) = ↑s₂ Y
⊢ ↑s₁ Y = ↑s₂ Y

Tactic:
dsimp at this h₁ h₂

Goal state after:
case refine_1
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
s₁ s₂ : ↑P.sections
h : F.sectionsPrecomp s₁ = F.sectionsPrecomp s₂
Y : D
X : CostructuredArrow F Y := Classical.arbitrary (CostructuredArrow F Y)
this : ↑s₁ (F.obj X.left) = ↑s₂ (F.obj X.left)
h₁ : (ConcreteCategory.hom (P.map X.hom)) (↑s₁ (F.obj X.left)) = ↑s₁ Y
h₂ : (ConcreteCategory.hom (P.map X.hom)) (↑s₂ (F.obj X.left)) = ↑s₂ Y
⊢ ↑s₁ Y = ↑s₂ Y
Module: Mathlib.CategoryTheory.Sites.Spaces

Goal state before:
pp: T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
S : Sieve X
f : Y ⟶ X
hf : S ∈ {S | ∀ x ∈ X, ∃ U f, S.arrows f ∧ x ∈ U}
y : T
hy : y ∈ Y
U : Opens T
g : U ⟶ X
hg : S.arrows g
hU : y ∈ U
⊢ ∃ U f_1, (Sieve.pullback f S).arrows f_1 ∧ y ∈ U

Tactic:
refine ⟨U ⊓ Y, homOfLE inf_le_right, ?_, hU, hy⟩

Goal state after:
T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
S : Sieve X
f : Y ⟶ X
hf : S ∈ {S | ∀ x ∈ X, ∃ U f, S.arrows f ∧ x ∈ U}
y : T
hy : y ∈ Y
U : Opens T
g : U ⟶ X
hg : S.arrows g
hU : y ∈ U
⊢ (Sieve.pullback f S).arrows (homOfLE ⋯)