internlm/Lean-Github huggingface dataset:
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof 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
Proof 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)
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof 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
Proof state after:
no goals
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof 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'
Proof 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')
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof 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
Proof 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')
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof 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]
Proof 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'
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof 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'
Proof 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'
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof 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
Proof 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'
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof 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]
Proof 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')
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof 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'
Proof state after:
no goals
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof 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
Proof state after:
no goals
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof 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)
Proof 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)
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof 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
Proof 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)
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof 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
Proof 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)
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof 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
Proof state after:
no goals
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof 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]
Proof state after:
no goals
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof 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₂⟩⟩
Proof 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)
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof 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)
Proof 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)
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof 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
Proof 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)
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof 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⟩
Proof 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)
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof 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
Proof 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)
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof 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⟩
Proof 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)
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof 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
Proof 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)
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof 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⟩
Proof 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)
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof 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
Proof 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)