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
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → Presieve.FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg ↦ x (gg ≫ g) ⋯
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), (y g).IsAmalgamation (z hg)
q : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg ↦ z hg
⊢ q.Compatible

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
⊢ L.pointwiseLeftKanExtensionUnit (F ⋙ G) ≫ L.whiskerLeft (G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).inv =
    whiskerRight (L.pointwiseLeftKanExtensionUnit F) G ≫ (L.associator (L.pointwiseLeftKanExtension F) G).hom

Tactic:
by

Goal state after:
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:
by

Goal state after:
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.PreservesLeftKanExtensions L
inst✝¹ : ∀ (F : A ⥤ B), L.HasLeftKanExtension F
inst✝ : ∀ (F : A ⥤ D), L.HasLeftKanExtension F
F F' : A ⥤ B
η : F ⟶ F'
⊢ (L.lan ⋙ (whiskeringRight C B D).obj G).map η ≫ (G.leftKanExtensionCompIsoOfPreserves F' L).hom =
    (G.leftKanExtensionCompIsoOfPreserves F L).hom ≫ ((whiskeringRight A B D).obj G ⋙ L.lan).map η

Tactic:
by

Goal state after:
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
F' : C ⥤ B
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
h✝ : (F' ⋙ G).IsRightKanExtension ((L.associator F' G).inv ≫ whiskerRight α G)
F'' : C ⥤ B
α' : L ⋙ F'' ⟶ F
h : F''.IsRightKanExtension α'
⊢ L.whiskerLeft (isoWhiskerRight (F'.rightKanExtensionUnique α F'' α') G).hom ≫
      (L.associator F'' G).inv ≫ whiskerRight α' G =
    (L.associator F' G).inv ≫ whiskerRight α G

Tactic:
by

Goal state after:
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✝¹ : L.HasRightKanExtension F
inst✝ : G.PreservesRightKanExtension F L
⊢ (L.rightKanExtension F).IsRightKanExtension (L.rightKanExtensionCounit F)

Tactic:
by

Goal state after:
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
⊢ L.whiskerLeft (G.rightKanExtensionCompIsoOfPreserves F L).hom ≫ L.rightKanExtensionCounit (F ⋙ G) =
    (L.associator (L.rightKanExtension F) G).inv ≫ whiskerRight (L.rightKanExtensionCounit F) G

Tactic:
by

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

Tactic:
by

Goal state after:
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
⊢ L.whiskerLeft (G.rightKanExtensionCompIsoOfPreserves F L).inv ≫
      (L.associator (L.rightKanExtension F) G).inv ≫ whiskerRight (L.rightKanExtensionCounit F) G =
    L.rightKanExtensionCounit (F ⋙ G)

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
⊢ L.whiskerLeft (G.pointwiseRightKanExtensionCompIsoOfPreserves F L).hom ≫ L.pointwiseRightKanExtensionCounit (F ⋙ G) =
    (L.associator (L.pointwiseRightKanExtension F) G).inv ≫ whiskerRight (L.pointwiseRightKanExtensionCounit F) G

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
⊢ L.whiskerLeft (G.pointwiseRightKanExtensionCompIsoOfPreserves F L).inv ≫
      (L.associator (L.pointwiseRightKanExtension F) G).inv ≫ whiskerRight (L.pointwiseRightKanExtensionCounit F) G =
    L.pointwiseRightKanExtensionCounit (F ⋙ G)

Tactic:
by

Goal state after:
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:
by

Goal state after:
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.PreservesRightKanExtensions L
inst✝¹ : ∀ (F : A ⥤ B), L.HasRightKanExtension F
inst✝ : ∀ (F : A ⥤ D), L.HasRightKanExtension F
F F' : A ⥤ B
η : F ⟶ F'
⊢ (L.ran ⋙ (whiskeringRight C B D).obj G).map η ≫ (G.rightKanExtensionCompIsoOfPreserves F' L).hom =
    (G.rightKanExtensionCompIsoOfPreserves F L).hom ≫ ((whiskeringRight A B D).obj G ⋙ L.ran).map η

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E✝ : Type u₃
inst✝ : Category.{v₃, u₃} E✝
X : C
E : PreOneHypercover X
F : C ⥤ D
x✝¹ x✝ : (PreZeroHypercover.map F E.toPreZeroHypercover).I₀
j : E.I₁ x✝¹ x✝
⊢ F.map (E.p₁ j) ≫ (PreZeroHypercover.map F E.toPreZeroHypercover).f x✝¹ =
    F.map (E.p₂ j) ≫ (PreZeroHypercover.map F E.toPreZeroHypercover).f x✝

Tactic:
by

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
⊢ Presieve.IsSheaf J.toGrothendieck P ↔
    ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
⊢ (E.map F).sieve₀ = Sieve.functorPushforward F E.sieve₀

Tactic:
by

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

Goal state before:
pp: 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
⊢ Presieve.singleton (𝟙 X) ≤ ⊤.arrows

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E✝ : Type u₃
inst✝¹ : Category.{v₃, u₃} E✝
X : C
E : PreOneHypercover X
F : C ⥤ D
A : Type u
inst✝ : Category.{t, u} A
P : Dᵒᵖ ⥤ A
⊢ IsLimit ((E.map F).multifork P) ≃ IsLimit (E.multifork (F.op ⋙ P))

Tactic:
by

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

Goal state before:
pp: 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₂
Y : C
f : Y ⟶ W
k : E.I₁ i₁ i₂
u : Y ⟶ E.Y k
hf₁ : f ≫ p₁ = u ≫ E.p₁ k
hf₂ : f ≫ p₂ = u ≫ E.p₂ k
⊢ F.map f ≫ F.map p₁ = F.map u ≫ (E.map F).p₁ k

Tactic:
by

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

Goal state before:
pp: 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₂
Y : C
f : Y ⟶ W
k : E.I₁ i₁ i₂
u : Y ⟶ E.Y k
hf₁ : f ≫ p₁ = u ≫ E.p₁ k
hf₂ : f ≫ p₂ = u ≫ E.p₂ k
⊢ F.map f ≫ F.map p₂ = F.map u ≫ (E.map F).p₂ k

Tactic:
by

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

Goal state before:
pp: 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₂
⊢ Sieve.functorPushforward F (E.sieve₁ p₁ p₂) ≤ (E.map F).sieve₁ (F.map p₁) (F.map p₂)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
i₁ i₂ : E.I₀
inst✝¹ : HasPullback (E.f i₁) (E.f i₂)
inst✝ : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
⊢ F.map (pullback.fst (E.f i₁) (E.f i₂)) ≫ (E.map F).f i₁ = F.map (pullback.snd (E.f i₁) (E.f i₂)) ≫ (E.map F).f i₂

Tactic:
by

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

Goal state before:
pp: 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 T : Sieve X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
i : E.I₀
⊢ ∃ F, F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
i₁ i₂ : E.I₀
inst✝¹ : HasPullback (E.f i₁) (E.f i₂)
inst✝ : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
⊢ Sieve.functorPushforward F (E.sieve₁' i₁ i₂) =
    (E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂)))

Tactic:
by

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

Goal state before:
pp: 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
⊢ l ≫ pullback.fst (E.f i₁) (E.f i₂) = p₁

Tactic:
by

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

Goal state before:
pp: 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₁
⊢ l ≫ pullback.snd (E.f i₁) (E.f i₂) = p₂

Tactic:
by

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

Goal state before:
pp: 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
⊢ S ∈ J.toGrothendieck X ↔ ∃ R ∈ J.coverings X, R ≤ S.arrows

Tactic:
by

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

Goal state before:
pp: C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.HasIsos
⊢ (toPretopology C J).toGrothendieck = J.toGrothendieck

Tactic:
by

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 : IsSheaf J.toGrothendieck P
S : C
R : Presieve S
hR : R ∈ J.coverings S
⊢ IsSheafFor P R

Tactic:
by

Goal state after:
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 : C
𝒰 𝒱 : PreZeroHypercover S
e : 𝒰 ≅ 𝒱
⊢ Presieve.IsSheafFor F 𝒰.presieve₀ ↔ Presieve.IsSheafFor F 𝒱.presieve₀

Tactic:
by

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

Goal state before:
pp: C : Type u_4
inst✝ : Category.{u_3, u_4} C
F : Cᵒᵖ ⥤ Type u_1
X : C
ι : Type u_2
Y Z : ι → C
g : (i : ι) → Z i ⟶ X
e : (i : ι) → Y i ≅ Z i
⊢ IsSheafFor F (ofArrows Y fun i ↦ (e i).hom ≫ g i) ↔ IsSheafFor F (ofArrows Z g)

Tactic:
by

Goal state after:
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

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

Goal state before:
pp: 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
⊢ Sieve.functorPushforward F (E.sieve₁ p₁ p₂) = (E.map F).sieve₁ (F.map p₁) (F.map p₂)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op
inst✝ : F.IsContinuous J K
G G' : Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
f : G ⟶ G'
hf : J.W f
⊢ K.W (H.map f)

Tactic:
by

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

Goal state before:
pp: C : Type u_4
inst✝³ : Category.{u_3, u_4} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
P : Dᵒᵖ ⥤ Type u_2
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst✝¹ : (ofArrows Y f).HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks (ofArrows Y f)
this✝¹ : (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)).HasPairwisePullbacks
x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))
i j : ι
this✝ : PreservesLimit (cospan (f i) (f j)) F
this : HasPullback (F.map (f i)) (F.map (f j))
⊢ Function.Bijective ⇑(ConcreteCategory.hom (P.map (pullbackComparison F (f i) (f j)).op))

Tactic:
by

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

Goal state before:
pp: C : Type u_4
inst✝³ : Category.{u_3, u_4} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
P : Dᵒᵖ ⥤ Type u_2
X : C
R : Presieve X
inst✝¹ : R.HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks R
⊢ IsSheafFor (F.op ⋙ P) R ↔ IsSheafFor P (map F R)

Tactic:
by

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

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
S✝ T✝ : C
f : S✝ ⟶ T✝
hf : IsIso f
⊢ Presieve.singleton f ∈ J.toPrecoverage.coverings T✝

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
inst✝ : F.IsContinuous J K
G : Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)
hG : Presieve.IsSheaf K G
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂) := F.op.lan
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op := F.op.lanAdjunction (Type (max u₁ v₁ u₂ v₂))
H' : (Cᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂) := F.op.lan
adj' : H' ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max w u₁ v₁ u₂ v₂))).obj F.op :=
  F.op.lanAdjunction (Type (max w u₁ v₁ u₂ v₂))
X : C
S : Sieve X
hS : S ∈ J X
hWS : J.W (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S).ι
this : K.W (H.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S).ι)
e : H ⋙
    (whiskeringRight Dᵒᵖ (Type (max u₁ v₁ u₂ v₂)) (Type (max (max (max (max u₁ u₂) v₁) v₂) w))).obj
      uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂} ≅
  (whiskeringRight Cᵒᵖ (Type (max u₁ v₁ u₂ v₂)) (Type (max (max (max (max u₁ u₂) v₁) v₂) w))).obj
      uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂} ⋙
    H' :=
  uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂}.lanCompIsoOfPreserves F.op
⊢ (H'.mapIso S.shrinkFunctorUliftFunctorIso.symm ≪≫
          (e.app (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S).toFunctor).symm).hom ≫
      whiskerRight (H.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S).ι)
        uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂} =
    H'.map (Sieve.shrinkFunctor.{max w u₁ v₁ u₂ v₂, v₁, u₁} S).ι ≫
      (H'.mapIso (shrinkYonedaUliftFunctorIso.app X).symm ≪≫
          (e.app (shrinkYoneda.{max u₁ v₁ u₂ v₂, v₁, u₁}.obj X)).symm).hom

Tactic:
by

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:
by

Goal state after: