-- Mathlib/CategoryTheory/Sites/Coherent/RegularTopology.lean
theorem mem_sieves_of_hasEffectiveEpi (S : Sieve X) :
    (∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π) → (S ∈ (regularTopology C) X)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
W : C
g : W ⟶ X
f : Presieve.ofArrows (fun x => Y) (fun x => π) g
⊢ ∃ e, S.arrows e ∧ 𝟙 W ≫ e = g

Tactic:
cases f

Result:
case mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
i✝ : Unit
⊢ ∃ e, S.arrows e ∧ 𝟙 Y ≫ e = π

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
W : C
g : W ⟶ X
f : Presieve.ofArrows (fun x => Y) (fun x => π) g
⊢ ∃ W_1 i e, S.arrows e ∧ i ≫ e = g

Tactic:
refine ⟨W, 𝟙 W, ?_⟩

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
W : C
g : W ⟶ X
f : Presieve.ofArrows (fun x => Y) (fun x => π) g
⊢ ∃ e, S.arrows e ∧ 𝟙 W ≫ e = g

Proof state:
case mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
i✝ : Unit
⊢ ∃ e, S.arrows e ∧ 𝟙 Y ≫ e = π

Tactic:
exact ⟨π, ⟨h.2, Category.id_comp π⟩⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
⊢ (Presieve.ofArrows (fun x => Y) fun x => π) ≤ S.arrows

Tactic:
apply Presieve.le_of_factorsThru_sieve (Presieve.ofArrows _ _) S _

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
⊢ (Presieve.ofArrows (fun x => Y) fun x => π).FactorsThru S.arrows

Proof state:
case intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
h_le : Sieve.generate (Presieve.ofArrows (fun x => Y) fun x => π) ≤ S
⊢ (regularCoverage C).Saturate X (Sieve.generate (Presieve.ofArrows (fun x => Y) fun x => π))

Tactic:
exact Coverage.Saturate.of X _ ⟨Y, π, rfl, h.1⟩

Result:
no goals

Proof state:
case intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
h_le : Sieve.generate (Presieve.ofArrows (fun x => Y) fun x => π) ≤ S
⊢ S ∈ (regularTopology C) X

Tactic:
apply Coverage.saturate_of_superset (regularCoverage C) h_le

Result:
case intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
h_le : Sieve.generate (Presieve.ofArrows (fun x => Y) fun x => π) ≤ S
⊢ (regularCoverage C).Saturate X (Sieve.generate (Presieve.ofArrows (fun x => Y) fun x => π))

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
⊢ (∃ Y π, EffectiveEpi π ∧ S.arrows π) → S ∈ (regularTopology C) X

Tactic:
rintro ⟨Y, π, h⟩

Result:
case intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
⊢ S ∈ (regularTopology C) X

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
⊢ Sieve.generate (Presieve.ofArrows (fun x => Y) fun x => π) ≤ S

Tactic:
rw [Sieve.generate_le_iff (Presieve.ofArrows _ _) S]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
⊢ (Presieve.ofArrows (fun x => Y) fun x => π) ≤ S.arrows

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
⊢ (Presieve.ofArrows (fun x => Y) fun x => π).FactorsThru S.arrows

Tactic:
intro W g f

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
W : C
g : W ⟶ X
f : Presieve.ofArrows (fun x => Y) (fun x => π) g
⊢ ∃ W_1 i e, S.arrows e ∧ i ≫ e = g

Proof state:
case intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
⊢ S ∈ (regularTopology C) X

Tactic:
have h_le : Sieve.generate (Presieve.ofArrows (fun () ↦ Y) (fun _ ↦ π)) ≤ S := by
  rw [Sieve.generate_le_iff (Presieve.ofArrows _ _) S]
  apply Presieve.le_of_factorsThru_sieve (Presieve.ofArrows _ _) S _
  intro W g f
  refine ⟨W, 𝟙 W, ?_⟩
  cases f
  exact ⟨π, ⟨h.2, Category.id_comp π⟩⟩

Result:
case intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
h_le : Sieve.generate (Presieve.ofArrows (fun x => Y) fun x => π) ≤ S
⊢ S ∈ (regularTopology C) X