[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
P Q : Presheaf C X
f g : P ⟶ Q
w : ∀ (U : Opens ↑X), NatTrans.app f (op U) = NatTrans.app g (op U)
⊢ f = g
[PROOFSTEP]
apply NatTrans.ext
[GOAL]
case app
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
P Q : Presheaf C X
f g : P ⟶ Q
w : ∀ (U : Opens ↑X), NatTrans.app f (op U) = NatTrans.app g (op U)
⊢ f.app = g.app
[PROOFSTEP]
ext U
[GOAL]
case app.h
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
P Q : Presheaf C X
f g : P ⟶ Q
w : ∀ (U : Opens ↑X), NatTrans.app f (op U) = NatTrans.app g (op U)
U : (Opens ↑X)ᵒᵖ
⊢ NatTrans.app f U = NatTrans.app g U
[PROOFSTEP]
induction U with
| _ U => ?_
[GOAL]
case app.h
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
P Q : Presheaf C X
f g : P ⟶ Q
w : ∀ (U : Opens ↑X), NatTrans.app f (op U) = NatTrans.app g (op U)
U : (Opens ↑X)ᵒᵖ
⊢ NatTrans.app f U = NatTrans.app g U
[PROOFSTEP]
induction U with
| _ U => ?_
[GOAL]
case app.h.h
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
P Q : Presheaf C X
f g : P ⟶ Q
w : ∀ (U : Opens ↑X), NatTrans.app f (op U) = NatTrans.app g (op U)
U : Opens ↑X
⊢ NatTrans.app f (op U) = NatTrans.app g (op U)
[PROOFSTEP]
apply w
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
v w x y z : Opens ↑X
h₀ : v ≤ x
h₁ : x ≤ z ⊓ w
h₂ : x ≤ y ⊓ z
⊢ v ≤ y
[PROOFSTEP]
restrict_tac
[GOAL]
C✝ : Type u
inst✝² : Category.{v, u} C✝
X : TopCat
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : ConcreteCategory C
F : Presheaf C X
U V W : Opens ↑X
e₁ : U ≤ V
e₂ : V ≤ W
x : (forget C).obj (F.obj (op W))
⊢ x |_ V |_ U = x |_ U
[PROOFSTEP]
delta restrictOpen restrict
[GOAL]
C✝ : Type u
inst✝² : Category.{v, u} C✝
X : TopCat
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : ConcreteCategory C
F : Presheaf C X
U V W : Opens ↑X
e₁ : U ≤ V
e₂ : V ≤ W
x : (forget C).obj (F.obj (op W))
⊢ ↑(F.map (homOfLE (_ : ∀ ⦃a : ↑X⦄, a ∈ ↑U → a ∈ ↑V)).op) (↑(F.map (homOfLE (_ : ∀ ⦃a : ↑X⦄, a ∈ ↑V → a ∈ ↑W)).op) x) =
    ↑(F.map (homOfLE (_ : ∀ ⦃a : ↑X⦄, a ∈ ↑U → a ∈ ↑W)).op) x
[PROOFSTEP]
rw [← comp_apply, ← Functor.map_comp]
[GOAL]
C✝ : Type u
inst✝² : Category.{v, u} C✝
X : TopCat
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : ConcreteCategory C
F : Presheaf C X
U V W : Opens ↑X
e₁ : U ≤ V
e₂ : V ≤ W
x : (forget C).obj (F.obj (op W))
⊢ ↑(F.map ((homOfLE (_ : ∀ ⦃a : ↑X⦄, a ∈ ↑V → a ∈ ↑W)).op ≫ (homOfLE (_ : ∀ ⦃a : ↑X⦄, a ∈ ↑U → a ∈ ↑V)).op)) x =
    ↑(F.map (homOfLE (_ : ∀ ⦃a : ↑X⦄, a ∈ ↑U → a ∈ ↑W)).op) x
[PROOFSTEP]
rfl
[GOAL]
C✝ : Type u
inst✝² : Category.{v, u} C✝
X : TopCat
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : ConcreteCategory C
F G : Presheaf C X
e : F ⟶ G
U V : Opens ↑X
h : U ≤ V
x : (forget C).obj (F.obj (op V))
⊢ ↑(NatTrans.app e (op U)) (x |_ U) = ↑(NatTrans.app e (op V)) x |_ U
[PROOFSTEP]
delta restrictOpen restrict
[GOAL]
C✝ : Type u
inst✝² : Category.{v, u} C✝
X : TopCat
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : ConcreteCategory C
F G : Presheaf C X
e : F ⟶ G
U V : Opens ↑X
h : U ≤ V
x : (forget C).obj (F.obj (op V))
⊢ ↑(NatTrans.app e (op U)) (↑(F.map (homOfLE (_ : ∀ ⦃a : ↑X⦄, a ∈ ↑U → a ∈ ↑V)).op) x) =
    ↑(G.map (homOfLE (_ : ∀ ⦃a : ↑X⦄, a ∈ ↑U → a ∈ ↑V)).op) (↑(NatTrans.app e (op V)) x)
[PROOFSTEP]
rw [← comp_apply, NatTrans.naturality, comp_apply]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
⊢ f _* ℱ = g _* ℱ
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ (Opens.map f).op.obj U ⟶ (Opens.map g).op.obj U
[PROOFSTEP]
dsimp [Functor.op]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ op ((Opens.map f).obj U.unop) ⟶ op ((Opens.map g).obj U.unop)
[PROOFSTEP]
apply Quiver.Hom.op
[GOAL]
case f
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ (Opens.map g).obj U.unop ⟶ (Opens.map f).obj U.unop
[PROOFSTEP]
apply eqToHom
[GOAL]
case f.p
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ (Opens.map g).obj U.unop = (Opens.map f).obj U.unop
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ NatTrans.app (pushforwardEq h ℱ).hom U =
    ℱ.map (id (eqToHom (_ : (Opens.map g).obj U.unop = (Opens.map f).obj U.unop)).op)
[PROOFSTEP]
simp [pushforwardEq]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ (Opens.map f).op.obj U = (Opens.map g).op.obj U
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ NatTrans.app (eqToHom (_ : f _* ℱ = g _* ℱ)) U = ℱ.map (eqToHom (_ : (Opens.map f).op.obj U = (Opens.map g).op.obj U))
[PROOFSTEP]
rw [eqToHom_app, eqToHom_map]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C X
U : Opens ↑Y
⊢ NatTrans.app (pushforwardEq (_ : f = f) ℱ).hom (op U) = 𝟙 ((f _* ℱ).obj (op U))
[PROOFSTEP]
dsimp [pushforwardEq]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C X
U : Opens ↑Y
⊢ ℱ.map (𝟙 (op ((Opens.map f).obj U))) = 𝟙 (ℱ.obj (op ((Opens.map f).obj U)))
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ℱ : Presheaf C X
⊢ 𝟙 X _* ℱ = ℱ
[PROOFSTEP]
unfold pushforwardObj
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ℱ : Presheaf C X
⊢ (Opens.map (𝟙 X)).op ⋙ ℱ = ℱ
[PROOFSTEP]
rw [Opens.map_id_eq]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ℱ : Presheaf C X
⊢ (𝟭 (Opens ↑X)).op ⋙ ℱ = ℱ
[PROOFSTEP]
erw [Functor.id_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ℱ : Presheaf C X
U : Set ↑X
p : IsOpen U
⊢ NatTrans.app (id ℱ).hom (op { carrier := U, is_open' := p }) = ℱ.map (𝟙 (op { carrier := U, is_open' := p }))
[PROOFSTEP]
dsimp [id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ℱ : Presheaf C X
U : Set ↑X
p : IsOpen U
⊢ NatTrans.app (whiskerRight (NatTrans.op (Opens.mapId X).inv) ℱ ≫ (Functor.leftUnitor ℱ).hom)
      (op { carrier := U, is_open' := p }) =
    ℱ.map (𝟙 (op { carrier := U, is_open' := p }))
[PROOFSTEP]
simp [CategoryStruct.comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ℱ : Presheaf C X
U : (Opens ↑X)ᵒᵖ
⊢ NatTrans.app (id ℱ).hom U = ℱ.map (eqToHom (_ : (Opens.map (𝟙 X)).op.obj U = U))
[PROOFSTEP]
induction U
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ℱ : Presheaf C X
X✝ : Opens ↑X
⊢ NatTrans.app (id ℱ).hom (op X✝) = ℱ.map (eqToHom (_ : (Opens.map (𝟙 X)).op.obj (op X✝) = op X✝))
[PROOFSTEP]
apply id_hom_app'
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ℱ : Presheaf C X
U : Set ↑X
p : IsOpen U
⊢ NatTrans.app (id ℱ).inv (op { carrier := U, is_open' := p }) = ℱ.map (𝟙 (op { carrier := U, is_open' := p }))
[PROOFSTEP]
dsimp [id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ℱ : Presheaf C X
U : Set ↑X
p : IsOpen U
⊢ NatTrans.app ((Functor.leftUnitor ℱ).inv ≫ whiskerRight (NatTrans.op (Opens.mapId X).hom) ℱ)
      (op { carrier := U, is_open' := p }) =
    ℱ.map (𝟙 (op { carrier := U, is_open' := p }))
[PROOFSTEP]
simp [CategoryStruct.comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ℱ : Presheaf C X
Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
U : (Opens ↑Z)ᵒᵖ
⊢ NatTrans.app (comp ℱ f g).hom U = 𝟙 (((f ≫ g) _* ℱ).obj U)
[PROOFSTEP]
simp [comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ℱ : Presheaf C X
Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
U : (Opens ↑Z)ᵒᵖ
⊢ NatTrans.app (comp ℱ f g).inv U = 𝟙 ((g _* (f _* ℱ)).obj U)
[PROOFSTEP]
simp [comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ℱ 𝒢 : Presheaf C X
α : ℱ ⟶ 𝒢
x✝¹ x✝ : (Opens ↑Y)ᵒᵖ
i : x✝¹ ⟶ x✝
⊢ (f _* ℱ).map i ≫ (fun U => NatTrans.app α ((Opens.map f).op.obj U)) x✝ =
    (fun U => NatTrans.app α ((Opens.map f).op.obj U)) x✝¹ ≫ (f _* 𝒢).map i
[PROOFSTEP]
erw [α.naturality]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ℱ 𝒢 : Presheaf C X
α : ℱ ⟶ 𝒢
x✝¹ x✝ : (Opens ↑Y)ᵒᵖ
i : x✝¹ ⟶ x✝
⊢ NatTrans.app α ((Opens.map f).op.obj x✝¹) ≫ 𝒢.map ((Opens.map f).op.map i) =
    (fun U => NatTrans.app α ((Opens.map f).op.obj U)) x✝¹ ≫ (f _* 𝒢).map i
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
⊢ (pullbackObj f ℱ).obj (op U) ≅ ℱ.obj (op { carrier := ↑f '' ↑U, is_open' := H })
[PROOFSTEP]
let x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (@homOfLE _ _ _ ((Opens.map f).obj ⟨_, H⟩) (Set.image_preimage.le_u_l _)).op
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
⊢ (pullbackObj f ℱ).obj (op U) ≅ ℱ.obj (op { carrier := ↑f '' ↑U, is_open' := H })
[PROOFSTEP]
have hx : IsTerminal x :=
  { lift := fun s ↦ by
      fapply CostructuredArrow.homMk
      change op (unop _) ⟶ op (⟨_, H⟩ : Opens _)
      · refine' (homOfLE _).op
        apply (Set.image_subset f s.pt.hom.unop.le).trans
        exact Set.image_preimage.l_u_le (SetLike.coe s.pt.left.unop)
      ·
        simp
          -- porting note : add `fac`, `uniq` manually
    fac := fun _ _ => by ext; simp
    uniq := fun _ _ _ => by ext; simp }
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
s : Cone (Functor.empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ s.pt ⟶ (asEmptyCone x).pt
[PROOFSTEP]
fapply CostructuredArrow.homMk
[GOAL]
case g
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
s : Cone (Functor.empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ s.pt.left ⟶ (asEmptyCone x).pt.left
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
s : Cone (Functor.empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ autoParam ((Opens.map f).op.map ?g ≫ (asEmptyCone x).pt.hom = s.pt.hom) _auto✝
[PROOFSTEP]
change op (unop _) ⟶ op (⟨_, H⟩ : Opens _)
[GOAL]
case g
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
s : Cone (Functor.empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ op s.pt.1.unop ⟶ op { carrier := ↑f '' ↑U, is_open' := H }
[PROOFSTEP]
refine' (homOfLE _).op
[GOAL]
case g
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
s : Cone (Functor.empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ { carrier := ↑f '' ↑U, is_open' := H } ≤ s.pt.1.unop
[PROOFSTEP]
apply (Set.image_subset f s.pt.hom.unop.le).trans
[GOAL]
case g
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
s : Cone (Functor.empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ ↑f '' ↑((Opens.map f).op.obj s.pt.left).unop ⊆ ↑s.pt.1.unop
[PROOFSTEP]
exact Set.image_preimage.l_u_le (SetLike.coe s.pt.left.unop)
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
s : Cone (Functor.empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ autoParam
    ((Opens.map f).op.map
          (let_fun this := (homOfLE (_ : ↑f '' ↑((Functor.fromPUnit (op U)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op;
          this) ≫
        (asEmptyCone x).pt.hom =
      s.pt.hom)
    _auto✝
[PROOFSTEP]
simp
  -- porting note : add `fac`, `uniq` manually
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
x✝¹ : Cone (Functor.empty (CostructuredArrow (Opens.map f).op (op U)))
x✝ : Discrete PEmpty
⊢ (fun s =>
          CostructuredArrow.homMk
            (let_fun this := (homOfLE (_ : ↑f '' ↑((Functor.fromPUnit (op U)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op;
            this))
        x✝¹ ≫
      NatTrans.app (asEmptyCone x).π x✝ =
    NatTrans.app x✝¹.π x✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
x✝¹ : Cone (Functor.empty (CostructuredArrow (Opens.map f).op (op U)))
x✝ : Discrete PEmpty
⊢ ((fun s =>
            CostructuredArrow.homMk
              (let_fun this :=
                (homOfLE (_ : ↑f '' ↑((Functor.fromPUnit (op U)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op;
              this))
          x✝¹ ≫
        NatTrans.app (asEmptyCone x).π x✝).left =
    (NatTrans.app x✝¹.π x✝).left
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
x✝² : Cone (Functor.empty (CostructuredArrow (Opens.map f).op (op U)))
x✝¹ : x✝².pt ⟶ (asEmptyCone x).pt
x✝ : ∀ (j : Discrete PEmpty), x✝¹ ≫ NatTrans.app (asEmptyCone x).π j = NatTrans.app x✝².π j
⊢ x✝¹ =
    (fun s =>
        CostructuredArrow.homMk
          (let_fun this := (homOfLE (_ : ↑f '' ↑((Functor.fromPUnit (op U)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op;
          this))
      x✝²
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
x✝² : Cone (Functor.empty (CostructuredArrow (Opens.map f).op (op U)))
x✝¹ : x✝².pt ⟶ (asEmptyCone x).pt
x✝ : ∀ (j : Discrete PEmpty), x✝¹ ≫ NatTrans.app (asEmptyCone x).π j = NatTrans.app x✝².π j
⊢ x✝¹.left =
    ((fun s =>
          CostructuredArrow.homMk
            (let_fun this := (homOfLE (_ : ↑f '' ↑((Functor.fromPUnit (op U)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op;
            this))
        x✝²).left
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (↑f '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (homOfLE (_ : ↑U ≤ (fun a => ↑f a) ⁻¹' ((fun a => ↑f a) '' ↑U))).op
hx : IsTerminal x
⊢ (pullbackObj f ℱ).obj (op U) ≅ ℱ.obj (op { carrier := ↑f '' ↑U, is_open' := H })
[PROOFSTEP]
exact IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) (colimitOfDiagramTerminal hx _)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U : (Opens ↑Y)ᵒᵖ
⊢ IsOpen (↑(𝟙 Y) '' ↑U.unop)
[PROOFSTEP]
simpa using U.unop.2
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U : (Opens ↑Y)ᵒᵖ
⊢ op { carrier := ↑(𝟙 Y) '' ↑U.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) } = U
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U V : (Opens ↑Y)ᵒᵖ
i : U ⟶ V
⊢ (pullbackObj (𝟙 Y) ℱ).map i ≫
      ((fun U =>
            pullbackObjObjOfImageOpen (𝟙 Y) ℱ U.unop (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) ≪≫
              ℱ.mapIso
                (eqToIso (_ : op { carrier := ↑(𝟙 Y) '' ↑U.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) } = U)))
          V).hom =
    ((fun U =>
            pullbackObjObjOfImageOpen (𝟙 Y) ℱ U.unop (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) ≪≫
              ℱ.mapIso
                (eqToIso (_ : op { carrier := ↑(𝟙 Y) '' ↑U.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) } = U)))
          U).hom ≫
      ℱ.map i
[PROOFSTEP]
simp only [pullbackObj_obj]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U V : (Opens ↑Y)ᵒᵖ
i : U ⟶ V
⊢ (pullbackObj (𝟙 Y) ℱ).map i ≫
      (pullbackObjObjOfImageOpen (𝟙 Y) ℱ V.unop (_ : IsOpen (↑(𝟙 Y) '' ↑V.unop)) ≪≫
          ℱ.mapIso
            (eqToIso (_ : op { carrier := ↑(𝟙 Y) '' ↑V.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑V.unop)) } = V))).hom =
    (pullbackObjObjOfImageOpen (𝟙 Y) ℱ U.unop (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) ≪≫
          ℱ.mapIso
            (eqToIso (_ : op { carrier := ↑(𝟙 Y) '' ↑U.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) } = U))).hom ≫
      ℱ.map i
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U V : (Opens ↑Y)ᵒᵖ
i : U ⟶ V
j✝ : CostructuredArrow (Opens.map (𝟙 Y)).op U
⊢ colimit.ι (Lan.diagram (Opens.map (𝟙 Y)).op ℱ U) j✝ ≫
      (pullbackObj (𝟙 Y) ℱ).map i ≫
        (pullbackObjObjOfImageOpen (𝟙 Y) ℱ V.unop (_ : IsOpen (↑(𝟙 Y) '' ↑V.unop)) ≪≫
            ℱ.mapIso
              (eqToIso
                (_ : op { carrier := ↑(𝟙 Y) '' ↑V.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑V.unop)) } = V))).hom =
    colimit.ι (Lan.diagram (Opens.map (𝟙 Y)).op ℱ U) j✝ ≫
      (pullbackObjObjOfImageOpen (𝟙 Y) ℱ U.unop (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) ≪≫
            ℱ.mapIso
              (eqToIso
                (_ : op { carrier := ↑(𝟙 Y) '' ↑U.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) } = U))).hom ≫
        ℱ.map i
[PROOFSTEP]
simp only [Functor.comp_obj, CostructuredArrow.proj_obj, pullbackObj_map, Iso.trans_hom, Functor.mapIso_hom,
  eqToIso.hom, Category.assoc]
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U V : (Opens ↑Y)ᵒᵖ
i : U ⟶ V
j✝ : CostructuredArrow (Opens.map (𝟙 Y)).op U
⊢ colimit.ι (Lan.diagram (Opens.map (𝟙 Y)).op ℱ U) j✝ ≫
      colimit.pre (Lan.diagram (Opens.map (𝟙 Y)).op ℱ V) (CostructuredArrow.map i) ≫
        (pullbackObjObjOfImageOpen (𝟙 Y) ℱ V.unop (_ : IsOpen (↑(𝟙 Y) '' ↑V.unop))).hom ≫
          ℱ.map (eqToHom (_ : op { carrier := ↑(𝟙 Y) '' ↑V.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑V.unop)) } = V)) =
    colimit.ι (Lan.diagram (Opens.map (𝟙 Y)).op ℱ U) j✝ ≫
      (pullbackObjObjOfImageOpen (𝟙 Y) ℱ U.unop (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop))).hom ≫
        ℱ.map (eqToHom (_ : op { carrier := ↑(𝟙 Y) '' ↑U.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) } = U)) ≫
          ℱ.map i
[PROOFSTEP]
erw [colimit.pre_desc_assoc, colimit.ι_desc_assoc, colimit.ι_desc_assoc]
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U V : (Opens ↑Y)ᵒᵖ
i : U ⟶ V
j✝ : CostructuredArrow (Opens.map (𝟙 Y)).op U
⊢ NatTrans.app
        (Cocone.whisker (CostructuredArrow.map i)
            (coconeOfDiagramTerminal
              (IsLimit.mk fun s =>
                CostructuredArrow.homMk
                  (let_fun this :=
                    (homOfLE (_ : ↑(𝟙 Y) '' ↑((Functor.fromPUnit (op V.unop)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op;
                  this))
              (Lan.diagram (Opens.map (𝟙 Y)).op ℱ (op V.unop)))).ι
        j✝ ≫
      ℱ.map (eqToHom (_ : op { carrier := ↑(𝟙 Y) '' ↑V.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑V.unop)) } = V)) =
    NatTrans.app
        (coconeOfDiagramTerminal
            (IsLimit.mk fun s =>
              CostructuredArrow.homMk
                (let_fun this :=
                  (homOfLE (_ : ↑(𝟙 Y) '' ↑((Functor.fromPUnit (op U.unop)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op;
                this))
            (Lan.diagram (Opens.map (𝟙 Y)).op ℱ (op U.unop))).ι
        j✝ ≫
      ℱ.map (eqToHom (_ : op { carrier := ↑(𝟙 Y) '' ↑U.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) } = U)) ≫
        ℱ.map i
[PROOFSTEP]
dsimp
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U V : (Opens ↑Y)ᵒᵖ
i : U ⟶ V
j✝ : CostructuredArrow (Opens.map (𝟙 Y)).op U
⊢ ℱ.map
        (IsTerminal.from
            (IsLimit.mk fun s =>
              CostructuredArrow.homMk
                (homOfLE (_ : ↑(𝟙 Y) '' ↑((Functor.fromPUnit (op V.unop)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op)
            ((CostructuredArrow.map i).obj j✝)).left ≫
      ℱ.map (eqToHom (_ : op { carrier := ↑(𝟙 Y) '' ↑V.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑V.unop)) } = V)) =
    ℱ.map
        (IsTerminal.from
            (IsLimit.mk fun s =>
              CostructuredArrow.homMk
                (homOfLE (_ : ↑(𝟙 Y) '' ↑((Functor.fromPUnit (op U.unop)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op)
            j✝).left ≫
      ℱ.map (eqToHom (_ : op { carrier := ↑(𝟙 Y) '' ↑U.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) } = U)) ≫
        ℱ.map i
[PROOFSTEP]
simp only [← ℱ.map_comp]
  -- Porting note : `congr` does not work, but `congr 1` does
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U V : (Opens ↑Y)ᵒᵖ
i : U ⟶ V
j✝ : CostructuredArrow (Opens.map (𝟙 Y)).op U
⊢ ℱ.map
      ((IsTerminal.from
            (IsLimit.mk fun s =>
              CostructuredArrow.homMk
                (homOfLE (_ : ↑(𝟙 Y) '' ↑((Functor.fromPUnit (op V.unop)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op)
            ((CostructuredArrow.map i).obj j✝)).left ≫
        eqToHom (_ : op { carrier := ↑(𝟙 Y) '' ↑V.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑V.unop)) } = V)) =
    ℱ.map
      ((IsTerminal.from
            (IsLimit.mk fun s =>
              CostructuredArrow.homMk
                (homOfLE (_ : ↑(𝟙 Y) '' ↑((Functor.fromPUnit (op U.unop)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op)
            j✝).left ≫
        eqToHom (_ : op { carrier := ↑(𝟙 Y) '' ↑U.unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑U.unop)) } = U) ≫ i)
[PROOFSTEP]
congr 1
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U : Opens ↑Y
⊢ (Opens.map (𝟙 Y)).op.obj (op U) = op U
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U : Opens ↑Y
⊢ NatTrans.app (id ℱ).inv (op U) =
    colimit.ι (Lan.diagram (Opens.map (𝟙 Y)).op ℱ (op U))
      (CostructuredArrow.mk (eqToHom (_ : (Opens.map (𝟙 Y)).op.obj (op U) = op U)))
[PROOFSTEP]
rw [← Category.id_comp ((id ℱ).inv.app (op U)), ← NatIso.app_inv, Iso.comp_inv_eq]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U : Opens ↑Y
⊢ 𝟙 (ℱ.obj (op U)) =
    colimit.ι (Lan.diagram (Opens.map (𝟙 Y)).op ℱ (op U))
        (CostructuredArrow.mk (eqToHom (_ : (Opens.map (𝟙 Y)).op.obj (op U) = op U))) ≫
      ((id ℱ).app (op U)).hom
[PROOFSTEP]
dsimp [id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U : Opens ↑Y
⊢ 𝟙 (ℱ.obj (op U)) =
    colimit.ι (Lan.diagram (Opens.map (𝟙 Y)).op ℱ (op U)) (CostructuredArrow.mk (𝟙 (op ((Opens.map (𝟙 Y)).obj U)))) ≫
      colimit.desc (Lan.diagram (Opens.map (𝟙 Y)).op ℱ (op U))
          (coconeOfDiagramTerminal
            (IsLimit.mk fun s =>
              CostructuredArrow.homMk
                (homOfLE (_ : ↑(𝟙 Y) '' ↑((Functor.fromPUnit (op U)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op)
            (Lan.diagram (Opens.map (𝟙 Y)).op ℱ (op U))) ≫
        ℱ.map
          (eqToHom
            (_ : op { carrier := ↑(𝟙 Y) '' ↑(op U).unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑(op U).unop)) } = op U))
[PROOFSTEP]
erw [colimit.ι_desc_assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U : Opens ↑Y
⊢ 𝟙 (ℱ.obj (op U)) =
    NatTrans.app
        (coconeOfDiagramTerminal
            (IsLimit.mk fun s =>
              CostructuredArrow.homMk
                (homOfLE (_ : ↑(𝟙 Y) '' ↑((Functor.fromPUnit (op U)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op)
            (Lan.diagram (Opens.map (𝟙 Y)).op ℱ (op U))).ι
        (CostructuredArrow.mk (𝟙 (op ((Opens.map (𝟙 Y)).obj U)))) ≫
      ℱ.map
        (eqToHom
          (_ : op { carrier := ↑(𝟙 Y) '' ↑(op U).unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑(op U).unop)) } = op U))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U : Opens ↑Y
⊢ 𝟙 (ℱ.obj (op U)) =
    ℱ.map
        (IsTerminal.from
            (IsLimit.mk fun s =>
              CostructuredArrow.homMk
                (homOfLE (_ : ↑(𝟙 Y) '' ↑((Functor.fromPUnit (op U)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op)
            (CostructuredArrow.mk (𝟙 (op ((Opens.map (𝟙 Y)).obj U))))).left ≫
      ℱ.map
        (eqToHom
          (_ : op { carrier := ↑(𝟙 Y) '' ↑(op U).unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑(op U).unop)) } = op U))
[PROOFSTEP]
rw [← ℱ.map_comp, ← ℱ.map_id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
ℱ : Presheaf C Y
U : Opens ↑Y
⊢ ℱ.map (𝟙 (op U)) =
    ℱ.map
      ((IsTerminal.from
            (IsLimit.mk fun s =>
              CostructuredArrow.homMk
                (homOfLE (_ : ↑(𝟙 Y) '' ↑((Functor.fromPUnit (op U)).obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op)
            (CostructuredArrow.mk (𝟙 (op ((Opens.map (𝟙 Y)).obj U))))).left ≫
        eqToHom
          (_ : op { carrier := ↑(𝟙 Y) '' ↑(op U).unop, is_open' := (_ : IsOpen (↑(𝟙 Y) '' ↑(op U).unop)) } = op U))
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
⊢ pushforward C (𝟙 X) = 𝟭 (Presheaf C X)
[PROOFSTEP]
apply CategoryTheory.Functor.ext
[GOAL]
case h_map
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
⊢ autoParam
    (∀ (X_1 Y : Presheaf C X) (f : X_1 ⟶ Y),
      (pushforward C (𝟙 X)).map f =
        eqToHom (_ : ?F.obj X_1 = ?G.obj X_1) ≫
          (𝟭 (Presheaf C X)).map f ≫ eqToHom (_ : (𝟭 (Presheaf C X)).obj Y = (pushforward C (𝟙 X)).obj Y))
    _auto✝
[PROOFSTEP]
intros a b f
[GOAL]
case h_map
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
a b : Presheaf C X
f : a ⟶ b
⊢ (pushforward C (𝟙 X)).map f =
    eqToHom (_ : ?F.obj a = ?G.obj a) ≫
      (𝟭 (Presheaf C X)).map f ≫ eqToHom (_ : (𝟭 (Presheaf C X)).obj b = (pushforward C (𝟙 X)).obj b)
[PROOFSTEP]
ext U
[GOAL]
case h_map.w
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
a b : Presheaf C X
f : a ⟶ b
U : Opens ↑X
⊢ NatTrans.app ((pushforward C (𝟙 X)).map f) (op U) =
    NatTrans.app
      (eqToHom (_ : ?F.obj a = ?G.obj a) ≫
        (𝟭 (Presheaf C X)).map f ≫ eqToHom (_ : (𝟭 (Presheaf C X)).obj b = (pushforward C (𝟙 X)).obj b))
      (op U)
[PROOFSTEP]
erw [NatTrans.congr f (Opens.op_map_id_obj (op U))]
[GOAL]
case h_map.w
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
a b : Presheaf C X
f : a ⟶ b
U : Opens ↑X
⊢ a.map (eqToHom (_ : (Opens.map (𝟙 X)).op.obj (op U) = op U)) ≫
      NatTrans.app f (op U) ≫ b.map (eqToHom (_ : op U = (Opens.map (𝟙 X)).op.obj (op U))) =
    NatTrans.app
      (eqToHom (_ : ?F.obj a = ?G.obj a) ≫
        (𝟭 (Presheaf C X)).map f ≫ eqToHom (_ : (𝟭 (Presheaf C X)).obj b = (pushforward C (𝟙 X)).obj b))
      (op U)
case h_obj
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
⊢ ∀ (X_1 : Presheaf C X), (pushforward C (𝟙 X)).obj X_1 = (𝟭 (Presheaf C X)).obj X_1
[PROOFSTEP]
simp only [Functor.op_obj, eqToHom_refl, CategoryTheory.Functor.map_id, Category.comp_id, Category.id_comp,
  Functor.id_obj, Functor.id_map]
[GOAL]
case h_obj
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
⊢ ∀ (X_1 : Presheaf C X), (pushforward C (𝟙 X)).obj X_1 = (𝟭 (Presheaf C X)).obj X_1
[PROOFSTEP]
apply Pushforward.id_eq
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C X
𝒢 : Presheaf C Y
H₂ : H₁.hom _* ℱ ⟶ 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ U = (Opens.map H₁.hom).op.obj (op ((Opens.map H₁.inv).obj U.unop))
[PROOFSTEP]
simp [Opens.map, Set.preimage_preimage]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C X
𝒢 : Presheaf C Y
H₂ : H₁.hom _* ℱ ⟶ 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ NatTrans.app (toPushforwardOfIso H₁ H₂) U =
    ℱ.map
        (eqToHom
          (_ :
            U =
              op
                {
                  carrier :=
                    ↑H₁.hom ⁻¹'
                      ↑(op { carrier := ↑H₁.inv ⁻¹' ↑U.unop, is_open' := (_ : IsOpen (↑H₁.inv ⁻¹' ↑U.unop)) }).unop,
                  is_open' :=
                    (_ :
                      IsOpen
                        (↑H₁.hom ⁻¹'
                          ↑(op
                                { carrier := ↑H₁.inv ⁻¹' ↑U.unop,
                                  is_open' := (_ : IsOpen (↑H₁.inv ⁻¹' ↑U.unop)) }).unop)) })) ≫
      NatTrans.app H₂ (op ((Opens.map H₁.inv).obj U.unop))
[PROOFSTEP]
delta toPushforwardOfIso
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C X
𝒢 : Presheaf C Y
H₂ : H₁.hom _* ℱ ⟶ 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ NatTrans.app (↑(Adjunction.homEquiv (Equivalence.toAdjunction (presheafEquivOfIso C H₁)) ℱ 𝒢) H₂) U =
    ℱ.map
        (eqToHom
          (_ :
            U =
              op
                {
                  carrier :=
                    ↑H₁.hom ⁻¹'
                      ↑(op { carrier := ↑H₁.inv ⁻¹' ↑U.unop, is_open' := (_ : IsOpen (↑H₁.inv ⁻¹' ↑U.unop)) }).unop,
                  is_open' :=
                    (_ :
                      IsOpen
                        (↑H₁.hom ⁻¹'
                          ↑(op
                                { carrier := ↑H₁.inv ⁻¹' ↑U.unop,
                                  is_open' := (_ : IsOpen (↑H₁.inv ⁻¹' ↑U.unop)) }).unop)) })) ≫
      NatTrans.app H₂ (op ((Opens.map H₁.inv).obj U.unop))
[PROOFSTEP]
simp only [pushforwardObj_obj, Functor.op_obj, Equivalence.toAdjunction, Adjunction.homEquiv_unit, Functor.id_obj,
  Functor.comp_obj, Adjunction.mkOfUnitCounit_unit, unop_op, eqToHom_map]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C X
𝒢 : Presheaf C Y
H₂ : H₁.hom _* ℱ ⟶ 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ NatTrans.app (NatTrans.app (Equivalence.unit (presheafEquivOfIso C H₁)) ℱ ≫ (presheafEquivOfIso C H₁).inverse.map H₂)
      U =
    eqToHom (_ : ℱ.obj U = ℱ.obj (op ((Opens.map H₁.hom).obj ((Opens.map H₁.inv).obj U.unop)))) ≫
      NatTrans.app H₂ (op ((Opens.map H₁.inv).obj U.unop))
[PROOFSTEP]
rw [NatTrans.comp_app, presheafEquivOfIso_inverse_map_app, Equivalence.Equivalence_mk'_unit]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C X
𝒢 : Presheaf C Y
H₂ : H₁.hom _* ℱ ⟶ 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ NatTrans.app (NatTrans.app (presheafEquivOfIso C H₁).unitIso.hom ℱ) U ≫
      NatTrans.app H₂ (op ((Opens.map H₁.inv).obj U.unop)) =
    eqToHom (_ : ℱ.obj U = ℱ.obj (op ((Opens.map H₁.hom).obj ((Opens.map H₁.inv).obj U.unop)))) ≫
      NatTrans.app H₂ (op ((Opens.map H₁.inv).obj U.unop))
[PROOFSTEP]
congr 1
[GOAL]
case e_a
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C X
𝒢 : Presheaf C Y
H₂ : H₁.hom _* ℱ ⟶ 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ NatTrans.app (NatTrans.app (presheafEquivOfIso C H₁).unitIso.hom ℱ) U =
    eqToHom (_ : ℱ.obj U = ℱ.obj (op ((Opens.map H₁.hom).obj ((Opens.map H₁.inv).obj U.unop))))
[PROOFSTEP]
simp only [Equivalence.unit, Equivalence.op, CategoryTheory.Equivalence.symm, Opens.mapMapIso, Functor.id_obj,
  Functor.comp_obj, Iso.symm_hom, NatIso.op_inv, Iso.symm_inv, NatTrans.op_app, NatIso.ofComponents_hom_app,
  eqToIso.hom, eqToHom_op, Equivalence.Equivalence_mk'_unitInv, Equivalence.Equivalence_mk'_counitInv, NatIso.op_hom,
  unop_op, op_unop, eqToIso.inv, NatIso.ofComponents_inv_app, eqToHom_unop, ← ℱ.map_comp, eqToHom_trans, eqToHom_map,
  presheafEquivOfIso_unitIso_hom_app_app]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C Y
𝒢 : Presheaf C X
H₂ : ℱ ⟶ H₁.hom _* 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ (Opens.map H₁.hom).op.obj (op ((Opens.map H₁.inv).obj U.unop)) = U
[PROOFSTEP]
simp [Opens.map, Set.preimage_preimage]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C Y
𝒢 : Presheaf C X
H₂ : ℱ ⟶ H₁.hom _* 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ NatTrans.app (pushforwardToOfIso H₁ H₂) U =
    NatTrans.app H₂ (op ((Opens.map H₁.inv).obj U.unop)) ≫
      𝒢.map
        (eqToHom
          (_ :
            op
                {
                  carrier :=
                    ↑H₁.hom ⁻¹'
                      ↑(op { carrier := ↑H₁.inv ⁻¹' ↑U.unop, is_open' := (_ : IsOpen (↑H₁.inv ⁻¹' ↑U.unop)) }).unop,
                  is_open' :=
                    (_ :
                      IsOpen
                        (↑H₁.hom ⁻¹'
                          ↑(op
                                { carrier := ↑H₁.inv ⁻¹' ↑U.unop,
                                  is_open' := (_ : IsOpen (↑H₁.inv ⁻¹' ↑U.unop)) }).unop)) } =
              U))
[PROOFSTEP]
simp [pushforwardToOfIso, Equivalence.toAdjunction, CategoryStruct.comp]


[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