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

Goal state before:
pp: 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
⊢ ⟨Z, v⟩ ∈ (pullbackArrows b s).uncurry ↔
    ⟨Z, v⟩ ∈ (fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) '' s.uncurry

Tactic:
constructor

Goal state after:
case mp
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
⊢ ⟨Z, v⟩ ∈ (pullbackArrows b s).uncurry →
    ⟨Z, v⟩ ∈ (fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) '' s.uncurry

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
⊢ ⟨Z, v⟩ ∈ (fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) '' s.uncurry →
    ⟨Z, v⟩ ∈ (pullbackArrows b s).uncurry
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: 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
⊢ ⟨Z, v⟩ ∈ (s.bind t).uncurry ↔
    ∃ i, ∃ (h : i ∈ s.uncurry), ∃ x ∈ (t i.snd ⋯).uncurry, Sigma.map id (fun Z g ↦ g ≫ i.snd) x = ⟨Z, v⟩

Tactic:
constructor

Goal state after:
case mp
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
⊢ ⟨Z, v⟩ ∈ (s.bind t).uncurry →
    ∃ i, ∃ (h : i ∈ s.uncurry), ∃ x ∈ (t i.snd ⋯).uncurry, Sigma.map id (fun Z g ↦ g ≫ i.snd) x = ⟨Z, v⟩

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
⊢ (∃ i, ∃ (h : i ∈ s.uncurry), ∃ x ∈ (t i.snd ⋯).uncurry, Sigma.map id (fun Z g ↦ g ≫ i.snd) x = ⟨Z, v⟩) →
    ⟨Z, v⟩ ∈ (s.bind t).uncurry
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
Z : C
v : Z ⟶ X
⊢ ⟨Z, v⟩ ∈ (ofArrows Y f).uncurry ↔ ∃ y, Y y = Z ∧ f y ≍ v

Tactic:
constructor

Goal state after:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
Z : C
v : Z ⟶ X
⊢ ⟨Z, v⟩ ∈ (ofArrows Y f).uncurry → ∃ y, Y y = Z ∧ f y ≍ v

case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
Z : C
v : Z ⟶ X
⊢ (∃ y, Y y = Z ∧ f y ≍ v) → ⟨Z, v⟩ ∈ (ofArrows Y f).uncurry
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
inst✝ : R.HasPairwisePullbacks
⊢ x.Compatible ↔ x.PullbackCompatible

Tactic:
constructor

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.HasPairwisePullbacks
⊢ x.Compatible → x.PullbackCompatible

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
⊢ x.PullbackCompatible → x.Compatible
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
z₁ z₂ : SecondObj P S
h :
  ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f),
    (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩)) z₁ =
      (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩)) z₂
⊢ z₁ = z₂

Tactic:
by
  apply Limits.Types.limit_ext
  rintro ⟨⟨Y, Z, g, f, hf⟩⟩
  apply h

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
⊢ forkMap P S.arrows ≫ firstMap P S = forkMap P S.arrows ≫ secondMap P S

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
b✝ : (Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' // S.arrows f' }
x✝ : P.obj (op X)
⊢ (ConcreteCategory.hom ((forkMap P S.arrows ≫ firstMap P S) ≫ Pi.π (fun f ↦ P.obj (op f.snd.fst)) b✝)).toFun x✝ =
    (ConcreteCategory.hom ((forkMap P S.arrows ≫ secondMap P S) ≫ Pi.π (fun f ↦ P.obj (op f.snd.fst)) b✝)).toFun x✝
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:
constructor

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

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
⊢ (ConcreteCategory.hom (firstMap P S)) x = (ConcreteCategory.hom (secondMap P S)) x →
    Presieve.FamilyOfElements.SieveCompatible ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
⊢ x.Compatible ↔ x.SieveCompatible

Tactic:
constructor

Goal state after:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
⊢ x.Compatible → x.SieveCompatible

case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
⊢ x.SieveCompatible → x.Compatible
Module: Mathlib.CategoryTheory.Sites.Sieves

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

Tactic:
constructor

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

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

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

Tactic:
rintro _ _ ⟨_, a, b, h, rfl⟩

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Presieve S
Y✝ w✝ : C
a : Y✝ ⟶ w✝
b : w✝ ⟶ S
h : R b
⊢ (ofArrows (fun f ↦ f.obj.left) fun f ↦ f.obj.hom).arrows (a ≫ b)
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'
⊢ (pullback e.hom (ofArrows Z f)).arrows a ↔ (ofArrows Z fun i ↦ f i ≫ e.inv).arrows a

Tactic:
constructor

Goal state after:
case mp
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'
⊢ (pullback e.hom (ofArrows Z f)).arrows a → (ofArrows Z fun i ↦ f i ≫ e.inv).arrows a

case mpr
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'
⊢ (ofArrows Z fun i ↦ f i ≫ e.inv).arrows a → (pullback e.hom (ofArrows Z f)).arrows a
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : I → C
Y Z : C
f : Z ⟶ Y
⊢ pullback f (ofObjects X Y) = ofObjects X Z

Tactic:
ext

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : I → C
Y Z : C
f : Z ⟶ Y
Y✝ : C
f✝ : Y✝ ⟶ Z
⊢ (pullback f (ofObjects X Y)).arrows f✝ ↔ (ofObjects X Z).arrows f✝
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
R : Presieve X
inst✝ : R.HasPullbacks f
W : C
g : W ⟶ Y
⊢ (generate (Presieve.pullbackArrows f R)).arrows g ↔ (pullback f (generate R)).arrows g

Tactic:
constructor

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 : C
g : W ⟶ Y
⊢ (generate (Presieve.pullbackArrows f R)).arrows g → (pullback f (generate R)).arrows g

case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
R : Presieve X
inst✝ : R.HasPullbacks f
W : C
g : W ⟶ Y
⊢ (pullback f (generate R)).arrows g → (generate (Presieve.pullbackArrows f R)).arrows g
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
⊢ (pullback f (generate R)).arrows (h ≫ pullback.snd g f)

Tactic:
rw [Sieve.pullback_apply, assoc, ← pullback.condition, ← assoc]

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
X Y : C
f : X ⟶ Y
R : Presieve X
⊢ generate (Presieve.pushforward f R) = pushforward f (generate R)

Tactic:
ext

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
R : Presieve X
Y✝ : C
f✝ : Y✝ ⟶ Y
⊢ (generate (Presieve.pushforward f R)).arrows f✝ ↔ (pushforward f (generate R)).arrows f✝
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
R : Sieve X
⊢ functorPullback (𝟭 C) R = R

Tactic:
ext

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
R : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (functorPullback (𝟭 C) R).arrows f✝ ↔ R.arrows 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 : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve ((F ⋙ G).obj X)
⊢ functorPullback (F ⋙ G) R = functorPullback F (functorPullback G R)

Tactic:
ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve ((F ⋙ G).obj X)
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (functorPullback (F ⋙ G) R).arrows f✝ ↔ (functorPullback F (functorPullback G R)).arrows 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 : 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:
constructor

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

case mpr
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)
⊢ (firstObjEqFamily P S.arrows).toEquiv ((ConcreteCategory.hom (forkMap P S.arrows)) t) = x → x.IsAmalgamation t
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 : C
f : X ⟶ Y
S : Sieve (F.obj Y)
⊢ functorPullback F (pullback (F.map f) S) = pullback f (functorPullback F S)

Tactic:
ext

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
S : Sieve (F.obj Y)
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (functorPullback F (pullback (F.map f) S)).arrows f✝ ↔ (pullback f (functorPullback F S)).arrows 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 : C
R : Presieve X
Y : D
f : Y ⟶ F.obj X
⊢ Presieve.functorPushforward F (generate R).arrows f ↔ Presieve.functorPushforward F R f

Tactic:
constructor

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Presieve X
Y : D
f : Y ⟶ F.obj X
⊢ Presieve.functorPushforward F (generate R).arrows f → Presieve.functorPushforward F R f

case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Presieve X
Y : D
f : Y ⟶ F.obj X
⊢ Presieve.functorPushforward F R f → Presieve.functorPushforward F (generate R).arrows 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
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : FirstObj P R
⊢ Presieve.FamilyOfElements.PullbackCompatible ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x) ↔
    (ConcreteCategory.hom (firstMap P R)) x = (ConcreteCategory.hom (secondMap P R)) x

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : FirstObj P R
⊢ Presieve.FamilyOfElements.PullbackCompatible ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x) →
    (ConcreteCategory.hom (firstMap P R)) x = (ConcreteCategory.hom (secondMap P R)) x

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : FirstObj P R
⊢ (ConcreteCategory.hom (firstMap P R)) x = (ConcreteCategory.hom (secondMap P R)) x →
    Presieve.FamilyOfElements.PullbackCompatible ((ConcreteCategory.hom (firstObjEqFamily P R).hom) 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
s : Presieve X
⊢ generate (Presieve.map F s) = functorPushforward F (generate s)

Tactic:
ext

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
s : Presieve X
Y✝ : D
f✝ : Y✝ ⟶ F.obj X
⊢ (generate (Presieve.map F s)).arrows f✝ ↔ (functorPushforward F (generate s)).arrows f✝
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ : C
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
⊢ (functorPushforward (𝟭 C) R).arrows f ↔ R.arrows f

Tactic:
constructor

Goal state after:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ : C
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
⊢ (functorPushforward (𝟭 C) R).arrows f → R.arrows f

case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ : C
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
⊢ R.arrows f → (functorPushforward (𝟭 C) R).arrows f
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝¹ : C
R : Sieve X✝¹
X✝ X : C
g : X ⟶ X✝¹
h : X✝ ⟶ (𝟭 C).obj X
hg : R.arrows g
⊢ R.arrows (h ≫ (𝟭 C).map g)

Tactic:
exact R.downward_closed hg h

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 : C
R : Presieve X
⊢ IsSeparatedFor P R ↔ IsSeparatedFor P (generate R).arrows

Tactic:
constructor

Goal state after:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ IsSeparatedFor P R → IsSeparatedFor P (generate R).arrows

case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ IsSeparatedFor P (generate R).arrows → IsSeparatedFor P 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 : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X
⊢ functorPushforward (F ⋙ G) R = functorPushforward G (functorPushforward F R)

Tactic:
ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X
Y✝ : E
f✝ : Y✝ ⟶ (F ⋙ G).obj X
⊢ (functorPushforward (F ⋙ G) R).arrows f✝ ↔ (functorPushforward G (functorPushforward F R)).arrows 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 : C
R : Sieve X
S : Sieve (F.obj X)
⊢ functorPushforward F R ≤ S ↔ R ≤ functorPullback F S

Tactic:
constructor

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Sieve X
S : Sieve (F.obj X)
⊢ functorPushforward F R ≤ S → R ≤ functorPullback F S

case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Sieve X
S : Sieve (F.obj X)
⊢ R ≤ functorPullback F S → functorPushforward F R ≤ S
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
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
⊢ x.IsAmalgamation t ↔ (firstObjEqFamily P R).toEquiv ((ConcreteCategory.hom (forkMap P R)) t) = x

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
⊢ x.IsAmalgamation t → (firstObjEqFamily P R).toEquiv ((ConcreteCategory.hom (forkMap P R)) t) = x

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
⊢ (firstObjEqFamily P R).toEquiv ((ConcreteCategory.hom (forkMap P R)) t) = x → x.IsAmalgamation t
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
X : C
S : Sieve X
e : C ≌ D
Y : D
iYX : Y ⟶ e.functor.obj X
⊢ (functorPushforward e.functor S).arrows iYX ↔ (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX

Tactic:
constructor

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
S : Sieve X
e : C ≌ D
Y : D
iYX : Y ⟶ e.functor.obj X
⊢ (functorPushforward e.functor S).arrows iYX → (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX

case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
S : Sieve X
e : C ≌ D
Y : D
iYX : Y ⟶ e.functor.obj X
⊢ (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX → (functorPushforward e.functor S).arrows iYX
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
e : C ≌ D
U : C
S : Sieve U
⊢ functorPushforward e.inverse (functorPushforward e.functor S) = pullback (e.unitInv.app U) S

Tactic:
ext

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
U : C
S : Sieve U
Y✝ : C
f✝ : Y✝ ⟶ e.inverse.obj (e.functor.obj U)
⊢ (functorPushforward e.inverse (functorPushforward e.functor S)).arrows f✝ ↔ (pullback (e.unitInv.app U) S).arrows 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
e : C ≌ D
X : C
S : Sieve X
⊢ pullback (e.unit.app X) (functorPushforward e.inverse (functorPushforward e.functor S)) = S

Tactic:
ext

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
S : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ (𝟭 C).obj X
⊢ (pullback (e.unit.app X) (functorPushforward e.inverse (functorPushforward e.functor S))).arrows f✝ ↔ S.arrows f✝
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
⊢ (∀ (i : Cone (S.arrows.diagram.op ⋙ P)), Nonempty (Unique (i ⟶ P.mapCone S.arrows.cocone.op))) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), x.SieveCompatible → ∃! t, x.IsAmalgamation t

Tactic:
constructor

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
⊢ (∀ (i : Cone (S.arrows.diagram.op ⋙ P)), Nonempty (Unique (i ⟶ P.mapCone S.arrows.cocone.op))) →
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), x.SieveCompatible → ∃! t, x.IsAmalgamation t

case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
⊢ (∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), x.SieveCompatible → ∃! t, x.IsAmalgamation t) →
    ∀ (i : Cone (S.arrows.diagram.op ⋙ P)), Nonempty (Unique (i ⟶ P.mapCone S.arrows.cocone.op))
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
x : { x // x.Compatible }
⊢ (fun t ↦ ⟨fun Y f hf ↦ (ConcreteCategory.hom (t.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f, ⋯⟩, ⋯⟩)
      ((fun t ↦ { app := fun X_1 ↦ ↾fun f ↦ ↑t (shrinkYonedaObjObjEquiv ↑f) ⋯, naturality := ⋯ }) x) =
    x

Tactic:
ext

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
x : { x // x.Compatible }
Y✝ : C
f✝ : Y✝ ⟶ X
hf✝ : S.arrows f✝
⊢ ↑((fun t ↦ ⟨fun Y f hf ↦ (ConcreteCategory.hom (t.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f, ⋯⟩, ⋯⟩)
          ((fun t ↦ { app := fun X_1 ↦ ↾fun f ↦ ↑t (shrinkYonedaObjObjEquiv ↑f) ⋯, naturality := ⋯ }) x))
      f✝ hf✝ =
    ↑x f✝ hf✝
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type w
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
⊢ Arrows.PullbackCompatible P π ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x) ↔
    (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type w
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
⊢ Arrows.PullbackCompatible P π ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x) →
    (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type w
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
⊢ (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x →
    Arrows.PullbackCompatible P π ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x)
Module: Mathlib.CategoryTheory.Sites.Sieves

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

Tactic:
ext

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (sieveOfSubfunctor S.functorInclusion).arrows f✝ ↔ S.arrows f✝