-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : TopologicalSpace N
inst_3 : Monoid N
f : M →* N
hf_inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hf : IsOpenMap.{u_1, u_2} (X := M) (Y := N) (⇑f : (a : M) → N)
U : Set (M × Mᵐᵒᵖ)
hU : IsOpen[inferInstance] U
hg_openMap :
  IsOpenMap.{u_1, u_2} (X := M × Mᵐᵒᵖ) (Y := N × Nᵐᵒᵖ)
    (Prod.map (⇑f : (a : M) → N)
      (Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
        (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M))))
y : Nˣ
refine_1 :
  (∃ (a : M) (a_1 : M),
      (a, op a_1) ∈ U ∧
        (f : (a : M) → N) a = (↑y : N) ∧
          Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
              (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M)) (op a_1) =
            op (↑y⁻¹ : N)) →
    ∀ (a b : M) (h : (a, op b) ∈ U) (ha : (f : (a : M) → N) a = (↑y : N))
      (hb :
        Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
            (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M)) (op b) =
          op (↑y⁻¹ : N)),
      Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (a * b) : N) ((f : (a : M) → N) 1 : N)
refine_2 :
  (∃ (a : M) (a_1 : M),
      (a, op a_1) ∈ U ∧
        (f : (a : M) → N) a = (↑y : N) ∧
          Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
              (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M)) (op a_1) =
            op (↑y⁻¹ : N)) →
    ∀ (a b : M) (h : (a, op b) ∈ U) (ha : (f : (a : M) → N) a = (↑y : N))
      (hb :
        Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
            (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M)) (op b) =
          op (↑y⁻¹ : N)),
      Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (b * a) : N) ((f : (a : M) → N) 1 : N)
refine_3 :
  (∃ (a : M) (a_1 : M),
      (a, op a_1) ∈ U ∧
        (f : (a : M) → N) a = (↑y : N) ∧
          Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
              (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M)) (op a_1) =
            op (↑y⁻¹ : N)) →
    ∀ (a b : M) (h : (a, op b) ∈ U) (ha : (f : (a : M) → N) a = (↑y : N))
      (hb :
        Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
            (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M)) (op b) =
          op (↑y⁻¹ : N)),
      ((↑{ val := a, inv := b, val_inv := ⋯, inv_val := ⋯ : Mˣ } : M),
            op (↑{ val := a, inv := b, val_inv := ⋯, inv_val := ⋯ : Mˣ }⁻¹ : M)) ∈
          U ∧
        (map f : (a : Mˣ) → Nˣ) { val := a, inv := b, val_inv := ⋯, inv_val := ⋯ } = y
⊢ (∃ (a : M) (a_1 : M),
      (a, op a_1) ∈ U ∧
        (f : (a : M) → N) a = (↑y : N) ∧
          Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
              (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M)) (op a_1) =
            op (↑y⁻¹ : N)) ↔
    ∃ (x : Mˣ), ((↑x : M), op (↑x⁻¹ : M)) ∈ U ∧ (map f : (a : Mˣ) → Nˣ) x = y

Tactic:
refine ⟨fun ⟨a, b, h, ha, hb⟩ ↦ ⟨⟨a, b, hf_inj ?_, hf_inj ?_⟩, ?_⟩,
    fun ⟨x, hxV, hx⟩ ↦ ⟨x, x.inv, by simp [hxV, ← hx]⟩⟩