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

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

Tactic:
·

Goal state after:
case mpr
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
⊢ (∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows) →
    Presieve.IsSheaf J.toGrothendieck P
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
⊢ ∃ W x x, True

pp: case refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
f g : A ⟶ B
⊢ ∃ W h, h ≫ f = h ≫ g

Tactic:
·

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
⊢ ∃ W x x, True
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasIsos
X : C
E F : PreZeroHypercover X
e : E ≅ F
hE : E.presieve₀ ∈ K.coverings X
⊢ F.presieve₀ ≤ Presieve.ofArrows (fun i ↦ F.X i.fst) fun i ↦ F.f i.fst

pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasIsos
X : C
E F : PreZeroHypercover X
e : E ≅ F
hE : E.presieve₀ ∈ K.coverings X
⊢ (Presieve.ofArrows (fun i ↦ F.X i.fst) fun i ↦ F.f i.fst) ≤ F.presieve₀

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasIsos
X : C
E F : PreZeroHypercover X
e : E ≅ F
hE : E.presieve₀ ∈ K.coverings X
⊢ F.presieve₀ ≤ Presieve.ofArrows (fun i ↦ F.X i.fst) fun i ↦ F.f i.fst
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasIsos
X : C
E F : PreZeroHypercover X
e : E ≅ F
hE : E.presieve₀ ∈ K.coverings X
⊢ (Presieve.ofArrows (fun i ↦ F.X i.fst) fun i ↦ F.f i.fst) ≤ F.presieve₀

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasIsos
X : C
E F : PreZeroHypercover X
e : E ≅ F
hE : E.presieve₀ ∈ K.coverings X
⊢ (Presieve.ofArrows (fun i ↦ F.X i.fst) fun i ↦ F.f i.fst) ≤ F.presieve₀
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasIsos
X : C
E F : PreZeroHypercover X
e : E ≅ F
hE : E.presieve₀ ∈ K.coverings X
this : F.presieve₀ = Presieve.ofArrows (fun i ↦ F.X i.fst) fun i ↦ e.inv.h₀ i.fst ≫ E.f (e.inv.s₀ i.fst)
⊢ (Presieve.ofArrows (fun i ↦ E.X (e.inv.s₀ i)) fun i ↦ E.f (e.inv.s₀ i)) ∈ K.coverings X

pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasIsos
X : C
E F : PreZeroHypercover X
e : E ≅ F
hE : E.presieve₀ ∈ K.coverings X
this : F.presieve₀ = Presieve.ofArrows (fun i ↦ F.X i.fst) fun i ↦ e.inv.h₀ i.fst ≫ E.f (e.inv.s₀ i.fst)
⊢ ∀ (i : F.I₀), (Presieve.ofArrows (fun k ↦ F.X i) fun k ↦ e.inv.h₀ i) ∈ K.coverings (E.X (e.inv.s₀ i))

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasIsos
X : C
E F : PreZeroHypercover X
e : E ≅ F
hE : E.presieve₀ ∈ K.coverings X
this : F.presieve₀ = Presieve.ofArrows (fun i ↦ F.X i.fst) fun i ↦ e.inv.h₀ i.fst ≫ E.f (e.inv.s₀ i.fst)
⊢ (Presieve.ofArrows (fun i ↦ E.X (e.inv.s₀ i)) fun i ↦ E.f (e.inv.s₀ i)) ∈ K.coverings X
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: case refine_1.refine_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
U : StructuredArrow X G := IsCofiltered.min (T.obj A) (T.obj B)
A' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToLeft (T.obj A) (T.obj B)))
B' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToRight (T.obj A) (T.obj B)))
⊢ (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).hom ≫
      (F ⋙ G).map (StructuredArrow.Hom.right (IsCofiltered.minToLeft A' B')) =
    A.hom

pp: case refine_1.refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
U : StructuredArrow X G := IsCofiltered.min (T.obj A) (T.obj B)
A' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToLeft (T.obj A) (T.obj B)))
B' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToRight (T.obj A) (T.obj B)))
⊢ (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).hom ≫
      (F ⋙ G).map (StructuredArrow.Hom.right (IsCofiltered.minToRight A' B')) =
    B.hom

Tactic:
·

Goal state after:
case refine_1.refine_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
U : StructuredArrow X G := IsCofiltered.min (T.obj A) (T.obj B)
A' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToLeft (T.obj A) (T.obj B)))
B' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToRight (T.obj A) (T.obj B)))
⊢ (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).hom ≫
      (F ⋙ G).map (StructuredArrow.Hom.right (IsCofiltered.minToLeft A' B')) =
    A.hom
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasIsos
X : C
E F : PreZeroHypercover X
e : E ≅ F
hE : E.presieve₀ ∈ K.coverings X
this : F.presieve₀ = Presieve.ofArrows (fun i ↦ F.X i.fst) fun i ↦ e.inv.h₀ i.fst ≫ E.f (e.inv.s₀ i.fst)
⊢ ∀ (i : F.I₀), (Presieve.ofArrows (fun k ↦ F.X i) fun k ↦ e.inv.h₀ i) ∈ K.coverings (E.X (e.inv.s₀ i))

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasIsos
X : C
E F : PreZeroHypercover X
e : E ≅ F
hE : E.presieve₀ ∈ K.coverings X
this : F.presieve₀ = Presieve.ofArrows (fun i ↦ F.X i.fst) fun i ↦ e.inv.h₀ i.fst ≫ E.f (e.inv.s₀ i.fst)
⊢ ∀ (i : F.I₀), (Presieve.ofArrows (fun k ↦ F.X i) fun k ↦ e.inv.h₀ i) ∈ K.coverings (E.X (e.inv.s₀ i))
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: case refine_1.refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
U : StructuredArrow X G := IsCofiltered.min (T.obj A) (T.obj B)
A' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToLeft (T.obj A) (T.obj B)))
B' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToRight (T.obj A) (T.obj B)))
⊢ (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).hom ≫
      (F ⋙ G).map (StructuredArrow.Hom.right (IsCofiltered.minToRight A' B')) =
    B.hom

Tactic:
·

Goal state after:
case refine_1.refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
U : StructuredArrow X G := IsCofiltered.min (T.obj A) (T.obj B)
A' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToLeft (T.obj A) (T.obj B)))
B' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToRight (T.obj A) (T.obj B)))
⊢ (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).hom ≫
      (F ⋙ G).map (StructuredArrow.Hom.right (IsCofiltered.minToRight A' B')) =
    B.hom
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
f g : A ⟶ B
⊢ ∃ W h, h ≫ f = h ≫ g

Tactic:
·

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
f g : A ⟶ B
⊢ ∃ W h, h ≫ f = h ≫ g
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
S : C
R : Presieve S
⊢ R.preZeroHypercover.presieve₀ ≤ R

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
S : C
R : Presieve S
⊢ R ≤ R.preZeroHypercover.presieve₀

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
S : C
R : Presieve S
⊢ R.preZeroHypercover.presieve₀ ≤ R
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
S : C
R : Presieve S
⊢ R ≤ R.preZeroHypercover.presieve₀

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
S : C
R : Presieve S
⊢ R ≤ R.preZeroHypercover.presieve₀
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: case refine_2.refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
f g : A ⟶ B
U : StructuredArrow X G := IsCofiltered.eq (T.map f) (T.map g)
A' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.eqHom (T.map f) (T.map g)))
B' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.eqHom (T.map f) (T.map g) ≫ T.map f))
f' : A' ⟶ B' := StructuredArrow.homMk (StructuredArrow.Hom.right f) ⋯
g' : A' ⟶ B' := StructuredArrow.homMk (StructuredArrow.Hom.right g) ⋯
⊢ StructuredArrow.homMk (StructuredArrow.Hom.right (IsCofiltered.eqHom f' g')) ⋯ ≫ f =
    StructuredArrow.homMk (StructuredArrow.Hom.right (IsCofiltered.eqHom f' g')) ⋯ ≫ g

Tactic:
·

Goal state after:
case refine_2.refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
f g : A ⟶ B
U : StructuredArrow X G := IsCofiltered.eq (T.map f) (T.map g)
A' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.eqHom (T.map f) (T.map g)))
B' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.eqHom (T.map f) (T.map g) ≫ T.map f))
f' : A' ⟶ B' := StructuredArrow.homMk (StructuredArrow.Hom.right f) ⋯
g' : A' ⟶ B' := StructuredArrow.homMk (StructuredArrow.Hom.right g) ⋯
⊢ StructuredArrow.homMk (StructuredArrow.Hom.right (IsCofiltered.eqHom f' g')) ⋯ ≫ f =
    StructuredArrow.homMk (StructuredArrow.Hom.right (IsCofiltered.eqHom f' g')) ⋯ ≫ g
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ (↑j).fst) (fun j ↦ YT (↑j).snd ⋯) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (↑i).snd
      | Sum.inr i => (eT (↑i).snd ⋯).hom ≫ (↑i).snd }
F : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ YR (↑j).snd ⋯) (fun j ↦ (↑j).fst) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (eR (↑i).snd ⋯).hom ≫ (↑i).snd
      | Sum.inr i => (↑i).snd }
i : E.I₀
⊢ E.X i ≅ F.X ((Equiv.refl E.I₀) i)

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ (↑j).fst) (fun j ↦ YT (↑j).snd ⋯) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (↑i).snd
      | Sum.inr i => (eT (↑i).snd ⋯).hom ≫ (↑i).snd }
F : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ YR (↑j).snd ⋯) (fun j ↦ (↑j).fst) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (eR (↑i).snd ⋯).hom ≫ (↑i).snd
      | Sum.inr i => (↑i).snd }
i : E.I₀
⊢ Iso.hom ?refine_1 ≫ F.f ((Equiv.refl E.I₀) i) = E.f i

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ (↑j).fst) (fun j ↦ YT (↑j).snd ⋯) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (↑i).snd
      | Sum.inr i => (eT (↑i).snd ⋯).hom ≫ (↑i).snd }
F : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ YR (↑j).snd ⋯) (fun j ↦ (↑j).fst) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (eR (↑i).snd ⋯).hom ≫ (↑i).snd
      | Sum.inr i => (↑i).snd }
i : E.I₀
⊢ E.X i ≅ F.X ((Equiv.refl E.I₀) i)
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case refine_1
C : Type u_2
inst✝ : Category.{v_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS : IsSeparatedFor P S ∧ ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
⊢ IsSeparatedFor P T

pp: case refine_2
C : Type u_2
inst✝ : Category.{v_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS : IsSeparatedFor P S ∧ ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
x : FamilyOfElements P T
hx : x.Compatible
⊢ ∃ t, x.IsAmalgamation t

Tactic:
·

Goal state after:
case refine_1
C : Type u_2
inst✝ : Category.{v_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS : IsSeparatedFor P S ∧ ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
⊢ IsSeparatedFor P T
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ (↑j).fst) (fun j ↦ YT (↑j).snd ⋯) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (↑i).snd
      | Sum.inr i => (eT (↑i).snd ⋯).hom ≫ (↑i).snd }
F : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ YR (↑j).snd ⋯) (fun j ↦ (↑j).fst) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (eR (↑i).snd ⋯).hom ≫ (↑i).snd
      | Sum.inr i => (↑i).snd }
i : E.I₀
⊢ (match i with
        | Sum.inl i => id (eR (↑i).snd ⋯).symm
        | Sum.inr i => id (eT (↑i).snd ⋯)).hom ≫
      F.f ((Equiv.refl E.I₀) i) =
    E.f i

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ (↑j).fst) (fun j ↦ YT (↑j).snd ⋯) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (↑i).snd
      | Sum.inr i => (eT (↑i).snd ⋯).hom ≫ (↑i).snd }
F : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ YR (↑j).snd ⋯) (fun j ↦ (↑j).fst) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (eR (↑i).snd ⋯).hom ≫ (↑i).snd
      | Sum.inr i => (↑i).snd }
i : E.I₀
⊢ (match i with
        | Sum.inl i => id (eR (↑i).snd ⋯).symm
        | Sum.inr i => id (eT (↑i).snd ⋯)).hom ≫
      F.f ((Equiv.refl E.I₀) i) =
    E.f i
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
E F : PreZeroHypercover S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
⊢ ∀ ⦃Z : C⦄ (g : Z ⟶ S), E.presieve₀ g → ∃ Y e, F.presieve₀ (e.hom ≫ g)

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
E F : PreZeroHypercover S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
⊢ ∀ ⦃Z : C⦄ (g : Z ⟶ S), F.presieve₀ g → ∃ Y e, E.presieve₀ (e.hom ≫ g)

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
E F : PreZeroHypercover S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
⊢ ∀ ⦃Z : C⦄ (g : Z ⟶ S), E.presieve₀ g → ∃ Y e, F.presieve₀ (e.hom ≫ g)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
E F : PreZeroHypercover S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
⊢ ∀ ⦃Z : C⦄ (g : Z ⟶ S), F.presieve₀ g → ∃ Y e, E.presieve₀ (e.hom ≫ g)

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
E F : PreZeroHypercover S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
⊢ ∀ ⦃Z : C⦄ (g : Z ⟶ S), F.presieve₀ g → ∃ Y e, E.presieve₀ (e.hom ≫ g)
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : K.Saturate X S
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ K.Saturate Y ⊤

pp: case hf
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : K.Saturate X S
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ S.arrows g

Tactic:
·

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : K.Saturate X S
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ K.Saturate Y ⊤