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

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
s : Presieve X
inst✝ : HasPullbacks C
B : C
b : B ⟶ X
Z : C
v : Z ⟶ B
Y : C
u : Y ⟶ X
hu : ⟨Y, u⟩ ∈ s.uncurry
h :
  ((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst = ⟨Z, v⟩.fst ∧
    ((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).snd ≍ ⟨Z, v⟩.snd
⊢ ⟨Z, v⟩ ∈ (pullbackArrows b s).uncurry

Tactic:
]

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
s : Presieve X
inst✝ : HasPullbacks C
B : C
b : B ⟶ X
Z : C
v : Z ⟶ B
Y : C
u : Y ⟶ X
hu : ⟨Y, u⟩ ∈ s.uncurry
h :
  ((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst = ⟨Z, v⟩.fst ∧
    ((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).snd ≍ ⟨Z, v⟩.snd
⊢ ⟨Z, v⟩ ∈ (pullbackArrows b s).uncurry
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
s : Presieve X
inst✝ : HasPullbacks C
B : C
b : B ⟶ X
Y : C
u : Y ⟶ X
hu : ⟨Y, u⟩ ∈ s.uncurry
v : ((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst ⟶ B
h :
  ((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).snd =
    ⟨((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst, v⟩.snd
⊢ ⟨((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst, v⟩ ∈ (pullbackArrows b s).uncurry

Tactic:
]

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
s : Presieve X
inst✝ : HasPullbacks C
B : C
b : B ⟶ X
Y : C
u : Y ⟶ X
hu : ⟨Y, u⟩ ∈ s.uncurry
v : ((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst ⟶ B
h :
  ((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).snd =
    ⟨((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst, v⟩.snd
⊢ ⟨((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst, v⟩ ∈ (pullbackArrows b s).uncurry
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
s : Presieve X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y
Z : C
v : Z ⟶ X
fst✝ : C
f : fst✝ ⟶ X
hf : ⟨fst✝, f⟩ ∈ s.uncurry
Y : C
g : Y ⟶ ⟨fst✝, f⟩.fst
hg : ⟨Y, g⟩ ∈ (t ⟨fst✝, f⟩.snd ⋯).uncurry
h :
  (Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst = ⟨Z, v⟩.fst ∧
    (Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).snd ≍ ⟨Z, v⟩.snd
⊢ ⟨Z, v⟩ ∈ (s.bind t).uncurry

Tactic:
]

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
s : Presieve X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y
Z : C
v : Z ⟶ X
fst✝ : C
f : fst✝ ⟶ X
hf : ⟨fst✝, f⟩ ∈ s.uncurry
Y : C
g : Y ⟶ ⟨fst✝, f⟩.fst
hg : ⟨Y, g⟩ ∈ (t ⟨fst✝, f⟩.snd ⋯).uncurry
h :
  (Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst = ⟨Z, v⟩.fst ∧
    (Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).snd ≍ ⟨Z, v⟩.snd
⊢ ⟨Z, v⟩ ∈ (s.bind t).uncurry
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
s : Presieve X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y
fst✝ : C
f : fst✝ ⟶ X
hf : ⟨fst✝, f⟩ ∈ s.uncurry
Y : C
g : Y ⟶ ⟨fst✝, f⟩.fst
hg : ⟨Y, g⟩ ∈ (t ⟨fst✝, f⟩.snd ⋯).uncurry
v : (Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst ⟶ X
h :
  (Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).snd =
    ⟨(Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst, v⟩.snd
⊢ ⟨(Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst, v⟩ ∈ (s.bind t).uncurry

Tactic:
]

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
s : Presieve X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y
fst✝ : C
f : fst✝ ⟶ X
hf : ⟨fst✝, f⟩ ∈ s.uncurry
Y : C
g : Y ⟶ ⟨fst✝, f⟩.fst
hg : ⟨Y, g⟩ ∈ (t ⟨fst✝, f⟩.snd ⋯).uncurry
v : (Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst ⟶ X
h :
  (Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).snd =
    ⟨(Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst, v⟩.snd
⊢ ⟨(Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst, v⟩ ∈ (s.bind t).uncurry
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
i : ι
v : Y i ⟶ X
h : f i ≍ v
⊢ ⟨Y i, f i⟩ ∈ (ofArrows Y f).uncurry

Tactic:
]

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
i : ι
v : Y i ⟶ X
h : f i ≍ v
⊢ ⟨Y i, f i⟩ ∈ (ofArrows Y f).uncurry
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.HasPairwisePullbacks
t : x.PullbackCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
this : HasPullback f₁ f₂
⊢ (ConcreteCategory.hom (P.map g₂.op)) (x f₂ hf₂) = (ConcreteCategory.hom (P.map g₂.op)) (x f₂ hf₂)

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ (ConcreteCategory.hom (P.map (𝟙 Y).op)) (x f hf) = x f hf

pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ h.choose ≫ ⋯.choose = 𝟙 Y ≫ f

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ (ConcreteCategory.hom (P.map (𝟙 Y).op)) (x f hf) = x f hf

C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ h.choose ≫ ⋯.choose = 𝟙 Y ≫ f
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ h.choose ≫ ⋯.choose = f

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ h.choose ≫ ⋯.choose = f
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
⊢ Presieve.FamilyOfElements.SieveCompatible ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x) ↔
    (ConcreteCategory.hom (firstMap P S)) x = (ConcreteCategory.hom (secondMap P S)) x

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
⊢ Presieve.FamilyOfElements.SieveCompatible ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x) ↔
    (ConcreteCategory.hom (firstMap P S)) x = (ConcreteCategory.hom (secondMap P S)) x
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
R : Presieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
hf : R f
⊢ (generate R).arrows (𝟙 X)

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
R : Presieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
hf : R f
⊢ (generate R).arrows (𝟙 X)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P (generate R).arrows
t : x.SieveCompatible
⊢ (FamilyOfElements.restrict ⋯ x).sieveExtend = x

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P (generate R).arrows
t : x.SieveCompatible
⊢ (FamilyOfElements.restrict ⋯ x).sieveExtend = x
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x₁ x₂ : FamilyOfElements P (generate R).arrows
t₁ : x₁.Compatible
t₂ : x₂.Compatible
h : FamilyOfElements.restrict ⋯ x₁ = FamilyOfElements.restrict ⋯ x₂
⊢ (FamilyOfElements.restrict ⋯ x₁).sieveExtend = (FamilyOfElements.restrict ⋯ x₂).sieveExtend

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x₁ x₂ : FamilyOfElements P (generate R).arrows
t₁ : x₁.Compatible
t₂ : x₂.Compatible
h : FamilyOfElements.restrict ⋯ x₁ = FamilyOfElements.restrict ⋯ x₂
⊢ (FamilyOfElements.restrict ⋯ x₁).sieveExtend = (FamilyOfElements.restrict ⋯ x₂).sieveExtend
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
Z : D
T : Presieve (F.obj Z)
x : FamilyOfElements P T
h : x.Compatible
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ Z
f₂ : Z₂ ⟶ Z
h₁ : Presieve.functorPullback F T f₁
h₂ : Presieve.functorPullback F T f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom ((F.op ⋙ P).map g₁.op)) (FamilyOfElements.functorPullback F x f₁ h₁) =
    (ConcreteCategory.hom ((F.op ⋙ P).map g₂.op)) (FamilyOfElements.functorPullback F x f₂ h₂)

Tactic:
exact h (F.map g₁) (F.map g₂) h₁ h₂ (by simp only [← F.map_comp, eq])

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Presieve S
⊢ (Presieve.ofArrows (fun f ↦ f.obj.left) fun f ↦ f.obj.hom) ≤ (generate R).arrows

Tactic:
]

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Presieve S
⊢ (Presieve.ofArrows (fun f ↦ f.obj.left) fun f ↦ f.obj.hom) ≤ (generate R).arrows
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
⊢ x ((f₂ ≫ f₁) ≫ f) ⋯ = x (f₂ ≫ f₁ ≫ f) ⋯

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
⊢ x ((f₂ ≫ f₁) ≫ f) ⋯ = x (f₂ ≫ f₁ ≫ f) ⋯
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Sieve S
⊢ R = R

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
hg : ∃ i a, g = a ≫ f i
⊢ (ofObjects Y X).arrows g

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
hg : ∃ i a, g = a ≫ f i
⊢ (ofObjects Y X).arrows g
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
⊢ (∃ i, Nonempty (W ⟶ Y i)) → ∃ i a, g = a ≫ f i

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
⊢ (∃ i, Nonempty (W ⟶ Y i)) → ∃ i a, g = a ≫ f i
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
⊢ ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X'), (pullback e.hom (ofArrows Z f)).arrows f_1 ↔ (ofArrows Z fun i ↦ f i ≫ e.inv).arrows f_1

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
⊢ ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X'), (pullback e.hom (ofArrows Z f)).arrows f_1 ↔ (ofArrows Z fun i ↦ f i ≫ e.inv).arrows f_1
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
W : C
a : W ⟶ X'
Y : C
i : I
b : W ⟶ Z i
fac : b ≫ f i = a ≫ e.hom
⊢ b ≫ f i ≫ e.inv = a

Tactic:
by simp [reassoc_of% fac]

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
t :
  ∀ (j : Discrete ((Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' // S.arrows f' })),
    (ConcreteCategory.hom (limit.π (Discrete.functor fun f ↦ P.obj (op f.snd.fst)) j))
        ((ConcreteCategory.hom (firstMap P S)) x) =
      (ConcreteCategory.hom (limit.π (Discrete.functor fun f ↦ P.obj (op f.snd.fst)) j))
        ((ConcreteCategory.hom (secondMap P S)) x)
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
hf : S.arrows f
⊢ (ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x (g ≫ f) ⋯ =
    (ConcreteCategory.hom (P.map g.op)) ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x f hf)

Tactic:
]

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
t :
  ∀ (j : Discrete ((Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' // S.arrows f' })),
    (ConcreteCategory.hom (limit.π (Discrete.functor fun f ↦ P.obj (op f.snd.fst)) j))
        ((ConcreteCategory.hom (firstMap P S)) x) =
      (ConcreteCategory.hom (limit.π (Discrete.functor fun f ↦ P.obj (op f.snd.fst)) j))
        ((ConcreteCategory.hom (secondMap P S)) x)
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
hf : S.arrows f
⊢ (ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x (g ≫ f) ⋯ =
    (ConcreteCategory.hom (P.map g.op)) ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x f hf)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
S : Sieve X
f : Y ⟶ X
⊢ S.arrows f ↔ S.arrows f

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
i : I
g : X ⟶ Y i
Z : C
h : Z ⟶ X
⊢ ∃ i, Nonempty (Z ⟶ Y i)

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
i : I
g : X ⟶ Y i
Z : C
h : Z ⟶ X
⊢ ∃ i, Nonempty (Z ⟶ Y i)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
R : Sieve Z
W : C
h : W ⟶ X
x✝ : (pushforward f (pushforward g R)).arrows h
y : W ⟶ Y
hy : y ≫ f = h
z : W ⟶ Z
hR : z ≫ g = y
hz : R.arrows z
⊢ y ≫ f = h ∧ R.arrows z

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
R : Sieve Z
W : C
h : W ⟶ X
x✝ : (pushforward f (pushforward g R)).arrows h
y : W ⟶ Y
hy : y ≫ f = h
z : W ⟶ Z
hR : z ≫ g = y
hz : R.arrows z
⊢ y ≫ f = h ∧ R.arrows z
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
S : Presieve X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y
f : Y ⟶ X
h : S f
⊢ pushforward f (R h) ≤ bind S R

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
S : Presieve X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y
f : Y ⟶ X
h : S f
⊢ pushforward f (R h) ≤ bind S R
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z✝ : C
f✝ : Y ⟶ X
S✝ R : Sieve X
f : Y ⟶ X
inst✝ : Mono f
S : Sieve Y
Z : C
g g₁ : Z ⟶ Y
hf : g₁ = g
hg₁ : S.arrows g₁
⊢ S.arrows g

Tactic:
]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z✝ : C
f✝ : Y ⟶ X
S✝ R : Sieve X
f : Y ⟶ X
inst✝ : Mono f
S : Sieve Y
Z : C
g g₁ : Z ⟶ Y
hf : g₁ = g
hg₁ : S.arrows g₁
⊢ S.arrows g
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z✝ : C
f✝ : Y ⟶ X
S✝ R : Sieve X
f : Y ⟶ X
inst✝ : Mono f
S : Sieve Y
Z : C
g g₁ : Z ⟶ Y
hf : g₁ = g
hg₁ : S.arrows g₁
⊢ S.arrows g₁

Tactic:
]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z✝ : C
f✝ : Y ⟶ X
S✝ R : Sieve X
f : Y ⟶ X
inst✝ : Mono f
S : Sieve Y
Z : C
g g₁ : Z ⟶ Y
hf : g₁ = g
hg₁ : S.arrows g₁
⊢ S.arrows g₁
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
x : FamilyOfElements P R
h : x.Compatible
Z₁ Z₂ W : C
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ X
f₂ : Z₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (f.app (op W))) ((ConcreteCategory.hom (P.map (Quiver.Hom.op ?g₂))) (x ?f₂ ?h₂)) =
    (ConcreteCategory.hom (f.app (op W))) ((ConcreteCategory.hom (P.map g₂.op)) (x f₂ h₂))

pp: case Y₂
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
x : FamilyOfElements P R
h : x.Compatible
Z₁ Z₂ W : C
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ X
f₂ : Z₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ C

pp: case g₂
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
x : FamilyOfElements P R
h : x.Compatible
Z₁ Z₂ W : C
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ X
f₂ : Z₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ W ⟶ ?Y₂

pp: case f₂
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
x : FamilyOfElements P R
h : x.Compatible
Z₁ Z₂ W : C
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ X
f₂ : Z₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ ?Y₂ ⟶ X

pp: case h₂
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
x : FamilyOfElements P R
h : x.Compatible
Z₁ Z₂ W : C
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ X
f₂ : Z₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ R ?f₂

pp: case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
x : FamilyOfElements P R
h : x.Compatible
Z₁ Z₂ W : C
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ X
f₂ : Z₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ g₁ ≫ f₁ = ?g₂ ≫ ?f₂

Tactic:
]

Goal state after:
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
x : FamilyOfElements P R
h : x.Compatible
Z₁ Z₂ W : C
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ X
f₂ : Z₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ g₁ ≫ f₁ = g₂ ≫ f₂
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
⊢ Presieve.IsSheafFor P S.arrows ↔
    ∀ (a : Presieve.FamilyOfElements P S.arrows),
      (ConcreteCategory.hom (firstMap P S)) ((firstObjEqFamily P S.arrows).toEquiv.symm a) =
          (ConcreteCategory.hom (secondMap P S)) ((firstObjEqFamily P S.arrows).toEquiv.symm a) →
        ∃! x, (ConcreteCategory.hom (forkMap P S.arrows)) x = (firstObjEqFamily P S.arrows).toEquiv.symm a

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
⊢ Presieve.IsSheafFor P S.arrows ↔
    ∀ (a : Presieve.FamilyOfElements P S.arrows),
      (ConcreteCategory.hom (firstMap P S)) ((firstObjEqFamily P S.arrows).toEquiv.symm a) =
          (ConcreteCategory.hom (secondMap P S)) ((firstObjEqFamily P S.arrows).toEquiv.symm a) →
        ∃! x, (ConcreteCategory.hom (forkMap P S.arrows)) x = (firstObjEqFamily P S.arrows).toEquiv.symm a
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
f : P ⟶ Q
h : x.IsAmalgamation t
Y : C
g : Y ⟶ X
hg : R g
⊢ (ConcreteCategory.hom (f.app (op Y))) (x g hg) = (ConcreteCategory.hom (f.app (op Y))) (x g hg)

Tactic:
]

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
R : Presieve X
inst✝ : R.HasPullbacks f
W✝ Y W : C
g : W ⟶ X
hg : R g
h : W✝ ⟶ Limits.pullback g f
this : HasPullback g f
⊢ (generate R).arrows ((h ≫ pullback.fst g f) ≫ g)

Tactic:
]

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
R : Presieve X
inst✝ : R.HasPullbacks f
W✝ Y W : C
g : W ⟶ X
hg : R g
h : W✝ ⟶ Limits.pullback g f
this : HasPullback g f
⊢ (generate R).arrows ((h ≫ pullback.fst g f) ≫ g)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve (F.obj X)
Y✝ Z✝ : C
f : Y✝ ⟶ X
hf : Presieve.functorPullback F R.arrows f
g : Z✝ ⟶ Y✝
⊢ R.arrows (F.map g ≫ F.map f)

Tactic:
]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve (F.obj X)
Y✝ Z✝ : C
f : Y✝ ⟶ X
hf : Presieve.functorPullback F R.arrows f
g : Z✝ ⟶ Y✝
⊢ R.arrows (F.map g ≫ F.map f)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve (F.obj X)
Y✝ Z✝ : C
f : Y✝ ⟶ X
hf : Presieve.functorPullback F R.arrows f
g : Z✝ ⟶ Y✝
⊢ R.arrows (F.map g ≫ F.map f)

Tactic:
exact R.downward_closed hf (F.map g)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
b✝ : x.Compatible
t : P.obj (op X)
⊢ x.IsAmalgamation t ↔ (firstObjEqFamily P S.arrows).toEquiv ((ConcreteCategory.hom (forkMap P S.arrows)) t) = x

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
b✝ : x.Compatible
t : P.obj (op X)
⊢ x.IsAmalgamation t ↔ (firstObjEqFamily P S.arrows).toEquiv ((ConcreteCategory.hom (forkMap P S.arrows)) t) = x
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Presieve (F.obj X)
⊢ Presieve.functorPullback F R ≤ (functorPullback F (generate R)).arrows

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Presieve (F.obj X)
⊢ Presieve.functorPullback F R ≤ (functorPullback F (generate R)).arrows
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (P.map (g₂ ≫ f₂).op)) t =
    (ConcreteCategory.hom (P.map g₂.op)) ((ConcreteCategory.hom (P.map f₂.op)) t)

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (P.map (g₂ ≫ f₂).op)) t =
    (ConcreteCategory.hom (P.map g₂.op)) ((ConcreteCategory.hom (P.map f₂.op)) t)