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

State before:
⊢ CoverDense (coherentTopology CompHaus) ExtrDisc.toCompHaus
Tactic:
constructor
State after:
case is_cover

⊢ ∀ (U : CompHaus), Sieve.coverByImage ExtrDisc.toCompHaus U ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) U

State before:
case is_cover

⊢ ∀ (U : CompHaus), Sieve.coverByImage ExtrDisc.toCompHaus U ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) U
Tactic:
intro B
State after:
case is_cover
B : CompHaus
⊢ Sieve.coverByImage ExtrDisc.toCompHaus B ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B

State before:
case is_cover
B : CompHaus
⊢ Sieve.coverByImage ExtrDisc.toCompHaus B ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Tactic:
let T := Presieve.singleton B.presentationπ
State after:
case is_cover
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
⊢ Sieve.coverByImage ExtrDisc.toCompHaus B ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B

State before:
case is_cover
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
⊢ Sieve.coverByImage ExtrDisc.toCompHaus B ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Tactic:
let S := Sieve.generate T
State after:
case is_cover
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
⊢ Sieve.coverByImage ExtrDisc.toCompHaus B ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B

State before:
case is_cover
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
⊢ Sieve.coverByImage ExtrDisc.toCompHaus B ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Tactic:
convert hS
State after:
case h.e'_4
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
⊢ Sieve.coverByImage ExtrDisc.toCompHaus B = S

State before:
case h.e'_4
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
⊢ Sieve.coverByImage ExtrDisc.toCompHaus B = S
Tactic:
ext Y f
State after:
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

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
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

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
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

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 ∃ _, _
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 π

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π, ?_ , ?_⟩
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

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
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

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
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

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
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

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 ⟨⟩
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)

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 ⟨()⟩
State after:
no goals

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 ⟨⟩
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)

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
State after:
no goals

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π)
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

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
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

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
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

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 ⟨(), ?_⟩
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

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
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

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
State after:
no goals

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π]
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)

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
State after:
no goals

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⟩⟩
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

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
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

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π
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

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 ,?_⟩
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

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]
  } ⟩
  ⟩
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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, ⟨_⟩⟩
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)

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
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)

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
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)

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 }
State after:
no goals