internlm/Lean-Github huggingface dataset:
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)
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))
Tactic:
dsimp at 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 : ∃ Y_1 h g_1, ofArrows (fun x => ∐ fun i => Xmap i) (fun x => Sigma.desc f) g_1 ∧ h ≫ g_1 = 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))
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)
R : ExtrDisc
g : R ⟶ Y
hZfg : ∃ Y_1 h g_1, ofArrows (fun x => ∐ fun i => Xmap i) (fun x => Sigma.desc f) g_1 ∧ h ≫ g_1 = 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))
Tactic:
rw [Presieve.ofArrows_pUnit] at 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 : ∃ Y_1 h g_1, Presieve.singleton (Sigma.desc f) g_1 ∧ h ≫ g_1 = 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))
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)
R : ExtrDisc
g : R ⟶ Y
hZfg : ∃ Y_1 h g_1, Presieve.singleton (Sigma.desc f) g_1 ∧ h ≫ g_1 = 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))
Tactic:
obtain ⟨W, ψ, σ, ⟨hW, hW'⟩⟩ := hZfg
Proof state after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.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)
R : ExtrDisc
g : R ⟶ Y
W : ExtrDisc
ψ : R ⟶ W
σ : W ⟶ Y
hW : Presieve.singleton (Sigma.desc f) σ
hW' : ψ ≫ σ = 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))
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.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)
R : ExtrDisc
g : R ⟶ Y
W : ExtrDisc
ψ : R ⟶ W
σ : W ⟶ Y
hW : Presieve.singleton (Sigma.desc f) σ
hW' : ψ ≫ σ = 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))
Tactic:
dsimp [Presieve.singleton] at hW
Proof state after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.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)
R : ExtrDisc
g : R ⟶ Y
W : ExtrDisc
ψ : R ⟶ W
σ : W ⟶ Y
hW : singleton' (Sigma.desc f) σ
hW' : ψ ≫ σ = 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))
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.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)
R : ExtrDisc
g : R ⟶ Y
W : ExtrDisc
ψ : R ⟶ W
σ : W ⟶ Y
hW : singleton' (Sigma.desc f) σ
hW' : ψ ≫ σ = 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))
Tactic:
induction hW
Proof state after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro.mk
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
W : ExtrDisc
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = 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))
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro.mk
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
W : ExtrDisc
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = 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))
Tactic:
rw [← hW', Sieve.pullback_comp Z]
Proof state after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro.mk
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
W : ExtrDisc
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = 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 ψ (Sieve.pullback (Sigma.desc f) Z))
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro.mk
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
W : ExtrDisc
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = 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 ψ (Sieve.pullback (Sigma.desc f) Z))
Tactic:
suffices : Sieve.pullback ψ ((Sieve.pullback F) Z) ∈ GrothendieckTopology.sieves
  (ExtensiveRegularCoverage _ _ _).toGrothendieck R
Proof state after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro.mk
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
W : ExtrDisc
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this :
  Sieve.pullback ψ (Sieve.pullback F Z) ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck ExtrDisc (ExtensiveRegularCoverage ExtrDisc ?m.558302 ?m.558303)) R
⊢ 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 ψ (Sieve.pullback (Sigma.desc f) Z))

case this
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
W : ExtrDisc
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
⊢ Sieve.pullback ψ (Sieve.pullback F Z) ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck ExtrDisc (ExtensiveRegularCoverage ExtrDisc ?m.558302 ?m.558303)) R
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case this
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
W : ExtrDisc
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
⊢ Sieve.pullback ψ (Sieve.pullback F Z) ∈
    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))))
      R
Tactic:
apply GrothendieckTopology.pullback_stable'
Proof state after:
case this.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
W : ExtrDisc
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
⊢ Sieve.pullback F Z ∈
    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))))
      (∐ fun i => Xmap i)
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case this.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
W : ExtrDisc
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
⊢ Sieve.pullback F Z ∈
    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))))
      (∐ fun i => Xmap i)
Tactic:
dsimp [Coverage.toGrothendieck]
Proof state after:
case this.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
W : ExtrDisc
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
⊢ Sieve.pullback (Sigma.desc f) (Sieve.generate T) ∈
    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)))
      (∐ fun i => Xmap i)
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case this.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
W : ExtrDisc
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
⊢ Sieve.pullback (Sigma.desc f) (Sieve.generate T) ∈
    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)))
      (∐ fun i => Xmap i)
Tactic:
suffices : Coverage.saturate (ExtensiveRegularCoverage _ _ _) Xs (Z.pullback F)
Proof state after:
case this.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
W : ExtrDisc
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Coverage.saturate (ExtensiveRegularCoverage ExtrDisc ?m.558925 ?m.558926) Xs (Sieve.pullback F Z)
⊢ Sieve.pullback (Sigma.desc f) (Sieve.generate T) ∈
    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)))
      (∐ fun i => Xmap i)

case this
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
W : ExtrDisc
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
⊢ Coverage.saturate (ExtensiveRegularCoverage ExtrDisc ?m.558925 ?m.558926) Xs (Sieve.pullback F Z)