awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
f : F ⟶ G
inst_3 : PreservesFiniteProducts F
inst_4 : PreservesFiniteProducts G
U : C
y : ToType (FC := TypeCat.Fun) (G.obj (op U))
h : Presheaf.imageSieve (FA := TypeCat.Fun) f y ∈ (coherentTopology C : (a : C) → Set (Sieve a)) U
⊢ Presheaf.imageSieve (FA := TypeCat.Fun) f y ∈ (regularTopology C : (a : C) → Set (Sieve a)) U
have h₁ : ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ U),
  EffectiveEpiFamily Y π ∧ ∀ (a : α), (Presheaf.imageSieve (FA := TypeCat.Fun) f y).arrows (π a)
Tactic: rw [coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
f : F ⟶ G
inst_3 : PreservesFiniteProducts F
inst_4 : PreservesFiniteProducts G
U : C
y : ToType (FC := TypeCat.Fun) (G.obj (op U))
h :
  ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ U),
    EffectiveEpiFamily Y π ∧ ∀ (a : α), (Presheaf.imageSieve (FA := TypeCat.Fun) f y).arrows (π a)
⊢ Presheaf.imageSieve (FA := TypeCat.Fun) f y ∈ (regularTopology C : (a : C) → Set (Sieve a)) U
have obtain : ∀ (α : Type),
  Finite α →
    ∀ (Z : α → C) (π : (a : α) → Z a ⟶ U) (h : EffectiveEpiFamily Z π)
      (h' : ∀ (a : α), (Presheaf.imageSieve (FA := TypeCat.Fun) f y).arrows (π a)),
      Presheaf.imageSieve (FA := TypeCat.Fun) f y ∈ (regularTopology C : (a : C) → Set (Sieve a)) U
Tactic: obtain ⟨α, _, Z, π, h, h'⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
f : F ⟶ G
inst_3 : PreservesFiniteProducts F
inst_4 : PreservesFiniteProducts G
U : C
y : ToType (FC := TypeCat.Fun) (G.obj (op U))
α : Type
w : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve (FA := TypeCat.Fun) f y).arrows (π a)
⊢ Presheaf.imageSieve (FA := TypeCat.Fun) f y ∈ (regularTopology C : (a : C) → Set (Sieve a)) U
have rw : ∃ (Y : C) (π : Y ⟶ U), EffectiveEpi π ∧ (Presheaf.imageSieve (FA := TypeCat.Fun) f y).arrows π
Tactic: rw [mem_sieves_iff_hasEffectiveEpi]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
f : F ⟶ G
inst_3 : PreservesFiniteProducts F
inst_4 : PreservesFiniteProducts G
U : C
y : ToType (FC := TypeCat.Fun) (G.obj (op U))
α : Type
w : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve (FA := TypeCat.Fun) f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) :=
  fun (a : α) ↦
    Exists.choose (p := fun (t : ToType (FC := TypeCat.Fun) (F.obj (op (Z a)))) ↦
      Eq (α := (fun (X : Type w) ↦ X) (G.obj (op (Z a))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (Z a))) :
              (a_1 : (fun (X : Type w) ↦ X) (F.obj (op (Z a)))) → (fun (X : Type w) ↦ X) (G.obj (op (Z a))))
            t :
          (fun (X : Type w) ↦ X) (G.obj (op (Z a))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (π a).op) :
              (a_1 : (fun (X : Type w) ↦ X) (G.obj (op U))) → (fun (X : Type w) ↦ X) (G.obj (op (Z a))))
            y :
          (fun (X : Type w) ↦ X) (G.obj (op (Z a)))))
      ⋯
x_1 : Fintype α := Fintype.ofFinite α
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (sigmaObj.{0, v_1, u_1} Z)) :=
  Iso.symm (Types.productIso fun (a : α) ↦ F.obj (op (Z a))) ≪≫
    Iso.symm (PreservesProduct.iso F fun (a : α) ↦ op (Z a)) ≪≫ F.mapIso (Iso.symm (opCoproductIsoProduct Z))
⊢ ∃ (Y : C) (π : Y ⟶ U), EffectiveEpi π ∧ (Presheaf.imageSieve (FA := TypeCat.Fun) f y).arrows π
have refine : Eq (α := (fun (X : Type w) ↦ X) (G.obj (op (sigmaObj.{0, v_1, u_1} Z))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (sigmaObj.{0, v_1, u_1} Z))) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op (∐ Z)))) → (fun (X : Type w) ↦ X) (G.obj (op (∐ Z))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) i'.hom :
            (a : (fun (X : Type w) ↦ X) ((a : α) → F.obj (op (Z a)))) → (fun (X : Type w) ↦ X) (F.obj (op (∐ Z))))
          x :
        (fun (X : Type w) ↦ X) (F.obj (op (sigmaObj.{0, v_1, u_1} Z)))) :
    (fun (X : Type w) ↦ X) (G.obj (op (sigmaObj.{0, v_1, u_1} Z))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (Quiver.Hom.op (Sigma.desc π))) :
        (a : (fun (X : Type w) ↦ X) (G.obj (op U))) → (fun (X : Type w) ↦ X) (G.obj (op (∐ Z))))
      y :
    (fun (X : Type w) ↦ X) (G.obj (op (sigmaObj.{0, v_1, u_1} Z))))
Tactic: refine ⟨∐ Z, Sigma.desc π, inferInstance, i'.hom x, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
f : F ⟶ G
inst_3 : PreservesFiniteProducts F
inst_4 : PreservesFiniteProducts G
U : C
y : ToType (FC := TypeCat.Fun) (G.obj (op U))
α : Type
w : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve (FA := TypeCat.Fun) f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) :=
  fun (a : α) ↦
    Exists.choose (p := fun (t : ToType (FC := TypeCat.Fun) (F.obj (op (Z a)))) ↦
      Eq (α := (fun (X : Type w) ↦ X) (G.obj (op (Z a))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (Z a))) :
              (a_1 : (fun (X : Type w) ↦ X) (F.obj (op (Z a)))) → (fun (X : Type w) ↦ X) (G.obj (op (Z a))))
            t :
          (fun (X : Type w) ↦ X) (G.obj (op (Z a))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (π a).op) :
              (a_1 : (fun (X : Type w) ↦ X) (G.obj (op U))) → (fun (X : Type w) ↦ X) (G.obj (op (Z a))))
            y :
          (fun (X : Type w) ↦ X) (G.obj (op (Z a)))))
      ⋯
x_1 : Fintype α := Fintype.ofFinite α
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (sigmaObj.{0, v_1, u_1} Z)) :=
  Iso.symm (Types.productIso fun (a : α) ↦ F.obj (op (Z a))) ≪≫
    Iso.symm (PreservesProduct.iso F fun (a : α) ↦ op (Z a)) ≪≫ F.mapIso (Iso.symm (opCoproductIsoProduct Z))
⊢ Eq (α := (fun (X : Type w) ↦ X) (G.obj (op (sigmaObj.{0, v_1, u_1} Z))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (sigmaObj.{0, v_1, u_1} Z))) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op (∐ Z)))) → (fun (X : Type w) ↦ X) (G.obj (op (∐ Z))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) i'.hom :
              (a : (fun (X : Type w) ↦ X) ((a : α) → F.obj (op (Z a)))) → (fun (X : Type w) ↦ X) (F.obj (op (∐ Z))))
            x :
          (fun (X : Type w) ↦ X) (F.obj (op (sigmaObj.{0, v_1, u_1} Z)))) :
      (fun (X : Type w) ↦ X) (G.obj (op (sigmaObj.{0, v_1, u_1} Z))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (Quiver.Hom.op (Sigma.desc π))) :
          (a : (fun (X : Type w) ↦ X) (G.obj (op U))) → (fun (X : Type w) ↦ X) (G.obj (op (∐ Z))))
        y :
      (fun (X : Type w) ↦ X) (G.obj (op (sigmaObj.{0, v_1, u_1} Z))))
have this : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
Tactic: have := preservesLimitsOfShape_of_equiv (Discrete.opposite α).symm G
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
inst_4 : Preregular.{v_1, u_1} C
inst_5 : FinitaryPreExtensive.{v_1, u_1} C
inst_6 : PreservesFiniteProducts F
inst_7 : PreservesFiniteProducts G
inst_8 : PreservesFiniteProducts.{v_2, w, u_2, w + 1} (forget D (FC := FD) (CC := CD))
⊢ Presheaf.IsLocallySurjective (coherentTopology C) (FA := FD) (CA := CD) f ↔
    Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f
have mp : Presheaf.IsLocallySurjective (coherentTopology C) (FA := FD) (CA := CD) f →
  Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
inst_4 : Preregular.{v_1, u_1} C
inst_5 : FinitaryPreExtensive.{v_1, u_1} C
inst_6 : PreservesFiniteProducts F
inst_7 : PreservesFiniteProducts G
inst_8 : PreservesFiniteProducts.{v_2, w, u_2, w + 1} (forget D (FC := FD) (CC := CD))
mp :
  Presheaf.IsLocallySurjective (coherentTopology C) (FA := FD) (CA := CD) f →
    Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f
⊢ Presheaf.IsLocallySurjective (coherentTopology C) (FA := FD) (CA := CD) f ↔
    Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f
have mpr : Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f →
  Presheaf.IsLocallySurjective (coherentTopology C) (FA := FD) (CA := CD) f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
inst_4 : Preregular.{v_1, u_1} C
inst_5 : FinitaryPreExtensive.{v_1, u_1} C
inst_6 : PreservesFiniteProducts F
inst_7 : PreservesFiniteProducts G
inst_8 : PreservesFiniteProducts.{v_2, w, u_2, w + 1} (forget D (FC := FD) (CC := CD))
⊢ Presheaf.IsLocallySurjective (coherentTopology C) (FA := FD) (CA := CD) f →
    Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f
have mp : Presheaf.IsLocallySurjective (coherentTopology C) (FA := TypeCat.Fun)
    (Functor.whiskerRight f (forget D (FC := FD) (CC := CD))) →
  Presheaf.IsLocallySurjective (regularTopology C) (FA := TypeCat.Fun)
    (Functor.whiskerRight f (forget D (FC := FD) (CC := CD)))
Tactic: rw [Presheaf.isLocallySurjective_iff_whisker_forget,
      Presheaf.isLocallySurjective_iff_whisker_forget (J := regularTopology C)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
inst_4 : Preregular.{v_1, u_1} C
inst_5 : FinitaryPreExtensive.{v_1, u_1} C
inst_6 : PreservesFiniteProducts F
inst_7 : PreservesFiniteProducts G
inst_8 : PreservesFiniteProducts.{v_2, w, u_2, w + 1} (forget D (FC := FD) (CC := CD))
⊢ Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f →
    Presheaf.IsLocallySurjective (coherentTopology C) (FA := FD) (CA := CD) f
have mpr : LE.le (α := GrothendieckTopology.{v_1, u_1} C) (regularTopology C) (coherentTopology C)
Tactic: refine Presheaf.isLocallySurjective_of_le (J := regularTopology C) ?_ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
inst_4 : Preregular.{v_1, u_1} C
inst_5 : FinitaryPreExtensive.{v_1, u_1} C
inst_6 : PreservesFiniteProducts F
inst_7 : PreservesFiniteProducts G
inst_8 : PreservesFiniteProducts.{v_2, w, u_2, w + 1} (forget D (FC := FD) (CC := CD))
⊢ LE.le (α := GrothendieckTopology.{v_1, u_1} C) (regularTopology C) (coherentTopology C)
have mpr : LE.le (α := GrothendieckTopology.{v_1, u_1} C) (regularTopology C)
  (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C))
Tactic: rw [← extensive_regular_generate_coherent]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.EffectivelyEnough
inst_5 : Precoherent.{v_2, u_2} D
inst_6 : F.Full
inst_7 : F.Faithful
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h_1 : EffectiveEpiFamily X₁ π₁
⊢ ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ B₂),
    EffectiveEpiFamily X₂ π₂ ∧ ∃ (i : β → α) (ι : (b : β) → X₂ b ⟶ X₁ (i b)), ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f
have obtain : ∀ (β : Type),
  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),
      ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ B₂),
        EffectiveEpiFamily X₂ π₂ ∧ ∃ (i : β → α) (ι : (b : β) → X₂ b ⟶ X₁ (i b)), ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f
Tactic: obtain ⟨β, _, Y₂, τ₂, H, i, ι, hh⟩ := Precoherent.pullback (F.map f) _ _
      (fun a ↦ F.map (π₁ a)) inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.EffectivelyEnough
inst_5 : Precoherent.{v_2, u_2} D
inst_6 : F.Full
inst_7 : F.Faithful
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h_1 : 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
⊢ ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ B₂),
    EffectiveEpiFamily X₂ π₂ ∧ ∃ (i : β → α) (ι : (b : β) → X₂ b ⟶ X₁ (i b)), ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f
have refine_1 : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj B₂)
  (fun (a : β) ↦ F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry))) fun (a : β) ↦
  F.map (F.preimage (F.effectiveEpiOver (Y₂ a) ≫ τ₂ a))
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), ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.EffectivelyEnough
inst_5 : Precoherent.{v_2, u_2} D
inst_6 : F.Full
inst_7 : F.Faithful
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h_1 : 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
refine_1 :
  EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj B₂)
    (fun (a : β) ↦ F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯))) fun (a : β) ↦
    F.map (F.preimage (F.effectiveEpiOver (Y₂ a) ≫ τ₂ a))
⊢ ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ B₂),
    EffectiveEpiFamily X₂ π₂ ∧ ∃ (i : β → α) (ι : (b : β) → X₂ b ⟶ X₁ (i b)), ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f
have refine_2 : ∀ (b : β),
  Eq (α := EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry) ⟶ B₁)
    (CategoryStruct.comp (Y := X₁ (i b))
      ((fun (b : β) ↦
          (F.preimage (F.effectiveEpiOver (Y₂ b) ≫ ι b) :
            EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry) ⟶ X₁ (i b)))
        b)
      (π₁ (i b)))
    ((fun (b : β) ↦
          (F.preimage (F.effectiveEpiOver (Y₂ b) ≫ τ₂ b) :
            EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry) ⟶ 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), ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.EffectivelyEnough
inst_5 : Precoherent.{v_2, u_2} D
inst_6 : F.Full
inst_7 : F.Faithful
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h_1 : 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.{v_2, u_2, 0} (C := D) (B := F.obj B₂)
    (fun (a : β) ↦ F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯))) fun (a : β) ↦
    F.map (F.preimage (F.effectiveEpiOver (Y₂ a) ≫ τ₂ a))
have refine_1 : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj B₂)
  (fun (a : β) ↦ F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry))) fun (a : β) ↦
  F.effectiveEpiOver (Y₂ a) ≫ τ₂ a
Tactic: simp only [Functor.map_preimage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.EffectivelyEnough
inst_5 : Precoherent.{v_2, u_2} D
inst_6 : F.Full
inst_7 : F.Faithful
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h_1 : 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 : β
⊢ Eq (α := EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯) ⟶ B₁)
    (CategoryStruct.comp (Y := X₁ (i b))
      ((fun (b : β) ↦
          (F.preimage (F.effectiveEpiOver (Y₂ b) ≫ ι b) :
            EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯) ⟶ X₁ (i b)))
        b)
      (π₁ (i b)))
    ((fun (b : β) ↦
          (F.preimage (F.effectiveEpiOver (Y₂ b) ≫ τ₂ b) :
            EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯) ⟶ B₂))
        b ≫
      f)
have refine_2 : Eq (α := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry)) ⟶ F.obj B₁)
  (F.map
    (CategoryStruct.comp (Y := X₁ (i b))
      ((fun (b : β) ↦
          (F.preimage (F.effectiveEpiOver (Y₂ b) ≫ ι b) :
            EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry) ⟶ X₁ (i b)))
        b)
      (π₁ (i b))))
  (F.map
    ((fun (b : β) ↦
          (F.preimage (F.effectiveEpiOver (Y₂ b) ≫ τ₂ b) :
            EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry) ⟶ B₂))
        b ≫
      f))
Tactic: apply F.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.EffectivelyEnough
inst_5 : Preregular.{v_2, u_2} D
inst_6 : F.Full
inst_7 : F.Faithful
X Y Z : C
f : X ⟶ Y
g : Z ⟶ Y
h : EffectiveEpi g
⊢ ∃ (W : C) (h : W ⟶ X) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ g = h ≫ f
have obtain : ∀ (W : D) (f' : W ⟶ F.obj X),
  EffectiveEpi f' →
    ∀ (i : W ⟶ F.obj Z) (w : i ≫ F.map g = f' ≫ F.map f),
      ∃ (W : C) (h : W ⟶ X) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ g = h ≫ f
Tactic: obtain ⟨W, f', _, i, w⟩ := Preregular.exists_fac (F.map f) (F.map g)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.EffectivelyEnough
inst_5 : Preregular.{v_2, u_2} D
inst_6 : F.Full
inst_7 : F.Faithful
X Y Z : C
f : X ⟶ Y
g : Z ⟶ Y
h : EffectiveEpi g
W : D
f' : W ⟶ F.obj X
w_1 : EffectiveEpi f'
i : W ⟶ F.obj Z
w : i ≫ F.map g = f' ≫ F.map f
⊢ ∃ (W : C) (h : W ⟶ X) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ g = h ≫ f
have refine_1 : EffectiveEpi (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry)))
  (F.map (F.preimage (F.effectiveEpiOver W ≫ f')) :
    F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry)) ⟶ F.obj X)
Tactic: refine ⟨_, F.preimage (F.effectiveEpiOver W ≫ f'),
      ⟨F.effectiveEpi_of_map _ ?_, F.preimage (F.effectiveEpiOver W ≫ i), ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.EffectivelyEnough
inst_5 : Preregular.{v_2, u_2} D
inst_6 : F.Full
inst_7 : F.Faithful
X Y Z : C
f : X ⟶ Y
g : Z ⟶ Y
h : EffectiveEpi g
W : D
f' : W ⟶ F.obj X
w_1 : EffectiveEpi f'
i : W ⟶ F.obj Z
w : i ≫ F.map g = f' ≫ F.map f
refine_1 :
  EffectiveEpi (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
    (F.map (F.preimage (F.effectiveEpiOver W ≫ f')) :
      F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)) ⟶ F.obj X)
⊢ ∃ (W : C) (h : W ⟶ X) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ g = h ≫ f
have refine_2 : Eq (α := EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry) ⟶ Y)
  (F.preimage (F.effectiveEpiOver W ≫ i) ≫ g :
    EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry) ⟶ Y)
  (F.preimage (F.effectiveEpiOver W ≫ f') ≫ f :
    EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry) ⟶ Y)
Tactic: refine ⟨_, F.preimage (F.effectiveEpiOver W ≫ f'),
      ⟨F.effectiveEpi_of_map _ ?_, F.preimage (F.effectiveEpiOver W ≫ i), ?_⟩⟩