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
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
a : α
refine_2 :
  ∀ (W : C) (g₁ : W ⟶ X) (g₂ : Y a ⟶ F.obj W) (h₁ : S.arrows g₁) (h₂ : π a = g₂ ≫ F.map g₁),
    S.arrows (F.preimage (g₀ a ≫ π a))
⊢ S.arrows (F.preimage (g₀ a ≫ π a))

Tactic:
obtain ⟨W, g₁, g₂, h₁, h₂⟩ := 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
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
a : α
W : C
g₁ : W ⟶ X
g₂ : Y a ⟶ F.obj W
h₁ : S.arrows g₁
h₂ : π a = g₂ ≫ F.map g₁
refine_2 : S.arrows (F.preimage (g₀ a ≫ g₂ ≫ F.map g₁))
⊢ S.arrows (F.preimage (g₀ a ≫ π a))

Tactic:
rw [h₂]
-- 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
a : α
W : C
g₁ : W ⟶ X
g₂ : Y a ⟶ F.obj W
h₁ : S.arrows g₁
h₂ : π a = g₂ ≫ F.map g₁
⊢ S.arrows (F.preimage (g₀ a ≫ g₂) ≫ g₁)

Tactic:
S.downward_closed h₁ (F.preimage (g₀ a ≫ g₂))

Premises used: CategoryTheory.Functor.preimage, CategoryTheory.Sieve.downward_closed, 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
a : α
W : C
g₁ : W ⟶ X
g₂ : Y a ⟶ F.obj W
h₁ : S.arrows g₁
h₂ : π a = g₂ ≫ F.map g₁
h : F.preimage (g₀ a ≫ g₂ ≫ F.map g₁) = F.preimage (g₀ a ≫ g₂) ≫ g₁
⊢ S.arrows (F.preimage (g₀ a ≫ g₂ ≫ F.map g₁))

Tactic:
convert! S.downward_closed h₁ (F.preimage (g₀ a ≫ g₂))

Premises used: CategoryTheory.Functor.preimage, CategoryTheory.Sieve.downward_closed, 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
a : α
W : C
g₁ : W ⟶ X
g₂ : Y a ⟶ F.obj W
h₁ : S.arrows g₁
h₂ : π a = g₂ ≫ F.map g₁
⊢ F.map (F.preimage (g₀ a ≫ g₂ ≫ F.map g₁)) = F.map (F.preimage (g₀ a ≫ g₂) ≫ g₁)

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
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
a : α
W : C
g₁ : W ⟶ X
g₂ : Y a ⟶ F.obj W
h₁ : S.arrows g₁
h₂ : π a = g₂ ≫ F.map g₁
⊢ F.preimage (g₀ a ≫ g₂ ≫ F.map g₁) = F.preimage (g₀ a ≫ g₂) ≫ g₁

Tactic:
exact F.map_injective (by simp)

Premises used: CategoryTheory.Functor.map_injective
-- 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
h :
  ∀ (X : C) (S : Sieve.{v_1, u_1} X),
    S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X ↔
      S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
⊢ coherentTopology C = F.inducedTopology (coherentTopology D)

Tactic:
ext X S
-- 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
⊢ Precoherent.{v_1, u_1} C

Tactic:
have := F.reflects_precoherent
-- 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
this : Precoherent.{v_1, u_1} C
h :
  S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X ↔
    ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X ↔
    S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X

Tactic:
rw [← exists_effectiveEpiFamily_iff_mem_induced F X]

Premises used: CategoryTheory.coherentTopology.exists_effectiveEpiFamily_iff_mem_induced
-- 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
this : Precoherent.{v_1, u_1} C
h h₁ : S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X ↔ S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X
⊢ S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X ↔
    ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
rw [← coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily S]

Premises used: CategoryTheory.coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily
-- 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
rw :
  ∀ {X : C} {S : Sieve.{v_1, u_1} X},
    Membership.mem (γ := Set (Sieve.{v_2, u_2} (F.obj X))) ((coherentTopology D : (a : D) → Set (Sieve a)) (F.obj X))
        (Sieve.functorPushforward F S) ↔
      S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
⊢ ∀ {X : C} {S : Sieve.{v_1, u_1} X},
    Membership.mem (γ := Set (Sieve.{v_2, u_2} (F.obj X))) ((coherentTopology D : (a : D) → Set (Sieve a)) (F.obj X))
        (Sieve.functorPushforward F S) ↔
      S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X

Tactic:
rw [eq_induced F]

Premises used: CategoryTheory.coherentTopology.eq_induced
-- 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},
    Membership.mem (γ := Set (Sieve.{v_2, u_2} (F.obj X))) ((coherentTopology D : (a : D) → Set (Sieve a)) (F.obj X))
        (Sieve.functorPushforward F S) ↔
      S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X

Tactic:
rfl
-- 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
⊢ CoverPreserving (coherentTopology C) (coherentTopology D) F

Tactic:
IsDenseSubsite.coverPreserving _ _ _

Premises used: CategoryTheory.Functor.IsDenseSubsite.coverPreserving
-- 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.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
⊢ F.IsCoverDense (regularTopology D)

Tactic:
F.isCoverDense_of_generate_singleton_functor_π_mem _ fun B ↦ ⟨_, F.effectiveEpiOver B, ?_⟩

Premises used: CategoryTheory.Functor.EffectivelyEnough.presentation, Nonempty.some, CategoryTheory.Functor.isCoverDense_of_generate_singleton_functor_π_mem, Exists.intro, CategoryTheory.Functor.effectiveEpiOver, CategoryTheory.Functor.EffectivePresentation.p
-- 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.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
refine :
  ∀ (B : D),
    Sieve.generate
        (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)) ∈
      (regularTopology D : (a : D) → Set (Sieve a)) B
⊢ F.IsCoverDense (regularTopology D)

Tactic:
refine F.isCoverDense_of_generate_singleton_functor_π_mem _ fun B ↦ ⟨_, F.effectiveEpiOver B, ?_⟩

Premises used: CategoryTheory.Functor.EffectivelyEnough.presentation, Nonempty.some, CategoryTheory.Functor.isCoverDense_of_generate_singleton_functor_π_mem, Exists.intro, CategoryTheory.Functor.effectiveEpiOver, CategoryTheory.Functor.EffectivePresentation.p
-- 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.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
B : D
hS :
  Membership.mem (γ := Set (Presieve.{v_2, u_2} B))
    (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage 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))
⊢ Sieve.generate
      (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)) ∈
    (regularTopology D : (a : D) → Set (Sieve a)) B

Tactic:
apply Coverage.Saturate.of

Premises used: CategoryTheory.Coverage.Saturate.of
-- 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.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
B : D
⊢ Membership.mem (γ := Set (Presieve.{v_2, u_2} B))
    (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage 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:
⟨F.effectiveEpiOverObj B, F.effectiveEpiOver B, ?_, inferInstance⟩

Premises used: Set.Mem, setOf, inferInstance, CategoryTheory.Functor.effectiveEpiOverObj, And.intro, Exists.intro, CategoryTheory.Functor.effectiveEpiOver
-- 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.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{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
⊢ Membership.mem (γ := Set (Presieve.{v_2, u_2} B))
    (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage 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 ⟨F.effectiveEpiOverObj B, F.effectiveEpiOver B, ?_, 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.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{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.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{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.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{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.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{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.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{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.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
⊢ (∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π) ↔
    S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X

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

Premises used: CategoryTheory.Functor.inducedTopology, _private.0.CategoryTheory.regularTopology.exists_effectiveEpi_iff_mem_induced.match_1, Membership.mem, CategoryTheory.regularTopology, Iff.intro, DFunLike.coe
-- 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.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
refine_1 :
  (∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π) →
    ∀ (Y : C) (π : Y ⟶ X) (H₁ : EffectiveEpi π) (H₂ : S.arrows π),
      S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
refine_2 :
  ∀ (hS : S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X),
    ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π
⊢ (∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π) ↔
    S ∈ (F.inducedTopology (regularTopology 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.PreservesEffectiveEpis
inst_3 : F.ReflectsEffectiveEpis
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Preregular.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
h : ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π
Y : C
π : Y ⟶ X
H₁ : EffectiveEpi π
H₂ : S.arrows π
refine_1 : ∃ (Y : D) (π : Y ⟶ F.obj X), EffectiveEpi π ∧ (Sieve.functorPushforward F S).arrows π
⊢ S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X

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

Premises used: Iff.mpr, CategoryTheory.regularTopology.mem_sieves_iff_hasEffectiveEpi, CategoryTheory.Sieve.functorPushforward