internlm/Lean-Github huggingface dataset:
Theorem: ExtrDisc.extensivity
Proof state before:
case h.e'_5
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) i)
a : α
⊢ (finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫
      δ.hom ≫ θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst) =
    finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫
      finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) fun a =>
        ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(i a))
Tactic:
simp [← Category.assoc, finiteCoproduct.ι_desc, fromExplicit]
Proof state after:
no goals
Theorem: ExtrDisc.extensivity
Proof state before:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
this : IsIso (θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst)
⊢ IsIso (Sigma.desc fun x => Limits.pullback.fst)
Tactic:
apply IsIso.of_isIso_comp_left θ.hom
Proof state after:
no goals
Theorem: ExtrDisc.extensivity
Proof state before:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
this : IsIso (δ.hom ≫ θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst)
⊢ IsIso (θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst)
Tactic:
apply IsIso.of_isIso_comp_left δ.hom
Proof state after:
no goals
Theorem: ExtrDisc.extensivity
Proof state before:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
⊢ IsIso (finiteCoproduct.desc (fun a => Z a) i)
Tactic:
let ε := ToFiniteCoproductIso Z
Proof state after:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
ε : ∐ Z ≅ finiteCoproduct Z := ToFiniteCoproductIso Z
⊢ IsIso (finiteCoproduct.desc (fun a => Z a) i)
Theorem: ExtrDisc.extensivity
Proof state before:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
ε : ∐ Z ≅ finiteCoproduct Z := ToFiniteCoproductIso Z
⊢ IsIso (ε.hom ≫ finiteCoproduct.desc Z i)
Tactic:
convert H
Proof state after:
case h.e'_5
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
ε : ∐ Z ≅ finiteCoproduct Z := ToFiniteCoproductIso Z
⊢ ε.hom ≫ finiteCoproduct.desc Z i = Sigma.desc i
Theorem: ExtrDisc.extensivity
Proof state before:
case h.e'_5
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
ε : ∐ Z ≅ finiteCoproduct Z := ToFiniteCoproductIso Z
⊢ ε.hom ≫ finiteCoproduct.desc Z i = Sigma.desc i
Tactic:
refine' Sigma.hom_ext _ _ (fun a => _)
Proof state after:
case h.e'_5
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
ε : ∐ Z ≅ finiteCoproduct Z := ToFiniteCoproductIso Z
a : α
⊢ Sigma.ι Z a ≫ ε.hom ≫ finiteCoproduct.desc Z i = Sigma.ι Z a ≫ Sigma.desc i
Theorem: ExtrDisc.extensivity
Proof state before:
case h.e'_5
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
ε : ∐ Z ≅ finiteCoproduct Z := ToFiniteCoproductIso Z
a : α
⊢ Sigma.ι Z a ≫ ε.hom ≫ finiteCoproduct.desc Z i = Sigma.ι Z a ≫ Sigma.desc i
Tactic:
simp [← Category.assoc]
Proof state after:
no goals
Theorem: ExtrDisc.extensivity
Proof state before:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
ε : ∐ Z ≅ finiteCoproduct Z := ToFiniteCoproductIso Z
this : IsIso (ε.hom ≫ finiteCoproduct.desc Z i)
⊢ IsIso (finiteCoproduct.desc (fun a => Z a) i)
Tactic:
apply IsIso.of_isIso_comp_left ε.hom
Proof state after:
no goals
Theorem: ExtrDisc.everything_proj
Proof state before:
⊢ EverythingIsProjective ExtrDisc
Tactic:
refine' fun P => ⟨(@fun X Y f e he => _)⟩
Proof state after:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
⊢ ∃ f', f' ≫ e = f
Theorem: ExtrDisc.everything_proj
Proof state before:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
⊢ ∃ f', f' ≫ e = f
Tactic:
have proj : Projective (toCompHaus.obj P) := inferInstanceAs (Projective P.compHaus)
Proof state after:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
⊢ ∃ f', f' ≫ e = f
Theorem: ExtrDisc.everything_proj
Proof state before:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
⊢ ∃ f', f' ≫ e = f
Tactic:
have : Epi (toCompHaus.map e) := by rw [CompHaus.epi_iff_surjective]
  change Function.Surjective e
  rwa [← ExtrDisc.epi_iff_surjective]
Proof state after:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
this : Epi (toCompHaus.map e)
⊢ ∃ f', f' ≫ e = f
Theorem: ExtrDisc.everything_proj
Proof state before:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
this : Epi (toCompHaus.map e)
⊢ ∃ f', f' ≫ e = f
Tactic:
set g := toCompHaus.preimage <| Projective.factorThru (toCompHaus.map f) (toCompHaus.map e) with hg
Proof state after:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
this : Epi (toCompHaus.map e)
g : P ⟶ X := toCompHaus.preimage (Projective.factorThru (toCompHaus.map f) (toCompHaus.map e))
hg : g = toCompHaus.preimage (Projective.factorThru (toCompHaus.map f) (toCompHaus.map e))
⊢ ∃ f', f' ≫ e = f
Theorem: ExtrDisc.everything_proj
Proof state before:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
this : Epi (toCompHaus.map e)
g : P ⟶ X := toCompHaus.preimage (Projective.factorThru (toCompHaus.map f) (toCompHaus.map e))
hg : g = toCompHaus.preimage (Projective.factorThru (toCompHaus.map f) (toCompHaus.map e))
⊢ ∃ f', f' ≫ e = f
Tactic:
refine' ⟨g, toCompHaus.map_injective _⟩
Proof state after:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
this : Epi (toCompHaus.map e)
g : P ⟶ X := toCompHaus.preimage (Projective.factorThru (toCompHaus.map f) (toCompHaus.map e))
hg : g = toCompHaus.preimage (Projective.factorThru (toCompHaus.map f) (toCompHaus.map e))
⊢ toCompHaus.map (g ≫ e) = toCompHaus.map f
Theorem: ExtrDisc.everything_proj
Proof state before:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
this : Epi (toCompHaus.map e)
g : P ⟶ X := toCompHaus.preimage (Projective.factorThru (toCompHaus.map f) (toCompHaus.map e))
hg : g = toCompHaus.preimage (Projective.factorThru (toCompHaus.map f) (toCompHaus.map e))
⊢ toCompHaus.map (g ≫ e) = toCompHaus.map f
Tactic:
rw [map_comp, hg, image_preimage, Projective.factorThru_comp]
Proof state after:
no goals
Theorem: ExtrDisc.everything_proj
Proof state before:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
⊢ Epi (toCompHaus.map e)
Tactic:
rw [CompHaus.epi_iff_surjective]
Proof state after:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
⊢ Function.Surjective ↑(toCompHaus.map e)
Theorem: ExtrDisc.everything_proj
Proof state before:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
⊢ Function.Surjective ↑(toCompHaus.map e)
Tactic:
change Function.Surjective e
Proof state after:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
⊢ Function.Surjective ↑e
Theorem: ExtrDisc.everything_proj
Proof state before:
P X Y : ExtrDisc
f : P ⟶ Y
e : X ⟶ Y
he : Epi e
proj : Projective (toCompHaus.obj P)
⊢ Function.Surjective ↑e
Tactic:
rwa [← ExtrDisc.epi_iff_surjective]
Proof state after:
no goals
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
⊢ 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))) =
    coherentTopology ExtrDisc
Tactic:
ext X S
Proof state after:
case h.h.h
X : ExtrDisc
S : Sieve X
⊢ 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))))
        X ↔
    S ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) X
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h
X : ExtrDisc
S : Sieve X
⊢ 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))))
        X ↔
    S ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) X
Tactic:
constructor
<;> intro h
Proof state after:
case h.h.h.mp
X : ExtrDisc
S : Sieve X
h :
  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))))
      X
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) X

case h.h.h.mpr
X : ExtrDisc
S : Sieve X
h : S ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) X
⊢ 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))))
      X
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp
X : ExtrDisc
S : Sieve X
h :
  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))))
      X
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) X
Tactic:
dsimp [Coverage.toGrothendieck] at *
Proof state after:
case h.h.h.mp
X : ExtrDisc
S : Sieve X
h :
  S ∈
    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)))
      X
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) X
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT :
  T ∈
    Coverage.covering
      (ExtensiveRegularCoverage ExtrDisc everything_proj
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
      Y
⊢ Sieve.generate T ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) Y
Tactic:
apply Coverage.saturate.of
Proof state after:
case h.h.h.mp.of.hS
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT :
  T ∈
    Coverage.covering
      (ExtensiveRegularCoverage ExtrDisc everything_proj
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
      Y
⊢ T ∈ Coverage.covering (coherentCoverage ExtrDisc) Y
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT :
  T ∈
    Coverage.covering
      (ExtensiveRegularCoverage ExtrDisc everything_proj
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
      Y
⊢ T ∈ Coverage.covering (coherentCoverage ExtrDisc) Y
Tactic:
dsimp [coherentCoverage]
Proof state after:
case h.h.h.mp.of.hS
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT :
  T ∈
    Coverage.covering
      (ExtensiveRegularCoverage ExtrDisc everything_proj
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
      Y
⊢ ∃ α x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT :
  T ∈
    Coverage.covering
      (ExtensiveRegularCoverage ExtrDisc everything_proj
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
      Y
⊢ ∃ α x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Tactic:
dsimp [ExtensiveRegularCoverage] at hT
Proof state after:
case h.h.h.mp.of.hS
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
⊢ ∃ α x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
⊢ ∃ α x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Tactic:
apply Or.elim hT
<;> intro h
Proof state after:
case h.h.h.mp.of.hS.left
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
h : T ∈ ExtensiveSieve Y
⊢ ∃ α x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π

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 π
Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.left
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
h : T ∈ ExtensiveSieve Y
⊢ ∃ α x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Tactic:
obtain ⟨α, x, Xmap, π, h⟩ := h
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 π)
⊢ ∃ α x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
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 π)
⊢ ∃ α x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Tactic:
use α
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 π)
⊢ ∃ x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
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 π)
⊢ ∃ x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Tactic:
use x
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 π)
⊢ ∃ X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
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 π)
⊢ ∃ X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Tactic:
use Xmap
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 π)
⊢ ∃ π, T = ofArrows Xmap π ∧ 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 π)
⊢ ∃ π, T = ofArrows Xmap π ∧ EffectiveEpiFamily Xmap π
Tactic:
use π
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 π)
⊢ T = ofArrows Xmap π ∧ 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 π)
⊢ T = ofArrows Xmap π ∧ EffectiveEpiFamily Xmap π
Tactic:
refine' ⟨h.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 π)
⊢ EffectiveEpiFamily Xmap π