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


[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : UniformSpace α
inst✝³ : MonoidWithZero M
inst✝² : Zero α
inst✝¹ : MulActionWithZero M α
inst✝ : UniformContinuousConstSMul M α
src✝ : MulAction M (Completion α) := inferInstance
r : M
⊢ r • 0 = 0
[PROOFSTEP]
rw [← coe_zero, ← coe_smul, MulActionWithZero.smul_zero r]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : UniformSpace α
inst✝³ : MonoidWithZero M
inst✝² : Zero α
inst✝¹ : MulActionWithZero M α
inst✝ : UniformContinuousConstSMul M α
src✝ : MulAction M (Completion α) := inferInstance
a : α
⊢ 0 • ↑α a = 0
[PROOFSTEP]
rw [← coe_smul, zero_smul, coe_zero]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : UniformAddGroup α
src✝¹ : Zero (Completion α) := inferInstance
src✝ : Add (Completion α) := inferInstance
a✝ b✝ c✝ : Completion α
a b c : α
⊢ ↑α a + ↑α b + ↑α c = ↑α a + (↑α b + ↑α c)
[PROOFSTEP]
repeat' rw_mod_cast [add_assoc]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : UniformAddGroup α
src✝¹ : Zero (Completion α) := inferInstance
src✝ : Add (Completion α) := inferInstance
a✝ b✝ c✝ : Completion α
a b c : α
⊢ ↑α a + ↑α b + ↑α c = ↑α a + (↑α b + ↑α c)
[PROOFSTEP]
rw_mod_cast [add_assoc]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : UniformAddGroup α
src✝¹ : Zero (Completion α) := inferInstance
src✝ : Add (Completion α) := inferInstance
a✝ : Completion α
a : α
⊢ 0 + ↑α a = ↑α a
[PROOFSTEP]
rw [← coe_zero, ← coe_add, zero_add]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : UniformAddGroup α
src✝¹ : Zero (Completion α) := inferInstance
src✝ : Add (Completion α) := inferInstance
a✝ : Completion α
a : α
⊢ ↑α a + 0 = ↑α a
[PROOFSTEP]
rw [← coe_zero, ← coe_add, add_zero]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : UniformAddGroup α
src✝¹ : Zero (Completion α) := inferInstance
src✝ : Add (Completion α) := inferInstance
a✝ : Completion α
a : α
⊢ 0 • ↑α a = 0
[PROOFSTEP]
rw [← coe_smul, ← coe_zero, zero_smul]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : UniformAddGroup α
src✝¹ : Zero (Completion α) := inferInstance
src✝ : Add (Completion α) := inferInstance
n : ℕ
a✝ : Completion α
a : α
⊢ (n + 1) • ↑α a = ↑α a + n • ↑α a
[PROOFSTEP]
rw [← coe_smul, succ_nsmul, coe_add, coe_smul]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : UniformAddGroup α
src✝² : AddMonoid (Completion α) := inferInstance
src✝¹ : Neg (Completion α) := inferInstance
src✝ : Sub (Completion α) := inferInstance
a✝ b✝ : Completion α
a b : α
⊢ ↑α a - ↑α b = ↑α a + -↑α b
[PROOFSTEP]
exact_mod_cast congr_arg ((↑) : α → Completion α) (sub_eq_add_neg a b)
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : UniformAddGroup α
src✝² : AddMonoid (Completion α) := inferInstance
src✝¹ : Neg (Completion α) := inferInstance
src✝ : Sub (Completion α) := inferInstance
a✝ : Completion α
a : α
⊢ 0 • ↑α a = 0
[PROOFSTEP]
rw [← coe_smul, ← coe_zero, zero_smul]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : UniformAddGroup α
src✝² : AddMonoid (Completion α) := inferInstance
src✝¹ : Neg (Completion α) := inferInstance
src✝ : Sub (Completion α) := inferInstance
n : ℕ
a✝ : Completion α
a : α
⊢ Int.ofNat (Nat.succ n) • ↑α a = ↑α a + (fun x x_1 => x • x_1) (Int.ofNat n) (↑α a)
[PROOFSTEP]
rw [← coe_smul, show Int.ofNat n.succ • a = a + Int.ofNat n • a from SubNegMonoid.zsmul_succ' n a, coe_add, coe_smul]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : UniformAddGroup α
src✝² : AddMonoid (Completion α) := inferInstance
src✝¹ : Neg (Completion α) := inferInstance
src✝ : Sub (Completion α) := inferInstance
n : ℕ
a✝ : Completion α
a : α
⊢ Int.negSucc n • ↑α a = -(fun x x_1 => x • x_1) (↑(Nat.succ n)) (↑α a)
[PROOFSTEP]
rw [← coe_smul, show (Int.negSucc n) • a = -((n.succ : ℤ) • a) from SubNegMonoid.zsmul_neg' n a, coe_neg, coe_smul]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : UniformAddGroup α
src✝ : SubNegMonoid (Completion α) := inferInstance
a✝ : Completion α
a : α
⊢ -↑α a + ↑α a = 0
[PROOFSTEP]
rw_mod_cast [add_left_neg]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : UniformAddGroup α
src✝ : SubNegMonoid (Completion α) := inferInstance
a✝ : Completion α
a : α
⊢ ↑α 0 = 0
[PROOFSTEP]
rfl
[GOAL]
M✝ : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
M : Type ?u.31551
inst✝² : Monoid M
inst✝¹ : DistribMulAction M α
inst✝ : UniformContinuousConstSMul M α
src✝ : MulAction M (Completion α) := inferInstance
r : M
⊢ r • 0 = 0
[PROOFSTEP]
rw [← coe_zero, ← coe_smul, smul_zero r]
[GOAL]
M✝ : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
M : Type ?u.31551
inst✝² : Monoid M
inst✝¹ : DistribMulAction M α
inst✝ : UniformContinuousConstSMul M α
src✝ : MulAction M (Completion α) := inferInstance
r : M
x y : Completion α
a b : α
⊢ r • (↑α a + ↑α b) = r • ↑α a + r • ↑α b
[PROOFSTEP]
simp only [← coe_add, ← coe_smul, smul_add]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddCommGroup α
inst✝ : UniformAddGroup α
src✝ : AddGroup (Completion α) := inferInstance
a b : Completion α
x y : α
⊢ ↑α x + ↑α y = ↑α y + ↑α x
[PROOFSTEP]
change (x : Completion α) + ↑y = ↑y + ↑x
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddCommGroup α
inst✝ : UniformAddGroup α
src✝ : AddGroup (Completion α) := inferInstance
a b : Completion α
x y : α
⊢ ↑α x + ↑α y = ↑α y + ↑α x
[PROOFSTEP]
rw [← coe_add, ← coe_add, add_comm]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddCommGroup α
inst✝³ : UniformAddGroup α
inst✝² : Semiring R
inst✝¹ : Module R α
inst✝ : UniformContinuousConstSMul R α
src✝¹ : DistribMulAction R (Completion α) := inferInstance
src✝ : MulActionWithZero R (Completion α) := inferInstance
a b : R
x : α
⊢ (a + b) • ↑α x = a • ↑α x + b • ↑α x
[PROOFSTEP]
rw [← coe_smul, add_smul, coe_add, coe_smul, coe_smul]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁷ : UniformSpace α
inst✝⁶ : AddGroup α
inst✝⁵ : UniformAddGroup α
inst✝⁴ : UniformSpace β
inst✝³ : AddGroup β
inst✝² : UniformAddGroup β
inst✝¹ : CompleteSpace β
inst✝ : SeparatedSpace β
f : α →+ β
hf✝ : Continuous ↑f
hf : UniformContinuous ↑f
⊢ Completion.extension (↑f) 0 = 0
[PROOFSTEP]
rw [← coe_zero, extension_coe hf, f.map_zero]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁷ : UniformSpace α
inst✝⁶ : AddGroup α
inst✝⁵ : UniformAddGroup α
inst✝⁴ : UniformSpace β
inst✝³ : AddGroup β
inst✝² : UniformAddGroup β
inst✝¹ : CompleteSpace β
inst✝ : SeparatedSpace β
f : α →+ β
hf✝ : Continuous ↑f
hf : UniformContinuous ↑f
a✝ b✝ : Completion α
a b : α
⊢ Completion.extension (↑f) (↑α a + ↑α b) = Completion.extension (↑f) (↑α a) + Completion.extension (↑f) (↑α b)
[PROOFSTEP]
rw_mod_cast [extension_coe hf, extension_coe hf, extension_coe hf, f.map_add]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
⊢ completion 0 (_ : Continuous fun x => AddZeroClass.toZero.1) = 0
[PROOFSTEP]
ext x
[GOAL]
case h
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
x : Completion α
⊢ ↑(completion 0 (_ : Continuous fun x => AddZeroClass.toZero.1)) x = ↑0 x
[PROOFSTEP]
refine Completion.induction_on x ?_ ?_
[GOAL]
case h.refine_1
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
x : Completion α
⊢ IsClosed {a | ↑(completion 0 (_ : Continuous fun x => AddZeroClass.toZero.1)) a = ↑0 a}
[PROOFSTEP]
apply isClosed_eq (AddMonoidHom.continuous_completion (0 : α →+ β) continuous_const)
[GOAL]
case h.refine_1
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
x : Completion α
⊢ Continuous fun x => ↑0 x
[PROOFSTEP]
simp [continuous_const]
[GOAL]
case h.refine_2
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
x : Completion α
⊢ ∀ (a : α), ↑(completion 0 (_ : Continuous fun x => AddZeroClass.toZero.1)) (↑α a) = ↑0 (↑α a)
[PROOFSTEP]
intro a
[GOAL]
case h.refine_2
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
x : Completion α
a : α
⊢ ↑(completion 0 (_ : Continuous fun x => AddZeroClass.toZero.1)) (↑α a) = ↑0 (↑α a)
[PROOFSTEP]
simp [(0 : α →+ β).completion_coe continuous_const, coe_zero]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁸ : UniformSpace α
inst✝⁷ : AddGroup α
inst✝⁶ : UniformAddGroup α
inst✝⁵ : UniformSpace β
inst✝⁴ : AddGroup β
inst✝³ : UniformAddGroup β
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : UniformAddGroup γ
f g : α →+ γ
hf : Continuous ↑f
hg : Continuous ↑g
⊢ completion (f + g) (_ : Continuous fun x => ↑f x + ↑g x) = completion f hf + completion g hg
[PROOFSTEP]
have hfg := hf.add hg
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁸ : UniformSpace α
inst✝⁷ : AddGroup α
inst✝⁶ : UniformAddGroup α
inst✝⁵ : UniformSpace β
inst✝⁴ : AddGroup β
inst✝³ : UniformAddGroup β
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : UniformAddGroup γ
f g : α →+ γ
hf : Continuous ↑f
hg : Continuous ↑g
hfg : Continuous fun x => ↑f x + ↑g x
⊢ completion (f + g) (_ : Continuous fun x => ↑f x + ↑g x) = completion f hf + completion g hg
[PROOFSTEP]
ext x
[GOAL]
case h
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁸ : UniformSpace α
inst✝⁷ : AddGroup α
inst✝⁶ : UniformAddGroup α
inst✝⁵ : UniformSpace β
inst✝⁴ : AddGroup β
inst✝³ : UniformAddGroup β
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : UniformAddGroup γ
f g : α →+ γ
hf : Continuous ↑f
hg : Continuous ↑g
hfg : Continuous fun x => ↑f x + ↑g x
x : Completion α
⊢ ↑(completion (f + g) (_ : Continuous fun x => ↑f x + ↑g x)) x = ↑(completion f hf + completion g hg) x
[PROOFSTEP]
refine Completion.induction_on x ?_ ?_
[GOAL]
case h.refine_1
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁸ : UniformSpace α
inst✝⁷ : AddGroup α
inst✝⁶ : UniformAddGroup α
inst✝⁵ : UniformSpace β
inst✝⁴ : AddGroup β
inst✝³ : UniformAddGroup β
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : UniformAddGroup γ
f g : α →+ γ
hf : Continuous ↑f
hg : Continuous ↑g
hfg : Continuous fun x => ↑f x + ↑g x
x : Completion α
⊢ IsClosed {a | ↑(completion (f + g) (_ : Continuous fun x => ↑f x + ↑g x)) a = ↑(completion f hf + completion g hg) a}
[PROOFSTEP]
exact isClosed_eq ((f + g).continuous_completion hfg) ((f.continuous_completion hf).add (g.continuous_completion hg))
[GOAL]
case h.refine_2
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁸ : UniformSpace α
inst✝⁷ : AddGroup α
inst✝⁶ : UniformAddGroup α
inst✝⁵ : UniformSpace β
inst✝⁴ : AddGroup β
inst✝³ : UniformAddGroup β
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : UniformAddGroup γ
f g : α →+ γ
hf : Continuous ↑f
hg : Continuous ↑g
hfg : Continuous fun x => ↑f x + ↑g x
x : Completion α
⊢ ∀ (a : α),
    ↑(completion (f + g) (_ : Continuous fun x => ↑f x + ↑g x)) (↑α a) = ↑(completion f hf + completion g hg) (↑α a)
[PROOFSTEP]
intro a
[GOAL]
case h.refine_2
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁸ : UniformSpace α
inst✝⁷ : AddGroup α
inst✝⁶ : UniformAddGroup α
inst✝⁵ : UniformSpace β
inst✝⁴ : AddGroup β
inst✝³ : UniformAddGroup β
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : UniformAddGroup γ
f g : α →+ γ
hf : Continuous ↑f
hg : Continuous ↑g
hfg : Continuous fun x => ↑f x + ↑g x
x : Completion α
a : α
⊢ ↑(completion (f + g) (_ : Continuous fun x => ↑f x + ↑g x)) (↑α a) = ↑(completion f hf + completion g hg) (↑α a)
[PROOFSTEP]
simp [(f + g).completion_coe hfg, coe_add, f.completion_coe hf, g.completion_coe hg]


[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la lb : β
hab : a ≠ b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
[PROOFSTEP]
apply continuousOn_extendFrom
[GOAL]
case hB
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la lb : β
hab : a ≠ b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
⊢ Icc a b ⊆ closure (Ioo a b)
[PROOFSTEP]
rw [closure_Ioo hab]
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la lb : β
hab : a ≠ b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
⊢ ∀ (x : α), x ∈ Icc a b → ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
[PROOFSTEP]
intro x x_in
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la lb : β
hab : a ≠ b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
x : α
x_in : x ∈ Icc a b
⊢ ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
[PROOFSTEP]
rcases eq_endpoints_or_mem_Ioo_of_mem_Icc x_in with (rfl | rfl | h)
[GOAL]
case hf.inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
b : α
la lb : β
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
x : α
hab : x ≠ b
hf : ContinuousOn f (Ioo x b)
ha : Tendsto f (𝓝[Ioi x] x) (𝓝 la)
x_in : x ∈ Icc x b
⊢ ∃ y, Tendsto f (𝓝[Ioo x b] x) (𝓝 y)
[PROOFSTEP]
exact ⟨la, ha.mono_left <| nhdsWithin_mono _ Ioo_subset_Ioi_self⟩
[GOAL]
case hf.inr.inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a : α
la lb : β
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
x : α
hab : a ≠ x
hf : ContinuousOn f (Ioo a x)
hb : Tendsto f (𝓝[Iio x] x) (𝓝 lb)
x_in : x ∈ Icc a x
⊢ ∃ y, Tendsto f (𝓝[Ioo a x] x) (𝓝 y)
[PROOFSTEP]
exact ⟨lb, hb.mono_left <| nhdsWithin_mono _ Ioo_subset_Iio_self⟩
[GOAL]
case hf.inr.inr
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la lb : β
hab : a ≠ b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
x : α
x_in : x ∈ Icc a b
h : x ∈ Ioo a b
⊢ ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
[PROOFSTEP]
exact ⟨f x, hf x h⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
la : β
hab : a < b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
⊢ extendFrom (Ioo a b) f a = la
[PROOFSTEP]
apply extendFrom_eq
[GOAL]
case hx
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
la : β
hab : a < b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
⊢ a ∈ closure (Ioo a b)
[PROOFSTEP]
rw [closure_Ioo hab.ne]
[GOAL]
case hx
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
la : β
hab : a < b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
⊢ a ∈ Icc a b
[PROOFSTEP]
simp only [le_of_lt hab, left_mem_Icc, right_mem_Icc]
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
la : β
hab : a < b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
⊢ Tendsto f (𝓝[Ioo a b] a) (𝓝 la)
[PROOFSTEP]
simpa [hab]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
lb : β
hab : a < b
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
⊢ extendFrom (Ioo a b) f b = lb
[PROOFSTEP]
apply extendFrom_eq
[GOAL]
case hx
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
lb : β
hab : a < b
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
⊢ b ∈ closure (Ioo a b)
[PROOFSTEP]
rw [closure_Ioo hab.ne]
[GOAL]
case hx
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
lb : β
hab : a < b
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
⊢ b ∈ Icc a b
[PROOFSTEP]
simp only [le_of_lt hab, left_mem_Icc, right_mem_Icc]
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
lb : β
hab : a < b
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
⊢ Tendsto f (𝓝[Ioo a b] b) (𝓝 lb)
[PROOFSTEP]
simpa [hab]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ico a b)
[PROOFSTEP]
apply continuousOn_extendFrom
[GOAL]
case hB
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
⊢ Ico a b ⊆ closure (Ioo a b)
[PROOFSTEP]
rw [closure_Ioo hab.ne]
[GOAL]
case hB
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
⊢ Ico a b ⊆ Icc a b
[PROOFSTEP]
exact Ico_subset_Icc_self
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
⊢ ∀ (x : α), x ∈ Ico a b → ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
[PROOFSTEP]
intro x x_in
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
x : α
x_in : x ∈ Ico a b
⊢ ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
[PROOFSTEP]
rcases eq_left_or_mem_Ioo_of_mem_Ico x_in with (rfl | h)
[GOAL]
case hf.inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
b : α
la : β
x : α
hab : x < b
hf : ContinuousOn f (Ioo x b)
ha : Tendsto f (𝓝[Ioi x] x) (𝓝 la)
x_in : x ∈ Ico x b
⊢ ∃ y, Tendsto f (𝓝[Ioo x b] x) (𝓝 y)
[PROOFSTEP]
use la
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
b : α
la : β
x : α
hab : x < b
hf : ContinuousOn f (Ioo x b)
ha : Tendsto f (𝓝[Ioi x] x) (𝓝 la)
x_in : x ∈ Ico x b
⊢ Tendsto f (𝓝[Ioo x b] x) (𝓝 la)
[PROOFSTEP]
simpa [hab]
[GOAL]
case hf.inr
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
x : α
x_in : x ∈ Ico a b
h : x ∈ Ioo a b
⊢ ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
[PROOFSTEP]
exact ⟨f x, hf x h⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
lb : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)
[PROOFSTEP]
have := @continuousOn_Ico_extendFrom_Ioo αᵒᵈ _ _ _ _ _ _ _ f _ _ lb hab
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
lb : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
this : ContinuousOn f (Ioo b a) → Tendsto f (𝓝[Ioi b] b) (𝓝 lb) → ContinuousOn (extendFrom (Ioo b a) f) (Ico b a)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)
[PROOFSTEP]
erw [dual_Ico, dual_Ioi, dual_Ioo] at this
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
lb : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
this :
  ContinuousOn f (↑OrderDual.ofDual ⁻¹' Ioo a b) →
    Tendsto f (𝓝[↑OrderDual.ofDual ⁻¹' Iio b] b) (𝓝 lb) →
      ContinuousOn (extendFrom (↑OrderDual.ofDual ⁻¹' Ioo a b) f) (↑OrderDual.ofDual ⁻¹' Ioc a b)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)
[PROOFSTEP]
exact this hf hb


[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝² : DivInvMonoid G₀
inst✝¹ : TopologicalSpace G₀
inst✝ : ContinuousMul G₀
f : α → G₀
s : Set α
l : Filter α
x : G₀
hf : Tendsto f l (𝓝 x)
y : G₀
⊢ Tendsto (fun a => f a / y) l (𝓝 (x / y))
[PROOFSTEP]
simpa only [div_eq_mul_inv] using hf.mul tendsto_const_nhds
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝³ : DivInvMonoid G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : ContinuousMul G₀
f : α → G₀
s : Set α
l : Filter α
inst✝ : TopologicalSpace α
hf : ContinuousOn f s
y : G₀
⊢ ContinuousOn (fun x => f x / y) s
[PROOFSTEP]
simpa only [div_eq_mul_inv] using hf.mul continuousOn_const
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝³ : DivInvMonoid G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : ContinuousMul G₀
f : α → G₀
s : Set α
l : Filter α
inst✝ : TopologicalSpace α
hf : Continuous f
y : G₀
⊢ Continuous fun x => f x / y
[PROOFSTEP]
simpa only [div_eq_mul_inv] using hf.mul continuous_const
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
f g : α → G₀
l : Filter α
a b : G₀
hf : Tendsto f l (𝓝 a)
hg : Tendsto g l (𝓝 b)
hy : b ≠ 0
⊢ Tendsto (f / g) l (𝓝 (a / b))
[PROOFSTEP]
simpa only [div_eq_mul_inv] using hf.mul (hg.inv₀ hy)
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : HasContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝ : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
⊢ Tendsto (fun n => f n * g n) l (𝓝 (x * y)) ↔ Tendsto f l (𝓝 x)
[PROOFSTEP]
refine' ⟨fun hfg => _, fun hf => hf.mul hg⟩
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : HasContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝ : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
hfg : Tendsto (fun n => f n * g n) l (𝓝 (x * y))
⊢ Tendsto f l (𝓝 x)
[PROOFSTEP]
rw [← mul_div_cancel x hy]
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : HasContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝ : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
hfg : Tendsto (fun n => f n * g n) l (𝓝 (x * y))
⊢ Tendsto f l (𝓝 (x * y / y))
[PROOFSTEP]
refine' Tendsto.congr' _ (hfg.div hg hy)
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : HasContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝ : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
hfg : Tendsto (fun n => f n * g n) l (𝓝 (x * y))
⊢ (fun n => f n * g n) / g =ᶠ[l] f
[PROOFSTEP]
refine' (hg.eventually_ne hy).mono fun n hn => mul_div_cancel _ hn
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : HasContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
f g : α → G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
a : α
hf : Continuous f
hg : Continuous g
h₀ : ∀ (x : α), g x ≠ 0
⊢ Continuous (f / g)
[PROOFSTEP]
simpa only [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : HasContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt (↿h) (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
⊢ ContinuousAt (fun x => h x (f x / g x)) a
[PROOFSTEP]
show ContinuousAt (↿h ∘ fun x => (x, f x / g x)) a
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : HasContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt (↿h) (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
⊢ ContinuousAt (↿h ∘ fun x => (x, f x / g x)) a
[PROOFSTEP]
by_cases hga : g a = 0
[GOAL]
case pos
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : HasContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt (↿h) (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
hga : g a = 0
⊢ ContinuousAt (↿h ∘ fun x => (x, f x / g x)) a
[PROOFSTEP]
rw [ContinuousAt]
[GOAL]
case pos
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : HasContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt (↿h) (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
hga : g a = 0
⊢ Tendsto (↿h ∘ fun x => (x, f x / g x)) (𝓝 a) (𝓝 ((↿h ∘ fun x => (x, f x / g x)) a))
[PROOFSTEP]
simp_rw [comp_apply, hga, div_zero]
[GOAL]
case pos
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : HasContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt (↿h) (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
hga : g a = 0
⊢ Tendsto (↿h ∘ fun x => (x, f x / g x)) (𝓝 a) (𝓝 ((↿h) (a, 0)))
[PROOFSTEP]
exact (h2h hga).comp (continuousAt_id.prod_mk tendsto_top)
[GOAL]
case neg
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : HasContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
f✝ g✝ : α → G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt (↿h) (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
hga : ¬g a = 0
⊢ ContinuousAt (↿h ∘ fun x => (x, f x / g x)) a
[PROOFSTEP]
exact ContinuousAt.comp (hh hga) (continuousAt_id.prod (hf.div hg hga))
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : ContinuousMul G₀
a : G₀
ha : a ≠ 0
⊢ map (fun x => a * x) (𝓝 1) = 𝓝 a
[PROOFSTEP]
rw [map_mul_left_nhds₀ ha, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : ContinuousMul G₀
a : G₀
ha : a ≠ 0
⊢ map (fun x => x * a) (𝓝 1) = 𝓝 a
[PROOFSTEP]
rw [map_mul_right_nhds₀ ha, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : ContinuousMul G₀
a : G₀
ha : a ≠ 0
⊢ 𝓝 (↑(Homeomorph.symm (Homeomorph.symm (Homeomorph.mulRight₀ a ha))) 1) = 𝓝 a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : ContinuousMul G₀
a : G₀
h : Tendsto Inv.inv (𝓝 1) (𝓝 1)
x : G₀
hx : x ≠ 0
⊢ ContinuousAt Inv.inv x
[PROOFSTEP]
have hx' := inv_ne_zero hx
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : ContinuousMul G₀
a : G₀
h : Tendsto Inv.inv (𝓝 1) (𝓝 1)
x : G₀
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ ContinuousAt Inv.inv x
[PROOFSTEP]
rw [ContinuousAt, ← map_mul_left_nhds_one₀ hx, ← nhds_translation_mul_inv₀ hx', tendsto_map'_iff, tendsto_comap_iff]
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : ContinuousMul G₀
a : G₀
h : Tendsto Inv.inv (𝓝 1) (𝓝 1)
x : G₀
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ Tendsto ((fun x_1 => x_1 * x⁻¹⁻¹) ∘ Inv.inv ∘ fun x_1 => x * x_1) (𝓝 1) (𝓝 1)
[PROOFSTEP]
simpa only [(· ∘ ·), mul_inv_rev, mul_inv_cancel_right₀ hx']
[GOAL]
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℤ
h : x ≠ 0 ∨ 0 ≤ m
⊢ ContinuousAt (fun x => x ^ m) x
[PROOFSTEP]
cases' m with m m
[GOAL]
case ofNat
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.ofNat m
⊢ ContinuousAt (fun x => x ^ Int.ofNat m) x
[PROOFSTEP]
simpa only [Int.ofNat_eq_coe, zpow_coe_nat] using continuousAt_pow x m
[GOAL]
case negSucc
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
⊢ ContinuousAt (fun x => x ^ Int.negSucc m) x
[PROOFSTEP]
simp only [zpow_negSucc]
[GOAL]
case negSucc
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
⊢ ContinuousAt (fun x => (x ^ (m + 1))⁻¹) x
[PROOFSTEP]
have hx : x ≠ 0 := h.resolve_right (Int.negSucc_lt_zero m).not_le
[GOAL]
case negSucc
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
hx : x ≠ 0
⊢ ContinuousAt (fun x => (x ^ (m + 1))⁻¹) x
[PROOFSTEP]
exact (continuousAt_pow x (m + 1)).inv₀ (pow_ne_zero _ hx)


[GOAL]
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hS : ∀ (ε : G), ε > 0 → ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
⊢ Dense ↑S
[PROOFSTEP]
cases subsingleton_or_nontrivial G
[GOAL]
case inl
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hS : ∀ (ε : G), ε > 0 → ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
h✝ : Subsingleton G
⊢ Dense ↑S
[PROOFSTEP]
refine fun x => _root_.subset_closure ?_
[GOAL]
case inl
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hS : ∀ (ε : G), ε > 0 → ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
h✝ : Subsingleton G
x : G
⊢ x ∈ ↑S
[PROOFSTEP]
rw [Subsingleton.elim x 0]
[GOAL]
case inl
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hS : ∀ (ε : G), ε > 0 → ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
h✝ : Subsingleton G
x : G
⊢ 0 ∈ ↑S
[PROOFSTEP]
exact zero_mem S
[GOAL]
case inr
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hS : ∀ (ε : G), ε > 0 → ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
h✝ : Nontrivial G
⊢ Dense ↑S
[PROOFSTEP]
refine dense_of_exists_between fun a b hlt => ?_
[GOAL]
case inr
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hS : ∀ (ε : G), ε > 0 → ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
h✝ : Nontrivial G
a b : G
hlt : a < b
⊢ ∃ c, c ∈ ↑S ∧ a < c ∧ c < b
[PROOFSTEP]
rcases hS (b - a) (sub_pos.2 hlt) with ⟨g, hgS, hg0, hg⟩
[GOAL]
case inr.intro.intro.intro
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hS : ∀ (ε : G), ε > 0 → ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
h✝ : Nontrivial G
a b : G
hlt : a < b
g : G
hgS : g ∈ S
hg0 : 0 < g
hg : g < b - a
⊢ ∃ c, c ∈ ↑S ∧ a < c ∧ c < b
[PROOFSTEP]
rcases(existsUnique_add_zsmul_mem_Ioc hg0 0 a).exists with ⟨m, hm⟩
[GOAL]
case inr.intro.intro.intro.intro
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hS : ∀ (ε : G), ε > 0 → ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
h✝ : Nontrivial G
a b : G
hlt : a < b
g : G
hgS : g ∈ S
hg0 : 0 < g
hg : g < b - a
m : ℤ
hm : 0 + m • g ∈ Ioc a (a + g)
⊢ ∃ c, c ∈ ↑S ∧ a < c ∧ c < b
[PROOFSTEP]
rw [zero_add] at hm
[GOAL]
case inr.intro.intro.intro.intro
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hS : ∀ (ε : G), ε > 0 → ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
h✝ : Nontrivial G
a b : G
hlt : a < b
g : G
hgS : g ∈ S
hg0 : 0 < g
hg : g < b - a
m : ℤ
hm : m • g ∈ Ioc a (a + g)
⊢ ∃ c, c ∈ ↑S ∧ a < c ∧ c < b
[PROOFSTEP]
refine ⟨m • g, zsmul_mem hgS _, hm.1, hm.2.trans_lt ?_⟩
[GOAL]
case inr.intro.intro.intro.intro
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hS : ∀ (ε : G), ε > 0 → ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
h✝ : Nontrivial G
a b : G
hlt : a < b
g : G
hgS : g ∈ S
hg0 : 0 < g
hg : g < b - a
m : ℤ
hm : m • g ∈ Ioc a (a + g)
⊢ a + g < b
[PROOFSTEP]
rwa [lt_sub_iff_add_lt'] at hg
[GOAL]
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hbot : S ≠ ⊥
H : ¬∃ a, IsLeast {g | g ∈ S ∧ 0 < g} a
⊢ Dense ↑S
[PROOFSTEP]
refine S.dense_of_not_isolated_zero fun ε ε0 => ?_
[GOAL]
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hbot : S ≠ ⊥
H : ¬∃ a, IsLeast {g | g ∈ S ∧ 0 < g} a
ε : G
ε0 : ε > 0
⊢ ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
[PROOFSTEP]
contrapose! H
[GOAL]
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hbot : S ≠ ⊥
ε : G
ε0 : ε > 0
H : ∀ (g : G), g ∈ S → ¬g ∈ Ioo 0 ε
⊢ ∃ a, IsLeast {g | g ∈ S ∧ 0 < g} a
[PROOFSTEP]
exact exists_isLeast_pos hbot ε0 (disjoint_left.2 H)
[GOAL]
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
⊢ Dense ↑S ∨ ∃ a, S = closure {a}
[PROOFSTEP]
refine (em _).imp (dense_of_not_isolated_zero S) fun h => ?_
[GOAL]
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
h : ¬∀ (ε : G), ε > 0 → ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
⊢ ∃ a, S = closure {a}
[PROOFSTEP]
push_neg at h
[GOAL]
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
h : ∃ ε, ε > 0 ∧ ∀ (g : G), g ∈ S → ¬g ∈ Ioo 0 ε
⊢ ∃ a, S = closure {a}
[PROOFSTEP]
rcases h with ⟨ε, ε0, hε⟩
[GOAL]
case intro.intro
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
ε : G
ε0 : ε > 0
hε : ∀ (g : G), g ∈ S → ¬g ∈ Ioo 0 ε
⊢ ∃ a, S = closure {a}
[PROOFSTEP]
exact cyclic_of_isolated_zero ε0 (disjoint_left.2 hε)


[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : OrderedCommGroup α
inst✝ : ContinuousConstSMul α α
s : Set α
h : IsUpperSet s
x y : α
hxy : x ≤ y
hx : x ∈ closure s
⊢ y ∈ closure ((y / x) • s)
[PROOFSTEP]
rw [closure_smul]
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : OrderedCommGroup α
inst✝ : ContinuousConstSMul α α
s : Set α
h : IsUpperSet s
x y : α
hxy : x ≤ y
hx : x ∈ closure s
⊢ y ∈ (y / x) • closure s
[PROOFSTEP]
exact ⟨x, hx, div_mul_cancel' _ _⟩
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : OrderedCommGroup α
inst✝ : ContinuousConstSMul α α
s : Set α
h : IsLowerSet s
x y : α
hxy : y ≤ x
hx : x ∈ closure s
⊢ y ∈ closure ((y / x) • s)
[PROOFSTEP]
rw [closure_smul]
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : OrderedCommGroup α
inst✝ : ContinuousConstSMul α α
s : Set α
h : IsLowerSet s
x y : α
hxy : y ≤ x
hx : x ∈ closure s
⊢ y ∈ (y / x) • closure s
[PROOFSTEP]
exact ⟨x, hx, div_mul_cancel' _ _⟩
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : OrderedCommGroup α
inst✝ : ContinuousConstSMul α α
s : Set α
hs : IsOpen s
⊢ IsOpen ↑(upperClosure s)
[PROOFSTEP]
rw [← mul_one s, ← mul_upperClosure]
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : OrderedCommGroup α
inst✝ : ContinuousConstSMul α α
s : Set α
hs : IsOpen s
⊢ IsOpen (s * ↑(upperClosure 1))
[PROOFSTEP]
exact hs.mul_right
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : OrderedCommGroup α
inst✝ : ContinuousConstSMul α α
s : Set α
hs : IsOpen s
⊢ IsOpen ↑(lowerClosure s)
[PROOFSTEP]
rw [← mul_one s, ← mul_lowerClosure]
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : OrderedCommGroup α
inst✝ : ContinuousConstSMul α α
s : Set α
hs : IsOpen s
⊢ IsOpen (s * ↑(lowerClosure 1))
[PROOFSTEP]
exact hs.mul_right
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : HasUpperLowerClosure α
s : Set α
h : IsUpperSet s
⊢ IsUpperSet (interior s)
[PROOFSTEP]
rw [← isLowerSet_compl, ← closure_compl]
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : HasUpperLowerClosure α
s : Set α
h : IsUpperSet s
⊢ IsLowerSet (closure sᶜ)
[PROOFSTEP]
exact h.compl.closure
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : HasUpperLowerClosure α
s : Set α
h : OrdConnected s
⊢ OrdConnected (interior s)
[PROOFSTEP]
rw [← h.upperClosure_inter_lowerClosure, interior_inter]
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : HasUpperLowerClosure α
s : Set α
h : OrdConnected s
⊢ OrdConnected (interior ↑(upperClosure s) ∩ interior ↑(lowerClosure s))
[PROOFSTEP]
exact (upperClosure s).upper.interior.ordConnected.inter (lowerClosure s).lower.interior.ordConnected


[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Preorder Y
inst✝ : OrderClosedTopology Y
f g : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure s)
⊢ IsLocalMaxOn f (closure s) a
[PROOFSTEP]
rcases mem_nhdsWithin.1 h with ⟨U, Uo, aU, hU⟩
[GOAL]
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Preorder Y
inst✝ : OrderClosedTopology Y
f g : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure s)
U : Set X
Uo : IsOpen U
aU : a ∈ U
hU : U ∩ s ⊆ {x | (fun x => f x ≤ f a) x}
⊢ IsLocalMaxOn f (closure s) a
[PROOFSTEP]
refine' mem_nhdsWithin.2 ⟨U, Uo, aU, _⟩
[GOAL]
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Preorder Y
inst✝ : OrderClosedTopology Y
f g : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure s)
U : Set X
Uo : IsOpen U
aU : a ∈ U
hU : U ∩ s ⊆ {x | (fun x => f x ≤ f a) x}
⊢ U ∩ closure s ⊆ {x | (fun x => f x ≤ f a) x}
[PROOFSTEP]
rintro x ⟨hxU, hxs⟩
[GOAL]
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Preorder Y
inst✝ : OrderClosedTopology Y
f g : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure s)
U : Set X
Uo : IsOpen U
aU : a ∈ U
hU : U ∩ s ⊆ {x | (fun x => f x ≤ f a) x}
x : X
hxU : x ∈ U
hxs : x ∈ closure s
⊢ x ∈ {x | (fun x => f x ≤ f a) x}
[PROOFSTEP]
refine' ContinuousWithinAt.closure_le _ _ continuousWithinAt_const hU
[GOAL]
case intro.intro.intro.intro.refine'_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Preorder Y
inst✝ : OrderClosedTopology Y
f g : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure s)
U : Set X
Uo : IsOpen U
aU : a ∈ U
hU : U ∩ s ⊆ {x | (fun x => f x ≤ f a) x}
x : X
hxU : x ∈ U
hxs : x ∈ closure s
⊢ x ∈ closure (U ∩ s)
[PROOFSTEP]
rwa [mem_closure_iff_nhdsWithin_neBot, nhdsWithin_inter_of_mem, ← mem_closure_iff_nhdsWithin_neBot]
[GOAL]
case intro.intro.intro.intro.refine'_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Preorder Y
inst✝ : OrderClosedTopology Y
f g : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure s)
U : Set X
Uo : IsOpen U
aU : a ∈ U
hU : U ∩ s ⊆ {x | (fun x => f x ≤ f a) x}
x : X
hxU : x ∈ U
hxs : x ∈ closure s
⊢ U ∈ 𝓝[s] x
[PROOFSTEP]
exact nhdsWithin_le_nhds (Uo.mem_nhds hxU)
[GOAL]
case intro.intro.intro.intro.refine'_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Preorder Y
inst✝ : OrderClosedTopology Y
f g : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure s)
U : Set X
Uo : IsOpen U
aU : a ∈ U
hU : U ∩ s ⊆ {x | (fun x => f x ≤ f a) x}
x : X
hxU : x ∈ U
hxs : x ∈ closure s
⊢ ContinuousWithinAt f (U ∩ s) x
[PROOFSTEP]
exact (hc _ hxs).mono ((inter_subset_right _ _).trans subset_closure)