case w.h
C : Type u_5
inst✝⁴ : Category C
D : Type u_1
inst✝³ : Category D
E : Type ?u.131136
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
⊢ (sheafHom H (whiskerLeft (Functor.op G) α)).app X = α.app X
C : Type u_5
inst✝⁴ : Category C
D : Type u_1
inst✝³ : Category D
E : Type ?u.131136
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
⊢ sheafHom H (whiskerLeft (Functor.op G) α) = α
ext X
case w.h.a
C : Type u_5
inst✝⁴ : Category C
D : Type u_1
inst✝³ : Category D
E : Type ?u.131136
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
⊢ yoneda.map ((sheafHom H (whiskerLeft (Functor.op G) α)).app X) = yoneda.map (α.app X)
case w.h
C : Type u_5
inst✝⁴ : Category C
D : Type u_1
inst✝³ : Category D
E : Type ?u.131136
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
⊢ (sheafHom H (whiskerLeft (Functor.op G) α)).app X = α.app X
apply yoneda.map_injective
case w.h.a.w.h.h
C : Type u_5
inst✝⁴ : Category C
D : Type u_1
inst✝³ : Category D
E : Type ?u.131136
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category 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
⊢ (yoneda.map ((sheafHom H (whiskerLeft (Functor.op G) α)).app X)).app U a✝ = (yoneda.map (α.app X)).app U a✝
case w.h.a
C : Type u_5
inst✝⁴ : Category C
D : Type u_1
inst✝³ : Category D
E : Type ?u.131136
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
⊢ yoneda.map ((sheafHom H (whiskerLeft (Functor.op G) α)).app X) = yoneda.map (α.app X)
ext U
case w.h.a.w.h.h
C : Type u_5
inst✝⁴ : Category C
D : Type u_1
inst✝³ : Category D
E : Type ?u.131136
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category 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
⊢ ((sheafYonedaHom H (whiskerLeft (Functor.op G) α)).app X).app U a✝ = (yoneda.map (α.app X)).app U a✝
case w.h.a.w.h.h
C : Type u_5
inst✝⁴ : Category C
D : Type u_1
inst✝³ : Category D
E : Type ?u.131136
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category 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
⊢ (yoneda.map ((sheafHom H (whiskerLeft (Functor.op G) α)).app X)).app U a✝ = (yoneda.map (α.app X)).app U a✝
erw [yoneda.image_preimage ((H.sheafYonedaHom (whiskerLeft G.op α)).app X)]
case w.h.a.w.h.h
C : Type u_5
inst✝⁴ : Category C
D : Type u_1
inst✝³ : Category D
E : Type ?u.131136
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category 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
⊢ (yoneda.map (α.app X)).app U a✝ = ((sheafYonedaHom H (whiskerLeft (Functor.op G) α)).app X).app U a✝
case w.h.a.w.h.h
C : Type u_5
inst✝⁴ : Category C
D : Type u_1
inst✝³ : Category D
E : Type ?u.131136
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category 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
⊢ ((sheafYonedaHom H (whiskerLeft (Functor.op G) α)).app X).app U a✝ = (yoneda.map (α.app X)).app U a✝
symm
case w.h.a.w.h.h
C : Type u_5
inst✝⁴ : Category C
D : Type u_1
inst✝³ : Category D
E : Type ?u.131136
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category 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 := (yoneda.map (α.app X)).app U a✝;
    this) =
    ((sheafYonedaHom H (whiskerLeft (Functor.op G) α)).app X).app U a✝
case w.h.a.w.h.h
C : Type u_5
inst✝⁴ : Category C
D : Type u_1
inst✝³ : Category D
E : Type ?u.131136
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category 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
⊢ (yoneda.map (α.app X)).app U a✝ = ((sheafYonedaHom H (whiskerLeft (Functor.op G) α)).app X).app U a✝
change (show (ℱ'.val ⋙ coyoneda.obj (op (unop U))).obj (op (unop X)) from _) = _
case w.h.a.w.h.h.hx
C : Type u_5
inst✝⁴ : Category C
D : Type u_1
inst✝³ : Category D
E : Type ?u.131136
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category 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 (Functor.op G) α) U.unop) a✝)

case w.h.a.w.h.h.h
C : Type u_5
inst✝⁴ : Category C
D : Type u_1
inst✝³ : Category D
E : Type ?u.131136
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category 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 (Functor.op G) α) U.unop) a✝)
    (let_fun this := (yoneda.map (α.app X)).app U a✝;
    this)
case w.h.a.w.h.h
C : Type u_5
inst✝⁴ : Category C
D : Type u_1
inst✝³ : Category D
E : Type ?u.131136
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category 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 := (yoneda.map (α.app X)).app U a✝;
    this) =
    ((sheafYonedaHom H (whiskerLeft (Functor.op G) α)).app X).app U a✝
apply sheaf_eq_amalgamation ℱ' (H.is_cover _)
case w.h.a.w.h.h.h
C : Type u_5
inst✝⁴ : Category C
D : Type u_1
inst✝³ : Category D
E : Type ?u.131136
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category 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 U.unop.op).map f.op
      (let_fun this := (yoneda.map (α.app X)).app U a✝;
      this) =
    pushforwardFamily (homOver (whiskerLeft (Functor.op G) α) U.unop) a✝ f hf
case w.h.a.w.h.h.h
C : Type u_5
inst✝⁴ : Category C
D : Type u_1
inst✝³ : Category D
E : Type ?u.131136
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category 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 (Functor.op G) α) U.unop) a✝)
    (let_fun this := (yoneda.map (α.app X)).app U a✝;
    this)
intro Y f hf
case w.h.a.w.h.h.h
C : Type u_5
inst✝⁴ : Category C
D : Type u_1
inst✝³ : Category D
E : Type ?u.131136
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category 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 U.unop.op).map ((Nonempty.some hf).lift ≫ (Nonempty.some hf).map).op
      (let_fun this := (yoneda.map (α.app X)).app U a✝;
      this) =
    pushforwardFamily (homOver (whiskerLeft (Functor.op G) α) U.unop) a✝ f hf
case w.h.a.w.h.h.h
C : Type u_5
inst✝⁴ : Category C
D : Type u_1
inst✝³ : Category D
E : Type ?u.131136
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category 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 U.unop.op).map f.op
      (let_fun this := (yoneda.map (α.app X)).app U a✝;
      this) =
    pushforwardFamily (homOver (whiskerLeft (Functor.op G) α) U.unop) a✝ f hf
conv_lhs => rw [← hf.some.fac]
case w.h.a.w.h.h.h
C : Type u_5
inst✝⁴ : Category C
D : Type u_1
inst✝³ : Category D
E : Type ?u.131136
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category 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✝ ≫ α.app X) ≫ ℱ'.val.map ((Nonempty.some hf).map.op ≫ (Nonempty.some hf).lift.op) =
    ((a✝ ≫ ℱ.map (Nonempty.some hf).map.op) ≫ α.app (G.obj (Nonempty.some hf).1).op) ≫
      ℱ'.val.map (Nonempty.some hf).lift.op
case w.h.a.w.h.h.h
C : Type u_5
inst✝⁴ : Category C
D : Type u_1
inst✝³ : Category D
E : Type ?u.131136
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category 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 U.unop.op).map ((Nonempty.some hf).lift ≫ (Nonempty.some hf).map).op
      (let_fun this := (yoneda.map (α.app X)).app U a✝;
      this) =
    pushforwardFamily (homOver (whiskerLeft (Functor.op G) α) U.unop) a✝ f hf
dsimp
no goals
case w.h.a.w.h.h.h
C : Type u_5
inst✝⁴ : Category C
D : Type u_1
inst✝³ : Category D
E : Type ?u.131136
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category 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✝ ≫ α.app X) ≫ ℱ'.val.map ((Nonempty.some hf).map.op ≫ (Nonempty.some hf).lift.op) =
    ((a✝ ≫ ℱ.map (Nonempty.some hf).map.op) ≫ α.app (G.obj (Nonempty.some hf).1).op) ≫
      ℱ'.val.map (Nonempty.some hf).lift.op
simp
no goals
case w.h.a.w.h.h.hx
C : Type u_5
inst✝⁴ : Category C
D : Type u_1
inst✝³ : Category D
E : Type ?u.131136
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category 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 (Functor.op G) α) U.unop) a✝)
exact (pushforwardFamily_compatible H _ _)