-- Mathlib/CategoryTheory/Sites/PreservesLocallyBijective.lean
lemma isLocallySurjective_of_whisker (hH : CoverPreserving J K H)
    [H.IsCoverDense K] [IsLocallySurjective J (whiskerLeft H.op f)] : IsLocallySurjective K f where
  imageSieve_mem {X} a

Proof state:
case h.hS
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{u_6, u_1} C
inst✝⁵ : Category.{u_7, u_2} D
inst✝⁴ : Category.{u_8, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallySurjective J (whiskerLeft H.op f)
X : D
a : ToType (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
map : H.obj Z ⟶ X
fac : lift ≫ map = g
hh :
  Sieve.functorPushforward H (imageSieve (whiskerLeft H.op f) ((ConcreteCategory.hom (G.map map.op)) a)) ∈
    K (H.obj (Opposite.unop (Opposite.op Z)))
⊢ imageSieve (whiskerLeft H.op f) ((ConcreteCategory.hom (G.map map.op)) a) ≤
    Sieve.functorPullback H (Sieve.pullback map (imageSieve f a))

Tactic:
intro W q ⟨x, h⟩

Result:
case h.hS
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{u_6, u_1} C
inst✝⁵ : Category.{u_7, u_2} D
inst✝⁴ : Category.{u_8, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallySurjective J (whiskerLeft H.op f)
X : D
a : ToType (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
map : H.obj Z ⟶ X
fac : lift ≫ map = g
hh :
  Sieve.functorPushforward H (imageSieve (whiskerLeft H.op f) ((ConcreteCategory.hom (G.map map.op)) a)) ∈
    K (H.obj (Opposite.unop (Opposite.op Z)))
W : C
q : W ⟶ Z
x : ToType ((H.op ⋙ F).obj (Opposite.op W))
h :
  (ConcreteCategory.hom ((whiskerLeft H.op f).app (Opposite.op W))) x =
    (ConcreteCategory.hom ((H.op ⋙ G).map q.op)) ((ConcreteCategory.hom (G.map map.op)) a)
⊢ (Sieve.functorPullback H (Sieve.pullback map (imageSieve f a))).arrows q

Proof state:
case h
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{u_6, u_1} C
inst✝⁵ : Category.{u_7, u_2} D
inst✝⁴ : Category.{u_8, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallySurjective J (whiskerLeft H.op f)
X : D
a : ToType (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
map : H.obj Z ⟶ X
fac : lift ≫ map = g
⊢ Sieve.pullback lift (Sieve.pullback map (imageSieve f a)) ∈ K Y

Tactic:
apply K.pullback_stable

Result:
case h.hS
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{u_6, u_1} C
inst✝⁵ : Category.{u_7, u_2} D
inst✝⁴ : Category.{u_8, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallySurjective J (whiskerLeft H.op f)
X : D
a : ToType (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
map : H.obj Z ⟶ X
fac : lift ≫ map = g
⊢ Sieve.pullback map (imageSieve f a) ∈ K (H.obj Z)