[GOAL]
M : Type u_1
X : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : TopologicalSpace X
⊢ instTopologicalSpaceUnits = TopologicalSpace.induced val inst✝² ⊓ TopologicalSpace.induced (fun u => ↑u⁻¹) inst✝²
[PROOFSTEP]
simp only [inducing_embedProduct.1, instTopologicalSpaceProd, induced_inf, instTopologicalSpaceMulOpposite,
  induced_compose]
[GOAL]
M : Type u_1
X : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : TopologicalSpace X
⊢ TopologicalSpace.induced (Prod.fst ∘ ↑(embedProduct M)) inst✝² ⊓
      TopologicalSpace.induced ((unop ∘ Prod.snd) ∘ ↑(embedProduct M)) inst✝² =
    TopologicalSpace.induced val inst✝² ⊓ TopologicalSpace.induced (fun u => ↑u⁻¹) inst✝²
[PROOFSTEP]
rfl
[GOAL]
M✝ : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Monoid M✝
inst✝² : TopologicalSpace X
M : Type u_3
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
⊢ Embedding val
[PROOFSTEP]
refine ⟨⟨?_⟩, ext⟩
[GOAL]
M✝ : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Monoid M✝
inst✝² : TopologicalSpace X
M : Type u_3
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
⊢ instTopologicalSpaceUnits = TopologicalSpace.induced val inst✝
[PROOFSTEP]
rw [topology_eq_inf, inf_eq_left, ← continuous_iff_le_induced, @continuous_iff_continuousAt _ _ (.induced _ _)]
[GOAL]
M✝ : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Monoid M✝
inst✝² : TopologicalSpace X
M : Type u_3
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
⊢ ∀ (x : Mˣ), ContinuousAt (fun u => ↑u⁻¹) x
[PROOFSTEP]
intros u s hs
[GOAL]
M✝ : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Monoid M✝
inst✝² : TopologicalSpace X
M : Type u_3
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
u : Mˣ
s : Set M
hs : s ∈ 𝓝 ((fun u => ↑u⁻¹) u)
⊢ s ∈ Filter.map (fun u => ↑u⁻¹) (𝓝 u)
[PROOFSTEP]
simp only [← hf, nhds_induced, Filter.mem_map] at hs ⊢
[GOAL]
M✝ : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Monoid M✝
inst✝² : TopologicalSpace X
M : Type u_3
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
u : Mˣ
s : Set M
hs : s ∈ 𝓝 (f ↑u)
⊢ (fun u => f ↑u) ⁻¹' s ∈ comap val (𝓝 ↑u)
[PROOFSTEP]
exact ⟨_, mem_inf_principal.1 (hc u u.isUnit hs), fun u' hu' ↦ hu' u'.isUnit⟩
[GOAL]
M : Type u_1
X : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : TopologicalSpace X
f : X → Mˣ
⊢ Continuous f ↔ Continuous (val ∘ f) ∧ Continuous fun x => ↑(f x)⁻¹
[PROOFSTEP]
simp only [inducing_embedProduct.continuous_iff, embedProduct_apply, (· ∘ ·), continuous_prod_mk,
  opHomeomorph.symm.inducing.continuous_iff, opHomeomorph_symm_apply, unop_op]
