[GOAL]
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
⊢ FactorsThruAlong S T (𝟙 X) ↔ FactorsThru S T
[PROOFSTEP]
simp [FactorsThruAlong, FactorsThru]
[GOAL]
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
h : S ≤ T
Y : C
g : Y ⟶ X
hg : S g
⊢ 𝟙 Y ≫ g = g
[PROOFSTEP]
simp
[GOAL]
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S : Presieve X
T : Sieve X
h : FactorsThru S T.arrows
⊢ S ≤ T.arrows
[PROOFSTEP]
rintro Y f hf
[GOAL]
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S : Presieve X
T : Sieve X
h : FactorsThru S T.arrows
Y : C
f : Y ⟶ X
hf : f ∈ S
⊢ f ∈ T.arrows
[PROOFSTEP]
obtain ⟨W, i, e, h1, rfl⟩ := h hf
[GOAL]
case intro.intro.intro.intro
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S : Presieve X
T : Sieve X
h : FactorsThru S T.arrows
Y W : C
i : Y ⟶ W
e : W ⟶ X
h1 : T.arrows e
hf : i ≫ e ∈ S
⊢ i ≫ e ∈ T.arrows
[PROOFSTEP]
exact T.downward_closed h1 _
[GOAL]
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type w
H : FactorsThru S T
hS : IsSheafFor P S
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ FactorsThruAlong R S f
⊢ IsSheafFor P T
[PROOFSTEP]
simp only [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor] at *
[GOAL]
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type w
H : FactorsThru S T
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ FactorsThruAlong R S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
⊢ IsSeparatedFor P T ∧
    ∀ (x : FamilyOfElements P T), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
choose W i e h1 h2 using H
[GOAL]
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type w
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ FactorsThruAlong R S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x 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 ∧
    ∀ (x : FamilyOfElements P T), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
refine ⟨?_, fun x hx => ?_⟩
[GOAL]
case refine_1
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type w
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ FactorsThruAlong R S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x 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
[PROOFSTEP]
intro x y₁ y₂ h₁ h₂
[GOAL]
case refine_1
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type w
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ FactorsThruAlong R S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x 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
y₁ y₂ : P.obj (Opposite.op X)
h₁ : FamilyOfElements.IsAmalgamation x y₁
h₂ : FamilyOfElements.IsAmalgamation x y₂
⊢ y₁ = y₂
[PROOFSTEP]
refine hS.1.ext (fun Y g hg => ?_)
[GOAL]
case refine_1
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type w
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ FactorsThruAlong R S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x 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
y₁ y₂ : P.obj (Opposite.op X)
h₁ : FamilyOfElements.IsAmalgamation x y₁
h₂ : FamilyOfElements.IsAmalgamation x y₂
Y : C
g : Y ⟶ X
hg : S g
⊢ P.map g.op y₁ = P.map g.op y₂
[PROOFSTEP]
simp only [← h2 hg, op_comp, P.map_comp, types_comp_apply, h₁ _ (h1 _), h₂ _ (h1 _)]
[GOAL]
case refine_2
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type w
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ FactorsThruAlong R S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x 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 : FamilyOfElements.Compatible x
⊢ ∃ t, FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
let y : S.FamilyOfElements P := fun Y g hg => P.map (i _).op (x (e hg) (h1 _))
[GOAL]
case refine_2
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type w
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ FactorsThruAlong R S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x 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 : FamilyOfElements.Compatible x
y : FamilyOfElements P S := fun Y g hg => P.map (i hg).op (x (e hg) (_ : T (e hg)))
⊢ ∃ t, FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
have hy : y.Compatible := by
  intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ h
  rw [← types_comp_apply (P.map (i h₁).op) (P.map g₁.op), ← types_comp_apply (P.map (i h₂).op) (P.map g₂.op), ←
    P.map_comp, ← op_comp, ← P.map_comp, ← op_comp]
  apply hx
  simp only [h2, h, Category.assoc]
[GOAL]
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type w
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ FactorsThruAlong R S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x 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 : FamilyOfElements.Compatible x
y : FamilyOfElements P S := fun Y g hg => P.map (i hg).op (x (e hg) (_ : T (e hg)))
⊢ FamilyOfElements.Compatible y
[PROOFSTEP]
intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ h
[GOAL]
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type w
h✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ FactorsThruAlong R S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x 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 : FamilyOfElements.Compatible x
y : FamilyOfElements P S := fun Y g hg => P.map (i hg).op (x (e hg) (_ : T (e hg)))
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : S f₁
h₂ : S f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ P.map g₁.op (y f₁ h₁) = P.map g₂.op (y f₂ h₂)
[PROOFSTEP]
rw [← types_comp_apply (P.map (i h₁).op) (P.map g₁.op), ← types_comp_apply (P.map (i h₂).op) (P.map g₂.op), ←
  P.map_comp, ← op_comp, ← P.map_comp, ← op_comp]
[GOAL]
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type w
h✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ FactorsThruAlong R S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x 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 : FamilyOfElements.Compatible x
y : FamilyOfElements P S := fun Y g hg => P.map (i hg).op (x (e hg) (_ : T (e hg)))
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : S f₁
h₂ : S f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ P.map (g₁ ≫ i h₁).op (x (e h₁) (_ : T (e h₁))) = P.map (g₂ ≫ i h₂).op (x (e h₂) (_ : T (e h₂)))
[PROOFSTEP]
apply hx
[GOAL]
case a
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type w
h✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ FactorsThruAlong R S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x 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 : FamilyOfElements.Compatible x
y : FamilyOfElements P S := fun Y g hg => P.map (i hg).op (x (e hg) (_ : T (e hg)))
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : S f₁
h₂ : S f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (g₁ ≫ i h₁) ≫ e h₁ = (g₂ ≫ i h₂) ≫ e h₂
[PROOFSTEP]
simp only [h2, h, Category.assoc]
[GOAL]
case refine_2
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type w
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ FactorsThruAlong R S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x 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 : FamilyOfElements.Compatible x
y : FamilyOfElements P S := fun Y g hg => P.map (i hg).op (x (e hg) (_ : T (e hg)))
hy : FamilyOfElements.Compatible y
⊢ ∃ t, FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
let ⟨_, h2'⟩ := hS
[GOAL]
case refine_2
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type w
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ FactorsThruAlong R S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x 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 : FamilyOfElements.Compatible x
y : FamilyOfElements P S := fun Y g hg => P.map (i hg).op (x (e hg) (_ : T (e hg)))
hy : FamilyOfElements.Compatible y
left✝ : IsSeparatedFor P S
h2' : ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
⊢ ∃ t, FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
obtain ⟨z, hz⟩ := h2' y hy
[GOAL]
case refine_2.intro
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type w
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ FactorsThruAlong R S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x 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 : FamilyOfElements.Compatible x
y : FamilyOfElements P S := fun Y g hg => P.map (i hg).op (x (e hg) (_ : T (e hg)))
hy : FamilyOfElements.Compatible y
left✝ : IsSeparatedFor P S
h2' : ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
z : P.obj (Opposite.op X)
hz : FamilyOfElements.IsAmalgamation y z
⊢ ∃ t, FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
refine ⟨z, fun Y g hg => ?_⟩
[GOAL]
case refine_2.intro
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type w
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ FactorsThruAlong R S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x 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 : FamilyOfElements.Compatible x
y : FamilyOfElements P S := fun Y g hg => P.map (i hg).op (x (e hg) (_ : T (e hg)))
hy : FamilyOfElements.Compatible y
left✝ : IsSeparatedFor P S
h2' : ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
z : P.obj (Opposite.op X)
hz : FamilyOfElements.IsAmalgamation y z
Y : C
g : Y ⟶ X
hg : T g
⊢ P.map g.op z = x g hg
[PROOFSTEP]
obtain ⟨R, hR1, hR2⟩ := h hg
[GOAL]
case refine_2.intro.intro.intro
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type w
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ FactorsThruAlong R S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x 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 : FamilyOfElements.Compatible x
y : FamilyOfElements P S := fun Y g hg => P.map (i hg).op (x (e hg) (_ : T (e hg)))
hy : FamilyOfElements.Compatible y
left✝ : IsSeparatedFor P S
h2' : ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
z : P.obj (Opposite.op X)
hz : FamilyOfElements.IsAmalgamation y z
Y : C
g : Y ⟶ X
hg : T g
R : Presieve Y
hR1 : IsSeparatedFor P R
hR2 : FactorsThruAlong R S g
⊢ P.map g.op z = x g hg
[PROOFSTEP]
choose WW ii ee hh1 hh2 using hR2
[GOAL]
case refine_2.intro.intro.intro
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type w
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ FactorsThruAlong R S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x 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 : FamilyOfElements.Compatible x
y : FamilyOfElements P S := fun Y g hg => P.map (i hg).op (x (e hg) (_ : T (e hg)))
hy : FamilyOfElements.Compatible y
left✝ : IsSeparatedFor P S
h2' : ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
z : P.obj (Opposite.op X)
hz : FamilyOfElements.IsAmalgamation y z
Y : C
g : Y ⟶ X
hg : T g
R : Presieve Y
hR1 : IsSeparatedFor P R
WW : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → R g → C
ii : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → Z ⟶ WW a
ee : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → WW a ⟶ X
hh1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (a : R g), S (ee a)
hh2 : ∀ ⦃Z : C⦄ ⦃g_1 : Z ⟶ Y⦄ (a : R g_1), ii a ≫ ee a = g_1 ≫ g
⊢ P.map g.op z = x g hg
[PROOFSTEP]
refine hR1.ext (fun Q t ht => ?_)
[GOAL]
case refine_2.intro.intro.intro
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type w
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ FactorsThruAlong R S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x 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 : FamilyOfElements.Compatible x
y : FamilyOfElements P S := fun Y g hg => P.map (i hg).op (x (e hg) (_ : T (e hg)))
hy : FamilyOfElements.Compatible y
left✝ : IsSeparatedFor P S
h2' : ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
z : P.obj (Opposite.op X)
hz : FamilyOfElements.IsAmalgamation y z
Y : C
g : Y ⟶ X
hg : T g
R : Presieve Y
hR1 : IsSeparatedFor P R
WW : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → R g → C
ii : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → Z ⟶ WW a
ee : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → WW a ⟶ X
hh1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (a : R g), S (ee a)
hh2 : ∀ ⦃Z : C⦄ ⦃g_1 : Z ⟶ Y⦄ (a : R g_1), ii a ≫ ee a = g_1 ≫ g
Q : C
t : Q ⟶ Y
ht : R t
⊢ P.map t.op (P.map g.op z) = P.map t.op (x g hg)
[PROOFSTEP]
rw [← types_comp_apply (P.map g.op) (P.map t.op), ← P.map_comp, ← op_comp, ← hh2 ht, op_comp, P.map_comp,
  types_comp_apply, hz _ (hh1 _), ← types_comp_apply _ (P.map (ii ht).op), ← P.map_comp, ← op_comp]
[GOAL]
case refine_2.intro.intro.intro
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type w
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ FactorsThruAlong R S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x 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 : FamilyOfElements.Compatible x
y : FamilyOfElements P S := fun Y g hg => P.map (i hg).op (x (e hg) (_ : T (e hg)))
hy : FamilyOfElements.Compatible y
left✝ : IsSeparatedFor P S
h2' : ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
z : P.obj (Opposite.op X)
hz : FamilyOfElements.IsAmalgamation y z
Y : C
g : Y ⟶ X
hg : T g
R : Presieve Y
hR1 : IsSeparatedFor P R
WW : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → R g → C
ii : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → Z ⟶ WW a
ee : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → WW a ⟶ X
hh1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (a : R g), S (ee a)
hh2 : ∀ ⦃Z : C⦄ ⦃g_1 : Z ⟶ Y⦄ (a : R g_1), ii a ≫ ee a = g_1 ≫ g
Q : C
t : Q ⟶ Y
ht : R t
⊢ P.map (ii ht ≫ i (_ : S (ee ht))).op (x (e (_ : S (ee ht))) (_ : T (e (_ : S (ee ht))))) = P.map t.op (x g hg)
[PROOFSTEP]
apply hx
[GOAL]
case refine_2.intro.intro.intro.a
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type w
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ FactorsThruAlong R S f
hS :
  IsSeparatedFor P S ∧
    ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x 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 : FamilyOfElements.Compatible x
y : FamilyOfElements P S := fun Y g hg => P.map (i hg).op (x (e hg) (_ : T (e hg)))
hy : FamilyOfElements.Compatible y
left✝ : IsSeparatedFor P S
h2' : ∀ (x : FamilyOfElements P S), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
z : P.obj (Opposite.op X)
hz : FamilyOfElements.IsAmalgamation y z
Y : C
g : Y ⟶ X
hg : T g
R : Presieve Y
hR1 : IsSeparatedFor P R
WW : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → R g → C
ii : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → Z ⟶ WW a
ee : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → WW a ⟶ X
hh1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (a : R g), S (ee a)
hh2 : ∀ ⦃Z : C⦄ ⦃g_1 : Z ⟶ Y⦄ (a : R g_1), ii a ≫ ee a = g_1 ≫ g
Q : C
t : Q ⟶ Y
ht : R t
⊢ (ii ht ≫ i (_ : S (ee ht))) ≫ e (_ : S (ee ht)) = t ≫ g
[PROOFSTEP]
simp only [Category.assoc, h2, hh2]
[GOAL]
C : Type ?u.25338
inst✝ : Category.{?u.25342, ?u.25338} C
J : GrothendieckTopology C
⊢ ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Presieve X),
    S ∈ (fun X => {S | Sieve.generate S ∈ GrothendieckTopology.sieves J X}) X →
      ∃ T, T ∈ (fun X => {S | Sieve.generate S ∈ GrothendieckTopology.sieves J X}) Y ∧ Presieve.FactorsThruAlong T S f
[PROOFSTEP]
intro X Y f S (hS : Sieve.generate S ∈ J X)
[GOAL]
C : Type ?u.25338
inst✝ : Category.{?u.25342, ?u.25338} C
J : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Presieve X
hS : Sieve.generate S ∈ GrothendieckTopology.sieves J X
⊢ ∃ T, T ∈ (fun X => {S | Sieve.generate S ∈ GrothendieckTopology.sieves J X}) Y ∧ Presieve.FactorsThruAlong T S f
[PROOFSTEP]
refine ⟨(Sieve.generate S).pullback f, ?_, fun Z g h => h⟩
[GOAL]
C : Type ?u.25338
inst✝ : Category.{?u.25342, ?u.25338} C
J : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Presieve X
hS : Sieve.generate S ∈ GrothendieckTopology.sieves J X
⊢ (Sieve.pullback f (Sieve.generate S)).arrows ∈ (fun X => {S | Sieve.generate S ∈ GrothendieckTopology.sieves J X}) Y
[PROOFSTEP]
dsimp
[GOAL]
C : Type ?u.25338
inst✝ : Category.{?u.25342, ?u.25338} C
J : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Presieve X
hS : Sieve.generate S ∈ GrothendieckTopology.sieves J X
⊢ Sieve.generate (Sieve.pullback f (Sieve.generate S)).arrows ∈ GrothendieckTopology.sieves J Y
[PROOFSTEP]
rw [Sieve.generate_sieve]
[GOAL]
C : Type ?u.25338
inst✝ : Category.{?u.25342, ?u.25338} C
J : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Presieve X
hS : Sieve.generate S ∈ GrothendieckTopology.sieves J X
⊢ Sieve.pullback f (Sieve.generate S) ∈ GrothendieckTopology.sieves J Y
[PROOFSTEP]
exact J.pullback_stable _ hS
[GOAL]
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X Y : C
S T : Sieve X
h : S ≤ T
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f T = ⊤
[PROOFSTEP]
ext Z g
[GOAL]
case h
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X Y : C
S T : Sieve X
h : S ≤ T
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ (Sieve.pullback f T).arrows g ↔ ⊤.arrows g
[PROOFSTEP]
simp only [Sieve.pullback_apply, Sieve.top_apply, iff_true]
[GOAL]
case h
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X Y : C
S T : Sieve X
h : S ≤ T
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ T.arrows (g ≫ f)
[PROOFSTEP]
apply h
[GOAL]
case h.a
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X Y : C
S T : Sieve X
h : S ≤ T
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ S.arrows (g ≫ f)
[PROOFSTEP]
apply S.downward_closed
[GOAL]
case h.a.x
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X Y : C
S T : Sieve X
h : S ≤ T
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ S.arrows f
[PROOFSTEP]
exact hf
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : saturate K X S
⊢ saturate K X T
[PROOFSTEP]
apply saturate.transitive _ _ _ hS
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : saturate K X S
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → saturate K Y (Sieve.pullback f T)
[PROOFSTEP]
intro Y g hg
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : saturate K X S
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ saturate K Y (Sieve.pullback g T)
[PROOFSTEP]
rw [eq_top_pullback (h := h)]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : saturate K X S
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ saturate K Y ⊤
[PROOFSTEP]
apply saturate.top
[GOAL]
case hf
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : saturate K X S
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ S.arrows g
[PROOFSTEP]
assumption
[GOAL]
C : Type ?u.30227
inst✝ : Category.{?u.30231, ?u.30227} C
K : Coverage C
⊢ ∀ ⦃X Y : C⦄ ⦃S : Sieve X⦄ (f : Y ⟶ X), S ∈ saturate K X → Sieve.pullback f S ∈ saturate K Y
[PROOFSTEP]
intro X Y S f hS
[GOAL]
C : Type ?u.30227
inst✝ : Category.{?u.30231, ?u.30227} C
K : Coverage C
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ saturate K X
⊢ Sieve.pullback f S ∈ saturate K Y
[PROOFSTEP]
induction hS generalizing Y with
| of X S hS =>
  obtain ⟨R, hR1, hR2⟩ := K.pullback f S hS
  suffices Sieve.generate R ≤ (Sieve.generate S).pullback f from saturate_of_superset _ this (saturate.of _ _ hR1)
  rintro Z g ⟨W, i, e, h1, h2⟩
  obtain ⟨WW, ii, ee, hh1, hh2⟩ := hR2 h1
  refine ⟨WW, i ≫ ii, ee, hh1, ?_⟩
  simp only [hh2, reassoc_of% h2, Category.assoc]
| top X => apply saturate.top
| transitive X R S _ hS H1 _ =>
  apply saturate.transitive
  apply H1 f
  intro Z g hg
  rw [← Sieve.pullback_comp]
  exact hS hg
[GOAL]
C : Type ?u.30227
inst✝ : Category.{?u.30231, ?u.30227} C
K : Coverage C
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ saturate K X
⊢ Sieve.pullback f S ∈ saturate K Y
[PROOFSTEP]
induction hS generalizing Y with
| of X S hS =>
  obtain ⟨R, hR1, hR2⟩ := K.pullback f S hS
  suffices Sieve.generate R ≤ (Sieve.generate S).pullback f from saturate_of_superset _ this (saturate.of _ _ hR1)
  rintro Z g ⟨W, i, e, h1, h2⟩
  obtain ⟨WW, ii, ee, hh1, hh2⟩ := hR2 h1
  refine ⟨WW, i ≫ ii, ee, hh1, ?_⟩
  simp only [hh2, reassoc_of% h2, Category.assoc]
| top X => apply saturate.top
| transitive X R S _ hS H1 _ =>
  apply saturate.transitive
  apply H1 f
  intro Z g hg
  rw [← Sieve.pullback_comp]
  exact hS hg
[GOAL]
case of
C : Type ?u.30227
inst✝ : Category.{?u.30231, ?u.30227} C
K : Coverage C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
Y : C
f : Y ⟶ X
⊢ Sieve.pullback f (Sieve.generate S) ∈ saturate K Y
[PROOFSTEP]

| of X S hS =>
  obtain ⟨R, hR1, hR2⟩ := K.pullback f S hS
  suffices Sieve.generate R ≤ (Sieve.generate S).pullback f from saturate_of_superset _ this (saturate.of _ _ hR1)
  rintro Z g ⟨W, i, e, h1, h2⟩
  obtain ⟨WW, ii, ee, hh1, hh2⟩ := hR2 h1
  refine ⟨WW, i ≫ ii, ee, hh1, ?_⟩
  simp only [hh2, reassoc_of% h2, Category.assoc]
[GOAL]
case of
C : Type ?u.30227
inst✝ : Category.{?u.30231, ?u.30227} C
K : Coverage C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
Y : C
f : Y ⟶ X
⊢ Sieve.pullback f (Sieve.generate S) ∈ saturate K Y
[PROOFSTEP]
obtain ⟨R, hR1, hR2⟩ := K.pullback f S hS
[GOAL]
case of.intro.intro
C : Type ?u.30227
inst✝ : Category.{?u.30231, ?u.30227} C
K : Coverage C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
Y : C
f : Y ⟶ X
R : Presieve Y
hR1 : R ∈ covering K Y
hR2 : Presieve.FactorsThruAlong R S f
⊢ Sieve.pullback f (Sieve.generate S) ∈ saturate K Y
[PROOFSTEP]
suffices Sieve.generate R ≤ (Sieve.generate S).pullback f from saturate_of_superset _ this (saturate.of _ _ hR1)
[GOAL]
case of.intro.intro
C : Type ?u.30227
inst✝ : Category.{?u.30231, ?u.30227} C
K : Coverage C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
Y : C
f : Y ⟶ X
R : Presieve Y
hR1 : R ∈ covering K Y
hR2 : Presieve.FactorsThruAlong R S f
⊢ Sieve.generate R ≤ Sieve.pullback f (Sieve.generate S)
[PROOFSTEP]
rintro Z g ⟨W, i, e, h1, h2⟩
[GOAL]
case of.intro.intro.intro.intro.intro.intro
C : Type ?u.30227
inst✝ : Category.{?u.30231, ?u.30227} C
K : Coverage C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
Y : C
f : Y ⟶ X
R : Presieve Y
hR1 : R ∈ covering K Y
hR2 : Presieve.FactorsThruAlong R S f
Z : C
g : Z ⟶ Y
W : C
i : Z ⟶ W
e : W ⟶ Y
h1 : R e
h2 : i ≫ e = g
⊢ (Sieve.pullback f (Sieve.generate S)).arrows g
[PROOFSTEP]
obtain ⟨WW, ii, ee, hh1, hh2⟩ := hR2 h1
[GOAL]
case of.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type ?u.30227
inst✝ : Category.{?u.30231, ?u.30227} C
K : Coverage C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
Y : C
f : Y ⟶ X
R : Presieve Y
hR1 : R ∈ covering K Y
hR2 : Presieve.FactorsThruAlong R S f
Z : C
g : Z ⟶ Y
W : C
i : Z ⟶ W
e : W ⟶ Y
h1 : R e
h2 : i ≫ e = g
WW : C
ii : W ⟶ WW
ee : WW ⟶ X
hh1 : S ee
hh2 : ii ≫ ee = e ≫ f
⊢ (Sieve.pullback f (Sieve.generate S)).arrows g
[PROOFSTEP]
refine ⟨WW, i ≫ ii, ee, hh1, ?_⟩
[GOAL]
case of.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type ?u.30227
inst✝ : Category.{?u.30231, ?u.30227} C
K : Coverage C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
Y : C
f : Y ⟶ X
R : Presieve Y
hR1 : R ∈ covering K Y
hR2 : Presieve.FactorsThruAlong R S f
Z : C
g : Z ⟶ Y
W : C
i : Z ⟶ W
e : W ⟶ Y
h1 : R e
h2 : i ≫ e = g
WW : C
ii : W ⟶ WW
ee : WW ⟶ X
hh1 : S ee
hh2 : ii ≫ ee = e ≫ f
⊢ (i ≫ ii) ≫ ee = g ≫ f
[PROOFSTEP]
simp only [hh2, reassoc_of% h2, Category.assoc]
[GOAL]
case top
C : Type ?u.30227
inst✝ : Category.{?u.30231, ?u.30227} C
K : Coverage C
X✝ : C
S : Sieve X✝
X Y : C
f : Y ⟶ X
⊢ Sieve.pullback f ⊤ ∈ saturate K Y
[PROOFSTEP]

| top X => apply saturate.top
[GOAL]
case top
C : Type ?u.30227
inst✝ : Category.{?u.30231, ?u.30227} C
K : Coverage C
X✝ : C
S : Sieve X✝
X Y : C
f : Y ⟶ X
⊢ Sieve.pullback f ⊤ ∈ saturate K Y
[PROOFSTEP]
apply saturate.top
[GOAL]
case transitive
C : Type ?u.30227
inst✝ : Category.{?u.30231, ?u.30227} C
K : Coverage C
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝ : saturate K X R
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Sieve.pullback f R ∈ saturate K Y
a_ih✝ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Sieve.pullback f_1 (Sieve.pullback f S) ∈ saturate K Y_1
Y : C
f : Y ⟶ X
⊢ Sieve.pullback f S ∈ saturate K Y
[PROOFSTEP]

| transitive X R S _ hS H1 _ =>
  apply saturate.transitive
  apply H1 f
  intro Z g hg
  rw [← Sieve.pullback_comp]
  exact hS hg
[GOAL]
case transitive
C : Type ?u.30227
inst✝ : Category.{?u.30231, ?u.30227} C
K : Coverage C
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝ : saturate K X R
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Sieve.pullback f R ∈ saturate K Y
a_ih✝ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Sieve.pullback f_1 (Sieve.pullback f S) ∈ saturate K Y_1
Y : C
f : Y ⟶ X
⊢ Sieve.pullback f S ∈ saturate K Y
[PROOFSTEP]
apply saturate.transitive
[GOAL]
case transitive.a
C : Type ?u.30227
inst✝ : Category.{?u.30231, ?u.30227} C
K : Coverage C
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝ : saturate K X R
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Sieve.pullback f R ∈ saturate K Y
a_ih✝ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Sieve.pullback f_1 (Sieve.pullback f S) ∈ saturate K Y_1
Y : C
f : Y ⟶ X
⊢ saturate K Y ?transitive.R
case transitive.a
C : Type ?u.30227
inst✝ : Category.{?u.30231, ?u.30227} C
K : Coverage C
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝ : saturate K X R
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Sieve.pullback f R ∈ saturate K Y
a_ih✝ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Sieve.pullback f_1 (Sieve.pullback f S) ∈ saturate K Y_1
Y : C
f : Y ⟶ X
⊢ ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄, ?transitive.R.arrows f_1 → saturate K Y_1 (Sieve.pullback f_1 (Sieve.pullback f S))
case transitive.R
C : Type ?u.30227
inst✝ : Category.{?u.30231, ?u.30227} C
K : Coverage C
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝ : saturate K X R
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Sieve.pullback f R ∈ saturate K Y
a_ih✝ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Sieve.pullback f_1 (Sieve.pullback f S) ∈ saturate K Y_1
Y : C
f : Y ⟶ X
⊢ Sieve Y
[PROOFSTEP]
apply H1 f
[GOAL]
case transitive.a
C : Type ?u.30227
inst✝ : Category.{?u.30231, ?u.30227} C
K : Coverage C
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝ : saturate K X R
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Sieve.pullback f R ∈ saturate K Y
a_ih✝ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Sieve.pullback f_1 (Sieve.pullback f S) ∈ saturate K Y_1
Y : C
f : Y ⟶ X
⊢ ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄,
    (Sieve.pullback f R).arrows f_1 → saturate K Y_1 (Sieve.pullback f_1 (Sieve.pullback f S))
[PROOFSTEP]
intro Z g hg
[GOAL]
case transitive.a
C : Type ?u.30227
inst✝ : Category.{?u.30231, ?u.30227} C
K : Coverage C
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝ : saturate K X R
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Sieve.pullback f R ∈ saturate K Y
a_ih✝ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Sieve.pullback f_1 (Sieve.pullback f S) ∈ saturate K Y_1
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f R).arrows g
⊢ saturate K Z (Sieve.pullback g (Sieve.pullback f S))
[PROOFSTEP]
rw [← Sieve.pullback_comp]
[GOAL]
case transitive.a
C : Type ?u.30227
inst✝ : Category.{?u.30231, ?u.30227} C
K : Coverage C
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝ : saturate K X R
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Sieve.pullback f R ∈ saturate K Y
a_ih✝ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Sieve.pullback f_1 (Sieve.pullback f S) ∈ saturate K Y_1
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f R).arrows g
⊢ saturate K Z (Sieve.pullback (g ≫ f) S)
[PROOFSTEP]
exact hS hg
[GOAL]
C : Type ?u.34348
inst✝ : Category.{?u.34352, ?u.34348} C
K : Coverage C
J : GrothendieckTopology C
⊢ toGrothendieck C K ≤ J ↔ K ≤ ofGrothendieck C J
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type ?u.34348
inst✝ : Category.{?u.34352, ?u.34348} C
K : Coverage C
J : GrothendieckTopology C
⊢ toGrothendieck C K ≤ J → K ≤ ofGrothendieck C J
[PROOFSTEP]
intro H X S hS
[GOAL]
case mp
C : Type ?u.34348
inst✝ : Category.{?u.34352, ?u.34348} C
K : Coverage C
J : GrothendieckTopology C
H : toGrothendieck C K ≤ J
X : C
S : Presieve X
hS : S ∈ covering K X
⊢ S ∈ covering (ofGrothendieck C J) X
[PROOFSTEP]
exact H _ <| saturate.of _ _ hS
[GOAL]
case mpr
C : Type ?u.34348
inst✝ : Category.{?u.34352, ?u.34348} C
K : Coverage C
J : GrothendieckTopology C
⊢ K ≤ ofGrothendieck C J → toGrothendieck C K ≤ J
[PROOFSTEP]
intro H X S hS
[GOAL]
case mpr
C : Type ?u.34348
inst✝ : Category.{?u.34352, ?u.34348} C
K : Coverage C
J : GrothendieckTopology C
H : K ≤ ofGrothendieck C J
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves (toGrothendieck C K) X
⊢ S ∈ GrothendieckTopology.sieves J X
[PROOFSTEP]
induction hS with
| of X S hS => exact H _ hS
| top => apply J.top_mem
| transitive X R S _ _ H1 H2 => exact J.transitive H1 _ H2
[GOAL]
case mpr
C : Type ?u.34348
inst✝ : Category.{?u.34352, ?u.34348} C
K : Coverage C
J : GrothendieckTopology C
H : K ≤ ofGrothendieck C J
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves (toGrothendieck C K) X
⊢ S ∈ GrothendieckTopology.sieves J X
[PROOFSTEP]
induction hS with
| of X S hS => exact H _ hS
| top => apply J.top_mem
| transitive X R S _ _ H1 H2 => exact J.transitive H1 _ H2
[GOAL]
case mpr.of
C : Type ?u.34348
inst✝ : Category.{?u.34352, ?u.34348} C
K : Coverage C
J : GrothendieckTopology C
H : K ≤ ofGrothendieck C J
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
⊢ Sieve.generate S ∈ GrothendieckTopology.sieves J X
[PROOFSTEP]

| of X S hS => exact H _ hS
[GOAL]
case mpr.of
C : Type ?u.34348
inst✝ : Category.{?u.34352, ?u.34348} C
K : Coverage C
J : GrothendieckTopology C
H : K ≤ ofGrothendieck C J
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
⊢ Sieve.generate S ∈ GrothendieckTopology.sieves J X
[PROOFSTEP]
exact H _ hS
[GOAL]
case mpr.top
C : Type ?u.34348
inst✝ : Category.{?u.34352, ?u.34348} C
K : Coverage C
J : GrothendieckTopology C
H : K ≤ ofGrothendieck C J
X : C
S : Sieve X
X✝ : C
⊢ ⊤ ∈ GrothendieckTopology.sieves J X✝
[PROOFSTEP]

| top => apply J.top_mem
[GOAL]
case mpr.top
C : Type ?u.34348
inst✝ : Category.{?u.34352, ?u.34348} C
K : Coverage C
J : GrothendieckTopology C
H : K ≤ ofGrothendieck C J
X : C
S : Sieve X
X✝ : C
⊢ ⊤ ∈ GrothendieckTopology.sieves J X✝
[PROOFSTEP]
apply J.top_mem
[GOAL]
case mpr.transitive
C : Type ?u.34348
inst✝ : Category.{?u.34352, ?u.34348} C
K : Coverage C
J : GrothendieckTopology C
H : K ≤ ofGrothendieck C J
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
H1 : R ∈ GrothendieckTopology.sieves J X
H2 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Sieve.pullback f S ∈ GrothendieckTopology.sieves J Y
⊢ S ∈ GrothendieckTopology.sieves J X
[PROOFSTEP]

| transitive X R S _ _ H1 H2 => exact J.transitive H1 _ H2
[GOAL]
case mpr.transitive
C : Type ?u.34348
inst✝ : Category.{?u.34352, ?u.34348} C
K : Coverage C
J : GrothendieckTopology C
H : K ≤ ofGrothendieck C J
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
H1 : R ∈ GrothendieckTopology.sieves J X
H2 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Sieve.pullback f S ∈ GrothendieckTopology.sieves J Y
⊢ S ∈ GrothendieckTopology.sieves J X
[PROOFSTEP]
exact J.transitive H1 _ H2
[GOAL]
C : Type ?u.34348
inst✝ : Category.{?u.34352, ?u.34348} C
J : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J X
⊢ S ∈ GrothendieckTopology.sieves (toGrothendieck C (ofGrothendieck C J)) X
[PROOFSTEP]
rw [← Sieve.generate_sieve S]
[GOAL]
C : Type ?u.34348
inst✝ : Category.{?u.34352, ?u.34348} C
J : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J X
⊢ Sieve.generate S.arrows ∈ GrothendieckTopology.sieves (toGrothendieck C (ofGrothendieck C J)) X
[PROOFSTEP]
apply saturate.of
[GOAL]
case hS
C : Type ?u.34348
inst✝ : Category.{?u.34352, ?u.34348} C
J : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J X
⊢ S.arrows ∈ covering (ofGrothendieck C J) X
[PROOFSTEP]
dsimp [ofGrothendieck]
[GOAL]
case hS
C : Type ?u.34348
inst✝ : Category.{?u.34352, ?u.34348} C
J : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J X
⊢ Sieve.generate S.arrows ∈ GrothendieckTopology.sieves J X
[PROOFSTEP]
rwa [Sieve.generate_sieve S]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
⊢ toGrothendieck C K = sInf {J | K ≤ ofGrothendieck C J}
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
⊢ toGrothendieck C K ≤ sInf {J | K ≤ ofGrothendieck C J}
[PROOFSTEP]
apply le_sInf
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
⊢ ∀ (b : GrothendieckTopology C), b ∈ {J | K ≤ ofGrothendieck C J} → toGrothendieck C K ≤ b
[PROOFSTEP]
intro J hJ
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
⊢ toGrothendieck C K ≤ J
[PROOFSTEP]
intro X S hS
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves (toGrothendieck C K) X
⊢ S ∈ GrothendieckTopology.sieves J X
[PROOFSTEP]
induction hS with
| of X S hS => apply hJ; assumption
| top => apply J.top_mem
| transitive X R S _ _ H1 H2 => exact J.transitive H1 _ H2
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves (toGrothendieck C K) X
⊢ S ∈ GrothendieckTopology.sieves J X
[PROOFSTEP]
induction hS with
| of X S hS => apply hJ; assumption
| top => apply J.top_mem
| transitive X R S _ _ H1 H2 => exact J.transitive H1 _ H2
[GOAL]
case a.a.of
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
⊢ Sieve.generate S ∈ GrothendieckTopology.sieves J X
[PROOFSTEP]

| of X S hS => apply hJ; assumption
[GOAL]
case a.a.of
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
⊢ Sieve.generate S ∈ GrothendieckTopology.sieves J X
[PROOFSTEP]
apply hJ
[GOAL]
case a.a.of.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
⊢ S ∈ covering K X
[PROOFSTEP]
assumption
[GOAL]
case a.a.top
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
X : C
S : Sieve X
X✝ : C
⊢ ⊤ ∈ GrothendieckTopology.sieves J X✝
[PROOFSTEP]

| top => apply J.top_mem
[GOAL]
case a.a.top
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
X : C
S : Sieve X
X✝ : C
⊢ ⊤ ∈ GrothendieckTopology.sieves J X✝
[PROOFSTEP]
apply J.top_mem
[GOAL]
case a.a.transitive
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
H1 : R ∈ GrothendieckTopology.sieves J X
H2 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Sieve.pullback f S ∈ GrothendieckTopology.sieves J Y
⊢ S ∈ GrothendieckTopology.sieves J X
[PROOFSTEP]

| transitive X R S _ _ H1 H2 => exact J.transitive H1 _ H2
[GOAL]
case a.a.transitive
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
H1 : R ∈ GrothendieckTopology.sieves J X
H2 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Sieve.pullback f S ∈ GrothendieckTopology.sieves J Y
⊢ S ∈ GrothendieckTopology.sieves J X
[PROOFSTEP]
exact J.transitive H1 _ H2
[GOAL]
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
⊢ sInf {J | K ≤ ofGrothendieck C J} ≤ toGrothendieck C K
[PROOFSTEP]
apply sInf_le
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
⊢ toGrothendieck C K ∈ {J | K ≤ ofGrothendieck C J}
[PROOFSTEP]
intro X S hS
[GOAL]
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
X : C
S : Presieve X
hS : S ∈ covering K X
⊢ S ∈ covering (ofGrothendieck C (toGrothendieck C K)) X
[PROOFSTEP]
apply saturate.of _ _ hS
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheaf (toGrothendieck C K) P ↔ ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheaf (toGrothendieck C K) P → ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
[PROOFSTEP]
intro H X R hR
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : IsSheaf (toGrothendieck C K) P
X : C
R : Presieve X
hR : R ∈ covering K X
⊢ IsSheafFor P R
[PROOFSTEP]
rw [Presieve.isSheafFor_iff_generate]
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : IsSheaf (toGrothendieck C K) P
X : C
R : Presieve X
hR : R ∈ covering K X
⊢ IsSheafFor P (Sieve.generate R).arrows
[PROOFSTEP]
apply H _ <| saturate.of _ _ hR
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
⊢ (∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R) → IsSheaf (toGrothendieck C K) P
[PROOFSTEP]
intro H X S hS
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves (toGrothendieck C K) X
⊢ IsSheafFor P S.arrows
[PROOFSTEP]
suffices ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (S.pullback f).arrows by simpa using this (f := 𝟙 _)
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves (toGrothendieck C K) X
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSheafFor P (Sieve.pullback f S).arrows
⊢ IsSheafFor P S.arrows
[PROOFSTEP]
simpa using this (f := 𝟙 _)
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves (toGrothendieck C K) X
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSheafFor P (Sieve.pullback f S).arrows
[PROOFSTEP]
induction hS with
| of X S hS =>
  intro Y f
  obtain ⟨T, hT1, hT2⟩ := K.pullback f S hS
  apply Presieve.isSheafFor_of_factorsThru (S := T)
  · intro Z g hg
    obtain ⟨W, i, e, h1, h2⟩ := hT2 hg
    exact ⟨Z, 𝟙 _, g, ⟨W, i, e, h1, h2⟩, by simp⟩
  · apply H; assumption
  · intro Z g _
    obtain ⟨R, hR1, hR2⟩ := K.pullback g _ hT1
    refine ⟨R, (H _ hR1).isSeparatedFor, hR2⟩
| top => intros; simpa using Presieve.isSheafFor_top_sieve _
| transitive X R S _ _ H1 H2 =>
  intro Y f
  simp only [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor] at *
  choose H1 H1' using H1
  choose H2 H2' using H2
  refine ⟨?_, fun x hx => ?_⟩
  · intro x t₁ t₂ h₁ h₂
    refine (H1 f).ext (fun Z g hg => ?_)
    refine (H2 hg (𝟙 _)).ext (fun ZZ gg hgg => ?_)
    simp only [Sieve.pullback_id, Sieve.pullback_apply] at hgg
    simp only [← types_comp_apply]
    rw [← P.map_comp, ← op_comp, h₁, h₂]
    simpa only [Sieve.pullback_apply, Category.assoc] using hgg
  let y : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), ((S.pullback (g ≫ f)).pullback (𝟙 _)).arrows.FamilyOfElements P := fun Z g ZZ gg hgg =>
    x (gg ≫ g) (by simpa using hgg)
  have hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible :=
    by
    intro Z g Y₁ Y₂ ZZ g₁ g₂ f₁ f₂ h₁ h₂ h
    rw [hx]
    rw [reassoc_of% h]
  choose z hz using fun ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : R.pullback f g) => H2' hg (𝟙 _) (y g) (hy g)
  let q : (R.pullback f).arrows.FamilyOfElements P := fun Z g hg => z hg
  have hq : q.Compatible := by
    intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ h
    apply (H2 h₁ g₁).ext
    intro ZZ gg hgg
    simp only [← types_comp_apply]
    rw [← P.map_comp, ← P.map_comp, ← op_comp, ← op_comp, hz, hz]
    · dsimp; congr 1; simp only [Category.assoc, h]
    · simpa [reassoc_of% h] using hgg
    · simpa using hgg
  obtain ⟨t, ht⟩ := H1' f q hq
  refine ⟨t, fun Z g hg => ?_⟩
  refine (H1 (g ≫ f)).ext (fun ZZ gg hgg => ?_)
  rw [← types_comp_apply _ (P.map gg.op), ← P.map_comp, ← op_comp, ht]
  swap; simpa using hgg
  refine (H2 hgg (𝟙 _)).ext (fun ZZZ ggg hggg => ?_)
  rw [← types_comp_apply _ (P.map ggg.op), ← P.map_comp, ← op_comp, hz]
  swap; simpa using hggg
  refine (H2 hgg ggg).ext (fun ZZZZ gggg _ => ?_)
  rw [← types_comp_apply _ (P.map gggg.op), ← P.map_comp, ← op_comp]
  apply hx
  simp
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves (toGrothendieck C K) X
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSheafFor P (Sieve.pullback f S).arrows
[PROOFSTEP]
induction hS with
| of X S hS =>
  intro Y f
  obtain ⟨T, hT1, hT2⟩ := K.pullback f S hS
  apply Presieve.isSheafFor_of_factorsThru (S := T)
  · intro Z g hg
    obtain ⟨W, i, e, h1, h2⟩ := hT2 hg
    exact ⟨Z, 𝟙 _, g, ⟨W, i, e, h1, h2⟩, by simp⟩
  · apply H; assumption
  · intro Z g _
    obtain ⟨R, hR1, hR2⟩ := K.pullback g _ hT1
    refine ⟨R, (H _ hR1).isSeparatedFor, hR2⟩
| top => intros; simpa using Presieve.isSheafFor_top_sieve _
| transitive X R S _ _ H1 H2 =>
  intro Y f
  simp only [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor] at *
  choose H1 H1' using H1
  choose H2 H2' using H2
  refine ⟨?_, fun x hx => ?_⟩
  · intro x t₁ t₂ h₁ h₂
    refine (H1 f).ext (fun Z g hg => ?_)
    refine (H2 hg (𝟙 _)).ext (fun ZZ gg hgg => ?_)
    simp only [Sieve.pullback_id, Sieve.pullback_apply] at hgg
    simp only [← types_comp_apply]
    rw [← P.map_comp, ← op_comp, h₁, h₂]
    simpa only [Sieve.pullback_apply, Category.assoc] using hgg
  let y : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), ((S.pullback (g ≫ f)).pullback (𝟙 _)).arrows.FamilyOfElements P := fun Z g ZZ gg hgg =>
    x (gg ≫ g) (by simpa using hgg)
  have hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible :=
    by
    intro Z g Y₁ Y₂ ZZ g₁ g₂ f₁ f₂ h₁ h₂ h
    rw [hx]
    rw [reassoc_of% h]
  choose z hz using fun ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : R.pullback f g) => H2' hg (𝟙 _) (y g) (hy g)
  let q : (R.pullback f).arrows.FamilyOfElements P := fun Z g hg => z hg
  have hq : q.Compatible := by
    intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ h
    apply (H2 h₁ g₁).ext
    intro ZZ gg hgg
    simp only [← types_comp_apply]
    rw [← P.map_comp, ← P.map_comp, ← op_comp, ← op_comp, hz, hz]
    · dsimp; congr 1; simp only [Category.assoc, h]
    · simpa [reassoc_of% h] using hgg
    · simpa using hgg
  obtain ⟨t, ht⟩ := H1' f q hq
  refine ⟨t, fun Z g hg => ?_⟩
  refine (H1 (g ≫ f)).ext (fun ZZ gg hgg => ?_)
  rw [← types_comp_apply _ (P.map gg.op), ← P.map_comp, ← op_comp, ht]
  swap; simpa using hgg
  refine (H2 hgg (𝟙 _)).ext (fun ZZZ ggg hggg => ?_)
  rw [← types_comp_apply _ (P.map ggg.op), ← P.map_comp, ← op_comp, hz]
  swap; simpa using hggg
  refine (H2 hgg ggg).ext (fun ZZZZ gggg _ => ?_)
  rw [← types_comp_apply _ (P.map gggg.op), ← P.map_comp, ← op_comp]
  apply hx
  simp
[GOAL]
case mpr.of
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSheafFor P (Sieve.pullback f (Sieve.generate S)).arrows
[PROOFSTEP]

| of X S hS =>
  intro Y f
  obtain ⟨T, hT1, hT2⟩ := K.pullback f S hS
  apply Presieve.isSheafFor_of_factorsThru (S := T)
  · intro Z g hg
    obtain ⟨W, i, e, h1, h2⟩ := hT2 hg
    exact ⟨Z, 𝟙 _, g, ⟨W, i, e, h1, h2⟩, by simp⟩
  · apply H; assumption
  · intro Z g _
    obtain ⟨R, hR1, hR2⟩ := K.pullback g _ hT1
    refine ⟨R, (H _ hR1).isSeparatedFor, hR2⟩
[GOAL]
case mpr.of
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSheafFor P (Sieve.pullback f (Sieve.generate S)).arrows
[PROOFSTEP]
intro Y f
[GOAL]
case mpr.of
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
Y : C
f : Y ⟶ X
⊢ IsSheafFor P (Sieve.pullback f (Sieve.generate S)).arrows
[PROOFSTEP]
obtain ⟨T, hT1, hT2⟩ := K.pullback f S hS
[GOAL]
case mpr.of.intro.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
Y : C
f : Y ⟶ X
T : Presieve Y
hT1 : T ∈ covering K Y
hT2 : FactorsThruAlong T S f
⊢ IsSheafFor P (Sieve.pullback f (Sieve.generate S)).arrows
[PROOFSTEP]
apply Presieve.isSheafFor_of_factorsThru (S := T)
[GOAL]
case mpr.of.intro.intro.H
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
Y : C
f : Y ⟶ X
T : Presieve Y
hT1 : T ∈ covering K Y
hT2 : FactorsThruAlong T S f
⊢ FactorsThru T (Sieve.pullback f (Sieve.generate S)).arrows
[PROOFSTEP]
intro Z g hg
[GOAL]
case mpr.of.intro.intro.H
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
Y : C
f : Y ⟶ X
T : Presieve Y
hT1 : T ∈ covering K Y
hT2 : FactorsThruAlong T S f
Z : C
g : Z ⟶ Y
hg : T g
⊢ ∃ W i e, (Sieve.pullback f (Sieve.generate S)).arrows e ∧ i ≫ e = g
[PROOFSTEP]
obtain ⟨W, i, e, h1, h2⟩ := hT2 hg
[GOAL]
case mpr.of.intro.intro.H.intro.intro.intro.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
Y : C
f : Y ⟶ X
T : Presieve Y
hT1 : T ∈ covering K Y
hT2 : FactorsThruAlong T S f
Z : C
g : Z ⟶ Y
hg : T g
W : C
i : Z ⟶ W
e : W ⟶ X
h1 : S e
h2 : i ≫ e = g ≫ f
⊢ ∃ W i e, (Sieve.pullback f (Sieve.generate S)).arrows e ∧ i ≫ e = g
[PROOFSTEP]
exact ⟨Z, 𝟙 _, g, ⟨W, i, e, h1, h2⟩, by simp⟩
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
Y : C
f : Y ⟶ X
T : Presieve Y
hT1 : T ∈ covering K Y
hT2 : FactorsThruAlong T S f
Z : C
g : Z ⟶ Y
hg : T g
W : C
i : Z ⟶ W
e : W ⟶ X
h1 : S e
h2 : i ≫ e = g ≫ f
⊢ 𝟙 Z ≫ g = g
[PROOFSTEP]
simp
[GOAL]
case mpr.of.intro.intro.hS
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
Y : C
f : Y ⟶ X
T : Presieve Y
hT1 : T ∈ covering K Y
hT2 : FactorsThruAlong T S f
⊢ IsSheafFor P T
[PROOFSTEP]
apply H
[GOAL]
case mpr.of.intro.intro.hS.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
Y : C
f : Y ⟶ X
T : Presieve Y
hT1 : T ∈ covering K Y
hT2 : FactorsThruAlong T S f
⊢ T ∈ covering K Y
[PROOFSTEP]
assumption
[GOAL]
case mpr.of.intro.intro.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
Y : C
f : Y ⟶ X
T : Presieve Y
hT1 : T ∈ covering K Y
hT2 : FactorsThruAlong T S f
⊢ ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄,
    (Sieve.pullback f (Sieve.generate S)).arrows f_1 → ∃ R, IsSeparatedFor P R ∧ FactorsThruAlong R T f_1
[PROOFSTEP]
intro Z g _
[GOAL]
case mpr.of.intro.intro.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
Y : C
f : Y ⟶ X
T : Presieve Y
hT1 : T ∈ covering K Y
hT2 : FactorsThruAlong T S f
Z : C
g : Z ⟶ Y
a✝ : (Sieve.pullback f (Sieve.generate S)).arrows g
⊢ ∃ R, IsSeparatedFor P R ∧ FactorsThruAlong R T g
[PROOFSTEP]
obtain ⟨R, hR1, hR2⟩ := K.pullback g _ hT1
[GOAL]
case mpr.of.intro.intro.h.intro.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
Y : C
f : Y ⟶ X
T : Presieve Y
hT1 : T ∈ covering K Y
hT2 : FactorsThruAlong T S f
Z : C
g : Z ⟶ Y
a✝ : (Sieve.pullback f (Sieve.generate S)).arrows g
R : Presieve Z
hR1 : R ∈ covering K Z
hR2 : FactorsThruAlong R T g
⊢ ∃ R, IsSeparatedFor P R ∧ FactorsThruAlong R T g
[PROOFSTEP]
refine ⟨R, (H _ hR1).isSeparatedFor, hR2⟩
[GOAL]
case mpr.top
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
X : C
S : Sieve X
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X✝), IsSheafFor P (Sieve.pullback f ⊤).arrows
[PROOFSTEP]

| top => intros; simpa using Presieve.isSheafFor_top_sieve _
[GOAL]
case mpr.top
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
X : C
S : Sieve X
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X✝), IsSheafFor P (Sieve.pullback f ⊤).arrows
[PROOFSTEP]
intros
[GOAL]
case mpr.top
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
X : C
S : Sieve X
X✝ Y✝ : C
f✝ : Y✝ ⟶ X✝
⊢ IsSheafFor P (Sieve.pullback f✝ ⊤).arrows
[PROOFSTEP]
simpa using Presieve.isSheafFor_top_sieve _
[GOAL]
case mpr.transitive
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSheafFor P (Sieve.pullback f R).arrows
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSheafFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSheafFor P (Sieve.pullback f S).arrows
[PROOFSTEP]

| transitive X R S _ _ H1 H2 =>
  intro Y f
  simp only [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor] at *
  choose H1 H1' using H1
  choose H2 H2' using H2
  refine ⟨?_, fun x hx => ?_⟩
  · intro x t₁ t₂ h₁ h₂
    refine (H1 f).ext (fun Z g hg => ?_)
    refine (H2 hg (𝟙 _)).ext (fun ZZ gg hgg => ?_)
    simp only [Sieve.pullback_id, Sieve.pullback_apply] at hgg
    simp only [← types_comp_apply]
    rw [← P.map_comp, ← op_comp, h₁, h₂]
    simpa only [Sieve.pullback_apply, Category.assoc] using hgg
  let y : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), ((S.pullback (g ≫ f)).pullback (𝟙 _)).arrows.FamilyOfElements P := fun Z g ZZ gg hgg =>
    x (gg ≫ g) (by simpa using hgg)
  have hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible :=
    by
    intro Z g Y₁ Y₂ ZZ g₁ g₂ f₁ f₂ h₁ h₂ h
    rw [hx]
    rw [reassoc_of% h]
  choose z hz using fun ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : R.pullback f g) => H2' hg (𝟙 _) (y g) (hy g)
  let q : (R.pullback f).arrows.FamilyOfElements P := fun Z g hg => z hg
  have hq : q.Compatible := by
    intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ h
    apply (H2 h₁ g₁).ext
    intro ZZ gg hgg
    simp only [← types_comp_apply]
    rw [← P.map_comp, ← P.map_comp, ← op_comp, ← op_comp, hz, hz]
    · dsimp; congr 1; simp only [Category.assoc, h]
    · simpa [reassoc_of% h] using hgg
    · simpa using hgg
  obtain ⟨t, ht⟩ := H1' f q hq
  refine ⟨t, fun Z g hg => ?_⟩
  refine (H1 (g ≫ f)).ext (fun ZZ gg hgg => ?_)
  rw [← types_comp_apply _ (P.map gg.op), ← P.map_comp, ← op_comp, ht]
  swap; simpa using hgg
  refine (H2 hgg (𝟙 _)).ext (fun ZZZ ggg hggg => ?_)
  rw [← types_comp_apply _ (P.map ggg.op), ← P.map_comp, ← op_comp, hz]
  swap; simpa using hggg
  refine (H2 hgg ggg).ext (fun ZZZZ gggg _ => ?_)
  rw [← types_comp_apply _ (P.map gggg.op), ← P.map_comp, ← op_comp]
  apply hx
  simp
[GOAL]
case mpr.transitive
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSheafFor P (Sieve.pullback f R).arrows
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSheafFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSheafFor P (Sieve.pullback f S).arrows
[PROOFSTEP]
intro Y f
[GOAL]
case mpr.transitive
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
H : ∀ {X : C} (R : Presieve X), R ∈ covering K X → IsSheafFor P R
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSheafFor P (Sieve.pullback f R).arrows
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSheafFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
Y : C
f : Y ⟶ X
⊢ IsSheafFor P (Sieve.pullback f S).arrows
[PROOFSTEP]
simp only [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor] at *
[GOAL]
case mpr.transitive
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X),
    IsSeparatedFor P (Sieve.pullback f R).arrows ∧
      ∀ (x : FamilyOfElements P (Sieve.pullback f R).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y),
        IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows ∧
          ∀ (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
            FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
⊢ IsSeparatedFor P (Sieve.pullback f S).arrows ∧
    ∀ (x : FamilyOfElements P (Sieve.pullback f S).arrows),
      FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
choose H1 H1' using H1
[GOAL]
case mpr.transitive
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y),
        IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows ∧
          ∀ (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
            FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
⊢ IsSeparatedFor P (Sieve.pullback f S).arrows ∧
    ∀ (x : FamilyOfElements P (Sieve.pullback f S).arrows),
      FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
choose H2 H2' using H2
[GOAL]
case mpr.transitive
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
⊢ IsSeparatedFor P (Sieve.pullback f S).arrows ∧
    ∀ (x : FamilyOfElements P (Sieve.pullback f S).arrows),
      FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
refine ⟨?_, fun x hx => ?_⟩
[GOAL]
case mpr.transitive.refine_1
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
⊢ IsSeparatedFor P (Sieve.pullback f S).arrows
[PROOFSTEP]
intro x t₁ t₂ h₁ h₂
[GOAL]
case mpr.transitive.refine_1
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
t₁ t₂ : P.obj (Opposite.op Y)
h₁ : FamilyOfElements.IsAmalgamation x t₁
h₂ : FamilyOfElements.IsAmalgamation x t₂
⊢ t₁ = t₂
[PROOFSTEP]
refine (H1 f).ext (fun Z g hg => ?_)
[GOAL]
case mpr.transitive.refine_1
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
t₁ t₂ : P.obj (Opposite.op Y)
h₁ : FamilyOfElements.IsAmalgamation x t₁
h₂ : FamilyOfElements.IsAmalgamation x t₂
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f R).arrows g
⊢ P.map g.op t₁ = P.map g.op t₂
[PROOFSTEP]
refine (H2 hg (𝟙 _)).ext (fun ZZ gg hgg => ?_)
[GOAL]
case mpr.transitive.refine_1
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
t₁ t₂ : P.obj (Opposite.op Y)
h₁ : FamilyOfElements.IsAmalgamation x t₁
h₂ : FamilyOfElements.IsAmalgamation x t₂
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f R).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows gg
⊢ P.map gg.op (P.map g.op t₁) = P.map gg.op (P.map g.op t₂)
[PROOFSTEP]
simp only [Sieve.pullback_id, Sieve.pullback_apply] at hgg
[GOAL]
case mpr.transitive.refine_1
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
t₁ t₂ : P.obj (Opposite.op Y)
h₁ : FamilyOfElements.IsAmalgamation x t₁
h₂ : FamilyOfElements.IsAmalgamation x t₂
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f R).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : S.arrows (gg ≫ g ≫ f)
⊢ P.map gg.op (P.map g.op t₁) = P.map gg.op (P.map g.op t₂)
[PROOFSTEP]
simp only [← types_comp_apply]
[GOAL]
case mpr.transitive.refine_1
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
t₁ t₂ : P.obj (Opposite.op Y)
h₁ : FamilyOfElements.IsAmalgamation x t₁
h₂ : FamilyOfElements.IsAmalgamation x t₂
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f R).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : S.arrows (gg ≫ g ≫ f)
⊢ (P.map g.op ≫ P.map gg.op) t₁ = (P.map g.op ≫ P.map gg.op) t₂
[PROOFSTEP]
rw [← P.map_comp, ← op_comp, h₁, h₂]
[GOAL]
case mpr.transitive.refine_1.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
t₁ t₂ : P.obj (Opposite.op Y)
h₁ : FamilyOfElements.IsAmalgamation x t₁
h₂ : FamilyOfElements.IsAmalgamation x t₂
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f R).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : S.arrows (gg ≫ g ≫ f)
⊢ (Sieve.pullback f S).arrows (gg ≫ g)
[PROOFSTEP]
simpa only [Sieve.pullback_apply, Category.assoc] using hgg
[GOAL]
case mpr.transitive.refine_2
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
⊢ ∃ t, FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
let y : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), ((S.pullback (g ≫ f)).pullback (𝟙 _)).arrows.FamilyOfElements P := fun Z g ZZ gg hgg =>
  x (gg ≫ g) (by simpa using hgg)
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
Z : C
g : Z ⟶ Y
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows gg
⊢ (Sieve.pullback f S).arrows (gg ≫ g)
[PROOFSTEP]
simpa using hgg
[GOAL]
case mpr.transitive.refine_2
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
⊢ ∃ t, FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
have hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible :=
  by
  intro Z g Y₁ Y₂ ZZ g₁ g₂ f₁ f₂ h₁ h₂ h
  rw [hx]
  rw [reassoc_of% h]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
⊢ ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
[PROOFSTEP]
intro Z g Y₁ Y₂ ZZ g₁ g₂ f₁ f₂ h₁ h₂ h
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
Z : C
g : Z ⟶ Y
Y₁ Y₂ ZZ : C
g₁ : ZZ ⟶ Y₁
g₂ : ZZ ⟶ Y₂
f₁ : Y₁ ⟶ Z
f₂ : Y₂ ⟶ Z
h₁ : (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows f₁
h₂ : (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ P.map g₁.op (y g f₁ h₁) = P.map g₂.op (y g f₂ h₂)
[PROOFSTEP]
rw [hx]
[GOAL]
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
Z : C
g : Z ⟶ Y
Y₁ Y₂ ZZ : C
g₁ : ZZ ⟶ Y₁
g₂ : ZZ ⟶ Y₂
f₁ : Y₁ ⟶ Z
f₂ : Y₂ ⟶ Z
h₁ : (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows f₁
h₂ : (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ g₁ ≫ f₁ ≫ g = g₂ ≫ f₂ ≫ g
[PROOFSTEP]
rw [reassoc_of% h]
[GOAL]
case mpr.transitive.refine_2
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
⊢ ∃ t, FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
choose z hz using fun ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : R.pullback f g) => H2' hg (𝟙 _) (y g) (hy g)
[GOAL]
case mpr.transitive.refine_2
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
⊢ ∃ t, FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
let q : (R.pullback f).arrows.FamilyOfElements P := fun Z g hg => z hg
[GOAL]
case mpr.transitive.refine_2
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
⊢ ∃ t, FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
have hq : q.Compatible := by
  intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ h
  apply (H2 h₁ g₁).ext
  intro ZZ gg hgg
  simp only [← types_comp_apply]
  rw [← P.map_comp, ← P.map_comp, ← op_comp, ← op_comp, hz, hz]
  · dsimp; congr 1; simp only [Category.assoc, h]
  · simpa [reassoc_of% h] using hgg
  · simpa using hgg
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
⊢ FamilyOfElements.Compatible q
[PROOFSTEP]
intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ h
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Y
f₂ : Y₂ ⟶ Y
h₁ : (Sieve.pullback f R).arrows f₁
h₂ : (Sieve.pullback f R).arrows f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ P.map g₁.op (q f₁ h₁) = P.map g₂.op (q f₂ h₂)
[PROOFSTEP]
apply (H2 h₁ g₁).ext
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Y
f₂ : Y₂ ⟶ Y
h₁ : (Sieve.pullback f R).arrows f₁
h₂ : (Sieve.pullback f R).arrows f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Z⦄,
    (Sieve.pullback g₁ (Sieve.pullback (f₁ ≫ f) S)).arrows f_1 →
      P.map f_1.op (P.map g₁.op (q f₁ h₁)) = P.map f_1.op (P.map g₂.op (q f₂ h₂))
[PROOFSTEP]
intro ZZ gg hgg
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Y
f₂ : Y₂ ⟶ Y
h₁ : (Sieve.pullback f R).arrows f₁
h₂ : (Sieve.pullback f R).arrows f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback g₁ (Sieve.pullback (f₁ ≫ f) S)).arrows gg
⊢ P.map gg.op (P.map g₁.op (q f₁ h₁)) = P.map gg.op (P.map g₂.op (q f₂ h₂))
[PROOFSTEP]
simp only [← types_comp_apply]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Y
f₂ : Y₂ ⟶ Y
h₁ : (Sieve.pullback f R).arrows f₁
h₂ : (Sieve.pullback f R).arrows f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback g₁ (Sieve.pullback (f₁ ≫ f) S)).arrows gg
⊢ (P.map g₁.op ≫ P.map gg.op) (z h₁) = (P.map g₂.op ≫ P.map gg.op) (z h₂)
[PROOFSTEP]
rw [← P.map_comp, ← P.map_comp, ← op_comp, ← op_comp, hz, hz]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Y
f₂ : Y₂ ⟶ Y
h₁ : (Sieve.pullback f R).arrows f₁
h₂ : (Sieve.pullback f R).arrows f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback g₁ (Sieve.pullback (f₁ ≫ f) S)).arrows gg
⊢ y f₁ (gg ≫ g₁) ?h = y f₂ (gg ≫ g₂) ?h
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Y
f₂ : Y₂ ⟶ Y
h₁ : (Sieve.pullback f R).arrows f₁
h₂ : (Sieve.pullback f R).arrows f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback g₁ (Sieve.pullback (f₁ ≫ f) S)).arrows gg
⊢ x ((gg ≫ g₁) ≫ f₁) (_ : S.arrows (((gg ≫ g₁) ≫ f₁) ≫ f)) = x ((gg ≫ g₂) ≫ f₂) (_ : S.arrows (((gg ≫ g₂) ≫ f₂) ≫ f))
[PROOFSTEP]
congr 1
[GOAL]
case e_f
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Y
f₂ : Y₂ ⟶ Y
h₁ : (Sieve.pullback f R).arrows f₁
h₂ : (Sieve.pullback f R).arrows f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback g₁ (Sieve.pullback (f₁ ≫ f) S)).arrows gg
⊢ (gg ≫ g₁) ≫ f₁ = (gg ≫ g₂) ≫ f₂
[PROOFSTEP]
simp only [Category.assoc, h]
[GOAL]
case h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Y
f₂ : Y₂ ⟶ Y
h₁ : (Sieve.pullback f R).arrows f₁
h₂ : (Sieve.pullback f R).arrows f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback g₁ (Sieve.pullback (f₁ ≫ f) S)).arrows gg
⊢ (Sieve.pullback (𝟙 Y₂) (Sieve.pullback (f₂ ≫ f) S)).arrows (gg ≫ g₂)
[PROOFSTEP]
simpa [reassoc_of% h] using hgg
[GOAL]
case h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Y
f₂ : Y₂ ⟶ Y
h₁ : (Sieve.pullback f R).arrows f₁
h₂ : (Sieve.pullback f R).arrows f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback g₁ (Sieve.pullback (f₁ ≫ f) S)).arrows gg
⊢ (Sieve.pullback (𝟙 Y₁) (Sieve.pullback (f₁ ≫ f) S)).arrows (gg ≫ g₁)
[PROOFSTEP]
simpa using hgg
[GOAL]
case mpr.transitive.refine_2
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
hq : FamilyOfElements.Compatible q
⊢ ∃ t, FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
obtain ⟨t, ht⟩ := H1' f q hq
[GOAL]
case mpr.transitive.refine_2.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
hq : FamilyOfElements.Compatible q
t : P.obj (Opposite.op Y)
ht : FamilyOfElements.IsAmalgamation q t
⊢ ∃ t, FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
refine ⟨t, fun Z g hg => ?_⟩
[GOAL]
case mpr.transitive.refine_2.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
hq : FamilyOfElements.Compatible q
t : P.obj (Opposite.op Y)
ht : FamilyOfElements.IsAmalgamation q t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
⊢ P.map g.op t = x g hg
[PROOFSTEP]
refine (H1 (g ≫ f)).ext (fun ZZ gg hgg => ?_)
[GOAL]
case mpr.transitive.refine_2.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
hq : FamilyOfElements.Compatible q
t : P.obj (Opposite.op Y)
ht : FamilyOfElements.IsAmalgamation q t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
⊢ P.map gg.op (P.map g.op t) = P.map gg.op (x g hg)
[PROOFSTEP]
rw [← types_comp_apply _ (P.map gg.op), ← P.map_comp, ← op_comp, ht]
[GOAL]
case mpr.transitive.refine_2.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
hq : FamilyOfElements.Compatible q
t : P.obj (Opposite.op Y)
ht : FamilyOfElements.IsAmalgamation q t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
⊢ q (gg ≫ g) ?mpr.transitive.refine_2.intro.h = P.map gg.op (x g hg)
case mpr.transitive.refine_2.intro.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
hq : FamilyOfElements.Compatible q
t : P.obj (Opposite.op Y)
ht : FamilyOfElements.IsAmalgamation q t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
⊢ (Sieve.pullback f R).arrows (gg ≫ g)
[PROOFSTEP]
swap
[GOAL]
case mpr.transitive.refine_2.intro.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
hq : FamilyOfElements.Compatible q
t : P.obj (Opposite.op Y)
ht : FamilyOfElements.IsAmalgamation q t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
⊢ (Sieve.pullback f R).arrows (gg ≫ g)
case mpr.transitive.refine_2.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
hq : FamilyOfElements.Compatible q
t : P.obj (Opposite.op Y)
ht : FamilyOfElements.IsAmalgamation q t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
⊢ q (gg ≫ g) ?mpr.transitive.refine_2.intro.h = P.map gg.op (x g hg)
[PROOFSTEP]
simpa using hgg
[GOAL]
case mpr.transitive.refine_2.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
hq : FamilyOfElements.Compatible q
t : P.obj (Opposite.op Y)
ht : FamilyOfElements.IsAmalgamation q t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
⊢ q (gg ≫ g) (_ : (Sieve.pullback f R).arrows (gg ≫ g)) = P.map gg.op (x g hg)
[PROOFSTEP]
refine (H2 hgg (𝟙 _)).ext (fun ZZZ ggg hggg => ?_)
[GOAL]
case mpr.transitive.refine_2.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
hq : FamilyOfElements.Compatible q
t : P.obj (Opposite.op Y)
ht : FamilyOfElements.IsAmalgamation q t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
ZZZ : C
ggg : ZZZ ⟶ ZZ
hggg : (Sieve.pullback (𝟙 ZZ) (Sieve.pullback (gg ≫ g ≫ f) S)).arrows ggg
⊢ P.map ggg.op (q (gg ≫ g) (_ : (Sieve.pullback f R).arrows (gg ≫ g))) = P.map ggg.op (P.map gg.op (x g hg))
[PROOFSTEP]
rw [← types_comp_apply _ (P.map ggg.op), ← P.map_comp, ← op_comp, hz]
[GOAL]
case mpr.transitive.refine_2.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
hq : FamilyOfElements.Compatible q
t : P.obj (Opposite.op Y)
ht : FamilyOfElements.IsAmalgamation q t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
ZZZ : C
ggg : ZZZ ⟶ ZZ
hggg : (Sieve.pullback (𝟙 ZZ) (Sieve.pullback (gg ≫ g ≫ f) S)).arrows ggg
⊢ y (gg ≫ g) ggg ?mpr.transitive.refine_2.intro.h = P.map (ggg ≫ gg).op (x g hg)
case mpr.transitive.refine_2.intro.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
hq : FamilyOfElements.Compatible q
t : P.obj (Opposite.op Y)
ht : FamilyOfElements.IsAmalgamation q t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
ZZZ : C
ggg : ZZZ ⟶ ZZ
hggg : (Sieve.pullback (𝟙 ZZ) (Sieve.pullback (gg ≫ g ≫ f) S)).arrows ggg
⊢ (Sieve.pullback (𝟙 ZZ) (Sieve.pullback ((gg ≫ g) ≫ f) S)).arrows ggg
[PROOFSTEP]
swap
[GOAL]
case mpr.transitive.refine_2.intro.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
hq : FamilyOfElements.Compatible q
t : P.obj (Opposite.op Y)
ht : FamilyOfElements.IsAmalgamation q t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
ZZZ : C
ggg : ZZZ ⟶ ZZ
hggg : (Sieve.pullback (𝟙 ZZ) (Sieve.pullback (gg ≫ g ≫ f) S)).arrows ggg
⊢ (Sieve.pullback (𝟙 ZZ) (Sieve.pullback ((gg ≫ g) ≫ f) S)).arrows ggg
case mpr.transitive.refine_2.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
hq : FamilyOfElements.Compatible q
t : P.obj (Opposite.op Y)
ht : FamilyOfElements.IsAmalgamation q t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
ZZZ : C
ggg : ZZZ ⟶ ZZ
hggg : (Sieve.pullback (𝟙 ZZ) (Sieve.pullback (gg ≫ g ≫ f) S)).arrows ggg
⊢ y (gg ≫ g) ggg ?mpr.transitive.refine_2.intro.h = P.map (ggg ≫ gg).op (x g hg)
[PROOFSTEP]
simpa using hggg
[GOAL]
case mpr.transitive.refine_2.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
hq : FamilyOfElements.Compatible q
t : P.obj (Opposite.op Y)
ht : FamilyOfElements.IsAmalgamation q t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
ZZZ : C
ggg : ZZZ ⟶ ZZ
hggg : (Sieve.pullback (𝟙 ZZ) (Sieve.pullback (gg ≫ g ≫ f) S)).arrows ggg
⊢ y (gg ≫ g) ggg (_ : (Sieve.pullback (𝟙 ZZ) (Sieve.pullback ((gg ≫ g) ≫ f) S)).arrows ggg) =
    P.map (ggg ≫ gg).op (x g hg)
[PROOFSTEP]
refine (H2 hgg ggg).ext (fun ZZZZ gggg _ => ?_)
[GOAL]
case mpr.transitive.refine_2.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
hq : FamilyOfElements.Compatible q
t : P.obj (Opposite.op Y)
ht : FamilyOfElements.IsAmalgamation q t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
ZZZ : C
ggg : ZZZ ⟶ ZZ
hggg : (Sieve.pullback (𝟙 ZZ) (Sieve.pullback (gg ≫ g ≫ f) S)).arrows ggg
ZZZZ : C
gggg : ZZZZ ⟶ ZZZ
x✝ : (Sieve.pullback ggg (Sieve.pullback (gg ≫ g ≫ f) S)).arrows gggg
⊢ P.map gggg.op (y (gg ≫ g) ggg (_ : (Sieve.pullback (𝟙 ZZ) (Sieve.pullback ((gg ≫ g) ≫ f) S)).arrows ggg)) =
    P.map gggg.op (P.map (ggg ≫ gg).op (x g hg))
[PROOFSTEP]
rw [← types_comp_apply _ (P.map gggg.op), ← P.map_comp, ← op_comp]
[GOAL]
case mpr.transitive.refine_2.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
hq : FamilyOfElements.Compatible q
t : P.obj (Opposite.op Y)
ht : FamilyOfElements.IsAmalgamation q t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
ZZZ : C
ggg : ZZZ ⟶ ZZ
hggg : (Sieve.pullback (𝟙 ZZ) (Sieve.pullback (gg ≫ g ≫ f) S)).arrows ggg
ZZZZ : C
gggg : ZZZZ ⟶ ZZZ
x✝ : (Sieve.pullback ggg (Sieve.pullback (gg ≫ g ≫ f) S)).arrows gggg
⊢ P.map gggg.op (y (gg ≫ g) ggg (_ : (Sieve.pullback (𝟙 ZZ) (Sieve.pullback ((gg ≫ g) ≫ f) S)).arrows ggg)) =
    P.map (gggg ≫ ggg ≫ gg).op (x g hg)
[PROOFSTEP]
apply hx
[GOAL]
case mpr.transitive.refine_2.intro.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
P : Cᵒᵖ ⥤ Type w
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X : C} (R : Presieve X),
    R ∈ covering K X →
      IsSeparatedFor P R ∧
        ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : FamilyOfElements P (Sieve.pullback f R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (Sieve.pullback f S).arrows
hx : FamilyOfElements.Compatible x
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg => x (gg ≫ g) (_ : (Sieve.pullback f S).arrows (gg ≫ g))
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), FamilyOfElements.Compatible (y g)
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), FamilyOfElements.IsAmalgamation (y g) (z hg)
q : FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg => z hg
hq : FamilyOfElements.Compatible q
t : P.obj (Opposite.op Y)
ht : FamilyOfElements.IsAmalgamation q t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
ZZZ : C
ggg : ZZZ ⟶ ZZ
hggg : (Sieve.pullback (𝟙 ZZ) (Sieve.pullback (gg ≫ g ≫ f) S)).arrows ggg
ZZZZ : C
gggg : ZZZZ ⟶ ZZZ
x✝ : (Sieve.pullback ggg (Sieve.pullback (gg ≫ g ≫ f) S)).arrows gggg
⊢ gggg ≫ ggg ≫ gg ≫ g = (gggg ≫ ggg ≫ gg) ≫ g
[PROOFSTEP]
simp