-- Mathlib/CategoryTheory/Sites/Coherent/Comparison.lean
theorem extensive_regular_generate_coherent [Preregular C] [FinitaryPreExtensive C] :
    ((extensiveCoverage C) ⊔ (regularCoverage C)).toGrothendieck =
    (coherentTopology C)

Proof state:
case h.h.h.refine_2.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro.mk.hS.hS
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y✝ : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y✝
hT : EffectiveEpiFamily X f
R Y : C
i✝ : Unit
ψ : R ⟶ ∐ fun i => X i
this :
  generate (Presieve.ofArrows X fun i => Sigma.ι X i) ≤ Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f))
⊢ IsIso (Sigma.desc fun i => Sigma.ι X i)

Tactic:
convert IsIso.id _

Result:
case h.e'_5.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y✝ : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y✝
hT : EffectiveEpiFamily X f
R Y : C
i✝ : Unit
ψ : R ⟶ ∐ fun i => X i
this :
  generate (Presieve.ofArrows X fun i => Sigma.ι X i) ≤ Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f))
e_4✝ : ∐ X = ∐ X
⊢ (Sigma.desc fun i => Sigma.ι X i) = 𝟙 (∐ X)

Proof state:
case h.h.h.refine_2.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro.mk
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y✝ : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y✝
hT : EffectiveEpiFamily X f
R Y : C
i✝ : Unit
ψ : R ⟶ ∐ fun i => X i
⊢ Sieve.pullback (ψ ≫ Sigma.desc f) (generate (Presieve.ofArrows X f)) ∈
    (Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C)) R

Tactic:
rw [Sieve.pullback_comp]

Result:
case h.h.h.refine_2.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro.mk
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y✝ : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y✝
hT : EffectiveEpiFamily X f
R Y : C
i✝ : Unit
ψ : R ⟶ ∐ fun i => X i
⊢ Sieve.pullback ψ (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f))) ∈
    (Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C)) R

Proof state:
case h.h.h.refine_2.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro.mk.hS
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y✝ : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y✝
hT : EffectiveEpiFamily X f
R Y : C
i✝ : Unit
ψ : R ⟶ ∐ fun i => X i
this :
  generate (Presieve.ofArrows X fun i => Sigma.ι X i) ≤ Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f))
⊢ Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f)) ∈
    (Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C)) (∐ fun i => X i)

Tactic:
apply Coverage.saturate_of_superset _ this

Result:
case h.h.h.refine_2.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro.mk.hS
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y✝ : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y✝
hT : EffectiveEpiFamily X f
R Y : C
i✝ : Unit
ψ : R ⟶ ∐ fun i => X i
this :
  generate (Presieve.ofArrows X fun i => Sigma.ι X i) ≤ Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f))
⊢ (extensiveCoverage C ⊔ regularCoverage C).Saturate (∐ X) (generate (Presieve.ofArrows X fun i => Sigma.ι X i))

Proof state:
case h.h.h.refine_2.of.intro.intro.intro.intro.intro.a
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y
hT : EffectiveEpiFamily X f
⊢ (extensiveCoverage C ⊔ regularCoverage C).Saturate Y
    (generate (Presieve.ofArrows (fun x => ∐ fun i => X i) fun x => Sigma.desc f))

Tactic:
apply Coverage.Saturate.of

Result:
case h.h.h.refine_2.of.intro.intro.intro.intro.intro.a.hS
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y
hT : EffectiveEpiFamily X f
⊢ (Presieve.ofArrows (fun x => ∐ fun i => X i) fun x => Sigma.desc f) ∈
    (extensiveCoverage C ⊔ regularCoverage C).covering Y

Proof state:
case h.h.h.refine_2.of.intro.intro.intro.intro.intro
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y
hT : EffectiveEpiFamily X f
⊢ generate (Presieve.ofArrows X f) ∈ (Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C)) Y

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

Result:
case h.h.h.refine_2.of.intro.intro.intro.intro.intro.a
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y
hT : EffectiveEpiFamily X f
⊢ (extensiveCoverage C ⊔ regularCoverage C).Saturate Y
    (generate (Presieve.ofArrows (fun x => ∐ fun i => X i) fun x => Sigma.desc f))

case h.h.h.refine_2.of.intro.intro.intro.intro.intro.a
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y
hT : EffectiveEpiFamily X f
⊢ ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄,
    (generate (Presieve.ofArrows (fun x => ∐ fun i => X i) fun x => Sigma.desc f)).arrows f_1 →
      (extensiveCoverage C ⊔ regularCoverage C).Saturate Y_1 (Sieve.pullback f_1 (generate (Presieve.ofArrows X f)))

Proof state:
case h.h.h.refine_1.of.hS
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y : C
T : Presieve Y
hT : T ∈ (extensiveCoverage C).covering Y ∨ T ∈ (regularCoverage C).covering Y
⊢ T ∈ (coherentCoverage C).covering Y

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⟩⟩)

Result:
no goals

Proof state:
case h.h.h.refine_2.of
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y : C
T : Presieve Y
hT : T ∈ (coherentCoverage C).covering Y
⊢ generate T ∈ (Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C)) Y

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

Result:
case h.h.h.refine_2.of.intro.intro.intro.intro.intro
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y
hT : EffectiveEpiFamily X f
⊢ generate (Presieve.ofArrows X f) ∈ (Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C)) Y