[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
[PROOFSTEP]
have obj_eq :
  ∀ (j : Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
[GOAL]
case obj_eq
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ ∀ (j : CategoryTheory.Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
[PROOFSTEP]
rintro ⟨i⟩
[GOAL]
case obj_eq.single
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
i : ι
⊢ (Pairwise.diagram U ⋙ Opens.map f).obj (Pairwise.single i) =
    (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj (Pairwise.single i)
[PROOFSTEP]
rfl
[GOAL]
case obj_eq.pair
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
a✝¹ a✝ : ι
⊢ (Pairwise.diagram U ⋙ Opens.map f).obj (Pairwise.pair a✝¹ a✝) =
    (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj (Pairwise.pair a✝¹ a✝)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
obj_eq :
  ∀ (j : CategoryTheory.Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
[PROOFSTEP]
refine Functor.hext obj_eq ?_
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
obj_eq :
  ∀ (j : CategoryTheory.Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
⊢ ∀ (X_1 Y_1 : CategoryTheory.Pairwise ι) (f_1 : X_1 ⟶ Y_1),
    HEq ((Pairwise.diagram U ⋙ Opens.map f).map f_1) ((Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).map f_1)
[PROOFSTEP]
intro i j g
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
obj_eq :
  ∀ (j : CategoryTheory.Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
i j : CategoryTheory.Pairwise ι
g : i ⟶ j
⊢ HEq ((Pairwise.diagram U ⋙ Opens.map f).map g) ((Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).map g)
[PROOFSTEP]
apply Subsingleton.helim
[GOAL]
case h₂
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
obj_eq :
  ∀ (j : CategoryTheory.Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
i j : CategoryTheory.Pairwise ι
g : i ⟶ j
⊢ ((Pairwise.diagram U ⋙ Opens.map f).obj i ⟶ (Pairwise.diagram U ⋙ Opens.map f).obj j) =
    ((Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj i ⟶
      (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j)
[PROOFSTEP]
rw [obj_eq, obj_eq]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq ((Opens.map f).mapCocone (Pairwise.cocone U)) (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))
[PROOFSTEP]
unfold Functor.mapCocone Cocones.functoriality
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq
    ((CategoryTheory.Functor.mk
          {
            obj := fun A =>
              { pt := (Opens.map f).obj A.pt, ι := NatTrans.mk fun j => (Opens.map f).map (NatTrans.app A.ι j) },
            map := fun {X_1 Y_1} f_1 => CoconeMorphism.mk ((Opens.map f).map f_1.Hom) }).obj
      (Pairwise.cocone U))
    (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq { pt := (Opens.map f).obj (iSup U), ι := NatTrans.mk fun j => (Opens.map f).map (Pairwise.coconeιApp U j) }
    (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))
[PROOFSTEP]
congr
[GOAL]
case e_5.h
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
case e_6.h
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ (Opens.map f).obj (iSup U) = iSup ((Opens.map f).toPrefunctor.obj ∘ U)
case e_7.e_5.h
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
case e_7.e_6.h.e_a
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ (Opens.map f).obj (iSup U) = iSup ((Opens.map f).toPrefunctor.obj ∘ U)
case e_7.e_7
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq (fun j => (Opens.map f).map (Pairwise.coconeιApp U j)) (Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U))
case e_7.e_8
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram U ⋙ Opens.map f).map f_1 ≫
            (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) Y_1 =
          (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) X_1 ≫
            ((Functor.const (CategoryTheory.Pairwise ι)).obj ((Opens.map f).obj (Pairwise.cocone U).pt)).map f_1)
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).map f_1 ≫
            Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) Y_1 =
          Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) X_1 ≫ 𝟙 (iSup ((Opens.map f).toPrefunctor.obj ∘ U)))
[PROOFSTEP]
iterate 2 rw [map_diagram]; rw [Opens.map_iSup]
[GOAL]
case e_5.h
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
case e_6.h
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ (Opens.map f).obj (iSup U) = iSup ((Opens.map f).toPrefunctor.obj ∘ U)
case e_7.e_5.h
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
case e_7.e_6.h.e_a
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ (Opens.map f).obj (iSup U) = iSup ((Opens.map f).toPrefunctor.obj ∘ U)
case e_7.e_7
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq (fun j => (Opens.map f).map (Pairwise.coconeιApp U j)) (Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U))
case e_7.e_8
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram U ⋙ Opens.map f).map f_1 ≫
            (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) Y_1 =
          (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) X_1 ≫
            ((Functor.const (CategoryTheory.Pairwise ι)).obj ((Opens.map f).obj (Pairwise.cocone U).pt)).map f_1)
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).map f_1 ≫
            Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) Y_1 =
          Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) X_1 ≫ 𝟙 (iSup ((Opens.map f).toPrefunctor.obj ∘ U)))
[PROOFSTEP]
rw [map_diagram]
[GOAL]
case e_6.h
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ (Opens.map f).obj (iSup U) = iSup ((Opens.map f).toPrefunctor.obj ∘ U)
case e_7.e_5.h
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
case e_7.e_6.h.e_a
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ (Opens.map f).obj (iSup U) = iSup ((Opens.map f).toPrefunctor.obj ∘ U)
case e_7.e_7
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq (fun j => (Opens.map f).map (Pairwise.coconeιApp U j)) (Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U))
case e_7.e_8
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram U ⋙ Opens.map f).map f_1 ≫
            (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) Y_1 =
          (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) X_1 ≫
            ((Functor.const (CategoryTheory.Pairwise ι)).obj ((Opens.map f).obj (Pairwise.cocone U).pt)).map f_1)
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).map f_1 ≫
            Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) Y_1 =
          Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) X_1 ≫ 𝟙 (iSup ((Opens.map f).toPrefunctor.obj ∘ U)))
[PROOFSTEP]
rw [Opens.map_iSup]
[GOAL]
case e_7.e_5.h
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
case e_7.e_6.h.e_a
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ (Opens.map f).obj (iSup U) = iSup ((Opens.map f).toPrefunctor.obj ∘ U)
case e_7.e_7
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq (fun j => (Opens.map f).map (Pairwise.coconeιApp U j)) (Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U))
case e_7.e_8
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram U ⋙ Opens.map f).map f_1 ≫
            (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) Y_1 =
          (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) X_1 ≫
            ((Functor.const (CategoryTheory.Pairwise ι)).obj ((Opens.map f).obj (Pairwise.cocone U).pt)).map f_1)
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).map f_1 ≫
            Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) Y_1 =
          Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) X_1 ≫ 𝟙 (iSup ((Opens.map f).toPrefunctor.obj ∘ U)))
[PROOFSTEP]
rw [map_diagram]
[GOAL]
case e_7.e_6.h.e_a
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ (Opens.map f).obj (iSup U) = iSup ((Opens.map f).toPrefunctor.obj ∘ U)
case e_7.e_7
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq (fun j => (Opens.map f).map (Pairwise.coconeιApp U j)) (Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U))
case e_7.e_8
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram U ⋙ Opens.map f).map f_1 ≫
            (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) Y_1 =
          (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) X_1 ≫
            ((Functor.const (CategoryTheory.Pairwise ι)).obj ((Opens.map f).obj (Pairwise.cocone U).pt)).map f_1)
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).map f_1 ≫
            Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) Y_1 =
          Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) X_1 ≫ 𝟙 (iSup ((Opens.map f).toPrefunctor.obj ∘ U)))
[PROOFSTEP]
rw [Opens.map_iSup]
[GOAL]
case e_7.e_7
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq (fun j => (Opens.map f).map (Pairwise.coconeιApp U j)) (Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U))
case e_7.e_8
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram U ⋙ Opens.map f).map f_1 ≫
            (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) Y_1 =
          (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) X_1 ≫
            ((Functor.const (CategoryTheory.Pairwise ι)).obj ((Opens.map f).obj (Pairwise.cocone U).pt)).map f_1)
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).map f_1 ≫
            Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) Y_1 =
          Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) X_1 ≫ 𝟙 (iSup ((Opens.map f).toPrefunctor.obj ∘ U)))
[PROOFSTEP]
apply Subsingleton.helim
[GOAL]
case e_7.e_7.h₂
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ ((X_1 : CategoryTheory.Pairwise ι) →
      (Pairwise.diagram U ⋙ Opens.map f).obj X_1 ⟶
        ((Functor.const (CategoryTheory.Pairwise ι)).obj ((Opens.map f).obj (iSup U))).obj X_1) =
    ((X_1 : CategoryTheory.Pairwise ι) →
      (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj X_1 ⟶
        ((Functor.const (CategoryTheory.Pairwise ι)).obj (iSup ((Opens.map f).toPrefunctor.obj ∘ U))).obj X_1)
case e_7.e_8
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram U ⋙ Opens.map f).map f_1 ≫
            (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) Y_1 =
          (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) X_1 ≫
            ((Functor.const (CategoryTheory.Pairwise ι)).obj ((Opens.map f).obj (Pairwise.cocone U).pt)).map f_1)
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).map f_1 ≫
            Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) Y_1 =
          Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) X_1 ≫ 𝟙 (iSup ((Opens.map f).toPrefunctor.obj ∘ U)))
[PROOFSTEP]
rw [map_diagram, Opens.map_iSup]
[GOAL]
case e_7.e_8
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram U ⋙ Opens.map f).map f_1 ≫
            (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) Y_1 =
          (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) X_1 ≫
            ((Functor.const (CategoryTheory.Pairwise ι)).obj ((Opens.map f).obj (Pairwise.cocone U).pt)).map f_1)
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).map f_1 ≫
            Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) Y_1 =
          Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) X_1 ≫ 𝟙 (iSup ((Opens.map f).toPrefunctor.obj ∘ U)))
[PROOFSTEP]
apply proof_irrel_heq
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
⊢ Nonempty (IsLimit ((f _* F).mapCone (Cocone.op (Pairwise.cocone U))))
[PROOFSTEP]
convert h ((Opens.map f).obj ∘ U) using 2
[GOAL]
case h.e'_1.h.e'_5
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
⊢ (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ F
case h.e'_1.h.e'_6
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ F
⊢ HEq ((f _* F).mapCone (Cocone.op (Pairwise.cocone U)))
    (F.mapCone (Cocone.op (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))))
[PROOFSTEP]
rw [← map_diagram]
[GOAL]
case h.e'_1.h.e'_5
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
⊢ (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram U ⋙ Opens.map f).op ⋙ F
case h.e'_1.h.e'_6
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ F
⊢ HEq ((f _* F).mapCone (Cocone.op (Pairwise.cocone U)))
    (F.mapCone (Cocone.op (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))))
[PROOFSTEP]
rfl
[GOAL]
case h.e'_1.h.e'_6
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ F
⊢ HEq ((f _* F).mapCone (Cocone.op (Pairwise.cocone U)))
    (F.mapCone (Cocone.op (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))))
[PROOFSTEP]
change HEq (Functor.mapCone F ((Opens.map f).mapCocone (Pairwise.cocone U)).op) _
[GOAL]
case h.e'_1.h.e'_6
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ F
⊢ HEq (F.mapCone (Cocone.op ((Opens.map f).mapCocone (Pairwise.cocone U))))
    (F.mapCone (Cocone.op (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))))
[PROOFSTEP]
congr
[GOAL]
case h.e'_1.h.e'_6.e_8.h.e_F
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ F
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
case h.e'_1.h.e'_6.e_9.e_5.h
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ F
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
case h.e'_1.h.e'_6.e_9.e_6
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ F
⊢ HEq ((Opens.map f).mapCocone (Pairwise.cocone U)) (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))
[PROOFSTEP]
iterate 2 rw [map_diagram]
[GOAL]
case h.e'_1.h.e'_6.e_8.h.e_F
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ F
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
case h.e'_1.h.e'_6.e_9.e_5.h
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ F
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
case h.e'_1.h.e'_6.e_9.e_6
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ F
⊢ HEq ((Opens.map f).mapCocone (Pairwise.cocone U)) (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))
[PROOFSTEP]
rw [map_diagram]
[GOAL]
case h.e'_1.h.e'_6.e_9.e_5.h
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ F
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
case h.e'_1.h.e'_6.e_9.e_6
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ F
⊢ HEq ((Opens.map f).mapCocone (Pairwise.cocone U)) (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))
[PROOFSTEP]
rw [map_diagram]
[GOAL]
case h.e'_1.h.e'_6.e_9.e_6
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ F
⊢ HEq ((Opens.map f).mapCocone (Pairwise.cocone U)) (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))
[PROOFSTEP]
apply mapCocone
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
F : Presheaf C X
h : Presheaf.IsSheaf F
⊢ Presheaf.IsSheaf (f _* F)
[PROOFSTEP]
rw [isSheaf_iff_isSheafPairwiseIntersections] at h ⊢
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
⊢ IsSheafPairwiseIntersections (f _* F)
[PROOFSTEP]
exact SheafConditionPairwiseIntersections.pushforward_sheaf_of_sheaf f h


[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
x✝² x✝¹ : Opens α
carrier✝¹ : Set α
is_open'✝¹ : IsOpen carrier✝¹
carrier✝ : Set α
is_open'✝ : IsOpen carrier✝
x✝ : { carrier := carrier✝¹, is_open' := is_open'✝¹ }.carrier = { carrier := carrier✝, is_open' := is_open'✝ }.carrier
⊢ { carrier := carrier✝¹, is_open' := is_open'✝¹ } = { carrier := carrier✝, is_open' := is_open'✝ }
[PROOFSTEP]
congr
[GOAL]
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Sort u_5
s : ι → Opens α
⊢ ↑(⨆ (i : ι), s i) = ⋃ (i : ι), ↑(s i)
[PROOFSTEP]
simp [iSup]
[GOAL]
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Sort u_5
x : α
s : ι → Opens α
⊢ x ∈ iSup s ↔ ∃ i, x ∈ s i
[PROOFSTEP]
rw [← SetLike.mem_coe]
[GOAL]
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Sort u_5
x : α
s : ι → Opens α
⊢ x ∈ ↑(iSup s) ↔ ∃ i, x ∈ s i
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
Us : Set (Opens α)
x : α
⊢ x ∈ sSup Us ↔ ∃ u, u ∈ Us ∧ x ∈ u
[PROOFSTEP]
simp_rw [sSup_eq_iSup, mem_iSup, exists_prop]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
src✝ : CompleteLattice (Opens α) := inferInstanceAs (CompleteLattice (Opens α))
a : Opens α
s : Set (Opens α)
⊢ ↑(a ⊓ sSup s) = ↑(⨆ (b : Opens α) (_ : b ∈ s), a ⊓ b)
[PROOFSTEP]
simp only [coe_inf, coe_iSup, coe_sSup, Set.inter_iUnion₂]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
U V : Opens α
i : U ≤ V
⊢ IsOpen (range (inclusion (_ : ↑U ⊆ ↑V)))
[PROOFSTEP]
rw [Set.range_inclusion i]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
U V : Opens α
i : U ≤ V
⊢ IsOpen {x | ↑x ∈ ↑U}
[PROOFSTEP]
exact U.isOpen.preimage continuous_subtype_val
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
U : Opens α
⊢ ¬Set.Nonempty ↑U ↔ U = ⊥
[PROOFSTEP]
rw [← coe_inj, coe_bot, ← Set.not_nonempty_iff_eq_empty]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
U : Opens α
⊢ U ≠ ⊥ ↔ Set.Nonempty ↑U
[PROOFSTEP]
rw [Ne.def, ← not_nonempty_iff_eq_bot, not_not]
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
α : Type u_5
t : TopologicalSpace α
h : t = ⊤
U : Opens α
⊢ U = ⊥ ∨ U = ⊤
[PROOFSTEP]
subst h
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
α : Type u_5
U : Opens α
⊢ U = ⊥ ∨ U = ⊤
[PROOFSTEP]
letI : TopologicalSpace α := ⊤
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
α : Type u_5
U : Opens α
this : TopologicalSpace α := ⊤
⊢ U = ⊥ ∨ U = ⊤
[PROOFSTEP]
rw [← coe_eq_empty, ← coe_eq_univ, ← isOpen_top_iff]
[GOAL]
ι : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
α : Type u_5
U : Opens α
this : TopologicalSpace α := ⊤
⊢ IsOpen ↑U
[PROOFSTEP]
exact U.2
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
⊢ IsBasis B ↔ ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
⊢ IsBasis B → ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
[PROOFSTEP]
intro h
[GOAL]
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
⊢ (∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U) → IsBasis B
[PROOFSTEP]
intro h
[GOAL]
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
⊢ ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
[PROOFSTEP]
rintro ⟨sU, hU⟩ x hx
[GOAL]
case mp.mk
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
⊢ ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ { carrier := sU, is_open' := hU }
[PROOFSTEP]
rcases h.mem_nhds_iff.mp (IsOpen.mem_nhds hU hx) with ⟨sV, ⟨⟨V, H₁, H₂⟩, hsV⟩⟩
[GOAL]
case mp.mk.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
V : Opens α
H₁ : V ∈ B
H₂ : ↑V = sV
⊢ ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ { carrier := sU, is_open' := hU }
[PROOFSTEP]
refine' ⟨V, H₁, _⟩
[GOAL]
case mp.mk.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
V : Opens α
H₁ : V ∈ B
H₂ : ↑V = sV
⊢ x ∈ V ∧ V ≤ { carrier := sU, is_open' := hU }
[PROOFSTEP]
cases V
[GOAL]
case mp.mk.intro.intro.intro.intro.mk
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
carrier✝ : Set α
is_open'✝ : IsOpen carrier✝
H₁ : { carrier := carrier✝, is_open' := is_open'✝ } ∈ B
H₂ : ↑{ carrier := carrier✝, is_open' := is_open'✝ } = sV
⊢ x ∈ { carrier := carrier✝, is_open' := is_open'✝ } ∧
    { carrier := carrier✝, is_open' := is_open'✝ } ≤ { carrier := sU, is_open' := hU }
[PROOFSTEP]
dsimp at H₂
[GOAL]
case mp.mk.intro.intro.intro.intro.mk
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
carrier✝ : Set α
is_open'✝ : IsOpen carrier✝
H₁ : { carrier := carrier✝, is_open' := is_open'✝ } ∈ B
H₂ : carrier✝ = sV
⊢ x ∈ { carrier := carrier✝, is_open' := is_open'✝ } ∧
    { carrier := carrier✝, is_open' := is_open'✝ } ≤ { carrier := sU, is_open' := hU }
[PROOFSTEP]
subst H₂
[GOAL]
case mp.mk.intro.intro.intro.intro.mk
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
carrier✝ : Set α
is_open'✝ : IsOpen carrier✝
H₁ : { carrier := carrier✝, is_open' := is_open'✝ } ∈ B
hsV : x ∈ carrier✝ ∧ carrier✝ ⊆ sU
⊢ x ∈ { carrier := carrier✝, is_open' := is_open'✝ } ∧
    { carrier := carrier✝, is_open' := is_open'✝ } ≤ { carrier := sU, is_open' := hU }
[PROOFSTEP]
exact hsV
[GOAL]
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
⊢ IsBasis B
[PROOFSTEP]
refine' isTopologicalBasis_of_open_of_nhds _ _
[GOAL]
case mpr.refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
⊢ ∀ (u : Set α), u ∈ SetLike.coe '' B → IsOpen u
[PROOFSTEP]
rintro sU ⟨U, -, rfl⟩
[GOAL]
case mpr.refine'_1.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
U : Opens α
⊢ IsOpen ↑U
[PROOFSTEP]
exact U.2
[GOAL]
case mpr.refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ SetLike.coe '' B ∧ a ∈ v ∧ v ⊆ u
[PROOFSTEP]
intro x sU hx hsU
[GOAL]
case mpr.refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
x : α
sU : Set α
hx : x ∈ sU
hsU : IsOpen sU
⊢ ∃ v, v ∈ SetLike.coe '' B ∧ x ∈ v ∧ v ⊆ sU
[PROOFSTEP]
rcases@h ⟨sU, hsU⟩ x hx with ⟨V, hV, H⟩
[GOAL]
case mpr.refine'_2.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
x : α
sU : Set α
hx : x ∈ sU
hsU : IsOpen sU
V : Opens α
hV : V ∈ B
H : x ∈ V ∧ V ≤ { carrier := sU, is_open' := hsU }
⊢ ∃ v, v ∈ SetLike.coe '' B ∧ x ∈ v ∧ v ⊆ sU
[PROOFSTEP]
exact ⟨V, ⟨V, hV, rfl⟩, H⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
⊢ IsBasis B ↔ ∀ (U : Opens α), ∃ Us, Us ⊆ B ∧ U = sSup Us
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
⊢ IsBasis B → ∀ (U : Opens α), ∃ Us, Us ⊆ B ∧ U = sSup Us
[PROOFSTEP]
intro hB U
[GOAL]
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ∃ Us, Us ⊆ B ∧ U = sSup Us
[PROOFSTEP]
refine ⟨{V : Opens α | V ∈ B ∧ V ≤ U}, fun U hU => hU.left, ext ?_⟩
[GOAL]
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ↑U = ↑(sSup {V | V ∈ B ∧ V ≤ U})
[PROOFSTEP]
rw [coe_sSup, hB.open_eq_sUnion' U.isOpen]
[GOAL]
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ⋃₀ {s | s ∈ SetLike.coe '' B ∧ s ⊆ ↑U} = ⋃ (i : Opens α) (_ : i ∈ {V | V ∈ B ∧ V ≤ U}), ↑i
[PROOFSTEP]
simp_rw [sUnion_eq_biUnion, iUnion, mem_setOf_eq, iSup_and, iSup_image]
[GOAL]
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ⨆ (b : Opens α) (_ : b ∈ B) (_ : ↑b ⊆ ↑U), ↑b = ⨆ (i : Opens α) (_ : i ∈ B) (_ : i ≤ U), ↑i
[PROOFSTEP]
rfl
[GOAL]
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
⊢ (∀ (U : Opens α), ∃ Us, Us ⊆ B ∧ U = sSup Us) → IsBasis B
[PROOFSTEP]
intro h
[GOAL]
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us, Us ⊆ B ∧ U = sSup Us
⊢ IsBasis B
[PROOFSTEP]
rw [isBasis_iff_nbhd]
[GOAL]
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us, Us ⊆ B ∧ U = sSup Us
⊢ ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
[PROOFSTEP]
intro U x hx
[GOAL]
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us, Us ⊆ B ∧ U = sSup Us
U : Opens α
x : α
hx : x ∈ U
⊢ ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
[PROOFSTEP]
rcases h U with ⟨Us, hUs, rfl⟩
[GOAL]
case mpr.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us, Us ⊆ B ∧ U = sSup Us
x : α
Us : Set (Opens α)
hUs : Us ⊆ B
hx : x ∈ sSup Us
⊢ ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ sSup Us
[PROOFSTEP]
rcases mem_sSup.1 hx with ⟨U, Us, xU⟩
[GOAL]
case mpr.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us, Us ⊆ B ∧ U = sSup Us
x : α
Us✝ : Set (Opens α)
hUs : Us✝ ⊆ B
hx : x ∈ sSup Us✝
U : Opens α
Us : U ∈ Us✝
xU : x ∈ U
⊢ ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ sSup Us✝
[PROOFSTEP]
exact ⟨U, hUs Us, xU, le_sSup Us⟩
[GOAL]
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ IsCompact U ∧ IsOpen U ↔ ∃ s, Set.Finite s ∧ U = ⋃ (i : ι) (_ : i ∈ s), ↑(b i)
[PROOFSTEP]
apply isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis fun i : ι => (b i).1
[GOAL]
case hb
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ IsTopologicalBasis (range fun i => (b i).carrier)
[PROOFSTEP]
convert (config := { transparency := .default }) hb
[GOAL]
case h.e'_3
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ (range fun i => (b i).carrier) = SetLike.coe '' range b
[PROOFSTEP]
ext
[GOAL]
case h.e'_3.h
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U x✝ : Set α
⊢ (x✝ ∈ range fun i => (b i).carrier) ↔ x✝ ∈ SetLike.coe '' range b
[PROOFSTEP]
simp
[GOAL]
case hb'
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ ∀ (i : ι), IsCompact (b i).carrier
[PROOFSTEP]
exact hb'
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
⊢ CompleteLattice.IsCompactElement s ↔ IsCompact ↑s
[PROOFSTEP]
rw [isCompact_iff_finite_subcover, CompleteLattice.isCompactElement_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
⊢ (∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1) ↔
    ∀ {ι : Type u_2} (U : ι → Set α),
      (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ (i : ι), U i → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
[PROOFSTEP]
refine' ⟨_, fun H ι U hU => _⟩
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
⊢ (∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1) →
    ∀ {ι : Type u_2} (U : ι → Set α),
      (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ (i : ι), U i → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
[PROOFSTEP]
introv H hU hU'
[GOAL]
case refine'_1
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ (i : ι), U i
⊢ ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
[PROOFSTEP]
obtain ⟨t, ht⟩ := H ι (fun i => ⟨U i, hU i⟩) (by simpa)
[GOAL]
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ (i : ι), U i
⊢ s ≤ ⨆ (i : ι), { carrier := U i, is_open' := (_ : IsOpen (U i)) }
[PROOFSTEP]
simpa
[GOAL]
case refine'_1.intro
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ (i : ι), U i
t : Finset ι
ht : s ≤ Finset.sup t fun i => { carrier := U i, is_open' := (_ : IsOpen (U i)) }
⊢ ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
[PROOFSTEP]
refine' ⟨t, Set.Subset.trans ht _⟩
[GOAL]
case refine'_1.intro
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ (i : ι), U i
t : Finset ι
ht : s ≤ Finset.sup t fun i => { carrier := U i, is_open' := (_ : IsOpen (U i)) }
⊢ ↑(Finset.sup t fun i => { carrier := U i, is_open' := (_ : IsOpen (U i)) }) ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
[PROOFSTEP]
rw [coe_finset_sup, Finset.sup_eq_iSup]
[GOAL]
case refine'_1.intro
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ Finset.sup t s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ (i : ι), U i
t : Finset ι
ht : s ≤ Finset.sup t fun i => { carrier := U i, is_open' := (_ : IsOpen (U i)) }
⊢ ⨆ (a : ι) (_ : a ∈ t), (SetLike.coe ∘ fun i => { carrier := U i, is_open' := (_ : IsOpen (U i)) }) a ⊆
    ⋃ (i : ι) (_ : i ∈ t), U i
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H :
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ (i : ι), U i → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
⊢ ∃ t, s ≤ Finset.sup t U
[PROOFSTEP]
obtain ⟨t, ht⟩ := H (fun i => U i) (fun i => (U i).isOpen) (by simpa using show (s : Set α) ⊆ ↑(iSup U) from hU)
[GOAL]
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H :
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ (i : ι), U i → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
⊢ ↑s ⊆ ⋃ (i : ι), (fun i => ↑(U i)) i
[PROOFSTEP]
simpa using show (s : Set α) ⊆ ↑(iSup U) from hU
[GOAL]
case refine'_2.intro
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H :
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ (i : ι), U i → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(U i)
⊢ ∃ t, s ≤ Finset.sup t U
[PROOFSTEP]
refine' ⟨t, Set.Subset.trans ht _⟩
[GOAL]
case refine'_2.intro
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H :
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ (i : ι), U i → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(U i)
⊢ ⋃ (i : ι) (_ : i ∈ t), ↑(U i) ⊆ ↑(Finset.sup t U)
[PROOFSTEP]
simp only [Set.iUnion_subset_iff]
[GOAL]
case refine'_2.intro
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H :
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ (i : ι), U i → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(U i)
⊢ ∀ (i : ι), i ∈ t → ↑(U i) ⊆ ↑(Finset.sup t U)
[PROOFSTEP]
show ∀ i ∈ t, U i ≤ t.sup U
[GOAL]
case refine'_2.intro
ι✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Opens α
H :
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ (i : ι), U i → ∃ t, ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), ↑(U i)
⊢ ∀ (i : ι), i ∈ t → U i ≤ Finset.sup t U
[PROOFSTEP]
exact fun i => Finset.le_sup
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : C(α, β)
s : Set (Opens β)
⊢ ↑(InfHom.toFun
        {
            toInfHom :=
              { toFun := fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) },
                map_inf' :=
                  (_ :
                    ∀ (a b : Opens β),
                      (fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) }) (a ⊓ b) =
                        (fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) }) (a ⊓ b)) },
            map_top' :=
              (_ :
                InfHom.toFun
                    { toFun := fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) },
                      map_inf' :=
                        (_ :
                          ∀ (a b : Opens β),
                            (fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) }) (a ⊓ b) =
                              (fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) })
                                (a ⊓ b)) }
                    ⊤ =
                  InfHom.toFun
                    { toFun := fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) },
                      map_inf' :=
                        (_ :
                          ∀ (a b : Opens β),
                            (fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) }) (a ⊓ b) =
                              (fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) })
                                (a ⊓ b)) }
                    ⊤) }.toInfHom
        (sSup s)) =
    ↑(sSup
        ({
                toInfHom :=
                  { toFun := fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) },
                    map_inf' :=
                      (_ :
                        ∀ (a b : Opens β),
                          (fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) }) (a ⊓ b) =
                            (fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) }) (a ⊓ b)) },
                map_top' :=
                  (_ :
                    InfHom.toFun
                        { toFun := fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) },
                          map_inf' :=
                            (_ :
                              ∀ (a b : Opens β),
                                (fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) })
                                    (a ⊓ b) =
                                  (fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) })
                                    (a ⊓ b)) }
                        ⊤ =
                      InfHom.toFun
                        { toFun := fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) },
                          map_inf' :=
                            (_ :
                              ∀ (a b : Opens β),
                                (fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) })
                                    (a ⊓ b) =
                                  (fun s => { carrier := ↑f ⁻¹' ↑s, is_open' := (_ : IsOpen (↑f ⁻¹' s.carrier)) })
                                    (a ⊓ b)) }
                        ⊤) }.toInfHom.toFun ''
          s))
[PROOFSTEP]
simp only [coe_sSup, preimage_iUnion, biUnion_image, coe_mk]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α ≃ₜ β
⊢ ∀ {a b : Opens α},
    ↑{ toFun := ↑(comap (Homeomorph.toContinuousMap (Homeomorph.symm f))),
              invFun := ↑(comap (Homeomorph.toContinuousMap f)),
              left_inv :=
                (_ :
                  ∀ (U : Opens α),
                    ↑(comap (Homeomorph.toContinuousMap f))
                        (↑(comap (Homeomorph.toContinuousMap (Homeomorph.symm f))) U) =
                      U),
              right_inv :=
                (_ :
                  ∀ (U : Opens β),
                    ↑(comap (Homeomorph.toContinuousMap (Homeomorph.symm f)))
                        (↑(comap (Homeomorph.toContinuousMap f)) U) =
                      U) }
          a ≤
        ↑{ toFun := ↑(comap (Homeomorph.toContinuousMap (Homeomorph.symm f))),
              invFun := ↑(comap (Homeomorph.toContinuousMap f)),
              left_inv :=
                (_ :
                  ∀ (U : Opens α),
                    ↑(comap (Homeomorph.toContinuousMap f))
                        (↑(comap (Homeomorph.toContinuousMap (Homeomorph.symm f))) U) =
                      U),
              right_inv :=
                (_ :
                  ∀ (U : Opens β),
                    ↑(comap (Homeomorph.toContinuousMap (Homeomorph.symm f)))
                        (↑(comap (Homeomorph.toContinuousMap f)) U) =
                      U) }
          b ↔
      a ≤ b
[PROOFSTEP]
simp only [← SetLike.coe_subset_coe]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α ≃ₜ β
⊢ ∀ {a b : Opens α},
    ↑(↑{ toFun := ↑(comap (Homeomorph.toContinuousMap (Homeomorph.symm f))),
                invFun := ↑(comap (Homeomorph.toContinuousMap f)),
                left_inv :=
                  (_ :
                    ∀ (U : Opens α),
                      ↑(comap (Homeomorph.toContinuousMap f))
                          (↑(comap (Homeomorph.toContinuousMap (Homeomorph.symm f))) U) =
                        U),
                right_inv :=
                  (_ :
                    ∀ (U : Opens β),
                      ↑(comap (Homeomorph.toContinuousMap (Homeomorph.symm f)))
                          (↑(comap (Homeomorph.toContinuousMap f)) U) =
                        U) }
            a) ⊆
        ↑(↑{ toFun := ↑(comap (Homeomorph.toContinuousMap (Homeomorph.symm f))),
                invFun := ↑(comap (Homeomorph.toContinuousMap f)),
                left_inv :=
                  (_ :
                    ∀ (U : Opens α),
                      ↑(comap (Homeomorph.toContinuousMap f))
                          (↑(comap (Homeomorph.toContinuousMap (Homeomorph.symm f))) U) =
                        U),
                right_inv :=
                  (_ :
                    ∀ (U : Opens β),
                      ↑(comap (Homeomorph.toContinuousMap (Homeomorph.symm f)))
                          (↑(comap (Homeomorph.toContinuousMap f)) U) =
                        U) }
            b) ↔
      ↑a ⊆ ↑b
[PROOFSTEP]
exact f.symm.surjective.preimage_subset_preimage_iff


[GOAL]
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst✝¹⁸ : Semiring R
inst✝¹⁷ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁵ : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : AddCommMonoid M₃
inst✝¹² : AddCommMonoid M₄
inst✝¹¹ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : (i : ι) → Module R (M₁' i)
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M₃
inst✝⁶ : Module R M₄
inst✝⁵ : (i : Fin (Nat.succ n)) → TopologicalSpace (M i)
inst✝⁴ : (i : ι) → TopologicalSpace (M₁ i)
inst✝³ : (i : ι) → TopologicalSpace (M₁' i)
inst✝² : TopologicalSpace M₂
inst✝¹ : TopologicalSpace M₃
inst✝ : TopologicalSpace M₄
f✝ f' : ContinuousMultilinearMap R M₁ M₂
f : MultilinearMap R M₁ M₂
hf : Continuous f.toFun
g : MultilinearMap R M₁ M₂
hg : Continuous g.toFun
h : { toMultilinearMap := f, cont := hf }.toMultilinearMap = { toMultilinearMap := g, cont := hg }.toMultilinearMap
⊢ { toMultilinearMap := f, cont := hf } = { toMultilinearMap := g, cont := hg }
[PROOFSTEP]
subst h
[GOAL]
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst✝¹⁸ : Semiring R
inst✝¹⁷ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁵ : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : AddCommMonoid M₃
inst✝¹² : AddCommMonoid M₄
inst✝¹¹ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : (i : ι) → Module R (M₁' i)
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M₃
inst✝⁶ : Module R M₄
inst✝⁵ : (i : Fin (Nat.succ n)) → TopologicalSpace (M i)
inst✝⁴ : (i : ι) → TopologicalSpace (M₁ i)
inst✝³ : (i : ι) → TopologicalSpace (M₁' i)
inst✝² : TopologicalSpace M₂
inst✝¹ : TopologicalSpace M₃
inst✝ : TopologicalSpace M₄
f✝ f' : ContinuousMultilinearMap R M₁ M₂
f : MultilinearMap R M₁ M₂
hf : Continuous f.toFun
hg : Continuous { toMultilinearMap := f, cont := hf }.toMultilinearMap.toFun
⊢ { toMultilinearMap := f, cont := hf } =
    { toMultilinearMap := { toMultilinearMap := f, cont := hf }.toMultilinearMap, cont := hg }
[PROOFSTEP]
rfl
[GOAL]
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst✝¹⁸ : Semiring R
inst✝¹⁷ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁵ : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : AddCommMonoid M₃
inst✝¹² : AddCommMonoid M₄
inst✝¹¹ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : (i : ι) → Module R (M₁' i)
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M₃
inst✝⁶ : Module R M₄
inst✝⁵ : (i : Fin (Nat.succ n)) → TopologicalSpace (M i)
inst✝⁴ : (i : ι) → TopologicalSpace (M₁ i)
inst✝³ : (i : ι) → TopologicalSpace (M₁' i)
inst✝² : TopologicalSpace M₂
inst✝¹ : TopologicalSpace M₃
inst✝ : TopologicalSpace M₄
f✝ f'✝ f f' : ContinuousMultilinearMap R M₁ M₂
⊢ f = f' ↔ ∀ (x : (i : ι) → M₁ i), ↑f x = ↑f' x
[PROOFSTEP]
rw [← toMultilinearMap_injective.eq_iff, MultilinearMap.ext_iff]
[GOAL]
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst✝¹⁸ : Semiring R
inst✝¹⁷ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁵ : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : AddCommMonoid M₃
inst✝¹² : AddCommMonoid M₄
inst✝¹¹ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : (i : ι) → Module R (M₁' i)
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M₃
inst✝⁶ : Module R M₄
inst✝⁵ : (i : Fin (Nat.succ n)) → TopologicalSpace (M i)
inst✝⁴ : (i : ι) → TopologicalSpace (M₁ i)
inst✝³ : (i : ι) → TopologicalSpace (M₁' i)
inst✝² : TopologicalSpace M₂
inst✝¹ : TopologicalSpace M₃
inst✝ : TopologicalSpace M₄
f✝ f'✝ f f' : ContinuousMultilinearMap R M₁ M₂
⊢ (∀ (x : (i : ι) → M₁ i), ↑f.toMultilinearMap x = ↑f'.toMultilinearMap x) ↔ ∀ (x : (i : ι) → M₁ i), ↑f x = ↑f' x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst✝¹⁸ : Semiring R
inst✝¹⁷ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁵ : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : AddCommMonoid M₃
inst✝¹² : AddCommMonoid M₄
inst✝¹¹ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : (i : ι) → Module R (M₁' i)
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M₃
inst✝⁶ : Module R M₄
inst✝⁵ : (i : Fin (Nat.succ n)) → TopologicalSpace (M i)
inst✝⁴ : (i : ι) → TopologicalSpace (M₁ i)
inst✝³ : (i : ι) → TopologicalSpace (M₁' i)
inst✝² : TopologicalSpace M₂
inst✝¹ : TopologicalSpace M₃
inst✝ : TopologicalSpace M₄
f✝ f' : ContinuousMultilinearMap R M₁ M₂
g : M₂ →L[R] M₃
f : ContinuousMultilinearMap R M₁ M₂
⊢ ↑(ContinuousLinearMap.compContinuousMultilinearMap g f) = ↑g ∘ ↑f
[PROOFSTEP]
ext m
[GOAL]
case h
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst✝¹⁸ : Semiring R
inst✝¹⁷ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁵ : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : AddCommMonoid M₃
inst✝¹² : AddCommMonoid M₄
inst✝¹¹ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : (i : ι) → Module R (M₁' i)
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M₃
inst✝⁶ : Module R M₄
inst✝⁵ : (i : Fin (Nat.succ n)) → TopologicalSpace (M i)
inst✝⁴ : (i : ι) → TopologicalSpace (M₁ i)
inst✝³ : (i : ι) → TopologicalSpace (M₁' i)
inst✝² : TopologicalSpace M₂
inst✝¹ : TopologicalSpace M₃
inst✝ : TopologicalSpace M₄
f✝ f' : ContinuousMultilinearMap R M₁ M₂
g : M₂ →L[R] M₃
f : ContinuousMultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
⊢ ↑(ContinuousLinearMap.compContinuousMultilinearMap g f) m = (↑g ∘ ↑f) m
[PROOFSTEP]
rfl
[GOAL]
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst✝²¹ : Semiring R
inst✝²⁰ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁸ : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹⁷ : AddCommMonoid M₂
inst✝¹⁶ : AddCommMonoid M₃
inst✝¹⁵ : AddCommMonoid M₄
inst✝¹⁴ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝¹³ : (i : ι) → Module R (M₁ i)
inst✝¹² : (i : ι) → Module R (M₁' i)
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module R M₃
inst✝⁹ : Module R M₄
inst✝⁸ : (i : Fin (Nat.succ n)) → TopologicalSpace (M i)
inst✝⁷ : (i : ι) → TopologicalSpace (M₁ i)
inst✝⁶ : (i : ι) → TopologicalSpace (M₁' i)
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : TopologicalSpace M₃
inst✝³ : TopologicalSpace M₄
f✝ f' : ContinuousMultilinearMap R M₁ M₂
ι' : Type u_1
M' : ι' → Type u_2
inst✝² : (i : ι') → AddCommMonoid (M' i)
inst✝¹ : (i : ι') → TopologicalSpace (M' i)
inst✝ : (i : ι') → Module R (M' i)
f : (i : ι') → ContinuousMultilinearMap R M₁ (M' i)
⊢ (fun f i => ContinuousLinearMap.compContinuousMultilinearMap (ContinuousLinearMap.proj i) f) (pi f) = f
[PROOFSTEP]
ext
[GOAL]
case h.H
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst✝²¹ : Semiring R
inst✝²⁰ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁸ : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹⁷ : AddCommMonoid M₂
inst✝¹⁶ : AddCommMonoid M₃
inst✝¹⁵ : AddCommMonoid M₄
inst✝¹⁴ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝¹³ : (i : ι) → Module R (M₁ i)
inst✝¹² : (i : ι) → Module R (M₁' i)
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module R M₃
inst✝⁹ : Module R M₄
inst✝⁸ : (i : Fin (Nat.succ n)) → TopologicalSpace (M i)
inst✝⁷ : (i : ι) → TopologicalSpace (M₁ i)
inst✝⁶ : (i : ι) → TopologicalSpace (M₁' i)
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : TopologicalSpace M₃
inst✝³ : TopologicalSpace M₄
f✝ f' : ContinuousMultilinearMap R M₁ M₂
ι' : Type u_1
M' : ι' → Type u_2
inst✝² : (i : ι') → AddCommMonoid (M' i)
inst✝¹ : (i : ι') → TopologicalSpace (M' i)
inst✝ : (i : ι') → Module R (M' i)
f : (i : ι') → ContinuousMultilinearMap R M₁ (M' i)
x✝¹ : ι'
x✝ : (i : ι) → M₁ i
⊢ ↑((fun f i => ContinuousLinearMap.compContinuousMultilinearMap (ContinuousLinearMap.proj i) f) (pi f) x✝¹) x✝ =
    ↑(f x✝¹) x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst✝²¹ : Semiring R
inst✝²⁰ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁸ : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹⁷ : AddCommMonoid M₂
inst✝¹⁶ : AddCommMonoid M₃
inst✝¹⁵ : AddCommMonoid M₄
inst✝¹⁴ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝¹³ : (i : ι) → Module R (M₁ i)
inst✝¹² : (i : ι) → Module R (M₁' i)
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module R M₃
inst✝⁹ : Module R M₄
inst✝⁸ : (i : Fin (Nat.succ n)) → TopologicalSpace (M i)
inst✝⁷ : (i : ι) → TopologicalSpace (M₁ i)
inst✝⁶ : (i : ι) → TopologicalSpace (M₁' i)
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : TopologicalSpace M₃
inst✝³ : TopologicalSpace M₄
f✝ f' : ContinuousMultilinearMap R M₁ M₂
ι' : Type u_1
M' : ι' → Type u_2
inst✝² : (i : ι') → AddCommMonoid (M' i)
inst✝¹ : (i : ι') → TopologicalSpace (M' i)
inst✝ : (i : ι') → Module R (M' i)
f : ContinuousMultilinearMap R M₁ ((i : ι') → M' i)
⊢ pi ((fun f i => ContinuousLinearMap.compContinuousMultilinearMap (ContinuousLinearMap.proj i) f) f) = f
[PROOFSTEP]
ext
[GOAL]
case H.h
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst✝²¹ : Semiring R
inst✝²⁰ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁸ : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹⁷ : AddCommMonoid M₂
inst✝¹⁶ : AddCommMonoid M₃
inst✝¹⁵ : AddCommMonoid M₄
inst✝¹⁴ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝¹³ : (i : ι) → Module R (M₁ i)
inst✝¹² : (i : ι) → Module R (M₁' i)
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module R M₃
inst✝⁹ : Module R M₄
inst✝⁸ : (i : Fin (Nat.succ n)) → TopologicalSpace (M i)
inst✝⁷ : (i : ι) → TopologicalSpace (M₁ i)
inst✝⁶ : (i : ι) → TopologicalSpace (M₁' i)
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : TopologicalSpace M₃
inst✝³ : TopologicalSpace M₄
f✝ f' : ContinuousMultilinearMap R M₁ M₂
ι' : Type u_1
M' : ι' → Type u_2
inst✝² : (i : ι') → AddCommMonoid (M' i)
inst✝¹ : (i : ι') → TopologicalSpace (M' i)
inst✝ : (i : ι') → Module R (M' i)
f : ContinuousMultilinearMap R M₁ ((i : ι') → M' i)
x✝¹ : (i : ι) → M₁ i
x✝ : ι'
⊢ ↑(pi ((fun f i => ContinuousLinearMap.compContinuousMultilinearMap (ContinuousLinearMap.proj i) f) f)) x✝¹ x✝ =
    ↑f x✝¹ x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst✝¹⁸ : Semiring R
inst✝¹⁷ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁵ : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : AddCommMonoid M₃
inst✝¹² : AddCommMonoid M₄
inst✝¹¹ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : (i : ι) → Module R (M₁' i)
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M₃
inst✝⁶ : Module R M₄
inst✝⁵ : (i : Fin (Nat.succ n)) → TopologicalSpace (M i)
inst✝⁴ : (i : ι) → TopologicalSpace (M₁ i)
inst✝³ : (i : ι) → TopologicalSpace (M₁' i)
inst✝² : TopologicalSpace M₂
inst✝¹ : TopologicalSpace M₃
inst✝ : TopologicalSpace M₄
f f' : ContinuousMultilinearMap R M₁ M₂
ι' : Type u_1
e : ι ≃ ι'
x✝¹ : ContinuousMultilinearMap R (fun x => M₂) M₃
x✝ : ι → M₂
⊢ ↑(domDomCongr e.symm (domDomCongr e x✝¹)) x✝ = ↑x✝¹ x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst✝¹⁸ : Semiring R
inst✝¹⁷ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁵ : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : AddCommMonoid M₃
inst✝¹² : AddCommMonoid M₄
inst✝¹¹ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : (i : ι) → Module R (M₁' i)
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M₃
inst✝⁶ : Module R M₄
inst✝⁵ : (i : Fin (Nat.succ n)) → TopologicalSpace (M i)
inst✝⁴ : (i : ι) → TopologicalSpace (M₁ i)
inst✝³ : (i : ι) → TopologicalSpace (M₁' i)
inst✝² : TopologicalSpace M₂
inst✝¹ : TopologicalSpace M₃
inst✝ : TopologicalSpace M₄
f f' : ContinuousMultilinearMap R M₁ M₂
ι' : Type u_1
e : ι ≃ ι'
x✝¹ : ContinuousMultilinearMap R (fun x => M₂) M₃
x✝ : ι' → M₂
⊢ ↑(domDomCongr e (domDomCongr e.symm x✝¹)) x✝ = ↑x✝¹ x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
A : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousMul A
⊢ Continuous (MultilinearMap.mkPiAlgebraFin R n A).toFun
[PROOFSTEP]
change Continuous fun m => (List.ofFn m).prod
[GOAL]
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
A : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousMul A
⊢ Continuous fun m => List.prod (List.ofFn m)
[PROOFSTEP]
simp_rw [List.ofFn_eq_map]
[GOAL]
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
A : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousMul A
⊢ Continuous fun m => List.prod (List.map m (List.finRange n))
[PROOFSTEP]
exact continuous_list_prod _ fun i _ => continuous_apply _