Theorem: ExtrDisc.extensiveRegular_generates_coherent
Proof state before:
case h.h.h.mp.transitive
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T S✝ : Sieve Y
a✝¹ :
  Coverage.saturate
    (ExtensiveRegularCoverage ExtrDisc everything_proj
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    Y T
a✝ :
  ∀ ⦃Y_1 : ExtrDisc⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f →
      Coverage.saturate
        (ExtensiveRegularCoverage ExtrDisc everything_proj
          (_ :
            ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
              (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
        Y_1 (Sieve.pullback f S✝)
a_ih✝¹ : T ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) Y
a_ih✝ :
  ∀ ⦃Y_1 : ExtrDisc⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Sieve.pullback f S✝ ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) Y_1
⊢ S✝ ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) Y
Tactic:
apply Coverage.saturate.transitive Y T
Proof state after:
case h.h.h.mp.transitive.a
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T S✝ : Sieve Y
a✝¹ :
  Coverage.saturate
    (ExtensiveRegularCoverage ExtrDisc everything_proj
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    Y T
a✝ :
  ∀ ⦃Y_1 : ExtrDisc⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f →
      Coverage.saturate
        (ExtensiveRegularCoverage ExtrDisc everything_proj
          (_ :
            ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
              (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
        Y_1 (Sieve.pullback f S✝)
a_ih✝¹ : T ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) Y
a_ih✝ :
  ∀ ⦃Y_1 : ExtrDisc⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Sieve.pullback f S✝ ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) Y_1
⊢ Coverage.saturate (coherentCoverage ExtrDisc) Y T

case h.h.h.mp.transitive.a
X : ExtrDisc
S : Sieve X
Y : ExtrDisc
T S✝ : Sieve Y
a✝¹ :
  Coverage.saturate
    (ExtensiveRegularCoverage ExtrDisc everything_proj
      (_ :
        ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
          (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
    Y T
a✝ :
  ∀ ⦃Y_1 : ExtrDisc⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f →
      Coverage.saturate
        (ExtensiveRegularCoverage ExtrDisc everything_proj
          (_ :
            ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
              (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
        Y_1 (Sieve.pullback f S✝)
a_ih✝¹ : T ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) Y
a_ih✝ :
  ∀ ⦃Y_1 : ExtrDisc⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Sieve.pullback f S✝ ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) Y_1
⊢ ∀ ⦃Y_1 : ExtrDisc⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Coverage.saturate (coherentCoverage ExtrDisc) Y_1 (Sieve.pullback f S✝)