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.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 π
⊢ ∃ (Y : D) (π : Y ⟶ F.obj X), EffectiveEpi π ∧ (Sieve.functorPushforward F S).arrows π

Tactic:
⟨F.obj Y, F.map π, ⟨?_, Sieve.image_mem_functorPushforward F S H₂⟩⟩

Premises used: 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.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 : EffectiveEpi (F.map π)
⊢ ∃ (Y : D) (π : Y ⟶ F.obj X), EffectiveEpi π ∧ (Sieve.functorPushforward F S).arrows π

Tactic:
refine ⟨F.obj Y, F.map π, ⟨?_, Sieve.image_mem_functorPushforward F S 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.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 π
⊢ EffectiveEpi (F.map π)

Tactic:
F.map_effectiveEpi _

Premises used: CategoryTheory.Functor.map_effectiveEpi
-- 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 π
⊢ EffectiveEpi (F.map π)

Tactic:
exact F.map_effectiveEpi _

Premises used: CategoryTheory.Functor.map_effectiveEpi
-- 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
hS : S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
refine_2 :
  ∀ (Y : D) (π : Y ⟶ F.obj X) (H₁ : EffectiveEpi π) (H₂ : (Sieve.functorPushforward F S).arrows π),
    ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π
⊢ ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π

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

Premises used: CategoryTheory.regularTopology.mem_sieves_iff_hasEffectiveEpi, 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.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
hS : S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
H₂ : (Sieve.functorPushforward F S).arrows π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
⊢ ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π

Tactic:
⟨_, F.preimage (g₀ ≫ π), ?_, (?_ : 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.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
hS : S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
H₂ : (Sieve.functorPushforward F S).arrows π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
refine_2 : EffectiveEpi (F.preimage (g₀ ≫ π))
refine_2₁ : S.arrows (F.preimage (g₀ ≫ π))
⊢ ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π

Tactic:
refine ⟨_, F.preimage (g₀ ≫ π), ?_, (?_ : 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.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
hS : S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
H₂ : (Sieve.functorPushforward F S).arrows π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
⊢ EffectiveEpi (F.preimage (g₀ ≫ π))

Tactic:
F.effectiveEpi_of_map _ ?_

Premises used: CategoryTheory.Functor.effectiveEpi_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.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
hS : S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
H₂ : (Sieve.functorPushforward F S).arrows π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
refine_2 : EffectiveEpi (F.map (F.preimage (g₀ ≫ π)))
⊢ EffectiveEpi (F.preimage (g₀ ≫ π))

Tactic:
refine F.effectiveEpi_of_map _ ?_

Premises used: CategoryTheory.Functor.effectiveEpi_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.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
hS : S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
H₂ : (Sieve.functorPushforward F S).arrows π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
refine_2 : EffectiveEpi (g₀ ≫ π)
⊢ EffectiveEpi (F.map (F.preimage (g₀ ≫ π)))

Tactic:
simp only [map_preimage]

Premises used: CategoryTheory.Functor.map_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.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
hS : S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
H₂ : (Sieve.functorPushforward F S).arrows π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
⊢ EffectiveEpi (g₀ ≫ π)

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.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
hS : S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
H₂ : (Sieve.functorPushforward F S).arrows π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
refine_2 :
  ∀ (W : C) (g₁ : W ⟶ X) (g₂ : Y ⟶ F.obj W) (h₁ : S.arrows g₁) (h₂ : π = g₂ ≫ F.map g₁), S.arrows (F.preimage (g₀ ≫ π))
⊢ S.arrows (F.preimage (g₀ ≫ π))

Tactic:
obtain ⟨W, g₁, g₂, h₁, h₂⟩ := 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.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
hS : S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
W : C
g₁ : W ⟶ X
g₂ : Y ⟶ F.obj W
h₁ : S.arrows g₁
h₂ : π = g₂ ≫ F.map g₁
refine_2 : S.arrows (F.preimage (g₀ ≫ g₂ ≫ F.map g₁))
⊢ S.arrows (F.preimage (g₀ ≫ π))

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.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
hS : S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
W : C
g₁ : W ⟶ X
g₂ : Y ⟶ F.obj W
h₁ : S.arrows g₁
h₂ : π = g₂ ≫ F.map g₁
⊢ S.arrows (F.preimage (g₀ ≫ g₂) ≫ g₁)

Tactic:
S.downward_closed h₁ (F.preimage (g₀ ≫ 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.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
hS : S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
W : C
g₁ : W ⟶ X
g₂ : Y ⟶ F.obj W
h₁ : S.arrows g₁
h₂ : π = g₂ ≫ F.map g₁
h : F.preimage (g₀ ≫ g₂ ≫ F.map g₁) = F.preimage (g₀ ≫ g₂) ≫ g₁
⊢ S.arrows (F.preimage (g₀ ≫ g₂ ≫ F.map g₁))

Tactic:
convert! S.downward_closed h₁ (F.preimage (g₀ ≫ 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.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
hS : S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
W : C
g₁ : W ⟶ X
g₂ : Y ⟶ F.obj W
h₁ : S.arrows g₁
h₂ : π = g₂ ≫ F.map g₁
⊢ F.map (F.preimage (g₀ ≫ g₂ ≫ F.map g₁)) = F.map (F.preimage (g₀ ≫ 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.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
hS : S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
W : C
g₁ : W ⟶ X
g₂ : Y ⟶ F.obj W
h₁ : S.arrows g₁
h₂ : π = g₂ ≫ F.map g₁
⊢ F.preimage (g₀ ≫ g₂ ≫ F.map g₁) = F.preimage (g₀ ≫ 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.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
h :
  ∀ (X : C) (S : Sieve.{v_1, u_1} X),
    S ∈ (regularTopology C : (a : C) → Set (Sieve a)) X ↔
      S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X
⊢ regularTopology C = F.inducedTopology (regularTopology 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.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
⊢ Preregular.{v_1, u_1} C

Tactic:
have := F.reflects_preregular
-- 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
this : Preregular.{v_1, u_1} C
h : S ∈ (regularTopology C : (a : C) → Set (Sieve a)) X ↔ ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π
⊢ S ∈ (regularTopology C : (a : C) → Set (Sieve a)) X ↔
    S ∈ (F.inducedTopology (regularTopology D) : (a : C) → Set (Sieve a)) X

Tactic:
rw [← exists_effectiveEpi_iff_mem_induced F X]

Premises used: CategoryTheory.regularTopology.exists_effectiveEpi_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.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
this : Preregular.{v_1, u_1} C
h h₁ : S ∈ (regularTopology C : (a : C) → Set (Sieve a)) X ↔ S ∈ (regularTopology C : (a : C) → Set (Sieve a)) X
⊢ S ∈ (regularTopology C : (a : C) → Set (Sieve a)) X ↔ ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π

Tactic:
rw [← mem_sieves_iff_hasEffectiveEpi S]

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

Tactic:
rw [eq_induced F]

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

Tactic:
IsDenseSubsite.coverPreserving _ _ _

Premises used: CategoryTheory.Functor.IsDenseSubsite.coverPreserving
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
inst_2 : Preregular.{v_1, u_1} C
inst_3 : FinitaryPreExtensive.{v_1, u_1} C
rw :
  IsSheaf (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C)) F ↔
    IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F
⊢ IsSheaf (coherentTopology C) F ↔ IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F

Tactic:
rw [← extensive_regular_generate_coherent]

Premises used: CategoryTheory.extensive_regular_generate_coherent
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
inst_2 : Preregular.{v_1, u_1} C
inst_3 : FinitaryPreExtensive.{v_1, u_1} C
⊢ IsSheaf (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C)) F ↔
    IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F

Tactic:
isSheaf_sup (extensiveCoverage C) (regularCoverage C) F

Premises used: CategoryTheory.regularCoverage, CategoryTheory.regularTopology, CategoryTheory.extensiveCoverage, CategoryTheory.extensiveTopology, CategoryTheory.Presheaf.isSheaf_sup
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
inst_2 : Preregular.{v_1, u_1} C
inst_3 : FinitaryPreExtensive.{v_1, u_1} C
⊢ IsSheaf (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C)) F ↔
    IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F

Tactic:
exact isSheaf_sup (extensiveCoverage C) (regularCoverage C) F

Premises used: CategoryTheory.regularCoverage, CategoryTheory.extensiveCoverage, CategoryTheory.Presheaf.isSheaf_sup
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
inst_2 : Preregular.{v_1, u_1} C
inst_3 : FinitaryExtensive.{v_1, u_1} C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
rw : IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F ↔ PreservesFiniteProducts F ∧ EqualizerCondition F
⊢ IsSheaf (coherentTopology C) F ↔ PreservesFiniteProducts F ∧ EqualizerCondition F

Tactic:
rw [isSheaf_coherent_iff_regular_and_extensive]

Premises used: CategoryTheory.Presheaf.isSheaf_coherent_iff_regular_and_extensive
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
inst_2 : Preregular.{v_1, u_1} C
inst_3 : FinitaryExtensive.{v_1, u_1} C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
⊢ IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F ↔ PreservesFiniteProducts F ∧ EqualizerCondition F

Tactic:
and_congr (isSheaf_iff_preservesFiniteProducts _)
    (@equalizerCondition_iff_isSheaf _ _ _ _ F _ h).symm

Premises used: CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts, CategoryTheory.regularTopology.equalizerCondition_iff_isSheaf, Iff.symm, and_congr
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
inst_2 : Preregular.{v_1, u_1} C
inst_3 : FinitaryExtensive.{v_1, u_1} C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
⊢ IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F ↔ PreservesFiniteProducts F ∧ EqualizerCondition F

Tactic:
exact and_congr (isSheaf_iff_preservesFiniteProducts _)
    (@equalizerCondition_iff_isSheaf _ _ _ _ F _ h).symm

Premises used: CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts, CategoryTheory.regularTopology.equalizerCondition_iff_isSheaf, Iff.symm, and_congr
-- 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_1 : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u₃
inst_2 : Category.{v₃, u₃} A
F_2 : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
inst_3 : Preregular.{v_1, u_1} C
inst_4 : FinitaryExtensive.{v_1, u_1} C
F : Sheaf.{v_1, v₃, u_1, u₃} (coherentTopology C) A
⊢ PreservesFiniteProducts (F.obj (P := IsSheaf (coherentTopology C)))

Tactic:
(Presheaf.isSheaf_iff_preservesFiniteProducts F.obj).1
    ((Presheaf.isSheaf_coherent_iff_regular_and_extensive F.obj).mp F.property).1

Premises used: CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Presheaf.isSheaf_coherent_iff_regular_and_extensive, CategoryTheory.ObjectProperty.FullSubcategory.obj, And.left, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
F : Functor.{v_1, v₃, u_1, u₃} Cᵒᵖ A
inst_2 : Preregular.{v_1, u_1} C
inst_3 : FinitaryExtensive.{v_1, u_1} C
inst_4 : ∀ (X : C), Projective.{v_1, u_1} X
rw : IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F ↔ PreservesFiniteProducts F
rw₁ : IsSheaf (extensiveTopology C) F ↔ PreservesFiniteProducts F
rw₂ rw₃ : PreservesFiniteProducts F ↔ PreservesFiniteProducts F
⊢ IsSheaf (coherentTopology C) F ↔ PreservesFiniteProducts F

Tactic:
rw [isSheaf_coherent_iff_regular_and_extensive, and_iff_left (isSheaf_of_projective F),
    isSheaf_iff_preservesFiniteProducts]

Premises used: CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts, and_iff_left, CategoryTheory.Presheaf.isSheaf_coherent_iff_regular_and_extensive, CategoryTheory.regularTopology.isSheaf_of_projective