-- Mathlib/CategoryTheory/Sites/LocallySurjective.lean
lemma isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective
    {F₁ F₂ F₃ : Cᵒᵖ ⥤ A} (f₁ : F₁ ⟶ F₂) (f₂ : F₂ ⟶ F₃)
    [IsLocallySurjective J (f₁ ≫ f₂)] [IsLocallyInjective J f₂] :
    IsLocallySurjective J f₁ where
  imageSieve_mem {X} x

Proof state:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallySurjective J (f₁ ≫ f₂)
inst✝ : IsLocallyInjective J f₂
X : C
x : ToType (F₂.obj (op X))
S : Sieve X := imageSieve (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x)
T : ⦃Y : C⦄ → (f : Y ⟶ X) → S.arrows f → Sieve Y :=
  fun Y f hf =>
    equalizerSieve
      ((ConcreteCategory.hom (f₁.app (op Y))) (localPreimage (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x) f hf))
      ((ConcreteCategory.hom (F₂.map f.op)) x)
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop (op X)⦄,
    (imageSieve (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x)).arrows f →
      Sieve.pullback f (Sieve.bind S.arrows T) ∈ J Y

Tactic:
intro Y f hf

Result:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallySurjective J (f₁ ≫ f₂)
inst✝ : IsLocallyInjective J f₂
X : C
x : ToType (F₂.obj (op X))
S : Sieve X := imageSieve (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x)
T : ⦃Y : C⦄ → (f : Y ⟶ X) → S.arrows f → Sieve Y :=
  fun Y f hf =>
    equalizerSieve
      ((ConcreteCategory.hom (f₁.app (op Y))) (localPreimage (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x) f hf))
      ((ConcreteCategory.hom (F₂.map f.op)) x)
Y : C
f : Y ⟶ unop (op X)
hf : (imageSieve (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x)).arrows f
⊢ Sieve.pullback f (Sieve.bind S.arrows T) ∈ J Y

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallySurjective J (f₁ ≫ f₂)
inst✝ : IsLocallyInjective J f₂
X : C
x : ToType (F₂.obj (op X))
S : Sieve X := imageSieve (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x)
⊢ imageSieve f₁ x ∈ J X

Tactic:
let T : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (_ : S f), Sieve Y := fun Y f hf =>
  equalizerSieve (f₁.app _ (localPreimage (f₁ ≫ f₂) (f₂.app _ x) f hf)) (F₂.map f.op x)

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallySurjective J (f₁ ≫ f₂)
inst✝ : IsLocallyInjective J f₂
X : C
x : ToType (F₂.obj (op X))
S : Sieve X := imageSieve (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x)
T : ⦃Y : C⦄ → (f : Y ⟶ X) → S.arrows f → Sieve Y :=
  fun Y f hf =>
    equalizerSieve
      ((ConcreteCategory.hom (f₁.app (op Y))) (localPreimage (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x) f hf))
      ((ConcreteCategory.hom (F₂.map f.op)) x)
⊢ imageSieve f₁ x ∈ J X