internlm/Lean-Github huggingface dataset:
Theorem: Profinite.extensivity
Proof state before:
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (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: Profinite.extensivity
Proof state before:
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
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: Profinite.extensivity
Proof state before:
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
⊢ IsIso (finiteCoproduct.desc (fun a => Z a) i)
Tactic:
let ε := ToFiniteCoproductIso Z
Proof state after:
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
ε : ∐ Z ≅ finiteCoproduct Z := ToFiniteCoproductIso Z
⊢ IsIso (finiteCoproduct.desc (fun a => Z a) i)
Theorem: Profinite.extensivity
Proof state before:
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
ε : ∐ 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 : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
ε : ∐ Z ≅ finiteCoproduct Z := ToFiniteCoproductIso Z
⊢ ε.hom ≫ finiteCoproduct.desc Z i = Sigma.desc i
Theorem: Profinite.extensivity
Proof state before:
case h.e'_5
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
ε : ∐ 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 : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
ε : ∐ Z ≅ finiteCoproduct Z := ToFiniteCoproductIso Z
a : α
⊢ Sigma.ι Z a ≫ ε.hom ≫ finiteCoproduct.desc Z i = Sigma.ι Z a ≫ Sigma.desc i
Theorem: Profinite.extensivity
Proof state before:
case h.e'_5
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
ε : ∐ 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: Profinite.extensivity
Proof state before:
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
ε : ∐ 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: Profinite.epi_pullback_of_epi
Proof state before:
⊢ EpiPullbackOfEpi Profinite
Tactic:
intro X Y Z f π hπ
Proof state after:
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Epi π
⊢ Epi Limits.pullback.fst
Theorem: Profinite.epi_pullback_of_epi
Proof state before:
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Epi π
⊢ Epi Limits.pullback.fst
Tactic:
suffices : Epi (fromExplicit f π ≫ (Limits.pullback.fst : Limits.pullback f π ⟶ Y))
Proof state after:
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Epi π
this : Epi (fromExplicit f π ≫ Limits.pullback.fst)
⊢ Epi Limits.pullback.fst

case this
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Epi π
⊢ Epi (fromExplicit f π ≫ Limits.pullback.fst)
Theorem: Profinite.epi_pullback_of_epi
Proof state before:
case this
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Epi π
⊢ Epi (fromExplicit f π ≫ Limits.pullback.fst)
Tactic:
rw [Profinite.epi_iff_surjective] at hπ ⊢
Proof state after:
case this
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
⊢ Function.Surjective ↑(fromExplicit f π ≫ Limits.pullback.fst)
Theorem: Profinite.epi_pullback_of_epi
Proof state before:
case this
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
⊢ Function.Surjective ↑(fromExplicit f π ≫ Limits.pullback.fst)
Tactic:
intro y
Proof state after:
case this
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
y : (forget Profinite).obj Y
⊢ ∃ a, ↑(fromExplicit f π ≫ Limits.pullback.fst) a = y
Theorem: Profinite.epi_pullback_of_epi
Proof state before:
case this
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
y : (forget Profinite).obj Y
⊢ ∃ a, ↑(fromExplicit f π ≫ Limits.pullback.fst) a = y
Tactic:
obtain ⟨z,hz⟩ := hπ (f y)
Proof state after:
case this.intro
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
y : (forget Profinite).obj Y
z : (forget Profinite).obj Z
hz : ↑π z = ↑f y
⊢ ∃ a, ↑(fromExplicit f π ≫ Limits.pullback.fst) a = y
Theorem: Profinite.epi_pullback_of_epi
Proof state before:
case this.intro
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
y : (forget Profinite).obj Y
z : (forget Profinite).obj Z
hz : ↑π z = ↑f y
⊢ ∃ a, ↑(fromExplicit f π ≫ Limits.pullback.fst) a = y
Tactic:
have : fromExplicit f π ≫ Limits.pullback.fst = Profinite.pullback.fst f π
Proof state after:
case this
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
y : (forget Profinite).obj Y
z : (forget Profinite).obj Z
hz : ↑π z = ↑f y
⊢ fromExplicit f π ≫ Limits.pullback.fst = pullback.fst f π

case this.intro
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
y : (forget Profinite).obj Y
z : (forget Profinite).obj Z
hz : ↑π z = ↑f y
this : fromExplicit f π ≫ Limits.pullback.fst = pullback.fst f π
⊢ ∃ a, ↑(fromExplicit f π ≫ Limits.pullback.fst) a = y
Theorem: Profinite.epi_pullback_of_epi
Proof state before:
case this.intro
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
y : (forget Profinite).obj Y
z : (forget Profinite).obj Z
hz : ↑π z = ↑f y
this : fromExplicit f π ≫ Limits.pullback.fst = pullback.fst f π
⊢ ∃ a, ↑(fromExplicit f π ≫ Limits.pullback.fst) a = y
Tactic:
rw [this]
Proof state after:
case this.intro
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
y : (forget Profinite).obj Y
z : (forget Profinite).obj Z
hz : ↑π z = ↑f y
this : fromExplicit f π ≫ Limits.pullback.fst = pullback.fst f π
⊢ ∃ a, ↑(pullback.fst f π) a = y
Theorem: Profinite.epi_pullback_of_epi
Proof state before:
case this.intro
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
y : (forget Profinite).obj Y
z : (forget Profinite).obj Z
hz : ↑π z = ↑f y
this : fromExplicit f π ≫ Limits.pullback.fst = pullback.fst f π
⊢ ∃ a, ↑(pullback.fst f π) a = y
Tactic:
exact ⟨⟨(y, z), hz.symm⟩, rfl⟩
Proof state after:
no goals
Theorem: Profinite.epi_pullback_of_epi
Proof state before:
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Epi π
this : Epi (fromExplicit f π ≫ Limits.pullback.fst)
⊢ Epi Limits.pullback.fst
Tactic:
exact @epi_of_epi _ _ _ _ _ _ _ this
Proof state after:
no goals
Theorem: Profinite.epi_pullback_of_epi
Proof state before:
case this
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
y : (forget Profinite).obj Y
z : (forget Profinite).obj Z
hz : ↑π z = ↑f y
⊢ fromExplicit f π ≫ Limits.pullback.fst = pullback.fst f π
Tactic:
dsimp [fromExplicit]
Proof state after:
case this
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
y : (forget Profinite).obj Y
z : (forget Profinite).obj Z
hz : ↑π z = ↑f y
⊢ Limits.pullback.lift (pullback.fst f π) (pullback.snd f π) (_ : pullback.fst f π ≫ f = pullback.snd f π ≫ π) ≫
      Limits.pullback.fst =
    pullback.fst f π
Theorem: Profinite.epi_pullback_of_epi
Proof state before:
case this
X Y Z : Profinite
f : Y ⟶ X
π : Z ⟶ X
hπ : Function.Surjective ↑π
y : (forget Profinite).obj Y
z : (forget Profinite).obj Z
hz : ↑π z = ↑f y
⊢ Limits.pullback.lift (pullback.fst f π) (pullback.snd f π) (_ : pullback.fst f π ≫ f = pullback.snd f π ≫ π) ≫
      Limits.pullback.fst =
    pullback.fst f π
Tactic:
simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]
Proof state after:
no goals
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
⊢ Coverage.toGrothendieck Profinite
      (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))) =
    coherentTopology Profinite
Tactic:
ext X S
Proof state after:
case h.h.h
X : Profinite
S : Sieve X
⊢ S ∈
      GrothendieckTopology.sieves
        (Coverage.toGrothendieck Profinite
          (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))))
        X ↔
    S ∈ GrothendieckTopology.sieves (coherentTopology Profinite) X
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case h.h.h
X : Profinite
S : Sieve X
⊢ S ∈
      GrothendieckTopology.sieves
        (Coverage.toGrothendieck Profinite
          (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))))
        X ↔
    S ∈ GrothendieckTopology.sieves (coherentTopology Profinite) X
Tactic:
constructor
<;> intro h
Proof state after:
case h.h.h.mp
X : Profinite
S : Sieve X
h :
  S ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck Profinite
        (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))))
      X
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology Profinite) X

case h.h.h.mpr
X : Profinite
S : Sieve X
h : S ∈ GrothendieckTopology.sieves (coherentTopology Profinite) X
⊢ S ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck Profinite
        (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))))
      X
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp
X : Profinite
S : Sieve X
h :
  S ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck Profinite
        (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))))
      X
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology Profinite) X
Tactic:
dsimp [Coverage.toGrothendieck] at *
Proof state after:
case h.h.h.mp
X : Profinite
S : Sieve X
h :
  S ∈
    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)))
      X
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology Profinite) X
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT :
  T ∈
    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)))
      Y
⊢ Sieve.generate T ∈ GrothendieckTopology.sieves (coherentTopology Profinite) Y
Tactic:
apply Coverage.saturate.of
Proof state after:
case h.h.h.mp.of.hS
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT :
  T ∈
    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)))
      Y
⊢ T ∈ Coverage.covering (coherentCoverage Profinite) Y
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT :
  T ∈
    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)))
      Y
⊢ T ∈ Coverage.covering (coherentCoverage Profinite) Y
Tactic:
dsimp [coherentCoverage]
Proof state after:
case h.h.h.mp.of.hS
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT :
  T ∈
    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)))
      Y
⊢ ∃ α x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT :
  T ∈
    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)))
      Y
⊢ ∃ α x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Tactic:
dsimp [ExtensiveRegularCoverage'] at hT
Proof state after:
case h.h.h.mp.of.hS
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
⊢ ∃ α x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS
X : Profinite
S : Sieve X
Y : Profinite
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 : Profinite
S : Sieve X
Y : Profinite
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 : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
h : T ∈ RegularSieve Y
⊢ ∃ α x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.left
X : Profinite
S : Sieve X
Y : Profinite
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 : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
α : Type
x : Fintype α
Xmap : α → Profinite
π : (a : α) → Xmap a ⟶ Y
h : T = ofArrows Xmap π ∧ IsIso (Sigma.desc π)
⊢ ∃ α x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.left.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
α : Type
x : Fintype α
Xmap : α → Profinite
π : (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 : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
α : Type
x : Fintype α
Xmap : α → Profinite
π : (a : α) → Xmap a ⟶ Y
h : T = ofArrows Xmap π ∧ IsIso (Sigma.desc π)
⊢ ∃ x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.left.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
α : Type
x : Fintype α
Xmap : α → Profinite
π : (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 : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
α : Type
x : Fintype α
Xmap : α → Profinite
π : (a : α) → Xmap a ⟶ Y
h : T = ofArrows Xmap π ∧ IsIso (Sigma.desc π)
⊢ ∃ X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.left.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
α : Type
x : Fintype α
Xmap : α → Profinite
π : (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 : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
α : Type
x : Fintype α
Xmap : α → Profinite
π : (a : α) → Xmap a ⟶ Y
h : T = ofArrows Xmap π ∧ IsIso (Sigma.desc π)
⊢ ∃ π, T = ofArrows Xmap π ∧ EffectiveEpiFamily Xmap π
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.left.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
α : Type
x : Fintype α
Xmap : α → Profinite
π : (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 : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
α : Type
x : Fintype α
Xmap : α → Profinite
π : (a : α) → Xmap a ⟶ Y
h : T = ofArrows Xmap π ∧ IsIso (Sigma.desc π)
⊢ T = ofArrows Xmap π ∧ EffectiveEpiFamily Xmap π
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.left.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
α : Type
x : Fintype α
Xmap : α → Profinite
π : (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 : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
α : Type
x : Fintype α
Xmap : α → Profinite
π : (a : α) → Xmap a ⟶ Y
h : T = ofArrows Xmap π ∧ IsIso (Sigma.desc π)
⊢ EffectiveEpiFamily Xmap π
Theorem: Profinite.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.of.hS.left.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
α : Type
x : Fintype α
Xmap : α → Profinite
π : (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 : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
α : Type
x : Fintype α
Xmap : α → Profinite
π : (a : α) → Xmap a ⟶ Y
h : T = ofArrows Xmap π ∧ IsIso (Sigma.desc π)
he : EffectiveEpiFamily Xmap π ↔ Epi (Sigma.desc π)
⊢ EffectiveEpiFamily Xmap π