internlm/Lean-Github huggingface dataset:
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case this.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)
R : ExtrDisc
g : R ⟶ Y
W : ExtrDisc
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ IsIso (Sigma.desc φ)
Tactic:
suffices : Sigma.desc φ = 𝟙 _
Proof state after:
case this.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)
R : ExtrDisc
g : R ⟶ Y
W : ExtrDisc
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this✝ : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
this : Sigma.desc φ = 𝟙 (∐ fun b => Xmap b)
⊢ IsIso (Sigma.desc φ)

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
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ Sigma.desc φ = 𝟙 (∐ fun b => Xmap b)
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
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ Sigma.desc φ = 𝟙 (∐ fun b => Xmap b)
Tactic:
ext
Proof state after:
case this.h.w
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.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
b✝ : I
x✝ : (forget ExtrDisc).obj (Xmap b✝)
⊢ ↑(Sigma.ι (fun b => Xmap b) b✝ ≫ Sigma.desc φ) x✝ = ↑(Sigma.ι (fun b => Xmap b) b✝ ≫ 𝟙 (∐ fun b => Xmap b)) x✝
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case this.h.w
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.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
b✝ : I
x✝ : (forget ExtrDisc).obj (Xmap b✝)
⊢ ↑(Sigma.ι (fun b => Xmap b) b✝ ≫ Sigma.desc φ) x✝ = ↑(Sigma.ι (fun b => Xmap b) b✝ ≫ 𝟙 (∐ fun b => Xmap b)) x✝
Tactic:
simp only [colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app, Category.comp_id]
Proof state after:
no goals
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case this.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)
R : ExtrDisc
g : R ⟶ Y
W : ExtrDisc
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this✝ : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
this : Sigma.desc φ = 𝟙 (∐ fun b => Xmap b)
⊢ IsIso (Sigma.desc φ)
Tactic:
rw [this]
Proof state after:
case this.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)
R : ExtrDisc
g : R ⟶ Y
W : ExtrDisc
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this✝ : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
this : Sigma.desc φ = 𝟙 (∐ fun b => Xmap b)
⊢ IsIso (𝟙 (∐ fun b => Xmap b))
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case this.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)
R : ExtrDisc
g : R ⟶ Y
W : ExtrDisc
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this✝ : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
this : Sigma.desc φ = 𝟙 (∐ fun b => Xmap b)
⊢ IsIso (𝟙 (∐ fun b => Xmap b))
Tactic:
exact inferInstance
Proof state after:
no goals
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case this.intro.intro.intro.refine'_1
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
Q : ExtrDisc
q : Q ⟶ ∐ Xmap
E : ExtrDisc
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ T (r ≫ F)
Tactic:
rw [h]
Proof state after:
case this.intro.intro.intro.refine'_1
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
Q : ExtrDisc
q : Q ⟶ ∐ Xmap
E : ExtrDisc
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ ofArrows Xmap f (r ≫ F)
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case this.intro.intro.intro.refine'_1
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
Q : ExtrDisc
q : Q ⟶ ∐ Xmap
E : ExtrDisc
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ ofArrows Xmap f (r ≫ F)
Tactic:
induction hq.1
Proof state after:
case this.intro.intro.intro.refine'_1.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
Q : ExtrDisc
q : Q ⟶ ∐ Xmap
E : ExtrDisc
r : E ⟶ ∐ Xmap
i✝ : I
e : Q ⟶ Xmap i✝
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) (Sigma.ι Xmap i✝) ∧ e ≫ Sigma.ι Xmap i✝ = q
⊢ ofArrows Xmap f (Sigma.ι Xmap i✝ ≫ F)
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case this.intro.intro.intro.refine'_1.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
Q : ExtrDisc
q : Q ⟶ ∐ Xmap
E : ExtrDisc
r : E ⟶ ∐ Xmap
i✝ : I
e : Q ⟶ Xmap i✝
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) (Sigma.ι Xmap i✝) ∧ e ≫ Sigma.ι Xmap i✝ = q
⊢ ofArrows Xmap f (Sigma.ι Xmap i✝ ≫ F)
Tactic:
dsimp
Proof state after:
case this.intro.intro.intro.refine'_1.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
Q : ExtrDisc
q : Q ⟶ ∐ Xmap
E : ExtrDisc
r : E ⟶ ∐ Xmap
i✝ : I
e : Q ⟶ Xmap i✝
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) (Sigma.ι Xmap i✝) ∧ e ≫ Sigma.ι Xmap i✝ = q
⊢ ofArrows Xmap f (Sigma.ι Xmap i✝ ≫ Sigma.desc f)
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case this.intro.intro.intro.refine'_1.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
Q : ExtrDisc
q : Q ⟶ ∐ Xmap
E : ExtrDisc
r : E ⟶ ∐ Xmap
i✝ : I
e : Q ⟶ Xmap i✝
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) (Sigma.ι Xmap i✝) ∧ e ≫ Sigma.ι Xmap i✝ = q
⊢ ofArrows Xmap f (Sigma.ι Xmap i✝ ≫ Sigma.desc f)
Tactic:
simp only [colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app]
Proof state after:
case this.intro.intro.intro.refine'_1.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
Q : ExtrDisc
q : Q ⟶ ∐ Xmap
E : ExtrDisc
r : E ⟶ ∐ Xmap
i✝ : I
e : Q ⟶ Xmap i✝
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) (Sigma.ι Xmap i✝) ∧ e ≫ Sigma.ι Xmap i✝ = q
⊢ ofArrows Xmap f (f i✝)
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case this.intro.intro.intro.refine'_1.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
Q : ExtrDisc
q : Q ⟶ ∐ Xmap
E : ExtrDisc
r : E ⟶ ∐ Xmap
i✝ : I
e : Q ⟶ Xmap i✝
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) (Sigma.ι Xmap i✝) ∧ e ≫ Sigma.ι Xmap i✝ = q
⊢ ofArrows Xmap f (f i✝)
Tactic:
exact Presieve.ofArrows.mk _
Proof state after:
no goals
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case this.intro.intro.intro.refine'_2
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
Q : ExtrDisc
q : Q ⟶ ∐ Xmap
E : ExtrDisc
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
Tactic:
rw [← hq.2]
Proof state after:
case this.intro.intro.intro.refine'_2
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
Q : ExtrDisc
q : Q ⟶ ∐ Xmap
E : ExtrDisc
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ e ≫ r ≫ F = (e ≫ r) ≫ Sigma.desc f
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case this.intro.intro.intro.refine'_2
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
Q : ExtrDisc
q : Q ⟶ ∐ Xmap
E : ExtrDisc
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ e ≫ r ≫ F = (e ≫ r) ≫ Sigma.desc f
Tactic:
rfl
Proof state after:
no goals
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.top
X : ExtrDisc
S : Sieve X
X✝ : ExtrDisc
⊢ ⊤ ∈
    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))))
      X✝
Tactic:
apply Coverage.saturate.top
Proof state after:
no goals
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.transitive.a
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T S✝ : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage ExtrDisc) Y T
a✝ :
  ∀ ⦃Y_1 : ExtrDisc⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Coverage.saturate (coherentCoverage ExtrDisc) Y_1 (Sieve.pullback f S✝)
a_ih✝¹ :
  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
a_ih✝ :
  ∀ ⦃Y_1 : ExtrDisc⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f →
      Sieve.pullback f S✝ ∈
        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_1
⊢ 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 T
Tactic:
assumption
Proof state after:
no goals
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.transitive.a
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T S✝ : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage ExtrDisc) Y T
a✝ :
  ∀ ⦃Y_1 : ExtrDisc⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Coverage.saturate (coherentCoverage ExtrDisc) Y_1 (Sieve.pullback f S✝)
a_ih✝¹ :
  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
a_ih✝ :
  ∀ ⦃Y_1 : ExtrDisc⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f →
      Sieve.pullback f S✝ ∈
        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_1
⊢ ∀ ⦃Y_1 : ExtrDisc⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.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 S✝)
Tactic:
assumption
Proof state after:
no goals
Theorem: ExtrDisc.isSheafForRegularSieve
Proof state before:
X : ExtrDisc
S : Presieve X
hS : S ∈ RegularSieve X
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
⊢ IsSheafFor F S
Tactic:
obtain ⟨Y, f, rfl, hf⟩ := hS
Proof state after:
case intro.intro.intro
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
⊢ IsSheafFor F (ofArrows (fun x => Y) fun x => f)
Theorem: ExtrDisc.isSheafForRegularSieve
Proof state before:
case intro.intro.intro
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
⊢ IsSheafFor F (ofArrows (fun x => Y) fun x => f)
Tactic:
have proj : Projective (toCompHaus.obj X) := inferInstanceAs (Projective X.compHaus)
Proof state after:
case intro.intro.intro
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
⊢ IsSheafFor F (ofArrows (fun x => Y) fun x => f)
Theorem: ExtrDisc.isSheafForRegularSieve
Proof state before:
case intro.intro.intro
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
⊢ IsSheafFor F (ofArrows (fun x => Y) fun x => f)
Tactic:
have : Epi (toCompHaus.map f) := by
  rw [CompHaus.epi_iff_surjective]
  change Function.Surjective f
  rwa [← ExtrDisc.epi_iff_surjective]
Proof state after:
case intro.intro.intro
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this : Epi (toCompHaus.map f)
⊢ IsSheafFor F (ofArrows (fun x => Y) fun x => f)
Theorem: ExtrDisc.isSheafForRegularSieve
Proof state before:
case intro.intro.intro
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this : Epi (toCompHaus.map f)
⊢ IsSheafFor F (ofArrows (fun x => Y) fun x => f)
Tactic:
set g := toCompHaus.preimage <| Projective.factorThru (𝟙 _) (toCompHaus.map f) with hg
Proof state after:
case intro.intro.intro
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
⊢ IsSheafFor F (ofArrows (fun x => Y) fun x => f)
Theorem: ExtrDisc.isSheafForRegularSieve
Proof state before:
case intro.intro.intro
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
⊢ IsSheafFor F (ofArrows (fun x => Y) fun x => f)
Tactic:
have hfg : g ≫ f = 𝟙 _ := by
  refine' toCompHaus.map_injective _
  rw [map_comp, hg, image_preimage, Projective.factorThru_comp, CategoryTheory.Functor.map_id]
Proof state after:
case intro.intro.intro
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hfg : g ≫ f = 𝟙 X
⊢ IsSheafFor F (ofArrows (fun x => Y) fun x => f)