-- Mathlib/CategoryTheory/Sites/Coherent/ReflectsPrecoherent.lean
lemma Functor.reflects_precoherent : Precoherent C where
  pullback {B₁ B₂} f α _ X₁ π₁ _

Proof state:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{?u.234, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.EffectivelyEnough
inst✝² : Precoherent D
inst✝¹ : F.Full
inst✝ : F.Faithful
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
x✝¹ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
x✝ : EffectiveEpiFamily X₁ π₁
⊢ ∃ β, ∃ (_ : Finite β), ∃ X₂ π₂, EffectiveEpiFamily X₂ π₂ ∧ ∃ i ι, ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f

Tactic:
obtain ⟨β, _, Y₂, τ₂, H, i, ι, hh⟩ := Precoherent.pullback (F.map f) _ _
  (fun a ↦ F.map (π₁ a)) inferInstance

Result:
case intro.intro.intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{?u.234, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.EffectivelyEnough
inst✝² : Precoherent D
inst✝¹ : F.Full
inst✝ : F.Faithful
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
x✝¹ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
x✝ : EffectiveEpiFamily X₁ π₁
β : Type
w✝ : Finite β
Y₂ : β → D
τ₂ : (b : β) → Y₂ b ⟶ F.obj B₂
H : EffectiveEpiFamily Y₂ τ₂
i : β → α
ι : (b : β) → Y₂ b ⟶ F.obj (X₁ (i b))
hh : ∀ (b : β), ι b ≫ F.map (π₁ (i b)) = τ₂ b ≫ F.map f
⊢ ∃ β, ∃ (_ : Finite β), ∃ X₂ π₂, EffectiveEpiFamily X₂ π₂ ∧ ∃ i ι, ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f

Proof state:
case intro.intro.intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{?u.234, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.EffectivelyEnough
inst✝² : Precoherent D
inst✝¹ : F.Full
inst✝ : F.Faithful
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
x✝¹ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
x✝ : EffectiveEpiFamily X₁ π₁
β : Type
w✝ : Finite β
Y₂ : β → D
τ₂ : (b : β) → Y₂ b ⟶ F.obj B₂
H : EffectiveEpiFamily Y₂ τ₂
i : β → α
ι : (b : β) → Y₂ b ⟶ F.obj (X₁ (i b))
hh : ∀ (b : β), ι b ≫ F.map (π₁ (i b)) = τ₂ b ≫ F.map f
⊢ ∃ β, ∃ (_ : Finite β), ∃ X₂ π₂, EffectiveEpiFamily X₂ π₂ ∧ ∃ i ι, ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f

Tactic:
refine ⟨β, inferInstance, _, fun b ↦ F.preimage (F.effectiveEpiOver (Y₂ b) ≫ τ₂ b),
  F.finite_effectiveEpiFamily_of_map _ _ ?_,
    ⟨i, fun b ↦ F.preimage (F.effectiveEpiOver (Y₂ b) ≫ ι b), ?_⟩⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.refine_1
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{?u.234, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.EffectivelyEnough
inst✝² : Precoherent D
inst✝¹ : F.Full
inst✝ : F.Faithful
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
x✝¹ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
x✝ : EffectiveEpiFamily X₁ π₁
β : Type
w✝ : Finite β
Y₂ : β → D
τ₂ : (b : β) → Y₂ b ⟶ F.obj B₂
H : EffectiveEpiFamily Y₂ τ₂
i : β → α
ι : (b : β) → Y₂ b ⟶ F.obj (X₁ (i b))
hh : ∀ (b : β), ι b ≫ F.map (π₁ (i b)) = τ₂ b ≫ F.map f
⊢ EffectiveEpiFamily (fun a => F.obj ⋯.some.p) fun a => F.map (F.preimage (F.effectiveEpiOver (Y₂ a) ≫ τ₂ a))

case intro.intro.intro.intro.intro.intro.intro.refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{?u.234, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.EffectivelyEnough
inst✝² : Precoherent D
inst✝¹ : F.Full
inst✝ : F.Faithful
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
x✝¹ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
x✝ : EffectiveEpiFamily X₁ π₁
β : Type
w✝ : Finite β
Y₂ : β → D
τ₂ : (b : β) → Y₂ b ⟶ F.obj B₂
H : EffectiveEpiFamily Y₂ τ₂
i : β → α
ι : (b : β) → Y₂ b ⟶ F.obj (X₁ (i b))
hh : ∀ (b : β), ι b ≫ F.map (π₁ (i b)) = τ₂ b ≫ F.map f
⊢ ∀ (b : β),
    (fun b => F.preimage (F.effectiveEpiOver (Y₂ b) ≫ ι b)) b ≫ π₁ (i b) =
      (fun b => F.preimage (F.effectiveEpiOver (Y₂ b) ≫ τ₂ b)) b ≫ f