-- 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)))
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

Tactic:
simp only [Sieve.functorPullback_apply, Presieve.functorPullback_mem, Sieve.pullback_apply]

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)
⊢ (imageSieve f a).arrows (H.map q ≫ map)

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)))
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)
⊢ (imageSieve f a).arrows (H.map q ≫ map)

Tactic:
exact ⟨x, by simpa using h⟩

Result:
no goals

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

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

Proof state:
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)
⊢ (ConcreteCategory.hom (f.app (Opposite.op (H.obj W)))) x = (ConcreteCategory.hom (G.map (H.map q ≫ map).op)) a

Tactic:
simpa using h

Result:
no goals

Proof state:
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))
⊢ imageSieve f a ∈ K X

Tactic:
apply K.transitive (H.is_cover_of_isCoverDense K X)

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