-- 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:
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 π)
⊢ IsIso (Sigma.desc (Cofan.mk X π).inj)

Tactic:
simpa using h'

Result:
no goals

Proof state:
case mp.of
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ (extensiveCoverage C).covering X
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), (Sieve.generate S).arrows (π a)

Tactic:
obtain ⟨α, _, Y, π, h, h'⟩ := hS

Result:
case mp.of.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
S : Presieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : S = Presieve.ofArrows Y π
h' : IsIso (Sigma.desc π)
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), (Sieve.generate 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
this : IsIso (Sigma.desc (Cofan.mk X fun x => 𝟙 X).inj)
⊢ IsColimit (Cofan.mk X fun x => 𝟙 X)

Tactic:
exact Cofan.isColimitOfIsIsoSigmaDesc (Cofan.mk X _)

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S : Sieve X✝
X : C
this : IsIso (coproductUniqueIso fun x => X).hom
⊢ IsIso (Sigma.desc (Cofan.mk X fun x => 𝟙 X).inj)

Tactic:
exact this

Result:
no goals

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

Tactic:
intro h

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

Proof state:
case mp.transitive
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)
a : ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), R.arrows (π a)
b :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∃ α, ∃ (_ : Finite α), ∃ Y_1 π, Nonempty (IsColimit (Cofan.mk Y π)) ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)

Tactic:
obtain ⟨α, w, Y₁, π, h, 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)
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)

Proof state:
case mp.of.intro.intro.intro.intro.intro.refine_2
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 π)
a : α
⊢ (Sieve.generate S).arrows (π a)

Tactic:
obtain ⟨rfl, _⟩ := h

Result:
case mp.of.intro.intro.intro.intro.intro.refine_2.refl
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 : α
⊢ (Sieve.generate (Presieve.ofArrows Y π)).arrows (π a)

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)
⊢ Nonempty (IsColimit (Cofan.mk X π))

Tactic:
exact h

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S : Sieve X✝
X : C
⊢ ∀ (a : Unit), ⊤.arrows ((fun x => 𝟙 X) a)

Tactic:
simp

Result:
no goals

Proof state:
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)
x✝¹ : C
x✝ : x✝¹ ⟶ X
hh : x✝ ∈ Presieve.ofArrows Y π
⊢ x✝ ∈ S.arrows

Tactic:
cases hh

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

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S : Sieve X✝
X : C
⊢ IsIso (Sigma.desc (Cofan.mk X fun x => 𝟙 X).inj)

Tactic:
have : IsIso (coproductUniqueIso (fun () => X)).hom := inferInstance

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

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

Tactic:
exact fun _ _ hh ↦ by cases hh; exact h' _

Result:
no goals

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)
β : α → 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)

Tactic:
exact ⟨(Σ a, β a), inferInstance, fun ⟨a,b⟩ => Y_n a b, fun ⟨a, b⟩ => (π_n a b) ≫ (π a),
  ⟨Limits.Cofan.isColimitTrans _ h.some _ (fun a ↦ (H a).1.some)⟩,
  fun c => (H c.fst).2 c.snd⟩

Result:
no goals

Proof state:
case mp.of.intro.intro.intro.intro.intro.refine_2.refl
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 : α
⊢ (Sieve.generate (Presieve.ofArrows Y π)).arrows (π a)

Tactic:
exact ⟨Y a, 𝟙 Y a, π a, Presieve.ofArrows.mk a, by simp⟩

Result:
no goals