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

Tactic:
change _ ∈ ((extensiveCoverage C) ⊔ (regularCoverage C)).toGrothendieck _ R

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

Proof state:
case h.h.h.refine_2.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
⊢ ⊤ ∈ (Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C)) X✝

Tactic:
apply Coverage.Saturate.top

Result:
no goals

Proof state:
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
⊢ (∃ α,
      ∃ (x : Finite α),
        ∃ X_1 π,
          (Presieve.ofArrows (fun x => ∐ fun i => X i) fun x => Sigma.desc f) = Presieve.ofArrows X_1 π ∧
            IsIso (Sigma.desc π)) ∨
    ∃ X_1 f_1,
      ((Presieve.ofArrows (fun x => ∐ fun i => X i) fun x => Sigma.desc f) =
          Presieve.ofArrows (fun x => X_1) fun x => f_1) ∧
        EffectiveEpi f_1

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

Result:
no goals

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

Tactic:
simp only [Coverage.sup_covering, extensiveCoverage, regularCoverage, Set.mem_union,
  Set.mem_setOf_eq]

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
⊢ (∃ α,
      ∃ (x : Finite α),
        ∃ X_1 π,
          (Presieve.ofArrows (fun x => ∐ fun i => X i) fun x => Sigma.desc f) = Presieve.ofArrows X_1 π ∧
            IsIso (Sigma.desc π)) ∨
    ∃ X_1 f_1,
      ((Presieve.ofArrows (fun x => ∐ fun i => X i) fun x => Sigma.desc f) =
          Presieve.ofArrows (fun x => X_1) fun x => f_1) ∧
        EffectiveEpi f_1

Proof state:
case h.h.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
⊢ S ∈ (Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C)) B ↔ S ∈ (coherentTopology C) B

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case h.h.h.refine_1
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
h : S ∈ (Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C)) B
⊢ S ∈ (coherentTopology C) B

case h.h.h.refine_2
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
h : S ∈ (coherentTopology C) B
⊢ S ∈ (Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C)) B

Proof state:
case h.h.h.refine_1.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✝¹ : (extensiveCoverage C ⊔ regularCoverage C).Saturate Y T
a✝ :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → (extensiveCoverage C ⊔ regularCoverage C).Saturate Y_1 (Sieve.pullback f S✝)
a_ih✝¹ : T ∈ (coherentTopology C) Y
a_ih✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Sieve.pullback f S✝ ∈ (coherentTopology C) Y_1
⊢ S✝ ∈ (coherentTopology C) Y

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

Result:
no goals

Proof state:
case h.h.h.refine_1.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 ∈ (extensiveCoverage C ⊔ regularCoverage C).covering Y
⊢ generate T ∈ (coherentTopology C) Y

Tactic:
apply Coverage.Saturate.of

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

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
⊢ generate (Presieve.ofArrows X fun i => Sigma.ι X i) ≤ Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f))

Tactic:
rintro Q q ⟨E, e, r, ⟨hq, rfl⟩⟩

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

Proof state:
case h.h.h.refine_1
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
h : S ∈ (Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C)) B
⊢ S ∈ (coherentTopology C) 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]

Result:
no goals