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

Goal state before:
pp: C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
hx : x.Compatible
Z : C
g : Z ⟶ Y
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows gg
⊢ (Sieve.pullback f S).arrows (gg ≫ g)

Tactic:
simpa using

Goal state after:
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
hx : x.Compatible
Z : C
g : Z ⟶ Y
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows gg
⊢ S.arrows (gg ≫ g ≫ f)
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case mp
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ K.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X : C
S : Presieve X
hS : S ∈ K.coverings X
⊢ IsSheafFor P S

Tactic:
simpa using

Goal state after:
case mp
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ K.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X : C
S : Presieve X
hS : S ∈ K.coverings X
⊢ IsSheafFor P S
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case trans
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
J : Precoverage C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.Small
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), Presieve.IsSheafFor P E.presieve₀
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
E : J.ZeroHypercover X := ⋯
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X),
    Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate E.restrictIndexOfSmall.presieve₀)).arrows

Tactic:
intro Y f

Goal state after:
case trans
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
J : Precoverage C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.Small
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), Presieve.IsSheafFor P E.presieve₀
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
E : J.ZeroHypercover X := { toPreZeroHypercover := E₀, mem₀ := hR }
Y : C
f : Y ⟶ X
⊢ Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate E.restrictIndexOfSmall.presieve₀)).arrows
Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve X
E : J.OneHypercover X
hE : H E
le : E.sieve₀ ≤ S
inst✝ : H.IsGenerating
F : Multifork (Cover.index ⟨S, ⋯⟩ P)
Y : C
f : Y ⟶ X
hf : (↑⟨S, ⋯⟩).arrows f
⊢ lift hP hE le F ≫ (Cover.multifork ⟨S, ⋯⟩ P).ι { Y := Y, f := f, hf := hf } = F.ι { Y := Y, f := f, hf := hf }

Tactic:
apply fac

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : J.IsGeneratedByOneHypercovers
P : Cᵒᵖ ⥤ A
⊢ IsSheaf J P ↔ ∀ ⦃X : C⦄ (E : J.OneHypercover X), Nonempty (IsLimit (E.multifork P))

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : J.IsGeneratedByOneHypercovers
P : Cᵒᵖ ⥤ A
⊢ IsSheaf J P ↔ ∀ ⦃X : C⦄ (E : J.OneHypercover X), 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 using

Goal state after:
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
          ((L.leftKanExtension F ⋙ G).descOfIsLeftKanExtension
            (whiskerRight (L.leftKanExtensionUnit F) G ≫ (L.associator (L.leftKanExtension F) G).hom)
            (L.leftKanExtension (F ⋙ G)) (L.leftKanExtensionUnit (F ⋙ G))) =
    L.leftKanExtensionUnit (F ⋙ G)
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
a : A
⊢ G.map ((L.leftKanExtensionUnit F).app a) ≫ (G.leftKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a) =
    (L.leftKanExtensionUnit (F ⋙ G)).app a

Tactic:
simpa using

Goal state after:
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
a : A
⊢ G.map ((L.leftKanExtensionUnit F).app a) ≫ (G.leftKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a) =
    (L.leftKanExtensionUnit (F ⋙ G)).app a
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
a : A
⊢ (L.leftKanExtensionUnit (F ⋙ G)).app a ≫ (G.leftKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a) =
    G.map ((L.leftKanExtensionUnit F).app a)

Tactic:
simpa using

Goal state after:
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
a : A
⊢ (L.leftKanExtensionUnit (F ⋙ G)).app a ≫ (G.leftKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a) =
    G.map ((L.leftKanExtensionUnit F).app a)
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.PreservesPointwiseLeftKanExtension F L
inst✝ : L.HasPointwiseLeftKanExtension F
⊢ whiskerRight (L.pointwiseLeftKanExtensionUnit F) G ≫
      (L.associator (L.pointwiseLeftKanExtension F) G).hom ≫
        L.whiskerLeft (G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).hom =
    L.pointwiseLeftKanExtensionUnit (F ⋙ G)

Tactic:
simpa using

Goal state after:
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.PreservesPointwiseLeftKanExtension F L
inst✝ : L.HasPointwiseLeftKanExtension F
⊢ whiskerRight (L.pointwiseLeftKanExtensionUnit F) G ≫
      (L.associator (L.pointwiseLeftKanExtension F) G).hom ≫
        L.whiskerLeft
          ((L.pointwiseLeftKanExtension F ⋙ G).descOfIsLeftKanExtension
            (whiskerRight (L.pointwiseLeftKanExtensionUnit F) G ≫ (L.associator (L.pointwiseLeftKanExtension F) G).hom)
            (L.pointwiseLeftKanExtension (F ⋙ G)) (L.pointwiseLeftKanExtensionUnit (F ⋙ G))) =
    L.pointwiseLeftKanExtensionUnit (F ⋙ G)
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.PreservesPointwiseLeftKanExtension F L
inst✝ : L.HasPointwiseLeftKanExtension F
a : A
⊢ G.map ((L.pointwiseLeftKanExtensionUnit F).app a) ≫
      (G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a) =
    (L.pointwiseLeftKanExtensionUnit (F ⋙ G)).app a

Tactic:
simpa using

Goal state after:
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.PreservesPointwiseLeftKanExtension F L
inst✝ : L.HasPointwiseLeftKanExtension F
a : A
⊢ G.map (Limits.colimit.ι (CostructuredArrow.proj L (L.obj a) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj a)))) ≫
      (G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a) =
    Limits.colimit.ι (CostructuredArrow.proj L (L.obj a) ⋙ F ⋙ G) (CostructuredArrow.mk (𝟙 (L.obj a)))
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.PreservesPointwiseLeftKanExtension F L
inst✝ : L.HasPointwiseLeftKanExtension F
a : A
⊢ (L.pointwiseLeftKanExtensionUnit (F ⋙ G)).app a ≫
      (G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a) =
    G.map ((L.pointwiseLeftKanExtensionUnit F).app a)

Tactic:
simpa using

Goal state after:
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.PreservesPointwiseLeftKanExtension F L
inst✝ : L.HasPointwiseLeftKanExtension F
a : A
⊢ Limits.colimit.ι (CostructuredArrow.proj L (L.obj a) ⋙ F ⋙ G) (CostructuredArrow.mk (𝟙 (L.obj a))) ≫
      (G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a) =
    G.map (Limits.colimit.ι (CostructuredArrow.proj L (L.obj a) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj a))))
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.PreservesRightKanExtension F L
inst✝ : L.HasRightKanExtension F
a : A
⊢ (G.rightKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a) ≫ G.map ((L.rightKanExtensionCounit F).app a) =
    (L.rightKanExtensionCounit (F ⋙ G)).app a

Tactic:
simpa using

Goal state after:
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.PreservesRightKanExtension F L
inst✝ : L.HasRightKanExtension F
a : A
⊢ (G.rightKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a) ≫ G.map ((L.rightKanExtensionCounit F).app a) =
    (L.rightKanExtensionCounit (F ⋙ G)).app a
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.PreservesPointwiseRightKanExtension F L
inst✝ : L.HasPointwiseRightKanExtension F
a : A
⊢ (G.pointwiseRightKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a) ≫
      (L.pointwiseRightKanExtensionCounit (F ⋙ G)).app a =
    G.map ((L.pointwiseRightKanExtensionCounit F).app a)

Tactic:
simpa using

Goal state after:
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.PreservesPointwiseRightKanExtension F L
inst✝ : L.HasPointwiseRightKanExtension F
a : A
⊢ (G.pointwiseRightKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a) ≫
      Limits.limit.π (StructuredArrow.proj (L.obj a) L ⋙ F ⋙ G) (StructuredArrow.mk (𝟙 (L.obj a))) =
    G.map (Limits.limit.π (StructuredArrow.proj (L.obj a) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj a))))
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.PreservesPointwiseRightKanExtension F L
inst✝ : L.HasPointwiseRightKanExtension F
a : A
⊢ (G.pointwiseRightKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a) ≫
      G.map ((L.pointwiseRightKanExtensionCounit F).app a) =
    (L.pointwiseRightKanExtensionCounit (F ⋙ G)).app a

Tactic:
simpa using

Goal state after:
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.PreservesPointwiseRightKanExtension F L
inst✝ : L.HasPointwiseRightKanExtension F
a : A
⊢ (G.pointwiseRightKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a) ≫
      G.map (Limits.limit.π (StructuredArrow.proj (L.obj a) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj a)))) =
    Limits.limit.π (StructuredArrow.proj (L.obj a) L ⋙ F ⋙ G) (StructuredArrow.mk (𝟙 (L.obj a)))
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case refine_1.pullback
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.HasIsos
X✝ : C
S✝ : Sieve X✝
X : C
S : Sieve X
hS : J.Saturate X S
Y : C
f : Y ⟶ X
h : ∃ R ∈ J.coverings X, R ≤ S.arrows
⊢ ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f S).arrows

Tactic:
| pullback X S hS Y f h =>

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

Goal state before:
pp: C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
h : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
S : C
R : Presieve S
hR : R ∈ J.coverings S
⊢ IsSheafFor P R

Tactic:
simpa using

Goal state after:
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
h : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
S : C
R : Presieve S
hR : R ∈ J.coverings S
⊢ IsSheafFor P (Sieve.generate (Sieve.generate R).arrows).arrows
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_3
inst✝ : Category.{u_2, u_3} C
F : Cᵒᵖ ⥤ Type u_1
S X Y : C
f : X ⟶ S
g : Y ⟶ S
e : X ≅ Y
he : e.hom ≫ g = f
⊢ IsSheafFor F (singleton f) ↔ IsSheafFor F (singleton g)

Tactic:
by
  subst he
  rw [← Presieve.ofArrows_pUnit.{0}, ← Presieve.ofArrows_pUnit,
    Presieve.isSheafFor_ofArrows_comp_iff]

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

Goal state before:
pp: C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : GrothendieckTopology C
S : C
R : Sieve S
⊢ R.arrows ∈ J.toPrecoverage.coverings S ↔ R ∈ J S

Tactic:
by
  rw [mem_toPrecoverage_iff, Sieve.generate_sieve]

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

Goal state before:
pp: C : Type u_3
inst✝¹ : Category.{u_2, u_3} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
J : GrothendieckTopology C
ι : Type (max u_3 u_2)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.toPrecoverage.coverings S
σ : ι → Type (max u_3 u_2)
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.toPrecoverage.coverings (X i)
⊢ (Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst) ∈ J.toPrecoverage.coverings S

Tactic:
rw [mem_toPrecoverage_iff, ← Presieve.bindOfArrows_ofArrows]
    exact J.bindOfArrows hf hg

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : Sheaf K (Type w)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
h : x.Compatible
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
X₁ : C
f₁ : X₁ ⟶ Z
h₁ : Z₁ ⟶ G.obj X₁
hf₁ : T f₁
H₁ : Presieve.functorPushforward G T (h₁ ≫ G.map f₁)
X₂ : C
f₂ : X₂ ⟶ Z
h₂ : Z₂ ⟶ G.obj X₂
hf₂ : T f₂
H₂ : Presieve.functorPushforward G T (h₂ ≫ G.map f₂)
eq : g₁ ≫ h₁ ≫ G.map f₁ = g₂ ≫ h₂ ≫ G.map f₂
this :
  (ConcreteCategory.hom (ℱ.obj.map (g₁ ≫ h₁).op)) (x f₁ hf₁) =
    (ConcreteCategory.hom (ℱ.obj.map (g₂ ≫ h₂).op)) (x f₂ hf₂)
⊢ (ConcreteCategory.hom (ℱ.obj.map g₁.op))
      (FunctorPushforwardStructure.casesOn { preobj := X₁, premap := f₁, lift := h₁, cover := hf₁, fac := ⋯ }
        fun Z_1 g h h₁_1 fac ↦ (ConcreteCategory.hom (ℱ.obj.map h.op)) (x g h₁_1)) =
    (ConcreteCategory.hom (ℱ.obj.map g₂.op))
      (FunctorPushforwardStructure.casesOn { preobj := X₂, premap := f₂, lift := h₂, cover := hf₂, fac := ⋯ }
        fun Z_1 g h h₁ fac ↦ (ConcreteCategory.hom (ℱ.obj.map h.op)) (x g h₁))

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : Sheaf K (Type w)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
h : x.Compatible
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
X₁ : C
f₁ : X₁ ⟶ Z
h₁ : Z₁ ⟶ G.obj X₁
hf₁ : T f₁
H₁ : Presieve.functorPushforward G T (h₁ ≫ G.map f₁)
X₂ : C
f₂ : X₂ ⟶ Z
h₂ : Z₂ ⟶ G.obj X₂
hf₂ : T f₂
H₂ : Presieve.functorPushforward G T (h₂ ≫ G.map f₂)
eq : g₁ ≫ h₁ ≫ G.map f₁ = g₂ ≫ h₂ ≫ G.map f₂
this :
  (ConcreteCategory.hom (ℱ.obj.map (g₁ ≫ h₁).op)) (x f₁ hf₁) =
    (ConcreteCategory.hom (ℱ.obj.map (g₂ ≫ h₂).op)) (x f₂ hf₂)
⊢ (ConcreteCategory.hom (ℱ.obj.map g₁.op)) ((ConcreteCategory.hom (ℱ.obj.map h₁.op)) (x f₁ hf₁)) =
    (ConcreteCategory.hom (ℱ.obj.map g₂.op)) ((ConcreteCategory.hom (ℱ.obj.map h₂.op)) (x f₂ hf₂))
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
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
X₁ : C
f₁ : X₁ ⟶ Z
h₁ : Z₁ ⟶ G.obj X₁
hf₁ : T f₁
H₁ : Presieve.functorPushforward G T (h₁ ≫ G.map f₁)
X₂ : C
f₂ : X₂ ⟶ Z
h₂ : Z₂ ⟶ G.obj X₂
hf₂ : T f₂
H₂ : Presieve.functorPushforward G T (h₂ ≫ G.map f₂)
eq : g₁ ≫ h₁ ≫ G.map f₁ = g₂ ≫ h₂ ≫ G.map f₂
⊢ (g₁ ≫ h₁) ≫ G.map f₁ = (g₂ ≫ h₂) ≫ G.map f₂

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : Sheaf K (Type w)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
h : x.Compatible
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
X₁ : C
f₁ : X₁ ⟶ Z
h₁ : Z₁ ⟶ G.obj X₁
hf₁ : T f₁
H₁ : Presieve.functorPushforward G T (h₁ ≫ G.map f₁)
X₂ : C
f₂ : X₂ ⟶ Z
h₂ : Z₂ ⟶ G.obj X₂
hf₂ : T f₂
H₂ : Presieve.functorPushforward G T (h₂ ≫ G.map f₂)
eq : g₁ ≫ h₁ ≫ G.map f₁ = g₂ ≫ h₂ ≫ G.map f₂
⊢ g₁ ≫ h₁ ≫ G.map f₁ = g₂ ≫ h₂ ≫ G.map f₂
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
Y : C
f : Y ⟶ Z
hf : T f
X : C
g : X ⟶ Z
f' : G.obj Y ⟶ G.obj X
hg : T g
eq : G.map f = f' ≫ G.map g
⊢ (FunctorPushforwardStructure.casesOn { preobj := X, premap := g, lift := f', cover := hg, fac := eq }
      fun Z_1 g h h₁ fac ↦ (ConcreteCategory.hom (ℱ.obj.map h.op)) (x g h₁)) =
    x f hf

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : Sheaf K (Type w)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
h : x.Compatible
Y : C
f : Y ⟶ Z
hf : T f
X : C
g : X ⟶ Z
f' : G.obj Y ⟶ G.obj X
hg : T g
eq : G.map f = f' ≫ G.map g
⊢ (ConcreteCategory.hom (ℱ.obj.map f'.op)) (x g hg) = x f hf
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
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
F : C ⥤ D
G : D ⥤ E
h : CoverPreserving J L (F ⋙ G)
inst✝² : G.IsCocontinuous K L
inst✝¹ : G.Full
inst✝ : G.Faithful
U : C
S : Sieve U
hS : S ∈ J U
⊢ Sieve.functorPullback G (Sieve.functorPushforward (F ⋙ G) S) ≤ Sieve.functorPushforward F S

Tactic:
Sieve.functorPushforward_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
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
F : C ⥤ D
G : D ⥤ E
h : CoverPreserving J L (F ⋙ G)
inst✝² : G.IsCocontinuous K L
inst✝¹ : G.Full
inst✝ : G.Faithful
U : C
S : Sieve U
hS : S ∈ J U
⊢ Sieve.functorPullback G (Sieve.functorPushforward G (Sieve.functorPushforward F S)) ≤ Sieve.functorPushforward F S