Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily (Condensed/Equivalence.lean)

State before:
X : ExtrDisc
S : Sieve X
⊢ (∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) ↔
    S ∈ GrothendieckTopology.sieves (CoverDense.inducedTopology coverDense) X
Tactic:
constructor
State after:
case mp
X : ExtrDisc
S : Sieve X
⊢ (∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) →
    S ∈ GrothendieckTopology.sieves (CoverDense.inducedTopology coverDense) X

case mpr
X : ExtrDisc
S : Sieve X
⊢ S ∈ GrothendieckTopology.sieves (CoverDense.inducedTopology coverDense) X →
    ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mp
X : ExtrDisc
S : Sieve X
⊢ (∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) →
    S ∈ GrothendieckTopology.sieves (CoverDense.inducedTopology coverDense) X
Tactic:
rintro ⟨α, _, Y, π, ⟨H₁, H₂⟩⟩
State after:
case mp.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ S ∈ GrothendieckTopology.sieves (CoverDense.inducedTopology coverDense) X

State before:
case mp.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ S ∈ GrothendieckTopology.sieves (CoverDense.inducedTopology coverDense) X
Tactic:
unfold CoverDense.inducedTopology
State after:
case mp.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ S ∈
    GrothendieckTopology.sieves
      (LocallyCoverDense.inducedTopology (_ : LocallyCoverDense (coherentTopology CompHaus) ExtrDisc.toCompHaus)) X

State before:
case mp.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ S ∈
    GrothendieckTopology.sieves
      (LocallyCoverDense.inducedTopology (_ : LocallyCoverDense (coherentTopology CompHaus) ExtrDisc.toCompHaus)) X
Tactic:
unfold LocallyCoverDense.inducedTopology
State after:
case mp.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ S ∈
    GrothendieckTopology.sieves
      {
        sieves := fun X S =>
          GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)
            (Sieve.functorPushforward ExtrDisc.toCompHaus S),
        top_mem' :=
          (_ :
            ∀ (X : ExtrDisc),
              GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)
                (Sieve.functorPushforward ExtrDisc.toCompHaus ⊤)),
        pullback_stable' :=
          (_ :
            ∀ (X Y : ExtrDisc) (S : Sieve X) (f : Y ⟶ X),
              S ∈
                  (fun X S =>
                      GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)
                        (Sieve.functorPushforward ExtrDisc.toCompHaus S))
                    X →
                Sieve.pullback f S ∈
                  (fun X S =>
                      GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)
                        (Sieve.functorPushforward ExtrDisc.toCompHaus S))
                    Y),
        transitive' :=
          (_ :
            ∀ (X : ExtrDisc) (S : Sieve X),
              S ∈
                  (fun X S =>
                      GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)
                        (Sieve.functorPushforward ExtrDisc.toCompHaus S))
                    X →
                ∀ (S' : Sieve X),
                  (∀ ⦃Y : ExtrDisc⦄ ⦃f : Y ⟶ X⦄,
                      S.arrows f →
                        Sieve.pullback f S' ∈
                          (fun X S =>
                              GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)
                                (Sieve.functorPushforward ExtrDisc.toCompHaus S))
                            Y) →
                    Sieve.functorPushforward ExtrDisc.toCompHaus S' ∈
                      GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)) }
      X

State before:
case mp.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ S ∈
    GrothendieckTopology.sieves
      {
        sieves := fun X S =>
          GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)
            (Sieve.functorPushforward ExtrDisc.toCompHaus S),
        top_mem' :=
          (_ :
            ∀ (X : ExtrDisc),
              GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)
                (Sieve.functorPushforward ExtrDisc.toCompHaus ⊤)),
        pullback_stable' :=
          (_ :
            ∀ (X Y : ExtrDisc) (S : Sieve X) (f : Y ⟶ X),
              S ∈
                  (fun X S =>
                      GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)
                        (Sieve.functorPushforward ExtrDisc.toCompHaus S))
                    X →
                Sieve.pullback f S ∈
                  (fun X S =>
                      GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)
                        (Sieve.functorPushforward ExtrDisc.toCompHaus S))
                    Y),
        transitive' :=
          (_ :
            ∀ (X : ExtrDisc) (S : Sieve X),
              S ∈
                  (fun X S =>
                      GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)
                        (Sieve.functorPushforward ExtrDisc.toCompHaus S))
                    X →
                ∀ (S' : Sieve X),
                  (∀ ⦃Y : ExtrDisc⦄ ⦃f : Y ⟶ X⦄,
                      S.arrows f →
                        Sieve.pullback f S' ∈
                          (fun X S =>
                              GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)
                                (Sieve.functorPushforward ExtrDisc.toCompHaus S))
                            Y) →
                    Sieve.functorPushforward ExtrDisc.toCompHaus S' ∈
                      GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)) }
      X
Tactic:
simp only [ExtrDisc.toCompHaus_obj]
State after:
case mp.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ S ∈ fun S =>
    GrothendieckTopology.sieves (coherentTopology CompHaus) X.compHaus (Sieve.functorPushforward ExtrDisc.toCompHaus S)

State before:
case mp.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ S ∈ fun S =>
    GrothendieckTopology.sieves (coherentTopology CompHaus) X.compHaus (Sieve.functorPushforward ExtrDisc.toCompHaus S)
Tactic:
change _ ∈ GrothendieckTopology.sieves _ _
State after:
case mp.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ Sieve.functorPushforward ExtrDisc.toCompHaus S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) X.compHaus

State before:
case mp.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ Sieve.functorPushforward ExtrDisc.toCompHaus S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) X.compHaus
Tactic:
apply (coherentTopology.Sieve_iff_hasEffectiveEpiFamily (Sieve.functorPushforward _ S)).mp
State after:
case mp.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), (Sieve.functorPushforward ExtrDisc.toCompHaus S).arrows (π a)

State before:
case mp.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), (Sieve.functorPushforward ExtrDisc.toCompHaus S).arrows (π a)
Tactic:
use α, inferInstance
State after:
case mp.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), (Sieve.functorPushforward ExtrDisc.toCompHaus S).arrows (π a)

State before:
case mp.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), (Sieve.functorPushforward ExtrDisc.toCompHaus S).arrows (π a)
Tactic:
use fun i => ExtrDisc.toCompHaus.obj (Y i)
State after:
case mp.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ ∃ π,
    EffectiveEpiFamily (fun i => ExtrDisc.toCompHaus.obj (Y i)) π ∧
      ∀ (a : α), (Sieve.functorPushforward ExtrDisc.toCompHaus S).arrows (π a)

State before:
case mp.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ ∃ π,
    EffectiveEpiFamily (fun i => ExtrDisc.toCompHaus.obj (Y i)) π ∧
      ∀ (a : α), (Sieve.functorPushforward ExtrDisc.toCompHaus S).arrows (π a)
Tactic:
use fun i => ExtrDisc.toCompHaus.map (π i)
State after:
case mp.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ (EffectiveEpiFamily (fun i => ExtrDisc.toCompHaus.obj (Y i)) fun i => ExtrDisc.toCompHaus.map (π i)) ∧
    ∀ (a : α), (Sieve.functorPushforward ExtrDisc.toCompHaus S).arrows ((fun i => ExtrDisc.toCompHaus.map (π i)) a)

State before:
case mp.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ (EffectiveEpiFamily (fun i => ExtrDisc.toCompHaus.obj (Y i)) fun i => ExtrDisc.toCompHaus.map (π i)) ∧
    ∀ (a : α), (Sieve.functorPushforward ExtrDisc.toCompHaus S).arrows ((fun i => ExtrDisc.toCompHaus.map (π i)) a)
Tactic:
constructor
State after:
case mp.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ EffectiveEpiFamily (fun i => ExtrDisc.toCompHaus.obj (Y i)) fun i => ExtrDisc.toCompHaus.map (π i)

case mp.intro.intro.intro.intro.intro.right
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ ∀ (a : α), (Sieve.functorPushforward ExtrDisc.toCompHaus S).arrows ((fun i => ExtrDisc.toCompHaus.map (π i)) a)

State before:
case mp.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ EffectiveEpiFamily (fun i => ExtrDisc.toCompHaus.obj (Y i)) fun i => ExtrDisc.toCompHaus.map (π i)
Tactic:
simp only [ExtrDisc.toCompHaus_obj, ExtrDisc.toCompHaus_map]
State after:
case mp.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ EffectiveEpiFamily (fun i => (Y i).compHaus) fun i => π i

State before:
case mp.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ EffectiveEpiFamily (fun i => (Y i).compHaus) fun i => π i
Tactic:
simp only [(ExtrDisc.effectiveEpiFamily_tfae _ _).out 0 2] at H₁
State after:
case mp.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₂ : ∀ (a : α), S.arrows (π a)
H₁ : ∀ (b : CoeSort.coe X), ∃ a x, ↑(π a) x = b
⊢ EffectiveEpiFamily (fun i => (Y i).compHaus) fun i => π i

State before:
case mp.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₂ : ∀ (a : α), S.arrows (π a)
H₁ : ∀ (b : CoeSort.coe X), ∃ a x, ↑(π a) x = b
⊢ EffectiveEpiFamily (fun i => (Y i).compHaus) fun i => π i
Tactic:
exact CompHaus.effectiveEpiFamily_of_jointly_surjective
    (fun i => (Y i).compHaus) (fun i => π i) H₁
State after:
no goals

State before:
case mp.intro.intro.intro.intro.intro.right
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → ExtrDisc
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ ∀ (a : α), (Sieve.functorPushforward ExtrDisc.toCompHaus S).arrows ((fun i => ExtrDisc.toCompHaus.map (π i)) a)
Tactic:
exact fun a => Sieve.image_mem_functorPushforward ExtrDisc.toCompHaus S (H₂ a)
State after:
no goals

State before:
case mpr
X : ExtrDisc
S : Sieve X
⊢ S ∈ GrothendieckTopology.sieves (CoverDense.inducedTopology coverDense) X →
    ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
intro hS
State after:
case mpr
X : ExtrDisc
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves (CoverDense.inducedTopology coverDense) X
⊢ ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr
X : ExtrDisc
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves (CoverDense.inducedTopology coverDense) X
⊢ ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
unfold CoverDense.inducedTopology at hS
State after:
case mpr
X : ExtrDisc
S : Sieve X
hS :
  S ∈
    GrothendieckTopology.sieves
      (LocallyCoverDense.inducedTopology (_ : LocallyCoverDense (coherentTopology CompHaus) ExtrDisc.toCompHaus)) X
⊢ ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr
X : ExtrDisc
S : Sieve X
hS :
  S ∈
    GrothendieckTopology.sieves
      (LocallyCoverDense.inducedTopology (_ : LocallyCoverDense (coherentTopology CompHaus) ExtrDisc.toCompHaus)) X
⊢ ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
unfold LocallyCoverDense.inducedTopology at hS
State after:
case mpr
X : ExtrDisc
S : Sieve X
hS :
  S ∈
    GrothendieckTopology.sieves
      {
        sieves := fun X S =>
          GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)
            (Sieve.functorPushforward ExtrDisc.toCompHaus S),
        top_mem' :=
          (_ :
            ∀ (X : ExtrDisc),
              GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)
                (Sieve.functorPushforward ExtrDisc.toCompHaus ⊤)),
        pullback_stable' :=
          (_ :
            ∀ (X Y : ExtrDisc) (S : Sieve X) (f : Y ⟶ X),
              S ∈
                  (fun X S =>
                      GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)
                        (Sieve.functorPushforward ExtrDisc.toCompHaus S))
                    X →
                Sieve.pullback f S ∈
                  (fun X S =>
                      GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)
                        (Sieve.functorPushforward ExtrDisc.toCompHaus S))
                    Y),
        transitive' :=
          (_ :
            ∀ (X : ExtrDisc) (S : Sieve X),
              S ∈
                  (fun X S =>
                      GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)
                        (Sieve.functorPushforward ExtrDisc.toCompHaus S))
                    X →
                ∀ (S' : Sieve X),
                  (∀ ⦃Y : ExtrDisc⦄ ⦃f : Y ⟶ X⦄,
                      S.arrows f →
                        Sieve.pullback f S' ∈
                          (fun X S =>
                              GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)
                                (Sieve.functorPushforward ExtrDisc.toCompHaus S))
                            Y) →
                    Sieve.functorPushforward ExtrDisc.toCompHaus S' ∈
                      GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)) }
      X
⊢ ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr
X : ExtrDisc
S : Sieve X
hS :
  S ∈
    GrothendieckTopology.sieves
      {
        sieves := fun X S =>
          GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)
            (Sieve.functorPushforward ExtrDisc.toCompHaus S),
        top_mem' :=
          (_ :
            ∀ (X : ExtrDisc),
              GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)
                (Sieve.functorPushforward ExtrDisc.toCompHaus ⊤)),
        pullback_stable' :=
          (_ :
            ∀ (X Y : ExtrDisc) (S : Sieve X) (f : Y ⟶ X),
              S ∈
                  (fun X S =>
                      GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)
                        (Sieve.functorPushforward ExtrDisc.toCompHaus S))
                    X →
                Sieve.pullback f S ∈
                  (fun X S =>
                      GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)
                        (Sieve.functorPushforward ExtrDisc.toCompHaus S))
                    Y),
        transitive' :=
          (_ :
            ∀ (X : ExtrDisc) (S : Sieve X),
              S ∈
                  (fun X S =>
                      GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)
                        (Sieve.functorPushforward ExtrDisc.toCompHaus S))
                    X →
                ∀ (S' : Sieve X),
                  (∀ ⦃Y : ExtrDisc⦄ ⦃f : Y ⟶ X⦄,
                      S.arrows f →
                        Sieve.pullback f S' ∈
                          (fun X S =>
                              GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)
                                (Sieve.functorPushforward ExtrDisc.toCompHaus S))
                            Y) →
                    Sieve.functorPushforward ExtrDisc.toCompHaus S' ∈
                      GrothendieckTopology.sieves (coherentTopology CompHaus) (ExtrDisc.toCompHaus.obj X)) }
      X
⊢ ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
simp only [ExtrDisc.toCompHaus_obj] at hS
State after:
case mpr
X : ExtrDisc
S : Sieve X
hS :
  S ∈ fun S =>
    GrothendieckTopology.sieves (coherentTopology CompHaus) X.compHaus (Sieve.functorPushforward ExtrDisc.toCompHaus S)
⊢ ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr
X : ExtrDisc
S : Sieve X
hS :
  S ∈ fun S =>
    GrothendieckTopology.sieves (coherentTopology CompHaus) X.compHaus (Sieve.functorPushforward ExtrDisc.toCompHaus S)
⊢ ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
change _ ∈ GrothendieckTopology.sieves _ _ at hS
State after:
case mpr
X : ExtrDisc
S : Sieve X
hS : Sieve.functorPushforward ExtrDisc.toCompHaus S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) X.compHaus
⊢ ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr
X : ExtrDisc
S : Sieve X
hS : Sieve.functorPushforward ExtrDisc.toCompHaus S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) X.compHaus
⊢ ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
replace hS := (coherentTopology.Sieve_iff_hasEffectiveEpiFamily _).mpr hS
State after:
case mpr
X : ExtrDisc
S : Sieve X
hS : ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), (Sieve.functorPushforward ExtrDisc.toCompHaus S).arrows (π a)
⊢ ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr
X : ExtrDisc
S : Sieve X
hS : ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), (Sieve.functorPushforward ExtrDisc.toCompHaus S).arrows (π a)
⊢ ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rcases hS with ⟨α, _, Y, π, ⟨H₁, H₂⟩⟩
State after:
case mpr.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward ExtrDisc.toCompHaus S).arrows (π a)
⊢ ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward ExtrDisc.toCompHaus S).arrows (π a)
⊢ ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
use α, inferInstance
State after:
case mpr.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward ExtrDisc.toCompHaus S).arrows (π a)
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward ExtrDisc.toCompHaus S).arrows (π a)
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
change ∀ a, ∃ (Y₀: ExtrDisc) (π₀ : Y₀⟶ X) (f₀: Y a ⟶ Y₀.compHaus), S.arrows π₀ ∧
    π a = f₀ ≫ ExtrDisc.toCompHaus.map π₀  at H₂
State after:
case mpr.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), ∃ Y₀ π₀ f₀, S.arrows π₀ ∧ π a = f₀ ≫ ExtrDisc.toCompHaus.map π₀
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), ∃ Y₀ π₀ f₀, S.arrows π₀ ∧ π a = f₀ ≫ ExtrDisc.toCompHaus.map π₀
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rw [Classical.skolem] at H₂
State after:
case mpr.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∃ f, ∀ (x : α), ∃ π₀ f₀, S.arrows π₀ ∧ π x = f₀ ≫ ExtrDisc.toCompHaus.map π₀
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∃ f, ∀ (x : α), ∃ π₀ f₀, S.arrows π₀ ∧ π x = f₀ ≫ ExtrDisc.toCompHaus.map π₀
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rcases H₂ with ⟨Y₀, H₂⟩
State after:
case mpr.intro.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
H₂ : ∀ (x : α), ∃ π₀ f₀, S.arrows π₀ ∧ π x = f₀ ≫ ExtrDisc.toCompHaus.map π₀
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr.intro.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
H₂ : ∀ (x : α), ∃ π₀ f₀, S.arrows π₀ ∧ π x = f₀ ≫ ExtrDisc.toCompHaus.map π₀
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rw [Classical.skolem] at H₂
State after:
case mpr.intro.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
H₂ : ∃ f, ∀ (x : α), ∃ f₀, S.arrows (f x) ∧ π x = f₀ ≫ ExtrDisc.toCompHaus.map (f x)
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr.intro.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
H₂ : ∃ f, ∀ (x : α), ∃ f₀, S.arrows (f x) ∧ π x = f₀ ≫ ExtrDisc.toCompHaus.map (f x)
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rcases H₂ with ⟨π₀, H₂⟩
State after:
case mpr.intro.intro.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
H₂ : ∀ (x : α), ∃ f₀, S.arrows (π₀ x) ∧ π x = f₀ ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr.intro.intro.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
H₂ : ∀ (x : α), ∃ f₀, S.arrows (π₀ x) ∧ π x = f₀ ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rw [Classical.skolem] at H₂
State after:
case mpr.intro.intro.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
H₂ : ∃ f, ∀ (x : α), S.arrows (π₀ x) ∧ π x = f x ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr.intro.intro.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
H₂ : ∃ f, ∀ (x : α), S.arrows (π₀ x) ∧ π x = f x ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rcases H₂ with ⟨f₀, H₂⟩
State after:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

State before:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
use Y₀ , π₀
State after:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ EffectiveEpiFamily Y₀ π₀ ∧ ∀ (a : α), S.arrows (π₀ a)

State before:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ EffectiveEpiFamily Y₀ π₀ ∧ ∀ (a : α), S.arrows (π₀ a)
Tactic:
constructor
State after:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ EffectiveEpiFamily Y₀ π₀

case mpr.intro.intro.intro.intro.intro.intro.intro.intro.right
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ ∀ (a : α), S.arrows (π₀ a)

State before:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ EffectiveEpiFamily Y₀ π₀
Tactic:
simp only [(ExtrDisc.effectiveEpiFamily_tfae _ _).out 0 2]
State after:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ ∀ (b : CoeSort.coe X), ∃ a x, ↑(π₀ a) x = b

State before:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ ∀ (b : CoeSort.coe X), ∃ a x, ↑(π₀ a) x = b
Tactic:
simp only [(CompHaus.effectiveEpiFamily_tfae _ _).out 0 2] at H₁
State after:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
H₁ : ∀ (b : ↑(ExtrDisc.toCompHaus.obj X).toTop), ∃ a x, ↑(π a) x = b
⊢ ∀ (b : CoeSort.coe X), ∃ a x, ↑(π₀ a) x = b

State before:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
H₁ : ∀ (b : ↑(ExtrDisc.toCompHaus.obj X).toTop), ∃ a x, ↑(π a) x = b
⊢ ∀ (b : CoeSort.coe X), ∃ a x, ↑(π₀ a) x = b
Tactic:
intro b
State after:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
H₁ : ∀ (b : ↑(ExtrDisc.toCompHaus.obj X).toTop), ∃ a x, ↑(π a) x = b
b : CoeSort.coe X
⊢ ∃ a x, ↑(π₀ a) x = b

State before:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
H₁ : ∀ (b : ↑(ExtrDisc.toCompHaus.obj X).toTop), ∃ a x, ↑(π a) x = b
b : CoeSort.coe X
⊢ ∃ a x, ↑(π₀ a) x = b
Tactic:
replace H₁ := H₁ b
State after:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
b : CoeSort.coe X
H₁ : ∃ a x, ↑(π a) x = b
⊢ ∃ a x, ↑(π₀ a) x = b

State before:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
b : CoeSort.coe X
H₁ : ∃ a x, ↑(π a) x = b
⊢ ∃ a x, ↑(π₀ a) x = b
Tactic:
rcases H₁ with ⟨i, x, H₁⟩
State after:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
b : CoeSort.coe X
i : α
x : ↑(Y i).toTop
H₁ : ↑(π i) x = b
⊢ ∃ a x, ↑(π₀ a) x = b

State before:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
b : CoeSort.coe X
i : α
x : ↑(Y i).toTop
H₁ : ↑(π i) x = b
⊢ ∃ a x, ↑(π₀ a) x = b
Tactic:
use i, f₀ i x
State after:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
b : CoeSort.coe X
i : α
x : ↑(Y i).toTop
H₁ : ↑(π i) x = b
⊢ ↑(π₀ i) (↑(f₀ i) x) = b

State before:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
b : CoeSort.coe X
i : α
x : ↑(Y i).toTop
H₁ : ↑(π i) x = b
⊢ ↑(π₀ i) (↑(f₀ i) x) = b
Tactic:
aesop_cat
State after:
no goals

State before:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.right
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ ∀ (a : α), S.arrows (π₀ a)
Tactic:
intro i
State after:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.right
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
i : α
⊢ S.arrows (π₀ i)

State before:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.right
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
i : α
⊢ S.arrows (π₀ i)
Tactic:
exact (H₂ i).1
State after:
no goals