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

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

Tactic:
intro h

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

Proof state:
case mp.of
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
T : Presieve Y
hS : T ∈ (regularCoverage C).covering Y
⊢ ∃ Y_1 π, EffectiveEpi π ∧ (Sieve.generate T).arrows π

Tactic:
rcases hS with ⟨Y', π, h'⟩

Result:
case mp.of.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
T : Presieve Y
Y' : C
π : Y' ⟶ Y
h' : (T = Presieve.ofArrows (fun x => Y') fun x => π) ∧ EffectiveEpi π
⊢ ∃ Y_1 π, EffectiveEpi π ∧ (Sieve.generate T).arrows π

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : (regularCoverage C).Saturate Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → (regularCoverage C).Saturate Y_1 (Sieve.pullback f S)
b : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → ∃ Y_2 π, EffectiveEpi π ∧ (Sieve.pullback f S).arrows π
Y₁ : C
π : Y₁ ⟶ Y
h₁ : EffectiveEpi π
h₂ : R.arrows π
Y' : C
π' : Y' ⟶ Y₁
h✝ : EffectiveEpi π'
H : (Sieve.pullback π S).arrows π'
⊢ S.arrows (π' ≫ π)

Tactic:
simpa using H

Result:
no goals

Proof state:
case mp.transitive.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : (regularCoverage C).Saturate Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → (regularCoverage C).Saturate Y_1 (Sieve.pullback f S)
b : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → ∃ Y_2 π, EffectiveEpi π ∧ (Sieve.pullback f S).arrows π
Y₁ : C
π : Y₁ ⟶ Y
h₁ : EffectiveEpi π
h₂ : R.arrows π
Y' : C
π' : Y' ⟶ Y₁
h✝ : EffectiveEpi π'
H : (Sieve.pullback π S).arrows π'
⊢ ∃ Y_1 π, EffectiveEpi π ∧ S.arrows π

Tactic:
exact ⟨Y', π' ≫ π, inferInstance, (by simpa using H)⟩

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 Y' : C
π : Y' ⟶ Y
right✝ : EffectiveEpi π
⊢ 𝟙 Y' ≫ π = π

Tactic:
simp

Result:
no goals

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

Tactic:
rcases h' with ⟨rfl, _⟩

Result:
case mp.of.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y Y' : C
π : Y' ⟶ Y
right✝ : EffectiveEpi π
⊢ (Sieve.generate (Presieve.ofArrows (fun x => Y') fun x => π)).arrows π

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

Tactic:
refine ⟨Y', π, h'.2, ?_⟩

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

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

Tactic:
induction h with
| of Y T hS =>
  rcases hS with ⟨Y', π, h'⟩
  refine ⟨Y', π, h'.2, ?_⟩
  rcases h' with ⟨rfl, _⟩
  exact ⟨Y', 𝟙 Y', π, Presieve.ofArrows.mk (), (by simp)⟩
| top Y => exact ⟨Y, (𝟙 Y), inferInstance, by simp only [Sieve.top_apply, forall_const]⟩
| transitive Y R S _ _ a b =>
  rcases a with ⟨Y₁, π, ⟨h₁,h₂⟩⟩
  choose Y' π' _ H using b h₂
  exact ⟨Y', π' ≫ π, inferInstance, (by simpa using H)⟩

Result:
no goals

Proof state:
case mp.transitive.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : (regularCoverage C).Saturate Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → (regularCoverage C).Saturate Y_1 (Sieve.pullback f S)
b : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → ∃ Y_2 π, EffectiveEpi π ∧ (Sieve.pullback f S).arrows π
Y₁ : C
π : Y₁ ⟶ Y
h₁ : EffectiveEpi π
h₂ : R.arrows π
⊢ ∃ Y_1 π, EffectiveEpi π ∧ S.arrows π

Tactic:
choose Y' π' _ H using b h₂

Result:
case mp.transitive.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : (regularCoverage C).Saturate Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → (regularCoverage C).Saturate Y_1 (Sieve.pullback f S)
b : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → ∃ Y_2 π, EffectiveEpi π ∧ (Sieve.pullback f S).arrows π
Y₁ : C
π : Y₁ ⟶ Y
h₁ : EffectiveEpi π
h₂ : R.arrows π
Y' : C
π' : Y' ⟶ Y₁
h✝ : EffectiveEpi π'
H : (Sieve.pullback π S).arrows π'
⊢ ∃ Y_1 π, EffectiveEpi π ∧ S.arrows π

Proof state:
case mp.of.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y Y' : C
π : Y' ⟶ Y
right✝ : EffectiveEpi π
⊢ (Sieve.generate (Presieve.ofArrows (fun x => Y') fun x => π)).arrows π

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

Result:
no goals

Proof state:
case mp.top
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
⊢ ∃ Y_1 π, EffectiveEpi π ∧ ⊤.arrows π

Tactic:
exact ⟨Y, (𝟙 Y), inferInstance, by simp only [Sieve.top_apply, forall_const]⟩

Result:
no goals

Proof state:
case mpr
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:
exact regularTopology.mem_sieves_of_hasEffectiveEpi S

Result:
no goals

Proof state:
case mp.transitive
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : (regularCoverage C).Saturate Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → (regularCoverage C).Saturate Y_1 (Sieve.pullback f S)
a : ∃ Y_1 π, EffectiveEpi π ∧ R.arrows π
b : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → ∃ Y_2 π, EffectiveEpi π ∧ (Sieve.pullback f S).arrows π
⊢ ∃ Y_1 π, EffectiveEpi π ∧ S.arrows π

Tactic:
rcases a with ⟨Y₁, π, ⟨h₁,h₂⟩⟩

Result:
case mp.transitive.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preregular C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : (regularCoverage C).Saturate Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → (regularCoverage C).Saturate Y_1 (Sieve.pullback f S)
b : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → ∃ Y_2 π, EffectiveEpi π ∧ (Sieve.pullback f S).arrows π
Y₁ : C
π : Y₁ ⟶ Y
h₁ : EffectiveEpi π
h₂ : R.arrows π
⊢ ∃ Y_1 π, EffectiveEpi π ∧ 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
⊢ ⊤.arrows (𝟙 Y)

Tactic:
simp only [Sieve.top_apply, forall_const]

Result:
no goals

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

Tactic:
constructor

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

case mpr
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