Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily (ExtrDisc/Topologies.lean)

State before:
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ (∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) ↔
    S ∈ GrothendieckTopology.sieves (coherentTopology C) X
Tactic:
constructor
State after:
case mp
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ (∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) →
    S ∈ GrothendieckTopology.sieves (coherentTopology C) X

case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology C) X → ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mp
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ (∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) →
    S ∈ GrothendieckTopology.sieves (coherentTopology C) X
Tactic:
exact coherentTopology.Sieve_of_has_EffectiveEpiFamily X S
State after:
no goals

State before:
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology C) X → ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
intro h
State after:
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
h : S ∈ GrothendieckTopology.sieves (coherentTopology C) X
⊢ ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
h : S ∈ GrothendieckTopology.sieves (coherentTopology C) X
⊢ ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
induction' h with Y T hS  Y Y R S _ _ a b
State after:
case mpr.of
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
hS : T ∈ Coverage.covering (coherentCoverage C) Y
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)

case mpr.top
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), ⊤.arrows (π a)

case mpr.transitive
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
a : ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), R.arrows (π a)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr.of
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
hS : T ∈ Coverage.covering (coherentCoverage C) Y
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)
Tactic:
rcases hS with ⟨a, h, Y', π, h'⟩
State after:
case mpr.of.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = ofArrows Y' π ∧ EffectiveEpiFamily Y' π
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)

State before:
case mpr.of.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = ofArrows Y' π ∧ EffectiveEpiFamily Y' π
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)
Tactic:
use a, h, Y', π
State after:
case mpr.of.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = ofArrows Y' π ∧ EffectiveEpiFamily Y' π
⊢ EffectiveEpiFamily Y' π ∧ ∀ (a : a), (Sieve.generate T).arrows (π a)

State before:
case mpr.of.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = ofArrows Y' π ∧ EffectiveEpiFamily Y' π
⊢ EffectiveEpiFamily Y' π ∧ ∀ (a : a), (Sieve.generate T).arrows (π a)
Tactic:
constructor
State after:
case mpr.of.intro.intro.intro.intro.left
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = ofArrows Y' π ∧ EffectiveEpiFamily Y' π
⊢ EffectiveEpiFamily Y' π

case mpr.of.intro.intro.intro.intro.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = ofArrows Y' π ∧ EffectiveEpiFamily Y' π
⊢ ∀ (a : a), (Sieve.generate T).arrows (π a)

State before:
case mpr.of.intro.intro.intro.intro.left
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = ofArrows Y' π ∧ EffectiveEpiFamily Y' π
⊢ EffectiveEpiFamily Y' π
Tactic:
tauto
State after:
no goals

State before:
case mpr.of.intro.intro.intro.intro.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = ofArrows Y' π ∧ EffectiveEpiFamily Y' π
⊢ ∀ (a : a), (Sieve.generate T).arrows (π a)
Tactic:
intro a'
State after:
case mpr.of.intro.intro.intro.intro.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = ofArrows Y' π ∧ EffectiveEpiFamily Y' π
a' : a
⊢ (Sieve.generate T).arrows (π a')

State before:
case mpr.of.intro.intro.intro.intro.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = ofArrows Y' π ∧ EffectiveEpiFamily Y' π
a' : a
⊢ (Sieve.generate T).arrows (π a')
Tactic:
cases' h' with h_left h_right
State after:
case mpr.of.intro.intro.intro.intro.right.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
a' : a
h_left : T = ofArrows Y' π
h_right : EffectiveEpiFamily Y' π
⊢ (Sieve.generate T).arrows (π a')

State before:
case mpr.of.intro.intro.intro.intro.right.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
a' : a
h_left : T = ofArrows Y' π
h_right : EffectiveEpiFamily Y' π
⊢ (Sieve.generate T).arrows (π a')
Tactic:
simp only [Sieve.generate_apply]
State after:
case mpr.of.intro.intro.intro.intro.right.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
a' : a
h_left : T = ofArrows Y' π
h_right : EffectiveEpiFamily Y' π
⊢ ∃ Y_1 h g, T g ∧ h ≫ g = π a'

State before:
case mpr.of.intro.intro.intro.intro.right.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
a' : a
h_left : T = ofArrows Y' π
h_right : EffectiveEpiFamily Y' π
⊢ ∃ Y_1 h g, T g ∧ h ≫ g = π a'
Tactic:
use Y' a', 𝟙 Y' a', π a'
State after:
case mpr.of.intro.intro.intro.intro.right.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
a' : a
h_left : T = ofArrows Y' π
h_right : EffectiveEpiFamily Y' π
⊢ T (π a') ∧ 𝟙 Y' a' ≫ π a' = π a'

State before:
case mpr.of.intro.intro.intro.intro.right.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
a' : a
h_left : T = ofArrows Y' π
h_right : EffectiveEpiFamily Y' π
⊢ T (π a') ∧ 𝟙 Y' a' ≫ π a' = π a'
Tactic:
constructor
State after:
case mpr.of.intro.intro.intro.intro.right.intro.left
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
a' : a
h_left : T = ofArrows Y' π
h_right : EffectiveEpiFamily Y' π
⊢ T (π a')

case mpr.of.intro.intro.intro.intro.right.intro.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
a' : a
h_left : T = ofArrows Y' π
h_right : EffectiveEpiFamily Y' π
⊢ 𝟙 Y' a' ≫ π a' = π a'

State before:
case mpr.of.intro.intro.intro.intro.right.intro.left
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
a' : a
h_left : T = ofArrows Y' π
h_right : EffectiveEpiFamily Y' π
⊢ T (π a')
Tactic:
rw [h_left]
State after:
case mpr.of.intro.intro.intro.intro.right.intro.left
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
a' : a
h_left : T = ofArrows Y' π
h_right : EffectiveEpiFamily Y' π
⊢ ofArrows Y' π (π a')

State before:
case mpr.of.intro.intro.intro.intro.right.intro.left
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
a' : a
h_left : T = ofArrows Y' π
h_right : EffectiveEpiFamily Y' π
⊢ ofArrows Y' π (π a')
Tactic:
exact Presieve.ofArrows.mk a'
State after:
no goals

State before:
case mpr.of.intro.intro.intro.intro.right.intro.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
a : Type
h : Fintype a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
a' : a
h_left : T = ofArrows Y' π
h_right : EffectiveEpiFamily Y' π
⊢ 𝟙 Y' a' ≫ π a' = π a'
Tactic:
apply Category.id_comp
State after:
no goals

State before:
case mpr.top
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), ⊤.arrows (π a)
Tactic:
use Unit, Unit.fintype, fun _ => Y, fun _ => (𝟙 Y)
State after:
case mpr.top
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
⊢ (EffectiveEpiFamily (fun x => Y) fun x => 𝟙 Y) ∧ ∀ (a : Unit), ⊤.arrows ((fun x => 𝟙 Y) a)

State before:
case mpr.top
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
⊢ (EffectiveEpiFamily (fun x => Y) fun x => 𝟙 Y) ∧ ∀ (a : Unit), ⊤.arrows ((fun x => 𝟙 Y) a)
Tactic:
cases' S with arrows downward_closed
State after:
case mpr.top.mk
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X Y : C
arrows : Presieve X
downward_closed : ∀ {Y Z : C} {f : Y ⟶ X}, arrows f → ∀ (g : Z ⟶ Y), arrows (g ≫ f)
⊢ (EffectiveEpiFamily (fun x => Y) fun x => 𝟙 Y) ∧ ∀ (a : Unit), ⊤.arrows ((fun x => 𝟙 Y) a)

State before:
case mpr.top.mk
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X Y : C
arrows : Presieve X
downward_closed : ∀ {Y Z : C} {f : Y ⟶ X}, arrows f → ∀ (g : Z ⟶ Y), arrows (g ≫ f)
⊢ (EffectiveEpiFamily (fun x => Y) fun x => 𝟙 Y) ∧ ∀ (a : Unit), ⊤.arrows ((fun x => 𝟙 Y) a)
Tactic:
constructor
State after:
case mpr.top.mk.left
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X Y : C
arrows : Presieve X
downward_closed : ∀ {Y Z : C} {f : Y ⟶ X}, arrows f → ∀ (g : Z ⟶ Y), arrows (g ≫ f)
⊢ EffectiveEpiFamily (fun x => Y) fun x => 𝟙 Y

case mpr.top.mk.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X Y : C
arrows : Presieve X
downward_closed : ∀ {Y Z : C} {f : Y ⟶ X}, arrows f → ∀ (g : Z ⟶ Y), arrows (g ≫ f)
⊢ ∀ (a : Unit), ⊤.arrows ((fun x => 𝟙 Y) a)

State before:
case mpr.top.mk.left
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X Y : C
arrows : Presieve X
downward_closed : ∀ {Y Z : C} {f : Y ⟶ X}, arrows f → ∀ (g : Z ⟶ Y), arrows (g ≫ f)
⊢ EffectiveEpiFamily (fun x => Y) fun x => 𝟙 Y
Tactic:
exact inferInstance
State after:
no goals

State before:
case mpr.top.mk.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X Y : C
arrows : Presieve X
downward_closed : ∀ {Y Z : C} {f : Y ⟶ X}, arrows f → ∀ (g : Z ⟶ Y), arrows (g ≫ f)
⊢ ∀ (a : Unit), ⊤.arrows ((fun x => 𝟙 Y) a)
Tactic:
simp only [Sieve.top_apply, forall_const]
State after:
no goals

State before:
case mpr.transitive
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
a : ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), R.arrows (π a)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rcases a with ⟨α, w, Y₁, π, ⟨h₁,h₂⟩⟩
State after:
case mpr.transitive.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr.transitive.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
have H : ∀ a : α, ∃ (β : Type) (_ : Fintype β) (Y_n : β → C)
    (π_n: (b : β) →  (Y_n b)⟶ Y₁ a),
      EffectiveEpiFamily Y_n π_n ∧ (∀ b : β, (S.pullback (π a)).arrows (π_n b)) :=
  fun a => b (h₂ a)
State after:
case mpr.transitive.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
H : ∀ (a : α), ∃ β x Y_n π_n, EffectiveEpiFamily Y_n π_n ∧ ∀ (b : β), (Sieve.pullback (π a) S).arrows (π_n b)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr.transitive.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
H : ∀ (a : α), ∃ β x Y_n π_n, EffectiveEpiFamily Y_n π_n ∧ ∀ (b : β), (Sieve.pullback (π a) S).arrows (π_n b)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rw [Classical.skolem] at H
State after:
case mpr.transitive.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
H : ∃ f, ∀ (x : α), ∃ x_1 Y_n π_n, EffectiveEpiFamily Y_n π_n ∧ ∀ (b : f x), (Sieve.pullback (π x) S).arrows (π_n b)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr.transitive.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
H : ∃ f, ∀ (x : α), ∃ x_1 Y_n π_n, EffectiveEpiFamily Y_n π_n ∧ ∀ (b : f x), (Sieve.pullback (π x) S).arrows (π_n b)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rcases H with ⟨β, H⟩
State after:
case mpr.transitive.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
H : ∀ (x : α), ∃ x_1 Y_n π_n, EffectiveEpiFamily Y_n π_n ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n b)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr.transitive.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
H : ∀ (x : α), ∃ x_1 Y_n π_n, EffectiveEpiFamily Y_n π_n ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n b)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rw [Classical.skolem] at H
State after:
case mpr.transitive.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
H : ∃ f, ∀ (x : α), ∃ Y_n π_n, EffectiveEpiFamily Y_n π_n ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n b)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr.transitive.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
H : ∃ f, ∀ (x : α), ∃ Y_n π_n, EffectiveEpiFamily Y_n π_n ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n b)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rcases H with ⟨_, H⟩
State after:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
H : ∀ (x : α), ∃ Y_n π_n, EffectiveEpiFamily Y_n π_n ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n b)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
H : ∀ (x : α), ∃ Y_n π_n, EffectiveEpiFamily Y_n π_n ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n b)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rw [Classical.skolem] at H
State after:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
H : ∃ f, ∀ (x : α), ∃ π_n, EffectiveEpiFamily (f x) π_n ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n b)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
H : ∃ f, ∀ (x : α), ∃ π_n, EffectiveEpiFamily (f x) π_n ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n b)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rcases H with ⟨Y_n, H⟩
State after:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
H : ∀ (x : α), ∃ π_n, EffectiveEpiFamily (Y_n x) π_n ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n b)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
H : ∀ (x : α), ∃ π_n, EffectiveEpiFamily (Y_n x) π_n ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n b)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rw [Classical.skolem] at H
State after:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
H : ∃ f, ∀ (x : α), EffectiveEpiFamily (Y_n x) (f x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (f x b)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
H : ∃ f, ∀ (x : α), EffectiveEpiFamily (Y_n x) (f x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (f x b)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rcases H with ⟨π_n, H⟩
State after:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
π_n : (x : α) → (b : β x) → Y_n x b ⟶ Y₁ x
H : ∀ (x : α), EffectiveEpiFamily (Y_n x) (π_n x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n x b)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
π_n : (x : α) → (b : β x) → Y_n x b ⟶ Y₁ x
H : ∀ (x : α), EffectiveEpiFamily (Y_n x) (π_n x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n x b)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
use Σ x, β x, inferInstance, fun ⟨a,b⟩ => Y_n a b, fun ⟨a, b⟩ => (π_n a b) ≫ (π a)
State after:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
π_n : (x : α) → (b : β x) → Y_n x b ⟶ Y₁ x
H : ∀ (x : α), EffectiveEpiFamily (Y_n x) (π_n x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n x b)
⊢ (EffectiveEpiFamily
      (fun x =>
        match x with
        | { fst := a, snd := b } => Y_n a b)
      fun x =>
      match x with
      | { fst := a, snd := b } => π_n a b ≫ π a) ∧
    ∀ (a : (x : α) × β x),
      S.arrows
        ((fun x =>
            match x with
            | { fst := a, snd := b } => π_n a b ≫ π a)
          a)

State before:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
π_n : (x : α) → (b : β x) → Y_n x b ⟶ Y₁ x
H : ∀ (x : α), EffectiveEpiFamily (Y_n x) (π_n x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n x b)
⊢ (EffectiveEpiFamily
      (fun x =>
        match x with
        | { fst := a, snd := b } => Y_n a b)
      fun x =>
      match x with
      | { fst := a, snd := b } => π_n a b ≫ π a) ∧
    ∀ (a : (x : α) × β x),
      S.arrows
        ((fun x =>
            match x with
            | { fst := a, snd := b } => π_n a b ≫ π a)
          a)
Tactic:
constructor
State after:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro.intro.left
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
π_n : (x : α) → (b : β x) → Y_n x b ⟶ Y₁ x
H : ∀ (x : α), EffectiveEpiFamily (Y_n x) (π_n x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n x b)
⊢ EffectiveEpiFamily
    (fun x =>
      match x with
      | { fst := a, snd := b } => Y_n a b)
    fun x =>
    match x with
    | { fst := a, snd := b } => π_n a b ≫ π a

case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro.intro.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
π_n : (x : α) → (b : β x) → Y_n x b ⟶ Y₁ x
H : ∀ (x : α), EffectiveEpiFamily (Y_n x) (π_n x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n x b)
⊢ ∀ (a : (x : α) × β x),
    S.arrows
      ((fun x =>
          match x with
          | { fst := a, snd := b } => π_n a b ≫ π a)
        a)

State before:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro.intro.left
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
π_n : (x : α) → (b : β x) → Y_n x b ⟶ Y₁ x
H : ∀ (x : α), EffectiveEpiFamily (Y_n x) (π_n x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n x b)
⊢ EffectiveEpiFamily
    (fun x =>
      match x with
      | { fst := a, snd := b } => Y_n a b)
    fun x =>
    match x with
    | { fst := a, snd := b } => π_n a b ≫ π a
Tactic:
apply EffectiveEpiFamily_transitive
State after:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro.intro.left.h
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
π_n : (x : α) → (b : β x) → Y_n x b ⟶ Y₁ x
H : ∀ (x : α), EffectiveEpiFamily (Y_n x) (π_n x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n x b)
⊢ EffectiveEpiFamily (fun a => Y₁ a) π

case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro.intro.left.H
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
π_n : (x : α) → (b : β x) → Y_n x b ⟶ Y₁ x
H : ∀ (x : α), EffectiveEpiFamily (Y_n x) (π_n x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n x b)
⊢ ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)

State before:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro.intro.left.h
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
π_n : (x : α) → (b : β x) → Y_n x b ⟶ Y₁ x
H : ∀ (x : α), EffectiveEpiFamily (Y_n x) (π_n x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n x b)
⊢ EffectiveEpiFamily (fun a => Y₁ a) π
Tactic:
exact h₁
State after:
no goals

State before:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro.intro.left.H
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
π_n : (x : α) → (b : β x) → Y_n x b ⟶ Y₁ x
H : ∀ (x : α), EffectiveEpiFamily (Y_n x) (π_n x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n x b)
⊢ ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
Tactic:
exact fun a => (H a).1
State after:
no goals

State before:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro.intro.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
π_n : (x : α) → (b : β x) → Y_n x b ⟶ Y₁ x
H : ∀ (x : α), EffectiveEpiFamily (Y_n x) (π_n x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n x b)
⊢ ∀ (a : (x : α) × β x),
    S.arrows
      ((fun x =>
          match x with
          | { fst := a, snd := b } => π_n a b ≫ π a)
        a)
Tactic:
exact fun c => (H c.fst).2 c.snd
State after:
no goals