[GOAL]
C : Type u_1
inst✝² : Category.{?u.2498, u_1} C
D : Type u_2
inst✝¹ : Category.{?u.2505, u_2} D
E : Type u_3
inst✝ : Category.{?u.2512, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
G : C ⥤ D
U Y✝ Z✝ : D
f✝ : Y✝ ⟶ U
x✝ : Presieve.coverByImage G U f✝
g : Z✝ ⟶ Y✝
Z : C
f₁ : Y✝ ⟶ G.obj Z
f₂ : G.obj Z ⟶ U
e : f₁ ≫ f₂ = f✝
⊢ (g ≫ f₁) ≫ f₂ = g ≫ f✝
[PROOFSTEP]
rw [Category.assoc, ← e]
[GOAL]
C : Type u_1
inst✝² : Category.{u_4, u_1} C
D : Type u_2
inst✝¹ : Category.{u_5, u_2} D
E : Type u_3
inst✝ : Category.{?u.4255, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
G : C ⥤ D
X : D
Y : C
f : G.obj Y ⟶ X
⊢ 𝟙 (G.obj Y) ≫ f = f
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝³ : Category.{u_5, u_1} C
D : Type u_2
inst✝² : Category.{u_6, u_2} D
E : Type u_3
inst✝¹ : Category.{?u.5707, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝ : Category.{?u.5759, u_4} A
G : C ⥤ D
H✝ H : CoverDense K G
ℱ : SheafOfTypes K
X : D
s t : ℱ.val.obj (op X)
h : ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), ℱ.val.map f.op s = ℱ.val.map f.op t
⊢ s = t
[PROOFSTEP]
apply (ℱ.cond (Sieve.coverByImage G X) (H.is_cover X)).isSeparatedFor.ext
[GOAL]
C : Type u_1
inst✝³ : Category.{u_5, u_1} C
D : Type u_2
inst✝² : Category.{u_6, u_2} D
E : Type u_3
inst✝¹ : Category.{?u.5707, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝ : Category.{?u.5759, u_4} A
G : C ⥤ D
H✝ H : CoverDense K G
ℱ : SheafOfTypes K
X : D
s t : ℱ.val.obj (op X)
h : ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), ℱ.val.map f.op s = ℱ.val.map f.op t
⊢ ∀ ⦃Y : D⦄ ⦃f : Y ⟶ X⦄, (Sieve.coverByImage G X).arrows f → ℱ.val.map f.op s = ℱ.val.map f.op t
[PROOFSTEP]
rintro Y _ ⟨Z, f₁, f₂, ⟨rfl⟩⟩
[GOAL]
case intro.mk.refl
C : Type u_1
inst✝³ : Category.{u_5, u_1} C
D : Type u_2
inst✝² : Category.{u_6, u_2} D
E : Type u_3
inst✝¹ : Category.{?u.5707, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝ : Category.{?u.5759, u_4} A
G : C ⥤ D
H✝ H : CoverDense K G
ℱ : SheafOfTypes K
X : D
s t : ℱ.val.obj (op X)
h : ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), ℱ.val.map f.op s = ℱ.val.map f.op t
Y : D
Z : C
f₁ : Y ⟶ G.obj Z
f₂ : G.obj Z ⟶ X
⊢ ℱ.val.map (f₁ ≫ f₂).op s = ℱ.val.map (f₁ ≫ f₂).op t
[PROOFSTEP]
simp [h f₂]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
E : Type u_3
inst✝² : Category.{?u.7958, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.8010, u_4} A
G : C ⥤ D
H✝ : CoverDense K G
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
⊢ Sieve.functorPushforward G (Sieve.functorPullback G ↑T) ∈ GrothendieckTopology.sieves K (G.obj X)
[PROOFSTEP]
refine' K.superset_covering _ (K.bind_covering T.property fun Y f _ => H.is_cover Y)
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
E : Type u_3
inst✝² : Category.{?u.7958, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.8010, u_4} A
G : C ⥤ D
H✝ : CoverDense K G
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
⊢ (Sieve.bind (↑T).arrows fun Y f x => Sieve.coverByImage G Y) ≤ Sieve.functorPushforward G (Sieve.functorPullback G ↑T)
[PROOFSTEP]
rintro Y _ ⟨Z, _, f, hf, ⟨W, g, f', ⟨rfl⟩⟩, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.mk.refl
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
E : Type u_3
inst✝² : Category.{?u.7958, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.8010, u_4} A
G : C ⥤ D
H✝ : CoverDense K G
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
Y Z : D
f : Z ⟶ G.obj X
hf : (↑T).arrows f
W : C
g : Y ⟶ G.obj W
f' : G.obj W ⟶ Z
⊢ (Sieve.functorPushforward G (Sieve.functorPullback G ↑T)).arrows ((g ≫ f') ≫ f)
[PROOFSTEP]
use W
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
E : Type u_3
inst✝² : Category.{?u.7958, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.8010, u_4} A
G : C ⥤ D
H✝ : CoverDense K G
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
Y Z : D
f : Z ⟶ G.obj X
hf : (↑T).arrows f
W : C
g : Y ⟶ G.obj W
f' : G.obj W ⟶ Z
⊢ ∃ g_1 h, (Sieve.functorPullback G ↑T).arrows g_1 ∧ (g ≫ f') ≫ f = h ≫ G.map g_1
[PROOFSTEP]
use G.preimage (f' ≫ f)
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
E : Type u_3
inst✝² : Category.{?u.7958, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.8010, u_4} A
G : C ⥤ D
H✝ : CoverDense K G
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
Y Z : D
f : Z ⟶ G.obj X
hf : (↑T).arrows f
W : C
g : Y ⟶ G.obj W
f' : G.obj W ⟶ Z
⊢ ∃ h, (Sieve.functorPullback G ↑T).arrows (G.preimage (f' ≫ f)) ∧ (g ≫ f') ≫ f = h ≫ G.map (G.preimage (f' ≫ f))
[PROOFSTEP]
use g
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
E : Type u_3
inst✝² : Category.{?u.7958, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.8010, u_4} A
G : C ⥤ D
H✝ : CoverDense K G
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
Y Z : D
f : Z ⟶ G.obj X
hf : (↑T).arrows f
W : C
g : Y ⟶ G.obj W
f' : G.obj W ⟶ Z
⊢ (Sieve.functorPullback G ↑T).arrows (G.preimage (f' ≫ f)) ∧ (g ≫ f') ≫ f = g ≫ G.map (G.preimage (f' ≫ f))
[PROOFSTEP]
constructor
[GOAL]
case h.left
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
E : Type u_3
inst✝² : Category.{?u.7958, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.8010, u_4} A
G : C ⥤ D
H✝ : CoverDense K G
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
Y Z : D
f : Z ⟶ G.obj X
hf : (↑T).arrows f
W : C
g : Y ⟶ G.obj W
f' : G.obj W ⟶ Z
⊢ (Sieve.functorPullback G ↑T).arrows (G.preimage (f' ≫ f))
[PROOFSTEP]
simpa using T.val.downward_closed hf f'
[GOAL]
case h.right
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
E : Type u_3
inst✝² : Category.{?u.7958, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.8010, u_4} A
G : C ⥤ D
H✝ : CoverDense K G
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
Y Z : D
f : Z ⟶ G.obj X
hf : (↑T).arrows f
W : C
g : Y ⟶ G.obj W
f' : G.obj W ⟶ Z
⊢ (g ≫ f') ≫ f = g ≫ G.map (G.preimage (f' ≫ f))
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.50179, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.50231, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
x : ℱ.obj (op X)
⊢ FamilyOfElements.Compatible (pushforwardFamily α x)
[PROOFSTEP]
intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ e
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.50179, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.50231, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
x : ℱ.obj (op X)
Y₁ Y₂ Z : D
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : coverByImage G X f₁
h₂ : coverByImage G X f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ ℱ'.val.map g₁.op (pushforwardFamily α x f₁ h₁) = ℱ'.val.map g₂.op (pushforwardFamily α x f₂ h₂)
[PROOFSTEP]
apply H.ext
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.50179, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.50231, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
x : ℱ.obj (op X)
Y₁ Y₂ Z : D
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : coverByImage G X f₁
h₂ : coverByImage G X f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ Z),
    ℱ'.val.map f.op (ℱ'.val.map g₁.op (pushforwardFamily α x f₁ h₁)) =
      ℱ'.val.map f.op (ℱ'.val.map g₂.op (pushforwardFamily α x f₂ h₂))
[PROOFSTEP]
intro Y f
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.50179, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.50231, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
x : ℱ.obj (op X)
Y₁ Y₂ Z : D
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : coverByImage G X f₁
h₂ : coverByImage G X f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
Y : C
f : G.obj Y ⟶ Z
⊢ ℱ'.val.map f.op (ℱ'.val.map g₁.op (pushforwardFamily α x f₁ h₁)) =
    ℱ'.val.map f.op (ℱ'.val.map g₂.op (pushforwardFamily α x f₂ h₂))
[PROOFSTEP]
simp only [pushforwardFamily, ← FunctorToTypes.map_comp_apply, ← op_comp]
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.50179, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.50231, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
x : ℱ.obj (op X)
Y₁ Y₂ Z : D
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : coverByImage G X f₁
h₂ : coverByImage G X f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
Y : C
f : G.obj Y ⟶ Z
⊢ ℱ'.val.map (f ≫ g₁ ≫ (Nonempty.some h₁).lift).op
      (NatTrans.app α (op (Nonempty.some h₁).1) (ℱ.map (Nonempty.some h₁).map.op x)) =
    ℱ'.val.map (f ≫ g₂ ≫ (Nonempty.some h₂).lift).op
      (NatTrans.app α (op (Nonempty.some h₂).1) (ℱ.map (Nonempty.some h₂).map.op x))
[PROOFSTEP]
change (ℱ.map _ ≫ α.app (op _) ≫ ℱ'.val.map _) _ = (ℱ.map _ ≫ α.app (op _) ≫ ℱ'.val.map _) _
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.50179, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.50231, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
x : ℱ.obj (op X)
Y₁ Y₂ Z : D
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : coverByImage G X f₁
h₂ : coverByImage G X f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
Y : C
f : G.obj Y ⟶ Z
⊢ (ℱ.map (Nonempty.some h₁).map.op ≫
        NatTrans.app α (op (Nonempty.some h₁).1) ≫ ℱ'.val.map (f ≫ g₁ ≫ (Nonempty.some h₁).lift).op)
      x =
    (ℱ.map (Nonempty.some h₂).map.op ≫
        NatTrans.app α (op (Nonempty.some h₂).1) ≫ ℱ'.val.map (f ≫ g₂ ≫ (Nonempty.some h₂).lift).op)
      x
[PROOFSTEP]
rw [← G.image_preimage (f ≫ g₁ ≫ _)]
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.50179, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.50231, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
x : ℱ.obj (op X)
Y₁ Y₂ Z : D
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : coverByImage G X f₁
h₂ : coverByImage G X f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
Y : C
f : G.obj Y ⟶ Z
⊢ (ℱ.map (Nonempty.some h₁).map.op ≫
        NatTrans.app α (op (Nonempty.some h₁).1) ≫
          ℱ'.val.map (G.map (G.preimage (f ≫ g₁ ≫ (Nonempty.some h₁).lift))).op)
      x =
    (ℱ.map (Nonempty.some h₂).map.op ≫
        NatTrans.app α (op (Nonempty.some h₂).1) ≫ ℱ'.val.map (f ≫ g₂ ≫ (Nonempty.some h₂).lift).op)
      x
[PROOFSTEP]
rw [← G.image_preimage (f ≫ g₂ ≫ _)]
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.50179, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.50231, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
x : ℱ.obj (op X)
Y₁ Y₂ Z : D
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : coverByImage G X f₁
h₂ : coverByImage G X f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
Y : C
f : G.obj Y ⟶ Z
⊢ (ℱ.map (Nonempty.some h₁).map.op ≫
        NatTrans.app α (op (Nonempty.some h₁).1) ≫
          ℱ'.val.map (G.map (G.preimage (f ≫ g₁ ≫ (Nonempty.some h₁).lift))).op)
      x =
    (ℱ.map (Nonempty.some h₂).map.op ≫
        NatTrans.app α (op (Nonempty.some h₂).1) ≫
          ℱ'.val.map (G.map (G.preimage (f ≫ g₂ ≫ (Nonempty.some h₂).lift))).op)
      x
[PROOFSTEP]
erw [← α.naturality (G.preimage _).op]
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.50179, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.50231, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
x : ℱ.obj (op X)
Y₁ Y₂ Z : D
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : coverByImage G X f₁
h₂ : coverByImage G X f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
Y : C
f : G.obj Y ⟶ Z
⊢ (ℱ.map (Nonempty.some h₁).map.op ≫
        (G.op ⋙ ℱ).map (G.preimage (f ≫ g₁ ≫ (Nonempty.some h₁).lift)).op ≫ NatTrans.app α (op Y))
      x =
    (ℱ.map (Nonempty.some h₂).map.op ≫
        NatTrans.app α (op (Nonempty.some h₂).1) ≫
          ℱ'.val.map (G.map (G.preimage (f ≫ g₂ ≫ (Nonempty.some h₂).lift))).op)
      x
[PROOFSTEP]
erw [← α.naturality (G.preimage _).op]
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.50179, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.50231, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
x : ℱ.obj (op X)
Y₁ Y₂ Z : D
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : coverByImage G X f₁
h₂ : coverByImage G X f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
Y : C
f : G.obj Y ⟶ Z
⊢ (ℱ.map (Nonempty.some h₁).map.op ≫
        (G.op ⋙ ℱ).map (G.preimage (f ≫ g₁ ≫ (Nonempty.some h₁).lift)).op ≫ NatTrans.app α (op Y))
      x =
    (ℱ.map (Nonempty.some h₂).map.op ≫
        (G.op ⋙ ℱ).map (G.preimage (f ≫ g₂ ≫ (Nonempty.some h₂).lift)).op ≫ NatTrans.app α (op Y))
      x
[PROOFSTEP]
refine' congr_fun _ x
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.50179, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.50231, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
x : ℱ.obj (op X)
Y₁ Y₂ Z : D
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : coverByImage G X f₁
h₂ : coverByImage G X f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
Y : C
f : G.obj Y ⟶ Z
⊢ ℱ.map (Nonempty.some h₁).map.op ≫
      (G.op ⋙ ℱ).map (G.preimage (f ≫ g₁ ≫ (Nonempty.some h₁).lift)).op ≫ NatTrans.app α (op Y) =
    ℱ.map (Nonempty.some h₂).map.op ≫
      (G.op ⋙ ℱ).map (G.preimage (f ≫ g₂ ≫ (Nonempty.some h₂).lift)).op ≫ NatTrans.app α (op Y)
[PROOFSTEP]
simp only [Functor.comp_map, ← Category.assoc, Functor.op_map, Quiver.Hom.unop_op]
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.50179, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.50231, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
x : ℱ.obj (op X)
Y₁ Y₂ Z : D
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : coverByImage G X f₁
h₂ : coverByImage G X f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
Y : C
f : G.obj Y ⟶ Z
⊢ (ℱ.map (Nonempty.some h₁).map.op ≫ ℱ.map (G.map (G.preimage ((f ≫ g₁) ≫ (Nonempty.some h₁).lift))).op) ≫
      NatTrans.app α (op Y) =
    (ℱ.map (Nonempty.some h₂).map.op ≫ ℱ.map (G.map (G.preimage ((f ≫ g₂) ≫ (Nonempty.some h₂).lift))).op) ≫
      NatTrans.app α (op Y)
[PROOFSTEP]
rw [← ℱ.map_comp, ← ℱ.map_comp]
  -- `simp only [← ℱ.map_comp]` does nothing, even if I add
    -- the relevant explicit inputs
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.50179, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.50231, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
x : ℱ.obj (op X)
Y₁ Y₂ Z : D
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : coverByImage G X f₁
h₂ : coverByImage G X f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
Y : C
f : G.obj Y ⟶ Z
⊢ ℱ.map ((Nonempty.some h₁).map.op ≫ (G.map (G.preimage ((f ≫ g₁) ≫ (Nonempty.some h₁).lift))).op) ≫
      NatTrans.app α (op Y) =
    ℱ.map ((Nonempty.some h₂).map.op ≫ (G.map (G.preimage ((f ≫ g₂) ≫ (Nonempty.some h₂).lift))).op) ≫
      NatTrans.app α (op Y)
[PROOFSTEP]
simp only [← op_comp, G.image_preimage]
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.50179, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.50231, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
x : ℱ.obj (op X)
Y₁ Y₂ Z : D
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : coverByImage G X f₁
h₂ : coverByImage G X f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
Y : C
f : G.obj Y ⟶ Z
⊢ ℱ.map (((f ≫ g₁) ≫ (Nonempty.some h₁).lift) ≫ (Nonempty.some h₁).map).op ≫ NatTrans.app α (op Y) =
    ℱ.map (((f ≫ g₂) ≫ (Nonempty.some h₂).lift) ≫ (Nonempty.some h₂).map).op ≫ NatTrans.app α (op Y)
[PROOFSTEP]
congr 3
[GOAL]
case h.e_a.e_a.e_f
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.50179, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.50231, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
x : ℱ.obj (op X)
Y₁ Y₂ Z : D
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : coverByImage G X f₁
h₂ : coverByImage G X f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
Y : C
f : G.obj Y ⟶ Z
⊢ ((f ≫ g₁) ≫ (Nonempty.some h₁).lift) ≫ (Nonempty.some h₁).map =
    ((f ≫ g₂) ≫ (Nonempty.some h₂).lift) ≫ (Nonempty.some h₂).map
[PROOFSTEP]
simp [e]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.58542, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.58594, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
x : ℱ.obj (op X)
Y : C
f : G.obj Y ⟶ X
⊢ pushforwardFamily α x f (_ : coverByImage G X f) = NatTrans.app α (op Y) (ℱ.map f.op x)
[PROOFSTEP]
unfold pushforwardFamily
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.58542, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.58594, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
x : ℱ.obj (op X)
Y : C
f : G.obj Y ⟶ X
⊢ ℱ'.val.map (Nonempty.some (_ : coverByImage G X f)).lift.op
      (NatTrans.app α (op (Nonempty.some (_ : coverByImage G X f)).1)
        (ℱ.map (Nonempty.some (_ : coverByImage G X f)).map.op x)) =
    NatTrans.app α (op Y) (ℱ.map f.op x)
[PROOFSTEP]
refine'
  congr_fun
    (_ :
      (fun t =>
          ℱ'.val.map ((Nonempty.some (_ : coverByImage G X f)).lift.op)
            (α.app (op (Nonempty.some (_ : coverByImage G X f)).1)
              (ℱ.map ((Nonempty.some (_ : coverByImage G X f)).map.op) t))) =
        (fun t => α.app (op Y) (ℱ.map (f.op) t)))
    x
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.58542, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.58594, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
x : ℱ.obj (op X)
Y : C
f : G.obj Y ⟶ X
⊢ (fun t =>
      ℱ'.val.map (Nonempty.some (_ : coverByImage G X f)).lift.op
        (NatTrans.app α (op (Nonempty.some (_ : coverByImage G X f)).obj)
          (ℱ.map (Nonempty.some (_ : coverByImage G X f)).map.op t))) =
    fun t => NatTrans.app α (op Y) (ℱ.map f.op t)
[PROOFSTEP]
rw [← G.image_preimage (Nonempty.some _ : Presieve.CoverByImageStructure _ _).lift]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.58542, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.58594, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
x : ℱ.obj (op X)
Y : C
f : G.obj Y ⟶ X
⊢ (fun t =>
      ℱ'.val.map (G.map (G.preimage (Nonempty.some (_ : coverByImage G X f)).lift)).op
        (NatTrans.app α (op (Nonempty.some (_ : coverByImage G X f)).obj)
          (ℱ.map (Nonempty.some (_ : coverByImage G X f)).map.op t))) =
    fun t => NatTrans.app α (op Y) (ℱ.map f.op t)
[PROOFSTEP]
change ℱ.map _ ≫ α.app (op _) ≫ ℱ'.val.map _ = ℱ.map f.op ≫ α.app (op Y)
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.58542, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.58594, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
x : ℱ.obj (op X)
Y : C
f : G.obj Y ⟶ X
⊢ ℱ.map (Nonempty.some (_ : coverByImage G X f)).map.op ≫
      NatTrans.app α (op (Nonempty.some (_ : coverByImage G X f)).1) ≫
        ℱ'.val.map (G.map (G.preimage (Nonempty.some (_ : coverByImage G X f)).lift)).op =
    ℱ.map f.op ≫ NatTrans.app α (op Y)
[PROOFSTEP]
erw [← α.naturality (G.preimage _).op]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.58542, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.58594, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
x : ℱ.obj (op X)
Y : C
f : G.obj Y ⟶ X
⊢ ℱ.map (Nonempty.some (_ : coverByImage G X f)).map.op ≫
      (G.op ⋙ ℱ).map (G.preimage (Nonempty.some (_ : coverByImage G X f)).lift).op ≫ NatTrans.app α (op Y) =
    ℱ.map f.op ≫ NatTrans.app α (op Y)
[PROOFSTEP]
simp only [← Functor.map_comp, ← Category.assoc, Functor.comp_map, G.image_preimage, G.op_map, Quiver.Hom.unop_op, ←
  op_comp, Presieve.CoverByImageStructure.fac]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.64256, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.64308, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
Y : C
f : op X ⟶ op (G.obj Y)
x : ℱ.obj (op X)
⊢ ℱ'.val.map f (appHom H α X x) = NatTrans.app α (op Y) (ℱ.map f x)
[PROOFSTEP]
refine'
  ((ℱ'.cond _ (H.is_cover X)).valid_glue (pushforwardFamily_compatible H α x) f.unop
        (Presieve.in_coverByImage G f.unop)).trans
    _
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.64256, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.64308, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
Y : C
f : op X ⟶ op (G.obj Y)
x : ℱ.obj (op X)
⊢ pushforwardFamily α x f.unop (_ : coverByImage G (op X).unop f.unop) = NatTrans.app α (op Y) (ℱ.map f x)
[PROOFSTEP]
apply pushforwardFamily_apply
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.66869, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.66921, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
Y : C
f : op X ⟶ op (G.obj Y)
⊢ appHom H α X ≫ ℱ'.val.map f = ℱ.map f ≫ NatTrans.app α (op Y)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.66869, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.66921, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : D
Y : C
f : op X ⟶ op (G.obj Y)
a✝ : ℱ.obj (op X)
⊢ (appHom H α X ≫ ℱ'.val.map f) a✝ = (ℱ.map f ≫ NatTrans.app α (op Y)) a✝
[PROOFSTEP]
apply appHom_restrict
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.69396, u_1} C
D : Type u_2
inst✝³ : Category.{?u.69403, u_2} D
E : Type u_3
inst✝² : Category.{?u.69410, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.69462, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ Type v
ℱ'✝ : SheafOfTypes K
α : G.op ⋙ ℱ✝ ⟶ G.op ⋙ ℱ'✝.val
ℱ ℱ' : SheafOfTypes K
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
X : D
⊢ appHom H i.hom X ≫ appHom H i.inv X = 𝟙 (ℱ.val.obj (op X))
[PROOFSTEP]
ext x
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{?u.69396, u_1} C
D : Type u_2
inst✝³ : Category.{?u.69403, u_2} D
E : Type u_3
inst✝² : Category.{?u.69410, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.69462, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ Type v
ℱ'✝ : SheafOfTypes K
α : G.op ⋙ ℱ✝ ⟶ G.op ⋙ ℱ'✝.val
ℱ ℱ' : SheafOfTypes K
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
X : D
x : ℱ.val.obj (op X)
⊢ (appHom H i.hom X ≫ appHom H i.inv X) x = 𝟙 (ℱ.val.obj (op X)) x
[PROOFSTEP]
apply H.ext
[GOAL]
case h.h
C : Type u_1
inst✝⁴ : Category.{?u.69396, u_1} C
D : Type u_2
inst✝³ : Category.{?u.69403, u_2} D
E : Type u_3
inst✝² : Category.{?u.69410, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.69462, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ Type v
ℱ'✝ : SheafOfTypes K
α : G.op ⋙ ℱ✝ ⟶ G.op ⋙ ℱ'✝.val
ℱ ℱ' : SheafOfTypes K
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
X : D
x : ℱ.val.obj (op X)
⊢ ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X),
    ℱ.val.map f.op ((appHom H i.hom X ≫ appHom H i.inv X) x) = ℱ.val.map f.op (𝟙 (ℱ.val.obj (op X)) x)
[PROOFSTEP]
intro Y f
[GOAL]
case h.h
C : Type u_1
inst✝⁴ : Category.{?u.69396, u_1} C
D : Type u_2
inst✝³ : Category.{?u.69403, u_2} D
E : Type u_3
inst✝² : Category.{?u.69410, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.69462, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ Type v
ℱ'✝ : SheafOfTypes K
α : G.op ⋙ ℱ✝ ⟶ G.op ⋙ ℱ'✝.val
ℱ ℱ' : SheafOfTypes K
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
X : D
x : ℱ.val.obj (op X)
Y : C
f : G.obj Y ⟶ X
⊢ ℱ.val.map f.op ((appHom H i.hom X ≫ appHom H i.inv X) x) = ℱ.val.map f.op (𝟙 (ℱ.val.obj (op X)) x)
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.69396, u_1} C
D : Type u_2
inst✝³ : Category.{?u.69403, u_2} D
E : Type u_3
inst✝² : Category.{?u.69410, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.69462, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ Type v
ℱ'✝ : SheafOfTypes K
α : G.op ⋙ ℱ✝ ⟶ G.op ⋙ ℱ'✝.val
ℱ ℱ' : SheafOfTypes K
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
X : D
⊢ appHom H i.inv X ≫ appHom H i.hom X = 𝟙 (ℱ'.val.obj (op X))
[PROOFSTEP]
ext x
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{?u.69396, u_1} C
D : Type u_2
inst✝³ : Category.{?u.69403, u_2} D
E : Type u_3
inst✝² : Category.{?u.69410, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.69462, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ Type v
ℱ'✝ : SheafOfTypes K
α : G.op ⋙ ℱ✝ ⟶ G.op ⋙ ℱ'✝.val
ℱ ℱ' : SheafOfTypes K
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
X : D
x : ℱ'.val.obj (op X)
⊢ (appHom H i.inv X ≫ appHom H i.hom X) x = 𝟙 (ℱ'.val.obj (op X)) x
[PROOFSTEP]
apply H.ext
[GOAL]
case h.h
C : Type u_1
inst✝⁴ : Category.{?u.69396, u_1} C
D : Type u_2
inst✝³ : Category.{?u.69403, u_2} D
E : Type u_3
inst✝² : Category.{?u.69410, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.69462, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ Type v
ℱ'✝ : SheafOfTypes K
α : G.op ⋙ ℱ✝ ⟶ G.op ⋙ ℱ'✝.val
ℱ ℱ' : SheafOfTypes K
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
X : D
x : ℱ'.val.obj (op X)
⊢ ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X),
    ℱ'.val.map f.op ((appHom H i.inv X ≫ appHom H i.hom X) x) = ℱ'.val.map f.op (𝟙 (ℱ'.val.obj (op X)) x)
[PROOFSTEP]
intro Y f
[GOAL]
case h.h
C : Type u_1
inst✝⁴ : Category.{?u.69396, u_1} C
D : Type u_2
inst✝³ : Category.{?u.69403, u_2} D
E : Type u_3
inst✝² : Category.{?u.69410, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.69462, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ Type v
ℱ'✝ : SheafOfTypes K
α : G.op ⋙ ℱ✝ ⟶ G.op ⋙ ℱ'✝.val
ℱ ℱ' : SheafOfTypes K
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
X : D
x : ℱ'.val.obj (op X)
Y : C
f : G.obj Y ⟶ X
⊢ ℱ'.val.map f.op ((appHom H i.inv X ≫ appHom H i.hom X) x) = ℱ'.val.map f.op (𝟙 (ℱ'.val.obj (op X)) x)
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.74475, u_1} C
D : Type u_2
inst✝³ : Category.{?u.74482, u_2} D
E : Type u_3
inst✝² : Category.{?u.74489, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.74541, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α✝ α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Dᵒᵖ
f : X ⟶ Y
⊢ ℱ.map f ≫ (fun X => appHom H α X.unop) Y = (fun X => appHom H α X.unop) X ≫ ℱ'.val.map f
[PROOFSTEP]
ext x
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{?u.74475, u_1} C
D : Type u_2
inst✝³ : Category.{?u.74482, u_2} D
E : Type u_3
inst✝² : Category.{?u.74489, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.74541, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α✝ α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Dᵒᵖ
f : X ⟶ Y
x : ℱ.obj X
⊢ (ℱ.map f ≫ (fun X => appHom H α X.unop) Y) x = ((fun X => appHom H α X.unop) X ≫ ℱ'.val.map f) x
[PROOFSTEP]
apply H.ext ℱ' (unop Y)
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{?u.74475, u_1} C
D : Type u_2
inst✝³ : Category.{?u.74482, u_2} D
E : Type u_3
inst✝² : Category.{?u.74489, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.74541, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α✝ α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Dᵒᵖ
f : X ⟶ Y
x : ℱ.obj X
⊢ ∀ ⦃Y_1 : C⦄ (f_1 : G.obj Y_1 ⟶ Y.unop),
    ℱ'.val.map f_1.op ((ℱ.map f ≫ (fun X => appHom H α X.unop) Y) x) =
      ℱ'.val.map f_1.op (((fun X => appHom H α X.unop) X ≫ ℱ'.val.map f) x)
[PROOFSTEP]
intro Y' f'
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{?u.74475, u_1} C
D : Type u_2
inst✝³ : Category.{?u.74482, u_2} D
E : Type u_3
inst✝² : Category.{?u.74489, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.74541, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α✝ α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Dᵒᵖ
f : X ⟶ Y
x : ℱ.obj X
Y' : C
f' : G.obj Y' ⟶ Y.unop
⊢ ℱ'.val.map f'.op ((ℱ.map f ≫ (fun X => appHom H α X.unop) Y) x) =
    ℱ'.val.map f'.op (((fun X => appHom H α X.unop) X ≫ ℱ'.val.map f) x)
[PROOFSTEP]
simp only [appHom_restrict, types_comp_apply, ← FunctorToTypes.map_comp_apply]
  -- porting note: Lean 3 proof continued with a rewrite but we're done here
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.82193, u_1} C
D : Type u_2
inst✝³ : Category.{?u.82200, u_2} D
E : Type u_3
inst✝² : Category.{?u.82207, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.82259, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ Type v
ℱ'✝ : SheafOfTypes K
α : G.op ⋙ ℱ✝ ⟶ G.op ⋙ ℱ'✝.val
ℱ ℱ' : SheafOfTypes K
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
⊢ { val := (presheafIso H i).hom } ≫ { val := (presheafIso H i).inv } = 𝟙 ℱ
[PROOFSTEP]
ext1
[GOAL]
case w
C : Type u_1
inst✝⁴ : Category.{?u.82193, u_1} C
D : Type u_2
inst✝³ : Category.{?u.82200, u_2} D
E : Type u_3
inst✝² : Category.{?u.82207, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.82259, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ Type v
ℱ'✝ : SheafOfTypes K
α : G.op ⋙ ℱ✝ ⟶ G.op ⋙ ℱ'✝.val
ℱ ℱ' : SheafOfTypes K
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
⊢ ({ val := (presheafIso H i).hom } ≫ { val := (presheafIso H i).inv }).val = (𝟙 ℱ).val
[PROOFSTEP]
apply (presheafIso H i).hom_inv_id
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.82193, u_1} C
D : Type u_2
inst✝³ : Category.{?u.82200, u_2} D
E : Type u_3
inst✝² : Category.{?u.82207, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.82259, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ Type v
ℱ'✝ : SheafOfTypes K
α : G.op ⋙ ℱ✝ ⟶ G.op ⋙ ℱ'✝.val
ℱ ℱ' : SheafOfTypes K
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
⊢ { val := (presheafIso H i).inv } ≫ { val := (presheafIso H i).hom } = 𝟙 ℱ'
[PROOFSTEP]
ext1
[GOAL]
case w
C : Type u_1
inst✝⁴ : Category.{?u.82193, u_1} C
D : Type u_2
inst✝³ : Category.{?u.82200, u_2} D
E : Type u_3
inst✝² : Category.{?u.82207, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.82259, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ Type v
ℱ'✝ : SheafOfTypes K
α : G.op ⋙ ℱ✝ ⟶ G.op ⋙ ℱ'✝.val
ℱ ℱ' : SheafOfTypes K
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
⊢ ({ val := (presheafIso H i).inv } ≫ { val := (presheafIso H i).hom }).val = (𝟙 ℱ').val
[PROOFSTEP]
apply (presheafIso H i).inv_hom_id
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.86992, u_1} C
D : Type u_2
inst✝³ : Category.{?u.86999, u_2} D
E : Type u_3
inst✝² : Category.{?u.87006, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.90244, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Aᵒᵖ
f : X ⟶ Y
⊢ (coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.90244)).obj ℱ).map f ≫ (fun X => presheafHom H (homOver α X.unop)) Y =
    (fun X => presheafHom H (homOver α X.unop)) X ≫ (coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.90244)).obj ℱ'.val).map f
[PROOFSTEP]
ext U x
[GOAL]
case w.h.h
C : Type u_1
inst✝⁴ : Category.{?u.86992, u_1} C
D : Type u_2
inst✝³ : Category.{?u.86999, u_2} D
E : Type u_3
inst✝² : Category.{?u.87006, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.90244, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.90244)).obj ℱ).obj X).obj U
⊢ NatTrans.app
      ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.90244)).obj ℱ).map f ≫ (fun X => presheafHom H (homOver α X.unop)) Y)
      U x =
    NatTrans.app
      ((fun X => presheafHom H (homOver α X.unop)) X ≫
        (coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.90244)).obj ℱ'.val).map f)
      U x
[PROOFSTEP]
change appHom H (homOver α (unop Y)) (unop U) (f.unop ≫ x) = f.unop ≫ appHom H (homOver α (unop X)) (unop U) x
[GOAL]
case w.h.h
C : Type u_1
inst✝⁴ : Category.{?u.86992, u_1} C
D : Type u_2
inst✝³ : Category.{?u.86999, u_2} D
E : Type u_3
inst✝² : Category.{?u.87006, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.90244, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.90244)).obj ℱ).obj X).obj U
⊢ appHom H (homOver α Y.unop) U.unop (f.unop ≫ x) = f.unop ≫ appHom H (homOver α X.unop) U.unop x
[PROOFSTEP]
symm
[GOAL]
case w.h.h
C : Type u_1
inst✝⁴ : Category.{?u.86992, u_1} C
D : Type u_2
inst✝³ : Category.{?u.86999, u_2} D
E : Type u_3
inst✝² : Category.{?u.87006, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.90244, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.90244)).obj ℱ).obj X).obj U
⊢ f.unop ≫ appHom H (homOver α X.unop) U.unop x = appHom H (homOver α Y.unop) U.unop (f.unop ≫ x)
[PROOFSTEP]
apply sheaf_eq_amalgamation
[GOAL]
case w.h.h.hT
C : Type u_1
inst✝⁴ : Category.{?u.86992, u_1} C
D : Type u_2
inst✝³ : Category.{?u.86999, u_2} D
E : Type u_3
inst✝² : Category.{?u.87006, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.90244, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.90244)).obj ℱ).obj X).obj U
⊢ Sieve.coverByImage G U.unop ∈ GrothendieckTopology.sieves K U.unop
case w.h.h.hx
C : Type u_1
inst✝⁴ : Category.{?u.86992, u_1} C
D : Type u_2
inst✝³ : Category.{?u.86999, u_2} D
E : Type u_3
inst✝² : Category.{?u.87006, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.90244, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.90244)).obj ℱ).obj X).obj U
⊢ FamilyOfElements.Compatible fun Y_1 f_1 h => pushforwardFamily (homOver α Y.unop) (f.unop ≫ x) f_1 h
case w.h.h.h
C : Type u_1
inst✝⁴ : Category.{?u.86992, u_1} C
D : Type u_2
inst✝³ : Category.{?u.86999, u_2} D
E : Type u_3
inst✝² : Category.{?u.87006, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.90244, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.90244)).obj ℱ).obj X).obj U
⊢ FamilyOfElements.IsAmalgamation (fun Y_1 f_1 h => pushforwardFamily (homOver α Y.unop) (f.unop ≫ x) f_1 h)
    (f.unop ≫ appHom H (homOver α X.unop) U.unop x)
[PROOFSTEP]
apply H.is_cover
[GOAL]
case w.h.h.hx
C : Type u_1
inst✝⁴ : Category.{?u.86992, u_1} C
D : Type u_2
inst✝³ : Category.{?u.86999, u_2} D
E : Type u_3
inst✝² : Category.{?u.87006, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.90244, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.90244)).obj ℱ).obj X).obj U
⊢ FamilyOfElements.Compatible fun Y_1 f_1 h => pushforwardFamily (homOver α Y.unop) (f.unop ≫ x) f_1 h
[PROOFSTEP]
exact pushforwardFamily_compatible H (homOver α Y.unop) (f.unop ≫ x)
[GOAL]
case w.h.h.h
C : Type u_1
inst✝⁴ : Category.{?u.86992, u_1} C
D : Type u_2
inst✝³ : Category.{?u.86999, u_2} D
E : Type u_3
inst✝² : Category.{?u.87006, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.90244, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.90244)).obj ℱ).obj X).obj U
⊢ FamilyOfElements.IsAmalgamation (fun Y_1 f_1 h => pushforwardFamily (homOver α Y.unop) (f.unop ≫ x) f_1 h)
    (f.unop ≫ appHom H (homOver α X.unop) U.unop x)
[PROOFSTEP]
intro Y' f' hf'
[GOAL]
case w.h.h.h
C : Type u_1
inst✝⁴ : Category.{?u.86992, u_1} C
D : Type u_2
inst✝³ : Category.{?u.86999, u_2} D
E : Type u_3
inst✝² : Category.{?u.87006, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.90244, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.90244)).obj ℱ).obj X).obj U
Y' : D
f' : Y' ⟶ U.unop
hf' : (Sieve.coverByImage G U.unop).arrows f'
⊢ (ℱ'.val ⋙ coyoneda.obj (op Y.unop)).map f'.op (f.unop ≫ appHom H (homOver α X.unop) U.unop x) =
    (fun Y_1 f_1 h => pushforwardFamily (homOver α Y.unop) (f.unop ≫ x) f_1 h) Y' f' hf'
[PROOFSTEP]
change unop X ⟶ ℱ.obj (op (unop _)) at x
[GOAL]
case w.h.h.h
C : Type u_1
inst✝⁴ : Category.{?u.86992, u_1} C
D : Type u_2
inst✝³ : Category.{?u.86999, u_2} D
E : Type u_3
inst✝² : Category.{?u.87006, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.90244, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
Y' : D
f' : Y' ⟶ U.unop
hf' : (Sieve.coverByImage G U.unop).arrows f'
x : X.unop ⟶ ℱ.obj (op U.unop)
⊢ (ℱ'.val ⋙ coyoneda.obj (op Y.unop)).map f'.op (f.unop ≫ appHom H (homOver α X.unop) U.unop x) =
    (fun Y_1 f_1 h => pushforwardFamily (homOver α Y.unop) (f.unop ≫ x) f_1 h) Y' f' hf'
[PROOFSTEP]
dsimp
[GOAL]
case w.h.h.h
C : Type u_1
inst✝⁴ : Category.{?u.86992, u_1} C
D : Type u_2
inst✝³ : Category.{?u.86999, u_2} D
E : Type u_3
inst✝² : Category.{?u.87006, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.90244, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
Y' : D
f' : Y' ⟶ U.unop
hf' : (Sieve.coverByImage G U.unop).arrows f'
x : X.unop ⟶ ℱ.obj (op U.unop)
⊢ (f.unop ≫ appHom H (homOver α X.unop) U.unop x) ≫ ℱ'.val.map f'.op =
    (((f.unop ≫ x) ≫ ℱ.map (Nonempty.some hf').map.op) ≫ NatTrans.app α (op (Nonempty.some hf').1)) ≫
      ℱ'.val.map (Nonempty.some hf').lift.op
[PROOFSTEP]
simp only [pushforwardFamily, Functor.comp_map, coyoneda_obj_map, homOver_app, Category.assoc]
[GOAL]
case w.h.h.h
C : Type u_1
inst✝⁴ : Category.{?u.86992, u_1} C
D : Type u_2
inst✝³ : Category.{?u.86999, u_2} D
E : Type u_3
inst✝² : Category.{?u.87006, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.90244, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
Y' : D
f' : Y' ⟶ U.unop
hf' : (Sieve.coverByImage G U.unop).arrows f'
x : X.unop ⟶ ℱ.obj (op U.unop)
⊢ f.unop ≫ appHom H (homOver α X.unop) U.unop x ≫ ℱ'.val.map f'.op =
    f.unop ≫
      x ≫
        ℱ.map (Nonempty.some hf').map.op ≫
          NatTrans.app α (op (Nonempty.some hf').1) ≫ ℱ'.val.map (Nonempty.some hf').lift.op
[PROOFSTEP]
congr 1
[GOAL]
case w.h.h.h.e_a
C : Type u_1
inst✝⁴ : Category.{?u.86992, u_1} C
D : Type u_2
inst✝³ : Category.{?u.86999, u_2} D
E : Type u_3
inst✝² : Category.{?u.87006, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.90244, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
Y' : D
f' : Y' ⟶ U.unop
hf' : (Sieve.coverByImage G U.unop).arrows f'
x : X.unop ⟶ ℱ.obj (op U.unop)
⊢ appHom H (homOver α X.unop) U.unop x ≫ ℱ'.val.map f'.op =
    x ≫
      ℱ.map (Nonempty.some hf').map.op ≫
        NatTrans.app α (op (Nonempty.some hf').1) ≫ ℱ'.val.map (Nonempty.some hf').lift.op
[PROOFSTEP]
conv_lhs => rw [← hf'.some.fac]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.86992, u_1} C
D : Type u_2
inst✝³ : Category.{?u.86999, u_2} D
E : Type u_3
inst✝² : Category.{?u.87006, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.90244, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
Y' : D
f' : Y' ⟶ U.unop
hf' : (Sieve.coverByImage G U.unop).arrows f'
x : X.unop ⟶ ℱ.obj (op U.unop)
| appHom H (homOver α X.unop) U.unop x ≫ ℱ'.val.map f'.op
[PROOFSTEP]
rw [← hf'.some.fac]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.86992, u_1} C
D : Type u_2
inst✝³ : Category.{?u.86999, u_2} D
E : Type u_3
inst✝² : Category.{?u.87006, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.90244, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
Y' : D
f' : Y' ⟶ U.unop
hf' : (Sieve.coverByImage G U.unop).arrows f'
x : X.unop ⟶ ℱ.obj (op U.unop)
| appHom H (homOver α X.unop) U.unop x ≫ ℱ'.val.map f'.op
[PROOFSTEP]
rw [← hf'.some.fac]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.86992, u_1} C
D : Type u_2
inst✝³ : Category.{?u.86999, u_2} D
E : Type u_3
inst✝² : Category.{?u.87006, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.90244, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
Y' : D
f' : Y' ⟶ U.unop
hf' : (Sieve.coverByImage G U.unop).arrows f'
x : X.unop ⟶ ℱ.obj (op U.unop)
| appHom H (homOver α X.unop) U.unop x ≫ ℱ'.val.map f'.op
[PROOFSTEP]
rw [← hf'.some.fac]
[GOAL]
case w.h.h.h.e_a
C : Type u_1
inst✝⁴ : Category.{?u.86992, u_1} C
D : Type u_2
inst✝³ : Category.{?u.86999, u_2} D
E : Type u_3
inst✝² : Category.{?u.87006, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.90244, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
Y' : D
f' : Y' ⟶ U.unop
hf' : (Sieve.coverByImage G U.unop).arrows f'
x : X.unop ⟶ ℱ.obj (op U.unop)
⊢ appHom H (homOver α X.unop) U.unop x ≫ ℱ'.val.map ((Nonempty.some hf').lift ≫ (Nonempty.some hf').map).op =
    x ≫
      ℱ.map (Nonempty.some hf').map.op ≫
        NatTrans.app α (op (Nonempty.some hf').1) ≫ ℱ'.val.map (Nonempty.some hf').lift.op
[PROOFSTEP]
simp only [← Category.assoc, op_comp, Functor.map_comp]
[GOAL]
case w.h.h.h.e_a
C : Type u_1
inst✝⁴ : Category.{?u.86992, u_1} C
D : Type u_2
inst✝³ : Category.{?u.86999, u_2} D
E : Type u_3
inst✝² : Category.{?u.87006, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.90244, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
Y' : D
f' : Y' ⟶ U.unop
hf' : (Sieve.coverByImage G U.unop).arrows f'
x : X.unop ⟶ ℱ.obj (op U.unop)
⊢ (appHom H (homOver α X.unop) U.unop x ≫ ℱ'.val.map (Nonempty.some hf').map.op) ≫
      ℱ'.val.map (Nonempty.some hf').lift.op =
    ((x ≫ ℱ.map (Nonempty.some hf').map.op) ≫ NatTrans.app α (op (Nonempty.some hf').1)) ≫
      ℱ'.val.map (Nonempty.some hf').lift.op
[PROOFSTEP]
congr 1
[GOAL]
case w.h.h.h.e_a.e_a
C : Type u_1
inst✝⁴ : Category.{?u.86992, u_1} C
D : Type u_2
inst✝³ : Category.{?u.86999, u_2} D
E : Type u_3
inst✝² : Category.{?u.87006, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.90244, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
Y' : D
f' : Y' ⟶ U.unop
hf' : (Sieve.coverByImage G U.unop).arrows f'
x : X.unop ⟶ ℱ.obj (op U.unop)
⊢ appHom H (homOver α X.unop) U.unop x ≫ ℱ'.val.map (Nonempty.some hf').map.op =
    (x ≫ ℱ.map (Nonempty.some hf').map.op) ≫ NatTrans.app α (op (Nonempty.some hf').1)
[PROOFSTEP]
refine' (appHom_restrict H (homOver α (unop X)) hf'.some.map.op x).trans _
[GOAL]
case w.h.h.h.e_a.e_a
C : Type u_1
inst✝⁴ : Category.{?u.86992, u_1} C
D : Type u_2
inst✝³ : Category.{?u.86999, u_2} D
E : Type u_3
inst✝² : Category.{?u.87006, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.90244, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
Y' : D
f' : Y' ⟶ U.unop
hf' : (Sieve.coverByImage G U.unop).arrows f'
x : X.unop ⟶ ℱ.obj (op U.unop)
⊢ NatTrans.app (homOver α X.unop) (op (Nonempty.some hf').obj)
      ((ℱ ⋙ coyoneda.obj (op X.unop)).map (Nonempty.some hf').map.op x) =
    (x ≫ ℱ.map (Nonempty.some hf').map.op) ≫ NatTrans.app α (op (Nonempty.some hf').1)
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.95394, u_1} C
D : Type u_2
inst✝³ : Category.{?u.95401, u_2} D
E : Type u_3
inst✝² : Category.{?u.95408, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.95460, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
⊢ ℱ ⋙ yoneda ⟶ ℱ'.val ⋙ yoneda
[PROOFSTEP]
let α := sheafCoyonedaHom H α
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.95394, u_1} C
D : Type u_2
inst✝³ : Category.{?u.95401, u_2} D
E : Type u_3
inst✝² : Category.{?u.95408, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.95460, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α✝ : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
α : coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.95460)).obj ℱ ⟶
  coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.95460)).obj ℱ'.val :=
  sheafCoyonedaHom H α✝
⊢ ℱ ⋙ yoneda ⟶ ℱ'.val ⋙ yoneda
[PROOFSTEP]
refine'
  { app := _
    naturality := _ }
[GOAL]
case refine'_1
C : Type u_1
inst✝⁴ : Category.{?u.95394, u_1} C
D : Type u_2
inst✝³ : Category.{?u.95401, u_2} D
E : Type u_3
inst✝² : Category.{?u.95408, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.95460, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α✝ : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
α : coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.95460)).obj ℱ ⟶
  coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.95460)).obj ℱ'.val :=
  sheafCoyonedaHom H α✝
⊢ (X : Dᵒᵖ) → (ℱ ⋙ yoneda).obj X ⟶ (ℱ'.val ⋙ yoneda).obj X
[PROOFSTEP]
intro U
[GOAL]
case refine'_1
C : Type u_1
inst✝⁴ : Category.{?u.95394, u_1} C
D : Type u_2
inst✝³ : Category.{?u.95401, u_2} D
E : Type u_3
inst✝² : Category.{?u.95408, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.95460, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α✝ : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
α : coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.95460)).obj ℱ ⟶
  coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.95460)).obj ℱ'.val :=
  sheafCoyonedaHom H α✝
U : Dᵒᵖ
⊢ (ℱ ⋙ yoneda).obj U ⟶ (ℱ'.val ⋙ yoneda).obj U
[PROOFSTEP]
refine'
  { app := fun X => (α.app X).app U
    naturality := fun X Y f => by simpa using congr_app (α.naturality f) U }
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.95394, u_1} C
D : Type u_2
inst✝³ : Category.{?u.95401, u_2} D
E : Type u_3
inst✝² : Category.{?u.95408, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.95460, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α✝ : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
α : coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.95460)).obj ℱ ⟶
  coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.95460)).obj ℱ'.val :=
  sheafCoyonedaHom H α✝
U : Dᵒᵖ
X Y : Aᵒᵖ
f : X ⟶ Y
⊢ ((ℱ ⋙ yoneda).obj U).map f ≫ (fun X => NatTrans.app (NatTrans.app α X) U) Y =
    (fun X => NatTrans.app (NatTrans.app α X) U) X ≫ ((ℱ'.val ⋙ yoneda).obj U).map f
[PROOFSTEP]
simpa using congr_app (α.naturality f) U
[GOAL]
case refine'_2
C : Type u_1
inst✝⁴ : Category.{?u.95394, u_1} C
D : Type u_2
inst✝³ : Category.{?u.95401, u_2} D
E : Type u_3
inst✝² : Category.{?u.95408, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.95460, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α✝ : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
α : coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.95460)).obj ℱ ⟶
  coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.95460)).obj ℱ'.val :=
  sheafCoyonedaHom H α✝
⊢ ∀ ⦃X Y : Dᵒᵖ⦄ (f : X ⟶ Y),
    ((ℱ ⋙ yoneda).map f ≫ NatTrans.mk fun X => NatTrans.app (NatTrans.app α X) Y) =
      (NatTrans.mk fun X_1 => NatTrans.app (NatTrans.app α X_1) X) ≫ (ℱ'.val ⋙ yoneda).map f
[PROOFSTEP]
intro U V i
[GOAL]
case refine'_2
C : Type u_1
inst✝⁴ : Category.{?u.95394, u_1} C
D : Type u_2
inst✝³ : Category.{?u.95401, u_2} D
E : Type u_3
inst✝² : Category.{?u.95408, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.95460, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α✝ : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
α : coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.95460)).obj ℱ ⟶
  coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.95460)).obj ℱ'.val :=
  sheafCoyonedaHom H α✝
U V : Dᵒᵖ
i : U ⟶ V
⊢ ((ℱ ⋙ yoneda).map i ≫ NatTrans.mk fun X => NatTrans.app (NatTrans.app α X) V) =
    (NatTrans.mk fun X => NatTrans.app (NatTrans.app α X) U) ≫ (ℱ'.val ⋙ yoneda).map i
[PROOFSTEP]
ext X x
[GOAL]
case refine'_2.w.h.h
C : Type u_1
inst✝⁴ : Category.{?u.95394, u_1} C
D : Type u_2
inst✝³ : Category.{?u.95401, u_2} D
E : Type u_3
inst✝² : Category.{?u.95408, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.95460, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α✝ : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
α : coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.95460)).obj ℱ ⟶
  coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.95460)).obj ℱ'.val :=
  sheafCoyonedaHom H α✝
U V : Dᵒᵖ
i : U ⟶ V
X : Aᵒᵖ
x : ((ℱ ⋙ yoneda).obj U).obj X
⊢ NatTrans.app ((ℱ ⋙ yoneda).map i ≫ NatTrans.mk fun X => NatTrans.app (NatTrans.app α X) V) X x =
    NatTrans.app ((NatTrans.mk fun X => NatTrans.app (NatTrans.app α X) U) ≫ (ℱ'.val ⋙ yoneda).map i) X x
[PROOFSTEP]
exact congr_fun ((α.app X).naturality i) x
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.104971, u_1} C
D : Type u_2
inst✝³ : Category.{?u.104978, u_2} D
E : Type u_3
inst✝² : Category.{?u.104985, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.105037, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
α' : ℱ ⋙ yoneda ⟶ ℱ'.val ⋙ yoneda := sheafYonedaHom H α
X Y : Dᵒᵖ
f : X ⟶ Y
⊢ yoneda.map (ℱ.map f ≫ (fun X => yoneda.preimage (NatTrans.app α' X)) Y) =
    yoneda.map ((fun X => yoneda.preimage (NatTrans.app α' X)) X ≫ ℱ'.val.map f)
[PROOFSTEP]
simpa using α'.naturality f
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.112516, u_1} C
D : Type u_2
inst✝³ : Category.{?u.112523, u_2} D
E : Type u_3
inst✝² : Category.{?u.112530, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.112582, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
⊢ ℱ.val ≅ ℱ'.val
[PROOFSTEP]
have : ∀ X : Dᵒᵖ, IsIso ((sheafHom H i.hom).app X) := by
  intro X
  suffices IsIso (yoneda.map ((sheafHom H i.hom).app X)) by apply isIso_of_reflects_iso _ yoneda
  use(sheafYonedaHom H i.inv).app X
  constructor <;> ext x : 2 <;> simp only [sheafHom, NatTrans.comp_app, NatTrans.id_app, Functor.image_preimage]
  · exact ((Types.presheafIso H (isoOver i (unop x))).app X).hom_inv_id
  · exact ((Types.presheafIso H (isoOver i (unop x))).app X).inv_hom_id
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.112516, u_1} C
D : Type u_2
inst✝³ : Category.{?u.112523, u_2} D
E : Type u_3
inst✝² : Category.{?u.112530, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.112582, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
⊢ ∀ (X : Dᵒᵖ), IsIso (NatTrans.app (sheafHom H i.hom) X)
[PROOFSTEP]
intro X
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.112516, u_1} C
D : Type u_2
inst✝³ : Category.{?u.112523, u_2} D
E : Type u_3
inst✝² : Category.{?u.112530, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.112582, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
X : Dᵒᵖ
⊢ IsIso (NatTrans.app (sheafHom H i.hom) X)
[PROOFSTEP]
suffices IsIso (yoneda.map ((sheafHom H i.hom).app X)) by apply isIso_of_reflects_iso _ yoneda
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.112516, u_1} C
D : Type u_2
inst✝³ : Category.{?u.112523, u_2} D
E : Type u_3
inst✝² : Category.{?u.112530, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.112582, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
X : Dᵒᵖ
this : IsIso (yoneda.map (NatTrans.app (sheafHom H i.hom) X))
⊢ IsIso (NatTrans.app (sheafHom H i.hom) X)
[PROOFSTEP]
apply isIso_of_reflects_iso _ yoneda
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.112516, u_1} C
D : Type u_2
inst✝³ : Category.{?u.112523, u_2} D
E : Type u_3
inst✝² : Category.{?u.112530, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.112582, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
X : Dᵒᵖ
⊢ IsIso (yoneda.map (NatTrans.app (sheafHom H i.hom) X))
[PROOFSTEP]
use(sheafYonedaHom H i.inv).app X
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{?u.112516, u_1} C
D : Type u_2
inst✝³ : Category.{?u.112523, u_2} D
E : Type u_3
inst✝² : Category.{?u.112530, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.112582, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
X : Dᵒᵖ
⊢ yoneda.map (NatTrans.app (sheafHom H i.hom) X) ≫ NatTrans.app (sheafYonedaHom H i.inv) X =
      𝟙 (yoneda.obj (ℱ.val.obj X)) ∧
    NatTrans.app (sheafYonedaHom H i.inv) X ≫ yoneda.map (NatTrans.app (sheafHom H i.hom) X) =
      𝟙 (yoneda.obj (ℱ'.val.obj X))
[PROOFSTEP]
constructor
[GOAL]
case h.left
C : Type u_1
inst✝⁴ : Category.{?u.112516, u_1} C
D : Type u_2
inst✝³ : Category.{?u.112523, u_2} D
E : Type u_3
inst✝² : Category.{?u.112530, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.112582, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
X : Dᵒᵖ
⊢ yoneda.map (NatTrans.app (sheafHom H i.hom) X) ≫ NatTrans.app (sheafYonedaHom H i.inv) X =
    𝟙 (yoneda.obj (ℱ.val.obj X))
[PROOFSTEP]
ext x : 2
[GOAL]
case h.right
C : Type u_1
inst✝⁴ : Category.{?u.112516, u_1} C
D : Type u_2
inst✝³ : Category.{?u.112523, u_2} D
E : Type u_3
inst✝² : Category.{?u.112530, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.112582, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
X : Dᵒᵖ
⊢ NatTrans.app (sheafYonedaHom H i.inv) X ≫ yoneda.map (NatTrans.app (sheafHom H i.hom) X) =
    𝟙 (yoneda.obj (ℱ'.val.obj X))
[PROOFSTEP]
ext x : 2
[GOAL]
case h.left.w.h
C : Type u_1
inst✝⁴ : Category.{?u.112516, u_1} C
D : Type u_2
inst✝³ : Category.{?u.112523, u_2} D
E : Type u_3
inst✝² : Category.{?u.112530, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.112582, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
X : Dᵒᵖ
x : Aᵒᵖ
⊢ NatTrans.app (yoneda.map (NatTrans.app (sheafHom H i.hom) X) ≫ NatTrans.app (sheafYonedaHom H i.inv) X) x =
    NatTrans.app (𝟙 (yoneda.obj (ℱ.val.obj X))) x
[PROOFSTEP]
simp only [sheafHom, NatTrans.comp_app, NatTrans.id_app, Functor.image_preimage]
[GOAL]
case h.right.w.h
C : Type u_1
inst✝⁴ : Category.{?u.112516, u_1} C
D : Type u_2
inst✝³ : Category.{?u.112523, u_2} D
E : Type u_3
inst✝² : Category.{?u.112530, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.112582, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
X : Dᵒᵖ
x : Aᵒᵖ
⊢ NatTrans.app (NatTrans.app (sheafYonedaHom H i.inv) X ≫ yoneda.map (NatTrans.app (sheafHom H i.hom) X)) x =
    NatTrans.app (𝟙 (yoneda.obj (ℱ'.val.obj X))) x
[PROOFSTEP]
simp only [sheafHom, NatTrans.comp_app, NatTrans.id_app, Functor.image_preimage]
[GOAL]
case h.left.w.h
C : Type u_1
inst✝⁴ : Category.{?u.112516, u_1} C
D : Type u_2
inst✝³ : Category.{?u.112523, u_2} D
E : Type u_3
inst✝² : Category.{?u.112530, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.112582, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
X : Dᵒᵖ
x : Aᵒᵖ
⊢ NatTrans.app (NatTrans.app (sheafYonedaHom H i.hom) X) x ≫ NatTrans.app (NatTrans.app (sheafYonedaHom H i.inv) X) x =
    𝟙 ((yoneda.obj (ℱ.val.obj X)).obj x)
[PROOFSTEP]
exact ((Types.presheafIso H (isoOver i (unop x))).app X).hom_inv_id
[GOAL]
case h.right.w.h
C : Type u_1
inst✝⁴ : Category.{?u.112516, u_1} C
D : Type u_2
inst✝³ : Category.{?u.112523, u_2} D
E : Type u_3
inst✝² : Category.{?u.112530, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.112582, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
X : Dᵒᵖ
x : Aᵒᵖ
⊢ NatTrans.app (NatTrans.app (sheafYonedaHom H i.inv) X) x ≫ NatTrans.app (NatTrans.app (sheafYonedaHom H i.hom) X) x =
    𝟙 ((yoneda.obj (ℱ'.val.obj X)).obj x)
[PROOFSTEP]
exact ((Types.presheafIso H (isoOver i (unop x))).app X).inv_hom_id
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.112516, u_1} C
D : Type u_2
inst✝³ : Category.{?u.112523, u_2} D
E : Type u_3
inst✝² : Category.{?u.112530, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.112582, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
this : ∀ (X : Dᵒᵖ), IsIso (NatTrans.app (sheafHom H i.hom) X)
⊢ ℱ.val ≅ ℱ'.val
[PROOFSTEP]
haveI : IsIso (sheafHom H i.hom) := by apply NatIso.isIso_of_isIso_app
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.112516, u_1} C
D : Type u_2
inst✝³ : Category.{?u.112523, u_2} D
E : Type u_3
inst✝² : Category.{?u.112530, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.112582, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
this : ∀ (X : Dᵒᵖ), IsIso (NatTrans.app (sheafHom H i.hom) X)
⊢ IsIso (sheafHom H i.hom)
[PROOFSTEP]
apply NatIso.isIso_of_isIso_app
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.112516, u_1} C
D : Type u_2
inst✝³ : Category.{?u.112523, u_2} D
E : Type u_3
inst✝² : Category.{?u.112530, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.112582, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
this✝ : ∀ (X : Dᵒᵖ), IsIso (NatTrans.app (sheafHom H i.hom) X)
this : IsIso (sheafHom H i.hom)
⊢ ℱ.val ≅ ℱ'.val
[PROOFSTEP]
apply asIso (sheafHom H i.hom)
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.121616, u_1} C
D : Type u_2
inst✝³ : Category.{?u.121623, u_2} D
E : Type u_3
inst✝² : Category.{?u.121630, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.121682, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
⊢ { val := (presheafIso H i).hom } ≫ { val := (presheafIso H i).inv } = 𝟙 ℱ
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{?u.121616, u_1} C
D : Type u_2
inst✝³ : Category.{?u.121623, u_2} D
E : Type u_3
inst✝² : Category.{?u.121630, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.121682, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
⊢ ({ val := (presheafIso H i).hom } ≫ { val := (presheafIso H i).inv }).val = (𝟙 ℱ).val
[PROOFSTEP]
apply (presheafIso H i).hom_inv_id
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.121616, u_1} C
D : Type u_2
inst✝³ : Category.{?u.121623, u_2} D
E : Type u_3
inst✝² : Category.{?u.121630, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.121682, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
⊢ { val := (presheafIso H i).inv } ≫ { val := (presheafIso H i).hom } = 𝟙 ℱ'
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{?u.121616, u_1} C
D : Type u_2
inst✝³ : Category.{?u.121623, u_2} D
E : Type u_3
inst✝² : Category.{?u.121630, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{?u.121682, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val
⊢ ({ val := (presheafIso H i).inv } ≫ { val := (presheafIso H i).hom }).val = (𝟙 ℱ').val
[PROOFSTEP]
apply (presheafIso H i).inv_hom_id
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
E : Type u_3
inst✝² : Category.{?u.125013, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
⊢ whiskerLeft G.op (sheafHom H α) = α
[PROOFSTEP]
ext X
[GOAL]
case w.h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
E : Type u_3
inst✝² : Category.{?u.125013, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
⊢ NatTrans.app (whiskerLeft G.op (sheafHom H α)) X = NatTrans.app α X
[PROOFSTEP]
apply yoneda.map_injective
[GOAL]
case w.h.a
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
E : Type u_3
inst✝² : Category.{?u.125013, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
⊢ yoneda.map (NatTrans.app (whiskerLeft G.op (sheafHom H α)) X) = yoneda.map (NatTrans.app α X)
[PROOFSTEP]
ext U
[GOAL]
case w.h.a.w.h.h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
E : Type u_3
inst✝² : Category.{?u.125013, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
⊢ NatTrans.app (yoneda.map (NatTrans.app (whiskerLeft G.op (sheafHom H α)) X)) U a✝ =
    NatTrans.app (yoneda.map (NatTrans.app α X)) U a✝
[PROOFSTEP]
erw [yoneda.image_preimage ((H.sheafYonedaHom α).app (G.op.obj X))]
[GOAL]
case w.h.a.w.h.h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
E : Type u_3
inst✝² : Category.{?u.125013, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
⊢ NatTrans.app (NatTrans.app (sheafYonedaHom H α) (G.op.obj X)) U a✝ = NatTrans.app (yoneda.map (NatTrans.app α X)) U a✝
[PROOFSTEP]
symm
[GOAL]
case w.h.a.w.h.h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
E : Type u_3
inst✝² : Category.{?u.125013, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
⊢ NatTrans.app (yoneda.map (NatTrans.app α X)) U a✝ = NatTrans.app (NatTrans.app (sheafYonedaHom H α) (G.op.obj X)) U a✝
[PROOFSTEP]
change (show (ℱ'.val ⋙ coyoneda.obj (op (unop U))).obj (op (G.obj (unop X))) from _) = _
[GOAL]
case w.h.a.w.h.h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
E : Type u_3
inst✝² : Category.{?u.125013, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
⊢ (let_fun this := NatTrans.app (yoneda.map (NatTrans.app α X)) U a✝;
    this) =
    NatTrans.app (NatTrans.app (sheafYonedaHom H α) (G.op.obj X)) U a✝
[PROOFSTEP]
apply
  sheaf_eq_amalgamation ℱ'
    (H.is_cover _)
      -- porting note: next line was not needed in mathlib3
[GOAL]
case w.h.a.w.h.h.hx
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
E : Type u_3
inst✝² : Category.{?u.125013, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
⊢ FamilyOfElements.Compatible (pushforwardFamily (homOver α U.unop) a✝)
[PROOFSTEP]
exact (pushforwardFamily_compatible H _ _)
[GOAL]
case w.h.a.w.h.h.h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
E : Type u_3
inst✝² : Category.{?u.125013, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
⊢ FamilyOfElements.IsAmalgamation (pushforwardFamily (homOver α U.unop) a✝)
    (let_fun this := NatTrans.app (yoneda.map (NatTrans.app α X)) U a✝;
    this)
[PROOFSTEP]
intro Y f hf
[GOAL]
case w.h.a.w.h.h.h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
E : Type u_3
inst✝² : Category.{?u.125013, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
f : Y ⟶ G.obj X.unop
hf : (Sieve.coverByImage G (G.obj X.unop)).arrows f
⊢ (ℱ'.val ⋙ coyoneda.obj (op U.unop)).map f.op
      (let_fun this := NatTrans.app (yoneda.map (NatTrans.app α X)) U a✝;
      this) =
    pushforwardFamily (homOver α U.unop) a✝ f hf
[PROOFSTEP]
conv_lhs => rw [← hf.some.fac]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
E : Type u_3
inst✝² : Category.{?u.125013, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
f : Y ⟶ G.obj X.unop
hf : (Sieve.coverByImage G (G.obj X.unop)).arrows f
| (ℱ'.val ⋙ coyoneda.obj (op U.unop)).map f.op
    (let_fun this := NatTrans.app (yoneda.map (NatTrans.app α X)) U a✝;
    this)
[PROOFSTEP]
rw [← hf.some.fac]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
E : Type u_3
inst✝² : Category.{?u.125013, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
f : Y ⟶ G.obj X.unop
hf : (Sieve.coverByImage G (G.obj X.unop)).arrows f
| (ℱ'.val ⋙ coyoneda.obj (op U.unop)).map f.op
    (let_fun this := NatTrans.app (yoneda.map (NatTrans.app α X)) U a✝;
    this)
[PROOFSTEP]
rw [← hf.some.fac]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
E : Type u_3
inst✝² : Category.{?u.125013, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
f : Y ⟶ G.obj X.unop
hf : (Sieve.coverByImage G (G.obj X.unop)).arrows f
| (ℱ'.val ⋙ coyoneda.obj (op U.unop)).map f.op
    (let_fun this := NatTrans.app (yoneda.map (NatTrans.app α X)) U a✝;
    this)
[PROOFSTEP]
rw [← hf.some.fac]
[GOAL]
case w.h.a.w.h.h.h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
E : Type u_3
inst✝² : Category.{?u.125013, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
f : Y ⟶ G.obj X.unop
hf : (Sieve.coverByImage G (G.obj X.unop)).arrows f
⊢ (ℱ'.val ⋙ coyoneda.obj (op U.unop)).map ((Nonempty.some hf).lift ≫ (Nonempty.some hf).map).op
      (let_fun this := NatTrans.app (yoneda.map (NatTrans.app α X)) U a✝;
      this) =
    pushforwardFamily (homOver α U.unop) a✝ f hf
[PROOFSTEP]
simp only [pushforwardFamily, Functor.comp_map, yoneda_map_app, coyoneda_obj_map, op_comp,
  FunctorToTypes.map_comp_apply, homOver_app, ← Category.assoc]
[GOAL]
case w.h.a.w.h.h.h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
E : Type u_3
inst✝² : Category.{?u.125013, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
f : Y ⟶ G.obj X.unop
hf : (Sieve.coverByImage G (G.obj X.unop)).arrows f
⊢ ((a✝ ≫ NatTrans.app α X) ≫ ℱ'.val.map (Nonempty.some hf).map.op) ≫ ℱ'.val.map (Nonempty.some hf).lift.op =
    (sheafOver ℱ' U.unop).val.map (Nonempty.some hf).lift.op
      ((a✝ ≫ ℱ.map (Nonempty.some hf).map.op) ≫ NatTrans.app α (op (Nonempty.some hf).1))
[PROOFSTEP]
congr 1
[GOAL]
case w.h.a.w.h.h.h.e_a
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
E : Type u_3
inst✝² : Category.{?u.125013, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
f : Y ⟶ G.obj X.unop
hf : (Sieve.coverByImage G (G.obj X.unop)).arrows f
⊢ (a✝ ≫ NatTrans.app α X) ≫ ℱ'.val.map (Nonempty.some hf).map.op =
    (a✝ ≫ ℱ.map (Nonempty.some hf).map.op) ≫ NatTrans.app α (op (Nonempty.some hf).1)
[PROOFSTEP]
simp only [Category.assoc]
[GOAL]
case w.h.a.w.h.h.h.e_a
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
E : Type u_3
inst✝² : Category.{?u.125013, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
f : Y ⟶ G.obj X.unop
hf : (Sieve.coverByImage G (G.obj X.unop)).arrows f
⊢ a✝ ≫ NatTrans.app α X ≫ ℱ'.val.map (Nonempty.some hf).map.op =
    a✝ ≫ ℱ.map (Nonempty.some hf).map.op ≫ NatTrans.app α (op (Nonempty.some hf).1)
[PROOFSTEP]
congr 1
[GOAL]
case w.h.a.w.h.h.h.e_a.e_a
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
E : Type u_3
inst✝² : Category.{?u.125013, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
f : Y ⟶ G.obj X.unop
hf : (Sieve.coverByImage G (G.obj X.unop)).arrows f
⊢ NatTrans.app α X ≫ ℱ'.val.map (Nonempty.some hf).map.op =
    ℱ.map (Nonempty.some hf).map.op ≫ NatTrans.app α (op (Nonempty.some hf).1)
[PROOFSTEP]
rw [← G.image_preimage hf.some.map]
[GOAL]
case w.h.a.w.h.h.h.e_a.e_a
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
E : Type u_3
inst✝² : Category.{?u.125013, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
f : Y ⟶ G.obj X.unop
hf : (Sieve.coverByImage G (G.obj X.unop)).arrows f
⊢ NatTrans.app α X ≫ ℱ'.val.map (G.map (G.preimage (Nonempty.some hf).map)).op =
    ℱ.map (G.map (G.preimage (Nonempty.some hf).map)).op ≫ NatTrans.app α (op (Nonempty.some hf).1)
[PROOFSTEP]
symm
[GOAL]
case w.h.a.w.h.h.h.e_a.e_a
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
E : Type u_3
inst✝² : Category.{?u.125013, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
f : Y ⟶ G.obj X.unop
hf : (Sieve.coverByImage G (G.obj X.unop)).arrows f
⊢ ℱ.map (G.map (G.preimage (Nonempty.some hf).map)).op ≫ NatTrans.app α (op (Nonempty.some hf).1) =
    NatTrans.app α X ≫ ℱ'.val.map (G.map (G.preimage (Nonempty.some hf).map)).op
[PROOFSTEP]
apply α.naturality (G.preimage hf.some.map).op
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_7, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
E : Type u_3
inst✝² : Category.{?u.131586, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
⊢ sheafHom H (whiskerLeft G.op α) = α
[PROOFSTEP]
ext X
[GOAL]
case w.h
C : Type u_1
inst✝⁴ : Category.{u_7, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
E : Type u_3
inst✝² : Category.{?u.131586, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
⊢ NatTrans.app (sheafHom H (whiskerLeft G.op α)) X = NatTrans.app α X
[PROOFSTEP]
apply yoneda.map_injective
[GOAL]
case w.h.a
C : Type u_1
inst✝⁴ : Category.{u_7, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
E : Type u_3
inst✝² : Category.{?u.131586, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
⊢ yoneda.map (NatTrans.app (sheafHom H (whiskerLeft G.op α)) X) = yoneda.map (NatTrans.app α X)
[PROOFSTEP]
ext U
[GOAL]
case w.h.a.w.h.h
C : Type u_1
inst✝⁴ : Category.{u_7, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
E : Type u_3
inst✝² : Category.{?u.131586, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj (ℱ.obj X)).obj U
⊢ NatTrans.app (yoneda.map (NatTrans.app (sheafHom H (whiskerLeft G.op α)) X)) U a✝ =
    NatTrans.app (yoneda.map (NatTrans.app α X)) U a✝
[PROOFSTEP]
erw [yoneda.image_preimage ((H.sheafYonedaHom (whiskerLeft G.op α)).app X)]
[GOAL]
case w.h.a.w.h.h
C : Type u_1
inst✝⁴ : Category.{u_7, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
E : Type u_3
inst✝² : Category.{?u.131586, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj (ℱ.obj X)).obj U
⊢ NatTrans.app (NatTrans.app (sheafYonedaHom H (whiskerLeft G.op α)) X) U a✝ =
    NatTrans.app (yoneda.map (NatTrans.app α X)) U a✝
[PROOFSTEP]
symm
[GOAL]
case w.h.a.w.h.h
C : Type u_1
inst✝⁴ : Category.{u_7, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
E : Type u_3
inst✝² : Category.{?u.131586, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj (ℱ.obj X)).obj U
⊢ NatTrans.app (yoneda.map (NatTrans.app α X)) U a✝ =
    NatTrans.app (NatTrans.app (sheafYonedaHom H (whiskerLeft G.op α)) X) U a✝
[PROOFSTEP]
change (show (ℱ'.val ⋙ coyoneda.obj (op (unop U))).obj (op (unop X)) from _) = _
[GOAL]
case w.h.a.w.h.h
C : Type u_1
inst✝⁴ : Category.{u_7, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
E : Type u_3
inst✝² : Category.{?u.131586, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj (ℱ.obj X)).obj U
⊢ (let_fun this := NatTrans.app (yoneda.map (NatTrans.app α X)) U a✝;
    this) =
    NatTrans.app (NatTrans.app (sheafYonedaHom H (whiskerLeft G.op α)) X) U a✝
[PROOFSTEP]
apply
  sheaf_eq_amalgamation ℱ'
    (H.is_cover _)
      -- porting note: next line was not needed in mathlib3
[GOAL]
case w.h.a.w.h.h.hx
C : Type u_1
inst✝⁴ : Category.{u_7, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
E : Type u_3
inst✝² : Category.{?u.131586, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj (ℱ.obj X)).obj U
⊢ FamilyOfElements.Compatible (pushforwardFamily (homOver (whiskerLeft G.op α) U.unop) a✝)
[PROOFSTEP]
exact (pushforwardFamily_compatible H _ _)
[GOAL]
case w.h.a.w.h.h.h
C : Type u_1
inst✝⁴ : Category.{u_7, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
E : Type u_3
inst✝² : Category.{?u.131586, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj (ℱ.obj X)).obj U
⊢ FamilyOfElements.IsAmalgamation (pushforwardFamily (homOver (whiskerLeft G.op α) U.unop) a✝)
    (let_fun this := NatTrans.app (yoneda.map (NatTrans.app α X)) U a✝;
    this)
[PROOFSTEP]
intro Y f hf
[GOAL]
case w.h.a.w.h.h.h
C : Type u_1
inst✝⁴ : Category.{u_7, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
E : Type u_3
inst✝² : Category.{?u.131586, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj (ℱ.obj X)).obj U
Y : D
f : Y ⟶ X.unop
hf : (Sieve.coverByImage G X.unop).arrows f
⊢ (ℱ'.val ⋙ coyoneda.obj (op U.unop)).map f.op
      (let_fun this := NatTrans.app (yoneda.map (NatTrans.app α X)) U a✝;
      this) =
    pushforwardFamily (homOver (whiskerLeft G.op α) U.unop) a✝ f hf
[PROOFSTEP]
conv_lhs => rw [← hf.some.fac]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_7, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
E : Type u_3
inst✝² : Category.{?u.131586, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj (ℱ.obj X)).obj U
Y : D
f : Y ⟶ X.unop
hf : (Sieve.coverByImage G X.unop).arrows f
| (ℱ'.val ⋙ coyoneda.obj (op U.unop)).map f.op
    (let_fun this := NatTrans.app (yoneda.map (NatTrans.app α X)) U a✝;
    this)
[PROOFSTEP]
rw [← hf.some.fac]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_7, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
E : Type u_3
inst✝² : Category.{?u.131586, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj (ℱ.obj X)).obj U
Y : D
f : Y ⟶ X.unop
hf : (Sieve.coverByImage G X.unop).arrows f
| (ℱ'.val ⋙ coyoneda.obj (op U.unop)).map f.op
    (let_fun this := NatTrans.app (yoneda.map (NatTrans.app α X)) U a✝;
    this)
[PROOFSTEP]
rw [← hf.some.fac]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_7, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
E : Type u_3
inst✝² : Category.{?u.131586, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj (ℱ.obj X)).obj U
Y : D
f : Y ⟶ X.unop
hf : (Sieve.coverByImage G X.unop).arrows f
| (ℱ'.val ⋙ coyoneda.obj (op U.unop)).map f.op
    (let_fun this := NatTrans.app (yoneda.map (NatTrans.app α X)) U a✝;
    this)
[PROOFSTEP]
rw [← hf.some.fac]
[GOAL]
case w.h.a.w.h.h.h
C : Type u_1
inst✝⁴ : Category.{u_7, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
E : Type u_3
inst✝² : Category.{?u.131586, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj (ℱ.obj X)).obj U
Y : D
f : Y ⟶ X.unop
hf : (Sieve.coverByImage G X.unop).arrows f
⊢ (ℱ'.val ⋙ coyoneda.obj (op U.unop)).map ((Nonempty.some hf).lift ≫ (Nonempty.some hf).map).op
      (let_fun this := NatTrans.app (yoneda.map (NatTrans.app α X)) U a✝;
      this) =
    pushforwardFamily (homOver (whiskerLeft G.op α) U.unop) a✝ f hf
[PROOFSTEP]
dsimp
[GOAL]
case w.h.a.w.h.h.h
C : Type u_1
inst✝⁴ : Category.{u_7, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
E : Type u_3
inst✝² : Category.{?u.131586, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_5, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj (ℱ.obj X)).obj U
Y : D
f : Y ⟶ X.unop
hf : (Sieve.coverByImage G X.unop).arrows f
⊢ (a✝ ≫ NatTrans.app α X) ≫ ℱ'.val.map ((Nonempty.some hf).map.op ≫ (Nonempty.some hf).lift.op) =
    ((a✝ ≫ ℱ.map (Nonempty.some hf).map.op) ≫ NatTrans.app α (op (G.obj (Nonempty.some hf).1))) ≫
      ℱ'.val.map (Nonempty.some hf).lift.op
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_7, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.139678, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_6, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'
i : IsIso (whiskerLeft G.op α.val)
⊢ IsIso α
[PROOFSTEP]
convert IsIso.of_iso (sheafIso H (asIso (whiskerLeft G.op α.val))) using 1
[GOAL]
case h.e'_5
C : Type u_1
inst✝⁴ : Category.{u_7, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.139678, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_6, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'
i : IsIso (whiskerLeft G.op α.val)
⊢ α = (sheafIso H (asIso (whiskerLeft G.op α.val))).hom
[PROOFSTEP]
ext1
[GOAL]
case h.e'_5.h
C : Type u_1
inst✝⁴ : Category.{u_7, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
E : Type u_3
inst✝² : Category.{?u.139678, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category.{u_6, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'
i : IsIso (whiskerLeft G.op α.val)
⊢ α.val = (sheafIso H (asIso (whiskerLeft G.op α.val))).hom.val
[PROOFSTEP]
apply (sheafHom_eq H _).symm
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
D : Type u_2
inst✝⁴ : Category.{u_6, u_2} D
E : Type u_3
inst✝³ : Category.{?u.142765, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{?u.142817, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝¹ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
inst✝ : Faithful G
⊢ CompatiblePreserving K G
[PROOFSTEP]
constructor
[GOAL]
case Compatible
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
D : Type u_2
inst✝⁴ : Category.{u_6, u_2} D
E : Type u_3
inst✝³ : Category.{?u.142765, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{?u.142817, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝¹ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
inst✝ : Faithful G
⊢ ∀ (ℱ : SheafOfTypes K) {Z : C} {T : Presieve Z} {x : FamilyOfElements (G.op ⋙ ℱ.val) T},
    FamilyOfElements.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₂ eq
[GOAL]
case Compatible
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
D : Type u_2
inst✝⁴ : Category.{u_6, u_2} D
E : Type u_3
inst✝³ : Category.{?u.142765, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{?u.142817, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝¹ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
inst✝ : Faithful G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : FamilyOfElements.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₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
⊢ ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)
[PROOFSTEP]
apply H.ext
[GOAL]
case Compatible.h
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
D : Type u_2
inst✝⁴ : Category.{u_6, u_2} D
E : Type u_3
inst✝³ : Category.{?u.142765, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{?u.142817, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝¹ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
inst✝ : Faithful G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : FamilyOfElements.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₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
⊢ ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), ℱ.val.map f.op (ℱ.val.map f₁.op (x g₁ hg₁)) = ℱ.val.map f.op (ℱ.val.map f₂.op (x g₂ hg₂))
[PROOFSTEP]
intro W i
[GOAL]
case Compatible.h
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
D : Type u_2
inst✝⁴ : Category.{u_6, u_2} D
E : Type u_3
inst✝³ : Category.{?u.142765, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{?u.142817, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝¹ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
inst✝ : Faithful G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : FamilyOfElements.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₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
⊢ ℱ.val.map i.op (ℱ.val.map f₁.op (x g₁ hg₁)) = ℱ.val.map i.op (ℱ.val.map f₂.op (x g₂ hg₂))
[PROOFSTEP]
simp only [← FunctorToTypes.map_comp_apply, ← op_comp]
[GOAL]
case Compatible.h
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
D : Type u_2
inst✝⁴ : Category.{u_6, u_2} D
E : Type u_3
inst✝³ : Category.{?u.142765, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{?u.142817, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝¹ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
inst✝ : Faithful G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : FamilyOfElements.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₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
⊢ ℱ.val.map (i ≫ f₁).op (x g₁ hg₁) = ℱ.val.map (i ≫ f₂).op (x g₂ hg₂)
[PROOFSTEP]
rw [← G.image_preimage (i ≫ f₁)]
[GOAL]
case Compatible.h
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
D : Type u_2
inst✝⁴ : Category.{u_6, u_2} D
E : Type u_3
inst✝³ : Category.{?u.142765, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{?u.142817, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝¹ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
inst✝ : Faithful G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : FamilyOfElements.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₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
⊢ ℱ.val.map (G.map (G.preimage (i ≫ f₁))).op (x g₁ hg₁) = ℱ.val.map (i ≫ f₂).op (x g₂ hg₂)
[PROOFSTEP]
rw [← G.image_preimage (i ≫ f₂)]
[GOAL]
case Compatible.h
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
D : Type u_2
inst✝⁴ : Category.{u_6, u_2} D
E : Type u_3
inst✝³ : Category.{?u.142765, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{?u.142817, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝¹ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
inst✝ : Faithful G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : FamilyOfElements.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₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
⊢ ℱ.val.map (G.map (G.preimage (i ≫ f₁))).op (x g₁ hg₁) = ℱ.val.map (G.map (G.preimage (i ≫ f₂))).op (x g₂ hg₂)
[PROOFSTEP]
apply hx
[GOAL]
case Compatible.h.a
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
D : Type u_2
inst✝⁴ : Category.{u_6, u_2} D
E : Type u_3
inst✝³ : Category.{?u.142765, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{?u.142817, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝¹ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
inst✝ : Faithful G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : FamilyOfElements.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₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
⊢ Full.preimage (i ≫ f₁) ≫ g₁ = Full.preimage (i ≫ f₂) ≫ g₂
[PROOFSTEP]
apply G.map_injective
[GOAL]
case Compatible.h.a.a
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
D : Type u_2
inst✝⁴ : Category.{u_6, u_2} D
E : Type u_3
inst✝³ : Category.{?u.142765, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{?u.142817, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝¹ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
inst✝ : Faithful G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : FamilyOfElements.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₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
⊢ G.map (Full.preimage (i ≫ f₁) ≫ g₁) = G.map (Full.preimage (i ≫ f₂) ≫ g₂)
[PROOFSTEP]
simp [eq]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.148653, u_1} C
D : Type u_2
inst✝⁴ : Category.{?u.148660, u_2} D
E : Type u_3
inst✝³ : Category.{?u.148667, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{?u.150533, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝¹ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
inst✝ : Faithful G
Hp : CoverPreserving J K G
⊢ ∀ {X Y : Sheaf K A}, Function.Injective (Sites.pullback A (_ : CompatiblePreserving K G) Hp).map
[PROOFSTEP]
intro ℱ ℱ' α β e
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.148653, u_1} C
D : Type u_2
inst✝⁴ : Category.{?u.148660, u_2} D
E : Type u_3
inst✝³ : Category.{?u.148667, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{?u.150533, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝¹ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ : Sheaf K A
inst✝ : Faithful G
Hp : CoverPreserving J K G
ℱ ℱ' : Sheaf K A
α β : ℱ ⟶ ℱ'
e :
  (Sites.pullback A (_ : CompatiblePreserving K G) Hp).map α =
    (Sites.pullback A (_ : CompatiblePreserving K G) Hp).map β
⊢ α = β
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u_1
inst✝⁵ : Category.{?u.148653, u_1} C
D : Type u_2
inst✝⁴ : Category.{?u.148660, u_2} D
E : Type u_3
inst✝³ : Category.{?u.148667, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{?u.150533, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝¹ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ : Sheaf K A
inst✝ : Faithful G
Hp : CoverPreserving J K G
ℱ ℱ' : Sheaf K A
α β : ℱ ⟶ ℱ'
e :
  (Sites.pullback A (_ : CompatiblePreserving K G) Hp).map α =
    (Sites.pullback A (_ : CompatiblePreserving K G) Hp).map β
⊢ α.val = β.val
[PROOFSTEP]
apply_fun fun e => e.val at e
[GOAL]
case h
C : Type u_1
inst✝⁵ : Category.{?u.148653, u_1} C
D : Type u_2
inst✝⁴ : Category.{?u.148660, u_2} D
E : Type u_3
inst✝³ : Category.{?u.148667, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{?u.150533, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝¹ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ : Sheaf K A
inst✝ : Faithful G
Hp : CoverPreserving J K G
ℱ ℱ' : Sheaf K A
α β : ℱ ⟶ ℱ'
e :
  ((Sites.pullback A (_ : CompatiblePreserving K G) Hp).map α).val =
    ((Sites.pullback A (_ : CompatiblePreserving K G) Hp).map β).val
⊢ α.val = β.val
[PROOFSTEP]
dsimp at e
[GOAL]
case h
C : Type u_1
inst✝⁵ : Category.{?u.148653, u_1} C
D : Type u_2
inst✝⁴ : Category.{?u.148660, u_2} D
E : Type u_3
inst✝³ : Category.{?u.148667, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{?u.150533, u_4} A
G : C ⥤ D
H : CoverDense K G
inst✝¹ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ : Sheaf K A
inst✝ : Faithful G
Hp : CoverPreserving J K G
ℱ ℱ' : Sheaf K A
α β : ℱ ⟶ ℱ'
e : whiskerLeft G.op α.val = whiskerLeft G.op β.val
⊢ α.val = β.val
[PROOFSTEP]
rw [← H.sheafHom_eq α.val, ← H.sheafHom_eq β.val, e]
[GOAL]
C D : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v, u} D
G : C ⥤ D
inst✝³ : Full G
inst✝² : Faithful G
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : Limits.HasLimits A
Hd : CoverDense K G
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
⊢ Sheaf J A ≌ Sheaf K A
[PROOFSTEP]
symm
[GOAL]
C D : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v, u} D
G : C ⥤ D
inst✝³ : Full G
inst✝² : Faithful G
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : Limits.HasLimits A
Hd : CoverDense K G
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
⊢ Sheaf K A ≌ Sheaf J A
[PROOFSTEP]
let α := Sites.pullbackCopullbackAdjunction.{w, v, u} A Hp Hl Hd.compatiblePreserving
[GOAL]
C D : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v, u} D
G : C ⥤ D
inst✝³ : Full G
inst✝² : Faithful G
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : Limits.HasLimits A
Hd : CoverDense K G
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
α : Sites.pullback A (_ : CompatiblePreserving K G) Hp ⊣ Sites.copullback A Hl :=
  Sites.pullbackCopullbackAdjunction A Hp Hl (_ : CompatiblePreserving K G)
⊢ Sheaf K A ≌ Sheaf J A
[PROOFSTEP]
have : ∀ X : Sheaf J A, IsIso (α.counit.app X) := by
  intro ℱ
  haveI : IsIso ((sheafToPresheaf J A).map (α.counit.app ℱ)) :=
    IsIso.of_iso ((@asIso _ _ _ _ _ (Ran.reflective A G.op)).app ℱ.val)
  apply
    ReflectsIsomorphisms.reflects
      (sheafToPresheaf J A)
        -- porting note: a bunch of instances are not synthesized in lean 4 for some reason
[GOAL]
C D : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v, u} D
G : C ⥤ D
inst✝³ : Full G
inst✝² : Faithful G
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : Limits.HasLimits A
Hd : CoverDense K G
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
α : Sites.pullback A (_ : CompatiblePreserving K G) Hp ⊣ Sites.copullback A Hl :=
  Sites.pullbackCopullbackAdjunction A Hp Hl (_ : CompatiblePreserving K G)
⊢ ∀ (X : Sheaf J A), IsIso (NatTrans.app α.counit X)
[PROOFSTEP]
intro ℱ
[GOAL]
C D : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v, u} D
G : C ⥤ D
inst✝³ : Full G
inst✝² : Faithful G
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : Limits.HasLimits A
Hd : CoverDense K G
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
α : Sites.pullback A (_ : CompatiblePreserving K G) Hp ⊣ Sites.copullback A Hl :=
  Sites.pullbackCopullbackAdjunction A Hp Hl (_ : CompatiblePreserving K G)
ℱ : Sheaf J A
⊢ IsIso (NatTrans.app α.counit ℱ)
[PROOFSTEP]
haveI : IsIso ((sheafToPresheaf J A).map (α.counit.app ℱ)) :=
  IsIso.of_iso ((@asIso _ _ _ _ _ (Ran.reflective A G.op)).app ℱ.val)
[GOAL]
C D : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v, u} D
G : C ⥤ D
inst✝³ : Full G
inst✝² : Faithful G
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : Limits.HasLimits A
Hd : CoverDense K G
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
α : Sites.pullback A (_ : CompatiblePreserving K G) Hp ⊣ Sites.copullback A Hl :=
  Sites.pullbackCopullbackAdjunction A Hp Hl (_ : CompatiblePreserving K G)
ℱ : Sheaf J A
this : IsIso ((sheafToPresheaf J A).map (NatTrans.app α.counit ℱ))
⊢ IsIso (NatTrans.app α.counit ℱ)
[PROOFSTEP]
apply
  ReflectsIsomorphisms.reflects
    (sheafToPresheaf J A)
      -- porting note: a bunch of instances are not synthesized in lean 4 for some reason
[GOAL]
C D : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v, u} D
G : C ⥤ D
inst✝³ : Full G
inst✝² : Faithful G
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : Limits.HasLimits A
Hd : CoverDense K G
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
α : Sites.pullback A (_ : CompatiblePreserving K G) Hp ⊣ Sites.copullback A Hl :=
  Sites.pullbackCopullbackAdjunction A Hp Hl (_ : CompatiblePreserving K G)
this : ∀ (X : Sheaf J A), IsIso (NatTrans.app α.counit X)
⊢ Sheaf K A ≌ Sheaf J A
[PROOFSTEP]
haveI : IsIso α.counit := NatIso.isIso_of_isIso_app _
[GOAL]
C D : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v, u} D
G : C ⥤ D
inst✝³ : Full G
inst✝² : Faithful G
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : Limits.HasLimits A
Hd : CoverDense K G
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
α : Sites.pullback A (_ : CompatiblePreserving K G) Hp ⊣ Sites.copullback A Hl :=
  Sites.pullbackCopullbackAdjunction A Hp Hl (_ : CompatiblePreserving K G)
this✝ : ∀ (X : Sheaf J A), IsIso (NatTrans.app α.counit X)
this : IsIso α.counit
⊢ Sheaf K A ≌ Sheaf J A
[PROOFSTEP]
haveI : Full (Sites.pullback A Hd.compatiblePreserving Hp) := CoverDense.Sites.Pullback.full J Hd Hp
[GOAL]
C D : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v, u} D
G : C ⥤ D
inst✝³ : Full G
inst✝² : Faithful G
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : Limits.HasLimits A
Hd : CoverDense K G
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
α : Sites.pullback A (_ : CompatiblePreserving K G) Hp ⊣ Sites.copullback A Hl :=
  Sites.pullbackCopullbackAdjunction A Hp Hl (_ : CompatiblePreserving K G)
this✝¹ : ∀ (X : Sheaf J A), IsIso (NatTrans.app α.counit X)
this✝ : IsIso α.counit
this : Full (Sites.pullback A (_ : CompatiblePreserving K G) Hp)
⊢ Sheaf K A ≌ Sheaf J A
[PROOFSTEP]
haveI : Faithful (Sites.pullback A Hd.compatiblePreserving Hp) := CoverDense.Sites.Pullback.faithful J Hd Hp
[GOAL]
C D : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v, u} D
G : C ⥤ D
inst✝³ : Full G
inst✝² : Faithful G
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : Limits.HasLimits A
Hd : CoverDense K G
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
α : Sites.pullback A (_ : CompatiblePreserving K G) Hp ⊣ Sites.copullback A Hl :=
  Sites.pullbackCopullbackAdjunction A Hp Hl (_ : CompatiblePreserving K G)
this✝² : ∀ (X : Sheaf J A), IsIso (NatTrans.app α.counit X)
this✝¹ : IsIso α.counit
this✝ : Full (Sites.pullback A (_ : CompatiblePreserving K G) Hp)
this : Faithful (Sites.pullback A (_ : CompatiblePreserving K G) Hp)
⊢ Sheaf K A ≌ Sheaf J A
[PROOFSTEP]
haveI : IsIso α.unit := CategoryTheory.unit_isIso_of_L_fully_faithful α
[GOAL]
C D : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v, u} D
G : C ⥤ D
inst✝³ : Full G
inst✝² : Faithful G
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : Limits.HasLimits A
Hd : CoverDense K G
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
α : Sites.pullback A (_ : CompatiblePreserving K G) Hp ⊣ Sites.copullback A Hl :=
  Sites.pullbackCopullbackAdjunction A Hp Hl (_ : CompatiblePreserving K G)
this✝³ : ∀ (X : Sheaf J A), IsIso (NatTrans.app α.counit X)
this✝² : IsIso α.counit
this✝¹ : Full (Sites.pullback A (_ : CompatiblePreserving K G) Hp)
this✝ : Faithful (Sites.pullback A (_ : CompatiblePreserving K G) Hp)
this : IsIso α.unit
⊢ Sheaf K A ≌ Sheaf J A
[PROOFSTEP]
exact
  { functor := Sites.pullback A Hd.compatiblePreserving Hp
    inverse := Sites.copullback A Hl
    unitIso := asIso α.unit
    counitIso := asIso α.counit
    functor_unitIso_comp := fun ℱ => by convert α.left_triangle_components }
[GOAL]
C D : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v, u} D
G : C ⥤ D
inst✝³ : Full G
inst✝² : Faithful G
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : Limits.HasLimits A
Hd : CoverDense K G
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
α : Sites.pullback A (_ : CompatiblePreserving K G) Hp ⊣ Sites.copullback A Hl :=
  Sites.pullbackCopullbackAdjunction A Hp Hl (_ : CompatiblePreserving K G)
this✝³ : ∀ (X : Sheaf J A), IsIso (NatTrans.app α.counit X)
this✝² : IsIso α.counit
this✝¹ : Full (Sites.pullback A (_ : CompatiblePreserving K G) Hp)
this✝ : Faithful (Sites.pullback A (_ : CompatiblePreserving K G) Hp)
this : IsIso α.unit
ℱ : Sheaf K A
⊢ (Sites.pullback A (_ : CompatiblePreserving K G) Hp).map (NatTrans.app (asIso α.unit).hom ℱ) ≫
      NatTrans.app (asIso α.counit).hom ((Sites.pullback A (_ : CompatiblePreserving K G) Hp).obj ℱ) =
    𝟙 ((Sites.pullback A (_ : CompatiblePreserving K G) Hp).obj ℱ)
[PROOFSTEP]
convert α.left_triangle_components