-- Mathlib/CategoryTheory/Sites/Equivalence.lean
lemma PreservesSheafification.transport
    [Functor.IsContinuous.{v₄} G K J] [Functor.IsContinuous.{v₃} G K J]
    [(G.sheafPushforwardContinuous B K J).EssSurj]
    [(G.sheafPushforwardContinuous A K J).EssSurj]
    [K.PreservesSheafification F] : J.PreservesSheafification F where
  le P Q f hf

Proof state:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁸ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁷ : Category.{v₄, u₄} B
F : A ⥤ B
inst✝⁶ : G.IsCoverDense J
inst✝⁵ : G.Full
inst✝⁴ : G.IsContinuous K J
inst✝³ : G.IsContinuous K J
inst✝² : (G.sheafPushforwardContinuous B K J).EssSurj
inst✝¹ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝ : K.PreservesSheafification F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
hf : K.W (whiskerLeft G.op f)
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f

Tactic:
have := K.W_of_preservesSheafification F (whiskerLeft G.op f) hf

Result:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁸ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁷ : Category.{v₄, u₄} B
F : A ⥤ B
inst✝⁶ : G.IsCoverDense J
inst✝⁵ : G.Full
inst✝⁴ : G.IsContinuous K J
inst✝³ : G.IsContinuous K J
inst✝² : (G.sheafPushforwardContinuous B K J).EssSurj
inst✝¹ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝ : K.PreservesSheafification F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
hf : K.W (whiskerLeft G.op f)
this : K.W (whiskerRight (whiskerLeft G.op f) F)
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f

Proof state:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁸ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁷ : Category.{v₄, u₄} B
F : A ⥤ B
inst✝⁶ : G.IsCoverDense J
inst✝⁵ : G.Full
inst✝⁴ : G.IsContinuous K J
inst✝³ : G.IsContinuous K J
inst✝² : (G.sheafPushforwardContinuous B K J).EssSurj
inst✝¹ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝ : K.PreservesSheafification F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
hf : K.W (whiskerLeft G.op f)
this : K.W (whiskerRight (whiskerLeft G.op f) F)
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f

Tactic:
rwa [whiskerRight_left,
  K.W_whiskerLeft_iff (G := G) (J := J) (f := whiskerRight f F)] at this

Result:
no goals

Proof state:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁸ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁷ : Category.{v₄, u₄} B
F : A ⥤ B
inst✝⁶ : G.IsCoverDense J
inst✝⁵ : G.Full
inst✝⁴ : G.IsContinuous K J
inst✝³ : G.IsContinuous K J
inst✝² : (G.sheafPushforwardContinuous B K J).EssSurj
inst✝¹ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝ : K.PreservesSheafification F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
hf : J.W f
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f

Tactic:
rw [← J.W_whiskerLeft_iff (G := G) (K := K)] at hf

Result:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁸ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁷ : Category.{v₄, u₄} B
F : A ⥤ B
inst✝⁶ : G.IsCoverDense J
inst✝⁵ : G.Full
inst✝⁴ : G.IsContinuous K J
inst✝³ : G.IsContinuous K J
inst✝² : (G.sheafPushforwardContinuous B K J).EssSurj
inst✝¹ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝ : K.PreservesSheafification F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
hf : K.W (whiskerLeft G.op f)
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f