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
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
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ Presieve.ofArrows P p₁ ∈ J.toPrecoverage.coverings Y

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
⊢ Presieve.IsSheaf J (F.op ⋙ 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
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : F.IsContinuous J K
G : Sheaf K (Type t)
⊢ Presieve.IsSheaf J (F.op ⋙ G.obj)

Tactic:
by

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

Goal state before:
pp: C : Type u_2
inst✝ : Category.{u_3, u_2} C
K : Precoverage C
J : GrothendieckTopology C
⊢ K.toGrothendieck ≤ J ↔ K ≤ J.toPrecoverage

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
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : F.IsContinuous J K
G : Dᵒᵖ ⥤ Type u_1
h : Presieve.IsSheaf K G
⊢ Presieve.IsSheaf J (F.op ⋙ G)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
U✝ : C
S✝ : Sieve U✝
hS : S✝ ∈ J U✝
⊢ Sieve.functorPushforward (𝟭 C) S✝ ∈ J ((𝟭 C).obj U✝)

Tactic:
by

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
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
F : C ⥤ D
hF : CoverPreserving J K F
G : D ⥤ A
hG : CoverPreserving K L G
U✝ : C
S✝ : Sieve U✝
hS : S✝ ∈ J U✝
⊢ Sieve.functorPushforward (F ⋙ G) S✝ ∈ L ((F ⋙ G).obj U✝)

Tactic:
by

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:
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
A : Type u
inst✝¹ : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
H : (Cᵒᵖ ⥤ A) ⥤ Dᵒᵖ ⥤ A
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj F.op
inst✝ : F.IsContinuous J K
G G' : Cᵒᵖ ⥤ A
f : G ⟶ G'
hf : J.W f
⊢ K.W (H.map f)

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
F₁ : C ⥤ D
F₂ : D ⥤ E
F₁₂ : C ⥤ E
e : F₁ ⋙ F₂ ≅ F₁₂
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
inst✝¹ : F₁.IsContinuous J K
inst✝ : F₂.IsContinuous K L
⊢ F₁₂.IsContinuous J L

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
F F' : C ⥤ D
τ : F ⟶ F'
e : F ≅ F'
G : D ⥤ E
F'' : C ⥤ C
eF'' : F'' ≅ 𝟭 C
FG : C ⥤ E
eFG : F ⋙ G ≅ FG
A : Type u
inst✝¹ : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
inst✝ : F.IsContinuous J K
⊢ (F ⋙ 𝟭 D).IsContinuous J 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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F F' : C ⥤ D
τ : F ⟶ F'
e : F ≅ F'
G : D ⥤ E
F'' : C ⥤ C
eF'' : F'' ≅ 𝟭 C
FG : C ⥤ E
eFG : F ⋙ G ≅ FG
A : Type u
inst✝¹ : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
inst✝ : F.IsContinuous J K
⊢ (𝟭 C ⋙ F).IsContinuous J K

Tactic:
by

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
⊢ (FamilyOfElements.functorPushforward G x).Compatible

Tactic:
by

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
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
⊢ f' ≫ G.map g = 𝟙 (G.obj Y) ≫ G.map f

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
F : C ⥤ D
J : Precoverage C
K : Precoverage D
inst✝⁴ : J.IsStableUnderBaseChange
inst✝³ : J.HasPullbacks
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.HasPullbacks
inst✝ : J.PullbacksPreservedBy F
h : J ≤ Precoverage.comap F K
x✝ : Sheaf K.toGrothendieck (Type (max u₁ v₁ u₂ v₂))
G : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
H : Presheaf.IsSheaf K.toGrothendieck G
⊢ Presieve.IsSheaf J.toGrothendieck (F.op ⋙ { obj := G, property := H }.obj)

Tactic:
by

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
Y : C
f : Y ⟶ Z
hf : T f
⊢ FamilyOfElements.functorPushforward G x (G.map f) ⋯ = x f hf

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
F : C ⥤ D
A : Type u
inst✝² : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : F.PreservesOneHypercovers J K
inst✝ : J.IsGeneratedByOneHypercovers
P : Dᵒᵖ ⥤ A
hP : Presheaf.IsSheaf K P
⊢ Presheaf.IsSheaf J (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
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : F.PreservesOneHypercovers J K
inst✝ : J.IsGeneratedByOneHypercovers
⊢ ∀ (G : Sheaf K (Type (max u₁ v₁ u₂ v₂))), Presieve.IsSheaf J (F.op ⋙ G.obj)

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
F F' : C ⥤ D
τ : F ⟶ F'
e : F ≅ F'
G : D ⥤ E
F'' : C ⥤ C
eF'' : F'' ≅ 𝟭 C
FG : C ⥤ E
eFG : F ⋙ G ≅ FG
A : Type u
inst✝² : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
inst✝¹ : F.IsContinuous J K
inst✝ : F'.IsContinuous J K
⊢ sheafPushforwardContinuousNatTrans e.inv A J K ≫ sheafPushforwardContinuousNatTrans e.hom A J K =
    𝟙 (F.sheafPushforwardContinuous A J 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
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
F F' : C ⥤ D
τ : F ⟶ F'
e : F ≅ F'
G : D ⥤ E
F'' : C ⥤ C
eF'' : F'' ≅ 𝟭 C
FG : C ⥤ E
eFG : F ⋙ G ≅ FG
A : Type u
inst✝² : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
inst✝¹ : F.IsContinuous J K
inst✝ : F'.IsContinuous J K
⊢ sheafPushforwardContinuousNatTrans e.hom A J K ≫ sheafPushforwardContinuousNatTrans e.inv A J K =
    𝟙 (F'.sheafPushforwardContinuous A J 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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : F.IsContinuous J K
inst✝ : G.IsContinuous K J
P : Sheaf K E
⊢ (F.sheafPushforwardContinuous E J K).map
        ({ app := fun P ↦ { hom := (Adjunction.whiskerLeft E adj.op).unit.app P.obj }, naturality := ⋯ }.app P) ≫
      { app := fun P ↦ { hom := (Adjunction.whiskerLeft E adj.op).counit.app P.obj }, naturality := ⋯ }.app
        ((F.sheafPushforwardContinuous E J K).obj P) =
    𝟙 ((F.sheafPushforwardContinuous E J K).obj 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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : F.IsContinuous J K
inst✝ : G.IsContinuous K J
P : Sheaf J E
⊢ { app := fun P ↦ { hom := (Adjunction.whiskerLeft E adj.op).unit.app P.obj }, naturality := ⋯ }.app
        ((G.sheafPushforwardContinuous E K J).obj P) ≫
      (G.sheafPushforwardContinuous E K J).map
        ({ app := fun P ↦ { hom := (Adjunction.whiskerLeft E adj.op).counit.app P.obj }, naturality := ⋯ }.app P) =
    𝟙 ((G.sheafPushforwardContinuous E K J).obj P)

Tactic:
by

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
E : Type u_3
inst✝ : Category.{v_3, u_3} E
G : C ⥤ D
G' : D ⥤ E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
U✝ : C
S✝ : Sieve ((𝟭 C).obj U✝)
h : S✝ ∈ J ((𝟭 C).obj U✝)
⊢ Sieve.functorPullback (𝟭 C) S✝ ∈ J U✝

Tactic:
by

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 G : C ⥤ D
e : F ≅ G
inst✝ : F.IsCocontinuous J K
U : C
S : Sieve (G.obj U)
hS : S ∈ K (G.obj U)
⊢ Sieve.functorPullback G S ∈ J U

Tactic:
by

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
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.functorPushforward F S ∈ K (F.obj U)

Tactic:
by

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
h : F.IsCocontinuous J K
U : D
S : Sieve U
hS : S ∈ K U
X : C
f : X ⟶ G.obj U
hf : (Sieve.functorPullback F (Sieve.pullback (adj.counit.app U) S)).arrows f
⊢ f = adj.unit.app X ≫ G.map (F.map f ≫ adj.counit.app U)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Z Z' : C
g : Z ⟶ W
j : E.I₁ i₁ i₂
h : Z ⟶ E.Y j
fac₁ : g ≫ p₁ = h ≫ E.p₁ j
fac₂ : g ≫ p₂ = h ≫ E.p₂ j
φ : Z' ⟶ Z
⊢ (φ ≫ g) ≫ p₁ = (φ ≫ h) ≫ E.p₁ j

Tactic:
by

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
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
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₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cone.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
⊢ G.obj ((c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).obj left).right = G.obj Y₁

Tactic:
by

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
h : CoverPreserving K J G
U : C
S : Sieve (F.obj U)
hS : S ∈ K (F.obj U)
X : C
f : X ⟶ U
Y : D
g : Y ⟶ F.obj U
u : X ⟶ G.obj Y
hg : S.arrows g
heq : f ≫ adj.unit.app U = u ≫ G.map g
this : F.map f = (adj.homEquiv X Y).symm u ≫ g
⊢ (Sieve.functorPullback F S).arrows f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Z Z' : C
g : Z ⟶ W
j : E.I₁ i₁ i₂
h : Z ⟶ E.Y j
fac₁ : g ≫ p₁ = h ≫ E.p₁ j
fac₂ : g ≫ p₂ = h ≫ E.p₂ j
φ : Z' ⟶ Z
⊢ (φ ≫ g) ≫ p₂ = (φ ≫ h) ≫ E.p₂ j

Tactic:
by

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
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
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₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cone.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
⊢ f₁ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app left))) ≫ eqToHom ⋯

Tactic:
by

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
⊢ F.IsCocontinuous J K ↔ CoverPreserving K J G

Tactic:
by

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

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
⊢ ∀ {Y Z : C} {f : Y ⟶ W},
    (∃ j h, f ≫ p₁ = h ≫ E.p₁ j ∧ f ≫ p₂ = h ≫ E.p₂ j) →
      ∀ (g : Z ⟶ Y), ∃ j h, (g ≫ f) ≫ p₁ = h ≫ E.p₁ j ∧ (g ≫ f) ≫ p₂ = h ≫ E.p₂ j

Tactic:
by

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
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
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₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cone.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ : f₁ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app left))) ≫ eqToHom ⋯
⊢ G.obj ((c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).obj right).right = G.obj Y₂

Tactic:
by

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
G : C ⥤ D
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
Y : C
f : G.obj Y ⟶ X
Y₁ : C
p₁ : Y₁ ⟶ Y
hp₁ : (↑⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).arrows p₁
Y₂ : C
p₂ : Y₂ ⟶ Y
hp₂ : (↑⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).arrows p₂
W : C
g₁ : W ⟶ Y₁
g₂ : W ⟶ Y₂
w : g₁ ≫ p₁ = g₂ ≫ p₂
⊢ G.map g₁ ≫ { Y := G.obj Y₁, f := G.map p₁ ≫ f, hf := hp₁ }.f =
    G.map g₂ ≫ { Y := G.obj Y₂, f := G.map p₂ ≫ f, hf := hp₂ }.f

Tactic:
by

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
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
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₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cone.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ : f₁ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app left))) ≫ eqToHom ⋯
⊢ f₂ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app right))) ≫ eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
G : C ⥤ D
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
Y : C
f : G.obj Y ⟶ X
⊢ ∀ (b : (GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).R),
    (s.ι
            {
              Y :=
                G.obj ((GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).fst b).Y,
              f :=
                G.map ((GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).fst b).f ≫
                  f,
              hf := ⋯ } ≫
          α.app (op ((GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).fst b).Y)) ≫
        (GrothendieckTopology.Cover.index ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩ F).fst b =
      (s.ι
            {
              Y :=
                G.obj ((GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).snd b).Y,
              f :=
                G.map ((GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).snd b).f ≫
                  f,
              hf := ⋯ } ≫
          α.app (op ((GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).snd b).Y)) ≫
        (GrothendieckTopology.Cover.index ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩ F).snd b

Tactic:
by

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
⊢ (↑⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).arrows g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
T : C
f : T ⟶ W
⊢ Sieve.pullback f (E.sieve₁ p₁ p₂) = E.sieve₁ (f ≫ p₁) (f ≫ p₂)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
k : E.I₁ i₁ i₂
⊢ E.toPullback k ≫ pullback.fst (E.f i₁) (E.f i₂) = E.p₁ k

Tactic:
by

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).arrows (G.map g ≫ f)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
k : E.I₁ i₁ i₂
⊢ E.toPullback k ≫ pullback.snd (E.f i₁) (E.f i₂) = E.p₂ k

Tactic:
by

Goal state after: