Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝³ : Category.{v_4, u_4} A
inst✝² : IsDenseSubsite J K G
inst✝¹ : (G.sheafPushforwardContinuous A J K).IsEquivalence
inst✝ : HasWeakSheafify J A
P₁ P₂ : Dᵒᵖ ⥤ A
f : P₁ ⟶ P₂
Q : Sheaf K A
g : (sheafifyOfIsEquivalence J K G A).obj P₂ ⟶ Q
this✝ : G.IsLocallyFull K
this : G.IsCoverDense K
adj₁ : (G.sheafPushforwardContinuous A J K).asEquivalence.symm.functor ⊣
  (G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse := ⋯
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := ⋯
⊢ (adj₂.homEquiv (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₁)
        ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q))
      ((adj₁.homEquiv ((presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₁)) Q)
        ((sheafifyOfIsEquivalence J K G A).map f ≫ g)) =
    (adj₂.homEquiv (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₁)
        ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q))
      ((presheafToSheaf J A).map (G.op.whiskerLeft f) ≫ (adj₁.homEquiv ((presheafToSheaf J A).obj (G.op ⋙ P₂)) Q) g)

pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝³ : Category.{v_4, u_4} A
inst✝² : IsDenseSubsite J K G
inst✝¹ : (G.sheafPushforwardContinuous A J K).IsEquivalence
inst✝ : HasWeakSheafify J A
P₁ P₂ : Dᵒᵖ ⥤ A
f : P₁ ⟶ P₂
Q : Sheaf K A
g : (sheafifyOfIsEquivalence J K G A).obj P₂ ⟶ Q
this✝ : G.IsLocallyFull K
this : G.IsCoverDense K
adj₁ : (G.sheafPushforwardContinuous A J K).asEquivalence.symm.functor ⊣
  (G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse := ⋯
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := ⋯
⊢ (adj₂.homEquiv (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₁)
        ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q))
      ((presheafToSheaf J A).map (G.op.whiskerLeft f) ≫ (adj₁.homEquiv ((presheafToSheaf J A).obj (G.op ⋙ P₂)) Q) g) =
    G.op.whiskerLeft f ≫
      (adj₂.homEquiv (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₂)
          ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q))
        ((adj₁.homEquiv ((presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₂)) Q) g)

Tactic:
· congr 1
    apply adj₁.homEquiv_naturality_left

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝³ : Category.{v_4, u_4} A
inst✝² : IsDenseSubsite J K G
inst✝¹ : (G.sheafPushforwardContinuous A J K).IsEquivalence
inst✝ : HasWeakSheafify J A
P₁ P₂ : Dᵒᵖ ⥤ A
f : P₁ ⟶ P₂
Q : Sheaf K A
g : (sheafifyOfIsEquivalence J K G A).obj P₂ ⟶ Q
this✝ : G.IsLocallyFull K
this : G.IsCoverDense K
adj₁ : (G.sheafPushforwardContinuous A J K).asEquivalence.symm.functor ⊣
  (G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse := ⋯
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := ⋯
⊢ (adj₂.homEquiv (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₁)
        ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q))
      ((presheafToSheaf J A).map (G.op.whiskerLeft f) ≫ (adj₁.homEquiv ((presheafToSheaf J A).obj (G.op ⋙ P₂)) Q) g) =
    G.op.whiskerLeft f ≫
      (adj₂.homEquiv (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₂)
          ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q))
        ((adj₁.homEquiv ((presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₂)) Q) g)