awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
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)
    (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C))

Tactic:
exact (Coverage.gi _).gc.monotone_l le_sup_right

Premises used: le_sup_right, CategoryTheory.Coverage.gi, GaloisConnection.monotone_l, GaloisInsertion.gc
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
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)
inst_4 : Preregular.{v_1, u_1} C
inst_5 : FinitaryExtensive.{v_1, u_1} C
F G : Sheaf.{v_1, v_2, u_1, u_2} (coherentTopology C) D
f : F ⟶ G
inst_6 : PreservesFiniteProducts.{v_2, w, u_2, w + 1} (forget D (FC := FD) (CC := CD))
⊢ IsLocallySurjective (FA := FD) (CA := CD) f ↔
    Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f.hom

Tactic:
presheafIsLocallySurjective_iff _ f.hom

Premises used: CategoryTheory.coherentTopology.presheafIsLocallySurjective_iff, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent
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₁ π₁
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
⊢ ∃ (β : 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

Premises used: inferInstance, CategoryTheory.Functor.map, CategoryTheory.Precoherent.pullback
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent
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

Tactic:
⟨β, 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), ?_⟩⟩

Premises used: CategoryTheory.Functor.preimage, CategoryTheory.Functor.finite_effectiveEpiFamily_of_map, inferInstance, And.intro, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.effectiveEpiOver
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent
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))
refine_2 :
  ∀ (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)
⊢ ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ B₂),
    EffectiveEpiFamily X₂ π₂ ∧ ∃ (i : β → α) (ι : (b : β) → X₂ b ⟶ X₁ (i b)), ∀ (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), ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent
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.effectiveEpiOver (Y₂ a) ≫ τ₂ a
⊢ 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))

Tactic:
simp only [Functor.map_preimage]

Premises used: CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent
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.effectiveEpiOver (Y₂ a) ≫ τ₂ a

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent
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 : β
refine_2 :
  Eq (α := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)) ⟶ 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 ⋯) ⟶ 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 ⋯) ⟶ B₂))
          b ≫
        f))
⊢ 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)

Tactic:
apply F.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent
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 (α := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)) ⟶ 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 ⋯) ⟶ 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 ⋯) ⟶ B₂))
          b ≫
        f))

Tactic:
simp [hh b]
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular
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
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
⊢ ∃ (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)

Premises used: CategoryTheory.Preregular.exists_fac, CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular
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

Tactic:
⟨_, F.preimage (F.effectiveEpiOver W ≫ f'),
      ⟨F.effectiveEpi_of_map _ ?_, F.preimage (F.effectiveEpiOver W ≫ i), ?_⟩⟩

Premises used: CategoryTheory.Functor.preimage, CategoryTheory.Functor.effectiveEpi_of_map, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.effectiveEpiOver
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular
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)
refine_2 :
  Eq (α := EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯) ⟶ Y)
    (F.preimage (F.effectiveEpiOver W ≫ i) ≫ g :
      EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯) ⟶ Y)
    (F.preimage (F.effectiveEpiOver W ≫ f') ≫ f :
      EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯) ⟶ Y)
⊢ ∃ (W : C) (h : W ⟶ X) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ g = h ≫ f

Tactic:
refine ⟨_, F.preimage (F.effectiveEpiOver W ≫ f'),
      ⟨F.effectiveEpi_of_map _ ?_, F.preimage (F.effectiveEpiOver W ≫ i), ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular
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.effectiveEpiOver W ≫ f' :
      F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)) ⟶ F.obj X)
⊢ 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)

Tactic:
simp only [Functor.map_preimage]

Premises used: CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular
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
⊢ EffectiveEpi (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
    (F.effectiveEpiOver W ≫ f' :
      F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)) ⟶ F.obj X)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular
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_2 :
  Eq (α := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)) ⟶ F.obj Y)
    (F.map (F.preimage (F.effectiveEpiOver W ≫ i) ≫ g) :
      F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)) ⟶ F.obj Y)
    (F.map (F.preimage (F.effectiveEpiOver W ≫ f') ≫ f) :
      F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)) ⟶ F.obj Y)
⊢ Eq (α := EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯) ⟶ Y)
    (F.preimage (F.effectiveEpiOver W ≫ i) ≫ g :
      EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯) ⟶ Y)
    (F.preimage (F.effectiveEpiOver W ≫ f') ≫ f :
      EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯) ⟶ Y)

Tactic:
apply F.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular
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
⊢ Eq (α := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)) ⟶ F.obj Y)
    (F.map (F.preimage (F.effectiveEpiOver W ≫ i) ≫ g) :
      F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)) ⟶ F.obj Y)
    (F.map (F.preimage (F.effectiveEpiOver W ≫ f') ≫ f) :
      F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)) ⟶ F.obj Y)

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
X B : C
π : X ⟶ B
c : PullbackCone π π
⊢ P.map π.op ≫ P.map c.fst.op = P.map π.op ≫ P.map c.snd.op

Tactic:
simp only [← Functor.map_comp, ← op_comp, c.condition]

Premises used: CategoryTheory.op_comp, CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P P' : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
i : P ≅ P'
hP : EqualizerCondition P
⊢ EqualizerCondition P'

Tactic:
fun X B π _ c hc ↦
  ⟨Fork.isLimitOfIsos _ (hP π c hc).some _ (i.app _) (i.app _) (i.app _)⟩

Premises used: CategoryTheory.Limits.Fork.ofι, Quiver.Hom.op, Nonempty.some, CategoryTheory.Limits.Cone.pt, Nonempty.intro, CategoryTheory.Functor.map, CategoryTheory.Limits.Fork.isLimitOfIsos, CategoryTheory.regularTopology.EqualizerCondition, Opposite.op, CategoryTheory.regularTopology.equalizerCondition_w, CategoryTheory.Iso.app, CategoryTheory.regularTopology.SingleEqualizerCondition
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
F : Functor.{v_3, v_1, u_3, u_1} E C
inst_3 : ∀ {X B : E} (π : X ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) F
inst_4 : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
_ : ∀ [EffectiveEpi π], SingleEqualizerCondition (F.op ⋙ P) π
⊢ ∀ [EffectiveEpi π], SingleEqualizerCondition (F.op ⋙ P) π

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
F : Functor.{v_3, v_1, u_3, u_1} E C
inst_3 : ∀ {X B : E} (π : X ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) F
inst_4 : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst_5 : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
⊢ P.map (F.map π).op = (F.op ⋙ P).map π.op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
F : Functor.{v_3, v_1, u_3, u_1} E C
inst_3 : ∀ {X B : E} (π : X ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) F
inst_4 : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst_5 : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
⊢ P.map (F.map π).op = (F.op ⋙ P).map π.op

Tactic:
have h : P.map (F.map π).op = (F.op ⋙ P).map π.op := by simp
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
F : Functor.{v_3, v_1, u_3, u_1} E C
inst_3 : ∀ {X B : E} (π : X ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) F
inst_4 : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst_5 : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
h : P.map (F.map π).op = (F.op ⋙ P).map π.op
⊢ Nonempty (IsLimit (Fork.ofι ((F.op ⋙ P).map π.op) ⋯))

Tactic:
⟨(IsLimit.equivIsoLimit (ForkOfι.ext ?_ _ h)) ?_⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.IsLimit.equivIsoLimit, CategoryTheory.Limits.ForkOfι.ext, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
P : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
F : Functor.{v_3, v_1, u_3, u_1} E C
inst_3 : ∀ {X B : E} (π : X ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) F
inst_4 : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst_5 : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
h : P.map (F.map π).op = (F.op ⋙ P).map π.op
refine_1 : P.map (F.map π).op ≫ (F.op ⋙ P).map c.fst.op = P.map (F.map π).op ≫ (F.op ⋙ P).map c.snd.op
refine_2 : IsLimit (Fork.ofι (P.map (F.map π).op) ⋯)
⊢ Nonempty (IsLimit (Fork.ofι ((F.op ⋙ P).map π.op) ⋯))

Tactic:
refine ⟨(IsLimit.equivIsoLimit (ForkOfι.ext ?_ _ h)) ?_⟩