awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
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.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
B : D
hS :
  Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
      (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B) =
    Presieve.ofArrows (fun (x : Unit) ↦ F.effectiveEpiOverObj B) fun (x : Unit) ↦ F.effectiveEpiOver B
hS₁ :
  EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := B) (fun (x : Unit) ↦ F.effectiveEpiOverObj B) fun (x : Unit) ↦
    F.effectiveEpiOver B
⊢ Membership.mem (γ := Set (Presieve.{v_2, u_2} B))
    (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage D)) B)
    (Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
      (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B))

Tactic:
refine ⟨Unit, inferInstance, fun _ => F.effectiveEpiOverObj B,
    fun _ => F.effectiveEpiOver B, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
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.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
B : D
hS :
  ∀ (x : D) (x_1 : x ⟶ B),
    Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
        (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B) x_1 =
      Presieve.ofArrows (fun (x : Unit) ↦ F.effectiveEpiOverObj B) (fun (x : Unit) ↦ F.effectiveEpiOver B) x_1
⊢ Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
      (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B) =
    Presieve.ofArrows (fun (x : Unit) ↦ F.effectiveEpiOverObj B) fun (x : Unit) ↦ F.effectiveEpiOver B

Tactic:
funext
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
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.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
B x : D
x_1 : x ⟶ B
hS :
  Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
      (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B) x_1 ↔
    Presieve.ofArrows (fun (x : Unit) ↦ F.effectiveEpiOverObj B) (fun (x : Unit) ↦ F.effectiveEpiOver B) x_1
⊢ Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
      (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B) x_1 =
    Presieve.ofArrows (fun (x : Unit) ↦ F.effectiveEpiOverObj B) (fun (x : Unit) ↦ F.effectiveEpiOver B) x_1

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
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.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
B x : D
x_1 : x ⟶ B
⊢ Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
      (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B) x_1 ↔
    Presieve.ofArrows (fun (x : Unit) ↦ F.effectiveEpiOverObj B) (fun (x : Unit) ↦ F.effectiveEpiOver B) x_1

Tactic:
⟨fun ⟨⟩ ↦ ⟨()⟩, ?_⟩

Premises used: Unit.unit, CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.Functor.effectiveEpiOverObj, Iff.intro, _private.0.CategoryTheory.coherentTopology.instIsCoverDense.match_1, CategoryTheory.Functor.effectiveEpiOver, CategoryTheory.Presieve.ofArrows
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
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.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
B x : D
x_1 : x ⟶ B
hS :
  Presieve.ofArrows (fun (x : Unit) ↦ F.effectiveEpiOverObj B) (fun (x : Unit) ↦ F.effectiveEpiOver B) x_1 →
    Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
      (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B) x_1
⊢ Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
      (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B) x_1 ↔
    Presieve.ofArrows (fun (x : Unit) ↦ F.effectiveEpiOverObj B) (fun (x : Unit) ↦ F.effectiveEpiOver B) x_1

Tactic:
refine ⟨fun ⟨⟩ ↦ ⟨()⟩, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
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.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
B Y : D
i : Unit
⊢ Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
    (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B) (Y := F.effectiveEpiOverObj B) (F.effectiveEpiOver B)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
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.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
B : D
hS : EffectiveEpi (Y := F.effectiveEpiOverObj B) (F.effectiveEpiOver B)
⊢ EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := B) (fun (x : Unit) ↦ F.effectiveEpiOverObj B) fun (x : Unit) ↦
    F.effectiveEpiOver B

Tactic:
rw [← effectiveEpi_iff_effectiveEpiFamily]

Premises used: CategoryTheory.effectiveEpi_iff_effectiveEpiFamily
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
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.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
B : D
⊢ EffectiveEpi (Y := F.effectiveEpiOverObj B) (F.effectiveEpiOver B)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
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.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
⊢ (∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
      EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) ↔
    S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X

Tactic:
⟨fun ⟨α, _, Y, π, ⟨H₁, H₂⟩⟩ ↦ ?_, fun hS ↦ ?_⟩

Premises used: CategoryTheory.Functor.inducedTopology, Membership.mem, Iff.intro, _private.0.CategoryTheory.coherentTopology.exists_effectiveEpiFamily_iff_mem_induced.match_1, DFunLike.coe, CategoryTheory.coherentTopology
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
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.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
refine_1 :
  (∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
      EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) →
    ∀ (α : Type),
      Finite α →
        ∀ (Y : α → C) (π : (a : α) → Y a ⟶ X) (H₁ : EffectiveEpiFamily Y π) (H₂ : ∀ (a : α), S.arrows (π a)),
          S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
refine_2 :
  ∀ (hS : S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X),
    ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ (∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
      EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) ↔
    S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X

Tactic:
refine ⟨fun ⟨α, _, Y, π, ⟨H₁, H₂⟩⟩ ↦ ?_, fun hS ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
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.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
h : ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
refine_1 :
  ∃ (α : Type) (_ : Finite α) (Y : α → D) (π : (a : α) → Y a ⟶ F.obj X),
    EffectiveEpiFamily Y π ∧ ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
⊢ S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X

Tactic:
apply (mem_sieves_iff_hasEffectiveEpiFamily (Sieve.functorPushforward _ S)).mpr

Premises used: Iff.mpr, CategoryTheory.coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily, CategoryTheory.Sieve.functorPushforward
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
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.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
h : ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ ∃ (α : Type) (_ : Finite α) (Y : α → D) (π : (a : α) → Y a ⟶ F.obj X),
    EffectiveEpiFamily Y π ∧ ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)

Tactic:
⟨α, inferInstance, fun i => F.obj (Y i),
      fun i => F.map (π i), ⟨?_,
      fun a => Sieve.image_mem_functorPushforward F S (H₂ a)⟩⟩

Premises used: inferInstance, CategoryTheory.Functor.map, And.intro, Exists.intro, CategoryTheory.Sieve.image_mem_functorPushforward, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
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.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
h : ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
refine_1 :
  EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj X) (fun (i : α) ↦ F.obj (Y i)) fun (i : α) ↦ F.map (π i)
⊢ ∃ (α : Type) (_ : Finite α) (Y : α → D) (π : (a : α) → Y a ⟶ F.obj X),
    EffectiveEpiFamily Y π ∧ ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)

Tactic:
refine ⟨α, inferInstance, fun i => F.obj (Y i),
      fun i => F.map (π i), ⟨?_,
      fun a => Sieve.image_mem_functorPushforward F S (H₂ a)⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
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.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
h : ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj X) (fun (i : α) ↦ F.obj (Y i)) fun (i : α) ↦ F.map (π i)

Tactic:
F.map_finite_effectiveEpiFamily _ _

Premises used: CategoryTheory.Functor.map_finite_effectiveEpiFamily
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
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.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
h : ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj X) (fun (i : α) ↦ F.obj (Y i)) fun (i : α) ↦ F.map (π i)

Tactic:
exact F.map_finite_effectiveEpiFamily _ _

Premises used: CategoryTheory.Functor.map_finite_effectiveEpiFamily
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
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.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
refine_2 :
  ∀ (α : Type),
    Finite α →
      ∀ (Y : α → D) (π : (a : α) → Y a ⟶ F.obj X) (H₁ : EffectiveEpiFamily Y π)
        (H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)),
        ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
          EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
obtain ⟨α, _, Y, π, ⟨H₁, H₂⟩⟩ := (mem_sieves_iff_hasEffectiveEpiFamily _).mp hS

Premises used: CategoryTheory.coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
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.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
α : Type
w : Finite α
Y : α → D
π : (a : α) → Y a ⟶ F.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
⊢ ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
⟨α, inferInstance, ?_⟩

Premises used: inferInstance, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
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.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
α : Type
w : Finite α
Y : α → D
π : (a : α) → Y a ⟶ F.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
refine_2 : ∃ (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
refine ⟨α, inferInstance, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
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.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
α : Type
w : Finite α
Y : α → D
π : (a : α) → Y a ⟶ F.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
Z : α → C := fun (a : α) ↦ EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)
g₀ : (a : α) → F.obj (Z a) ⟶ Y a := fun (a : α) ↦ F.effectiveEpiOver (Y a)
⊢ EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj X) (fun (a : α) ↦ F.obj (Z a)) fun (a : α) ↦ g₀ a ≫ π a

Tactic:
have : EffectiveEpiFamily _ (fun a ↦ g₀ a ≫ π a) := inferInstance
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
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.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
α : Type
w : Finite α
Y : α → D
π : (a : α) → Y a ⟶ F.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
Z : α → C := fun (a : α) ↦ EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)
g₀ : (a : α) → F.obj (Z a) ⟶ Y a := fun (a : α) ↦ F.effectiveEpiOver (Y a)
this : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj X) (fun (a : α) ↦ F.obj (Z a)) fun (a : α) ↦ g₀ a ≫ π a
⊢ ∃ (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
⟨Z, fun a ↦ F.preimage (g₀ a ≫ π a), ?_, fun a ↦ (?_ : S.arrows (F.preimage _))⟩

Premises used: CategoryTheory.Functor.preimage, And.intro, Exists.intro, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
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.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
α : Type
w : Finite α
Y : α → D
π : (a : α) → Y a ⟶ F.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
Z : α → C := fun (a : α) ↦ EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)
g₀ : (a : α) → F.obj (Z a) ⟶ Y a := fun (a : α) ↦ F.effectiveEpiOver (Y a)
this : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj X) (fun (a : α) ↦ F.obj (Z a)) fun (a : α) ↦ g₀ a ≫ π a
refine_2 : EffectiveEpiFamily.{v_1, u_1, 0} (B := X) Z fun (a : α) ↦ F.preimage (g₀ a ≫ π a)
refine_2₁ : ∀ (a : α), S.arrows (F.preimage (g₀ a ≫ π a))
⊢ ∃ (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
refine ⟨Z, fun a ↦ F.preimage (g₀ a ≫ π a), ?_, fun a ↦ (?_ : S.arrows (F.preimage _))⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
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.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
α : Type
w : Finite α
Y : α → D
π : (a : α) → Y a ⟶ F.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
Z : α → C := fun (a : α) ↦ EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)
g₀ : (a : α) → F.obj (Z a) ⟶ Y a := fun (a : α) ↦ F.effectiveEpiOver (Y a)
this : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj X) (fun (a : α) ↦ F.obj (Z a)) fun (a : α) ↦ g₀ a ≫ π a
⊢ EffectiveEpiFamily.{v_1, u_1, 0} (B := X) Z fun (a : α) ↦ F.preimage (g₀ a ≫ π a)

Tactic:
F.finite_effectiveEpiFamily_of_map _ _ ?_

Premises used: CategoryTheory.Functor.finite_effectiveEpiFamily_of_map
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
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.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
α : Type
w : Finite α
Y : α → D
π : (a : α) → Y a ⟶ F.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
Z : α → C := fun (a : α) ↦ EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)
g₀ : (a : α) → F.obj (Z a) ⟶ Y a := fun (a : α) ↦ F.effectiveEpiOver (Y a)
this : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj X) (fun (a : α) ↦ F.obj (Z a)) fun (a : α) ↦ g₀ a ≫ π a
refine_2 :
  EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj X) (fun (a : α) ↦ F.obj (Z a)) fun (a : α) ↦
    F.map (F.preimage (g₀ a ≫ π a))
⊢ EffectiveEpiFamily.{v_1, u_1, 0} (B := X) Z fun (a : α) ↦ F.preimage (g₀ a ≫ π a)

Tactic:
refine F.finite_effectiveEpiFamily_of_map _ _ ?_

Premises used: CategoryTheory.Functor.finite_effectiveEpiFamily_of_map
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
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.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
α : Type
w : Finite α
Y : α → D
π : (a : α) → Y a ⟶ F.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
Z : α → C := fun (a : α) ↦ EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)
g₀ : (a : α) → F.obj (Z a) ⟶ Y a := fun (a : α) ↦ F.effectiveEpiOver (Y a)
this : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj X) (fun (a : α) ↦ F.obj (Z a)) fun (a : α) ↦ g₀ a ≫ π a
⊢ EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj X) (fun (a : α) ↦ F.obj (Z a)) fun (a : α) ↦
    F.map (F.preimage (g₀ a ≫ π a))

Tactic:
simpa using this