internlm/Lean-Github huggingface dataset:
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : EffectiveEpiFamily Xmap f
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
⊢ Sieve.generate T ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck ExtrDisc
        (ExtensiveRegularCoverage ExtrDisc everything_proj
          (_ :
            ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
              (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst))))
      Y
Tactic:
rw [he] at hT
Proof state after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
⊢ Sieve.generate T ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck ExtrDisc
        (ExtensiveRegularCoverage ExtrDisc everything_proj
          (_ :
            ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
              (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst))))
      Y
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
⊢ Sieve.generate T ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck ExtrDisc
        (ExtensiveRegularCoverage ExtrDisc everything_proj
          (_ :
            ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
              (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst))))
      Y
Tactic:
let φ := fun (i : I) ↦ Sigma.ι Xmap i
Proof state after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
⊢ Sieve.generate T ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck ExtrDisc
        (ExtensiveRegularCoverage ExtrDisc everything_proj
          (_ :
            ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
              (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst))))
      Y
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
⊢ Sieve.generate T ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck ExtrDisc
        (ExtensiveRegularCoverage ExtrDisc everything_proj
          (_ :
            ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
              (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst))))
      Y
Tactic:
let F := Sigma.desc f
Proof state after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
⊢ Sieve.generate T ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck ExtrDisc
        (ExtensiveRegularCoverage ExtrDisc everything_proj
          (_ :
            ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
              (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst))))
      Y
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
⊢ Sieve.generate T ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck ExtrDisc
        (ExtensiveRegularCoverage ExtrDisc everything_proj
          (_ :
            ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
              (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst))))
      Y
Tactic:
let Z := Sieve.generate T
Proof state after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
⊢ Sieve.generate T ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck ExtrDisc
        (ExtensiveRegularCoverage ExtrDisc everything_proj
          (_ :
            ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
              (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst))))
      Y
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
⊢ Sieve.generate T ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck ExtrDisc
        (ExtensiveRegularCoverage ExtrDisc everything_proj
          (_ :
            ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
              (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst))))
      Y
Tactic:
let Xs := (∐ fun (i : I) => Xmap i)
Proof state after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : ExtrDisc := ∐ fun i => Xmap i
⊢ Sieve.generate T ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck ExtrDisc
        (ExtensiveRegularCoverage ExtrDisc everything_proj
          (_ :
            ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
              (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst))))
      Y
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : ExtrDisc := ∐ fun i => Xmap i
⊢ Sieve.generate T ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck ExtrDisc
        (ExtensiveRegularCoverage ExtrDisc everything_proj
          (_ :
            ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
              (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst))))
      Y
Tactic:
let Zf : Sieve Y := Sieve.generate 
  (Presieve.ofArrows (fun (_ : Unit) ↦ Xs) (fun (_ : Unit) ↦ F))
Proof state after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : ExtrDisc := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ Sieve.generate T ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck ExtrDisc
        (ExtensiveRegularCoverage ExtrDisc everything_proj
          (_ :
            ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
              (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst))))
      Y
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : ExtrDisc := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ Sieve.generate T ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck ExtrDisc
        (ExtensiveRegularCoverage ExtrDisc everything_proj
          (_ :
            ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
              (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst))))
      Y
Tactic:
apply Coverage.saturate.transitive Y Zf
Proof state after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : ExtrDisc := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ Coverage.saturate
    (ExtensiveRegularCoverage ExtrDisc everything_proj
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    Y Zf

case h.h.h.mpr.of.intro.intro.intro.intro.intro.a
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : ExtrDisc := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ ∀ ⦃Y_1 : ExtrDisc⦄ ⦃f : Y_1 ⟶ Y⦄,
    Zf.arrows f →
      Coverage.saturate
        (ExtensiveRegularCoverage ExtrDisc everything_proj
          (_ :
            ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
              (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
        Y_1 (Sieve.pullback f (Sieve.generate T))
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : ExtrDisc := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ Coverage.saturate
    (ExtensiveRegularCoverage ExtrDisc everything_proj
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    Y Zf
Tactic:
apply Coverage.saturate.of
Proof state after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.hS
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : ExtrDisc := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ (ofArrows (fun x => Xs) fun x => F) ∈
    Coverage.covering
      (ExtensiveRegularCoverage ExtrDisc everything_proj
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
      Y
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.hS
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : ExtrDisc := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ (ofArrows (fun x => Xs) fun x => F) ∈
    Coverage.covering
      (ExtensiveRegularCoverage ExtrDisc everything_proj
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
      Y
Tactic:
dsimp [ExtensiveRegularCoverage]
Proof state after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.hS
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : ExtrDisc := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ (ofArrows (fun x => ∐ fun i => Xmap i) fun x => Sigma.desc f) ∈ ExtensiveSieve Y ∪ RegularSieve Y
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.hS
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : ExtrDisc := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ (ofArrows (fun x => ∐ fun i => Xmap i) fun x => Sigma.desc f) ∈ ExtensiveSieve Y ∪ RegularSieve Y
Tactic:
simp only [Set.mem_union, Set.mem_setOf_eq]
Proof state after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.hS
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : ExtrDisc := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ (ofArrows (fun x => ∐ fun i => Xmap i) fun x => Sigma.desc f) ∈ ExtensiveSieve Y ∨
    (ofArrows (fun x => ∐ fun i => Xmap i) fun x => Sigma.desc f) ∈ RegularSieve Y
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.hS
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : ExtrDisc := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ (ofArrows (fun x => ∐ fun i => Xmap i) fun x => Sigma.desc f) ∈ ExtensiveSieve Y ∨
    (ofArrows (fun x => ∐ fun i => Xmap i) fun x => Sigma.desc f) ∈ RegularSieve Y
Tactic:
right
Proof state after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.hS.h
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : ExtrDisc := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ (ofArrows (fun x => ∐ fun i => Xmap i) fun x => Sigma.desc f) ∈ RegularSieve Y
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.hS.h
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : ExtrDisc := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ (ofArrows (fun x => ∐ fun i => Xmap i) fun x => Sigma.desc f) ∈ RegularSieve Y
Tactic:
use Xs
Proof state after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.hS.h
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : ExtrDisc := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ ∃ f_1, ((ofArrows (fun x => ∐ fun i => Xmap i) fun x => Sigma.desc f) = ofArrows (fun x => Xs) fun x => f_1) ∧ Epi f_1
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.hS.h
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : ExtrDisc := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ ∃ f_1, ((ofArrows (fun x => ∐ fun i => Xmap i) fun x => Sigma.desc f) = ofArrows (fun x => Xs) fun x => f_1) ∧ Epi f_1
Tactic:
use F
Proof state after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.hS.h
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : ExtrDisc := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ ((ofArrows (fun x => ∐ fun i => Xmap i) fun x => Sigma.desc f) = ofArrows (fun x => Xs) fun x => F) ∧ Epi F
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.hS.h
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : ExtrDisc := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ ((ofArrows (fun x => ∐ fun i => Xmap i) fun x => Sigma.desc f) = ofArrows (fun x => Xs) fun x => F) ∧ Epi F
Tactic:
refine' ⟨rfl, inferInstance⟩
Proof state after:
no goals
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : ExtrDisc := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ ∀ ⦃Y_1 : ExtrDisc⦄ ⦃f : Y_1 ⟶ Y⦄,
    Zf.arrows f →
      Coverage.saturate
        (ExtensiveRegularCoverage ExtrDisc everything_proj
          (_ :
            ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
              (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
        Y_1 (Sieve.pullback f (Sieve.generate T))
Tactic:
intro R g hZfg
Proof state after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → ExtrDisc
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : ExtrDisc := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : ExtrDisc
g : R ⟶ Y
hZfg : Zf.arrows g
⊢ Coverage.saturate
    (ExtensiveRegularCoverage ExtrDisc everything_proj
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    R (Sieve.pullback g (Sieve.generate T))