[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
U✝ : C
S✝ : Sieve U✝
hS : S✝ ∈ GrothendieckTopology.sieves J U✝
⊢ Sieve.functorPushforward (𝟭 C) S✝ ∈ GrothendieckTopology.sieves J ((𝟭 C).obj U✝)
[PROOFSTEP]
simpa using hS
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
F : C ⥤ D
hF : CoverPreserving J K F
G : D ⥤ A
hG : CoverPreserving K L G
U✝ : C
S✝ : Sieve U✝
hS : S✝ ∈ GrothendieckTopology.sieves J U✝
⊢ Sieve.functorPushforward (F ⋙ G) S✝ ∈ GrothendieckTopology.sieves L ((F ⋙ G).obj U✝)
[PROOFSTEP]
rw [Sieve.functorPushforward_comp]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
F : C ⥤ D
hF : CoverPreserving J K F
G : D ⥤ A
hG : CoverPreserving K L G
U✝ : C
S✝ : Sieve U✝
hS : S✝ ∈ GrothendieckTopology.sieves J U✝
⊢ Sieve.functorPushforward G (Sieve.functorPushforward F S✝) ∈ GrothendieckTopology.sieves L ((F ⋙ G).obj U✝)
[PROOFSTEP]
exact hG.cover_preserve (hF.cover_preserve hS)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
h : Compatible x
⊢ Compatible (FamilyOfElements.functorPushforward G x)
[PROOFSTEP]
rintro Z₁ Z₂ W g₁ g₂ f₁' f₂' H₁ H₂ eq
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
h : Compatible x
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁' : Z₁ ⟶ G.obj Z
f₂' : Z₂ ⟶ G.obj Z
H₁ : Presieve.functorPushforward G T f₁'
H₂ : Presieve.functorPushforward G T f₂'
eq : g₁ ≫ f₁' = g₂ ≫ f₂'
⊢ ℱ.val.map g₁.op (FamilyOfElements.functorPushforward G x f₁' H₁) =
    ℱ.val.map g₂.op (FamilyOfElements.functorPushforward G x f₂' H₂)
[PROOFSTEP]
unfold FamilyOfElements.functorPushforward
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
h : Compatible x
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁' : Z₁ ⟶ G.obj Z
f₂' : Z₂ ⟶ G.obj Z
H₁ : Presieve.functorPushforward G T f₁'
H₂ : Presieve.functorPushforward G T f₂'
eq : g₁ ≫ f₁' = g₂ ≫ f₂'
⊢ ℱ.val.map g₁.op
      (FunctorPushforwardStructure.casesOn (getFunctorPushforwardStructure H₁) fun Z_1 g h h₁ fac =>
        ℱ.val.map h.op (x g h₁)) =
    ℱ.val.map g₂.op
      (FunctorPushforwardStructure.casesOn (getFunctorPushforwardStructure H₂) fun Z_1 g h h₁ fac =>
        ℱ.val.map h.op (x g h₁))
[PROOFSTEP]
rcases getFunctorPushforwardStructure H₁ with ⟨X₁, f₁, h₁, hf₁, rfl⟩
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
h : Compatible x
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₂' : Z₂ ⟶ G.obj Z
H₂ : Presieve.functorPushforward G T f₂'
X₁ : C
f₁ : X₁ ⟶ Z
h₁ : Z₁ ⟶ G.obj X₁
hf₁ : T f₁
H₁ : Presieve.functorPushforward G T (h₁ ≫ G.map f₁)
eq : g₁ ≫ h₁ ≫ G.map f₁ = g₂ ≫ f₂'
⊢ ℱ.val.map g₁.op
      (FunctorPushforwardStructure.casesOn
        { preobj := X₁, premap := f₁, lift := h₁, cover := hf₁, fac := (_ : h₁ ≫ G.map f₁ = h₁ ≫ G.map f₁) }
        fun Z_1 g h h₁_1 fac => ℱ.val.map h.op (x g h₁_1)) =
    ℱ.val.map g₂.op
      (FunctorPushforwardStructure.casesOn (getFunctorPushforwardStructure H₂) fun Z_1 g h h₁ fac =>
        ℱ.val.map h.op (x g h₁))
[PROOFSTEP]
rcases getFunctorPushforwardStructure H₂ with ⟨X₂, f₂, h₂, hf₂, rfl⟩
[GOAL]
case mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
h : Compatible x
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
X₁ : C
f₁ : X₁ ⟶ Z
h₁ : Z₁ ⟶ G.obj X₁
hf₁ : T f₁
H₁ : Presieve.functorPushforward G T (h₁ ≫ G.map f₁)
X₂ : C
f₂ : X₂ ⟶ Z
h₂ : Z₂ ⟶ G.obj X₂
hf₂ : T f₂
H₂ : Presieve.functorPushforward G T (h₂ ≫ G.map f₂)
eq : g₁ ≫ h₁ ≫ G.map f₁ = g₂ ≫ h₂ ≫ G.map f₂
⊢ ℱ.val.map g₁.op
      (FunctorPushforwardStructure.casesOn
        { preobj := X₁, premap := f₁, lift := h₁, cover := hf₁, fac := (_ : h₁ ≫ G.map f₁ = h₁ ≫ G.map f₁) }
        fun Z_1 g h h₁_1 fac => ℱ.val.map h.op (x g h₁_1)) =
    ℱ.val.map g₂.op
      (FunctorPushforwardStructure.casesOn
        { preobj := X₂, premap := f₂, lift := h₂, cover := hf₂, fac := (_ : h₂ ≫ G.map f₂ = h₂ ≫ G.map f₂) }
        fun Z_1 g h h₁ fac => ℱ.val.map h.op (x g h₁))
[PROOFSTEP]
suffices ℱ.val.map (g₁ ≫ h₁).op (x f₁ hf₁) = ℱ.val.map (g₂ ≫ h₂).op (x f₂ hf₂) by simpa using this
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
h : Compatible x
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
X₁ : C
f₁ : X₁ ⟶ Z
h₁ : Z₁ ⟶ G.obj X₁
hf₁ : T f₁
H₁ : Presieve.functorPushforward G T (h₁ ≫ G.map f₁)
X₂ : C
f₂ : X₂ ⟶ Z
h₂ : Z₂ ⟶ G.obj X₂
hf₂ : T f₂
H₂ : Presieve.functorPushforward G T (h₂ ≫ G.map f₂)
eq : g₁ ≫ h₁ ≫ G.map f₁ = g₂ ≫ h₂ ≫ G.map f₂
this : ℱ.val.map (g₁ ≫ h₁).op (x f₁ hf₁) = ℱ.val.map (g₂ ≫ h₂).op (x f₂ hf₂)
⊢ ℱ.val.map g₁.op
      (FunctorPushforwardStructure.casesOn
        { preobj := X₁, premap := f₁, lift := h₁, cover := hf₁, fac := (_ : h₁ ≫ G.map f₁ = h₁ ≫ G.map f₁) }
        fun Z_1 g h h₁_1 fac => ℱ.val.map h.op (x g h₁_1)) =
    ℱ.val.map g₂.op
      (FunctorPushforwardStructure.casesOn
        { preobj := X₂, premap := f₂, lift := h₂, cover := hf₂, fac := (_ : h₂ ≫ G.map f₂ = h₂ ≫ G.map f₂) }
        fun Z_1 g h h₁ fac => ℱ.val.map h.op (x g h₁))
[PROOFSTEP]
simpa using this
[GOAL]
case mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
h : Compatible x
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
X₁ : C
f₁ : X₁ ⟶ Z
h₁ : Z₁ ⟶ G.obj X₁
hf₁ : T f₁
H₁ : Presieve.functorPushforward G T (h₁ ≫ G.map f₁)
X₂ : C
f₂ : X₂ ⟶ Z
h₂ : Z₂ ⟶ G.obj X₂
hf₂ : T f₂
H₂ : Presieve.functorPushforward G T (h₂ ≫ G.map f₂)
eq : g₁ ≫ h₁ ≫ G.map f₁ = g₂ ≫ h₂ ≫ G.map f₂
⊢ ℱ.val.map (g₁ ≫ h₁).op (x f₁ hf₁) = ℱ.val.map (g₂ ≫ h₂).op (x f₂ hf₂)
[PROOFSTEP]
apply hG.Compatible ℱ h _ _ hf₁ hf₂
[GOAL]
case mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
h : Compatible x
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
X₁ : C
f₁ : X₁ ⟶ Z
h₁ : Z₁ ⟶ G.obj X₁
hf₁ : T f₁
H₁ : Presieve.functorPushforward G T (h₁ ≫ G.map f₁)
X₂ : C
f₂ : X₂ ⟶ Z
h₂ : Z₂ ⟶ G.obj X₂
hf₂ : T f₂
H₂ : Presieve.functorPushforward G T (h₂ ≫ G.map f₂)
eq : g₁ ≫ h₁ ≫ G.map f₁ = g₂ ≫ h₂ ≫ G.map f₂
⊢ (g₁ ≫ h₁) ≫ G.map f₁ = (g₂ ≫ h₂) ≫ G.map f₂
[PROOFSTEP]
simpa using eq
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
h : FamilyOfElements.Compatible x
Y : C
f : Y ⟶ Z
hf : T f
⊢ FamilyOfElements.functorPushforward G x (G.map f) (_ : Presieve.functorPushforward G T (G.map f)) = x f hf
[PROOFSTEP]
unfold FamilyOfElements.functorPushforward
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
h : FamilyOfElements.Compatible x
Y : C
f : Y ⟶ Z
hf : T f
⊢ (FunctorPushforwardStructure.casesOn (getFunctorPushforwardStructure (_ : Presieve.functorPushforward G T (G.map f)))
      fun Z_1 g h h₁ fac => ℱ.val.map h.op (x g h₁)) =
    x f hf
[PROOFSTEP]
rcases e₁ : getFunctorPushforwardStructure (image_mem_functorPushforward G T hf) with ⟨X, g, f', hg, eq⟩
[GOAL]
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
h : FamilyOfElements.Compatible x
Y : C
f : Y ⟶ Z
hf : T f
X : C
g : X ⟶ Z
f' : G.obj Y ⟶ G.obj X
hg : T g
eq : G.map f = f' ≫ G.map g
e₁ :
  getFunctorPushforwardStructure (_ : Presieve.functorPushforward G T (G.map f)) =
    { preobj := X, premap := g, lift := f', cover := hg, fac := eq }
⊢ (FunctorPushforwardStructure.casesOn { preobj := X, premap := g, lift := f', cover := hg, fac := eq }
      fun Z_1 g h h₁ fac => ℱ.val.map h.op (x g h₁)) =
    x f hf
[PROOFSTEP]
simpa using hG.Compatible ℱ h f' (𝟙 _) hg hf (by simp [eq])
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
h : FamilyOfElements.Compatible x
Y : C
f : Y ⟶ Z
hf : T f
X : C
g : X ⟶ Z
f' : G.obj Y ⟶ G.obj X
hg : T g
eq : G.map f = f' ≫ G.map g
e₁ :
  getFunctorPushforwardStructure (_ : Presieve.functorPushforward G T (G.map f)) =
    { preobj := X, premap := g, lift := f', cover := hg, fac := eq }
⊢ f' ≫ G.map g = 𝟙 (G.obj Y) ≫ G.map f
[PROOFSTEP]
simp [eq]
[GOAL]
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ : SheafOfTypes K✝
Z : C✝
T : Presieve Z
x : FamilyOfElements (G✝.op ⋙ ℱ.val) T
h : Compatible x
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
⊢ CompatiblePreserving K G
[PROOFSTEP]
constructor
[GOAL]
case Compatible
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ : SheafOfTypes K✝
Z : C✝
T : Presieve Z
x : FamilyOfElements (G✝.op ⋙ ℱ.val) T
h : Compatible x
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
⊢ ∀ (ℱ : SheafOfTypes K) {Z : C} {T : Presieve Z} {x : FamilyOfElements (G.op ⋙ ℱ.val) T},
    Compatible x →
      ∀ {Y₁ Y₂ : C} {X : D} (f₁ : X ⟶ G.obj Y₁) (f₂ : X ⟶ G.obj Y₂) {g₁ : Y₁ ⟶ Z} {g₂ : Y₂ ⟶ Z} (hg₁ : T g₁)
        (hg₂ : T g₂), f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂ → ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)
[PROOFSTEP]
intro ℱ Z T x hx Y₁ Y₂ X f₁ f₂ g₁ g₂ hg₁ hg₂ e
[GOAL]
case Compatible
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
⊢ ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)
[PROOFSTEP]
let c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj
    (PullbackCone.mk f₁ f₂ e)
      /-
          This can then be viewed as a cospan of structured arrows, and we may obtain an arbitrary cone
          over it since `StructuredArrow W u` is cofiltered.
          Then, it suffices to prove that it is compatible when restricted onto `u(c'.X.right)`.
          -/
[GOAL]
case Compatible
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
⊢ ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)
[PROOFSTEP]
let c' := IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre _ _ _)
[GOAL]
case Compatible
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
⊢ ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)
[PROOFSTEP]
have eq₁ : f₁ = (c'.pt.hom ≫ G.map (c'.π.app left).right) ≫ eqToHom (by simp) :=
  by
  erw [← (c'.π.app left).w]
  dsimp
  simp
[GOAL]
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
⊢ G.obj ((Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).obj left).right = G.obj Y₁
[PROOFSTEP]
simp
[GOAL]
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
⊢ f₁ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π left).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₁ ≫ 𝟙 (G.obj Y₁)))).right =
            G.obj Y₁)
[PROOFSTEP]
erw [← (c'.π.app left).w]
[GOAL]
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
⊢ f₁ =
    ((Functor.fromPUnit c.pt).map (NatTrans.app c'.π left).left ≫
        ((Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).obj left).hom) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₁ ≫ 𝟙 (G.obj Y₁)))).right =
            G.obj Y₁)
[PROOFSTEP]
dsimp
[GOAL]
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
⊢ f₁ = (𝟙 X ≫ f₁ ≫ 𝟙 (G.obj Y₁)) ≫ 𝟙 (G.obj Y₁)
[PROOFSTEP]
simp
[GOAL]
case Compatible
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ :
  f₁ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π left).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₁ ≫ 𝟙 (G.obj Y₁)))).right =
            G.obj Y₁)
⊢ ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)
[PROOFSTEP]
have eq₂ : f₂ = (c'.pt.hom ≫ G.map (c'.π.app right).right) ≫ eqToHom (by simp) :=
  by
  erw [← (c'.π.app right).w]
  dsimp
  simp
[GOAL]
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ :
  f₁ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π left).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₁ ≫ 𝟙 (G.obj Y₁)))).right =
            G.obj Y₁)
⊢ G.obj ((Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).obj right).right = G.obj Y₂
[PROOFSTEP]
simp
[GOAL]
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ :
  f₁ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π left).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₁ ≫ 𝟙 (G.obj Y₁)))).right =
            G.obj Y₁)
⊢ f₂ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π right).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₂ ≫ 𝟙 (G.obj Y₂)))).right =
            G.obj Y₂)
[PROOFSTEP]
erw [← (c'.π.app right).w]
[GOAL]
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ :
  f₁ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π left).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₁ ≫ 𝟙 (G.obj Y₁)))).right =
            G.obj Y₁)
⊢ f₂ =
    ((Functor.fromPUnit c.pt).map (NatTrans.app c'.π right).left ≫
        ((Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).obj right).hom) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₂ ≫ 𝟙 (G.obj Y₂)))).right =
            G.obj Y₂)
[PROOFSTEP]
dsimp
[GOAL]
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ :
  f₁ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π left).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₁ ≫ 𝟙 (G.obj Y₁)))).right =
            G.obj Y₁)
⊢ f₂ = (𝟙 X ≫ f₂ ≫ 𝟙 (G.obj Y₂)) ≫ 𝟙 (G.obj Y₂)
[PROOFSTEP]
simp
[GOAL]
case Compatible
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ :
  f₁ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π left).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₁ ≫ 𝟙 (G.obj Y₁)))).right =
            G.obj Y₁)
eq₂ :
  f₂ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π right).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₂ ≫ 𝟙 (G.obj Y₂)))).right =
            G.obj Y₂)
⊢ ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)
[PROOFSTEP]
conv_lhs => rw [eq₁]
[GOAL]
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ :
  f₁ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π left).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₁ ≫ 𝟙 (G.obj Y₁)))).right =
            G.obj Y₁)
eq₂ :
  f₂ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π right).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₂ ≫ 𝟙 (G.obj Y₂)))).right =
            G.obj Y₂)
| ℱ.val.map f₁.op (x g₁ hg₁)
[PROOFSTEP]
rw [eq₁]
[GOAL]
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ :
  f₁ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π left).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₁ ≫ 𝟙 (G.obj Y₁)))).right =
            G.obj Y₁)
eq₂ :
  f₂ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π right).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₂ ≫ 𝟙 (G.obj Y₂)))).right =
            G.obj Y₂)
| ℱ.val.map f₁.op (x g₁ hg₁)
[PROOFSTEP]
rw [eq₁]
[GOAL]
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ :
  f₁ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π left).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₁ ≫ 𝟙 (G.obj Y₁)))).right =
            G.obj Y₁)
eq₂ :
  f₂ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π right).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₂ ≫ 𝟙 (G.obj Y₂)))).right =
            G.obj Y₂)
| ℱ.val.map f₁.op (x g₁ hg₁)
[PROOFSTEP]
rw [eq₁]
[GOAL]
case Compatible
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ :
  f₁ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π left).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₁ ≫ 𝟙 (G.obj Y₁)))).right =
            G.obj Y₁)
eq₂ :
  f₂ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π right).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₂ ≫ 𝟙 (G.obj Y₂)))).right =
            G.obj Y₂)
⊢ ℱ.val.map
      ((c'.pt.hom ≫ G.map (NatTrans.app c'.π left).right) ≫
          eqToHom
            (_ :
              G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₁ ≫ 𝟙 (G.obj Y₁)))).right =
                G.obj Y₁)).op
      (x g₁ hg₁) =
    ℱ.val.map f₂.op (x g₂ hg₂)
[PROOFSTEP]
conv_rhs => rw [eq₂]
[GOAL]
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ :
  f₁ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π left).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₁ ≫ 𝟙 (G.obj Y₁)))).right =
            G.obj Y₁)
eq₂ :
  f₂ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π right).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₂ ≫ 𝟙 (G.obj Y₂)))).right =
            G.obj Y₂)
| ℱ.val.map f₂.op (x g₂ hg₂)
[PROOFSTEP]
rw [eq₂]
[GOAL]
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ :
  f₁ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π left).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₁ ≫ 𝟙 (G.obj Y₁)))).right =
            G.obj Y₁)
eq₂ :
  f₂ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π right).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₂ ≫ 𝟙 (G.obj Y₂)))).right =
            G.obj Y₂)
| ℱ.val.map f₂.op (x g₂ hg₂)
[PROOFSTEP]
rw [eq₂]
[GOAL]
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ :
  f₁ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π left).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₁ ≫ 𝟙 (G.obj Y₁)))).right =
            G.obj Y₁)
eq₂ :
  f₂ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π right).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₂ ≫ 𝟙 (G.obj Y₂)))).right =
            G.obj Y₂)
| ℱ.val.map f₂.op (x g₂ hg₂)
[PROOFSTEP]
rw [eq₂]
[GOAL]
case Compatible
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ :
  f₁ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π left).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₁ ≫ 𝟙 (G.obj Y₁)))).right =
            G.obj Y₁)
eq₂ :
  f₂ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π right).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₂ ≫ 𝟙 (G.obj Y₂)))).right =
            G.obj Y₂)
⊢ ℱ.val.map
      ((c'.pt.hom ≫ G.map (NatTrans.app c'.π left).right) ≫
          eqToHom
            (_ :
              G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₁ ≫ 𝟙 (G.obj Y₁)))).right =
                G.obj Y₁)).op
      (x g₁ hg₁) =
    ℱ.val.map
      ((c'.pt.hom ≫ G.map (NatTrans.app c'.π right).right) ≫
          eqToHom
            (_ :
              G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₂ ≫ 𝟙 (G.obj Y₂)))).right =
                G.obj Y₂)).op
      (x g₂ hg₂)
[PROOFSTEP]
simp only [op_comp, Functor.map_comp, types_comp_apply, eqToHom_op, eqToHom_map]
[GOAL]
case Compatible
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ :
  f₁ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π left).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₁ ≫ 𝟙 (G.obj Y₁)))).right =
            G.obj Y₁)
eq₂ :
  f₂ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π right).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₂ ≫ 𝟙 (G.obj Y₂)))).right =
            G.obj Y₂)
⊢ ℱ.val.map
      (IsCofiltered.cone
              (Cone.toStructuredArrow
                  ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)) ⋙
                StructuredArrow.pre
                  ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)).pt
                  (cospan g₁ g₂) G)).pt.hom.op
      (ℱ.val.map
        (G.map
            (NatTrans.app
                (IsCofiltered.cone
                    (Cone.toStructuredArrow
                        ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)) ⋙
                      StructuredArrow.pre
                        ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)).pt
                        (cospan g₁ g₂) G)).π
                left).right).op
        (eqToHom
          (_ :
            ℱ.val.obj (op (G.obj Y₁)) =
              ℱ.val.obj
                (op
                  (G.obj
                    ((Cone.toStructuredArrow
                              ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj
                                (PullbackCone.mk f₁ f₂ e)) ⋙
                            StructuredArrow.pre
                              ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj
                                  (PullbackCone.mk f₁ f₂ e)).pt
                              (cospan g₁ g₂) G).obj
                        left).right)))
          (x g₁ hg₁))) =
    ℱ.val.map
      (IsCofiltered.cone
              (Cone.toStructuredArrow
                  ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)) ⋙
                StructuredArrow.pre
                  ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)).pt
                  (cospan g₁ g₂) G)).pt.hom.op
      (ℱ.val.map
        (G.map
            (NatTrans.app
                (IsCofiltered.cone
                    (Cone.toStructuredArrow
                        ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)) ⋙
                      StructuredArrow.pre
                        ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)).pt
                        (cospan g₁ g₂) G)).π
                right).right).op
        (eqToHom
          (_ :
            ℱ.val.obj (op (G.obj Y₂)) =
              ℱ.val.obj
                (op
                  (G.obj
                    ((Cone.toStructuredArrow
                              ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj
                                (PullbackCone.mk f₁ f₂ e)) ⋙
                            StructuredArrow.pre
                              ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj
                                  (PullbackCone.mk f₁ f₂ e)).pt
                              (cospan g₁ g₂) G).obj
                        right).right)))
          (x g₂ hg₂)))
[PROOFSTEP]
apply congr_arg
[GOAL]
case Compatible.h
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ :
  f₁ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π left).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₁ ≫ 𝟙 (G.obj Y₁)))).right =
            G.obj Y₁)
eq₂ :
  f₂ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π right).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₂ ≫ 𝟙 (G.obj Y₂)))).right =
            G.obj Y₂)
⊢ ℱ.val.map
      (G.map
          (NatTrans.app
              (IsCofiltered.cone
                  (Cone.toStructuredArrow
                      ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)) ⋙
                    StructuredArrow.pre
                      ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)).pt
                      (cospan g₁ g₂) G)).π
              left).right).op
      (eqToHom
        (_ :
          ℱ.val.obj (op (G.obj Y₁)) =
            ℱ.val.obj
              (op
                (G.obj
                  ((Cone.toStructuredArrow
                            ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj
                              (PullbackCone.mk f₁ f₂ e)) ⋙
                          StructuredArrow.pre
                            ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj
                                (PullbackCone.mk f₁ f₂ e)).pt
                            (cospan g₁ g₂) G).obj
                      left).right)))
        (x g₁ hg₁)) =
    ℱ.val.map
      (G.map
          (NatTrans.app
              (IsCofiltered.cone
                  (Cone.toStructuredArrow
                      ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)) ⋙
                    StructuredArrow.pre
                      ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)).pt
                      (cospan g₁ g₂) G)).π
              right).right).op
      (eqToHom
        (_ :
          ℱ.val.obj (op (G.obj Y₂)) =
            ℱ.val.obj
              (op
                (G.obj
                  ((Cone.toStructuredArrow
                            ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj
                              (PullbackCone.mk f₁ f₂ e)) ⋙
                          StructuredArrow.pre
                            ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj
                                (PullbackCone.mk f₁ f₂ e)).pt
                            (cospan g₁ g₂) G).obj
                      right).right)))
        (x g₂ hg₂))
[PROOFSTEP]
injection c'.π.naturality WalkingCospan.Hom.inl with _ e₁
[GOAL]
case Compatible.h
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ :
  f₁ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π left).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₁ ≫ 𝟙 (G.obj Y₁)))).right =
            G.obj Y₁)
eq₂ :
  f₂ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π right).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₂ ≫ 𝟙 (G.obj Y₂)))).right =
            G.obj Y₂)
left_eq✝ :
  (((Functor.const WalkingCospan).obj c'.pt).map Hom.inl).left ≫ (NatTrans.app c'.π one).left =
    (NatTrans.app c'.π left).left ≫
      ((Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).map Hom.inl).left
e₁ :
  (((Functor.const WalkingCospan).obj c'.pt).map Hom.inl).right ≫ (NatTrans.app c'.π one).right =
    (NatTrans.app c'.π left).right ≫
      ((Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).map Hom.inl).right
⊢ ℱ.val.map
      (G.map
          (NatTrans.app
              (IsCofiltered.cone
                  (Cone.toStructuredArrow
                      ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)) ⋙
                    StructuredArrow.pre
                      ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)).pt
                      (cospan g₁ g₂) G)).π
              left).right).op
      (eqToHom
        (_ :
          ℱ.val.obj (op (G.obj Y₁)) =
            ℱ.val.obj
              (op
                (G.obj
                  ((Cone.toStructuredArrow
                            ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj
                              (PullbackCone.mk f₁ f₂ e)) ⋙
                          StructuredArrow.pre
                            ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj
                                (PullbackCone.mk f₁ f₂ e)).pt
                            (cospan g₁ g₂) G).obj
                      left).right)))
        (x g₁ hg₁)) =
    ℱ.val.map
      (G.map
          (NatTrans.app
              (IsCofiltered.cone
                  (Cone.toStructuredArrow
                      ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)) ⋙
                    StructuredArrow.pre
                      ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)).pt
                      (cospan g₁ g₂) G)).π
              right).right).op
      (eqToHom
        (_ :
          ℱ.val.obj (op (G.obj Y₂)) =
            ℱ.val.obj
              (op
                (G.obj
                  ((Cone.toStructuredArrow
                            ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj
                              (PullbackCone.mk f₁ f₂ e)) ⋙
                          StructuredArrow.pre
                            ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj
                                (PullbackCone.mk f₁ f₂ e)).pt
                            (cospan g₁ g₂) G).obj
                      right).right)))
        (x g₂ hg₂))
[PROOFSTEP]
injection c'.π.naturality WalkingCospan.Hom.inr with _ e₂
[GOAL]
case Compatible.h
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
J : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
L : GrothendieckTopology A
G✝ : C✝ ⥤ D✝
hG : CompatiblePreserving K✝ G✝
ℱ✝ : SheafOfTypes K✝
Z✝ : C✝
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ :
  f₁ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π left).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₁ ≫ 𝟙 (G.obj Y₁)))).right =
            G.obj Y₁)
eq₂ :
  f₂ =
    (c'.pt.hom ≫ G.map (NatTrans.app c'.π right).right) ≫
      eqToHom
        (_ :
          G.obj ((StructuredArrow.pre X (cospan g₁ g₂) G).obj (StructuredArrow.mk (f₂ ≫ 𝟙 (G.obj Y₂)))).right =
            G.obj Y₂)
left_eq✝¹ :
  (((Functor.const WalkingCospan).obj c'.pt).map Hom.inl).left ≫ (NatTrans.app c'.π one).left =
    (NatTrans.app c'.π left).left ≫
      ((Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).map Hom.inl).left
e₁ :
  (((Functor.const WalkingCospan).obj c'.pt).map Hom.inl).right ≫ (NatTrans.app c'.π one).right =
    (NatTrans.app c'.π left).right ≫
      ((Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).map Hom.inl).right
left_eq✝ :
  (((Functor.const WalkingCospan).obj c'.pt).map Hom.inr).left ≫ (NatTrans.app c'.π one).left =
    (NatTrans.app c'.π right).left ≫
      ((Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).map Hom.inr).left
e₂ :
  (((Functor.const WalkingCospan).obj c'.pt).map Hom.inr).right ≫ (NatTrans.app c'.π one).right =
    (NatTrans.app c'.π right).right ≫
      ((Cone.toStructuredArrow c ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).map Hom.inr).right
⊢ ℱ.val.map
      (G.map
          (NatTrans.app
              (IsCofiltered.cone
                  (Cone.toStructuredArrow
                      ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)) ⋙
                    StructuredArrow.pre
                      ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)).pt
                      (cospan g₁ g₂) G)).π
              left).right).op
      (eqToHom
        (_ :
          ℱ.val.obj (op (G.obj Y₁)) =
            ℱ.val.obj
              (op
                (G.obj
                  ((Cone.toStructuredArrow
                            ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj
                              (PullbackCone.mk f₁ f₂ e)) ⋙
                          StructuredArrow.pre
                            ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj
                                (PullbackCone.mk f₁ f₂ e)).pt
                            (cospan g₁ g₂) G).obj
                      left).right)))
        (x g₁ hg₁)) =
    ℱ.val.map
      (G.map
          (NatTrans.app
              (IsCofiltered.cone
                  (Cone.toStructuredArrow
                      ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)) ⋙
                    StructuredArrow.pre
                      ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)).pt
                      (cospan g₁ g₂) G)).π
              right).right).op
      (eqToHom
        (_ :
          ℱ.val.obj (op (G.obj Y₂)) =
            ℱ.val.obj
              (op
                (G.obj
                  ((Cone.toStructuredArrow
                            ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj
                              (PullbackCone.mk f₁ f₂ e)) ⋙
                          StructuredArrow.pre
                            ((Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj
                                (PullbackCone.mk f₁ f₂ e)).pt
                            (cospan g₁ g₂) G).obj
                      right).right)))
        (x g₂ hg₂))
[PROOFSTEP]
exact hx (c'.π.app left).right (c'.π.app right).right hg₁ hg₂ (e₁.symm.trans e₂)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
A : Type u₃
inst✝² : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
h : Compatible x
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
⊢ CompatiblePreserving K F
[PROOFSTEP]
constructor
[GOAL]
case Compatible
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
A : Type u₃
inst✝² : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
h : Compatible x
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
⊢ ∀ (ℱ : SheafOfTypes K) {Z : C} {T : Presieve Z} {x : FamilyOfElements (F.op ⋙ ℱ.val) T},
    Compatible x →
      ∀ {Y₁ Y₂ : C} {X : D} (f₁ : X ⟶ F.obj Y₁) (f₂ : X ⟶ F.obj Y₂) {g₁ : Y₁ ⟶ Z} {g₂ : Y₂ ⟶ Z} (hg₁ : T g₁)
        (hg₂ : T g₂), f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂ → ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)
[PROOFSTEP]
introv hx he
[GOAL]
case Compatible
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
A : Type u₃
inst✝² : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ✝ : SheafOfTypes K
Z✝ : C
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (F.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ F.obj Y₁
f₂ : X ⟶ F.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂
⊢ ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)
[PROOFSTEP]
obtain ⟨X', e⟩ := hF f₁
[GOAL]
case Compatible.mk
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
A : Type u₃
inst✝² : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ✝ : SheafOfTypes K
Z✝ : C
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (F.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ F.obj Y₁
f₂ : X ⟶ F.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂
X' : C
e : F.obj X' ≅ X
⊢ ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)
[PROOFSTEP]
apply (ℱ.1.mapIso e.op).toEquiv.injective
[GOAL]
case Compatible.mk.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
A : Type u₃
inst✝² : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ✝ : SheafOfTypes K
Z✝ : C
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (F.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ F.obj Y₁
f₂ : X ⟶ F.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂
X' : C
e : F.obj X' ≅ X
⊢ ↑(ℱ.val.mapIso (Iso.op e)).toEquiv (ℱ.val.map f₁.op (x g₁ hg₁)) =
    ↑(ℱ.val.mapIso (Iso.op e)).toEquiv (ℱ.val.map f₂.op (x g₂ hg₂))
[PROOFSTEP]
simp only [Iso.op_hom, Iso.toEquiv_fun, ℱ.1.mapIso_hom, ← FunctorToTypes.map_comp_apply]
[GOAL]
case Compatible.mk.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
A : Type u₃
inst✝² : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ✝ : SheafOfTypes K
Z✝ : C
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (F.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ F.obj Y₁
f₂ : X ⟶ F.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂
X' : C
e : F.obj X' ≅ X
⊢ ℱ.val.map (f₁.op ≫ e.hom.op) (x g₁ hg₁) = ℱ.val.map (f₂.op ≫ e.hom.op) (x g₂ hg₂)
[PROOFSTEP]
simpa using hx (F.preimage <| e.hom ≫ f₁) (F.preimage <| e.hom ≫ f₂) hg₁ hg₂ (F.map_injective <| by simpa using he)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
A : Type u₃
inst✝² : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ✝ : SheafOfTypes K
Z✝ : C
T✝ : Presieve Z✝
x✝ : FamilyOfElements (G.op ⋙ ℱ✝.val) T✝
h : Compatible x✝
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (F.op ⋙ ℱ.val) T
hx : Compatible x
Y₁ Y₂ : C
X : D
f₁ : X ⟶ F.obj Y₁
f₂ : X ⟶ F.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂
X' : C
e : F.obj X' ≅ X
⊢ F.map (F.preimage (e.hom ≫ f₁) ≫ g₁) = F.map (F.preimage (e.hom ≫ f₂) ≫ g₂)
[PROOFSTEP]
simpa using he
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G✝ : C ⥤ D
hG : CompatiblePreserving K G✝
ℱ✝ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T
h : Compatible x
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
⊢ Presheaf.IsSheaf J (G.op ⋙ ℱ.val)
[PROOFSTEP]
intro X U S hS x hx
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G✝ : C ⥤ D
hG : CompatiblePreserving K G✝
ℱ✝ : SheafOfTypes K
Z : C
T : Presieve Z
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T
h : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements ((G.op ⋙ ℱ.val) ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
⊢ ∃! t, IsAmalgamation x t
[PROOFSTEP]
change FamilyOfElements (G.op ⋙ ℱ.val ⋙ coyoneda.obj (op X)) _ at x 
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G✝ : C ⥤ D
hG : CompatiblePreserving K G✝
ℱ✝ : SheafOfTypes K
Z : C
T : Presieve Z
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T
h : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (G.op ⋙ ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
⊢ ∃! t, IsAmalgamation x t
[PROOFSTEP]
let H := ℱ.2 X _ (hG₂.cover_preserve hS)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G✝ : C ⥤ D
hG : CompatiblePreserving K G✝
ℱ✝ : SheafOfTypes K
Z : C
T : Presieve Z
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T
h : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (G.op ⋙ ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj (op X)) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
⊢ ∃! t, IsAmalgamation x t
[PROOFSTEP]
let hx' := hx.functorPushforward hG₁ (sheafOver ℱ X)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G✝ : C ⥤ D
hG : CompatiblePreserving K G✝
ℱ✝ : SheafOfTypes K
Z : C
T : Presieve Z
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T
h : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (G.op ⋙ ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj (op X)) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
⊢ ∃! t, IsAmalgamation x t
[PROOFSTEP]
constructor
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G✝ : C ⥤ D
hG : CompatiblePreserving K G✝
ℱ✝ : SheafOfTypes K
Z : C
T : Presieve Z
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T
h : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (G.op ⋙ ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj (op X)) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
⊢ (fun t => IsAmalgamation x t) ?w ∧
    ∀ (y : ((G.op ⋙ ℱ.val) ⋙ coyoneda.obj (op X)).obj (op U)), (fun t => IsAmalgamation x t) y → y = ?w
case w
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G✝ : C ⥤ D
hG : CompatiblePreserving K G✝
ℱ✝ : SheafOfTypes K
Z : C
T : Presieve Z
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T
h : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (G.op ⋙ ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj (op X)) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
⊢ ((G.op ⋙ ℱ.val) ⋙ coyoneda.obj (op X)).obj (op U)
[PROOFSTEP]
swap
[GOAL]
case w
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G✝ : C ⥤ D
hG : CompatiblePreserving K G✝
ℱ✝ : SheafOfTypes K
Z : C
T : Presieve Z
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T
h : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (G.op ⋙ ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj (op X)) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
⊢ ((G.op ⋙ ℱ.val) ⋙ coyoneda.obj (op X)).obj (op U)
[PROOFSTEP]
apply H.amalgamate (x.functorPushforward G)
[GOAL]
case w
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G✝ : C ⥤ D
hG : CompatiblePreserving K G✝
ℱ✝ : SheafOfTypes K
Z : C
T : Presieve Z
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T
h : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (G.op ⋙ ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj (op X)) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
⊢ Compatible (FamilyOfElements.functorPushforward G x)
[PROOFSTEP]
exact hx'
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G✝ : C ⥤ D
hG : CompatiblePreserving K G✝
ℱ✝ : SheafOfTypes K
Z : C
T : Presieve Z
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T
h : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (G.op ⋙ ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj (op X)) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
⊢ (fun t => IsAmalgamation x t) (IsSheafFor.amalgamate H (FamilyOfElements.functorPushforward G x) hx') ∧
    ∀ (y : ((G.op ⋙ ℱ.val) ⋙ coyoneda.obj (op X)).obj (op U)),
      (fun t => IsAmalgamation x t) y → y = IsSheafFor.amalgamate H (FamilyOfElements.functorPushforward G x) hx'
[PROOFSTEP]
constructor
[GOAL]
case h.left
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G✝ : C ⥤ D
hG : CompatiblePreserving K G✝
ℱ✝ : SheafOfTypes K
Z : C
T : Presieve Z
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T
h : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (G.op ⋙ ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj (op X)) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
⊢ (fun t => IsAmalgamation x t) (IsSheafFor.amalgamate H (FamilyOfElements.functorPushforward G x) hx')
[PROOFSTEP]
intro V f hf
[GOAL]
case h.left
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G✝ : C ⥤ D
hG : CompatiblePreserving K G✝
ℱ✝ : SheafOfTypes K
Z : C
T : Presieve Z
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T
h : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (G.op ⋙ ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj (op X)) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
V : C
f : V ⟶ U
hf : S.arrows f
⊢ ((G.op ⋙ ℱ.val) ⋙ coyoneda.obj (op X)).map f.op
      (IsSheafFor.amalgamate H (FamilyOfElements.functorPushforward G x) hx') =
    x f hf
[PROOFSTEP]
convert H.isAmalgamation hx' (G.map f) (image_mem_functorPushforward G S hf)
[GOAL]
case h.e'_3.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G✝ : C ⥤ D
hG : CompatiblePreserving K G✝
ℱ✝ : SheafOfTypes K
Z : C
T : Presieve Z
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T
h : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (G.op ⋙ ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj (op X)) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
V : C
f : V ⟶ U
hf : S.arrows f
e_1✝ : ((G.op ⋙ ℱ.val) ⋙ coyoneda.obj (op X)).obj (op V) = (ℱ.val ⋙ coyoneda.obj (op X)).obj (op (G.obj V))
⊢ x f hf = FamilyOfElements.functorPushforward G x (G.map f) (_ : Presieve.functorPushforward G S.arrows (G.map f))
[PROOFSTEP]
rw [hG₁.apply_map (sheafOver ℱ X) hx]
[GOAL]
case h.right
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G✝ : C ⥤ D
hG : CompatiblePreserving K G✝
ℱ✝ : SheafOfTypes K
Z : C
T : Presieve Z
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T
h : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (G.op ⋙ ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj (op X)) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
⊢ ∀ (y : ((G.op ⋙ ℱ.val) ⋙ coyoneda.obj (op X)).obj (op U)),
    (fun t => IsAmalgamation x t) y → y = IsSheafFor.amalgamate H (FamilyOfElements.functorPushforward G x) hx'
[PROOFSTEP]
intro y hy
[GOAL]
case h.right
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G✝ : C ⥤ D
hG : CompatiblePreserving K G✝
ℱ✝ : SheafOfTypes K
Z : C
T : Presieve Z
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T
h : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (G.op ⋙ ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj (op X)) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
y : ((G.op ⋙ ℱ.val) ⋙ coyoneda.obj (op X)).obj (op U)
hy : IsAmalgamation x y
⊢ y = IsSheafFor.amalgamate H (FamilyOfElements.functorPushforward G x) hx'
[PROOFSTEP]
refine' H.isSeparatedFor _ y _ _ (H.isAmalgamation (hx.functorPushforward hG₁ (sheafOver ℱ X)))
[GOAL]
case h.right
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G✝ : C ⥤ D
hG : CompatiblePreserving K G✝
ℱ✝ : SheafOfTypes K
Z : C
T : Presieve Z
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T
h : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (G.op ⋙ ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj (op X)) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
y : ((G.op ⋙ ℱ.val) ⋙ coyoneda.obj (op X)).obj (op U)
hy : IsAmalgamation x y
⊢ IsAmalgamation (FamilyOfElements.functorPushforward G x) y
[PROOFSTEP]
rintro V f
  ⟨Z, f', g', h, rfl⟩
      -- porting note: didn't need coercion (S : Presieve U) in Lean 3
[GOAL]
case h.right.intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G✝ : C ⥤ D
hG : CompatiblePreserving K G✝
ℱ✝ : SheafOfTypes K
Z✝ : C
T : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T
h✝ : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (G.op ⋙ ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj (op X)) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
y : ((G.op ⋙ ℱ.val) ⋙ coyoneda.obj (op X)).obj (op U)
hy : IsAmalgamation x y
V : D
Z : C
f' : Z ⟶ U
g' : V ⟶ G.obj Z
h : S.arrows f'
⊢ (ℱ.val ⋙ coyoneda.obj (op X)).map (g' ≫ G.map f').op y =
    FamilyOfElements.functorPushforward G x (g' ≫ G.map f') (_ : ∃ Z_1 g h, S.arrows g ∧ g' ≫ G.map f' = h ≫ G.map g)
[PROOFSTEP]
erw [FamilyOfElements.comp_of_compatible (S.functorPushforward G) hx'
    (image_mem_functorPushforward G (S : Presieve U) h) g']
[GOAL]
case h.right.intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G✝ : C ⥤ D
hG : CompatiblePreserving K G✝
ℱ✝ : SheafOfTypes K
Z✝ : C
T : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T
h✝ : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (G.op ⋙ ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj (op X)) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
y : ((G.op ⋙ ℱ.val) ⋙ coyoneda.obj (op X)).obj (op U)
hy : IsAmalgamation x y
V : D
Z : C
f' : Z ⟶ U
g' : V ⟶ G.obj Z
h : S.arrows f'
⊢ (ℱ.val ⋙ coyoneda.obj (op X)).map (g' ≫ G.map f').op y =
    (sheafOver ℱ X).val.map g'.op
      (FamilyOfElements.functorPushforward G x (G.map f') (_ : Presieve.functorPushforward G S.arrows (G.map f')))
[PROOFSTEP]
dsimp
[GOAL]
case h.right.intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G✝ : C ⥤ D
hG : CompatiblePreserving K G✝
ℱ✝ : SheafOfTypes K
Z✝ : C
T : Presieve Z✝
x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T
h✝ : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (G.op ⋙ ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj (op X)) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
y : ((G.op ⋙ ℱ.val) ⋙ coyoneda.obj (op X)).obj (op U)
hy : IsAmalgamation x y
V : D
Z : C
f' : Z ⟶ U
g' : V ⟶ G.obj Z
h : S.arrows f'
⊢ y ≫ ℱ.val.map ((G.map f').op ≫ g'.op) =
    FamilyOfElements.functorPushforward G x (G.map f') (_ : Presieve.functorPushforward G S.arrows (G.map f')) ≫
      ℱ.val.map g'.op
[PROOFSTEP]
simp [hG₁.apply_map (sheafOver ℱ X) hx h, ← hy f' h]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G✝ : C ⥤ D
hG : CompatiblePreserving K G✝
ℱ✝ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T
h : Compatible x
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
⊢ { obj := fun ℱ => pullbackSheaf hG₁ hG₂ ℱ,
          map := fun {X Y} f => { val := ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map f.val } }.map
      (𝟙 ℱ) =
    𝟙
      ({ obj := fun ℱ => pullbackSheaf hG₁ hG₂ ℱ,
            map := fun {X Y} f => { val := ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map f.val } }.obj
        ℱ)
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G✝ : C ⥤ D
hG : CompatiblePreserving K G✝
ℱ✝ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T
h : Compatible x
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
⊢ ({ obj := fun ℱ => pullbackSheaf hG₁ hG₂ ℱ,
            map := fun {X Y} f => { val := ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map f.val } }.map
        (𝟙 ℱ)).val =
    (𝟙
        ({ obj := fun ℱ => pullbackSheaf hG₁ hG₂ ℱ,
              map := fun {X Y} f => { val := ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map f.val } }.obj
          ℱ)).val
[PROOFSTEP]
apply ((whiskeringLeft _ _ _).obj G.op).map_id
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G✝ : C ⥤ D
hG : CompatiblePreserving K G✝
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G✝.op ⋙ ℱ.val) T
h : Compatible x
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
X✝ Y✝ Z✝ : Sheaf K A
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun ℱ => pullbackSheaf hG₁ hG₂ ℱ,
          map := fun {X Y} f => { val := ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map f.val } }.map
      (f ≫ g) =
    { obj := fun ℱ => pullbackSheaf hG₁ hG₂ ℱ,
            map := fun {X Y} f => { val := ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map f.val } }.map
        f ≫
      { obj := fun ℱ => pullbackSheaf hG₁ hG₂ ℱ,
            map := fun {X Y} f => { val := ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map f.val } }.map
        g
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G✝ : C ⥤ D
hG : CompatiblePreserving K G✝
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G✝.op ⋙ ℱ.val) T
h : Compatible x
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
X✝ Y✝ Z✝ : Sheaf K A
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ({ obj := fun ℱ => pullbackSheaf hG₁ hG₂ ℱ,
            map := fun {X Y} f => { val := ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map f.val } }.map
        (f ≫ g)).val =
    ({ obj := fun ℱ => pullbackSheaf hG₁ hG₂ ℱ,
              map := fun {X Y} f => { val := ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map f.val } }.map
          f ≫
        { obj := fun ℱ => pullbackSheaf hG₁ hG₂ ℱ,
              map := fun {X Y} f => { val := ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map f.val } }.map
          g).val
[PROOFSTEP]
apply ((whiskeringLeft _ _ _).obj G.op).map_comp
