awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : DiscreteTopology M
⊢ DiscreteTopology.{u_1} Mᵈᵐᵃ

Tactic:
isEmbedding_mk_symm.discreteTopology

Premises used: Topology.IsEmbedding.discreteTopology, DomMulAct.isEmbedding_mk_symm
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : SeparableSpace M
⊢ SeparableSpace.{u_1} Mᵈᵐᵃ

Tactic:
isQuotientMap_mk.separableSpace

Premises used: Topology.IsQuotientMap.separableSpace, DomMulAct.isQuotientMap_mk
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : FirstCountableTopology M
⊢ FirstCountableTopology.{u_1} Mᵈᵐᵃ

Tactic:
isInducing_mk_symm.firstCountableTopology

Premises used: DomMulAct.isInducing_mk_symm, Topology.IsInducing.firstCountableTopology
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : SecondCountableTopology M
⊢ SecondCountableTopology.{u_1} Mᵈᵐᵃ

Tactic:
isInducing_mk_symm.secondCountableTopology

Premises used: DomMulAct.isInducing_mk_symm, Topology.IsInducing.secondCountableTopology
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : CompactSpace M
⊢ CompactSpace.{u_1} Mᵈᵐᵃ

Tactic:
mkHomeomorph.compactSpace

Premises used: DomMulAct.mkHomeomorph, Homeomorph.compactSpace
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : LocallyCompactSpace M
⊢ LocallyCompactSpace.{u_1} Mᵈᵐᵃ

Tactic:
isOpenEmbedding_mk_symm.locallyCompactSpace

Premises used: Topology.IsOpenEmbedding.locallyCompactSpace, DomMulAct.isOpenEmbedding_mk_symm
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : WeaklyLocallyCompactSpace M
⊢ WeaklyLocallyCompactSpace.{u_1} Mᵈᵐᵃ

Tactic:
isClosedEmbedding_mk_symm.weaklyLocallyCompactSpace

Premises used: DomMulAct.isClosedEmbedding_mk_symm, Topology.IsClosedEmbedding.weaklyLocallyCompactSpace
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
x : M
⊢ Eq (α := Filter Mᵈᵐᵃ) (map (⇑mk : (a : M) → Mᵈᵐᵃ) (𝓝 x) : Filter Mᵈᵐᵃ) (𝓝 ((mk : (a : M) → Mᵈᵐᵃ) x) : Filter Mᵈᵐᵃ)

Tactic:
mkHomeomorph.map_nhds_eq x

Premises used: Homeomorph.map_nhds_eq, DomMulAct.mkHomeomorph
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
x : Mᵈᵐᵃ
⊢ Eq (α := Filter M) (map (⇑(Equiv.symm mk) : (a : Mᵈᵐᵃ) → M) (𝓝 x) : Filter M)
    (𝓝 ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) x) : Filter M)

Tactic:
mkHomeomorph.symm.map_nhds_eq x

Premises used: MulOpposite.opEquiv, Homeomorph.map_nhds_eq, DomMulAct.mkHomeomorph, DomMulAct.mk, Homeomorph.symm
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
x : Mᵈᵐᵃ
⊢ Eq (α := Filter M) (comap (⇑mk : (a : M) → Mᵈᵐᵃ) (𝓝 x) : Filter M) (𝓝 ((Equiv.symm mk : (a : Mᵈᵐᵃ) → M) x) : Filter M)

Tactic:
mkHomeomorph.comap_nhds_eq x

Premises used: DomMulAct.mkHomeomorph, Homeomorph.comap_nhds_eq
-- Module: Mathlib.Topology.Algebra.Constructions.DomMulAct
Goal:
M : Type u_1
inst : TopologicalSpace M
x : M
⊢ Eq (α := Filter Mᵈᵐᵃ) (comap (⇑(Equiv.symm mk) : (a : Mᵈᵐᵃ) → M) (𝓝 x) : Filter Mᵈᵐᵃ)
    (𝓝 ((mk : (a : M) → Mᵈᵐᵃ) x) : Filter Mᵈᵐᵃ)

Tactic:
mkHomeomorph.symm.comap_nhds_eq x

Premises used: MulOpposite.opEquiv, DomMulAct.mkHomeomorph, Homeomorph.comap_nhds_eq, DomMulAct.mk, Homeomorph.symm, MulOpposite.op
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
inst : TopologicalSpace M
⊢ Continuous[instTopologicalSpaceMulOpposite, inst] unop

Tactic:
continuous_induced_dom

Premises used: continuous_induced_dom
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
inst : TopologicalSpace M
⊢ Continuous[inst, instTopologicalSpaceMulOpposite] op

Tactic:
continuous_induced_rng.2 continuous_id

Premises used: Iff.mpr, continuous_id, continuous_induced_rng
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : TopologicalSpace M
inst_1 : T2Space M
⊢ T2Space.{u_1} Mᵐᵒᵖ

Tactic:
opHomeomorph.t2Space

Premises used: MulOpposite.opHomeomorph, Homeomorph.t2Space
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : TopologicalSpace M
inst_1 : DiscreteTopology M
⊢ DiscreteTopology.{u_1} Mᵐᵒᵖ

Tactic:
opHomeomorph.symm.isEmbedding.discreteTopology

Premises used: MulOpposite.opHomeomorph, Homeomorph.isEmbedding, Topology.IsEmbedding.discreteTopology, Homeomorph.symm
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : TopologicalSpace M
inst_1 : CompactSpace M
⊢ CompactSpace.{u_1} Mᵐᵒᵖ

Tactic:
opHomeomorph.compactSpace

Premises used: MulOpposite.opHomeomorph, Homeomorph.compactSpace
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : TopologicalSpace M
inst_1 : WeaklyLocallyCompactSpace M
⊢ WeaklyLocallyCompactSpace.{u_1} Mᵐᵒᵖ

Tactic:
opHomeomorph.symm.isClosedEmbedding.weaklyLocallyCompactSpace

Premises used: MulOpposite.opHomeomorph, Homeomorph.symm, Topology.IsClosedEmbedding.weaklyLocallyCompactSpace, Homeomorph.isClosedEmbedding
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : TopologicalSpace M
inst_1 : LocallyCompactSpace M
⊢ LocallyCompactSpace.{u_1} Mᵐᵒᵖ

Tactic:
opHomeomorph.symm.isClosedEmbedding.locallyCompactSpace

Premises used: MulOpposite.opHomeomorph, Homeomorph.symm, Homeomorph.isClosedEmbedding, Topology.IsClosedEmbedding.locallyCompactSpace
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
inst : TopologicalSpace M
x : M
⊢ map op (𝓝 x) = 𝓝 (op x)

Tactic:
opHomeomorph.map_nhds_eq x

Premises used: MulOpposite.opHomeomorph, Homeomorph.map_nhds_eq, MulOpposite.op
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
inst : TopologicalSpace M
x : Mᵐᵒᵖ
⊢ map unop (𝓝 x) = 𝓝 (unop x)

Tactic:
opHomeomorph.symm.map_nhds_eq x

Premises used: MulOpposite.opHomeomorph, MulOpposite, Homeomorph.map_nhds_eq, Homeomorph.symm, MulOpposite.unop
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
inst : TopologicalSpace M
x : Mᵐᵒᵖ
⊢ comap op (𝓝 x) = 𝓝 (unop x)

Tactic:
opHomeomorph.comap_nhds_eq x

Premises used: MulOpposite.opHomeomorph, Homeomorph.comap_nhds_eq, MulOpposite.unop, MulOpposite.op
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
inst : TopologicalSpace M
x : M
⊢ comap unop (𝓝 x) = 𝓝 (op x)

Tactic:
opHomeomorph.symm.comap_nhds_eq x

Premises used: MulOpposite.opHomeomorph, MulOpposite, Homeomorph.comap_nhds_eq, Homeomorph.symm, MulOpposite.unop, MulOpposite.op
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Monoid M
⊢ IsInducing (X := Mˣ) (Y := M × Mᵐᵒᵖ) (⇑(embedProduct M) : (a : Mˣ) → M × Mᵐᵒᵖ)

Tactic:
⟨rfl⟩

Premises used: Topology.IsInducing.mk, rfl
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Monoid M
⊢ IsEmbedding (X := Mˣ) (Y := M × Mᵐᵒᵖ) (⇑(embedProduct M) : (a : Mˣ) → M × Mᵐᵒᵖ)

Tactic:
⟨isInducing_embedProduct, embedProduct_injective M⟩

Premises used: Units.embedProduct_injective, Units.isInducing_embedProduct, Topology.IsEmbedding.mk
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : TopologicalSpace N
inst_3 : Monoid N
inst_4 : TopologicalSpace X
inst_5 : T2Space M
⊢ T2Space.{u_1} Mˣ

Tactic:
isEmbedding_embedProduct.t2Space

Premises used: Units.isEmbedding_embedProduct, Topology.IsEmbedding.t2Space
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : TopologicalSpace N
inst_3 : Monoid N
inst_4 : TopologicalSpace X
inst_5 : DiscreteTopology M
⊢ DiscreteTopology.{u_1} Mˣ

Tactic:
isEmbedding_embedProduct.discreteTopology

Premises used: Units.isEmbedding_embedProduct, Topology.IsEmbedding.discreteTopology
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Monoid M
simp :
  Eq (α := TopologicalSpace Mˣ)
    (TopologicalSpace.induced (Function.comp (β := M × Mᵐᵒᵖ) Prod.fst (⇑(embedProduct M) : (a : Mˣ) → M × Mᵐᵒᵖ)) inst ⊓
      TopologicalSpace.induced
        (Function.comp (β := M × Mᵐᵒᵖ) (unop ∘ Prod.snd) (⇑(embedProduct M) : (a : Mˣ) → M × Mᵐᵒᵖ)) inst)
    (TopologicalSpace.induced val inst ⊓ TopologicalSpace.induced (fun (u : Mˣ) ↦ (↑u⁻¹ : M)) inst)
⊢ Eq (α := TopologicalSpace Mˣ) instTopologicalSpaceUnits
    (TopologicalSpace.induced val inst ⊓ TopologicalSpace.induced (fun (u : Mˣ) ↦ (↑u⁻¹ : M)) inst)

Tactic:
simp only [isInducing_embedProduct.1, instTopologicalSpaceProd, induced_inf,
    instTopologicalSpaceMulOpposite, induced_compose]

Premises used: induced_inf, instTopologicalSpaceProd, induced_compose, MulOpposite.instTopologicalSpaceMulOpposite, Topology.IsInducing.eq_induced, Units.isInducing_embedProduct
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Monoid M
⊢ Eq (α := TopologicalSpace Mˣ)
    (TopologicalSpace.induced (Function.comp (β := M × Mᵐᵒᵖ) Prod.fst (⇑(embedProduct M) : (a : Mˣ) → M × Mᵐᵒᵖ)) inst ⊓
      TopologicalSpace.induced
        (Function.comp (β := M × Mᵐᵒᵖ) (unop ∘ Prod.snd) (⇑(embedProduct M) : (a : Mˣ) → M × Mᵐᵒᵖ)) inst)
    (TopologicalSpace.induced val inst ⊓ TopologicalSpace.induced (fun (u : Mˣ) ↦ (↑u⁻¹ : M)) inst)

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_4
inst : Monoid M
inst_1 : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x : M | IsUnit x}
hf : ∀ (u : Mˣ), f (↑u : M) = (↑u⁻¹ : M)
⊢ IsEmbedding.{u_4, u_4} (X := Mˣ) val

Tactic:
⟨⟨?_⟩, val_injective⟩

Premises used: Topology.IsInducing.mk, Units.val_injective, Topology.IsEmbedding.mk
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_4
inst : Monoid M
inst_1 : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x : M | IsUnit x}
hf : ∀ (u : Mˣ), f (↑u : M) = (↑u⁻¹ : M)
refine : Eq (α := TopologicalSpace Mˣ) instTopologicalSpaceUnits (TopologicalSpace.induced val inst_1)
⊢ IsEmbedding.{u_4, u_4} (X := Mˣ) val

Tactic:
refine ⟨⟨?_⟩, val_injective⟩
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_4
inst : Monoid M
inst_1 : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x : M | IsUnit x}
hf : ∀ (u : Mˣ), f (↑u : M) = (↑u⁻¹ : M)
rw : ∀ (x : Mˣ), ContinuousAt (Y := M) (fun (u : Mˣ) ↦ (↑u⁻¹ : M)) x
⊢ Eq (α := TopologicalSpace Mˣ) instTopologicalSpaceUnits (TopologicalSpace.induced val inst_1)

Tactic:
rw [topology_eq_inf, inf_eq_left, ← continuous_iff_le_induced,
    @continuous_iff_continuousAt _ _ (.induced _ _)]

Premises used: continuous_iff_le_induced, Units.topology_eq_inf, inf_eq_left, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_4
inst : Monoid M
inst_1 : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x : M | IsUnit x}
hf : ∀ (u : Mˣ), f (↑u : M) = (↑u⁻¹ : M)
u : Mˣ
s : Set M
hs : Membership.mem (γ := Filter M) (𝓝 ((fun (u : Mˣ) ↦ (↑u⁻¹ : M)) u)) s
simp :
  ∀ (hs : s ∈ 𝓝 (f (↑u : M))),
    Membership.mem (γ := Filter Mˣ) (comap val (𝓝 (↑u : M))) ((fun (u : Mˣ) ↦ f (↑u : M)) ⁻¹' s)
⊢ Membership.mem (γ := Filter M) (Filter.map (fun (u : Mˣ) ↦ (↑u⁻¹ : M)) (𝓝 u)) s

Tactic:
simp only [← hf, nhds_induced, Filter.mem_map] at hs ⊢

Premises used: nhds_induced, Filter.mem_map
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_4
inst : Monoid M
inst_1 : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x : M | IsUnit x}
hf : ∀ (u : Mˣ), f (↑u : M) = (↑u⁻¹ : M)
u : Mˣ
s : Set M
hs : s ∈ 𝓝 (f (↑u : M))
⊢ Membership.mem (γ := Filter Mˣ) (comap val (𝓝 (↑u : M))) ((fun (u : Mˣ) ↦ f (↑u : M)) ⁻¹' s)

Tactic:
⟨_, mem_inf_principal.1 (hc u u.isUnit hs), fun u' hu' ↦ hu' u'.isUnit⟩

Premises used: Units.val, Set.Mem, setOf, And.intro, Exists.intro, Iff.mp, Filter.mem_inf_principal, Units.isUnit
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_4
inst : Monoid M
inst_1 : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x : M | IsUnit x}
hf : ∀ (u : Mˣ), f (↑u : M) = (↑u⁻¹ : M)
u : Mˣ
s : Set M
hs : s ∈ 𝓝 (f (↑u : M))
⊢ Membership.mem (γ := Filter Mˣ) (comap val (𝓝 (↑u : M))) ((fun (u : Mˣ) ↦ f (↑u : M)) ⁻¹' s)

Tactic:
exact ⟨_, mem_inf_principal.1 (hc u u.isUnit hs), fun u' hu' ↦ hu' u'.isUnit⟩
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_4
inst : DivisionMonoid M
inst_1 : TopologicalSpace M
h : ContinuousOn.{u_4, u_4} (X := M) Inv.inv {x : M | IsUnit x}
⊢ IsEmbedding.{u_4, u_4} (X := Mˣ) val

Tactic:
isEmbedding_val_mk' h fun u ↦ (val_inv_eq_inv_val u).symm

Premises used: Units.val_inv_eq_inv_val, Units.isEmbedding_val_mk', Eq.symm
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Monoid M
⊢ Continuous[instTopologicalSpaceUnits, instTopologicalSpaceProd] (⇑(embedProduct M) : (a : Mˣ) → M × Mᵐᵒᵖ)

Tactic:
continuous_induced_dom

Premises used: continuous_induced_dom
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Monoid M
⊢ Continuous[instTopologicalSpaceUnits, inst] val

Tactic:
(@continuous_embedProduct M _ _).fst

Premises used: Units.continuous_embedProduct, Continuous.fst
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
X : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : TopologicalSpace X
f : X → Mˣ
⊢ Continuous[inst_2, instTopologicalSpaceUnits] f ↔
    Continuous[inst_2, inst] (val ∘ f) ∧ Continuous[inst_2, inst] fun (x : X) ↦ (↑(f x)⁻¹ : M)

Tactic:
simp only [isInducing_embedProduct.continuous_iff, embedProduct_apply, Function.comp_def,
    continuous_prodMk, opHomeomorph.symm.isInducing.continuous_iff, opHomeomorph_symm_apply,
    unop_op]

Premises used: Homeomorph.isInducing, MulOpposite.opHomeomorph, Topology.IsInducing.continuous_iff, Function.comp_def, Homeomorph.symm, MulOpposite.unop_op, MulOpposite.opHomeomorph_symm_apply, continuous_prodMk, Units.isInducing_embedProduct, Units.embedProduct_apply
-- Module: Mathlib.Topology.Algebra.Constructions
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Monoid M
⊢ Continuous[instTopologicalSpaceUnits, inst] fun (u : Mˣ) ↦ (↑u⁻¹ : M)

Tactic:
(Units.continuous_iff.1 continuous_id).2

Premises used: Units.continuous_iff, continuous_id, And.right, Iff.mp
-- 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 : Continuous[inst, inst_2] (⇑f : (a : M) → N)
⊢ Continuous[instTopologicalSpaceUnits, instTopologicalSpaceUnits] (⇑(map f) : (a : Mˣ) → Nˣ)

Tactic:
Units.continuous_iff.mpr ⟨hf.comp continuous_val, hf.comp continuous_coe_inv⟩

Premises used: Iff.mpr, Units.continuous_val, Continuous.comp, Units.continuous_iff, And.intro, Units.continuous_coe_inv
-- 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
⊢ 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))))

Tactic:
have hg_openMap := hf.prodMap <| opHomeomorph.isOpenMap.comp (hf.comp opHomeomorph.symm.isOpenMap)
-- 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))))
⊢ IsOpen[instTopologicalSpaceUnits]
    (Set.image (α := Mˣ) (⇑(map f) : (a : Mˣ) → Nˣ) ((⇑(embedProduct M) : (a : Mˣ) → M × Mᵐᵒᵖ) ⁻¹' U))

Tactic:
⟨_, hg_openMap U hU, Set.ext fun y ↦ ?_⟩

Premises used: Set.ext, And.intro, Exists.intro, IsOpen
-- 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))))
refine :
  ∀ (y : Nˣ),
    Membership.mem (γ := Set Nˣ)
        (Set.preimage (β := N × Nᵐᵒᵖ) (⇑(embedProduct N) : (a : Nˣ) → 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))) ''
            U))
        y ↔
      Membership.mem (γ := Set Nˣ)
        (Set.image (α := Mˣ) (⇑(map f) : (a : Mˣ) → Nˣ) ((⇑(embedProduct M) : (a : Mˣ) → M × Mᵐᵒᵖ) ⁻¹' U)) y
⊢ IsOpen[instTopologicalSpaceUnits]
    (Set.image (α := Mˣ) (⇑(map f) : (a : Mˣ) → Nˣ) ((⇑(embedProduct M) : (a : Mˣ) → M × Mᵐᵒᵖ) ⁻¹' U))

Tactic:
refine ⟨_, hg_openMap U hU, Set.ext fun y ↦ ?_⟩
-- 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ˣ
simp :
  (∃ (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
⊢ Membership.mem (γ := Set Nˣ)
      (Set.preimage (β := N × Nᵐᵒᵖ) (⇑(embedProduct N) : (a : Nˣ) → 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))) ''
          U))
      y ↔
    Membership.mem (γ := Set Nˣ)
      (Set.image (α := Mˣ) (⇑(map f) : (a : Mˣ) → Nˣ) ((⇑(embedProduct M) : (a : Mˣ) → M × Mᵐᵒᵖ) ⁻¹' U)) y

Tactic:
simp only [embedProduct, OneHom.coe_mk, Set.mem_preimage, Set.mem_image, Prod.mk.injEq,
    Prod.map, Prod.exists, MulOpposite.exists, MonoidHom.coe_mk]

Premises used: OneHom.coe_mk, Set.mem_image, MulOpposite.exists, Prod.map, MonoidHom.coe_mk, Prod.mk.injEq, Units.embedProduct, Prod.exists, Set.mem_preimage
-- 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ˣ
h : ∃ (x : Mˣ), ((↑x : M), op (↑x⁻¹ : M)) ∈ U ∧ (map f : (a : Mˣ) → Nˣ) x = y
x : Mˣ
hxV : ((↑x : M), op (↑x⁻¹ : M)) ∈ U
hx : (map f : (a : Mˣ) → Nˣ) x = y
⊢ ((↑x : M), op x.inv) ∈ U ∧
    (f : (a : M) → N) (↑x : M) = (↑y : N) ∧
      Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
          (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M)) (op x.inv) =
        op (↑y⁻¹ : N)

Tactic:
simp [hxV, ← hx]
-- 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ˣ
h_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)

Tactic:
simp_all
-- 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ˣ
h_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) (b * a) : N) ((f : (a : M) → N) 1 : N)

Tactic:
simp_all