internlm/Lean-Github huggingface dataset:
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case h.e'_4.h
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Y : CompHaus
f : Y ⟶ B
⊢ (Sieve.coverByImage ExtrDisc.toCompHaus B).arrows f ↔ S.arrows f
Tactic:
constructor
Proof state after:
case h.e'_4.h.mp
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Y : CompHaus
f : Y ⟶ B
⊢ (Sieve.coverByImage ExtrDisc.toCompHaus B).arrows f → S.arrows f

case h.e'_4.h.mpr
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Y : CompHaus
f : Y ⟶ B
⊢ S.arrows f → (Sieve.coverByImage ExtrDisc.toCompHaus B).arrows f
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Tactic:
apply Coverage.saturate.of
Proof state after:
case hS
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
⊢ T ∈ Coverage.covering (coherentCoverage CompHaus) B
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case hS
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
⊢ T ∈ Coverage.covering (coherentCoverage CompHaus) B
Tactic:
change ∃ _, _
Proof state after:
case hS
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
⊢ ∃ x x_1 X π, T = Presieve.ofArrows X π ∧ EffectiveEpiFamily X π
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case hS
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
⊢ ∃ x x_1 X π, T = Presieve.ofArrows X π ∧ EffectiveEpiFamily X π
Tactic:
refine ⟨Unit, inferInstance,
  fun _ => B.presentation.compHaus, fun _ => B.presentationπ, ?_ , ?_⟩
Proof state after:
case hS.refine_1
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
⊢ T = Presieve.ofArrows (fun x => (CompHaus.presentation B).compHaus) fun x => CompHaus.presentationπ B

case hS.refine_2
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
⊢ EffectiveEpiFamily (fun x => (CompHaus.presentation B).compHaus) fun x => CompHaus.presentationπ B
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case hS.refine_1
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
⊢ T = Presieve.ofArrows (fun x => (CompHaus.presentation B).compHaus) fun x => CompHaus.presentationπ B
Tactic:
funext X f
Proof state after:
case hS.refine_1.h.h
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
X : CompHaus
f : X ⟶ B
⊢ T f = Presieve.ofArrows (fun x => (CompHaus.presentation B).compHaus) (fun x => CompHaus.presentationπ B) f
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case hS.refine_1.h.h
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
X : CompHaus
f : X ⟶ B
⊢ T f = Presieve.ofArrows (fun x => (CompHaus.presentation B).compHaus) (fun x => CompHaus.presentationπ B) f
Tactic:
ext
Proof state after:
case hS.refine_1.h.h.a
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
X : CompHaus
f : X ⟶ B
⊢ T f ↔ Presieve.ofArrows (fun x => (CompHaus.presentation B).compHaus) (fun x => CompHaus.presentationπ B) f
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case hS.refine_1.h.h.a
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
X : CompHaus
f : X ⟶ B
⊢ T f ↔ Presieve.ofArrows (fun x => (CompHaus.presentation B).compHaus) (fun x => CompHaus.presentationπ B) f
Tactic:
constructor
Proof state after:
case hS.refine_1.h.h.a.mp
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
X : CompHaus
f : X ⟶ B
⊢ T f → Presieve.ofArrows (fun x => (CompHaus.presentation B).compHaus) (fun x => CompHaus.presentationπ B) f

case hS.refine_1.h.h.a.mpr
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
X : CompHaus
f : X ⟶ B
⊢ Presieve.ofArrows (fun x => (CompHaus.presentation B).compHaus) (fun x => CompHaus.presentationπ B) f → T f
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case hS.refine_1.h.h.a.mp
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
X : CompHaus
f : X ⟶ B
⊢ T f → Presieve.ofArrows (fun x => (CompHaus.presentation B).compHaus) (fun x => CompHaus.presentationπ B) f
Tactic:
rintro ⟨⟩
Proof state after:
case hS.refine_1.h.h.a.mp.mk
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
Y : CompHaus
⊢ Presieve.ofArrows (fun x => (CompHaus.presentation B).compHaus) (fun x => CompHaus.presentationπ B)
    (CompHaus.presentationπ B)
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case hS.refine_1.h.h.a.mp.mk
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
Y : CompHaus
⊢ Presieve.ofArrows (fun x => (CompHaus.presentation B).compHaus) (fun x => CompHaus.presentationπ B)
    (CompHaus.presentationπ B)
Tactic:
refine ⟨()⟩
Proof state after:
no goals
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case hS.refine_1.h.h.a.mpr
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
X : CompHaus
f : X ⟶ B
⊢ Presieve.ofArrows (fun x => (CompHaus.presentation B).compHaus) (fun x => CompHaus.presentationπ B) f → T f
Tactic:
rintro ⟨⟩
Proof state after:
case hS.refine_1.h.h.a.mpr.mk
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
Y : CompHaus
i✝ : Unit
⊢ T (CompHaus.presentationπ B)
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case hS.refine_1.h.h.a.mpr.mk
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
Y : CompHaus
i✝ : Unit
⊢ T (CompHaus.presentationπ B)
Tactic:
simp
Proof state after:
no goals
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case hS.refine_2
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
⊢ EffectiveEpiFamily (fun x => (CompHaus.presentation B).compHaus) fun x => CompHaus.presentationπ B
Tactic:
have := CompHaus.effectiveEpiFamily_tfae
  (fun (_ : Unit) => B.presentation.compHaus)
  (fun (_ : Unit) => B.presentationπ)
Proof state after:
case hS.refine_2
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
this :
  List.TFAE
    [EffectiveEpiFamily (fun x => (CompHaus.presentation B).compHaus) fun x => CompHaus.presentationπ B,
      Epi (Sigma.desc fun x => CompHaus.presentationπ B), ∀ (b : ↑B.toTop), ∃ a x, ↑(CompHaus.presentationπ B) x = b]
⊢ EffectiveEpiFamily (fun x => (CompHaus.presentation B).compHaus) fun x => CompHaus.presentationπ B
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case hS.refine_2
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
this :
  List.TFAE
    [EffectiveEpiFamily (fun x => (CompHaus.presentation B).compHaus) fun x => CompHaus.presentationπ B,
      Epi (Sigma.desc fun x => CompHaus.presentationπ B), ∀ (b : ↑B.toTop), ∃ a x, ↑(CompHaus.presentationπ B) x = b]
⊢ EffectiveEpiFamily (fun x => (CompHaus.presentation B).compHaus) fun x => CompHaus.presentationπ B
Tactic:
apply (this.out 0 2).mpr
Proof state after:
case hS.refine_2
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
this :
  List.TFAE
    [EffectiveEpiFamily (fun x => (CompHaus.presentation B).compHaus) fun x => CompHaus.presentationπ B,
      Epi (Sigma.desc fun x => CompHaus.presentationπ B), ∀ (b : ↑B.toTop), ∃ a x, ↑(CompHaus.presentationπ B) x = b]
⊢ ∀ (b : ↑B.toTop), ∃ a x, ↑(CompHaus.presentationπ B) x = b
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case hS.refine_2
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
this :
  List.TFAE
    [EffectiveEpiFamily (fun x => (CompHaus.presentation B).compHaus) fun x => CompHaus.presentationπ B,
      Epi (Sigma.desc fun x => CompHaus.presentationπ B), ∀ (b : ↑B.toTop), ∃ a x, ↑(CompHaus.presentationπ B) x = b]
⊢ ∀ (b : ↑B.toTop), ∃ a x, ↑(CompHaus.presentationπ B) x = b
Tactic:
intro b
Proof state after:
case hS.refine_2
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
this :
  List.TFAE
    [EffectiveEpiFamily (fun x => (CompHaus.presentation B).compHaus) fun x => CompHaus.presentationπ B,
      Epi (Sigma.desc fun x => CompHaus.presentationπ B), ∀ (b : ↑B.toTop), ∃ a x, ↑(CompHaus.presentationπ B) x = b]
b : ↑B.toTop
⊢ ∃ a x, ↑(CompHaus.presentationπ B) x = b
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case hS.refine_2
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
this :
  List.TFAE
    [EffectiveEpiFamily (fun x => (CompHaus.presentation B).compHaus) fun x => CompHaus.presentationπ B,
      Epi (Sigma.desc fun x => CompHaus.presentationπ B), ∀ (b : ↑B.toTop), ∃ a x, ↑(CompHaus.presentationπ B) x = b]
b : ↑B.toTop
⊢ ∃ a x, ↑(CompHaus.presentationπ B) x = b
Tactic:
refine ⟨(), ?_⟩
Proof state after:
case hS.refine_2
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
this :
  List.TFAE
    [EffectiveEpiFamily (fun x => (CompHaus.presentation B).compHaus) fun x => CompHaus.presentationπ B,
      Epi (Sigma.desc fun x => CompHaus.presentationπ B), ∀ (b : ↑B.toTop), ∃ a x, ↑(CompHaus.presentationπ B) x = b]
b : ↑B.toTop
⊢ ∃ x, ↑(CompHaus.presentationπ B) x = b
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case hS.refine_2
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
this :
  List.TFAE
    [EffectiveEpiFamily (fun x => (CompHaus.presentation B).compHaus) fun x => CompHaus.presentationπ B,
      Epi (Sigma.desc fun x => CompHaus.presentationπ B), ∀ (b : ↑B.toTop), ∃ a x, ↑(CompHaus.presentationπ B) x = b]
b : ↑B.toTop
⊢ ∃ x, ↑(CompHaus.presentationπ B) x = b
Tactic:
have hπ :
  Function.Surjective B.presentationπ := by
    rw [← CompHaus.epi_iff_surjective B.presentationπ]
    exact CompHaus.epiPresentπ B
Proof state after:
case hS.refine_2
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
this :
  List.TFAE
    [EffectiveEpiFamily (fun x => (CompHaus.presentation B).compHaus) fun x => CompHaus.presentationπ B,
      Epi (Sigma.desc fun x => CompHaus.presentationπ B), ∀ (b : ↑B.toTop), ∃ a x, ↑(CompHaus.presentationπ B) x = b]
b : ↑B.toTop
hπ : Function.Surjective ↑(CompHaus.presentationπ B)
⊢ ∃ x, ↑(CompHaus.presentationπ B) x = b
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case hS.refine_2
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
this :
  List.TFAE
    [EffectiveEpiFamily (fun x => (CompHaus.presentation B).compHaus) fun x => CompHaus.presentationπ B,
      Epi (Sigma.desc fun x => CompHaus.presentationπ B), ∀ (b : ↑B.toTop), ∃ a x, ↑(CompHaus.presentationπ B) x = b]
b : ↑B.toTop
hπ : Function.Surjective ↑(CompHaus.presentationπ B)
⊢ ∃ x, ↑(CompHaus.presentationπ B) x = b
Tactic:
exact hπ b
Proof state after:
no goals
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
this :
  List.TFAE
    [EffectiveEpiFamily (fun x => (CompHaus.presentation B).compHaus) fun x => CompHaus.presentationπ B,
      Epi (Sigma.desc fun x => CompHaus.presentationπ B), ∀ (b : ↑B.toTop), ∃ a x, ↑(CompHaus.presentationπ B) x = b]
b : ↑B.toTop
⊢ Function.Surjective ↑(CompHaus.presentationπ B)
Tactic:
rw [← CompHaus.epi_iff_surjective B.presentationπ]
Proof state after:
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
this :
  List.TFAE
    [EffectiveEpiFamily (fun x => (CompHaus.presentation B).compHaus) fun x => CompHaus.presentationπ B,
      Epi (Sigma.desc fun x => CompHaus.presentationπ B), ∀ (b : ↑B.toTop), ∃ a x, ↑(CompHaus.presentationπ B) x = b]
b : ↑B.toTop
⊢ Epi (CompHaus.presentationπ B)
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
this :
  List.TFAE
    [EffectiveEpiFamily (fun x => (CompHaus.presentation B).compHaus) fun x => CompHaus.presentationπ B,
      Epi (Sigma.desc fun x => CompHaus.presentationπ B), ∀ (b : ↑B.toTop), ∃ a x, ↑(CompHaus.presentationπ B) x = b]
b : ↑B.toTop
⊢ Epi (CompHaus.presentationπ B)
Tactic:
exact CompHaus.epiPresentπ B
Proof state after:
no goals
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case h.e'_4.h.mp
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Y : CompHaus
f : Y ⟶ B
⊢ (Sieve.coverByImage ExtrDisc.toCompHaus B).arrows f → S.arrows f
Tactic:
rintro ⟨⟨obj, lift, map, fact⟩⟩
Proof state after:
case h.e'_4.h.mp.intro.mk
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Y : CompHaus
f : Y ⟶ B
obj : ExtrDisc
lift : Y ⟶ ExtrDisc.toCompHaus.obj obj
map : ExtrDisc.toCompHaus.obj obj ⟶ B
fact : lift ≫ map = f
⊢ S.arrows f
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case h.e'_4.h.mp.intro.mk
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Y : CompHaus
f : Y ⟶ B
obj : ExtrDisc
lift : Y ⟶ ExtrDisc.toCompHaus.obj obj
map : ExtrDisc.toCompHaus.obj obj ⟶ B
fact : lift ≫ map = f
⊢ S.arrows f
Tactic:
obtain ⟨obj_factors⟩ : Projective obj.compHaus := by
  infer_instance
Proof state after:
case h.e'_4.h.mp.intro.mk.mk
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Y : CompHaus
f : Y ⟶ B
obj : ExtrDisc
lift : Y ⟶ ExtrDisc.toCompHaus.obj obj
map : ExtrDisc.toCompHaus.obj obj ⟶ B
fact : lift ≫ map = f
obj_factors : ∀ {E X : CompHaus} (f : obj.compHaus ⟶ X) (e : E ⟶ X) [inst : Epi e], ∃ f', f' ≫ e = f
⊢ S.arrows f
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case h.e'_4.h.mp.intro.mk.mk
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Y : CompHaus
f : Y ⟶ B
obj : ExtrDisc
lift : Y ⟶ ExtrDisc.toCompHaus.obj obj
map : ExtrDisc.toCompHaus.obj obj ⟶ B
fact : lift ≫ map = f
obj_factors : ∀ {E X : CompHaus} (f : obj.compHaus ⟶ X) (e : E ⟶ X) [inst : Epi e], ∃ f', f' ≫ e = f
⊢ S.arrows f
Tactic:
obtain ⟨p, p_factors⟩ := obj_factors map B.presentationπ
Proof state after:
case h.e'_4.h.mp.intro.mk.mk.intro
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Y : CompHaus
f : Y ⟶ B
obj : ExtrDisc
lift : Y ⟶ ExtrDisc.toCompHaus.obj obj
map : ExtrDisc.toCompHaus.obj obj ⟶ B
fact : lift ≫ map = f
obj_factors : ∀ {E X : CompHaus} (f : obj.compHaus ⟶ X) (e : E ⟶ X) [inst : Epi e], ∃ f', f' ≫ e = f
p : obj.compHaus ⟶ (CompHaus.presentation B).compHaus
p_factors : p ≫ CompHaus.presentationπ B = map
⊢ S.arrows f
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case h.e'_4.h.mp.intro.mk.mk.intro
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Y : CompHaus
f : Y ⟶ B
obj : ExtrDisc
lift : Y ⟶ ExtrDisc.toCompHaus.obj obj
map : ExtrDisc.toCompHaus.obj obj ⟶ B
fact : lift ≫ map = f
obj_factors : ∀ {E X : CompHaus} (f : obj.compHaus ⟶ X) (e : E ⟶ X) [inst : Epi e], ∃ f', f' ≫ e = f
p : obj.compHaus ⟶ (CompHaus.presentation B).compHaus
p_factors : p ≫ CompHaus.presentationπ B = map
⊢ S.arrows f
Tactic:
refine ⟨(CompHaus.presentation B).compHaus ,?_⟩
Proof state after:
case h.e'_4.h.mp.intro.mk.mk.intro
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Y : CompHaus
f : Y ⟶ B
obj : ExtrDisc
lift : Y ⟶ ExtrDisc.toCompHaus.obj obj
map : ExtrDisc.toCompHaus.obj obj ⟶ B
fact : lift ≫ map = f
obj_factors : ∀ {E X : CompHaus} (f : obj.compHaus ⟶ X) (e : E ⟶ X) [inst : Epi e], ∃ f', f' ≫ e = f
p : obj.compHaus ⟶ (CompHaus.presentation B).compHaus
p_factors : p ≫ CompHaus.presentationπ B = map
⊢ ∃ h g, T g ∧ h ≫ g = f
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case h.e'_4.h.mp.intro.mk.mk.intro
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Y : CompHaus
f : Y ⟶ B
obj : ExtrDisc
lift : Y ⟶ ExtrDisc.toCompHaus.obj obj
map : ExtrDisc.toCompHaus.obj obj ⟶ B
fact : lift ≫ map = f
obj_factors : ∀ {E X : CompHaus} (f : obj.compHaus ⟶ X) (e : E ⟶ X) [inst : Epi e], ∃ f', f' ≫ e = f
p : obj.compHaus ⟶ (CompHaus.presentation B).compHaus
p_factors : p ≫ CompHaus.presentationπ B = map
⊢ ∃ h g, T g ∧ h ≫ g = f
Tactic:
refine ⟨lift ≫ p, ⟨ B.presentationπ
    , {
    left := Presieve.singleton.mk
    right := by
      rw [Category.assoc, p_factors, fact]
  } ⟩
  ⟩
Proof state after:
no goals
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Y : CompHaus
f : Y ⟶ B
obj : ExtrDisc
lift : Y ⟶ ExtrDisc.toCompHaus.obj obj
map : ExtrDisc.toCompHaus.obj obj ⟶ B
fact : lift ≫ map = f
⊢ Projective obj.compHaus
Tactic:
infer_instance
Proof state after:
no goals
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Y : CompHaus
f : Y ⟶ B
obj : ExtrDisc
lift : Y ⟶ ExtrDisc.toCompHaus.obj obj
map : ExtrDisc.toCompHaus.obj obj ⟶ B
fact : lift ≫ map = f
obj_factors : ∀ {E X : CompHaus} (f : obj.compHaus ⟶ X) (e : E ⟶ X) [inst : Epi e], ∃ f', f' ≫ e = f
p : obj.compHaus ⟶ (CompHaus.presentation B).compHaus
p_factors : p ≫ CompHaus.presentationπ B = map
⊢ (lift ≫ p) ≫ CompHaus.presentationπ B = f
Tactic:
rw [Category.assoc, p_factors, fact]
Proof state after:
no goals
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case h.e'_4.h.mpr
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Y : CompHaus
f : Y ⟶ B
⊢ S.arrows f → (Sieve.coverByImage ExtrDisc.toCompHaus B).arrows f
Tactic:
rintro ⟨Z, h, g, hypo1, ⟨_⟩⟩
Proof state after:
case h.e'_4.h.mpr.intro.intro.intro.intro.refl
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Y Z : CompHaus
h : Y ⟶ Z
g : Z ⟶ B
hypo1 : T g
⊢ (Sieve.coverByImage ExtrDisc.toCompHaus B).arrows (h ≫ g)
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case h.e'_4.h.mpr.intro.intro.intro.intro.refl
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Y Z : CompHaus
h : Y ⟶ Z
g : Z ⟶ B
hypo1 : T g
⊢ (Sieve.coverByImage ExtrDisc.toCompHaus B).arrows (h ≫ g)
Tactic:
cases hypo1
Proof state after:
case h.e'_4.h.mpr.intro.intro.intro.intro.refl.mk
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Y : CompHaus
h : Y ⟶ (CompHaus.presentation B).compHaus
⊢ (Sieve.coverByImage ExtrDisc.toCompHaus B).arrows (h ≫ CompHaus.presentationπ B)
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case h.e'_4.h.mpr.intro.intro.intro.intro.refl.mk
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Y : CompHaus
h : Y ⟶ (CompHaus.presentation B).compHaus
⊢ (Sieve.coverByImage ExtrDisc.toCompHaus B).arrows (h ≫ CompHaus.presentationπ B)
Tactic:
constructor
Proof state after:
case h.e'_4.h.mpr.intro.intro.intro.intro.refl.mk.val
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Y : CompHaus
h : Y ⟶ (CompHaus.presentation B).compHaus
⊢ Presieve.CoverByImageStructure ExtrDisc.toCompHaus (h ≫ CompHaus.presentationπ B)
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case h.e'_4.h.mpr.intro.intro.intro.intro.refl.mk.val
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Y : CompHaus
h : Y ⟶ (CompHaus.presentation B).compHaus
⊢ Presieve.CoverByImageStructure ExtrDisc.toCompHaus (h ≫ CompHaus.presentationπ B)
Tactic:
refine
{ obj := CompHaus.presentation B
  lift := h
  map := CompHaus.presentationπ B
  fac := rfl }
Proof state after:
no goals
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof state before:
X : ExtrDisc
S : Sieve X
⊢ (∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) ↔
    S ∈ GrothendieckTopology.sieves (CoverDense.inducedTopology coverDense) X
Tactic:
constructor
Proof 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)
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof 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₂⟩⟩
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 (CoverDense.inducedTopology coverDense) X