[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
⊢ _root_.Equivalence fun a b => ∃ Z z fst snd, fst ≫ π a.fst = snd ≫ π b.fst ∧ ↑fst z = a.snd ∧ ↑snd z = b.snd
[PROOFSTEP]
constructor
[GOAL]
case refl
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
⊢ ∀ (x : ↑(finiteCoproduct X).toTop), ∃ Z z fst snd, fst ≫ π x.fst = snd ≫ π x.fst ∧ ↑fst z = x.snd ∧ ↑snd z = x.snd
[PROOFSTEP]
rintro ⟨a, x⟩
[GOAL]
case refl.mk
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
x : ↑(X a).toTop
⊢ ∃ Z z fst snd,
    fst ≫ π { fst := a, snd := x }.fst = snd ≫ π { fst := a, snd := x }.fst ∧
      ↑fst z = { fst := a, snd := x }.snd ∧ ↑snd z = { fst := a, snd := x }.snd
[PROOFSTEP]
refine ⟨X a, x, 𝟙 _, 𝟙 _, by simp, rfl, rfl⟩
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
x : ↑(X a).toTop
⊢ 𝟙 (X a) ≫ π { fst := a, snd := x }.fst = 𝟙 (X a) ≫ π { fst := a, snd := x }.fst
[PROOFSTEP]
simp
[GOAL]
case symm
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
⊢ ∀ {x y : ↑(finiteCoproduct X).toTop},
    (∃ Z z fst snd, fst ≫ π x.fst = snd ≫ π y.fst ∧ ↑fst z = x.snd ∧ ↑snd z = y.snd) →
      ∃ Z z fst snd, fst ≫ π y.fst = snd ≫ π x.fst ∧ ↑fst z = y.snd ∧ ↑snd z = x.snd
[PROOFSTEP]
rintro ⟨a, x⟩ ⟨b, y⟩ ⟨Z, z, fst, snd, w, h1, h2⟩
[GOAL]
case symm.mk.mk.intro.intro.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
x : ↑(X a).toTop
b : α
y : ↑(X b).toTop
Z : CompHaus
z : ↑Z.toTop
fst : Z ⟶ X { fst := a, snd := x }.fst
snd : Z ⟶ X { fst := b, snd := y }.fst
w : fst ≫ π { fst := a, snd := x }.fst = snd ≫ π { fst := b, snd := y }.fst
h1 : ↑fst z = { fst := a, snd := x }.snd
h2 : ↑snd z = { fst := b, snd := y }.snd
⊢ ∃ Z z fst snd,
    fst ≫ π { fst := b, snd := y }.fst = snd ≫ π { fst := a, snd := x }.fst ∧
      ↑fst z = { fst := b, snd := y }.snd ∧ ↑snd z = { fst := a, snd := x }.snd
[PROOFSTEP]
exact ⟨Z, z, snd, fst, w.symm, h2, h1⟩
[GOAL]
case trans
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
⊢ ∀ {x y z : ↑(finiteCoproduct X).toTop},
    (∃ Z z fst snd, fst ≫ π x.fst = snd ≫ π y.fst ∧ ↑fst z = x.snd ∧ ↑snd z = y.snd) →
      (∃ Z z_1 fst snd, fst ≫ π y.fst = snd ≫ π z.fst ∧ ↑fst z_1 = y.snd ∧ ↑snd z_1 = z.snd) →
        ∃ Z z_1 fst snd, fst ≫ π x.fst = snd ≫ π z.fst ∧ ↑fst z_1 = x.snd ∧ ↑snd z_1 = z.snd
[PROOFSTEP]
rintro ⟨a, x⟩ ⟨b, y⟩ ⟨z, c⟩ ⟨Z, z, fstZ, sndZ, hZ, hZ1, hZ2⟩ ⟨W, w, fstW, sndW, hW, hW1, hW2⟩
[GOAL]
case trans.mk.mk.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
x : ↑(X a).toTop
b : α
y : ↑(X b).toTop
z✝ : α
c : ↑(X z✝).toTop
Z : CompHaus
z : ↑Z.toTop
fstZ : Z ⟶ X { fst := a, snd := x }.fst
sndZ : Z ⟶ X { fst := b, snd := y }.fst
hZ : fstZ ≫ π { fst := a, snd := x }.fst = sndZ ≫ π { fst := b, snd := y }.fst
hZ1 : ↑fstZ z = { fst := a, snd := x }.snd
hZ2 : ↑sndZ z = { fst := b, snd := y }.snd
W : CompHaus
w : ↑W.toTop
fstW : W ⟶ X { fst := b, snd := y }.fst
sndW : W ⟶ X { fst := z✝, snd := c }.fst
hW : fstW ≫ π { fst := b, snd := y }.fst = sndW ≫ π { fst := z✝, snd := c }.fst
hW1 : ↑fstW w = { fst := b, snd := y }.snd
hW2 : ↑sndW w = { fst := z✝, snd := c }.snd
⊢ ∃ Z z fst snd,
    fst ≫ π { fst := a, snd := x }.fst = snd ≫ π { fst := z✝, snd := c }.fst ∧
      ↑fst z = { fst := a, snd := x }.snd ∧ ↑snd z = { fst := z✝, snd := c }.snd
[PROOFSTEP]
refine
  ⟨pullback sndZ fstW, ⟨⟨z, w⟩, by dsimp; rw [hZ2, hW1]⟩, pullback.fst _ _ ≫ fstZ, pullback.snd _ _ ≫ sndW, ?_, hZ1,
    hW2⟩
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
x : ↑(X a).toTop
b : α
y : ↑(X b).toTop
z✝ : α
c : ↑(X z✝).toTop
Z : CompHaus
z : ↑Z.toTop
fstZ : Z ⟶ X { fst := a, snd := x }.fst
sndZ : Z ⟶ X { fst := b, snd := y }.fst
hZ : fstZ ≫ π { fst := a, snd := x }.fst = sndZ ≫ π { fst := b, snd := y }.fst
hZ1 : ↑fstZ z = { fst := a, snd := x }.snd
hZ2 : ↑sndZ z = { fst := b, snd := y }.snd
W : CompHaus
w : ↑W.toTop
fstW : W ⟶ X { fst := b, snd := y }.fst
sndW : W ⟶ X { fst := z✝, snd := c }.fst
hW : fstW ≫ π { fst := b, snd := y }.fst = sndW ≫ π { fst := z✝, snd := c }.fst
hW1 : ↑fstW w = { fst := b, snd := y }.snd
hW2 : ↑sndW w = { fst := z✝, snd := c }.snd
⊢ (z, w) ∈ {xy | ↑sndZ xy.fst = ↑fstW xy.snd}
[PROOFSTEP]
dsimp
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
x : ↑(X a).toTop
b : α
y : ↑(X b).toTop
z✝ : α
c : ↑(X z✝).toTop
Z : CompHaus
z : ↑Z.toTop
fstZ : Z ⟶ X { fst := a, snd := x }.fst
sndZ : Z ⟶ X { fst := b, snd := y }.fst
hZ : fstZ ≫ π { fst := a, snd := x }.fst = sndZ ≫ π { fst := b, snd := y }.fst
hZ1 : ↑fstZ z = { fst := a, snd := x }.snd
hZ2 : ↑sndZ z = { fst := b, snd := y }.snd
W : CompHaus
w : ↑W.toTop
fstW : W ⟶ X { fst := b, snd := y }.fst
sndW : W ⟶ X { fst := z✝, snd := c }.fst
hW : fstW ≫ π { fst := b, snd := y }.fst = sndW ≫ π { fst := z✝, snd := c }.fst
hW1 : ↑fstW w = { fst := b, snd := y }.snd
hW2 : ↑sndW w = { fst := z✝, snd := c }.snd
⊢ ↑sndZ z = ↑fstW w
[PROOFSTEP]
rw [hZ2, hW1]
[GOAL]
case trans.mk.mk.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
x : ↑(X a).toTop
b : α
y : ↑(X b).toTop
z✝ : α
c : ↑(X z✝).toTop
Z : CompHaus
z : ↑Z.toTop
fstZ : Z ⟶ X { fst := a, snd := x }.fst
sndZ : Z ⟶ X { fst := b, snd := y }.fst
hZ : fstZ ≫ π { fst := a, snd := x }.fst = sndZ ≫ π { fst := b, snd := y }.fst
hZ1 : ↑fstZ z = { fst := a, snd := x }.snd
hZ2 : ↑sndZ z = { fst := b, snd := y }.snd
W : CompHaus
w : ↑W.toTop
fstW : W ⟶ X { fst := b, snd := y }.fst
sndW : W ⟶ X { fst := z✝, snd := c }.fst
hW : fstW ≫ π { fst := b, snd := y }.fst = sndW ≫ π { fst := z✝, snd := c }.fst
hW1 : ↑fstW w = { fst := b, snd := y }.snd
hW2 : ↑sndW w = { fst := z✝, snd := c }.snd
⊢ (pullback.fst sndZ fstW ≫ fstZ) ≫ π { fst := a, snd := x }.fst =
    (pullback.snd sndZ fstW ≫ sndW) ≫ π { fst := z✝, snd := c }.fst
[PROOFSTEP]
dsimp at *
[GOAL]
case trans.mk.mk.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
x : ↑(X a).toTop
b : α
y : ↑(X b).toTop
z✝ : α
c : ↑(X z✝).toTop
Z : CompHaus
z : ↑Z.toTop
fstZ : Z ⟶ X { fst := a, snd := x }.fst
sndZ : Z ⟶ X { fst := b, snd := y }.fst
hZ : fstZ ≫ π a = sndZ ≫ π b
hZ1 : ↑fstZ z = x
hZ2 : ↑sndZ z = y
W : CompHaus
w : ↑W.toTop
fstW : W ⟶ X { fst := b, snd := y }.fst
sndW : W ⟶ X { fst := z✝, snd := c }.fst
hW : fstW ≫ π b = sndW ≫ π z✝
hW1 : ↑fstW w = y
hW2 : ↑sndW w = c
⊢ (pullback.fst sndZ fstW ≫ fstZ) ≫ π a = (pullback.snd sndZ fstW ≫ sndW) ≫ π z✝
[PROOFSTEP]
simp only [Category.assoc, hZ, ← hW]
[GOAL]
case trans.mk.mk.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
x : ↑(X a).toTop
b : α
y : ↑(X b).toTop
z✝ : α
c : ↑(X z✝).toTop
Z : CompHaus
z : ↑Z.toTop
fstZ : Z ⟶ X { fst := a, snd := x }.fst
sndZ : Z ⟶ X { fst := b, snd := y }.fst
hZ : fstZ ≫ π a = sndZ ≫ π b
hZ1 : ↑fstZ z = x
hZ2 : ↑sndZ z = y
W : CompHaus
w : ↑W.toTop
fstW : W ⟶ X { fst := b, snd := y }.fst
sndW : W ⟶ X { fst := z✝, snd := c }.fst
hW : fstW ≫ π b = sndW ≫ π z✝
hW1 : ↑fstW w = y
hW2 : ↑sndW w = c
⊢ pullback.fst sndZ fstW ≫ sndZ ≫ π b = pullback.snd sndZ fstW ≫ fstW ≫ π b
[PROOFSTEP]
apply ContinuousMap.ext
[GOAL]
case trans.mk.mk.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
x : ↑(X a).toTop
b : α
y : ↑(X b).toTop
z✝ : α
c : ↑(X z✝).toTop
Z : CompHaus
z : ↑Z.toTop
fstZ : Z ⟶ X { fst := a, snd := x }.fst
sndZ : Z ⟶ X { fst := b, snd := y }.fst
hZ : fstZ ≫ π a = sndZ ≫ π b
hZ1 : ↑fstZ z = x
hZ2 : ↑sndZ z = y
W : CompHaus
w : ↑W.toTop
fstW : W ⟶ X { fst := b, snd := y }.fst
sndW : W ⟶ X { fst := z✝, snd := c }.fst
hW : fstW ≫ π b = sndW ≫ π z✝
hW1 : ↑fstW w = y
hW2 : ↑sndW w = c
⊢ ∀ (a : ↑(pullback sndZ fstW).toTop),
    ↑(pullback.fst sndZ fstW ≫ sndZ ≫ π b) a = ↑(pullback.snd sndZ fstW ≫ fstW ≫ π b) a
[PROOFSTEP]
rintro ⟨⟨u, v⟩, h⟩
[GOAL]
case trans.mk.mk.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.mk
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
x : ↑(X a).toTop
b : α
y : ↑(X b).toTop
z✝ : α
c : ↑(X z✝).toTop
Z : CompHaus
z : ↑Z.toTop
fstZ : Z ⟶ X { fst := a, snd := x }.fst
sndZ : Z ⟶ X { fst := b, snd := y }.fst
hZ : fstZ ≫ π a = sndZ ≫ π b
hZ1 : ↑fstZ z = x
hZ2 : ↑sndZ z = y
W : CompHaus
w : ↑W.toTop
fstW : W ⟶ X { fst := b, snd := y }.fst
sndW : W ⟶ X { fst := z✝, snd := c }.fst
hW : fstW ≫ π b = sndW ≫ π z✝
hW1 : ↑fstW w = y
hW2 : ↑sndW w = c
u : ↑Z.toTop
v : ↑W.toTop
h : (u, v) ∈ {xy | ↑sndZ xy.fst = ↑fstW xy.snd}
⊢ ↑(pullback.fst sndZ fstW ≫ sndZ ≫ π b) { val := (u, v), property := h } =
    ↑(pullback.snd sndZ fstW ≫ fstW ≫ π b) { val := (u, v), property := h }
[PROOFSTEP]
change π b (sndZ u) = π b (fstW v)
[GOAL]
case trans.mk.mk.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.h.mk.mk
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
x : ↑(X a).toTop
b : α
y : ↑(X b).toTop
z✝ : α
c : ↑(X z✝).toTop
Z : CompHaus
z : ↑Z.toTop
fstZ : Z ⟶ X { fst := a, snd := x }.fst
sndZ : Z ⟶ X { fst := b, snd := y }.fst
hZ : fstZ ≫ π a = sndZ ≫ π b
hZ1 : ↑fstZ z = x
hZ2 : ↑sndZ z = y
W : CompHaus
w : ↑W.toTop
fstW : W ⟶ X { fst := b, snd := y }.fst
sndW : W ⟶ X { fst := z✝, snd := c }.fst
hW : fstW ≫ π b = sndW ≫ π z✝
hW1 : ↑fstW w = y
hW2 : ↑sndW w = c
u : ↑Z.toTop
v : ↑W.toTop
h : (u, v) ∈ {xy | ↑sndZ xy.fst = ↑fstW xy.snd}
⊢ ↑(π b) (↑sndZ u) = ↑(π b) (↑fstW v)
[PROOFSTEP]
rw [h]
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
⊢ ∀ (a b : ↑(finiteCoproduct fun a => X a).toTop),
    a ≈ b →
      (fun x =>
            match x with
            | { fst := a, snd := x } => ↑(π a) x)
          a =
        (fun x =>
            match x with
            | { fst := a, snd := x } => ↑(π a) x)
          b
[PROOFSTEP]
rintro ⟨a, x⟩ ⟨b, y⟩ ⟨Z, z, fst, snd, h, hx, hy⟩
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
x : ↑((fun a => X a) a).toTop
b : α
y : ↑((fun a => X a) b).toTop
Z : CompHaus
z : ↑Z.toTop
fst : Z ⟶ (fun a => X a) { fst := a, snd := x }.fst
snd : Z ⟶ (fun a => X a) { fst := b, snd := y }.fst
h : fst ≫ π { fst := a, snd := x }.fst = snd ≫ π { fst := b, snd := y }.fst
hx : ↑fst z = { fst := a, snd := x }.snd
hy : ↑snd z = { fst := b, snd := y }.snd
⊢ (fun x =>
        match x with
        | { fst := a, snd := x } => ↑(π a) x)
      { fst := a, snd := x } =
    (fun x =>
        match x with
        | { fst := a, snd := x } => ↑(π a) x)
      { fst := b, snd := y }
[PROOFSTEP]
dsimp at *
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
x : ↑((fun a => X a) a).toTop
b : α
y : ↑((fun a => X a) b).toTop
Z : CompHaus
z : ↑Z.toTop
fst : Z ⟶ (fun a => X a) { fst := a, snd := x }.fst
snd : Z ⟶ (fun a => X a) { fst := b, snd := y }.fst
h : fst ≫ π a = snd ≫ π b
hx : ↑fst z = x
hy : ↑snd z = y
⊢ ↑(π a) x = ↑(π b) y
[PROOFSTEP]
rw [← hx, ← hy]
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
x : ↑((fun a => X a) a).toTop
b : α
y : ↑((fun a => X a) b).toTop
Z : CompHaus
z : ↑Z.toTop
fst : Z ⟶ (fun a => X a) { fst := a, snd := x }.fst
snd : Z ⟶ (fun a => X a) { fst := b, snd := y }.fst
h : fst ≫ π a = snd ≫ π b
hx : ↑fst z = x
hy : ↑snd z = y
⊢ ↑(π a) (↑fst z) = ↑(π b) (↑snd z)
[PROOFSTEP]
apply_fun (fun t => t z) at h 
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
x : ↑((fun a => X a) a).toTop
b : α
y : ↑((fun a => X a) b).toTop
Z : CompHaus
z : ↑Z.toTop
fst : Z ⟶ (fun a => X a) { fst := a, snd := x }.fst
snd : Z ⟶ (fun a => X a) { fst := b, snd := y }.fst
hx : ↑fst z = x
hy : ↑snd z = y
h : ↑(fst ≫ π a) z = ↑(snd ≫ π b) z
⊢ ↑(π a) (↑fst z) = ↑(π b) (↑snd z)
[PROOFSTEP]
exact h
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
⊢ Continuous (ιFun π)
[PROOFSTEP]
apply Continuous.quotient_lift
[GOAL]
case h
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
⊢ Continuous fun x =>
    match x with
    | { fst := a, snd := x } => ↑(π a) x
[PROOFSTEP]
apply continuous_sigma
[GOAL]
case h.hf
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
⊢ ∀ (i : α),
    Continuous fun a =>
      match { fst := i, snd := a } with
      | { fst := a, snd := x } => ↑(π a) x
[PROOFSTEP]
intro a
[GOAL]
case h.hf
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
⊢ Continuous fun a_1 =>
    match { fst := a, snd := a_1 } with
    | { fst := a, snd := x } => ↑(π a) x
[PROOFSTEP]
exact (π a).continuous
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
⊢ Function.Injective (ιFun π)
[PROOFSTEP]
rintro ⟨⟨a, x⟩⟩ ⟨⟨b, y⟩⟩ (h : π _ _ = π _ _)
[GOAL]
case mk.mk.mk.mk
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a₁✝ : Quotient (relation π)
a : α
x : ↑((fun a => X a) a).toTop
a₂✝ : Quotient (relation π)
b : α
y : ↑((fun a => X a) b).toTop
h : ↑(π a) x = ↑(π b) y
⊢ Quot.mk Setoid.r { fst := a, snd := x } = Quot.mk Setoid.r { fst := b, snd := y }
[PROOFSTEP]
apply Quotient.sound'
[GOAL]
case mk.mk.mk.mk.a
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a₁✝ : Quotient (relation π)
a : α
x : ↑((fun a => X a) a).toTop
a₂✝ : Quotient (relation π)
b : α
y : ↑((fun a => X a) b).toTop
h : ↑(π a) x = ↑(π b) y
⊢ Setoid.r { fst := a, snd := x } { fst := b, snd := y }
[PROOFSTEP]
refine ⟨pullback (π a) (π b), ⟨⟨x, y⟩, h⟩, pullback.fst _ _, pullback.snd _ _, ?_, rfl, rfl⟩
[GOAL]
case mk.mk.mk.mk.a
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a₁✝ : Quotient (relation π)
a : α
x : ↑((fun a => X a) a).toTop
a₂✝ : Quotient (relation π)
b : α
y : ↑((fun a => X a) b).toTop
h : ↑(π a) x = ↑(π b) y
⊢ pullback.fst (π a) (π b) ≫ π { fst := a, snd := x }.fst = pullback.snd (π a) (π b) ≫ π { fst := b, snd := y }.fst
[PROOFSTEP]
ext ⟨_, h⟩
[GOAL]
case mk.mk.mk.mk.a.w.mk
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a₁✝ : Quotient (relation π)
a : α
x : ↑((fun a => X a) a).toTop
a₂✝ : Quotient (relation π)
b : α
y : ↑((fun a => X a) b).toTop
h✝ : ↑(π a) x = ↑(π b) y
val✝ : ↑(X a).toTop × ↑(X b).toTop
h : val✝ ∈ {xy | ↑(π a) xy.fst = ↑(π b) xy.snd}
⊢ ↑(pullback.fst (π a) (π b) ≫ π { fst := a, snd := x }.fst) { val := val✝, property := h } =
    ↑(pullback.snd (π a) (π b) ≫ π { fst := b, snd := y }.fst) { val := val✝, property := h }
[PROOFSTEP]
exact h
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
⊢ IsIso (ιHom π)
[PROOFSTEP]
apply isIso_of_bijective
[GOAL]
case bij
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
⊢ Function.Bijective ↑(ιHom π)
[PROOFSTEP]
refine ⟨ιFun_injective _, ?_⟩
[GOAL]
case bij
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
⊢ Function.Surjective ↑(ιHom π)
[PROOFSTEP]
intro b
[GOAL]
case bij
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
b : (forget CompHaus).obj B
⊢ ∃ a, ↑(ιHom π) a = b
[PROOFSTEP]
obtain ⟨a, x, h⟩ := surj b
[GOAL]
case bij.intro.intro
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
b : (forget CompHaus).obj B
a : α
x : ↑(X a).toTop
h : ↑(π a) x = b
⊢ ∃ a, ↑(ιHom π) a = b
[PROOFSTEP]
refine ⟨Quotient.mk _ ⟨a, x⟩, h⟩
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
⊢ Continuous fun x => Quotient.mk (relation π) { fst := a, snd := x }
[PROOFSTEP]
apply Continuous.comp
[GOAL]
case hg
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
⊢ Continuous (Quot.mk Setoid.r)
case hf
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
⊢ Continuous fun x => { fst := a, snd := x }
[PROOFSTEP]
apply continuous_quot_mk
[GOAL]
case hf
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
⊢ Continuous fun x => { fst := a, snd := x }
[PROOFSTEP]
apply continuous_sigmaMk (σ := fun a => X a)
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
W : CompHaus
e : (a : α) → X a ⟶ W
h : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
⊢ ∀ (a b : ↑(finiteCoproduct fun a => (fun a => X a) a).toTop),
    a ≈ b →
      (fun x =>
            match x with
            | { fst := a, snd := x } => ↑(e a) x)
          a =
        (fun x =>
            match x with
            | { fst := a, snd := x } => ↑(e a) x)
          b
[PROOFSTEP]
rintro ⟨a, x⟩ ⟨b, y⟩ ⟨Z, z, fst, snd, hh, hx, hy⟩
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
W : CompHaus
e : (a : α) → X a ⟶ W
h : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
x : ↑((fun a => (fun a => X a) a) a).toTop
b : α
y : ↑((fun a => (fun a => X a) a) b).toTop
Z : CompHaus
z : ↑Z.toTop
fst : Z ⟶ (fun a => (fun a => X a) a) { fst := a, snd := x }.fst
snd : Z ⟶ (fun a => (fun a => X a) a) { fst := b, snd := y }.fst
hh : fst ≫ π { fst := a, snd := x }.fst = snd ≫ π { fst := b, snd := y }.fst
hx : ↑fst z = { fst := a, snd := x }.snd
hy : ↑snd z = { fst := b, snd := y }.snd
⊢ (fun x =>
        match x with
        | { fst := a, snd := x } => ↑(e a) x)
      { fst := a, snd := x } =
    (fun x =>
        match x with
        | { fst := a, snd := x } => ↑(e a) x)
      { fst := b, snd := y }
[PROOFSTEP]
dsimp at *
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
W : CompHaus
e : (a : α) → X a ⟶ W
h : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
x : ↑((fun a => (fun a => X a) a) a).toTop
b : α
y : ↑((fun a => (fun a => X a) a) b).toTop
Z : CompHaus
z : ↑Z.toTop
fst : Z ⟶ (fun a => (fun a => X a) a) { fst := a, snd := x }.fst
snd : Z ⟶ (fun a => (fun a => X a) a) { fst := b, snd := y }.fst
hh : fst ≫ π a = snd ≫ π b
hx : ↑fst z = x
hy : ↑snd z = y
⊢ ↑(e a) x = ↑(e b) y
[PROOFSTEP]
rw [← hx, ← hy]
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
W : CompHaus
e : (a : α) → X a ⟶ W
h : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
x : ↑((fun a => (fun a => X a) a) a).toTop
b : α
y : ↑((fun a => (fun a => X a) a) b).toTop
Z : CompHaus
z : ↑Z.toTop
fst : Z ⟶ (fun a => (fun a => X a) a) { fst := a, snd := x }.fst
snd : Z ⟶ (fun a => (fun a => X a) a) { fst := b, snd := y }.fst
hh : fst ≫ π a = snd ≫ π b
hx : ↑fst z = x
hy : ↑snd z = y
⊢ ↑(e a) (↑fst z) = ↑(e b) (↑snd z)
[PROOFSTEP]
specialize h _ _ fst snd ?_
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
W : CompHaus
e : (a : α) → X a ⟶ W
h : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
x : ↑((fun a => (fun a => X a) a) a).toTop
b : α
y : ↑((fun a => (fun a => X a) a) b).toTop
Z : CompHaus
z : ↑Z.toTop
fst : Z ⟶ (fun a => (fun a => X a) a) { fst := a, snd := x }.fst
snd : Z ⟶ (fun a => (fun a => X a) a) { fst := b, snd := y }.fst
hh : fst ≫ π a = snd ≫ π b
hx : ↑fst z = x
hy : ↑snd z = y
⊢ fst ≫ π' π { fst := a, snd := x }.fst = snd ≫ π' π { fst := b, snd := y }.fst
[PROOFSTEP]
ext z
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.intro.w
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
W : CompHaus
e : (a : α) → X a ⟶ W
h : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
x : ↑((fun a => (fun a => X a) a) a).toTop
b : α
y : ↑((fun a => (fun a => X a) a) b).toTop
Z : CompHaus
z✝ : ↑Z.toTop
fst : Z ⟶ (fun a => (fun a => X a) a) { fst := a, snd := x }.fst
snd : Z ⟶ (fun a => (fun a => X a) a) { fst := b, snd := y }.fst
hh : fst ≫ π a = snd ≫ π b
hx : ↑fst z✝ = x
hy : ↑snd z✝ = y
z : (forget CompHaus).obj Z
⊢ ↑(fst ≫ π' π { fst := a, snd := x }.fst) z = ↑(snd ≫ π' π { fst := b, snd := y }.fst) z
[PROOFSTEP]
apply ιFun_injective
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.intro.w.a
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
W : CompHaus
e : (a : α) → X a ⟶ W
h : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
x : ↑((fun a => (fun a => X a) a) a).toTop
b : α
y : ↑((fun a => (fun a => X a) a) b).toTop
Z : CompHaus
z✝ : ↑Z.toTop
fst : Z ⟶ (fun a => (fun a => X a) a) { fst := a, snd := x }.fst
snd : Z ⟶ (fun a => (fun a => X a) a) { fst := b, snd := y }.fst
hh : fst ≫ π a = snd ≫ π b
hx : ↑fst z✝ = x
hy : ↑snd z✝ = y
z : (forget CompHaus).obj Z
⊢ ιFun π (↑(fst ≫ π' π { fst := a, snd := x }.fst) z) = ιFun π (↑(snd ≫ π' π { fst := b, snd := y }.fst) z)
[PROOFSTEP]
apply_fun (fun q => q z) at hh 
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.intro.w.a
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
W : CompHaus
e : (a : α) → X a ⟶ W
h : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
x : ↑((fun a => (fun a => X a) a) a).toTop
b : α
y : ↑((fun a => (fun a => X a) a) b).toTop
Z : CompHaus
z✝ : ↑Z.toTop
fst : Z ⟶ (fun a => (fun a => X a) a) { fst := a, snd := x }.fst
snd : Z ⟶ (fun a => (fun a => X a) a) { fst := b, snd := y }.fst
hx : ↑fst z✝ = x
hy : ↑snd z✝ = y
z : (forget CompHaus).obj Z
hh : ↑(fst ≫ π a) z = ↑(snd ≫ π b) z
⊢ ιFun π (↑(fst ≫ π' π { fst := a, snd := x }.fst) z) = ιFun π (↑(snd ≫ π' π { fst := b, snd := y }.fst) z)
[PROOFSTEP]
exact hh
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
W : CompHaus
e : (a : α) → X a ⟶ W
a : α
x : ↑((fun a => (fun a => X a) a) a).toTop
b : α
y : ↑((fun a => (fun a => X a) a) b).toTop
Z : CompHaus
z : ↑Z.toTop
fst : Z ⟶ (fun a => (fun a => X a) a) { fst := a, snd := x }.fst
snd : Z ⟶ (fun a => (fun a => X a) a) { fst := b, snd := y }.fst
hh : fst ≫ π a = snd ≫ π b
hx : ↑fst z = x
hy : ↑snd z = y
h : fst ≫ e { fst := a, snd := x }.fst = snd ≫ e { fst := b, snd := y }.fst
⊢ ↑(e a) (↑fst z) = ↑(e b) (↑snd z)
[PROOFSTEP]
apply_fun (fun q => q z) at h 
[GOAL]
case mk.mk.intro.intro.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
W : CompHaus
e : (a : α) → X a ⟶ W
a : α
x : ↑((fun a => (fun a => X a) a) a).toTop
b : α
y : ↑((fun a => (fun a => X a) a) b).toTop
Z : CompHaus
z : ↑Z.toTop
fst : Z ⟶ (fun a => (fun a => X a) a) { fst := a, snd := x }.fst
snd : Z ⟶ (fun a => (fun a => X a) a) { fst := b, snd := y }.fst
hh : fst ≫ π a = snd ≫ π b
hx : ↑fst z = x
hy : ↑snd z = y
h : ↑(fst ≫ e { fst := a, snd := x }.fst) z = ↑(snd ≫ e { fst := b, snd := y }.fst) z
⊢ ↑(e a) (↑fst z) = ↑(e b) (↑snd z)
[PROOFSTEP]
exact h
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
W : CompHaus
e : (a : α) → X a ⟶ W
h : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
⊢ Continuous
    (Quotient.lift
      (fun x =>
        match x with
        | { fst := a, snd := x } => ↑(e a) x)
      (_ :
        ∀ (a b : ↑(finiteCoproduct fun a => (fun a => X a) a).toTop),
          a ≈ b →
            (fun x =>
                  match x with
                  | { fst := a, snd := x } => ↑(e a) x)
                a =
              (fun x =>
                  match x with
                  | { fst := a, snd := x } => ↑(e a) x)
                b))
[PROOFSTEP]
apply Continuous.quotient_lift
[GOAL]
case h
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
W : CompHaus
e : (a : α) → X a ⟶ W
h : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
⊢ Continuous fun x =>
    match x with
    | { fst := a, snd := x } => ↑(e a) x
[PROOFSTEP]
apply continuous_sigma
[GOAL]
case h.hf
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
W : CompHaus
e : (a : α) → X a ⟶ W
h : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
⊢ ∀ (i : α),
    Continuous fun a =>
      match { fst := i, snd := a } with
      | { fst := a, snd := x } => ↑(e a) x
[PROOFSTEP]
intro a
[GOAL]
case h.hf
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
W : CompHaus
e : (a : α) → X a ⟶ W
h : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ Continuous fun a_1 =>
    match { fst := a, snd := a_1 } with
    | { fst := a, snd := x } => ↑(e a) x
[PROOFSTEP]
exact (e a).continuous
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
⊢ ∀ {W : CompHaus} (e : (a : α) → X a ⟶ W)
    (h :
      ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂)
    (a : α),
    π' π a ≫
        (fun {W} e h =>
            ContinuousMap.mk
              (Quotient.lift
                (fun x =>
                  match x with
                  | { fst := a, snd := x } => ↑(e a) x)
                (_ :
                  ∀ (a b : ↑(finiteCoproduct fun a => (fun a => X a) a).toTop),
                    a ≈ b →
                      (fun x =>
                            match x with
                            | { fst := a, snd := x } => ↑(e a) x)
                          a =
                        (fun x =>
                            match x with
                            | { fst := a, snd := x } => ↑(e a) x)
                          b)))
          e
          (_ :
            ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
              g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) =
      e a
[PROOFSTEP]
intro Z e h a
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
Z : CompHaus
e : (a : α) → X a ⟶ Z
h :
  ∀ {Z_1 : CompHaus} (a₁ a₂ : α) (g₁ : Z_1 ⟶ X a₁) (g₂ : Z_1 ⟶ X a₂),
    g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ π' π a ≫
      (fun {W} e h =>
          ContinuousMap.mk
            (Quotient.lift
              (fun x =>
                match x with
                | { fst := a, snd := x } => ↑(e a) x)
              (_ :
                ∀ (a b : ↑(finiteCoproduct fun a => (fun a => X a) a).toTop),
                  a ≈ b →
                    (fun x =>
                          match x with
                          | { fst := a, snd := x } => ↑(e a) x)
                        a =
                      (fun x =>
                          match x with
                          | { fst := a, snd := x } => ↑(e a) x)
                        b)))
        e
        (_ :
          ∀ {Z_1 : CompHaus} (a₁ a₂ : α) (g₁ : Z_1 ⟶ X a₁) (g₂ : Z_1 ⟶ X a₂),
            g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) =
    e a
[PROOFSTEP]
ext
[GOAL]
case w
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
Z : CompHaus
e : (a : α) → X a ⟶ Z
h :
  ∀ {Z_1 : CompHaus} (a₁ a₂ : α) (g₁ : Z_1 ⟶ X a₁) (g₂ : Z_1 ⟶ X a₂),
    g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
x✝ : (forget CompHaus).obj (X a)
⊢ ↑(π' π a ≫
          (fun {W} e h =>
              ContinuousMap.mk
                (Quotient.lift
                  (fun x =>
                    match x with
                    | { fst := a, snd := x } => ↑(e a) x)
                  (_ :
                    ∀ (a b : ↑(finiteCoproduct fun a => (fun a => X a) a).toTop),
                      a ≈ b →
                        (fun x =>
                              match x with
                              | { fst := a, snd := x } => ↑(e a) x)
                            a =
                          (fun x =>
                              match x with
                              | { fst := a, snd := x } => ↑(e a) x)
                            b)))
            e
            (_ :
              ∀ {Z_1 : CompHaus} (a₁ a₂ : α) (g₁ : Z_1 ⟶ X a₁) (g₂ : Z_1 ⟶ X a₂),
                g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂))
      x✝ =
    ↑(e a) x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
⊢ ∀ {W : CompHaus} (e : (a : α) → X a ⟶ W)
    (h :
      ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂)
    (m : QB π ⟶ W),
    (∀ (a : α), π' π a ≫ m = e a) →
      m =
        (fun {W} e h =>
            ContinuousMap.mk
              (Quotient.lift
                (fun x =>
                  match x with
                  | { fst := a, snd := x } => ↑(e a) x)
                (_ :
                  ∀ (a b : ↑(finiteCoproduct fun a => (fun a => X a) a).toTop),
                    a ≈ b →
                      (fun x =>
                            match x with
                            | { fst := a, snd := x } => ↑(e a) x)
                          a =
                        (fun x =>
                            match x with
                            | { fst := a, snd := x } => ↑(e a) x)
                          b)))
          e
          (_ :
            ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
              g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂)
[PROOFSTEP]
intro Z e h m hm
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
Z : CompHaus
e : (a : α) → X a ⟶ Z
h :
  ∀ {Z_1 : CompHaus} (a₁ a₂ : α) (g₁ : Z_1 ⟶ X a₁) (g₂ : Z_1 ⟶ X a₂),
    g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : QB π ⟶ Z
hm : ∀ (a : α), π' π a ≫ m = e a
⊢ m =
    (fun {W} e h =>
        ContinuousMap.mk
          (Quotient.lift
            (fun x =>
              match x with
              | { fst := a, snd := x } => ↑(e a) x)
            (_ :
              ∀ (a b : ↑(finiteCoproduct fun a => (fun a => X a) a).toTop),
                a ≈ b →
                  (fun x =>
                        match x with
                        | { fst := a, snd := x } => ↑(e a) x)
                      a =
                    (fun x =>
                        match x with
                        | { fst := a, snd := x } => ↑(e a) x)
                      b)))
      e
      (_ :
        ∀ {Z_1 : CompHaus} (a₁ a₂ : α) (g₁ : Z_1 ⟶ X a₁) (g₂ : Z_1 ⟶ X a₂),
          g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂)
[PROOFSTEP]
ext ⟨⟨a, x⟩⟩
[GOAL]
case w.mk.mk
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
Z : CompHaus
e : (a : α) → X a ⟶ Z
h :
  ∀ {Z_1 : CompHaus} (a₁ a₂ : α) (g₁ : Z_1 ⟶ X a₁) (g₂ : Z_1 ⟶ X a₂),
    g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : QB π ⟶ Z
hm : ∀ (a : α), π' π a ≫ m = e a
x✝ : (forget CompHaus).obj (QB π)
a : α
x : ↑((fun a => (fun a => X a) a) a).toTop
⊢ ↑m (Quot.mk Setoid.r { fst := a, snd := x }) =
    ↑((fun {W} e h =>
            ContinuousMap.mk
              (Quotient.lift
                (fun x =>
                  match x with
                  | { fst := a, snd := x } => ↑(e a) x)
                (_ :
                  ∀ (a b : ↑(finiteCoproduct fun a => (fun a => X a) a).toTop),
                    a ≈ b →
                      (fun x =>
                            match x with
                            | { fst := a, snd := x } => ↑(e a) x)
                          a =
                        (fun x =>
                            match x with
                            | { fst := a, snd := x } => ↑(e a) x)
                          b)))
          e
          (_ :
            ∀ {Z_1 : CompHaus} (a₁ a₂ : α) (g₁ : Z_1 ⟶ X a₁) (g₂ : Z_1 ⟶ X a₂),
              g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂))
      (Quot.mk Setoid.r { fst := a, snd := x })
[PROOFSTEP]
specialize hm a
[GOAL]
case w.mk.mk
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
Z : CompHaus
e : (a : α) → X a ⟶ Z
h :
  ∀ {Z_1 : CompHaus} (a₁ a₂ : α) (g₁ : Z_1 ⟶ X a₁) (g₂ : Z_1 ⟶ X a₂),
    g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : QB π ⟶ Z
x✝ : (forget CompHaus).obj (QB π)
a : α
x : ↑((fun a => (fun a => X a) a) a).toTop
hm : π' π a ≫ m = e a
⊢ ↑m (Quot.mk Setoid.r { fst := a, snd := x }) =
    ↑((fun {W} e h =>
            ContinuousMap.mk
              (Quotient.lift
                (fun x =>
                  match x with
                  | { fst := a, snd := x } => ↑(e a) x)
                (_ :
                  ∀ (a b : ↑(finiteCoproduct fun a => (fun a => X a) a).toTop),
                    a ≈ b →
                      (fun x =>
                            match x with
                            | { fst := a, snd := x } => ↑(e a) x)
                          a =
                        (fun x =>
                            match x with
                            | { fst := a, snd := x } => ↑(e a) x)
                          b)))
          e
          (_ :
            ∀ {Z_1 : CompHaus} (a₁ a₂ : α) (g₁ : Z_1 ⟶ X a₁) (g₂ : Z_1 ⟶ X a₂),
              g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂))
      (Quot.mk Setoid.r { fst := a, snd := x })
[PROOFSTEP]
apply_fun (fun q => q x) at hm 
[GOAL]
case w.mk.mk
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
Z : CompHaus
e : (a : α) → X a ⟶ Z
h :
  ∀ {Z_1 : CompHaus} (a₁ a₂ : α) (g₁ : Z_1 ⟶ X a₁) (g₂ : Z_1 ⟶ X a₂),
    g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : QB π ⟶ Z
x✝ : (forget CompHaus).obj (QB π)
a : α
x : ↑((fun a => (fun a => X a) a) a).toTop
hm : ↑(π' π a ≫ m) x = ↑(e a) x
⊢ ↑m (Quot.mk Setoid.r { fst := a, snd := x }) =
    ↑((fun {W} e h =>
            ContinuousMap.mk
              (Quotient.lift
                (fun x =>
                  match x with
                  | { fst := a, snd := x } => ↑(e a) x)
                (_ :
                  ∀ (a b : ↑(finiteCoproduct fun a => (fun a => X a) a).toTop),
                    a ≈ b →
                      (fun x =>
                            match x with
                            | { fst := a, snd := x } => ↑(e a) x)
                          a =
                        (fun x =>
                            match x with
                            | { fst := a, snd := x } => ↑(e a) x)
                          b)))
          e
          (_ :
            ∀ {Z_1 : CompHaus} (a₁ a₂ : α) (g₁ : Z_1 ⟶ X a₁) (g₂ : Z_1 ⟶ X a₂),
              g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂))
      (Quot.mk Setoid.r { fst := a, snd := x })
[PROOFSTEP]
exact hm
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
⊢ π' π a ≫ (ι (fun a => π a) surj).hom = π a
[PROOFSTEP]
ext
[GOAL]
case w
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
x✝ : (forget CompHaus).obj (X a)
⊢ ↑(π' π a ≫ (ι (fun a => π a) surj).hom) x✝ = ↑(π a) x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
⊢ π a ≫ (ι (fun a => π a) surj).inv = π' π a
[PROOFSTEP]
rw [Iso.comp_inv_eq]
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
a : α
⊢ π a = π' π a ≫ (ι (fun a => π a) surj).hom
[PROOFSTEP]
exact
  π'_comp_ι_hom _ surj
    _
      -- TODO: Make a general construction for transferring such structs along isomorphisms.
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
W : CompHaus
e : (a : α) → X a ⟶ W
h : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : CompHaus
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hh : g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂
⊢ g₁ ≫ e a₁ = g₂ ≫ e a₂
[PROOFSTEP]
apply h
[GOAL]
case a
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
W : CompHaus
e : (a : α) → X a ⟶ W
h : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : CompHaus
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hh : g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂
⊢ g₁ ≫ π a₁ = g₂ ≫ π a₂
[PROOFSTEP]
rw [← cancel_mono (ι _ surj).inv]
[GOAL]
case a
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
W : CompHaus
e : (a : α) → X a ⟶ W
h : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : CompHaus
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hh : g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂
⊢ (g₁ ≫ π a₁) ≫ (ι (fun a => π a) surj).inv = (g₂ ≫ π a₂) ≫ (ι (fun a => π a) surj).inv
[PROOFSTEP]
simpa only [Category.assoc, π_comp_ι_inv]
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
⊢ ∀ {W : CompHaus} (e : (a : α) → X a ⟶ W)
    (h : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂)
    (a : α),
    π a ≫
        (fun {W} e h =>
            (ι π surj).inv ≫
              EffectiveEpiFamilyStruct.desc (structAux π) e
                (_ :
                  ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
                    g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂))
          e
          (_ :
            ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
              g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) =
      e a
[PROOFSTEP]
intro W e h a
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
W : CompHaus
e : (a : α) → X a ⟶ W
h : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ π a ≫
      (fun {W} e h =>
          (ι π surj).inv ≫
            EffectiveEpiFamilyStruct.desc (structAux π) e
              (_ :
                ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
                  g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂))
        e
        (_ :
          ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) =
    e a
[PROOFSTEP]
simp only [Eq.ndrec, id_eq, eq_mpr_eq_cast, π_comp_ι_inv_assoc, (structAux π).fac]
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
⊢ ∀ {W : CompHaus} (e : (a : α) → X a ⟶ W)
    (h : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂)
    (m : B ⟶ W),
    (∀ (a : α), π a ≫ m = e a) →
      m =
        (fun {W} e h =>
            (ι π surj).inv ≫
              EffectiveEpiFamilyStruct.desc (structAux π) e
                (_ :
                  ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
                    g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂))
          e
          (_ :
            ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂)
[PROOFSTEP]
intro W e h m hm
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
W : CompHaus
e : (a : α) → X a ⟶ W
h : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
⊢ m =
    (fun {W} e h =>
        (ι π surj).inv ≫
          EffectiveEpiFamilyStruct.desc (structAux π) e
            (_ :
              ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
                g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂))
      e
      (_ : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂)
[PROOFSTEP]
dsimp
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
W : CompHaus
e : (a : α) → X a ⟶ W
h : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
⊢ m =
    (ι π surj).inv ≫
      EffectiveEpiFamilyStruct.desc (structAux π) e
        (_ :
          ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
            g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂)
[PROOFSTEP]
rw [Iso.eq_inv_comp]
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
W : CompHaus
e : (a : α) → X a ⟶ W
h : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
⊢ (ι π surj).hom ≫ m =
    EffectiveEpiFamilyStruct.desc (structAux π) e
      (_ :
        ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
          g₁ ≫ π' π a₁ = g₂ ≫ π' π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂)
[PROOFSTEP]
apply (structAux π).uniq
[GOAL]
case a
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
W : CompHaus
e : (a : α) → X a ⟶ W
h : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
⊢ ∀ (a : α), π' π a ≫ (ι π surj).hom ≫ m = e a
[PROOFSTEP]
intro a
[GOAL]
case a
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
W : CompHaus
e : (a : α) → X a ⟶ W
h : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
a : α
⊢ π' π a ≫ (ι π surj).hom ≫ m = e a
[PROOFSTEP]
simpa using hm a
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
⊢ TFAE [EffectiveEpiFamily X π, Epi (Sigma.desc π), ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b]
[PROOFSTEP]
tfae_have 1 → 2
[GOAL]
case tfae_1_to_2
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
⊢ EffectiveEpiFamily X π → Epi (Sigma.desc π)
[PROOFSTEP]
intro
[GOAL]
case tfae_1_to_2
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
✝ : EffectiveEpiFamily X π
⊢ Epi (Sigma.desc π)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
⊢ TFAE [EffectiveEpiFamily X π, Epi (Sigma.desc π), ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b]
[PROOFSTEP]
tfae_have 2 → 3
[GOAL]
case tfae_2_to_3
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
⊢ Epi (Sigma.desc π) → ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
[PROOFSTEP]
intro e
[GOAL]
case tfae_2_to_3
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Epi (Sigma.desc π)
⊢ ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
[PROOFSTEP]
rw [epi_iff_surjective] at e 
[GOAL]
case tfae_2_to_3
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
⊢ ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
[PROOFSTEP]
let i : ∐ X ≅ finiteCoproduct X := (colimit.isColimit _).coconePointUniqueUpToIso (finiteCoproduct.isColimit _)
[GOAL]
case tfae_2_to_3
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
⊢ ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
[PROOFSTEP]
intro b
[GOAL]
case tfae_2_to_3
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
b : ↑B.toTop
⊢ ∃ a x, ↑(π a) x = b
[PROOFSTEP]
obtain ⟨t, rfl⟩ := e b
[GOAL]
case tfae_2_to_3.intro
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : (forget CompHaus).obj (∐ fun b => X b)
⊢ ∃ a x, ↑(π a) x = ↑(Sigma.desc π) t
[PROOFSTEP]
let q := i.hom t
[GOAL]
case tfae_2_to_3.intro
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : (forget CompHaus).obj (∐ fun b => X b)
q : (fun x => (forget CompHaus).obj (finiteCoproduct X)) t := ↑i.hom t
⊢ ∃ a x, ↑(π a) x = ↑(Sigma.desc π) t
[PROOFSTEP]
refine ⟨q.1, q.2, ?_⟩
[GOAL]
case tfae_2_to_3.intro
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : (forget CompHaus).obj (∐ fun b => X b)
q : (fun x => (forget CompHaus).obj (finiteCoproduct X)) t := ↑i.hom t
⊢ ↑(π q.fst) q.snd = ↑(Sigma.desc π) t
[PROOFSTEP]
have : t = i.inv (i.hom t) := show t = (i.hom ≫ i.inv) t by simp only [i.hom_inv_id]; rfl
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : (forget CompHaus).obj (∐ fun b => X b)
q : (fun x => (forget CompHaus).obj (finiteCoproduct X)) t := ↑i.hom t
⊢ t = ↑(i.hom ≫ i.inv) t
[PROOFSTEP]
simp only [i.hom_inv_id]
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : (forget CompHaus).obj (∐ fun b => X b)
q : (fun x => (forget CompHaus).obj (finiteCoproduct X)) t := ↑i.hom t
⊢ t = ↑(𝟙 (∐ X)) t
[PROOFSTEP]
rfl
[GOAL]
case tfae_2_to_3.intro
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : (forget CompHaus).obj (∐ fun b => X b)
q : (fun x => (forget CompHaus).obj (finiteCoproduct X)) t := ↑i.hom t
this : t = ↑i.inv (↑i.hom t)
⊢ ↑(π q.fst) q.snd = ↑(Sigma.desc π) t
[PROOFSTEP]
rw [this]
[GOAL]
case tfae_2_to_3.intro
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : (forget CompHaus).obj (∐ fun b => X b)
q : (fun x => (forget CompHaus).obj (finiteCoproduct X)) t := ↑i.hom t
this : t = ↑i.inv (↑i.hom t)
⊢ ↑(π q.fst) q.snd = ↑(Sigma.desc π) (↑i.inv (↑i.hom t))
[PROOFSTEP]
show _ = (i.inv ≫ Sigma.desc π) (i.hom t)
[GOAL]
case tfae_2_to_3.intro
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : (forget CompHaus).obj (∐ fun b => X b)
q : (fun x => (forget CompHaus).obj (finiteCoproduct X)) t := ↑i.hom t
this : t = ↑i.inv (↑i.hom t)
⊢ ↑(π q.fst) q.snd = ↑(i.inv ≫ Sigma.desc π) (↑i.hom t)
[PROOFSTEP]
suffices i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π by rw [this]; rfl
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : (forget CompHaus).obj (∐ fun b => X b)
q : (fun x => (forget CompHaus).obj (finiteCoproduct X)) t := ↑i.hom t
this✝ : t = ↑i.inv (↑i.hom t)
this : i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π
⊢ ↑(π q.fst) q.snd = ↑(i.inv ≫ Sigma.desc π) (↑i.hom t)
[PROOFSTEP]
rw [this]
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : (forget CompHaus).obj (∐ fun b => X b)
q : (fun x => (forget CompHaus).obj (finiteCoproduct X)) t := ↑i.hom t
this✝ : t = ↑i.inv (↑i.hom t)
this : i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π
⊢ ↑(π q.fst) q.snd = ↑(finiteCoproduct.desc X π) (↑i.hom t)
[PROOFSTEP]
rfl
[GOAL]
case tfae_2_to_3.intro
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : (forget CompHaus).obj (∐ fun b => X b)
q : (fun x => (forget CompHaus).obj (finiteCoproduct X)) t := ↑i.hom t
this : t = ↑i.inv (↑i.hom t)
⊢ i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π
[PROOFSTEP]
rw [Iso.inv_comp_eq]
[GOAL]
case tfae_2_to_3.intro
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : (forget CompHaus).obj (∐ fun b => X b)
q : (fun x => (forget CompHaus).obj (finiteCoproduct X)) t := ↑i.hom t
this : t = ↑i.inv (↑i.hom t)
⊢ Sigma.desc π = i.hom ≫ finiteCoproduct.desc X π
[PROOFSTEP]
apply colimit.hom_ext
[GOAL]
case tfae_2_to_3.intro.w
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : (forget CompHaus).obj (∐ fun b => X b)
q : (fun x => (forget CompHaus).obj (finiteCoproduct X)) t := ↑i.hom t
this : t = ↑i.inv (↑i.hom t)
⊢ ∀ (j : Discrete α),
    colimit.ι (Discrete.functor X) j ≫ Sigma.desc π =
      colimit.ι (Discrete.functor X) j ≫ i.hom ≫ finiteCoproduct.desc X π
[PROOFSTEP]
rintro ⟨a⟩
[GOAL]
case tfae_2_to_3.intro.w.mk
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : (forget CompHaus).obj (∐ fun b => X b)
q : (fun x => (forget CompHaus).obj (finiteCoproduct X)) t := ↑i.hom t
this : t = ↑i.inv (↑i.hom t)
a : α
⊢ colimit.ι (Discrete.functor X) { as := a } ≫ Sigma.desc π =
    colimit.ι (Discrete.functor X) { as := a } ≫ i.hom ≫ finiteCoproduct.desc X π
[PROOFSTEP]
simp only [Discrete.functor_obj, colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app,
  colimit.comp_coconePointUniqueUpToIso_hom_assoc]
[GOAL]
case tfae_2_to_3.intro.w.mk
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : (forget CompHaus).obj (∐ fun b => X b)
q : (fun x => (forget CompHaus).obj (finiteCoproduct X)) t := ↑i.hom t
this : t = ↑i.inv (↑i.hom t)
a : α
⊢ π a = NatTrans.app (finiteCoproduct.cocone X).ι { as := a } ≫ finiteCoproduct.desc X π
[PROOFSTEP]
ext
[GOAL]
case tfae_2_to_3.intro.w.mk.w
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : (forget CompHaus).obj (∐ fun b => X b)
q : (fun x => (forget CompHaus).obj (finiteCoproduct X)) t := ↑i.hom t
this : t = ↑i.inv (↑i.hom t)
a : α
x✝ : (forget CompHaus).obj (X a)
⊢ ↑(π a) x✝ = ↑(NatTrans.app (finiteCoproduct.cocone X).ι { as := a } ≫ finiteCoproduct.desc X π) x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_2_to_3 : Epi (Sigma.desc π) → ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
⊢ TFAE [EffectiveEpiFamily X π, Epi (Sigma.desc π), ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b]
[PROOFSTEP]
tfae_have 3 → 1
[GOAL]
case tfae_3_to_1
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_2_to_3 : Epi (Sigma.desc π) → ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
⊢ (∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b) → EffectiveEpiFamily X π
[PROOFSTEP]
apply effectiveEpiFamily_of_jointly_surjective
[GOAL]
α : Type
inst✝ : Fintype α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_2_to_3 : Epi (Sigma.desc π) → ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b
tfae_3_to_1 : (∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b) → EffectiveEpiFamily X π
⊢ TFAE [EffectiveEpiFamily X π, Epi (Sigma.desc π), ∀ (b : ↑B.toTop), ∃ a x, ↑(π a) x = b]
[PROOFSTEP]
tfae_finish
[GOAL]
⊢ Precoherent CompHaus
[PROOFSTEP]
constructor
[GOAL]
case pullback
⊢ ∀ {B₁ B₂ : CompHaus} (f : B₂ ⟶ B₁) (α : Type) [inst : Fintype α] (X₁ : α → CompHaus) (π₁ : (a : α) → X₁ a ⟶ B₁),
    EffectiveEpiFamily X₁ π₁ → ∃ β x X₂ π₂, EffectiveEpiFamily X₂ π₂ ∧ ∃ i ι, ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f
[PROOFSTEP]
intro B₁ B₂ f α _ X₁ π₁ h₁
[GOAL]
case pullback
B₁ B₂ : CompHaus
f : B₂ ⟶ B₁
α : Type
inst✝ : Fintype α
X₁ : α → CompHaus
π₁ : (a : α) → X₁ a ⟶ B₁
h₁ : EffectiveEpiFamily X₁ π₁
⊢ ∃ β x X₂ π₂, EffectiveEpiFamily X₂ π₂ ∧ ∃ i ι, ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f
[PROOFSTEP]
refine ⟨α, inferInstance, fun a => pullback f (π₁ a), fun a => pullback.fst _ _, ?_, id, fun a => pullback.snd _ _, ?_⟩
[GOAL]
case pullback.refine_1
B₁ B₂ : CompHaus
f : B₂ ⟶ B₁
α : Type
inst✝ : Fintype α
X₁ : α → CompHaus
π₁ : (a : α) → X₁ a ⟶ B₁
h₁ : EffectiveEpiFamily X₁ π₁
⊢ EffectiveEpiFamily (fun a => pullback f (π₁ a)) fun a => pullback.fst f (π₁ a)
[PROOFSTEP]
have := (effectiveEpiFamily_tfae _ π₁).out 0 2
[GOAL]
case pullback.refine_1
B₁ B₂ : CompHaus
f : B₂ ⟶ B₁
α : Type
inst✝ : Fintype α
X₁ : α → CompHaus
π₁ : (a : α) → X₁ a ⟶ B₁
h₁ : EffectiveEpiFamily X₁ π₁
this : EffectiveEpiFamily (fun a => X₁ a) π₁ ↔ ∀ (b : ↑B₁.toTop), ∃ a x, ↑(π₁ a) x = b
⊢ EffectiveEpiFamily (fun a => pullback f (π₁ a)) fun a => pullback.fst f (π₁ a)
[PROOFSTEP]
rw [this] at h₁ 
[GOAL]
case pullback.refine_1
B₁ B₂ : CompHaus
f : B₂ ⟶ B₁
α : Type
inst✝ : Fintype α
X₁ : α → CompHaus
π₁ : (a : α) → X₁ a ⟶ B₁
h₁ : ∀ (b : ↑B₁.toTop), ∃ a x, ↑(π₁ a) x = b
this : EffectiveEpiFamily (fun a => X₁ a) π₁ ↔ ∀ (b : ↑B₁.toTop), ∃ a x, ↑(π₁ a) x = b
⊢ EffectiveEpiFamily (fun a => pullback f (π₁ a)) fun a => pullback.fst f (π₁ a)
[PROOFSTEP]
clear this
[GOAL]
case pullback.refine_1
B₁ B₂ : CompHaus
f : B₂ ⟶ B₁
α : Type
inst✝ : Fintype α
X₁ : α → CompHaus
π₁ : (a : α) → X₁ a ⟶ B₁
h₁ : ∀ (b : ↑B₁.toTop), ∃ a x, ↑(π₁ a) x = b
⊢ EffectiveEpiFamily (fun a => pullback f (π₁ a)) fun a => pullback.fst f (π₁ a)
[PROOFSTEP]
have := (effectiveEpiFamily_tfae _ (fun a => pullback.fst f (π₁ a))).out 0 2
[GOAL]
case pullback.refine_1
B₁ B₂ : CompHaus
f : B₂ ⟶ B₁
α : Type
inst✝ : Fintype α
X₁ : α → CompHaus
π₁ : (a : α) → X₁ a ⟶ B₁
h₁ : ∀ (b : ↑B₁.toTop), ∃ a x, ↑(π₁ a) x = b
this :
  (EffectiveEpiFamily (fun a => pullback f (π₁ a)) fun a => pullback.fst f (π₁ a)) ↔
    ∀ (b : ↑B₂.toTop), ∃ a x, ↑(pullback.fst f (π₁ a)) x = b
⊢ EffectiveEpiFamily (fun a => pullback f (π₁ a)) fun a => pullback.fst f (π₁ a)
[PROOFSTEP]
rw [this]
[GOAL]
case pullback.refine_1
B₁ B₂ : CompHaus
f : B₂ ⟶ B₁
α : Type
inst✝ : Fintype α
X₁ : α → CompHaus
π₁ : (a : α) → X₁ a ⟶ B₁
h₁ : ∀ (b : ↑B₁.toTop), ∃ a x, ↑(π₁ a) x = b
this :
  (EffectiveEpiFamily (fun a => pullback f (π₁ a)) fun a => pullback.fst f (π₁ a)) ↔
    ∀ (b : ↑B₂.toTop), ∃ a x, ↑(pullback.fst f (π₁ a)) x = b
⊢ ∀ (b : ↑B₂.toTop), ∃ a x, ↑(pullback.fst f (π₁ a)) x = b
[PROOFSTEP]
clear this
[GOAL]
case pullback.refine_1
B₁ B₂ : CompHaus
f : B₂ ⟶ B₁
α : Type
inst✝ : Fintype α
X₁ : α → CompHaus
π₁ : (a : α) → X₁ a ⟶ B₁
h₁ : ∀ (b : ↑B₁.toTop), ∃ a x, ↑(π₁ a) x = b
⊢ ∀ (b : ↑B₂.toTop), ∃ a x, ↑(pullback.fst f (π₁ a)) x = b
[PROOFSTEP]
intro b₂
[GOAL]
case pullback.refine_1
B₁ B₂ : CompHaus
f : B₂ ⟶ B₁
α : Type
inst✝ : Fintype α
X₁ : α → CompHaus
π₁ : (a : α) → X₁ a ⟶ B₁
h₁ : ∀ (b : ↑B₁.toTop), ∃ a x, ↑(π₁ a) x = b
b₂ : ↑B₂.toTop
⊢ ∃ a x, ↑(pullback.fst f (π₁ a)) x = b₂
[PROOFSTEP]
obtain ⟨a, x, h⟩ := h₁ (f b₂)
[GOAL]
case pullback.refine_1.intro.intro
B₁ B₂ : CompHaus
f : B₂ ⟶ B₁
α : Type
inst✝ : Fintype α
X₁ : α → CompHaus
π₁ : (a : α) → X₁ a ⟶ B₁
h₁ : ∀ (b : ↑B₁.toTop), ∃ a x, ↑(π₁ a) x = b
b₂ : ↑B₂.toTop
a : α
x : ↑(X₁ a).toTop
h : ↑(π₁ a) x = ↑f b₂
⊢ ∃ a x, ↑(pullback.fst f (π₁ a)) x = b₂
[PROOFSTEP]
refine ⟨a, ⟨⟨b₂, x⟩, h.symm⟩, rfl⟩
[GOAL]
case pullback.refine_2
B₁ B₂ : CompHaus
f : B₂ ⟶ B₁
α : Type
inst✝ : Fintype α
X₁ : α → CompHaus
π₁ : (a : α) → X₁ a ⟶ B₁
h₁ : EffectiveEpiFamily X₁ π₁
⊢ ∀ (b : α), (fun a => pullback.snd f (π₁ a)) b ≫ π₁ (id b) = (fun a => pullback.fst f (π₁ a)) b ≫ f
[PROOFSTEP]
intro a
[GOAL]
case pullback.refine_2
B₁ B₂ : CompHaus
f : B₂ ⟶ B₁
α : Type
inst✝ : Fintype α
X₁ : α → CompHaus
π₁ : (a : α) → X₁ a ⟶ B₁
h₁ : EffectiveEpiFamily X₁ π₁
a : α
⊢ (fun a => pullback.snd f (π₁ a)) a ≫ π₁ (id a) = (fun a => pullback.fst f (π₁ a)) a ≫ f
[PROOFSTEP]
dsimp
[GOAL]
case pullback.refine_2
B₁ B₂ : CompHaus
f : B₂ ⟶ B₁
α : Type
inst✝ : Fintype α
X₁ : α → CompHaus
π₁ : (a : α) → X₁ a ⟶ B₁
h₁ : EffectiveEpiFamily X₁ π₁
a : α
⊢ pullback.snd f (π₁ a) ≫ π₁ a = pullback.fst f (π₁ a) ≫ f
[PROOFSTEP]
ext ⟨⟨_, _⟩, h⟩
[GOAL]
case pullback.refine_2.w.mk.mk
B₁ B₂ : CompHaus
f : B₂ ⟶ B₁
α : Type
inst✝ : Fintype α
X₁ : α → CompHaus
π₁ : (a : α) → X₁ a ⟶ B₁
h₁ : EffectiveEpiFamily X₁ π₁
a : α
fst✝ : ↑B₂.toTop
snd✝ : ↑(X₁ a).toTop
h : (fst✝, snd✝) ∈ {xy | ↑f xy.fst = ↑(π₁ a) xy.snd}
⊢ ↑(pullback.snd f (π₁ a) ≫ π₁ a) { val := (fst✝, snd✝), property := h } =
    ↑(pullback.fst f (π₁ a) ≫ f) { val := (fst✝, snd✝), property := h }
[PROOFSTEP]
exact h.symm
