[GOAL]
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹⁰ : Monoid A
inst✝⁹ : Monoid B
inst✝⁸ : Monoid C
inst✝⁷ : Monoid D
inst✝⁶ : CommGroup E
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace C
inst✝² : TopologicalSpace D
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalGroup E
f g : ContinuousMonoidHom A B
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
[GOAL]
case mk.mk.mk
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹⁰ : Monoid A
inst✝⁹ : Monoid B
inst✝⁸ : Monoid C
inst✝⁷ : Monoid D
inst✝⁶ : CommGroup E
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace C
inst✝² : TopologicalSpace D
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalGroup E
g : ContinuousMonoidHom A B
toFun✝ : A → B
map_one'✝ : toFun✝ 1 = 1
map_mul'✝ :
  ∀ (x y : A),
    OneHom.toFun { toFun := toFun✝, map_one' := map_one'✝ } (x * y) =
      OneHom.toFun { toFun := toFun✝, map_one' := map_one'✝ } x *
        OneHom.toFun { toFun := toFun✝, map_one' := map_one'✝ } y
continuous_toFun✝ :
  Continuous (↑{ toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }).toFun
h :
  (fun f => f.toFun)
      { toMonoidHom := { toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
        continuous_toFun := continuous_toFun✝ } =
    (fun f => f.toFun) g
⊢ { toMonoidHom := { toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
      continuous_toFun := continuous_toFun✝ } =
    g
[PROOFSTEP]
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk.mk.mk
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹⁰ : Monoid A
inst✝⁹ : Monoid B
inst✝⁸ : Monoid C
inst✝⁷ : Monoid D
inst✝⁶ : CommGroup E
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace C
inst✝² : TopologicalSpace D
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalGroup E
toFun✝¹ : A → B
map_one'✝¹ : toFun✝¹ 1 = 1
map_mul'✝¹ :
  ∀ (x y : A),
    OneHom.toFun { toFun := toFun✝¹, map_one' := map_one'✝¹ } (x * y) =
      OneHom.toFun { toFun := toFun✝¹, map_one' := map_one'✝¹ } x *
        OneHom.toFun { toFun := toFun✝¹, map_one' := map_one'✝¹ } y
continuous_toFun✝¹ :
  Continuous (↑{ toOneHom := { toFun := toFun✝¹, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }).toFun
toFun✝ : A → B
map_one'✝ : toFun✝ 1 = 1
map_mul'✝ :
  ∀ (x y : A),
    OneHom.toFun { toFun := toFun✝, map_one' := map_one'✝ } (x * y) =
      OneHom.toFun { toFun := toFun✝, map_one' := map_one'✝ } x *
        OneHom.toFun { toFun := toFun✝, map_one' := map_one'✝ } y
continuous_toFun✝ :
  Continuous (↑{ toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }).toFun
h :
  (fun f => f.toFun)
      { toMonoidHom := { toOneHom := { toFun := toFun✝¹, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
        continuous_toFun := continuous_toFun✝¹ } =
    (fun f => f.toFun)
      { toMonoidHom := { toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
        continuous_toFun := continuous_toFun✝ }
⊢ { toMonoidHom := { toOneHom := { toFun := toFun✝¹, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
      continuous_toFun := continuous_toFun✝¹ } =
    { toMonoidHom := { toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
      continuous_toFun := continuous_toFun✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹⁰ : Monoid A
inst✝⁹ : Monoid B
inst✝⁸ : Monoid C
inst✝⁷ : Monoid D
inst✝⁶ : CommGroup E
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace C
inst✝² : TopologicalSpace D
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalGroup E
f g : ContinuousMonoidHom A B
h : toContinuousMap f = toContinuousMap g
⊢ ∀ (x : A), ↑f x = ↑g x
[PROOFSTEP]
convert FunLike.ext_iff.1 h
[GOAL]
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
⊢ IsOpen (Set.range toContinuousMap)ᶜ
[PROOFSTEP]
suffices
  Set.range (toContinuousMap : ContinuousMonoidHom A B → C(A, B)) =
    ({f | f '' {1} ⊆ {1}ᶜ} ∪
          ⋃ (x) (y) (U) (V) (W) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ : Disjoint (U * V) W),
            {f | f '' { x } ⊆ U} ∩ {f | f '' { y } ⊆ V} ∩ {f | f '' {x * y} ⊆ W} :
        Set C(A, B))ᶜ
  by
  rw [this, compl_compl]
  refine' (ContinuousMap.isOpen_gen isCompact_singleton isOpen_compl_singleton).union _
  repeat' apply isOpen_iUnion; intro
  repeat' apply IsOpen.inter
  all_goals apply ContinuousMap.isOpen_gen isCompact_singleton; assumption
[GOAL]
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
⊢ IsOpen (Set.range toContinuousMap)ᶜ
[PROOFSTEP]
rw [this, compl_compl]
[GOAL]
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
⊢ IsOpen
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
      ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
        Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})
[PROOFSTEP]
refine' (ContinuousMap.isOpen_gen isCompact_singleton isOpen_compl_singleton).union _
[GOAL]
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
⊢ IsOpen
    (⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
      Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})
[PROOFSTEP]
repeat' apply isOpen_iUnion; intro
[GOAL]
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
⊢ IsOpen
    (⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
      Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})
[PROOFSTEP]
apply isOpen_iUnion
[GOAL]
case h
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
⊢ ∀ (i : A),
    IsOpen
      (⋃ (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
        Disjoint (U * V) W), {f | ↑f '' {i} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {i * y} ⊆ W})
[PROOFSTEP]
intro
[GOAL]
case h
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝ : A
⊢ IsOpen
    (⋃ (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
      Disjoint (U * V) W), {f | ↑f '' {i✝} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {i✝ * y} ⊆ W})
[PROOFSTEP]
apply isOpen_iUnion
[GOAL]
case h.h
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝ : A
⊢ ∀ (i : A),
    IsOpen
      (⋃ (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ : Disjoint (U * V) W),
        {f | ↑f '' {i✝} ⊆ U} ∩ {f | ↑f '' {i} ⊆ V} ∩ {f | ↑f '' {i✝ * i} ⊆ W})
[PROOFSTEP]
intro
[GOAL]
case h.h
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝¹ i✝ : A
⊢ IsOpen
    (⋃ (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ : Disjoint (U * V) W),
      {f | ↑f '' {i✝¹} ⊆ U} ∩ {f | ↑f '' {i✝} ⊆ V} ∩ {f | ↑f '' {i✝¹ * i✝} ⊆ W})
[PROOFSTEP]
apply isOpen_iUnion
[GOAL]
case h.h.h
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝¹ i✝ : A
⊢ ∀ (i : Set B),
    IsOpen
      (⋃ (V : Set B) (W : Set B) (_ : IsOpen i) (_ : IsOpen V) (_ : IsOpen W) (_ : Disjoint (i * V) W),
        {f | ↑f '' {i✝¹} ⊆ i} ∩ {f | ↑f '' {i✝} ⊆ V} ∩ {f | ↑f '' {i✝¹ * i✝} ⊆ W})
[PROOFSTEP]
intro
[GOAL]
case h.h.h
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝² i✝¹ : A
i✝ : Set B
⊢ IsOpen
    (⋃ (V : Set B) (W : Set B) (_ : IsOpen i✝) (_ : IsOpen V) (_ : IsOpen W) (_ : Disjoint (i✝ * V) W),
      {f | ↑f '' {i✝²} ⊆ i✝} ∩ {f | ↑f '' {i✝¹} ⊆ V} ∩ {f | ↑f '' {i✝² * i✝¹} ⊆ W})
[PROOFSTEP]
apply isOpen_iUnion
[GOAL]
case h.h.h.h
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝² i✝¹ : A
i✝ : Set B
⊢ ∀ (i : Set B),
    IsOpen
      (⋃ (W : Set B) (_ : IsOpen i✝) (_ : IsOpen i) (_ : IsOpen W) (_ : Disjoint (i✝ * i) W),
        {f | ↑f '' {i✝²} ⊆ i✝} ∩ {f | ↑f '' {i✝¹} ⊆ i} ∩ {f | ↑f '' {i✝² * i✝¹} ⊆ W})
[PROOFSTEP]
intro
[GOAL]
case h.h.h.h
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝³ i✝² : A
i✝¹ i✝ : Set B
⊢ IsOpen
    (⋃ (W : Set B) (_ : IsOpen i✝¹) (_ : IsOpen i✝) (_ : IsOpen W) (_ : Disjoint (i✝¹ * i✝) W),
      {f | ↑f '' {i✝³} ⊆ i✝¹} ∩ {f | ↑f '' {i✝²} ⊆ i✝} ∩ {f | ↑f '' {i✝³ * i✝²} ⊆ W})
[PROOFSTEP]
apply isOpen_iUnion
[GOAL]
case h.h.h.h.h
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝³ i✝² : A
i✝¹ i✝ : Set B
⊢ ∀ (i : Set B),
    IsOpen
      (⋃ (_ : IsOpen i✝¹) (_ : IsOpen i✝) (_ : IsOpen i) (_ : Disjoint (i✝¹ * i✝) i),
        {f | ↑f '' {i✝³} ⊆ i✝¹} ∩ {f | ↑f '' {i✝²} ⊆ i✝} ∩ {f | ↑f '' {i✝³ * i✝²} ⊆ i})
[PROOFSTEP]
intro
[GOAL]
case h.h.h.h.h
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝⁴ i✝³ : A
i✝² i✝¹ i✝ : Set B
⊢ IsOpen
    (⋃ (_ : IsOpen i✝²) (_ : IsOpen i✝¹) (_ : IsOpen i✝) (_ : Disjoint (i✝² * i✝¹) i✝),
      {f | ↑f '' {i✝⁴} ⊆ i✝²} ∩ {f | ↑f '' {i✝³} ⊆ i✝¹} ∩ {f | ↑f '' {i✝⁴ * i✝³} ⊆ i✝})
[PROOFSTEP]
apply isOpen_iUnion
[GOAL]
case h.h.h.h.h.h
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝⁴ i✝³ : A
i✝² i✝¹ i✝ : Set B
⊢ IsOpen i✝² →
    IsOpen
      (⋃ (_ : IsOpen i✝¹) (_ : IsOpen i✝) (_ : Disjoint (i✝² * i✝¹) i✝),
        {f | ↑f '' {i✝⁴} ⊆ i✝²} ∩ {f | ↑f '' {i✝³} ⊆ i✝¹} ∩ {f | ↑f '' {i✝⁴ * i✝³} ⊆ i✝})
[PROOFSTEP]
intro
[GOAL]
case h.h.h.h.h.h
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝⁵ i✝⁴ : A
i✝³ i✝² i✝¹ : Set B
i✝ : IsOpen i✝³
⊢ IsOpen
    (⋃ (_ : IsOpen i✝²) (_ : IsOpen i✝¹) (_ : Disjoint (i✝³ * i✝²) i✝¹),
      {f | ↑f '' {i✝⁵} ⊆ i✝³} ∩ {f | ↑f '' {i✝⁴} ⊆ i✝²} ∩ {f | ↑f '' {i✝⁵ * i✝⁴} ⊆ i✝¹})
[PROOFSTEP]
apply isOpen_iUnion
[GOAL]
case h.h.h.h.h.h.h
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝⁵ i✝⁴ : A
i✝³ i✝² i✝¹ : Set B
i✝ : IsOpen i✝³
⊢ IsOpen i✝² →
    IsOpen
      (⋃ (_ : IsOpen i✝¹) (_ : Disjoint (i✝³ * i✝²) i✝¹),
        {f | ↑f '' {i✝⁵} ⊆ i✝³} ∩ {f | ↑f '' {i✝⁴} ⊆ i✝²} ∩ {f | ↑f '' {i✝⁵ * i✝⁴} ⊆ i✝¹})
[PROOFSTEP]
intro
[GOAL]
case h.h.h.h.h.h.h
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝⁶ i✝⁵ : A
i✝⁴ i✝³ i✝² : Set B
i✝¹ : IsOpen i✝⁴
i✝ : IsOpen i✝³
⊢ IsOpen
    (⋃ (_ : IsOpen i✝²) (_ : Disjoint (i✝⁴ * i✝³) i✝²),
      {f | ↑f '' {i✝⁶} ⊆ i✝⁴} ∩ {f | ↑f '' {i✝⁵} ⊆ i✝³} ∩ {f | ↑f '' {i✝⁶ * i✝⁵} ⊆ i✝²})
[PROOFSTEP]
apply isOpen_iUnion
[GOAL]
case h.h.h.h.h.h.h.h
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝⁶ i✝⁵ : A
i✝⁴ i✝³ i✝² : Set B
i✝¹ : IsOpen i✝⁴
i✝ : IsOpen i✝³
⊢ IsOpen i✝² →
    IsOpen
      (⋃ (_ : Disjoint (i✝⁴ * i✝³) i✝²),
        {f | ↑f '' {i✝⁶} ⊆ i✝⁴} ∩ {f | ↑f '' {i✝⁵} ⊆ i✝³} ∩ {f | ↑f '' {i✝⁶ * i✝⁵} ⊆ i✝²})
[PROOFSTEP]
intro
[GOAL]
case h.h.h.h.h.h.h.h
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝⁷ i✝⁶ : A
i✝⁵ i✝⁴ i✝³ : Set B
i✝² : IsOpen i✝⁵
i✝¹ : IsOpen i✝⁴
i✝ : IsOpen i✝³
⊢ IsOpen
    (⋃ (_ : Disjoint (i✝⁵ * i✝⁴) i✝³),
      {f | ↑f '' {i✝⁷} ⊆ i✝⁵} ∩ {f | ↑f '' {i✝⁶} ⊆ i✝⁴} ∩ {f | ↑f '' {i✝⁷ * i✝⁶} ⊆ i✝³})
[PROOFSTEP]
apply isOpen_iUnion
[GOAL]
case h.h.h.h.h.h.h.h.h
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝⁷ i✝⁶ : A
i✝⁵ i✝⁴ i✝³ : Set B
i✝² : IsOpen i✝⁵
i✝¹ : IsOpen i✝⁴
i✝ : IsOpen i✝³
⊢ Disjoint (i✝⁵ * i✝⁴) i✝³ → IsOpen ({f | ↑f '' {i✝⁷} ⊆ i✝⁵} ∩ {f | ↑f '' {i✝⁶} ⊆ i✝⁴} ∩ {f | ↑f '' {i✝⁷ * i✝⁶} ⊆ i✝³})
[PROOFSTEP]
intro
[GOAL]
case h.h.h.h.h.h.h.h.h
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝⁸ i✝⁷ : A
i✝⁶ i✝⁵ i✝⁴ : Set B
i✝³ : IsOpen i✝⁶
i✝² : IsOpen i✝⁵
i✝¹ : IsOpen i✝⁴
i✝ : Disjoint (i✝⁶ * i✝⁵) i✝⁴
⊢ IsOpen ({f | ↑f '' {i✝⁸} ⊆ i✝⁶} ∩ {f | ↑f '' {i✝⁷} ⊆ i✝⁵} ∩ {f | ↑f '' {i✝⁸ * i✝⁷} ⊆ i✝⁴})
[PROOFSTEP]
apply isOpen_iUnion
[GOAL]
case h.h.h.h.h.h.h.h.h
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝⁸ i✝⁷ : A
i✝⁶ i✝⁵ i✝⁴ : Set B
i✝³ : IsOpen i✝⁶
i✝² : IsOpen i✝⁵
i✝¹ : IsOpen i✝⁴
i✝ : Disjoint (i✝⁶ * i✝⁵) i✝⁴
⊢ IsOpen ({f | ↑f '' {i✝⁸} ⊆ i✝⁶} ∩ {f | ↑f '' {i✝⁷} ⊆ i✝⁵} ∩ {f | ↑f '' {i✝⁸ * i✝⁷} ⊆ i✝⁴})
[PROOFSTEP]
repeat' apply IsOpen.inter
[GOAL]
case h.h.h.h.h.h.h.h.h
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝⁸ i✝⁷ : A
i✝⁶ i✝⁵ i✝⁴ : Set B
i✝³ : IsOpen i✝⁶
i✝² : IsOpen i✝⁵
i✝¹ : IsOpen i✝⁴
i✝ : Disjoint (i✝⁶ * i✝⁵) i✝⁴
⊢ IsOpen ({f | ↑f '' {i✝⁸} ⊆ i✝⁶} ∩ {f | ↑f '' {i✝⁷} ⊆ i✝⁵} ∩ {f | ↑f '' {i✝⁸ * i✝⁷} ⊆ i✝⁴})
[PROOFSTEP]
apply IsOpen.inter
[GOAL]
case h.h.h.h.h.h.h.h.h.h₁
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝⁸ i✝⁷ : A
i✝⁶ i✝⁵ i✝⁴ : Set B
i✝³ : IsOpen i✝⁶
i✝² : IsOpen i✝⁵
i✝¹ : IsOpen i✝⁴
i✝ : Disjoint (i✝⁶ * i✝⁵) i✝⁴
⊢ IsOpen ({f | ↑f '' {i✝⁸} ⊆ i✝⁶} ∩ {f | ↑f '' {i✝⁷} ⊆ i✝⁵})
[PROOFSTEP]
apply IsOpen.inter
[GOAL]
case h.h.h.h.h.h.h.h.h.h₁.h₁
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝⁸ i✝⁷ : A
i✝⁶ i✝⁵ i✝⁴ : Set B
i✝³ : IsOpen i✝⁶
i✝² : IsOpen i✝⁵
i✝¹ : IsOpen i✝⁴
i✝ : Disjoint (i✝⁶ * i✝⁵) i✝⁴
⊢ IsOpen {f | ↑f '' {i✝⁸} ⊆ i✝⁶}
[PROOFSTEP]
apply IsOpen.inter
[GOAL]
case h.h.h.h.h.h.h.h.h.h₁.h₂
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝⁸ i✝⁷ : A
i✝⁶ i✝⁵ i✝⁴ : Set B
i✝³ : IsOpen i✝⁶
i✝² : IsOpen i✝⁵
i✝¹ : IsOpen i✝⁴
i✝ : Disjoint (i✝⁶ * i✝⁵) i✝⁴
⊢ IsOpen {f | ↑f '' {i✝⁷} ⊆ i✝⁵}
[PROOFSTEP]
apply IsOpen.inter
[GOAL]
case h.h.h.h.h.h.h.h.h.h₂
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝⁸ i✝⁷ : A
i✝⁶ i✝⁵ i✝⁴ : Set B
i✝³ : IsOpen i✝⁶
i✝² : IsOpen i✝⁵
i✝¹ : IsOpen i✝⁴
i✝ : Disjoint (i✝⁶ * i✝⁵) i✝⁴
⊢ IsOpen {f | ↑f '' {i✝⁸ * i✝⁷} ⊆ i✝⁴}
[PROOFSTEP]
apply IsOpen.inter
[GOAL]
case h.h.h.h.h.h.h.h.h.h₁.h₁
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝⁸ i✝⁷ : A
i✝⁶ i✝⁵ i✝⁴ : Set B
i✝³ : IsOpen i✝⁶
i✝² : IsOpen i✝⁵
i✝¹ : IsOpen i✝⁴
i✝ : Disjoint (i✝⁶ * i✝⁵) i✝⁴
⊢ IsOpen {f | ↑f '' {i✝⁸} ⊆ i✝⁶}
case h.h.h.h.h.h.h.h.h.h₁.h₂
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝⁸ i✝⁷ : A
i✝⁶ i✝⁵ i✝⁴ : Set B
i✝³ : IsOpen i✝⁶
i✝² : IsOpen i✝⁵
i✝¹ : IsOpen i✝⁴
i✝ : Disjoint (i✝⁶ * i✝⁵) i✝⁴
⊢ IsOpen {f | ↑f '' {i✝⁷} ⊆ i✝⁵}
case h.h.h.h.h.h.h.h.h.h₂
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝⁸ i✝⁷ : A
i✝⁶ i✝⁵ i✝⁴ : Set B
i✝³ : IsOpen i✝⁶
i✝² : IsOpen i✝⁵
i✝¹ : IsOpen i✝⁴
i✝ : Disjoint (i✝⁶ * i✝⁵) i✝⁴
⊢ IsOpen {f | ↑f '' {i✝⁸ * i✝⁷} ⊆ i✝⁴}
[PROOFSTEP]
all_goals apply ContinuousMap.isOpen_gen isCompact_singleton; assumption
[GOAL]
case h.h.h.h.h.h.h.h.h.h₁.h₁
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝⁸ i✝⁷ : A
i✝⁶ i✝⁵ i✝⁴ : Set B
i✝³ : IsOpen i✝⁶
i✝² : IsOpen i✝⁵
i✝¹ : IsOpen i✝⁴
i✝ : Disjoint (i✝⁶ * i✝⁵) i✝⁴
⊢ IsOpen {f | ↑f '' {i✝⁸} ⊆ i✝⁶}
[PROOFSTEP]
apply ContinuousMap.isOpen_gen isCompact_singleton
[GOAL]
case h.h.h.h.h.h.h.h.h.h₁.h₁
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝⁸ i✝⁷ : A
i✝⁶ i✝⁵ i✝⁴ : Set B
i✝³ : IsOpen i✝⁶
i✝² : IsOpen i✝⁵
i✝¹ : IsOpen i✝⁴
i✝ : Disjoint (i✝⁶ * i✝⁵) i✝⁴
⊢ IsOpen i✝⁶
[PROOFSTEP]
assumption
[GOAL]
case h.h.h.h.h.h.h.h.h.h₁.h₂
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝⁸ i✝⁷ : A
i✝⁶ i✝⁵ i✝⁴ : Set B
i✝³ : IsOpen i✝⁶
i✝² : IsOpen i✝⁵
i✝¹ : IsOpen i✝⁴
i✝ : Disjoint (i✝⁶ * i✝⁵) i✝⁴
⊢ IsOpen {f | ↑f '' {i✝⁷} ⊆ i✝⁵}
[PROOFSTEP]
apply ContinuousMap.isOpen_gen isCompact_singleton
[GOAL]
case h.h.h.h.h.h.h.h.h.h₁.h₂
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝⁸ i✝⁷ : A
i✝⁶ i✝⁵ i✝⁴ : Set B
i✝³ : IsOpen i✝⁶
i✝² : IsOpen i✝⁵
i✝¹ : IsOpen i✝⁴
i✝ : Disjoint (i✝⁶ * i✝⁵) i✝⁴
⊢ IsOpen i✝⁵
[PROOFSTEP]
assumption
[GOAL]
case h.h.h.h.h.h.h.h.h.h₂
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝⁸ i✝⁷ : A
i✝⁶ i✝⁵ i✝⁴ : Set B
i✝³ : IsOpen i✝⁶
i✝² : IsOpen i✝⁵
i✝¹ : IsOpen i✝⁴
i✝ : Disjoint (i✝⁶ * i✝⁵) i✝⁴
⊢ IsOpen {f | ↑f '' {i✝⁸ * i✝⁷} ⊆ i✝⁴}
[PROOFSTEP]
apply ContinuousMap.isOpen_gen isCompact_singleton
[GOAL]
case h.h.h.h.h.h.h.h.h.h₂
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
this :
  Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
i✝⁸ i✝⁷ : A
i✝⁶ i✝⁵ i✝⁴ : Set B
i✝³ : IsOpen i✝⁶
i✝² : IsOpen i✝⁵
i✝¹ : IsOpen i✝⁴
i✝ : Disjoint (i✝⁶ * i✝⁵) i✝⁴
⊢ IsOpen i✝⁴
[PROOFSTEP]
assumption
[GOAL]
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
⊢ Set.range toContinuousMap =
    ({f | ↑f '' {1} ⊆ {1}ᶜ} ∪
        ⋃ (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (_ : IsOpen U) (_ : IsOpen V) (_ : IsOpen W) (_ :
          Disjoint (U * V) W), {f | ↑f '' {x} ⊆ U} ∩ {f | ↑f '' {y} ⊆ V} ∩ {f | ↑f '' {x * y} ⊆ W})ᶜ
[PROOFSTEP]
simp_rw [Set.compl_union, Set.compl_iUnion, Set.image_singleton, Set.singleton_subset_iff, Set.ext_iff,
  Set.mem_inter_iff, Set.mem_iInter, Set.mem_compl_iff]
[GOAL]
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
⊢ ∀ (x : C(A, B)),
    x ∈ Set.range toContinuousMap ↔
      ¬x ∈ {f | ¬↑f 1 ∈ {1}} ∧
        ∀ (i i_1 : A) (i_2 i_3 i_4 : Set B),
          IsOpen i_2 →
            IsOpen i_3 →
              IsOpen i_4 →
                Disjoint (i_2 * i_3) i_4 → ¬x ∈ {f | ↑f i ∈ i_2} ∩ {f | ↑f i_1 ∈ i_3} ∩ {f | ↑f (i * i_1) ∈ i_4}
[PROOFSTEP]
refine' fun f => ⟨_, _⟩
[GOAL]
case refine'_1
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
f : C(A, B)
⊢ f ∈ Set.range toContinuousMap →
    ¬f ∈ {f | ¬↑f 1 ∈ {1}} ∧
      ∀ (i i_1 : A) (i_2 i_3 i_4 : Set B),
        IsOpen i_2 →
          IsOpen i_3 →
            IsOpen i_4 →
              Disjoint (i_2 * i_3) i_4 → ¬f ∈ {f | ↑f i ∈ i_2} ∩ {f | ↑f i_1 ∈ i_3} ∩ {f | ↑f (i * i_1) ∈ i_4}
[PROOFSTEP]
rintro ⟨f, rfl⟩
[GOAL]
case refine'_1.intro
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
f : ContinuousMonoidHom A B
⊢ ¬toContinuousMap f ∈ {f | ¬↑f 1 ∈ {1}} ∧
    ∀ (i i_1 : A) (i_2 i_3 i_4 : Set B),
      IsOpen i_2 →
        IsOpen i_3 →
          IsOpen i_4 →
            Disjoint (i_2 * i_3) i_4 →
              ¬toContinuousMap f ∈ {f | ↑f i ∈ i_2} ∩ {f | ↑f i_1 ∈ i_3} ∩ {f | ↑f (i * i_1) ∈ i_4}
[PROOFSTEP]
exact
  ⟨fun h => h (map_one f), fun x y U V W _hU _hV _hW h ⟨⟨hfU, hfV⟩, hfW⟩ =>
    h.le_bot ⟨Set.mul_mem_mul hfU hfV, (congr_arg (· ∈ W) (map_mul f x y)).mp hfW⟩⟩
[GOAL]
case refine'_2
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
f : C(A, B)
⊢ (¬f ∈ {f | ¬↑f 1 ∈ {1}} ∧
      ∀ (i i_1 : A) (i_2 i_3 i_4 : Set B),
        IsOpen i_2 →
          IsOpen i_3 →
            IsOpen i_4 →
              Disjoint (i_2 * i_3) i_4 → ¬f ∈ {f | ↑f i ∈ i_2} ∩ {f | ↑f i_1 ∈ i_3} ∩ {f | ↑f (i * i_1) ∈ i_4}) →
    f ∈ Set.range toContinuousMap
[PROOFSTEP]
rintro ⟨hf1, hf2⟩
[GOAL]
case refine'_2.intro
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
f : C(A, B)
hf1 : ¬f ∈ {f | ¬↑f 1 ∈ {1}}
hf2 :
  ∀ (i i_1 : A) (i_2 i_3 i_4 : Set B),
    IsOpen i_2 →
      IsOpen i_3 →
        IsOpen i_4 → Disjoint (i_2 * i_3) i_4 → ¬f ∈ {f | ↑f i ∈ i_2} ∩ {f | ↑f i_1 ∈ i_3} ∩ {f | ↑f (i * i_1) ∈ i_4}
⊢ f ∈ Set.range toContinuousMap
[PROOFSTEP]
suffices ∀ x y, f (x * y) = f x * f y by
  refine'
    ⟨({ f with
          map_one' := of_not_not hf1
          map_mul' := this } :
        ContinuousMonoidHom A B),
      ContinuousMap.ext fun _ => rfl⟩
[GOAL]
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
f : C(A, B)
hf1 : ¬f ∈ {f | ¬↑f 1 ∈ {1}}
hf2 :
  ∀ (i i_1 : A) (i_2 i_3 i_4 : Set B),
    IsOpen i_2 →
      IsOpen i_3 →
        IsOpen i_4 → Disjoint (i_2 * i_3) i_4 → ¬f ∈ {f | ↑f i ∈ i_2} ∩ {f | ↑f i_1 ∈ i_3} ∩ {f | ↑f (i * i_1) ∈ i_4}
this : ∀ (x y : A), ↑f (x * y) = ↑f x * ↑f y
⊢ f ∈ Set.range toContinuousMap
[PROOFSTEP]
refine'
  ⟨({ f with
        map_one' := of_not_not hf1
        map_mul' := this } :
      ContinuousMonoidHom A B),
    ContinuousMap.ext fun _ => rfl⟩
[GOAL]
case refine'_2.intro
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
f : C(A, B)
hf1 : ¬f ∈ {f | ¬↑f 1 ∈ {1}}
hf2 :
  ∀ (i i_1 : A) (i_2 i_3 i_4 : Set B),
    IsOpen i_2 →
      IsOpen i_3 →
        IsOpen i_4 → Disjoint (i_2 * i_3) i_4 → ¬f ∈ {f | ↑f i ∈ i_2} ∩ {f | ↑f i_1 ∈ i_3} ∩ {f | ↑f (i * i_1) ∈ i_4}
⊢ ∀ (x y : A), ↑f (x * y) = ↑f x * ↑f y
[PROOFSTEP]
intro x y
[GOAL]
case refine'_2.intro
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
f : C(A, B)
hf1 : ¬f ∈ {f | ¬↑f 1 ∈ {1}}
hf2 :
  ∀ (i i_1 : A) (i_2 i_3 i_4 : Set B),
    IsOpen i_2 →
      IsOpen i_3 →
        IsOpen i_4 → Disjoint (i_2 * i_3) i_4 → ¬f ∈ {f | ↑f i ∈ i_2} ∩ {f | ↑f i_1 ∈ i_3} ∩ {f | ↑f (i * i_1) ∈ i_4}
x y : A
⊢ ↑f (x * y) = ↑f x * ↑f y
[PROOFSTEP]
contrapose! hf2
[GOAL]
case refine'_2.intro
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
f : C(A, B)
hf1 : ¬f ∈ {f | ¬↑f 1 ∈ {1}}
x y : A
hf2 : ↑f (x * y) ≠ ↑f x * ↑f y
⊢ ∃ i i_1 i_2 i_3 i_4,
    IsOpen i_2 ∧
      IsOpen i_3 ∧
        IsOpen i_4 ∧ Disjoint (i_2 * i_3) i_4 ∧ f ∈ {f | ↑f i ∈ i_2} ∩ {f | ↑f i_1 ∈ i_3} ∩ {f | ↑f (i * i_1) ∈ i_4}
[PROOFSTEP]
obtain ⟨UV, W, hUV, hW, hfUV, hfW, h⟩ := t2_separation hf2.symm
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
f : C(A, B)
hf1 : ¬f ∈ {f | ¬↑f 1 ∈ {1}}
x y : A
hf2 : ↑f (x * y) ≠ ↑f x * ↑f y
UV W : Set B
hUV : IsOpen UV
hW : IsOpen W
hfUV : ↑f x * ↑f y ∈ UV
hfW : ↑f (x * y) ∈ W
h : Disjoint UV W
⊢ ∃ i i_1 i_2 i_3 i_4,
    IsOpen i_2 ∧
      IsOpen i_3 ∧
        IsOpen i_4 ∧ Disjoint (i_2 * i_3) i_4 ∧ f ∈ {f | ↑f i ∈ i_2} ∩ {f | ↑f i_1 ∈ i_3} ∩ {f | ↑f (i * i_1) ∈ i_4}
[PROOFSTEP]
have hB := @continuous_mul B _ _ _
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
f : C(A, B)
hf1 : ¬f ∈ {f | ¬↑f 1 ∈ {1}}
x y : A
hf2 : ↑f (x * y) ≠ ↑f x * ↑f y
UV W : Set B
hUV : IsOpen UV
hW : IsOpen W
hfUV : ↑f x * ↑f y ∈ UV
hfW : ↑f (x * y) ∈ W
h : Disjoint UV W
hB : Continuous fun p => p.fst * p.snd
⊢ ∃ i i_1 i_2 i_3 i_4,
    IsOpen i_2 ∧
      IsOpen i_3 ∧
        IsOpen i_4 ∧ Disjoint (i_2 * i_3) i_4 ∧ f ∈ {f | ↑f i ∈ i_2} ∩ {f | ↑f i_1 ∈ i_3} ∩ {f | ↑f (i * i_1) ∈ i_4}
[PROOFSTEP]
obtain ⟨U, V, hU, hV, hfU, hfV, h'⟩ := isOpen_prod_iff.mp (hUV.preimage hB) (f x) (f y) hfUV
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
f : C(A, B)
hf1 : ¬f ∈ {f | ¬↑f 1 ∈ {1}}
x y : A
hf2 : ↑f (x * y) ≠ ↑f x * ↑f y
UV W : Set B
hUV : IsOpen UV
hW : IsOpen W
hfUV : ↑f x * ↑f y ∈ UV
hfW : ↑f (x * y) ∈ W
h : Disjoint UV W
hB : Continuous fun p => p.fst * p.snd
U V : Set B
hU : IsOpen U
hV : IsOpen V
hfU : ↑f x ∈ U
hfV : ↑f y ∈ V
h' : U ×ˢ V ⊆ (fun p => p.fst * p.snd) ⁻¹' UV
⊢ ∃ i i_1 i_2 i_3 i_4,
    IsOpen i_2 ∧
      IsOpen i_3 ∧
        IsOpen i_4 ∧ Disjoint (i_2 * i_3) i_4 ∧ f ∈ {f | ↑f i ∈ i_2} ∩ {f | ↑f i_1 ∈ i_3} ∩ {f | ↑f (i * i_1) ∈ i_4}
[PROOFSTEP]
refine' ⟨x, y, U, V, W, hU, hV, hW, h.mono_left _, ⟨hfU, hfV⟩, hfW⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
f : C(A, B)
hf1 : ¬f ∈ {f | ¬↑f 1 ∈ {1}}
x y : A
hf2 : ↑f (x * y) ≠ ↑f x * ↑f y
UV W : Set B
hUV : IsOpen UV
hW : IsOpen W
hfUV : ↑f x * ↑f y ∈ UV
hfW : ↑f (x * y) ∈ W
h : Disjoint UV W
hB : Continuous fun p => p.fst * p.snd
U V : Set B
hU : IsOpen U
hV : IsOpen V
hfU : ↑f x ∈ U
hfV : ↑f y ∈ V
h' : U ×ˢ V ⊆ (fun p => p.fst * p.snd) ⁻¹' UV
⊢ U * V ≤ UV
[PROOFSTEP]
rintro _ ⟨x, y, hx : (x, y).1 ∈ U, hy : (x, y).2 ∈ V, rfl⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : Monoid D
inst✝⁸ : CommGroup E
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace D
inst✝³ : TopologicalSpace E
inst✝² : TopologicalGroup E
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
f : C(A, B)
hf1 : ¬f ∈ {f | ¬↑f 1 ∈ {1}}
x✝ y✝ : A
hf2 : ↑f (x✝ * y✝) ≠ ↑f x✝ * ↑f y✝
UV W : Set B
hUV : IsOpen UV
hW : IsOpen W
hfUV : ↑f x✝ * ↑f y✝ ∈ UV
hfW : ↑f (x✝ * y✝) ∈ W
h : Disjoint UV W
hB : Continuous fun p => p.fst * p.snd
U V : Set B
hU : IsOpen U
hV : IsOpen V
hfU : ↑f x✝ ∈ U
hfV : ↑f y✝ ∈ V
h' : U ×ˢ V ⊆ (fun p => p.fst * p.snd) ⁻¹' UV
x y : B
hx : (x, y).fst ∈ U
hy : (x, y).snd ∈ V
⊢ (fun x x_1 => x * x_1) x y ∈ UV
[PROOFSTEP]
exact h' ⟨hx, hy⟩
