C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v₁
x : functor S ⟶ P
g : yoneda.obj X ⟶ P
⊢ functorInclusion S ≫ g = x ↔
    ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (↑yonedaEquiv g) = x.app Y.op { val := f, property := h }
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v₁
x : functor S ⟶ P
g : yoneda.obj X ⟶ P
⊢ functorInclusion S ≫ g = x ↔ FamilyOfElements.IsAmalgamation (↑(↑natTransEquivCompatibleFamily x)) (↑yonedaEquiv g)
change _ ↔ ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S f), P.map f.op (yonedaEquiv g) = x.app (op Y) ⟨f, h⟩
case mp
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v₁
x : functor S ⟶ P
g : yoneda.obj X ⟶ P
⊢ functorInclusion S ≫ g = x →
    ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (↑yonedaEquiv g) = x.app Y.op { val := f, property := h }

case mpr
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v₁
x : functor S ⟶ P
g : yoneda.obj X ⟶ P
⊢ (∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (↑yonedaEquiv g) = x.app Y.op { val := f, property := h }) →
    functorInclusion S ≫ g = x
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v₁
x : functor S ⟶ P
g : yoneda.obj X ⟶ P
⊢ functorInclusion S ≫ g = x ↔
    ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (↑yonedaEquiv g) = x.app Y.op { val := f, property := h }
constructor
case mp
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v₁
g : yoneda.obj X ⟶ P
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ P.map f.op (↑yonedaEquiv g) = (functorInclusion S ≫ g).app Y.op { val := f, property := hf }
case mp
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v₁
x : functor S ⟶ P
g : yoneda.obj X ⟶ P
⊢ functorInclusion S ≫ g = x →
    ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (↑yonedaEquiv g) = x.app Y.op { val := f, property := h }
rintro rfl Y f hf
case mp
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v₁
g : yoneda.obj X ⟶ P
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ↑yonedaEquiv (yoneda.map f ≫ g) = (functorInclusion S ≫ g).app Y.op { val := f, property := hf }
case mp
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v₁
g : yoneda.obj X ⟶ P
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ P.map f.op (↑yonedaEquiv g) = (functorInclusion S ≫ g).app Y.op { val := f, property := hf }
rw [yonedaEquiv_naturality]
case mp
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v₁
g : yoneda.obj X ⟶ P
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ g.app Y.op (𝟙 Y ≫ f) = g.app Y.op f
case mp
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v₁
g : yoneda.obj X ⟶ P
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ↑yonedaEquiv (yoneda.map f ≫ g) = (functorInclusion S ≫ g).app Y.op { val := f, property := hf }
dsimp
no goals
case mp
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v₁
g : yoneda.obj X ⟶ P
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ g.app Y.op (𝟙 Y ≫ f) = g.app Y.op f
simp
case mpr
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v₁
x : functor S ⟶ P
g : yoneda.obj X ⟶ P
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (↑yonedaEquiv g) = x.app Y.op { val := f, property := h }
⊢ functorInclusion S ≫ g = x
case mpr
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v₁
x : functor S ⟶ P
g : yoneda.obj X ⟶ P
⊢ (∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (↑yonedaEquiv g) = x.app Y.op { val := f, property := h }) →
    functorInclusion S ≫ g = x
intro h
case mpr.w.h.h.mk
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v₁
x : functor S ⟶ P
g : yoneda.obj X ⟶ P
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (↑yonedaEquiv g) = x.app Y.op { val := f, property := h }
Y : Cᵒᵖ
f : Y.unop ⟶ X
hf : S.arrows f
⊢ (functorInclusion S ≫ g).app Y { val := f, property := hf } = x.app Y { val := f, property := hf }
case mpr
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v₁
x : functor S ⟶ P
g : yoneda.obj X ⟶ P
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (↑yonedaEquiv g) = x.app Y.op { val := f, property := h }
⊢ functorInclusion S ≫ g = x
ext Y ⟨f, hf⟩
case h.e'_2.h
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v₁
x : functor S ⟶ P
g : yoneda.obj X ⟶ P
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (↑yonedaEquiv g) = x.app Y.op { val := f, property := h }
Y : Cᵒᵖ
f : Y.unop ⟶ X
hf : S.arrows f
e_1✝ : P.obj Y = P.obj Y.unop.op
⊢ (functorInclusion S ≫ g).app Y { val := f, property := hf } = P.map f.op (↑yonedaEquiv g)
case mpr.w.h.h.mk
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v₁
x : functor S ⟶ P
g : yoneda.obj X ⟶ P
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (↑yonedaEquiv g) = x.app Y.op { val := f, property := h }
Y : Cᵒᵖ
f : Y.unop ⟶ X
hf : S.arrows f
⊢ (functorInclusion S ≫ g).app Y { val := f, property := hf } = x.app Y { val := f, property := hf }
convert h f hf
case h.e'_2.h
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v₁
x : functor S ⟶ P
g : yoneda.obj X ⟶ P
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (↑yonedaEquiv g) = x.app Y.op { val := f, property := h }
Y : Cᵒᵖ
f : Y.unop ⟶ X
hf : S.arrows f
e_1✝ : P.obj Y = P.obj Y.unop.op
⊢ (functorInclusion S ≫ g).app Y { val := f, property := hf } = ↑yonedaEquiv (yoneda.map f ≫ g)
case h.e'_2.h
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v₁
x : functor S ⟶ P
g : yoneda.obj X ⟶ P
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (↑yonedaEquiv g) = x.app Y.op { val := f, property := h }
Y : Cᵒᵖ
f : Y.unop ⟶ X
hf : S.arrows f
e_1✝ : P.obj Y = P.obj Y.unop.op
⊢ (functorInclusion S ≫ g).app Y { val := f, property := hf } = P.map f.op (↑yonedaEquiv g)
rw [yonedaEquiv_naturality]
no goals
case h.e'_2.h
C : Type u₁
inst✝ : Category C
P✝ Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type v₁
x : functor S ⟶ P
g : yoneda.obj X ⟶ P
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S.arrows f), P.map f.op (↑yonedaEquiv g) = x.app Y.op { val := f, property := h }
Y : Cᵒᵖ
f : Y.unop ⟶ X
hf : S.arrows f
e_1✝ : P.obj Y = P.obj Y.unop.op
⊢ (functorInclusion S ≫ g).app Y { val := f, property := hf } = ↑yonedaEquiv (yoneda.map f ≫ g)
simp [yonedaEquiv]