awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
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))
this : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
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))))
        (x a) :
      (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))))

Tactic:
have : f.app ⟨Z a⟩ (x a) = G.map (π a).op y := (h' a).choose_spec
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
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))
this_1 : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
a : α
this :
  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))))
        (x a) :
      (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))))
⊢ 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))))
        (x a) :
      (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))))

Tactic:
this
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
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))
this_1 : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
a : α
this :
  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))))
        (x a) :
      (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))))
⊢ Eq.{max (w + 1) 1} (α := (∏ᶜ fun (a : α) ↦ F.obj (op (Z a))) ⟶ F.obj (op (Z a)))
    (Iso.hom (Types.productIso fun (a : α) ↦ F.obj (op (Z a))) ≫ ↾fun (f : (j : α) → F.obj (op (Z j))) ↦ f a)
    (Pi.π (fun (a : α) ↦ F.obj (op (Z a))) a)

Tactic:
have := Types.productIso_hom_comp_eval (fun a ↦ F.obj (op (Z a))) a
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
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))
this_1 : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
a : α
this_2 :
  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))))
        (x a) :
      (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))))
this :
  Eq.{max (w + 1) 1} (α := (∏ᶜ fun (a : α) ↦ F.obj (op (Z a))) ⟶ F.obj (op (Z a)))
    (Iso.hom (Types.productIso fun (a : α) ↦ F.obj (op (Z a))) ≫ ↾fun (f : (j : α) → F.obj (op (Z j))) ↦ f a)
    (Pi.π (fun (a : α) ↦ F.obj (op (Z a))) a)
⊢ Eq.{w + 1} (α := ((j : α) → F.obj (op (Z j))) ⟶ F.obj (op (Z a))) (↾fun (f : (j : α) → F.obj (op (Z j))) ↦ f a)
    (Iso.inv (Types.productIso fun (a : α) ↦ F.obj (op (Z a))) ≫ Pi.π (fun (a : α) ↦ F.obj (op (Z a))) a)

Tactic:
rw [← Iso.eq_inv_comp] at this

Premises used: CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
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))
this_1 : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
a : α
this_2 :
  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))))
        (x a) :
      (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))))
this :
  Eq.{w + 1} (α := ((j : α) → F.obj (op (Z j))) ⟶ F.obj (op (Z a))) (↾fun (f : (j : α) → F.obj (op (Z j))) ↦ f a)
    (Iso.inv (Types.productIso fun (a : α) ↦ F.obj (op (Z a))) ≫ Pi.π (fun (a : α) ↦ F.obj (op (Z a))) a)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.π (fun (b : α) ↦ F.obj (op (Z b))) a) :
        (a_1 : ∏ᶜ fun (j : α) ↦ F.obj (op (Z j))) → F.obj (op (Z a)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (Types.productIso fun (a : α) ↦ F.obj (op (Z a)))) :
            (a : (a : α) → F.obj (op (Z a))) → ∏ᶜ fun (a : α) ↦ F.obj (op (Z a)))
          x :
        ∏ᶜ fun (a : α) ↦ F.obj (op (Z a))) =
    x a

Tactic:
simp [← comp_apply]

Premises used: CategoryTheory.comp_apply
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
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))
this_1 : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
a : α
this :
  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))))
        (x a) :
      (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))))
⊢ Eq (α := G.obj (op (Z a)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (Quiver.Hom.op (Sigma.ι Z a))) :
          (a_1 : G.obj (op (∐ Z))) → G.obj (op (Z a)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (Quiver.Hom.op (Sigma.desc π))) :
              (a : G.obj (op U)) → G.obj (op (∐ Z)))
            y :
          G.obj (op (sigmaObj.{0, v_1, u_1} Z))) :
      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))))

Tactic:
simp only [← Functor.map_comp_apply, ← op_comp, Sigma.ι_desc]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp_apply, CategoryTheory.Limits.Sigma.ι_desc
-- 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))
mp :
  Presheaf.IsLocallySurjective (coherentTopology C) (FA := FD) (CA := CD) f →
    Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f
mpr :
  Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f →
    Presheaf.IsLocallySurjective (coherentTopology C) (FA := FD) (CA := CD) f
⊢ Presheaf.IsLocallySurjective (coherentTopology C) (FA := FD) (CA := CD) f ↔
    Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f

Tactic:
constructor
-- 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))
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)))
⊢ Presheaf.IsLocallySurjective (coherentTopology C) (FA := FD) (CA := CD) f →
    Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f

Tactic:
rw [Presheaf.isLocallySurjective_iff_whisker_forget,
      Presheaf.isLocallySurjective_iff_whisker_forget (J := regularTopology C)]

Premises used: CategoryTheory.regularTopology, CategoryTheory.Presheaf.isLocallySurjective_iff_whisker_forget
-- 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))
⊢ 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:
regularTopology.isLocallySurjective_sheaf_of_types _

Premises used: CategoryTheory.regularTopology.isLocallySurjective_sheaf_of_types
-- 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))
⊢ 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:
exact regularTopology.isLocallySurjective_sheaf_of_types _

Premises used: CategoryTheory.regularTopology.isLocallySurjective_sheaf_of_types
-- 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))
⊢ Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f →
    Presheaf.IsLocallySurjective (coherentTopology C) (FA := FD) (CA := CD) f

Tactic:
Presheaf.isLocallySurjective_of_le (J := regularTopology C) ?_ _

Premises used: CategoryTheory.Presheaf.isLocallySurjective_of_le
-- 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))
mpr : LE.le (α := GrothendieckTopology.{v_1, u_1} C) (regularTopology C) (coherentTopology C)
⊢ Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f →
    Presheaf.IsLocallySurjective (coherentTopology C) (FA := FD) (CA := CD) f

Tactic:
refine Presheaf.isLocallySurjective_of_le (J := regularTopology C) ?_ _

Premises used: CategoryTheory.Presheaf.isLocallySurjective_of_le
-- 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))
mpr :
  LE.le (α := GrothendieckTopology.{v_1, u_1} C) (regularTopology C)
    (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C))
⊢ LE.le (α := GrothendieckTopology.{v_1, u_1} C) (regularTopology C) (coherentTopology C)

Tactic:
rw [← extensive_regular_generate_coherent]

Premises used: CategoryTheory.extensive_regular_generate_coherent
-- 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:
(Coverage.gi _).gc.monotone_l le_sup_right

Premises used: le_sup_right, CategoryTheory.Coverage.gi, GaloisConnection.monotone_l, GaloisInsertion.gc