-- Mathlib/CategoryTheory/Sites/CoverLifting.lean
lemma toSheafify_pullbackSheafificationCompatibility (F : Dᵒᵖ ⥤ A) :
    toSheafify J (G.op ⋙ F) ≫
    ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).val =
    whiskerLeft _ (toSheafify K _)

Proof state:
case a.a
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝⁵ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁴ : G.IsCocontinuous J K
inst✝³ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝² : G.IsContinuous J K
inst✝¹ : HasWeakSheafify J A
inst✝ : HasWeakSheafify K A
F : Dᵒᵖ ⥤ A
adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A
adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := sheafificationAdjunction K A
adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := G.sheafAdjunctionCocontinuous A J K
eq :
  adj₁.unit.app F ≫
      G.op.ran.map (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F)) ≫
        G.op.ran.map ((sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) =
    adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))
⊢ (adj₁.homEquiv ((𝟭 (Dᵒᵖ ⥤ A)).obj F)
          ((G.sheafPushforwardContinuous A J K).obj ((presheafToSheaf K A).obj F)).val).symm
      (adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))) =
    (adj₁.homEquiv ((𝟭 (Dᵒᵖ ⥤ A)).obj F)
          ((G.sheafPushforwardContinuous A J K).obj ((presheafToSheaf K A).obj F)).val).symm
      ((adj₁.homEquiv F ((sheafToPresheaf J A).obj ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F)))
        (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F)))

Tactic:
simp only [Adjunction.homEquiv_counit, map_comp, Category.assoc,
  Adjunction.homEquiv_unit, Adjunction.unit_naturality]

Result:
case a.a
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝⁵ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁴ : G.IsCocontinuous J K
inst✝³ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝² : G.IsContinuous J K
inst✝¹ : HasWeakSheafify J A
inst✝ : HasWeakSheafify K A
F : Dᵒᵖ ⥤ A
adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A
adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := sheafificationAdjunction K A
adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := G.sheafAdjunctionCocontinuous A J K
eq :
  adj₁.unit.app F ≫
      G.op.ran.map (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F)) ≫
        G.op.ran.map ((sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) =
    adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))
⊢ ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F) ≫
      ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map
          ((sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))) ≫
        adj₁.counit.app ((G.sheafPushforwardContinuous A J K).obj ((presheafToSheaf K A).obj F)).val =
    ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F) ≫
      ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₁.unit.app ((presheafToSheaf K A ⋙ sheafToPresheaf K A).obj F)) ≫
        adj₁.counit.app ((G.sheafPushforwardContinuous A J K).obj ((presheafToSheaf K A).obj F)).val

Proof state:
case a.a
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝⁵ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁴ : G.IsCocontinuous J K
inst✝³ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝² : G.IsContinuous J K
inst✝¹ : HasWeakSheafify J A
inst✝ : HasWeakSheafify K A
F : Dᵒᵖ ⥤ A
adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A
adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := sheafificationAdjunction K A
adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := G.sheafAdjunctionCocontinuous A J K
eq :
  adj₁.unit.app F ≫
      G.op.ran.map (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F)) ≫
        G.op.ran.map ((sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) =
    adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))
⊢ ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F) ≫
      ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map
          ((sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))) ≫
        adj₁.counit.app ((G.sheafPushforwardContinuous A J K).obj ((presheafToSheaf K A).obj F)).val =
    ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F) ≫
      ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₁.unit.app ((presheafToSheaf K A ⋙ sheafToPresheaf K A).obj F)) ≫
        adj₁.counit.app ((G.sheafPushforwardContinuous A J K).obj ((presheafToSheaf K A).obj F)).val

Tactic:
congr 3

Result:
case a.a.e_a.e_a.e_a
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝⁵ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁴ : G.IsCocontinuous J K
inst✝³ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝² : G.IsContinuous J K
inst✝¹ : HasWeakSheafify J A
inst✝ : HasWeakSheafify K A
F : Dᵒᵖ ⥤ A
adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A
adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := sheafificationAdjunction K A
adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := G.sheafAdjunctionCocontinuous A J K
eq :
  adj₁.unit.app F ≫
      G.op.ran.map (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F)) ≫
        G.op.ran.map ((sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) =
    adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))
⊢ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F)) =
    adj₁.unit.app ((presheafToSheaf K A ⋙ sheafToPresheaf K A).obj F)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝⁵ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁴ : G.IsCocontinuous J K
inst✝³ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝² : G.IsContinuous J K
inst✝¹ : HasWeakSheafify J A
inst✝ : HasWeakSheafify K A
F : Dᵒᵖ ⥤ A
adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A
⊢ toSheafify J (G.op ⋙ F) ≫ ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).val =
    whiskerLeft G.op (toSheafify K F)

Tactic:
let adj₂ := sheafificationAdjunction J A

Result:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝⁵ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁴ : G.IsCocontinuous J K
inst✝³ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝² : G.IsContinuous J K
inst✝¹ : HasWeakSheafify J A
inst✝ : HasWeakSheafify K A
F : Dᵒᵖ ⥤ A
adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A
⊢ toSheafify J (G.op ⋙ F) ≫ ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).val =
    whiskerLeft G.op (toSheafify K F)