internlm/Lean-Github huggingface dataset:
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    Xs (Sieve.pullback F Z)
Tactic:
suffices : Sieve.generate (Presieve.ofArrows Xmap φ) ≤ Z.pullback F
Proof state after:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    Xs (Sieve.pullback F Z)

case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
⊢ Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
⊢ Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
Tactic:
intro Q q hq
Proof state after:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
hq : (Sieve.generate (ofArrows Xmap φ)).arrows q
⊢ (Sieve.pullback F Z).arrows q
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
hq : (Sieve.generate (ofArrows Xmap φ)).arrows q
⊢ (Sieve.pullback F Z).arrows q
Tactic:
simp only [Sieve.pullback_apply, Sieve.generate_apply]
Proof state after:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
hq : (Sieve.generate (ofArrows Xmap φ)).arrows q
⊢ ∃ Y_1 h g, T g ∧ h ≫ g = q ≫ Sigma.desc f
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
hq : (Sieve.generate (ofArrows Xmap φ)).arrows q
⊢ ∃ Y_1 h g, T g ∧ h ≫ g = q ≫ Sigma.desc f
Tactic:
simp only [Sieve.generate_apply] at hq
Proof state after:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
hq : ∃ Y h g, ofArrows Xmap (fun i => Sigma.ι Xmap i) g ∧ h ≫ g = q
⊢ ∃ Y_1 h g, T g ∧ h ≫ g = q ≫ Sigma.desc f
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
hq : ∃ Y h g, ofArrows Xmap (fun i => Sigma.ι Xmap i) g ∧ h ≫ g = q
⊢ ∃ Y_1 h g, T g ∧ h ≫ g = q ≫ Sigma.desc f
Tactic:
obtain ⟨E, e, r, hq⟩ := hq
Proof state after:
case this.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
E : Profinite
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ ∃ Y_1 h g, T g ∧ h ≫ g = q ≫ Sigma.desc f
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case this.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
E : Profinite
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ ∃ Y_1 h g, T g ∧ h ≫ g = q ≫ Sigma.desc f
Tactic:
refine' ⟨E, e, r ≫ F, ⟨_, _⟩⟩
Proof state after:
case this.intro.intro.intro.refine'_1
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
E : Profinite
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ T (r ≫ F)

case this.intro.intro.intro.refine'_2
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
E : Profinite
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ e ≫ r ≫ F = q ≫ Sigma.desc f
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro.mk
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this :
  Sieve.pullback ψ (Sieve.pullback F Z) ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck Profinite (ExtensiveRegularCoverage' Profinite ?m.588132 ?m.588133)) R
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (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:
exact this
Proof state after:
no goals
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case this.a
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Coverage.saturate (ExtensiveRegularCoverage' Profinite ?m.593517 ?m.593518) Xs (Sieve.pullback F Z)
⊢ Sieve.pullback (Sigma.desc f) (Sieve.generate T) ∈
    Coverage.saturate
      (ExtensiveRegularCoverage' Profinite
        (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
      (∐ fun i => Xmap i)
Tactic:
exact this
Proof state after:
no goals
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    Xs (Sieve.pullback F Z)
Tactic:
apply Coverage.saturate_of_superset _ this
Proof state after:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    (∐ Xmap) (Sieve.generate (ofArrows Xmap φ))
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    (∐ Xmap) (Sieve.generate (ofArrows Xmap φ))
Tactic:
apply Coverage.saturate.of
Proof state after:
case this.hS
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ ofArrows Xmap φ ∈
    Coverage.covering
      (ExtensiveRegularCoverage' Profinite
        (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
      (∐ Xmap)
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case this.hS
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ ofArrows Xmap φ ∈
    Coverage.covering
      (ExtensiveRegularCoverage' Profinite
        (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
      (∐ Xmap)
Tactic:
dsimp [ExtensiveRegularCoverage']
Proof state after:
case this.hS
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ (ofArrows Xmap fun i => Sigma.ι Xmap i) ∈ ExtensiveSieve (∐ Xmap) ∪ RegularSieve (∐ Xmap)
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case this.hS
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ (ofArrows Xmap fun i => Sigma.ι Xmap i) ∈ ExtensiveSieve (∐ Xmap) ∪ RegularSieve (∐ Xmap)
Tactic:
left
Proof state after:
case this.hS.h
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ (ofArrows Xmap fun i => Sigma.ι Xmap i) ∈ ExtensiveSieve (∐ Xmap)
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case this.hS.h
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ (ofArrows Xmap fun i => Sigma.ι Xmap i) ∈ ExtensiveSieve (∐ Xmap)
Tactic:
refine' ⟨I, hI, Xmap, φ, ⟨rfl, _⟩⟩
Proof state after:
case this.hS.h
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
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 : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ IsIso (Sigma.desc φ)