-- 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
⊢ Sieve.pullback map (imageSieve f a) ∈ K (H.obj Z)

Tactic:
have hh := hH.cover_preserve <| imageSieve_mem J (whiskerLeft H.op f) (G.map map.op a)

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)))
⊢ Sieve.pullback map (imageSieve f a) ∈ K (H.obj Z)

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⦄ ⦃f_1 : Y ⟶ X⦄, (Sieve.coverByImage H X).arrows f_1 → Sieve.pullback f_1 (imageSieve f a) ∈ K Y

Tactic:
intro Y g ⟨⟨Z, lift, map, fac⟩⟩

Result:
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 g (imageSieve f a) ∈ K Y

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 g (imageSieve f a) ∈ K Y

Tactic:
rw [← fac, Sieve.pullback_comp]

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

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)))
⊢ Sieve.functorPushforward H (Sieve.functorPullback H (Sieve.pullback map (imageSieve f a))) ∈ K (H.obj Z)

Tactic:
refine K.superset_covering (Sieve.functorPushforward_monotone H _ ?_) hh

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)))
⊢ imageSieve (whiskerLeft H.op f) ((ConcreteCategory.hom (G.map map.op)) a) ≤
    Sieve.functorPullback H (Sieve.pullback map (imageSieve f a))