-- Mathlib/Topology/Algebra/Group/Basic.lean
@[to_additive]
lemma TopologicalGroup.isOpenMap_iff_nhds_one
    {H : Type*} [Monoid H] [TopologicalSpace H] [ContinuousConstSMul H H]
    {F : Type*} [FunLike F G H] [MonoidHomClass F G H] {f : F} :
    IsOpenMap f ↔ 𝓝 1 ≤ .map f (𝓝 1)

Proof state:
G : Type w
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
H : Type u_1
inst✝⁴ : Monoid H
inst✝³ : TopologicalSpace H
inst✝² : ContinuousConstSMul H H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : 𝓝 1 ≤ map (⇑f) (𝓝 1)
x : G
this : map (fun x_1 => f x * x_1) (𝓝 1) = 𝓝 (f x)
⊢ map (fun x_1 => f x * x_1) (𝓝 1) ≤ map (fun x_1 => f (x * x_1)) (𝓝 1)

Tactic:
refine (Filter.map_mono h).trans ?_

Result:
G : Type w
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
H : Type u_1
inst✝⁴ : Monoid H
inst✝³ : TopologicalSpace H
inst✝² : ContinuousConstSMul H H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : 𝓝 1 ≤ map (⇑f) (𝓝 1)
x : G
this : map (fun x_1 => f x * x_1) (𝓝 1) = 𝓝 (f x)
⊢ map (fun x_1 => f x * x_1) (map (⇑f) (𝓝 1)) ≤ map (fun x_1 => f (x * x_1)) (𝓝 1)

Proof state:
G : Type w
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
H : Type u_1
inst✝⁴ : Monoid H
inst✝³ : TopologicalSpace H
inst✝² : ContinuousConstSMul H H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
⊢ IsOpenMap ⇑f ↔ 𝓝 1 ≤ map (⇑f) (𝓝 1)

Tactic:
refine ⟨fun H ↦ map_one f ▸ H.nhds_le 1, fun h ↦ IsOpenMap.of_nhds_le fun x ↦ ?_⟩

Result:
G : Type w
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
H : Type u_1
inst✝⁴ : Monoid H
inst✝³ : TopologicalSpace H
inst✝² : ContinuousConstSMul H H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : 𝓝 1 ≤ map (⇑f) (𝓝 1)
x : G
⊢ 𝓝 (f x) ≤ map (⇑f) (𝓝 x)

Proof state:
G : Type w
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
H : Type u_1
inst✝⁴ : Monoid H
inst✝³ : TopologicalSpace H
inst✝² : ContinuousConstSMul H H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : 𝓝 1 ≤ map (⇑f) (𝓝 1)
x : G
this : map (fun x_1 => f x * x_1) (𝓝 1) = 𝓝 (f x)
⊢ 𝓝 (f x) ≤ map (⇑f) (𝓝 x)

Tactic:
rw [← map_mul_left_nhds_one x, Filter.map_map, Function.comp_def, ← this]

Result:
G : Type w
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
H : Type u_1
inst✝⁴ : Monoid H
inst✝³ : TopologicalSpace H
inst✝² : ContinuousConstSMul H H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : 𝓝 1 ≤ map (⇑f) (𝓝 1)
x : G
this : map (fun x_1 => f x * x_1) (𝓝 1) = 𝓝 (f x)
⊢ map (fun x_1 => f x * x_1) (𝓝 1) ≤ map (fun x_1 => f (x * x_1)) (𝓝 1)

Proof state:
G : Type w
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
H : Type u_1
inst✝⁴ : Monoid H
inst✝³ : TopologicalSpace H
inst✝² : ContinuousConstSMul H H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : 𝓝 1 ≤ map (⇑f) (𝓝 1)
x : G
this : map (fun x_1 => f x * x_1) (𝓝 1) = 𝓝 (f x)
⊢ map (fun x_1 => f x * x_1) (map (⇑f) (𝓝 1)) ≤ map (fun x_1 => f (x * x_1)) (𝓝 1)

Tactic:
simp [Function.comp_def]

Result:
no goals

Proof state:
G : Type w
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
H : Type u_1
inst✝⁴ : Monoid H
inst✝³ : TopologicalSpace H
inst✝² : ContinuousConstSMul H H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : 𝓝 1 ≤ map (⇑f) (𝓝 1)
x : G
⊢ map (fun x_1 => f x * x_1) (𝓝 1) = 𝓝 (f x)

Tactic:
simpa [-Homeomorph.map_nhds_eq, Units.smul_def] using
  (Homeomorph.smul ((toUnits x).map (MonoidHomClass.toMonoidHom f))).map_nhds_eq (1 : H)

Result:
no goals