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

Proof state:
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
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
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
f : Y ⟶ G.obj (unop X)
hf : (Sieve.coverByImage G (G.obj (unop X))).arrows f
⊢ ((a✝ ≫ α.app X) ≫ ℱ'.val.map (Nonempty.some hf).map.op) ≫ ℱ'.val.map (Nonempty.some hf).lift.op =
    (sheafOver ℱ' (unop U)).val.map (Nonempty.some hf).lift.op
      ((a✝ ≫ ℱ.map (Nonempty.some hf).map.op) ≫ α.app (op (Nonempty.some hf).1))

Tactic:
congr 1

Result:
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
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
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
f : Y ⟶ G.obj (unop X)
hf : (Sieve.coverByImage G (G.obj (unop X))).arrows f
⊢ (a✝ ≫ α.app X) ≫ ℱ'.val.map (Nonempty.some hf).map.op =
    (a✝ ≫ ℱ.map (Nonempty.some hf).map.op) ≫ α.app (op (Nonempty.some hf).1)

Proof state:
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
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
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
⊢ (yoneda.map (α.app X)).app U a✝ = ((sheafYonedaHom α).app (G.op.obj X)).app U a✝

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

Result:
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
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
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
⊢ (let_fun this := (yoneda.map (α.app X)).app U a✝;
    this) =
    ((sheafYonedaHom α).app (G.op.obj X)).app U a✝

Proof state:
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
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
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
f : Y ⟶ G.obj (unop X)
hf : (Sieve.coverByImage G (G.obj (unop X))).arrows f
this :
  { val := ℱ'.val ⋙ coyoneda.obj (op ((G.op ⋙ ℱ).obj X)), cond := ⋯ }.val.map (Nonempty.some hf).map.op
      ((whiskerRight α (coyoneda.obj (op ((G.op ⋙ ℱ).obj X)))).app (op (unop X)) (𝟙 (unop (op ((G.op ⋙ ℱ).obj X))))) =
    (whiskerRight α (coyoneda.obj (op ((G.op ⋙ ℱ).obj X)))).app (op (Nonempty.some hf).obj)
      ((ℱ ⋙ coyoneda.obj (op ((G.op ⋙ ℱ).obj X))).map (Nonempty.some hf).map.op (𝟙 (unop (op ((G.op ⋙ ℱ).obj X)))))
⊢ α.app X ≫ ℱ'.val.map (Nonempty.some hf).map.op = ℱ.map (Nonempty.some hf).map.op ≫ α.app (op (Nonempty.some hf).1)

Tactic:
simpa using this

Result:
no goals

Proof state:
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
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
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
⊢ ((sheafYonedaHom α).app (G.op.obj 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_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, 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
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
⊢ (yoneda.map (α.app X)).app U a✝ = ((sheafYonedaHom α).app (G.op.obj X)).app U a✝

Proof state:
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
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
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
⊢ (pushforwardFamily (homOver α (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_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, 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
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
f : Y ⟶ G.obj (unop X)
hf : (Sieve.coverByImage G (G.obj (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 α (unop U)) a✝ f hf

Proof state:
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
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
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
⊢ yoneda.map ((whiskerLeft G.op (sheafHom α)).app X) = yoneda.map (α.app X)

Tactic:
ext U

Result:
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
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
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
⊢ (yoneda.map ((whiskerLeft G.op (sheafHom α)).app X)).app U a✝ = (yoneda.map (α.app X)).app U a✝

Proof state:
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
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
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
f : Y ⟶ G.obj (unop X)
hf : (Sieve.coverByImage G (G.obj (unop X))).arrows f
⊢ (ℱ'.val ⋙ coyoneda.obj (op (unop U))).map ((Nonempty.some hf).lift ≫ (Nonempty.some hf).map).op
      (let_fun this := (yoneda.map (α.app X)).app U a✝;
      this) =
    pushforwardFamily (homOver α (unop U)) a✝ f hf

Tactic:
simp only [pushforwardFamily, Functor.comp_map, yoneda_map_app, coyoneda_obj_map, op_comp,
  FunctorToTypes.map_comp_apply, homOver_app, ← Category.assoc]

Result:
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
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
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
f : Y ⟶ G.obj (unop X)
hf : (Sieve.coverByImage G (G.obj (unop X))).arrows f
⊢ ((a✝ ≫ α.app X) ≫ ℱ'.val.map (Nonempty.some hf).map.op) ≫ ℱ'.val.map (Nonempty.some hf).lift.op =
    (sheafOver ℱ' (unop U)).val.map (Nonempty.some hf).lift.op
      ((a✝ ≫ ℱ.map (Nonempty.some hf).map.op) ≫ α.app (op (Nonempty.some hf).1))