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

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✝¹ : IsLocallyInjective J (f₁ ≫ f₂)
inst✝ : IsLocallySurjective J f₁
X : Cᵒᵖ
x₁ x₂ : ToType (F₂.obj X)
h : (ConcreteCategory.hom (f₂.app X)) x₁ = (ConcreteCategory.hom (f₂.app X)) x₂
⊢ equalizerSieve x₁ x₂ ∈ J (unop X)

Tactic:
let S := imageSieve f₁ x₁ ⊓ imageSieve f₁ 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✝¹ : IsLocallyInjective J (f₁ ≫ f₂)
inst✝ : IsLocallySurjective J f₁
X : Cᵒᵖ
x₁ x₂ : ToType (F₂.obj X)
h : (ConcreteCategory.hom (f₂.app X)) x₁ = (ConcreteCategory.hom (f₂.app X)) x₂
S : Sieve (unop X) := imageSieve f₁ x₁ ⊓ imageSieve f₁ x₂
⊢ equalizerSieve x₁ x₂ ∈ J (unop X)

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✝¹ : IsLocallyInjective J (f₁ ≫ f₂)
inst✝ : IsLocallySurjective J f₁
X : Cᵒᵖ
x₁ x₂ : ToType (F₂.obj X)
h : (ConcreteCategory.hom (f₂.app X)) x₁ = (ConcreteCategory.hom (f₂.app X)) x₂
S : Sieve (unop X) := imageSieve f₁ x₁ ⊓ imageSieve f₁ x₂
hS : S ∈ J (unop X)
⊢ equalizerSieve x₁ x₂ ∈ J (unop X)

Tactic:
let T : ∀ ⦃Y : C⦄ (f : Y ⟶ X.unop) (_ : S f), Sieve Y := fun Y f hf =>
  equalizerSieve (localPreimage f₁ x₁ f hf.1) (localPreimage f₁ x₂ f hf.2)

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✝¹ : IsLocallyInjective J (f₁ ≫ f₂)
inst✝ : IsLocallySurjective J f₁
X : Cᵒᵖ
x₁ x₂ : ToType (F₂.obj X)
h : (ConcreteCategory.hom (f₂.app X)) x₁ = (ConcreteCategory.hom (f₂.app X)) x₂
S : Sieve (unop X) := imageSieve f₁ x₁ ⊓ imageSieve f₁ x₂
hS : S ∈ J (unop X)
T : ⦃Y : C⦄ → (f : Y ⟶ unop X) → S.arrows f → Sieve Y :=
  fun Y f hf => equalizerSieve (localPreimage f₁ x₁ f ⋯) (localPreimage f₁ x₂ f ⋯)
⊢ equalizerSieve x₁ x₂ ∈ J (unop X)

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✝¹ : IsLocallyInjective J (f₁ ≫ f₂)
inst✝ : IsLocallySurjective J f₁
X : Cᵒᵖ
x₁ x₂ : ToType (F₂.obj X)
h : (ConcreteCategory.hom (f₂.app X)) x₁ = (ConcreteCategory.hom (f₂.app X)) x₂
S : Sieve (unop X) := imageSieve f₁ x₁ ⊓ imageSieve f₁ x₂
hS : S ∈ J (unop X)
T : ⦃Y : C⦄ → (f : Y ⟶ unop X) → S.arrows f → Sieve Y :=
  fun Y f hf => equalizerSieve (localPreimage f₁ x₁ f ⋯) (localPreimage f₁ x₂ f ⋯)
⊢ equalizerSieve x₁ x₂ ∈ J (unop X)

Tactic:
refine J.superset_covering ?_ (J.transitive hS (Sieve.bind S.1 T) ?_)

Result:
case refine_1
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✝¹ : IsLocallyInjective J (f₁ ≫ f₂)
inst✝ : IsLocallySurjective J f₁
X : Cᵒᵖ
x₁ x₂ : ToType (F₂.obj X)
h : (ConcreteCategory.hom (f₂.app X)) x₁ = (ConcreteCategory.hom (f₂.app X)) x₂
S : Sieve (unop X) := imageSieve f₁ x₁ ⊓ imageSieve f₁ x₂
hS : S ∈ J (unop X)
T : ⦃Y : C⦄ → (f : Y ⟶ unop X) → S.arrows f → Sieve Y :=
  fun Y f hf => equalizerSieve (localPreimage f₁ x₁ f ⋯) (localPreimage f₁ x₂ f ⋯)
⊢ Sieve.bind S.arrows T ≤ equalizerSieve x₁ x₂

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✝¹ : IsLocallyInjective J (f₁ ≫ f₂)
inst✝ : IsLocallySurjective J f₁
X : Cᵒᵖ
x₁ x₂ : ToType (F₂.obj X)
h : (ConcreteCategory.hom (f₂.app X)) x₁ = (ConcreteCategory.hom (f₂.app X)) x₂
S : Sieve (unop X) := imageSieve f₁ x₁ ⊓ imageSieve f₁ x₂
hS : S ∈ J (unop X)
T : ⦃Y : C⦄ → (f : Y ⟶ unop X) → S.arrows f → Sieve Y :=
  fun Y f hf => equalizerSieve (localPreimage f₁ x₁ f ⋯) (localPreimage f₁ x₂ f ⋯)
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop X⦄, S.arrows f → Sieve.pullback f (Sieve.bind S.arrows T) ∈ J Y

Proof state:
case sj
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✝¹ : IsLocallyInjective J (f₁ ≫ f₂)
inst✝ : IsLocallySurjective J f₁
X : Cᵒᵖ
x₁ x₂ : ToType (F₂.obj X)
h : (ConcreteCategory.hom (f₂.app X)) x₁ = (ConcreteCategory.hom (f₂.app X)) x₂
S : Sieve (unop X) := imageSieve f₁ x₁ ⊓ imageSieve f₁ x₂
⊢ imageSieve f₁ x₂ ∈ J (unop X)

Tactic:
apply imageSieve_mem

Result:
no goals

Proof state:
case refine_2.h
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✝¹ : IsLocallyInjective J (f₁ ≫ f₂)
inst✝ : IsLocallySurjective J f₁
X : Cᵒᵖ
x₁ x₂ : ToType (F₂.obj X)
h : (ConcreteCategory.hom (f₂.app X)) x₁ = (ConcreteCategory.hom (f₂.app X)) x₂
S : Sieve (unop X) := imageSieve f₁ x₁ ⊓ imageSieve f₁ x₂
hS : S ∈ J (unop X)
T : ⦃Y : C⦄ → (f : Y ⟶ unop X) → S.arrows f → Sieve Y :=
  fun Y f hf => equalizerSieve (localPreimage f₁ x₁ f ⋯) (localPreimage f₁ x₂ f ⋯)
Y : C
f : Y ⟶ unop X
hf : S.arrows f
⊢ (ConcreteCategory.hom (f₁.app (op Y) ≫ f₂.app (op Y))) (localPreimage f₁ x₁ f ⋯) =
    (ConcreteCategory.hom (f₁.app (op Y) ≫ f₂.app (op Y))) (localPreimage f₁ x₂ f ⋯)

Tactic:
rw [ConcreteCategory.comp_apply, ConcreteCategory.comp_apply, app_localPreimage,
  app_localPreimage, NatTrans.naturality_apply, NatTrans.naturality_apply, h]

Result:
no goals