-- Mathlib/CategoryTheory/Sites/Coherent/ExtensiveTopology.lean
lemma extensiveTopology.mem_sieves_iff_contains_colimit_cofan {X : C} (S : Sieve X) :
    S ∈ (extensiveTopology C) X ↔
      (∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → (Y a ⟶ X)),
        Nonempty (IsColimit (Cofan.mk X π)) ∧ (∀ a : α, (S.arrows) (π a)))

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
⊢ (∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)) →
    S ∈ (extensiveTopology C) X

Tactic:
intro ⟨α, _, Y, π, h, h'⟩

Result:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
⊢ S ∈ (extensiveTopology C) X

Proof state:
case mp.of.intro.intro.intro.intro.intro.refine_1
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : S = Presieve.ofArrows Y π
h' : IsIso (Sigma.desc π)
⊢ Nonempty (IsColimit (Cofan.mk X π))

Tactic:
have : IsIso (Sigma.desc (Cofan.mk X π).inj) := by simpa using h'

Result:
case mp.of.intro.intro.intro.intro.intro.refine_1
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : S = Presieve.ofArrows Y π
h' : IsIso (Sigma.desc π)
this : IsIso (Sigma.desc (Cofan.mk X π).inj)
⊢ Nonempty (IsColimit (Cofan.mk X π))

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S : Sieve X✝
X : C
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h' : IsIso (Sigma.desc π)
a : α
⊢ 𝟙 Y a ≫ π a = π a

Tactic:
simp

Result:
no goals

Proof state:
case mp.of.intro.intro.intro.intro.intro.refine_1
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : S = Presieve.ofArrows Y π
h' : IsIso (Sigma.desc π)
this : IsIso (Sigma.desc (Cofan.mk X π).inj)
⊢ Nonempty (IsColimit (Cofan.mk X π))

Tactic:
exact ⟨Cofan.isColimitOfIsIsoSigmaDesc (Cofan.mk X π)⟩

Result:
no goals

Proof state:
case mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
i✝ : α
⊢ π i✝ ∈ S.arrows

Tactic:
exact h' _

Result:
no goals

Proof state:
case mpr.hR
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
⊢ IsIso (Sigma.desc π)

Tactic:
rw [show IsIso (Sigma.desc π) ↔ _ from
  Limits.Cofan.isColimit_iff_isIso_sigmaDesc (c := Cofan.mk X π)]

Result:
case mpr.hR
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
⊢ Nonempty (IsColimit (Cofan.mk X π))

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
⊢ S ∈ (extensiveTopology C) X ↔
    ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
⊢ S ∈ (extensiveTopology C) X →
    ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)

case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
⊢ (∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)) →
    S ∈ (extensiveTopology C) X

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
⊢ S ∈ (extensiveTopology C) X

Tactic:
apply (extensiveCoverage C).mem_toGrothendieck_sieves_of_superset (R := Presieve.ofArrows Y π)

Result:
case mpr.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
⊢ Presieve.ofArrows Y π ≤ S.arrows

case mpr.hR
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
⊢ Presieve.ofArrows Y π ∈ (extensiveCoverage C).covering X

Proof state:
case mp.transitive.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : (extensiveCoverage C).Saturate X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → (extensiveCoverage C).Saturate Y (Sieve.pullback f S)
b :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∃ α, ∃ (_ : Finite α), ∃ Y_1 π, Nonempty (IsColimit (Cofan.mk Y π)) ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Finite α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), R.arrows (π a)
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)

Tactic:
choose β _ Y_n π_n H using fun a => b (h' a)

Result:
case mp.transitive.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : (extensiveCoverage C).Saturate X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → (extensiveCoverage C).Saturate Y (Sieve.pullback f S)
b :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∃ α, ∃ (_ : Finite α), ∃ Y_1 π, Nonempty (IsColimit (Cofan.mk Y π)) ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Finite α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), R.arrows (π a)
β : α → Type
x✝ : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (a_1 : β a) → Y_n a a_1 ⟶ Y₁ a
H :
  ∀ (a : α), Nonempty (IsColimit (Cofan.mk (Y₁ a) (π_n a))) ∧ ∀ (a_1 : β a), (Sieve.pullback (π a) S).arrows (π_n a a_1)
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)

Proof state:
case mp.top
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S : Sieve X✝
X : C
⊢ IsColimit (Cofan.mk X fun x => 𝟙 X)

Tactic:
have : IsIso (Sigma.desc (Cofan.mk X fun (_ : Unit) ↦ 𝟙 X).inj) := by
  have : IsIso (coproductUniqueIso (fun () => X)).hom := inferInstance
  exact this

Result:
case mp.top
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S : Sieve X✝
X : C
this : IsIso (Sigma.desc (Cofan.mk X fun x => 𝟙 X).inj)
⊢ IsColimit (Cofan.mk X fun x => 𝟙 X)

Proof state:
case mpr.hR
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
⊢ Presieve.ofArrows Y π ∈ (extensiveCoverage C).covering X

Tactic:
refine ⟨α, inferInstance, Y, π, rfl, ?_⟩

Result:
case mpr.hR
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
⊢ IsIso (Sigma.desc π)