awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
Y : C
T : Presieve.{v_1, u_1} Y
hT :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
    (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C ⊔ regularCoverage C)) Y) T
h :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
    (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) Y) T
⊢ generate T ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y

Tactic:
apply Coverage.Saturate.of

Premises used: CategoryTheory.Coverage.Saturate.of
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
Y : C
T : Presieve.{v_1, u_1} Y
hT :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
    (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C ⊔ regularCoverage C)) Y) T
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
      (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C)) Y) T ∨
    Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
      (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage C)) Y) T

Tactic:
simp only [Coverage.sup_covering, Set.mem_union] at hT

Premises used: Set.mem_union, CategoryTheory.Coverage.sup_covering
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
Y : C
T : Presieve.{v_1, u_1} Y
hT :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
      (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C)) Y) T ∨
    Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
      (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage C)) Y) T
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
    (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) Y) T

Tactic:
Or.elim hT
        (fun ⟨α, x, X, π, ⟨h, _⟩⟩ ↦ ⟨α, x, X, π, ⟨h, inferInstance⟩⟩)
        (fun ⟨Z, f, ⟨h, _⟩⟩ ↦ ⟨Unit, inferInstance, fun _ ↦ Z, fun _ ↦ f, ⟨h, inferInstance⟩⟩)

Premises used: _private.0.CategoryTheory.extensive_regular_generate_coherent.match_4, _private.0.CategoryTheory.extensive_regular_generate_coherent.match_3, Membership.mem, inferInstance, CategoryTheory.coherentCoverage, Unit, And.intro, Exists.intro, CategoryTheory.Precoverage.coverings, Or.elim, CategoryTheory.Coverage.toPrecoverage
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
Y : C
T : Presieve.{v_1, u_1} Y
hT :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
      (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C)) Y) T ∨
    Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
      (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage C)) Y) T
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
    (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) Y) T

Tactic:
exact Or.elim hT
        (fun ⟨α, x, X, π, ⟨h, _⟩⟩ ↦ ⟨α, x, X, π, ⟨h, inferInstance⟩⟩)
        (fun ⟨Z, f, ⟨h, _⟩⟩ ↦ ⟨Unit, inferInstance, fun _ ↦ Z, fun _ ↦ f, ⟨h, inferInstance⟩⟩)

Premises used: Or.elim
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
X : C
⊢ ⊤ ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X

Tactic:
apply Coverage.Saturate.top

Premises used: CategoryTheory.Coverage.Saturate.top
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
Y : C
T S_1 : Sieve.{v_1, u_1} Y
h_1 : Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y T
h_2 :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y_1 (Sieve.pullback f S_1)
a_ih : T ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y
a_ih_1 :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Sieve.pullback f S_1 ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y_1
h : Coverage.Saturate (coherentCoverage C) Y T
h₁ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Coverage.Saturate (coherentCoverage C) Y_1 (Sieve.pullback f S_1)
⊢ S_1 ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y

Tactic:
apply Coverage.Saturate.transitive Y T

Premises used: CategoryTheory.Coverage.Saturate.transitive
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
Y : C
T S_1 : Sieve.{v_1, u_1} Y
h : Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y T
h_1 :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y_1 (Sieve.pullback f S_1)
a_ih : T ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y
a_ih_1 :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Sieve.pullback f S_1 ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y_1
⊢ Coverage.Saturate (coherentCoverage C) Y T

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
Y : C
T S_1 : Sieve.{v_1, u_1} Y
h : Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y T
h_1 :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y_1 (Sieve.pullback f S_1)
a_ih : T ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y
a_ih_1 :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Sieve.pullback f S_1 ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y_1
⊢ ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Coverage.Saturate (coherentCoverage C) Y_1 (Sieve.pullback f S_1)

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
Y : C
T S_1 : Sieve.{v_1, u_1} Y
h_1 : Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y T
h_2 :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y_1 (Sieve.pullback f S_1)
a_ih : T ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y
a_ih_1 :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Sieve.pullback f S_1 ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y_1
h : Coverage.Saturate (coherentCoverage C) Y T
h₁ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Coverage.Saturate (coherentCoverage C) Y_1 (Sieve.pullback f S_1)
h₂ : Coverage.Saturate (coherentCoverage C) Y T
h₃ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Coverage.Saturate (coherentCoverage C) Y_1 (Sieve.pullback f S_1)
⊢ S_1 ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y

Tactic:
apply Coverage.Saturate.transitive Y T <;> [assumption; assumption]

Premises used: CategoryTheory.Coverage.Saturate.transitive
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
h : S ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) B
h₁ :
  ∀ (Y : C) (T : Presieve.{v_1, u_1} Y)
    (hT :
      Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
        (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C ⊔ regularCoverage C)) Y) T),
    generate T ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y
h₂ : ∀ (X : C), ⊤ ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X
h₃ :
  ∀ (Y : C) (T S : Sieve.{v_1, u_1} Y),
    Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y T →
      (∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
          T.arrows f → Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y_1 (Sieve.pullback f S)) →
        T ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y →
          (∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
              T.arrows f → Sieve.pullback f S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y_1) →
            S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y
⊢ S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) B

Tactic:
induction h with
    | of Y T hT =>
      apply Coverage.Saturate.of
      simp only [Coverage.sup_covering, Set.mem_union] at hT
      exact Or.elim hT
        (fun ⟨α, x, X, π, ⟨h, _⟩⟩ ↦ ⟨α, x, X, π, ⟨h, inferInstance⟩⟩)
        (fun ⟨Z, f, ⟨h, _⟩⟩ ↦ ⟨Unit, inferInstance, fun _ ↦ Z, fun _ ↦ f, ⟨h, inferInstance⟩⟩)
    | top => apply Coverage.Saturate.top
    | transitive Y T => apply Coverage.Saturate.transitive Y T <;> [assumption; assumption]

Premises used: Set.mem_union, CategoryTheory.GrothendieckTopology.transitive, CategoryTheory.Coverage.Saturate.top, CategoryTheory.Coverage.Saturate.of, CategoryTheory.Coverage.sup_covering
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
Y : C
T : Presieve.{v_1, u_1} Y
hT :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
    (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) Y) T
h :
  ∀ (I : Type),
    Finite I →
      ∀ (X : I → C) (f : (a : I) → X a ⟶ Y) (hT : EffectiveEpiFamily X f),
        generate (Presieve.ofArrows X f) ∈
          (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y
⊢ generate T ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y

Tactic:
obtain ⟨I, _, X, f, rfl, hT⟩ := hT

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
Y : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y
hT : EffectiveEpiFamily X f
h :
  Coverage.Saturate.{v_1, u_1} (extensiveCoverage C ⊔ regularCoverage C) Y
    (generate
      (Presieve.ofArrows (fun (x : Unit) ↦ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i) fun (x : Unit) ↦ Sigma.desc f))
h₁ :
  ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄,
    arrows
        (generate
          (Presieve.ofArrows (fun (x : Unit) ↦ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i) fun (x : Unit) ↦ Sigma.desc f))
        f_1 →
      Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y_1
        (Sieve.pullback f_1 (generate (Presieve.ofArrows X f)))
⊢ generate (Presieve.ofArrows X f) ∈
    (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y

Tactic:
apply Coverage.Saturate.transitive Y (generate (Presieve.ofArrows
        (fun (_ : Unit) ↦ (∐ fun (i : I) => X i)) (fun (_ : Unit) ↦ Sigma.desc f)))

Premises used: CategoryTheory.Limits.Sigma.desc, CategoryTheory.Limits.sigmaObj, CategoryTheory.Coverage.Saturate.transitive, CategoryTheory.Sieve.generate, CategoryTheory.Presieve.ofArrows
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
Y : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y
hT : EffectiveEpiFamily X f
h :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
    (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C ⊔ regularCoverage C)) Y)
    (Presieve.ofArrows (fun (x : Unit) ↦ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i) fun (x : Unit) ↦ Sigma.desc f)
⊢ Coverage.Saturate.{v_1, u_1} (extensiveCoverage C ⊔ regularCoverage C) Y
    (generate
      (Presieve.ofArrows (fun (x : Unit) ↦ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i) fun (x : Unit) ↦ Sigma.desc f))

Tactic:
apply Coverage.Saturate.of

Premises used: CategoryTheory.Coverage.Saturate.of
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
Y : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y
hT : EffectiveEpiFamily X f
⊢ (∃ (α : Type) (x : Finite α) (X_1 : α → C) (π : (a : α) → X_1 a ⟶ Y),
      (Presieve.ofArrows (fun (x : Unit) ↦ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i) fun (x : Unit) ↦ Sigma.desc f) =
          Presieve.ofArrows X_1 π ∧
        IsIso (X := sigmaObj.{0, v_1, u_1} X_1) (Sigma.desc π)) ∨
    ∃ (X_1 : C) (f_1 : X_1 ⟶ Y),
      Eq (α := Presieve.{v_1, u_1} Y)
          (Presieve.ofArrows (fun (x : Unit) ↦ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i) fun (x : Unit) ↦ Sigma.desc f)
          (Presieve.ofArrows (fun (x : Unit) ↦ X_1) fun (x : Unit) ↦ f_1) ∧
        EffectiveEpi f_1

Tactic:
Or.inr ⟨_, Sigma.desc f, ⟨rfl, inferInstance⟩⟩

Premises used: inferInstance, And.intro, Exists.intro, CategoryTheory.Limits.Sigma.desc, Or.inr, rfl
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
Y : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y
hT : EffectiveEpiFamily X f
⊢ (∃ (α : Type) (x : Finite α) (X_1 : α → C) (π : (a : α) → X_1 a ⟶ Y),
      (Presieve.ofArrows (fun (x : Unit) ↦ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i) fun (x : Unit) ↦ Sigma.desc f) =
          Presieve.ofArrows X_1 π ∧
        IsIso (X := sigmaObj.{0, v_1, u_1} X_1) (Sigma.desc π)) ∨
    ∃ (X_1 : C) (f_1 : X_1 ⟶ Y),
      Eq (α := Presieve.{v_1, u_1} Y)
          (Presieve.ofArrows (fun (x : Unit) ↦ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i) fun (x : Unit) ↦ Sigma.desc f)
          (Presieve.ofArrows (fun (x : Unit) ↦ X_1) fun (x : Unit) ↦ f_1) ∧
        EffectiveEpi f_1

Tactic:
exact Or.inr ⟨_, Sigma.desc f, ⟨rfl, inferInstance⟩⟩

Premises used: Or.inr
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
Y_1 : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y_1
hT : EffectiveEpiFamily X f
R Y : C
i : Unit
ψ : R ⟶ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i
h :
  Sieve.pullback ψ (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f))) ∈
    (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) R
⊢ Sieve.pullback (ψ ≫ Sigma.desc f) (generate (Presieve.ofArrows X f)) ∈
    (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) R

Tactic:
rw [Sieve.pullback_comp]

Premises used: CategoryTheory.Sieve.pullback_comp
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
Y_1 : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y_1
hT : EffectiveEpiFamily X f
R Y : C
i : Unit
ψ : R ⟶ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i
h :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} (C := C) (sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i)))
    ((Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a))
      (sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i))
    (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f)))
⊢ Sieve.pullback ψ (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f))) ∈
    (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) R

Tactic:
apply pullback_stable

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
Y_1 : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y_1
hT : EffectiveEpiFamily X f
R Y : C
i : Unit
ψ : R ⟶ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i
Q E : C
e : Q ⟶ E
r : E ⟶ sigmaObj.{0, v_1, u_1} X
hq : Presieve.ofArrows X (fun (i : I) ↦ Sigma.ι X i) r
mk :
  ∀ (i : I) (e : Q ⟶ X i),
    Presieve.ofArrows X f (CategoryStruct.comp (Y := sigmaObj.{0, v_1, u_1} X) (Sigma.ι X i) (Sigma.desc f))
⊢ Presieve.ofArrows X f (r ≫ Sigma.desc f)

Tactic:
cases hq
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
Y_1 : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y_1
hT : EffectiveEpiFamily X f
R Y : C
i : Unit
ψ : R ⟶ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i
Q : C
i_1 : I
e : Q ⟶ X i_1
⊢ Presieve.ofArrows X f (CategoryStruct.comp (Y := sigmaObj.{0, v_1, u_1} X) (Sigma.ι X i_1) (Sigma.desc f))

Tactic:
simpa using Presieve.ofArrows.mk _

Premises used: CategoryTheory.Presieve.ofArrows.mk
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
Y_1 : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y_1
hT : EffectiveEpiFamily X f
R Y : C
i : Unit
ψ : R ⟶ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i
Q E : C
e : Q ⟶ E
r : E ⟶ sigmaObj.{0, v_1, u_1} X
hq : Presieve.ofArrows X (fun (i : I) ↦ Sigma.ι X i) r
⊢ e ≫ r ≫ Sigma.desc f = (e ≫ r) ≫ Sigma.desc f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
Y_1 : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y_1
hT : EffectiveEpiFamily X f
R Y : C
i : Unit
ψ : R ⟶ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i
Q E : C
e : Q ⟶ E
r : E ⟶ sigmaObj.{0, v_1, u_1} X
hq : Presieve.ofArrows X (fun (i : I) ↦ Sigma.ι X i) r
⊢ arrows (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f))) (e ≫ r)

Tactic:
exact ⟨E, e, r ≫ (Sigma.desc f), by cases hq; simpa using Presieve.ofArrows.mk _, by simp⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
Y_1 : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y_1
hT : EffectiveEpiFamily X f
R Y : C
i : Unit
ψ : R ⟶ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i
⊢ LE.le (α := Sieve.{v_1, u_1} (sigmaObj.{0, v_1, u_1} X)) (generate (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i))
    (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f)))

Tactic:
have : generate (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i) ≤
            (generate (Presieve.ofArrows X f)).pullback (Sigma.desc f) := by
          rintro Q q ⟨E, e, r, ⟨hq, rfl⟩⟩
          exact ⟨E, e, r ≫ (Sigma.desc f), by cases hq; simpa using Presieve.ofArrows.mk _, by simp⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
Y_1 : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y_1
hT : EffectiveEpiFamily X f
R Y : C
i : Unit
ψ : R ⟶ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i
this :
  LE.le (α := Sieve.{v_1, u_1} (sigmaObj.{0, v_1, u_1} X)) (generate (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i))
    (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f)))
h :
  Coverage.Saturate.{v_1, u_1} (extensiveCoverage C ⊔ regularCoverage C) (sigmaObj.{0, v_1, u_1} X)
    (generate (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i))
⊢ Membership.mem (γ := Set (Sieve.{v_1, u_1} (C := C) (sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i)))
    ((Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a))
      (sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i))
    (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f)))

Tactic:
apply Coverage.saturate_of_superset _ this

Premises used: CategoryTheory.Coverage.saturate_of_superset
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
Y_1 : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y_1
hT : EffectiveEpiFamily X f
R Y : C
i : Unit
ψ : R ⟶ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i
this :
  LE.le (α := Sieve.{v_1, u_1} (sigmaObj.{0, v_1, u_1} X)) (generate (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i))
    (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f)))
h :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} (sigmaObj.{0, v_1, u_1} X)))
    (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C ⊔ regularCoverage C))
      (sigmaObj.{0, v_1, u_1} X))
    (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i)
⊢ Coverage.Saturate.{v_1, u_1} (extensiveCoverage C ⊔ regularCoverage C) (sigmaObj.{0, v_1, u_1} X)
    (generate (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i))

Tactic:
apply Coverage.Saturate.of

Premises used: CategoryTheory.Coverage.Saturate.of
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
Y_1 : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y_1
hT : EffectiveEpiFamily X f
R Y : C
i : Unit
ψ : R ⟶ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i
this :
  LE.le (α := Sieve.{v_1, u_1} (sigmaObj.{0, v_1, u_1} X)) (generate (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i))
    (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f)))
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} (sigmaObj.{0, v_1, u_1} X)))
    (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C ⊔ regularCoverage C))
      (sigmaObj.{0, v_1, u_1} X))
    (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i)

Tactic:
Or.inl ⟨I, inferInstance, _, _, ⟨rfl, ?_⟩⟩

Premises used: Set.union, Set.Mem, setOf, inferInstance, And.intro, Exists.intro, Or.inl, rfl
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
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
B : C
S : Sieve.{v_1, u_1} B
Y_1 : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y_1
hT : EffectiveEpiFamily X f
R Y : C
i : Unit
ψ : R ⟶ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i
this :
  LE.le (α := Sieve.{v_1, u_1} (sigmaObj.{0, v_1, u_1} X)) (generate (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i))
    (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f)))
h :
  IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} X) (Y := sigmaObj.{0, v_1, u_1} X)
    (Sigma.desc fun (i : I) ↦ Sigma.ι X i)
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} (sigmaObj.{0, v_1, u_1} X)))
    (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C ⊔ regularCoverage C))
      (sigmaObj.{0, v_1, u_1} X))
    (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i)

Tactic:
refine Or.inl ⟨I, inferInstance, _, _, ⟨rfl, ?_⟩⟩

Premises used: Or.inl