-- 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.transitive
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 S✝ : Sieve Y
a✝¹ : (coherentCoverage C).Saturate Y T
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → (coherentCoverage C).Saturate Y_1 (Sieve.pullback f S✝)
a_ih✝¹ : T ∈ (Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C)) Y
a_ih✝ :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Sieve.pullback f S✝ ∈ (Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C)) Y_1
⊢ S✝ ∈ (Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C)) Y

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

Result:
no goals

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 ⊔ regularCoverage C).covering Y
⊢ T ∈ (coherentCoverage C).covering Y

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

Result:
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

Proof state:
case 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
R Y : C
i✝ : Unit
ψ : R ⟶ ∐ fun i => X i
Q E : C
e : Q ⟶ E
r : E ⟶ ∐ X
hq : Presieve.ofArrows X (fun i => Sigma.ι X i) r
⊢ (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f))).arrows (e ≫ r)

Tactic:
exact ⟨E, e, r ≫ (Sigma.desc f), by cases hq; simpa using Presieve.ofArrows.mk _, by simp⟩

Result:
no goals

Proof state:
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
Q E : C
e : Q ⟶ E
r : E ⟶ ∐ X
hq : Presieve.ofArrows X (fun i => Sigma.ι X i) r
⊢ e ≫ r ≫ Sigma.desc f = (e ≫ r) ≫ Sigma.desc f

Tactic:
simp

Result:
no goals

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
⊢ Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f)) ∈
    (Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C)) (∐ fun i => X i)

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⟩

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))
⊢ Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f)) ∈
    (Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C)) (∐ fun i => X i)

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 ψ (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f))) ∈
    (Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C)) R

Tactic:
apply pullback_stable

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
⊢ Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f)) ∈
    (Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C)) (∐ fun i => 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
⊢ ∀ ⦃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)))

Tactic:
rintro R g ⟨W, ψ, σ, ⟨⟩, rfl⟩

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
⊢ (extensiveCoverage C ⊔ regularCoverage C).Saturate R
    (Sieve.pullback (ψ ≫ Sigma.desc f) (generate (Presieve.ofArrows X f)))

Proof state:
case 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
Q : C
i✝ : I
e : Q ⟶ X i✝
⊢ Presieve.ofArrows X f (Sigma.ι X i✝ ≫ Sigma.desc f)

Tactic:
simpa using Presieve.ofArrows.mk _

Result:
no goals

Proof state:
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)

Tactic:
aesop

Result:
no goals

Proof state:
case h.h.h.refine_1.top
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
X✝ : C
⊢ ⊤ ∈ (coherentTopology C) X✝

Tactic:
apply Coverage.Saturate.top

Result:
no goals

Proof state:
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
Q E : C
e : Q ⟶ E
r : E ⟶ ∐ X
hq : Presieve.ofArrows X (fun i => Sigma.ι X i) r
⊢ Presieve.ofArrows X f (r ≫ Sigma.desc f)

Tactic:
cases hq

Result:
case 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
Q : C
i✝ : I
e : Q ⟶ X i✝
⊢ Presieve.ofArrows X f (Sigma.ι X i✝ ≫ Sigma.desc f)