internlm/Lean-Github huggingface dataset:
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof 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
Proof 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
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof 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
Proof 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
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof 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]
Proof 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)
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof 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 _ _
Proof 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
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof 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
Proof 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)
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof 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
Proof 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)
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof 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)
Proof 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)
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof 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)
Proof 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)
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof 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
Proof 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)
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof 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]
Proof 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
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof 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₁
Proof 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
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof 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₁
Proof state after:
no goals
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof 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)
Proof state after:
no goals
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof 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
Proof 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)
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof 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
Proof 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)
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof 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
Proof 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)
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof 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
Proof 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)
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof 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
Proof 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)
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof 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
Proof 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)
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof 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₂⟩⟩
Proof 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)
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof 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
Proof 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)
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof 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₂
Proof 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)