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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
h₁ : K.W = ObjectProperty.isLocal fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
h₂ : ∀ (R : Sheaf J A), (Function.Bijective fun g ↦ G.op.whiskerLeft f ≫ g) ↔ Function.Bijective fun g ↦ f ≫ g
⊢ ObjectProperty.isLocal (fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj)
      (((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).map f) ↔
    ObjectProperty.isLocal (fun x ↦ x ∈ Set.range (sheafToPresheaf J A).obj) f

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
h₁ : K.W = ObjectProperty.isLocal fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
h₂ : ∀ (R : Sheaf J A), (Function.Bijective fun g ↦ G.op.whiskerLeft f ≫ g) ↔ Function.Bijective fun g ↦ f ≫ g
⊢ ObjectProperty.isLocal (fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj)
      (((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).map f) ↔
    ObjectProperty.isLocal (fun x ↦ x ∈ Set.range (sheafToPresheaf J A).obj) f
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✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
x✝ : F.multicospanShape.R
⊢ eqToHom ⋯ ≫ WalkingMulticospan.Hom.snd x✝ = eqToHom ⋯ ≫ WalkingMulticospan.Hom.snd x✝

pp: case w
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
x✝ : F.multicospanShape.R
⊢ ⟨(f.hom.s₀ (f.inv.s₀ x✝.fst.1), f.hom.s₀ (f.inv.s₀ x✝.fst.2)), f.hom.s₁ (f.inv.s₁ x✝.snd)⟩ = x✝

Tactic:
]

Goal state after:
case w
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
x✝ : F.multicospanShape.R
⊢ ⟨(f.hom.s₀ (f.inv.s₀ x✝.fst.1), f.hom.s₀ (f.inv.s₀ x✝.fst.2)), f.hom.s₁ (f.inv.s₁ x✝.snd)⟩ = x✝
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case left
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
a✝ : E.multicospanShape.L
⊢ eqToHom ⋯ ≫ (eqToIso ⋯).hom.app ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left a✝)) =
    𝟙 ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left a✝))

Tactic:
]

Goal state after:
case left
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
a✝ : E.multicospanShape.L
⊢ eqToHom ⋯ ≫ (eqToIso ⋯).hom.app ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left a✝)) =
    𝟙 ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left a✝))
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
a✝ : E.multicospanShape.R
⊢ eqToHom ⋯ ≫ (eqToIso ⋯).hom.app ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.right a✝)) =
    𝟙 ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.right a✝))

Tactic:
]

Goal state after:
case right
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
a✝ : E.multicospanShape.R
⊢ eqToHom ⋯ ≫ (eqToIso ⋯).hom.app ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.right a✝)) =
    𝟙 ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.right a✝))
Module: Mathlib.CategoryTheory.Sites.Equivalence

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ K.W (G.op.whiskerLeft f) ↔ K.W.inverseImage ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op) f

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ K.W (G.op.whiskerLeft f) ↔ K.W.inverseImage ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op) f
Module: Mathlib.CategoryTheory.Sites.Equivalence

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁷ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁶ : Category.{v₄, u₄} B
F : A ⥤ B
inst✝⁵ : G.IsCoverDense J
inst✝⁴ : G.Full
inst✝³ : G.IsContinuous K J
inst✝² : (G.sheafPushforwardContinuous B K J).EssSurj
inst✝¹ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝ : K.PreservesSheafification F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
hf : K.W (G.op.whiskerLeft f)
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁷ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁶ : Category.{v₄, u₄} B
F : A ⥤ B
inst✝⁵ : G.IsCoverDense J
inst✝⁴ : G.Full
inst✝³ : G.IsContinuous K J
inst✝² : (G.sheafPushforwardContinuous B K J).EssSurj
inst✝¹ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝ : K.PreservesSheafification F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
hf : K.W (G.op.whiskerLeft f)
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f
Module: Mathlib.CategoryTheory.Sites.Equivalence

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁷ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁶ : Category.{v₄, u₄} B
F : A ⥤ B
inst✝⁵ : G.IsCoverDense J
inst✝⁴ : G.Full
inst✝³ : G.IsContinuous K J
inst✝² : (G.sheafPushforwardContinuous B K J).EssSurj
inst✝¹ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝ : K.PreservesSheafification F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
hf : K.W (G.op.whiskerLeft f)
this : K.W ((G.op.associator P F).hom ≫ G.op.whiskerLeft (whiskerRight f F) ≫ (G.op.associator Q F).inv)
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁷ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁶ : Category.{v₄, u₄} B
F : A ⥤ B
inst✝⁵ : G.IsCoverDense J
inst✝⁴ : G.Full
inst✝³ : G.IsContinuous K J
inst✝² : (G.sheafPushforwardContinuous B K J).EssSurj
inst✝¹ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝ : K.PreservesSheafification F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
hf : K.W (G.op.whiskerLeft f)
this : K.W ((G.op.associator P F).hom ≫ G.op.whiskerLeft (whiskerRight f F) ≫ (G.op.associator Q F).inv)
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f
Module: Mathlib.CategoryTheory.Sites.Equivalence

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁷ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁶ : Category.{v₄, u₄} B
F : A ⥤ B
inst✝⁵ : G.IsCoverDense J
inst✝⁴ : G.Full
inst✝³ : G.IsContinuous K J
inst✝² : (G.sheafPushforwardContinuous B K J).EssSurj
inst✝¹ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝ : K.PreservesSheafification F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
hf : K.W (G.op.whiskerLeft f)
this✝ : K.W ((G.op.associator P F).hom ≫ G.op.whiskerLeft (whiskerRight f F) ≫ (G.op.associator Q F).inv)
this : J.W (whiskerRight f F)
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁷ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁶ : Category.{v₄, u₄} B
F : A ⥤ B
inst✝⁵ : G.IsCoverDense J
inst✝⁴ : G.Full
inst✝³ : G.IsContinuous K J
inst✝² : (G.sheafPushforwardContinuous B K J).EssSurj
inst✝¹ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝ : K.PreservesSheafification F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
hf : K.W (G.op.whiskerLeft f)
this✝ : K.W ((G.op.associator P F).hom ≫ G.op.whiskerLeft (whiskerRight f F) ≫ (G.op.associator Q F).inv)
this : J.W (whiskerRight f F)
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f
Module: Mathlib.CategoryTheory.Sites.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁸ : Category.{v₃, u₃} A
inst✝⁷ : G.IsCoverDense J
inst✝⁶ : G.Full
inst✝⁵ : G.IsContinuous K J
inst✝⁴ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝³ : G.IsCocontinuous K J
FA : A → A → Type u_1
CA : A → Type u_2
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
inst✝ : K.WEqualsLocallyBijective A
hG : CoverPreserving K J G
X✝ Y✝ : Cᵒᵖ ⥤ A
f : X✝ ⟶ Y✝
⊢ Presheaf.IsLocallyInjective K (G.op.whiskerLeft f) ∧ Presheaf.IsLocallySurjective K (G.op.whiskerLeft f) ↔
    Presheaf.IsLocallyInjective K (G.op.whiskerLeft f) ∧ Presheaf.IsLocallySurjective K (G.op.whiskerLeft f)

Tactic:
]

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
F : PreOneHypercover S
G✝ : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover S
f : G.Hom E
g : G.Hom F
i✝ j✝ : G.I₀
k : G.I₁ i✝ j✝
⊢ G.p₁ k ≫ f.h₀ i✝ ≫ E.f (__spread✝⁻⁰.s₀ i✝).1 = G.p₁ k ≫ g.h₀ i✝ ≫ F.f (__spread✝⁻⁰.s₀ i✝).2

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
F : PreOneHypercover S
G✝ : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover S
f : G.Hom E
g : G.Hom F
i✝ j✝ : G.I₀
k : G.I₁ i✝ j✝
⊢ G.p₁ k ≫ f.h₀ i✝ ≫ E.f (__spread✝⁻⁰.s₀ i✝).1 = G.p₁ k ≫ g.h₀ i✝ ≫ F.f (__spread✝⁻⁰.s₀ i✝).2
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Presieve Y
R : Presieve Y.left := fun Z g ↦ S (Over.homMk g ⋯)
hR : functorPullback (Over.forget X) R = S
⊢ functorPullback (Over.forget X) R = functorPullback (Over.forget X) R

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
⊢ ∀ {a b : Sieve Y}, functorPushforward (Over.forget X) a ≤ functorPushforward (Over.forget X) b ↔ a ≤ b

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
⊢ ∀ {a b : Sieve Y}, functorPushforward (Over.forget X) a ≤ functorPushforward (Over.forget X) b ↔ a ≤ b
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over X := Over.mk (b ≫ W.hom)
⊢ g ≫ Y₁.hom = g ≫ Y₁.hom

Tactic:
]

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over X := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
⊢ S.arrows (d ≫ a)

Tactic:
]

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over X := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
⊢ S.arrows (d ≫ a)
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
⊢ E.sieve₁ (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂)) ∈ J (Limits.pullback (E.f i₁) (E.f i₂))

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
⊢ E.sieve₁ (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂)) ∈ J (Limits.pullback (E.f i₁) (E.f i₂))
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
J : GrothendieckTopology C
S : C
E : PreOneHypercover S
inst✝ : E.HasPullbacks
mem₀ : E.sieve₀ ∈ J S
mem₁' : ∀ (i₁ i₂ : E.I₀), E.sieve₁' i₁ i₂ ∈ J (Limits.pullback (E.f i₁) (E.f i₂))
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
⊢ Sieve.pullback (pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂) ∈ J W

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S : C
E : PreOneHypercover S
inst✝ : E.HasPullbacks
mem₀ : E.sieve₀ ∈ J S
mem₁' : ∀ (i₁ i₂ : E.I₀), E.sieve₁' i₁ i₂ ∈ J (Limits.pullback (E.f i₁) (E.f i₂))
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
⊢ Sieve.pullback (pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂) ∈ J W
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
E : PreOneHypercover Y
i₁ i₂ : E.I₀
W : Over X
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Y✝ : C
f✝ : Y✝ ⟶ W.left
⊢ (E.sieve₁ p₁ p₂).arrows (Over.homMk f✝ ⋯) ↔
    ((E.map (Over.forget X)).sieve₁ (Over.Hom.left p₁) (Over.Hom.left p₂)).arrows f✝

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
E : PreOneHypercover Y
i₁ i₂ : E.I₀
W : Over X
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Y✝ : C
f✝ : Y✝ ⟶ W.left
⊢ (E.sieve₁ p₁ p₂).arrows (Over.homMk f✝ ⋯) ↔
    ((E.map (Over.forget X)).sieve₁ (Over.Hom.left p₁) (Over.Hom.left p₂)).arrows f✝
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

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

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = (ConcreteCategory.hom (F.map f.op)) (x i)
W X : C
a : W ⟶ X
i : I
b : W ⟶ Y i
⊢ (ConcreteCategory.hom (F.map a.op)) (s X) = (ConcreteCategory.hom (F.map b.op)) (x i)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y
Z : C
g : Z ⟶ Y.left
hg : (generate R).arrows (Over.homMk g ⋯)
⊢ (generate (Presieve.functorPushforward (Over.forget X) R)).arrows g

Tactic:
]

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y
Z : C
g : Z ⟶ Y.left
hg : (generate R).arrows (Over.homMk g ⋯)
⊢ (generate (Presieve.functorPushforward (Over.forget X) R)).arrows g
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
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : Sheaf J A
c : Multifork (E.multicospanIndex F.obj)
m : c.pt ⟶ (E.multifork F.obj).pt
hm : ∀ (i : E.multicospanShape.L), m ≫ (E.multifork F.obj).ι i = c.ι i
i₀ : E.I₀
⊢ m ≫ F.obj.map (E.f i₀).op = c.ι i₀

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : Sheaf J A
c : Multifork (E.multicospanIndex F.obj)
m : c.pt ⟶ (E.multifork F.obj).pt
hm : ∀ (i : E.multicospanShape.L), m ≫ (E.multifork F.obj).ι i = c.ι i
i₀ : E.I₀
⊢ m ≫ F.obj.map (E.f i₀).op = c.ι i₀
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y
⊢ Presieve.functorPushforward (Over.forget X) R ≤ ((overEquiv Y) (generate R)).arrows

Tactic:
]

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y
⊢ Presieve.functorPushforward (Over.forget X) R ≤ ((overEquiv Y) (generate R)).arrows
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y.left
Z : Over X
g : Z ⟶ Y
hg : (generate R).arrows (Over.Hom.left g)
⊢ (generate (Presieve.functorPullback (Over.forget X) R)).arrows g

Tactic:
]

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y.left
Z : Over X
g : Z ⟶ Y
hg : (generate R).arrows (Over.Hom.left g)
⊢ (generate (Presieve.functorPullback (Over.forget X) R)).arrows g
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
J : GrothendieckTopology C
S : C
inst✝² : HasPullbacks C
E : J.OneHypercover S
F : J.OneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
i₁ i₂ : (E.inter F.toPreOneHypercover).I₀
W : C
p₁ : W ⟶ (E.inter F.toPreOneHypercover).X i₁
p₂ : W ⟶ (E.inter F.toPreOneHypercover).X i₂
h : p₁ ≫ (E.inter F.toPreOneHypercover).f i₁ = p₂ ≫ (E.inter F.toPreOneHypercover).f i₂
⊢ (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i₁.1) (F.f i₁.2)) (p₂ ≫ pullback.fst (E.f i₂.1) (F.f i₂.2))).arrows
      fun x f x_1 ↦
      Sieve.pullback f (F.sieve₁ (p₁ ≫ pullback.snd (E.f i₁.1) (F.f i₁.2)) (p₂ ≫ pullback.snd (E.f i₂.1) (F.f i₂.2)))) ∈
    J W

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
A : Type u_1
inst✝³ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S : C
inst✝² : HasPullbacks C
E : J.OneHypercover S
F : J.OneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
i₁ i₂ : (E.inter F.toPreOneHypercover).I₀
W : C
p₁ : W ⟶ (E.inter F.toPreOneHypercover).X i₁
p₂ : W ⟶ (E.inter F.toPreOneHypercover).X i₂
h : p₁ ≫ (E.inter F.toPreOneHypercover).f i₁ = p₂ ≫ (E.inter F.toPreOneHypercover).f i₂
⊢ (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i₁.1) (F.f i₁.2)) (p₂ ≫ pullback.fst (E.f i₂.1) (F.f i₂.2))).arrows
      fun x f x_1 ↦
      Sieve.pullback f (F.sieve₁ (p₁ ≫ pullback.snd (E.f i₁.1) (F.f i₁.2)) (p₂ ≫ pullback.snd (E.f i₂.1) (F.f i₂.2)))) ∈
    J W
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y.left
⊢ Presieve.functorPullback (Over.forget X) R ≤ ((overEquiv Y).symm (generate R)).arrows

Tactic:
]

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y.left
⊢ Presieve.functorPullback (Over.forget X) R ≤ ((overEquiv Y).symm (generate R)).arrows
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: case hex
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = (ConcreteCategory.hom (F.map f.op)) (x i)
hs' : ∀ {W X : C} (a : W ⟶ X) (i : I) (x : W ⟶ Y i), (ConcreteCategory.hom (F.map a.op)) (s X) = s W
Y₁ Y₂ : C
f : Y₂ ⟶ Y₁
Z : C
φ : Z ⟶ Y₂
i : I
g : Z ⟶ Y i
⊢ (ConcreteCategory.hom (F.map φ.op)) ((ConcreteCategory.hom (F.map f.op)) (s Y₁)) =
    (ConcreteCategory.hom (F.map f.op ≫ F.map φ.op)) (s Y₁)

Tactic:
]

Goal state after:
case hex
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = (ConcreteCategory.hom (F.map f.op)) (x i)
hs' : ∀ {W X : C} (a : W ⟶ X) (i : I) (x : W ⟶ Y i), (ConcreteCategory.hom (F.map a.op)) (s X) = s W
Y₁ Y₂ : C
f : Y₂ ⟶ Y₁
Z : C
φ : Z ⟶ Y₂
i : I
g : Z ⟶ Y i
⊢ (ConcreteCategory.hom (F.map φ.op)) ((ConcreteCategory.hom (F.map f.op)) (s Y₁)) =
    (ConcreteCategory.hom (F.map f.op ≫ F.map φ.op)) (s Y₁)
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
y₁ y₂ : ↑F.sections
hy₁ : ∀ (i : I), ↑y₁ (Opposite.op (Y i)) = x i
hy₂ : ∀ (i : I), ↑y₂ (Opposite.op (Y i)) = x i
i : I
⊢ x i = x i

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
i j : E.I₀
⊢ ⊤ ≤ E.toPreOneHypercover.sieve₁' i j

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
i j : E.I₀
⊢ ⊤ ≤ E.toPreOneHypercover.sieve₁' i j