-- Mathlib/CategoryTheory/Sites/Coherent/CoherentTopology.lean
theorem coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily (S : Sieve X) :
    (S ∈ (coherentTopology C) X) ↔
    (∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → (Y a ⟶ X)),
        EffectiveEpiFamily Y π ∧ (∀ a : α, (S.arrows) (π a)) )

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
a : Type
h : Finite a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
right✝ : EffectiveEpiFamily Y' π
a' : a
⊢ 𝟙 Y' a' ≫ π a' = π a'

Tactic:
simp

Result:
no goals

Proof state:
case mp.top
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), ⊤.arrows (π a)

Tactic:
exact ⟨Unit, inferInstance, fun _ => Y, fun _ => (𝟙 Y), inferInstance, by simp⟩

Result:
no goals

Proof state:
case mp.of
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
hS : T ∈ (coherentCoverage C).covering Y
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)

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

Result:
case mp.of.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Finite a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = Presieve.ofArrows Y' π
right✝ : EffectiveEpiFamily Y' π
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
h : S ∈ (coherentTopology C) X
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
induction h with
| of Y T hS =>
  obtain ⟨a, h, Y', π, h', _⟩ := hS
  refine ⟨a, h, Y', π, inferInstance, fun a' ↦ ?_⟩
  obtain ⟨rfl, _⟩ := h'
  exact ⟨Y' a', 𝟙 Y' a', π a', Presieve.ofArrows.mk a', by simp⟩
| top Y =>
  exact ⟨Unit, inferInstance, fun _ => Y, fun _ => (𝟙 Y), inferInstance, by simp⟩
| transitive Y R S _ _ a b =>
  obtain ⟨α, w, Y₁, π, ⟨h₁,h₂⟩⟩ := a
  choose β _ Y_n π_n H using fun a => b (h₂ a)
  exact ⟨(Σ a, β a), inferInstance, fun ⟨a,b⟩ => Y_n a b, fun ⟨a, b⟩ => (π_n a b) ≫ (π a),
    EffectiveEpiFamily.transitive_of_finite _ h₁ _ (fun a => (H a).1),
    fun c => (H c.fst).2 c.snd⟩

Result:
no goals

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ (∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) → S ∈ (coherentTopology C) X

Tactic:
exact coherentTopology.mem_sieves_of_hasEffectiveEpiFamily S

Result:
no goals

Proof state:
case mp.of.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Finite a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = Presieve.ofArrows Y' π
right✝ : EffectiveEpiFamily Y' π
a' : a
⊢ (Sieve.generate T).arrows (π a')

Tactic:
obtain ⟨rfl, _⟩ := h'

Result:
case mp.of.intro.intro.intro.intro.intro.refl
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
a : Type
h : Finite a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
right✝ : EffectiveEpiFamily Y' π
a' : a
⊢ (Sieve.generate (Presieve.ofArrows Y' π)).arrows (π a')

Proof state:
case mp.of.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Finite a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = Presieve.ofArrows Y' π
right✝ : EffectiveEpiFamily Y' π
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)

Tactic:
refine ⟨a, h, Y', π, inferInstance, fun a' ↦ ?_⟩

Result:
case mp.of.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Finite a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = Presieve.ofArrows Y' π
right✝ : EffectiveEpiFamily Y' π
a' : a
⊢ (Sieve.generate T).arrows (π a')

Proof state:
case mp.transitive.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : (coherentCoverage C).Saturate Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → (coherentCoverage C).Saturate Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α, ∃ (_ : Finite α), ∃ Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Finite α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (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✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : (coherentCoverage C).Saturate Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → (coherentCoverage C).Saturate Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α, ∃ (_ : Finite α), ∃ Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Finite α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
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 : α), EffectiveEpiFamily (Y_n a) (π_n a) ∧ ∀ (a_1 : β a), (Sieve.pullback (π a) S).arrows (π_n a a_1)
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ S ∈ (coherentTopology C) X → ∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
intro h

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
h : S ∈ (coherentTopology C) X
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

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

Tactic:
simp

Result:
no goals

Proof state:
case mp.of.intro.intro.intro.intro.intro.refl
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
a : Type
h : Finite a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
right✝ : EffectiveEpiFamily Y' π
a' : a
⊢ (Sieve.generate (Presieve.ofArrows Y' π)).arrows (π a')

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

Result:
no goals