internlm/Lean-Github huggingface dataset:
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.left.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
α : Type
x : Fintype α
Xmap : α → ExtrDisc
π : (a : α) → Xmap a ⟶ Y
h : T = ofArrows Xmap π ∧ IsIso (Sigma.desc π)
⊢ EffectiveEpiFamily Xmap π
Tactic:
have he := (effectiveEpiFamily_tfae Xmap π).out 0 1
Proof state after:
case h.h.h.mp.of.hS.left.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
α : Type
x : Fintype α
Xmap : α → ExtrDisc
π : (a : α) → Xmap a ⟶ Y
h : T = ofArrows Xmap π ∧ IsIso (Sigma.desc π)
he : EffectiveEpiFamily Xmap π ↔ Epi (Sigma.desc π)
⊢ EffectiveEpiFamily Xmap π
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.left.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
α : Type
x : Fintype α
Xmap : α → ExtrDisc
π : (a : α) → Xmap a ⟶ Y
h : T = ofArrows Xmap π ∧ IsIso (Sigma.desc π)
he : EffectiveEpiFamily Xmap π ↔ Epi (Sigma.desc π)
⊢ EffectiveEpiFamily Xmap π
Tactic:
rw [he]
Proof state after:
case h.h.h.mp.of.hS.left.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
α : Type
x : Fintype α
Xmap : α → ExtrDisc
π : (a : α) → Xmap a ⟶ Y
h : T = ofArrows Xmap π ∧ IsIso (Sigma.desc π)
he : EffectiveEpiFamily Xmap π ↔ Epi (Sigma.desc π)
⊢ Epi (Sigma.desc π)
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.left.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
α : Type
x : Fintype α
Xmap : α → ExtrDisc
π : (a : α) → Xmap a ⟶ Y
h : T = ofArrows Xmap π ∧ IsIso (Sigma.desc π)
he : EffectiveEpiFamily Xmap π ↔ Epi (Sigma.desc π)
⊢ Epi (Sigma.desc π)
Tactic:
letI := h.2
Proof state after:
case h.h.h.mp.of.hS.left.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
α : Type
x : Fintype α
Xmap : α → ExtrDisc
π : (a : α) → Xmap a ⟶ Y
h : T = ofArrows Xmap π ∧ IsIso (Sigma.desc π)
he : EffectiveEpiFamily Xmap π ↔ Epi (Sigma.desc π)
this : IsIso (Sigma.desc π) := h.right
⊢ Epi (Sigma.desc π)
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.left.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
α : Type
x : Fintype α
Xmap : α → ExtrDisc
π : (a : α) → Xmap a ⟶ Y
h : T = ofArrows Xmap π ∧ IsIso (Sigma.desc π)
he : EffectiveEpiFamily Xmap π ↔ Epi (Sigma.desc π)
this : IsIso (Sigma.desc π) := h.right
⊢ Epi (Sigma.desc π)
Tactic:
exact inferInstance
Proof state after:
no goals
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.right
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
h : T ∈ RegularSieve Y
⊢ ∃ α x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Tactic:
obtain ⟨Z, f, h⟩ := h
Proof state after:
case h.h.h.mp.of.hS.right.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Epi f
⊢ ∃ α x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.right.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Epi f
⊢ ∃ α x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Tactic:
use Unit
Proof state after:
case h.h.h.mp.of.hS.right.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Epi f
⊢ ∃ x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.right.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Epi f
⊢ ∃ x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Tactic:
use inferInstance
Proof state after:
case h.h.h.mp.of.hS.right.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Epi f
⊢ ∃ X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.right.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Epi f
⊢ ∃ X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Tactic:
use (fun _ ↦ Z)
Proof state after:
case h.h.h.mp.of.hS.right.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Epi f
⊢ ∃ π, T = ofArrows (fun x => Z) π ∧ EffectiveEpiFamily (fun x => Z) π
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.right.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Epi f
⊢ ∃ π, T = ofArrows (fun x => Z) π ∧ EffectiveEpiFamily (fun x => Z) π
Tactic:
use (fun _ ↦ f)
Proof state after:
case h.h.h.mp.of.hS.right.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Epi f
⊢ (T = ofArrows (fun x => Z) fun x => f) ∧ EffectiveEpiFamily (fun x => Z) fun x => f
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.right.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Epi f
⊢ (T = ofArrows (fun x => Z) fun x => f) ∧ EffectiveEpiFamily (fun x => Z) fun x => f
Tactic:
refine' ⟨h.1,_⟩
Proof state after:
case h.h.h.mp.of.hS.right.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Epi f
⊢ EffectiveEpiFamily (fun x => Z) fun x => f
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.right.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Epi f
⊢ EffectiveEpiFamily (fun x => Z) fun x => f
Tactic:
have he := (effectiveEpiFamily_tfae (fun (_ : Unit) ↦ Z) (fun _ ↦ f)).out 0 1
Proof state after:
case h.h.h.mp.of.hS.right.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Epi f
he : (EffectiveEpiFamily (fun x => Z) fun x => f) ↔ Epi (Sigma.desc fun x => f)
⊢ EffectiveEpiFamily (fun x => Z) fun x => f
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.right.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Epi f
he : (EffectiveEpiFamily (fun x => Z) fun x => f) ↔ Epi (Sigma.desc fun x => f)
⊢ EffectiveEpiFamily (fun x => Z) fun x => f
Tactic:
rw [he]
Proof state after:
case h.h.h.mp.of.hS.right.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Epi f
he : (EffectiveEpiFamily (fun x => Z) fun x => f) ↔ Epi (Sigma.desc fun x => f)
⊢ Epi (Sigma.desc fun x => f)
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.right.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Epi f
he : (EffectiveEpiFamily (fun x => Z) fun x => f) ↔ Epi (Sigma.desc fun x => f)
⊢ Epi (Sigma.desc fun x => f)
Tactic:
rw [ExtrDisc.epi_iff_surjective _] at h ⊢
Proof state after:
case h.h.h.mp.of.hS.right.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Function.Surjective ↑f
he : (EffectiveEpiFamily (fun x => Z) fun x => f) ↔ Epi (Sigma.desc fun x => f)
⊢ Function.Surjective ↑(Sigma.desc fun x => f)
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.right.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Function.Surjective ↑f
he : (EffectiveEpiFamily (fun x => Z) fun x => f) ↔ Epi (Sigma.desc fun x => f)
⊢ Function.Surjective ↑(Sigma.desc fun x => f)
Tactic:
intro x
Proof state after:
case h.h.h.mp.of.hS.right.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Function.Surjective ↑f
he : (EffectiveEpiFamily (fun x => Z) fun x => f) ↔ Epi (Sigma.desc fun x => f)
x : CoeSort.coe Y
⊢ ∃ a, ↑(Sigma.desc fun x => f) a = x
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.right.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Function.Surjective ↑f
he : (EffectiveEpiFamily (fun x => Z) fun x => f) ↔ Epi (Sigma.desc fun x => f)
x : CoeSort.coe Y
⊢ ∃ a, ↑(Sigma.desc fun x => f) a = x
Tactic:
obtain ⟨y,hy⟩ := h.2 x
Proof state after:
case h.h.h.mp.of.hS.right.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Function.Surjective ↑f
he : (EffectiveEpiFamily (fun x => Z) fun x => f) ↔ Epi (Sigma.desc fun x => f)
x : CoeSort.coe Y
y : CoeSort.coe Z
hy : ↑f y = x
⊢ ∃ a, ↑(Sigma.desc fun x => f) a = x
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.right.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Function.Surjective ↑f
he : (EffectiveEpiFamily (fun x => Z) fun x => f) ↔ Epi (Sigma.desc fun x => f)
x : CoeSort.coe Y
y : CoeSort.coe Z
hy : ↑f y = x
⊢ ∃ a, ↑(Sigma.desc fun x => f) a = x
Tactic:
use Sigma.ι (fun (_ : Unit) ↦ Z) Unit.unit y
Proof state after:
case h.h.h.mp.of.hS.right.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Function.Surjective ↑f
he : (EffectiveEpiFamily (fun x => Z) fun x => f) ↔ Epi (Sigma.desc fun x => f)
x : CoeSort.coe Y
y : CoeSort.coe Z
hy : ↑f y = x
⊢ ↑(Sigma.desc fun x => f) (↑(Sigma.ι (fun x => Z) ()) y) = x
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.right.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Function.Surjective ↑f
he : (EffectiveEpiFamily (fun x => Z) fun x => f) ↔ Epi (Sigma.desc fun x => f)
x : CoeSort.coe Y
y : CoeSort.coe Z
hy : ↑f y = x
⊢ ↑(Sigma.desc fun x => f) (↑(Sigma.ι (fun x => Z) ()) y) = x
Tactic:
rw [← hy]
Proof state after:
case h.h.h.mp.of.hS.right.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Function.Surjective ↑f
he : (EffectiveEpiFamily (fun x => Z) fun x => f) ↔ Epi (Sigma.desc fun x => f)
x : CoeSort.coe Y
y : CoeSort.coe Z
hy : ↑f y = x
⊢ ↑(Sigma.desc fun x => f) (↑(Sigma.ι (fun x => Z) ()) y) = ↑f y
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.right.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Function.Surjective ↑f
he : (EffectiveEpiFamily (fun x => Z) fun x => f) ↔ Epi (Sigma.desc fun x => f)
x : CoeSort.coe Y
y : CoeSort.coe Z
hy : ↑f y = x
⊢ ↑(Sigma.desc fun x => f) (↑(Sigma.ι (fun x => Z) ()) y) = ↑f y
Tactic:
suffices : (f : Z → Y) = Sigma.ι (fun (_ : Unit) ↦ Z) Unit.unit ≫ Sigma.desc (fun _ ↦ f)
Proof state after:
case h.h.h.mp.of.hS.right.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Function.Surjective ↑f
he : (EffectiveEpiFamily (fun x => Z) fun x => f) ↔ Epi (Sigma.desc fun x => f)
x : CoeSort.coe Y
y : CoeSort.coe Z
hy : ↑f y = x
this : ↑f = ↑(Sigma.ι (fun x => Z) () ≫ Sigma.desc fun x => f)
⊢ ↑(Sigma.desc fun x => f) (↑(Sigma.ι (fun x => Z) ()) y) = ↑f y

case this
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Function.Surjective ↑f
he : (EffectiveEpiFamily (fun x => Z) fun x => f) ↔ Epi (Sigma.desc fun x => f)
x : CoeSort.coe Y
y : CoeSort.coe Z
hy : ↑f y = x
⊢ ↑f = ↑(Sigma.ι (fun x => Z) () ≫ Sigma.desc fun x => f)
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case this
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Function.Surjective ↑f
he : (EffectiveEpiFamily (fun x => Z) fun x => f) ↔ Epi (Sigma.desc fun x => f)
x : CoeSort.coe Y
y : CoeSort.coe Z
hy : ↑f y = x
⊢ ↑f = ↑(Sigma.ι (fun x => Z) () ≫ Sigma.desc fun x => f)
Tactic:
simp only [colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app]
Proof state after:
no goals
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.right.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Function.Surjective ↑f
he : (EffectiveEpiFamily (fun x => Z) fun x => f) ↔ Epi (Sigma.desc fun x => f)
x : CoeSort.coe Y
y : CoeSort.coe Z
hy : ↑f y = x
this : ↑f = ↑(Sigma.ι (fun x => Z) () ≫ Sigma.desc fun x => f)
⊢ ↑(Sigma.desc fun x => f) (↑(Sigma.ι (fun x => Z) ()) y) = ↑f y
Tactic:
rw [this]
Proof state after:
case h.h.h.mp.of.hS.right.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Function.Surjective ↑f
he : (EffectiveEpiFamily (fun x => Z) fun x => f) ↔ Epi (Sigma.desc fun x => f)
x : CoeSort.coe Y
y : CoeSort.coe Z
hy : ↑f y = x
this : ↑f = ↑(Sigma.ι (fun x => Z) () ≫ Sigma.desc fun x => f)
⊢ ↑(Sigma.desc fun x => f) (↑(Sigma.ι (fun x => Z) ()) y) = ↑(Sigma.ι (fun x => Z) () ≫ Sigma.desc fun x => f) y
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.right.intro.intro.intro
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : ExtrDisc
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Function.Surjective ↑f
he : (EffectiveEpiFamily (fun x => Z) fun x => f) ↔ Epi (Sigma.desc fun x => f)
x : CoeSort.coe Y
y : CoeSort.coe Z
hy : ↑f y = x
this : ↑f = ↑(Sigma.ι (fun x => Z) () ≫ Sigma.desc fun x => f)
⊢ ↑(Sigma.desc fun x => f) (↑(Sigma.ι (fun x => Z) ()) y) = ↑(Sigma.ι (fun x => Z) () ≫ Sigma.desc fun x => f) y
Tactic:
rfl
Proof state after:
no goals
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.top
X : ExtrDisc
S : Sieve X
X✝ : ExtrDisc
⊢ ⊤ ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) X✝
Tactic:
apply Coverage.saturate.top
Proof state after:
no goals
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.transitive.a
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T S✝ : Sieve Y
a✝¹ :
  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
a✝ :
  ∀ ⦃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✝)
a_ih✝¹ : T ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) Y
a_ih✝ :
  ∀ ⦃Y_1 : ExtrDisc⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Sieve.pullback f S✝ ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) Y_1
⊢ Coverage.saturate (coherentCoverage ExtrDisc) Y T
Tactic:
assumption
Proof state after:
no goals
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.transitive.a
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T S✝ : Sieve Y
a✝¹ :
  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
a✝ :
  ∀ ⦃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✝)
a_ih✝¹ : T ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) Y
a_ih✝ :
  ∀ ⦃Y_1 : ExtrDisc⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Sieve.pullback f S✝ ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) Y_1
⊢ ∀ ⦃Y_1 : ExtrDisc⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Coverage.saturate (coherentCoverage ExtrDisc) Y_1 (Sieve.pullback f S✝)
Tactic:
assumption
Proof state after:
no goals
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mpr.of
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ Coverage.covering (coherentCoverage ExtrDisc) Y
⊢ 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:
dsimp [coherentCoverage] at hT
Proof state after:
case h.h.h.mpr.of
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : ∃ α x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
⊢ 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
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : ∃ α x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
⊢ 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:
obtain ⟨I, hI, Xmap, f, ⟨h, hT⟩⟩ := 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 : EffectiveEpiFamily Xmap 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 : EffectiveEpiFamily Xmap 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:
have he := (effectiveEpiFamily_tfae Xmap f).out 0 1
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 : 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