Theorem: Profinite.extensiveRegular_generates_coherent (Profinite/ExplicitSheaves.lean)

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
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

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
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

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 *
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

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
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

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]
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 π

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
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 π

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
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 π

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
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 π

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 α
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 π

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
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 π

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
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 π

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 π
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 π

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,_⟩
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 π

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
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 π

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 π)
he : EffectiveEpiFamily Xmap π ↔ Epi (Sigma.desc π)
⊢ EffectiveEpiFamily Xmap π
Tactic:
rw [he]
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 π)
⊢ Epi (Sigma.desc π)

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 π)
he : EffectiveEpiFamily Xmap π ↔ Epi (Sigma.desc π)
⊢ Epi (Sigma.desc π)
Tactic:
letI := h.2
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 π)
this : IsIso (Sigma.desc π) := h.right
⊢ Epi (Sigma.desc π)

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 π)
he : EffectiveEpiFamily Xmap π ↔ Epi (Sigma.desc π)
this : IsIso (Sigma.desc π) := h.right
⊢ Epi (Sigma.desc π)
Tactic:
exact inferInstance
State after:
no goals

State before:
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 π
Tactic:
obtain ⟨Z, f, h⟩ := h
State after:
case h.h.h.mp.of.hS.right.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Epi f
⊢ ∃ α x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π

State before:
case h.h.h.mp.of.hS.right.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Epi f
⊢ ∃ α x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Tactic:
use Unit
State after:
case h.h.h.mp.of.hS.right.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Epi f
⊢ ∃ x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π

State before:
case h.h.h.mp.of.hS.right.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Epi f
⊢ ∃ x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Tactic:
use inferInstance
State after:
case h.h.h.mp.of.hS.right.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Epi f
⊢ ∃ X π, T = ofArrows X π ∧ EffectiveEpiFamily X π

State before:
case h.h.h.mp.of.hS.right.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Epi f
⊢ ∃ X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
Tactic:
use (fun _ ↦ Z)
State after:
case h.h.h.mp.of.hS.right.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Epi f
⊢ ∃ π, T = ofArrows (fun x => Z) π ∧ EffectiveEpiFamily (fun x => Z) π

State before:
case h.h.h.mp.of.hS.right.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
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)
State after:
case h.h.h.mp.of.hS.right.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
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

State before:
case h.h.h.mp.of.hS.right.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
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,_⟩
State after:
case h.h.h.mp.of.hS.right.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
f : Z ⟶ Y
h : (T = ofArrows (fun x => Z) fun x => f) ∧ Epi f
⊢ EffectiveEpiFamily (fun x => Z) fun x => f

State before:
case h.h.h.mp.of.hS.right.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
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
State after:
case h.h.h.mp.of.hS.right.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
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

State before:
case h.h.h.mp.of.hS.right.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
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]
State after:
case h.h.h.mp.of.hS.right.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
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)

State before:
case h.h.h.mp.of.hS.right.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
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 [Profinite.epi_iff_surjective _] at h ⊢
State after:
case h.h.h.mp.of.hS.right.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
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)

State before:
case h.h.h.mp.of.hS.right.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
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
State after:
case h.h.h.mp.of.hS.right.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
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 : (forget Profinite).obj Y
⊢ ∃ a, ↑(Sigma.desc fun x => f) a = x

State before:
case h.h.h.mp.of.hS.right.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
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 : (forget Profinite).obj Y
⊢ ∃ a, ↑(Sigma.desc fun x => f) a = x
Tactic:
obtain ⟨y,hy⟩ := h.2 x
State after:
case h.h.h.mp.of.hS.right.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
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 : (forget Profinite).obj Y
y : (forget Profinite).obj Z
hy : ↑f y = x
⊢ ∃ a, ↑(Sigma.desc fun x => f) a = x

State before:
case h.h.h.mp.of.hS.right.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
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 : (forget Profinite).obj Y
y : (forget Profinite).obj Z
hy : ↑f y = x
⊢ ∃ a, ↑(Sigma.desc fun x => f) a = x
Tactic:
use Sigma.ι (fun (_ : Unit) ↦ Z) Unit.unit y
State after:
case h.h.h.mp.of.hS.right.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
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 : (forget Profinite).obj Y
y : (forget Profinite).obj Z
hy : ↑f y = x
⊢ ↑(Sigma.desc fun x => f) (↑(Sigma.ι (fun x => Z) ()) y) = x

State before:
case h.h.h.mp.of.hS.right.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
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 : (forget Profinite).obj Y
y : (forget Profinite).obj Z
hy : ↑f y = x
⊢ ↑(Sigma.desc fun x => f) (↑(Sigma.ι (fun x => Z) ()) y) = x
Tactic:
rw [← hy]
State after:
case h.h.h.mp.of.hS.right.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
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 : (forget Profinite).obj Y
y : (forget Profinite).obj Z
hy : ↑f y = x
⊢ ↑(Sigma.desc fun x => f) (↑(Sigma.ι (fun x => Z) ()) y) = ↑f y

State before:
case h.h.h.mp.of.hS.right.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
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 : (forget Profinite).obj Y
y : (forget Profinite).obj 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)
State after:
case h.h.h.mp.of.hS.right.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
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 : (forget Profinite).obj Y
y : (forget Profinite).obj 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 : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
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 : (forget Profinite).obj Y
y : (forget Profinite).obj Z
hy : ↑f y = x
⊢ ↑f = ↑(Sigma.ι (fun x => Z) () ≫ Sigma.desc fun x => f)

State before:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
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 : (forget Profinite).obj Y
y : (forget Profinite).obj 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]
State after:
no goals

State before:
case h.h.h.mp.of.hS.right.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
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 : (forget Profinite).obj Y
y : (forget Profinite).obj 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]
State after:
case h.h.h.mp.of.hS.right.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
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 : (forget Profinite).obj Y
y : (forget Profinite).obj 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

State before:
case h.h.h.mp.of.hS.right.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ ExtensiveSieve Y ∪ RegularSieve Y
Z : Profinite
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 : (forget Profinite).obj Y
y : (forget Profinite).obj 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
State after:
no goals

State before:
case h.h.h.mp.top
X : Profinite
S : Sieve X
X✝ : Profinite
⊢ ⊤ ∈ GrothendieckTopology.sieves (coherentTopology Profinite) X✝
Tactic:
apply Coverage.saturate.top
State after:
no goals

State before:
case h.h.h.mp.transitive
X : Profinite
S : Sieve X
Y : Profinite
T S✝ : Sieve Y
a✝¹ :
  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)))
    Y T
a✝ :
  ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f →
      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)))
        Y_1 (Sieve.pullback f S✝)
a_ih✝¹ : T ∈ GrothendieckTopology.sieves (coherentTopology Profinite) Y
a_ih✝ :
  ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Sieve.pullback f S✝ ∈ GrothendieckTopology.sieves (coherentTopology Profinite) Y_1
⊢ S✝ ∈ GrothendieckTopology.sieves (coherentTopology Profinite) Y
Tactic:
apply Coverage.saturate.transitive Y T
State after:
case h.h.h.mp.transitive.a
X : Profinite
S : Sieve X
Y : Profinite
T S✝ : Sieve Y
a✝¹ :
  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)))
    Y T
a✝ :
  ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f →
      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)))
        Y_1 (Sieve.pullback f S✝)
a_ih✝¹ : T ∈ GrothendieckTopology.sieves (coherentTopology Profinite) Y
a_ih✝ :
  ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Sieve.pullback f S✝ ∈ GrothendieckTopology.sieves (coherentTopology Profinite) Y_1
⊢ Coverage.saturate (coherentCoverage Profinite) Y T

case h.h.h.mp.transitive.a
X : Profinite
S : Sieve X
Y : Profinite
T S✝ : Sieve Y
a✝¹ :
  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)))
    Y T
a✝ :
  ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f →
      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)))
        Y_1 (Sieve.pullback f S✝)
a_ih✝¹ : T ∈ GrothendieckTopology.sieves (coherentTopology Profinite) Y
a_ih✝ :
  ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Sieve.pullback f S✝ ∈ GrothendieckTopology.sieves (coherentTopology Profinite) Y_1
⊢ ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Coverage.saturate (coherentCoverage Profinite) Y_1 (Sieve.pullback f S✝)

State before:
case h.h.h.mp.transitive.a
X : Profinite
S : Sieve X
Y : Profinite
T S✝ : Sieve Y
a✝¹ :
  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)))
    Y T
a✝ :
  ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f →
      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)))
        Y_1 (Sieve.pullback f S✝)
a_ih✝¹ : T ∈ GrothendieckTopology.sieves (coherentTopology Profinite) Y
a_ih✝ :
  ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Sieve.pullback f S✝ ∈ GrothendieckTopology.sieves (coherentTopology Profinite) Y_1
⊢ Coverage.saturate (coherentCoverage Profinite) Y T
Tactic:
assumption
State after:
no goals

State before:
case h.h.h.mp.transitive.a
X : Profinite
S : Sieve X
Y : Profinite
T S✝ : Sieve Y
a✝¹ :
  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)))
    Y T
a✝ :
  ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f →
      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)))
        Y_1 (Sieve.pullback f S✝)
a_ih✝¹ : T ∈ GrothendieckTopology.sieves (coherentTopology Profinite) Y
a_ih✝ :
  ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Sieve.pullback f S✝ ∈ GrothendieckTopology.sieves (coherentTopology Profinite) Y_1
⊢ ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Coverage.saturate (coherentCoverage Profinite) Y_1 (Sieve.pullback f S✝)
Tactic:
assumption
State after:
no goals

State before:
case h.h.h.mpr.of
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : T ∈ Coverage.covering (coherentCoverage Profinite) Y
⊢ Sieve.generate T ∈
    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))))
      Y
Tactic:
dsimp [coherentCoverage] at hT
State after:
case h.h.h.mpr.of
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : ∃ α x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
⊢ Sieve.generate T ∈
    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))))
      Y

State before:
case h.h.h.mpr.of
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
hT : ∃ α x X π, T = ofArrows X π ∧ EffectiveEpiFamily X π
⊢ Sieve.generate T ∈
    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))))
      Y
Tactic:
obtain ⟨I, hI, Xmap, f, ⟨h, hT⟩⟩ := hT
State after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : EffectiveEpiFamily Xmap f
⊢ Sieve.generate T ∈
    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))))
      Y

State before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : EffectiveEpiFamily Xmap f
⊢ Sieve.generate T ∈
    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))))
      Y
Tactic:
have he := (effectiveEpiFamily_tfae Xmap f).out 0 1
State after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : EffectiveEpiFamily Xmap f
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
⊢ Sieve.generate T ∈
    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))))
      Y

State before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : EffectiveEpiFamily Xmap f
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
⊢ Sieve.generate T ∈
    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))))
      Y
Tactic:
rw [he] at hT
State after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
⊢ Sieve.generate T ∈
    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))))
      Y

State before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
⊢ Sieve.generate T ∈
    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))))
      Y
Tactic:
let φ := fun (i : I) ↦ Sigma.ι Xmap i
State after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
⊢ Sieve.generate T ∈
    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))))
      Y

State before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
⊢ Sieve.generate T ∈
    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))))
      Y
Tactic:
let F := Sigma.desc f
State after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
⊢ Sieve.generate T ∈
    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))))
      Y

State before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
⊢ Sieve.generate T ∈
    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))))
      Y
Tactic:
let Z := Sieve.generate T
State after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
⊢ Sieve.generate T ∈
    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))))
      Y

State before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
⊢ Sieve.generate T ∈
    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))))
      Y
Tactic:
let Xs := (∐ fun (i : I) => Xmap i)
State after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
⊢ Sieve.generate T ∈
    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))))
      Y

State before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
⊢ Sieve.generate T ∈
    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))))
      Y
Tactic:
let Zf : Sieve Y := Sieve.generate 
  (Presieve.ofArrows (fun (_ : Unit) ↦ Xs) (fun (_ : Unit) ↦ F))
State after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ Sieve.generate T ∈
    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))))
      Y

State before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ Sieve.generate T ∈
    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))))
      Y
Tactic:
apply Coverage.saturate.transitive Y Zf
State after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ 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)))
    Y Zf

case h.h.h.mpr.of.intro.intro.intro.intro.intro.a
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    Zf.arrows f →
      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)))
        Y_1 (Sieve.pullback f (Sieve.generate T))

State before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ 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)))
    Y Zf
Tactic:
apply Coverage.saturate.of
State after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.hS
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ (ofArrows (fun x => Xs) fun x => F) ∈
    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

State before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.hS
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ (ofArrows (fun x => Xs) fun x => F) ∈
    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
Tactic:
dsimp [ExtensiveRegularCoverage']
State after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.hS
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ (ofArrows (fun x => ∐ fun i => Xmap i) fun x => Sigma.desc f) ∈ ExtensiveSieve Y ∪ RegularSieve Y

State before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.hS
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ (ofArrows (fun x => ∐ fun i => Xmap i) fun x => Sigma.desc f) ∈ ExtensiveSieve Y ∪ RegularSieve Y
Tactic:
simp only [Set.mem_union, Set.mem_setOf_eq]
State after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.hS
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ (ofArrows (fun x => ∐ fun i => Xmap i) fun x => Sigma.desc f) ∈ ExtensiveSieve Y ∨
    (ofArrows (fun x => ∐ fun i => Xmap i) fun x => Sigma.desc f) ∈ RegularSieve Y

State before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.hS
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ (ofArrows (fun x => ∐ fun i => Xmap i) fun x => Sigma.desc f) ∈ ExtensiveSieve Y ∨
    (ofArrows (fun x => ∐ fun i => Xmap i) fun x => Sigma.desc f) ∈ RegularSieve Y
Tactic:
right
State after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.hS.h
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ (ofArrows (fun x => ∐ fun i => Xmap i) fun x => Sigma.desc f) ∈ RegularSieve Y

State before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.hS.h
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ (ofArrows (fun x => ∐ fun i => Xmap i) fun x => Sigma.desc f) ∈ RegularSieve Y
Tactic:
use Xs
State after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.hS.h
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ ∃ f_1, ((ofArrows (fun x => ∐ fun i => Xmap i) fun x => Sigma.desc f) = ofArrows (fun x => Xs) fun x => f_1) ∧ Epi f_1

State before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.hS.h
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ ∃ f_1, ((ofArrows (fun x => ∐ fun i => Xmap i) fun x => Sigma.desc f) = ofArrows (fun x => Xs) fun x => f_1) ∧ Epi f_1
Tactic:
use F
State after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.hS.h
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ ((ofArrows (fun x => ∐ fun i => Xmap i) fun x => Sigma.desc f) = ofArrows (fun x => Xs) fun x => F) ∧ Epi F

State before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.hS.h
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ ((ofArrows (fun x => ∐ fun i => Xmap i) fun x => Sigma.desc f) = ofArrows (fun x => Xs) fun x => F) ∧ Epi F
Tactic:
refine' ⟨rfl, inferInstance⟩
State after:
no goals

State before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
⊢ ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    Zf.arrows f →
      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)))
        Y_1 (Sieve.pullback f (Sieve.generate T))
Tactic:
intro R g hZfg
State after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
hZfg : Zf.arrows g
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    R (Sieve.pullback g (Sieve.generate T))

State before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
hZfg : Zf.arrows g
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    R (Sieve.pullback g (Sieve.generate T))
Tactic:
dsimp at hZfg
State after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
hZfg : ∃ Y_1 h g_1, ofArrows (fun x => ∐ fun i => Xmap i) (fun x => Sigma.desc f) g_1 ∧ h ≫ g_1 = g
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    R (Sieve.pullback g (Sieve.generate T))

State before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
hZfg : ∃ Y_1 h g_1, ofArrows (fun x => ∐ fun i => Xmap i) (fun x => Sigma.desc f) g_1 ∧ h ≫ g_1 = g
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    R (Sieve.pullback g (Sieve.generate T))
Tactic:
rw [Presieve.ofArrows_pUnit] at hZfg
State after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
hZfg : ∃ Y_1 h g_1, Presieve.singleton (Sigma.desc f) g_1 ∧ h ≫ g_1 = g
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    R (Sieve.pullback g (Sieve.generate T))

State before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
hZfg : ∃ Y_1 h g_1, Presieve.singleton (Sigma.desc f) g_1 ∧ h ≫ g_1 = g
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    R (Sieve.pullback g (Sieve.generate T))
Tactic:
obtain ⟨W, ψ, σ, ⟨hW, hW'⟩⟩ := hZfg
State after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
ψ : R ⟶ W
σ : W ⟶ Y
hW : Presieve.singleton (Sigma.desc f) σ
hW' : ψ ≫ σ = g
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    R (Sieve.pullback g (Sieve.generate T))

State before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
ψ : R ⟶ W
σ : W ⟶ Y
hW : Presieve.singleton (Sigma.desc f) σ
hW' : ψ ≫ σ = g
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    R (Sieve.pullback g (Sieve.generate T))
Tactic:
dsimp [Presieve.singleton] at hW
State after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
ψ : R ⟶ W
σ : W ⟶ Y
hW : singleton' (Sigma.desc f) σ
hW' : ψ ≫ σ = g
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    R (Sieve.pullback g (Sieve.generate T))

State before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
ψ : R ⟶ W
σ : W ⟶ Y
hW : singleton' (Sigma.desc f) σ
hW' : ψ ≫ σ = g
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    R (Sieve.pullback g (Sieve.generate T))
Tactic:
induction hW
State after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro.mk
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    R (Sieve.pullback g (Sieve.generate T))

State before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro.mk
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    R (Sieve.pullback g (Sieve.generate T))
Tactic:
rw [← hW', Sieve.pullback_comp Z]
State after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro.mk
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    R (Sieve.pullback ψ (Sieve.pullback (Sigma.desc f) Z))

State before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro.mk
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    R (Sieve.pullback ψ (Sieve.pullback (Sigma.desc f) Z))
Tactic:
suffices : Sieve.pullback ψ ((Sieve.pullback F) Z) ∈ GrothendieckTopology.sieves
  (ExtensiveRegularCoverage' _ _ _).toGrothendieck R
State after:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro.mk
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this :
  Sieve.pullback ψ (Sieve.pullback F Z) ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck Profinite (ExtensiveRegularCoverage' Profinite ?m.588132 ?m.588133)) R
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    R (Sieve.pullback ψ (Sieve.pullback (Sigma.desc f) Z))

case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
⊢ Sieve.pullback ψ (Sieve.pullback F Z) ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck Profinite (ExtensiveRegularCoverage' Profinite ?m.588132 ?m.588133)) R

State before:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
⊢ Sieve.pullback ψ (Sieve.pullback F Z) ∈
    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))))
      R
Tactic:
apply GrothendieckTopology.pullback_stable'
State after:
case this.a
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
⊢ Sieve.pullback F Z ∈
    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))))
      (∐ fun i => Xmap i)

State before:
case this.a
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
⊢ Sieve.pullback F Z ∈
    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))))
      (∐ fun i => Xmap i)
Tactic:
dsimp [Coverage.toGrothendieck]
State after:
case this.a
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
⊢ Sieve.pullback (Sigma.desc f) (Sieve.generate T) ∈
    Coverage.saturate
      (ExtensiveRegularCoverage' Profinite
        (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
      (∐ fun i => Xmap i)

State before:
case this.a
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
⊢ Sieve.pullback (Sigma.desc f) (Sieve.generate T) ∈
    Coverage.saturate
      (ExtensiveRegularCoverage' Profinite
        (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
      (∐ fun i => Xmap i)
Tactic:
suffices : Coverage.saturate (ExtensiveRegularCoverage' _ _ _) Xs (Z.pullback F)
State after:
case this.a
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Coverage.saturate (ExtensiveRegularCoverage' Profinite ?m.593517 ?m.593518) Xs (Sieve.pullback F Z)
⊢ Sieve.pullback (Sigma.desc f) (Sieve.generate T) ∈
    Coverage.saturate
      (ExtensiveRegularCoverage' Profinite
        (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
      (∐ fun i => Xmap i)

case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
⊢ Coverage.saturate (ExtensiveRegularCoverage' Profinite ?m.593517 ?m.593518) Xs (Sieve.pullback F Z)

State before:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    Xs (Sieve.pullback F Z)
Tactic:
suffices : Sieve.generate (Presieve.ofArrows Xmap φ) ≤ Z.pullback F
State after:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    Xs (Sieve.pullback F Z)

case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
⊢ Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z

State before:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
⊢ Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
Tactic:
intro Q q hq
State after:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
hq : (Sieve.generate (ofArrows Xmap φ)).arrows q
⊢ (Sieve.pullback F Z).arrows q

State before:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
hq : (Sieve.generate (ofArrows Xmap φ)).arrows q
⊢ (Sieve.pullback F Z).arrows q
Tactic:
simp only [Sieve.pullback_apply, Sieve.generate_apply]
State after:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
hq : (Sieve.generate (ofArrows Xmap φ)).arrows q
⊢ ∃ Y_1 h g, T g ∧ h ≫ g = q ≫ Sigma.desc f

State before:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
hq : (Sieve.generate (ofArrows Xmap φ)).arrows q
⊢ ∃ Y_1 h g, T g ∧ h ≫ g = q ≫ Sigma.desc f
Tactic:
simp only [Sieve.generate_apply] at hq
State after:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
hq : ∃ Y h g, ofArrows Xmap (fun i => Sigma.ι Xmap i) g ∧ h ≫ g = q
⊢ ∃ Y_1 h g, T g ∧ h ≫ g = q ≫ Sigma.desc f

State before:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
hq : ∃ Y h g, ofArrows Xmap (fun i => Sigma.ι Xmap i) g ∧ h ≫ g = q
⊢ ∃ Y_1 h g, T g ∧ h ≫ g = q ≫ Sigma.desc f
Tactic:
obtain ⟨E, e, r, hq⟩ := hq
State after:
case this.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
E : Profinite
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ ∃ Y_1 h g, T g ∧ h ≫ g = q ≫ Sigma.desc f

State before:
case this.intro.intro.intro
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
E : Profinite
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ ∃ Y_1 h g, T g ∧ h ≫ g = q ≫ Sigma.desc f
Tactic:
refine' ⟨E, e, r ≫ F, ⟨_, _⟩⟩
State after:
case this.intro.intro.intro.refine'_1
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
E : Profinite
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ T (r ≫ F)

case this.intro.intro.intro.refine'_2
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
E : Profinite
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ e ≫ r ≫ F = q ≫ Sigma.desc f

State before:
case h.h.h.mpr.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro.mk
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this :
  Sieve.pullback ψ (Sieve.pullback F Z) ∈
    GrothendieckTopology.sieves
      (Coverage.toGrothendieck Profinite (ExtensiveRegularCoverage' Profinite ?m.588132 ?m.588133)) R
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    R (Sieve.pullback ψ (Sieve.pullback (Sigma.desc f) Z))
Tactic:
exact this
State after:
no goals

State before:
case this.a
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Coverage.saturate (ExtensiveRegularCoverage' Profinite ?m.593517 ?m.593518) Xs (Sieve.pullback F Z)
⊢ Sieve.pullback (Sigma.desc f) (Sieve.generate T) ∈
    Coverage.saturate
      (ExtensiveRegularCoverage' Profinite
        (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
      (∐ fun i => Xmap i)
Tactic:
exact this
State after:
no goals

State before:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    Xs (Sieve.pullback F Z)
Tactic:
apply Coverage.saturate_of_superset _ this
State after:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    (∐ Xmap) (Sieve.generate (ofArrows Xmap φ))

State before:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ Coverage.saturate
    (ExtensiveRegularCoverage' Profinite
      (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    (∐ Xmap) (Sieve.generate (ofArrows Xmap φ))
Tactic:
apply Coverage.saturate.of
State after:
case this.hS
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ ofArrows Xmap φ ∈
    Coverage.covering
      (ExtensiveRegularCoverage' Profinite
        (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
      (∐ Xmap)

State before:
case this.hS
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ ofArrows Xmap φ ∈
    Coverage.covering
      (ExtensiveRegularCoverage' Profinite
        (_ : ∀ {X Y Z : Profinite} (f : Y ⟶ X) (π : Z ⟶ X) [inst : Epi π], Epi Limits.pullback.fst)
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : Profinite} {Z : α → Profinite} (π : (a : α) → Z a ⟶ X) {Y : Profinite}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
      (∐ Xmap)
Tactic:
dsimp [ExtensiveRegularCoverage']
State after:
case this.hS
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ (ofArrows Xmap fun i => Sigma.ι Xmap i) ∈ ExtensiveSieve (∐ Xmap) ∪ RegularSieve (∐ Xmap)

State before:
case this.hS
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ (ofArrows Xmap fun i => Sigma.ι Xmap i) ∈ ExtensiveSieve (∐ Xmap) ∪ RegularSieve (∐ Xmap)
Tactic:
left
State after:
case this.hS.h
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ (ofArrows Xmap fun i => Sigma.ι Xmap i) ∈ ExtensiveSieve (∐ Xmap)

State before:
case this.hS.h
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ (ofArrows Xmap fun i => Sigma.ι Xmap i) ∈ ExtensiveSieve (∐ Xmap)
Tactic:
refine' ⟨I, hI, Xmap, φ, ⟨rfl, _⟩⟩
State after:
case this.hS.h
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ IsIso (Sigma.desc φ)

State before:
case this.hS.h
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ IsIso (Sigma.desc φ)
Tactic:
suffices : Sigma.desc φ = 𝟙 _
State after:
case this.hS.h
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this✝ : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
this : Sigma.desc φ = 𝟙 (∐ fun b => Xmap b)
⊢ IsIso (Sigma.desc φ)

case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ Sigma.desc φ = 𝟙 (∐ fun b => Xmap b)

State before:
case this
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
⊢ Sigma.desc φ = 𝟙 (∐ fun b => Xmap b)
Tactic:
ext
State after:
case this.h.w
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
b✝ : I
x✝ : (forget Profinite).obj (Xmap b✝)
⊢ ↑(Sigma.ι (fun b => Xmap b) b✝ ≫ Sigma.desc φ) x✝ = ↑(Sigma.ι (fun b => Xmap b) b✝ ≫ 𝟙 (∐ fun b => Xmap b)) x✝

State before:
case this.h.w
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
b✝ : I
x✝ : (forget Profinite).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]
State after:
no goals

State before:
case this.hS.h
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this✝ : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
this : Sigma.desc φ = 𝟙 (∐ fun b => Xmap b)
⊢ IsIso (Sigma.desc φ)
Tactic:
rw [this]
State after:
case this.hS.h
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this✝ : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
this : Sigma.desc φ = 𝟙 (∐ fun b => Xmap b)
⊢ IsIso (𝟙 (∐ fun b => Xmap b))

State before:
case this.hS.h
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
this✝ : Sieve.generate (ofArrows Xmap φ) ≤ Sieve.pullback F Z
this : Sigma.desc φ = 𝟙 (∐ fun b => Xmap b)
⊢ IsIso (𝟙 (∐ fun b => Xmap b))
Tactic:
exact inferInstance
State after:
no goals

State before:
case this.intro.intro.intro.refine'_1
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
E : Profinite
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ T (r ≫ F)
Tactic:
rw [h]
State after:
case this.intro.intro.intro.refine'_1
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
E : Profinite
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ ofArrows Xmap f (r ≫ F)

State before:
case this.intro.intro.intro.refine'_1
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
E : Profinite
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ ofArrows Xmap f (r ≫ F)
Tactic:
induction hq.1
State after:
case this.intro.intro.intro.refine'_1.mk
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
E : Profinite
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)

State before:
case this.intro.intro.intro.refine'_1.mk
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
E : Profinite
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
State after:
case this.intro.intro.intro.refine'_1.mk
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
E : Profinite
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)

State before:
case this.intro.intro.intro.refine'_1.mk
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
E : Profinite
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]
State after:
case this.intro.intro.intro.refine'_1.mk
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
E : Profinite
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✝)

State before:
case this.intro.intro.intro.refine'_1.mk
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
E : Profinite
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 _
State after:
no goals

State before:
case this.intro.intro.intro.refine'_2
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
E : Profinite
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ e ≫ r ≫ F = q ≫ Sigma.desc f
Tactic:
rw [← hq.2]
State after:
case this.intro.intro.intro.refine'_2
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
E : Profinite
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ e ≫ r ≫ F = (e ≫ r) ≫ Sigma.desc f

State before:
case this.intro.intro.intro.refine'_2
X : Profinite
S : Sieve X
Y : Profinite
T : Presieve Y
I : Type
hI : Fintype I
Xmap : I → Profinite
f : (a : I) → Xmap a ⟶ Y
h : T = ofArrows Xmap f
hT : Epi (Sigma.desc f)
he : EffectiveEpiFamily Xmap f ↔ Epi (Sigma.desc f)
φ : (i : I) → Xmap i ⟶ ∐ Xmap := fun i => Sigma.ι Xmap i
F : (∐ fun b => Xmap b) ⟶ Y := Sigma.desc f
Z : Sieve Y := Sieve.generate T
Xs : Profinite := ∐ fun i => Xmap i
Zf : Sieve Y := Sieve.generate (ofArrows (fun x => Xs) fun x => F)
R : Profinite
g : R ⟶ Y
W : Profinite
σ : W ⟶ Y
ψ : R ⟶ ∐ fun i => Xmap i
hW' : ψ ≫ Sigma.desc f = g
Q : Profinite
q : Q ⟶ ∐ Xmap
E : Profinite
e : Q ⟶ E
r : E ⟶ ∐ Xmap
hq : ofArrows Xmap (fun i => Sigma.ι Xmap i) r ∧ e ≫ r = q
⊢ e ≫ r ≫ F = (e ≫ r) ≫ Sigma.desc f
Tactic:
rfl
State after:
no goals

State before:
case h.h.h.mpr.top
X : Profinite
S : Sieve X
X✝ : Profinite
⊢ ⊤ ∈
    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✝
Tactic:
apply Coverage.saturate.top
State after:
no goals

State before:
case h.h.h.mpr.transitive
X : Profinite
S : Sieve X
Y : Profinite
T S✝ : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage Profinite) Y T
a✝ :
  ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Coverage.saturate (coherentCoverage Profinite) Y_1 (Sieve.pullback f S✝)
a_ih✝¹ :
  T ∈
    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))))
      Y
a_ih✝ :
  ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f →
      Sieve.pullback f 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))))
          Y_1
⊢ 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))))
      Y
Tactic:
apply Coverage.saturate.transitive Y T
State after:
case h.h.h.mpr.transitive.a
X : Profinite
S : Sieve X
Y : Profinite
T S✝ : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage Profinite) Y T
a✝ :
  ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Coverage.saturate (coherentCoverage Profinite) Y_1 (Sieve.pullback f S✝)
a_ih✝¹ :
  T ∈
    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))))
      Y
a_ih✝ :
  ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f →
      Sieve.pullback f 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))))
          Y_1
⊢ 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)))
    Y T

case h.h.h.mpr.transitive.a
X : Profinite
S : Sieve X
Y : Profinite
T S✝ : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage Profinite) Y T
a✝ :
  ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Coverage.saturate (coherentCoverage Profinite) Y_1 (Sieve.pullback f S✝)
a_ih✝¹ :
  T ∈
    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))))
      Y
a_ih✝ :
  ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f →
      Sieve.pullback f 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))))
          Y_1
⊢ ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f →
      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)))
        Y_1 (Sieve.pullback f S✝)

State before:
case h.h.h.mpr.transitive.a
X : Profinite
S : Sieve X
Y : Profinite
T S✝ : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage Profinite) Y T
a✝ :
  ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Coverage.saturate (coherentCoverage Profinite) Y_1 (Sieve.pullback f S✝)
a_ih✝¹ :
  T ∈
    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))))
      Y
a_ih✝ :
  ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f →
      Sieve.pullback f 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))))
          Y_1
⊢ 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)))
    Y T
Tactic:
assumption
State after:
no goals

State before:
case h.h.h.mpr.transitive.a
X : Profinite
S : Sieve X
Y : Profinite
T S✝ : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage Profinite) Y T
a✝ :
  ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Coverage.saturate (coherentCoverage Profinite) Y_1 (Sieve.pullback f S✝)
a_ih✝¹ :
  T ∈
    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))))
      Y
a_ih✝ :
  ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f →
      Sieve.pullback f 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))))
          Y_1
⊢ ∀ ⦃Y_1 : Profinite⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f →
      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)))
        Y_1 (Sieve.pullback f S✝)
Tactic:
assumption
State after:
no goals