-- 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.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
⊢ α.app X ≫ ℱ'.val.map (Nonempty.some hf).map.op = ℱ.map (Nonempty.some hf).map.op ≫ α.app (op (Nonempty.some hf).1)

Tactic:
have := naturality_apply (G := G) (ℱ := ℱ ⋙ coyoneda.obj (op <| (G.op ⋙ ℱ).obj X))
  (ℱ' := ⟨_, Presheaf.isSheaf_comp_of_isSheaf K ℱ'.val
    (coyoneda.obj (op ((G.op ⋙ ℱ).obj X))) ℱ'.cond⟩)
  (whiskerRight α (coyoneda.obj _)) hf.some.map (𝟙 _)

Result:
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)

Proof state:
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
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✝).Compatible

Tactic:
exact (pushforwardFamily_compatible _ _)

Result:
no goals

Proof state:
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)

Tactic:
congr 1

Result:
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
⊢ α.app X ≫ ℱ'.val.map (Nonempty.some hf).map.op = ℱ.map (Nonempty.some hf).map.op ≫ α.app (op (Nonempty.some hf).1)

Proof state:
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
⊢ whiskerLeft G.op (sheafHom α) = α

Tactic:
ext X

Result:
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
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ᵒᵖ
⊢ (whiskerLeft G.op (sheafHom α)).app X = α.app X

Proof state:
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)

Tactic:
simp only [Category.assoc]

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
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ᵒᵖ
⊢ (whiskerLeft G.op (sheafHom α)).app X = α.app X

Tactic:
apply yoneda.map_injective

Result:
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)

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 f.op
      (let_fun this := (yoneda.map (α.app X)).app U a✝;
      this) =
    pushforwardFamily (homOver α (unop U)) a✝ f hf

Tactic:
conv_lhs => rw [← hf.some.fac]

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 ((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