-- Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean
theorem sheafHom_eq (α : ℱ ⟶ ℱ'.val) : sheafHom (whiskerLeft G.op α) = α

Proof state:
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
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_5, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj (ℱ.obj X)).obj U
⊢ (pushforwardFamily (homOver (whiskerLeft G.op α) (unop U)) a✝).IsAmalgamation
    (let_fun this := (yoneda.map (α.app X)).app U a✝;
    this)

Tactic:
intro Y f hf

Result:
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
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_5, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj (ℱ.obj X)).obj U
Y : D
f : Y ⟶ unop X
hf : (Sieve.coverByImage G (unop X)).arrows f
⊢ (ℱ'.val ⋙ coyoneda.obj (op (unop U))).map f.op
      (let_fun this := (yoneda.map (α.app X)).app U a✝;
      this) =
    pushforwardFamily (homOver (whiskerLeft G.op α) (unop U)) a✝ f hf

Proof state:
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
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_5, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj (ℱ.obj X)).obj U
⊢ ((sheafYonedaHom (whiskerLeft G.op α)).app X).app U a✝ = (yoneda.map (α.app X)).app U a✝

Tactic:
symm

Result:
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
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_5, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : 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 (whiskerLeft G.op α)).app X).app U a✝

Proof state:
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
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_5, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
⊢ (sheafHom (whiskerLeft G.op α)).app X = α.app X

Tactic:
apply yoneda.map_injective

Result:
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
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_5, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
⊢ yoneda.map ((sheafHom (whiskerLeft G.op α)).app X) = yoneda.map (α.app X)

Proof state:
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
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_5, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj (ℱ.obj X)).obj U
⊢ (pushforwardFamily (homOver (whiskerLeft G.op α) (unop U)) a✝).Compatible

Tactic:
exact (pushforwardFamily_compatible _ _)

Result:
no goals

Proof state:
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
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_5, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : 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 (whiskerLeft G.op α)).app X).app U a✝

Tactic:
change (show (ℱ'.val ⋙ coyoneda.obj (op (unop U))).obj (op (unop X)) from _) = _

Result:
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
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_5, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : 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 (whiskerLeft G.op α)).app X).app U a✝

Proof state:
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
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_5, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj (ℱ.obj X)).obj U
⊢ (yoneda.map ((sheafHom (whiskerLeft G.op α)).app X)).app U a✝ = (yoneda.map (α.app X)).app U a✝

Tactic:
erw [yoneda.map_preimage]

Result:
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
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_5, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj (ℱ.obj X)).obj U
⊢ ((sheafYonedaHom (whiskerLeft G.op α)).app X).app U a✝ = (yoneda.map (α.app X)).app U a✝

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_7, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_5, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
⊢ sheafHom (whiskerLeft G.op α) = α

Tactic:
ext X

Result:
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
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_5, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
⊢ (sheafHom (whiskerLeft G.op α)).app X = α.app X

Proof state:
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
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_5, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : 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 (whiskerLeft G.op α)).app X).app U a✝

Tactic:
apply sheaf_eq_amalgamation ℱ' (G.is_cover_of_isCoverDense _ _)

Result:
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
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_5, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj (ℱ.obj X)).obj U
⊢ (pushforwardFamily (homOver (whiskerLeft G.op α) (unop U)) a✝).Compatible

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
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_5, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.val
X : Dᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj (ℱ.obj X)).obj U
⊢ (pushforwardFamily (homOver (whiskerLeft G.op α) (unop U)) a✝).IsAmalgamation
    (let_fun this := (yoneda.map (α.app X)).app U a✝;
    this)