Theorem: Profinite.extensiveRegular_generates_coherent
Proof 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
Proof 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✝)