awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
x : X
g : G
U : Set G
hU : U ∈ 𝓝 g
this : Eq (α := G → X) (fun (x_1 : G) ↦ x_1 • x) ((fun (x_1 : G) ↦ x_1 • g • x) ∘ fun (x : G) ↦ x * g⁻¹)
hU₁ : Membership.mem (γ := Filter G) (𝓝 1) ((fun (x : G) ↦ x * g⁻¹) '' U)
⊢ HSMul.hSMul (α := Set G) (β := Set X) ((fun (x : G) ↦ x * g⁻¹) '' U) {g • x} ∈ 𝓝 (g • x)

Tactic:
apply smul_singleton_mem_nhds_of_sigmaCompact

Premises used: smul_singleton_mem_nhds_of_sigmaCompact
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
x : X
g : G
U : Set G
hU : U ∈ 𝓝 g
this : Eq (α := G → X) (fun (x_1 : G) ↦ x_1 • x) ((fun (x_1 : G) ↦ x_1 • g • x) ∘ fun (x : G) ↦ x * g⁻¹)
⊢ Membership.mem (γ := Filter G) (𝓝 1) ((fun (x : G) ↦ x * g⁻¹) '' U)

Tactic:
simpa using isOpenMap_mul_right g⁻¹ |>.image_mem_nhds hU

Premises used: IsOpenMap.image_mem_nhds, isOpenMap_mul_right, Inv.inv
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : SigmaCompactSpace G
H : Type u_3
inst_4 : Group H
inst_5 : TopologicalSpace H
inst_6 : BaireSpace H
inst_7 : T2Space H
inst_8 : ContinuousMul H
f : G →* H
hf : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
h'f : Continuous[inst, inst_5] (⇑f : (a : G) → H)
A : MulAction G H := MulAction.compHom H f
⊢ ContinuousSMul G H

Tactic:
have : ContinuousSMul G H := continuousSMul_compHom h'f
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : SigmaCompactSpace G
H : Type u_3
inst_4 : Group H
inst_5 : TopologicalSpace H
inst_6 : BaireSpace H
inst_7 : T2Space H
inst_8 : ContinuousMul H
f : G →* H
hf : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
h'f : Continuous[inst, inst_5] (⇑f : (a : G) → H)
A : MulAction G H := MulAction.compHom H f
this : ContinuousSMul G H
⊢ IsPretransitive G H

Tactic:
have : IsPretransitive G H := isPretransitive_compHom hf
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : SigmaCompactSpace G
H : Type u_3
inst_4 : Group H
inst_5 : TopologicalSpace H
inst_6 : BaireSpace H
inst_7 : T2Space H
inst_8 : ContinuousMul H
f : G →* H
hf : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
h'f : Continuous[inst, inst_5] (⇑f : (a : G) → H)
A : MulAction G H := MulAction.compHom H f
this_1 : ContinuousSMul G H
this : IsPretransitive G H
⊢ Eq (α := (a : G) → H) (⇑f : (a : G) → H) fun (g : G) ↦ HSMul.hSMul (β := H) g 1

Tactic:
simp [A, MulAction.compHom_smul_def]

Premises used: MulAction.compHom_smul_def
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : SigmaCompactSpace G
H : Type u_3
inst_4 : Group H
inst_5 : TopologicalSpace H
inst_6 : BaireSpace H
inst_7 : T2Space H
inst_8 : ContinuousMul H
f : G →* H
hf : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
h'f : Continuous[inst, inst_5] (⇑f : (a : G) → H)
A : MulAction G H := MulAction.compHom H f
this_1 : ContinuousSMul G H
this : IsPretransitive G H
⊢ Eq (α := (a : G) → H) (⇑f : (a : G) → H) fun (g : G) ↦ HSMul.hSMul (β := H) g 1

Tactic:
have : f = (fun (g : G) ↦ g • (1 : H)) := by simp [A, MulAction.compHom_smul_def]
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : SigmaCompactSpace G
H : Type u_3
inst_4 : Group H
inst_5 : TopologicalSpace H
inst_6 : BaireSpace H
inst_7 : T2Space H
inst_8 : ContinuousMul H
f : G →* H
hf : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
h'f : Continuous[inst, inst_5] (⇑f : (a : G) → H)
A : MulAction G H := MulAction.compHom H f
this_1 : ContinuousSMul G H
this_2 : IsPretransitive G H
this : Eq (α := (a : G) → H) (⇑f : (a : G) → H) fun (g : G) ↦ HSMul.hSMul (β := H) g 1
rw : IsOpenMap.{u_1, u_3} (Y := H) fun (g : G) ↦ HSMul.hSMul (β := H) g 1
⊢ IsOpenMap.{u_1, u_3} (X := G) (Y := H) (⇑f : (a : G) → H)

Tactic:
rw [this]
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : SigmaCompactSpace G
H : Type u_3
inst_4 : Group H
inst_5 : TopologicalSpace H
inst_6 : BaireSpace H
inst_7 : T2Space H
inst_8 : ContinuousMul H
f : G →* H
hf : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
h'f : Continuous[inst, inst_5] (⇑f : (a : G) → H)
A : MulAction G H := MulAction.compHom H f
this_1 : ContinuousSMul G H
this_2 : IsPretransitive G H
this : Eq (α := (a : G) → H) (⇑f : (a : G) → H) fun (g : G) ↦ HSMul.hSMul (β := H) g 1
⊢ IsOpenMap.{u_1, u_3} (Y := H) fun (g : G) ↦ HSMul.hSMul (β := H) g 1

Tactic:
isOpenMap_smul_of_sigmaCompact _

Premises used: isOpenMap_smul_of_sigmaCompact
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : SigmaCompactSpace G
H : Type u_3
inst_4 : Group H
inst_5 : TopologicalSpace H
inst_6 : BaireSpace H
inst_7 : T2Space H
inst_8 : ContinuousMul H
f : G →* H
hf : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
h'f : Continuous[inst, inst_5] (⇑f : (a : G) → H)
A : MulAction G H := MulAction.compHom H f
this_1 : ContinuousSMul G H
this_2 : IsPretransitive G H
this : Eq (α := (a : G) → H) (⇑f : (a : G) → H) fun (g : G) ↦ HSMul.hSMul (β := H) g 1
⊢ IsOpenMap.{u_1, u_3} (Y := H) fun (g : G) ↦ HSMul.hSMul (β := H) g 1

Tactic:
exact isOpenMap_smul_of_sigmaCompact _

Premises used: isOpenMap_smul_of_sigmaCompact
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
β : Type v
inst : TopologicalSpace β
inst_1 : Group α
inst_2 : MulAction α β
inst_3 : ContinuousConstSMul α β
s : Set α
t : Set β
inst_4 : TopologicalSpace α
⊢ interior s • interior t ⊆ interior (s • t)

Tactic:
(Set.smul_subset_smul_right interior_subset).trans subset_interior_smul_right

Premises used: interior_subset, HasSubset.Subset.trans, subset_interior_smul_right, Set.smul_subset_smul_right
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Group α
inst_3 : MulAction α β
inst_4 : ContinuousInv α
inst_5 : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed[inst_1] t
hs : IsCompact s
x : Prod.{u, v} (↑s : Type u) β
⊢ (fun (gx : Prod.{u, v} (↑s : Type u) β) ↦ (gx.1, (↑gx.1 : α)⁻¹ • gx.2))
      ((fun (gx : Prod.{u, v} (↑s : Type u) β) ↦ (gx.1, (↑gx.1 : α) • gx.2)) x) =
    x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Group α
inst_3 : MulAction α β
inst_4 : ContinuousInv α
inst_5 : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed[inst_1] t
hs : IsCompact s
x : Prod.{u, v} (↑s : Type u) β
⊢ (fun (gx : Prod.{u, v} (↑s : Type u) β) ↦ (gx.1, (↑gx.1 : α) • gx.2))
      ((fun (gx : Prod.{u, v} (↑s : Type u) β) ↦ (gx.1, (↑gx.1 : α)⁻¹ • gx.2)) x) =
    x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Group α
inst_3 : MulAction α β
inst_4 : ContinuousInv α
inst_5 : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed[inst_1] t
hs : IsCompact s
Φ : Prod.{u, v} (↑s : Type u) β ≃ₜ Prod.{u, v} (↑s : Type u) β :=
  { toFun := fun (gx : Prod.{u, v} (↑s : Type u) β) ↦ (gx.1, (↑gx.1 : α) • gx.2),
    invFun := fun (gx : Prod.{u, v} (↑s : Type u) β) ↦ (gx.1, (↑gx.1 : α)⁻¹ • gx.2), left_inv := ⋯, right_inv := ⋯,
    continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ s • t =
    image (α := Prod.{u, v} (↑s : Type u) β)
      (comp (β := Prod.{u, v} (↑s : Type u) β) snd (⇑Φ : (a : (↑s : Type u) × β) → (↑s : Type u) × β)) (snd ⁻¹' t)

Tactic:
have : s • t = (snd ∘ Φ) '' snd ⁻¹' t :=
    subset_antisymm
      (smul_subset_iff.mpr fun g hg x hx ↦ mem_image_of_mem (snd ∘ Φ) (x := ⟨⟨g, hg⟩, x⟩) hx)
      (image_subset_iff.mpr fun ⟨⟨g, hg⟩, x⟩ hx ↦ smul_mem_smul hg hx)
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Group α
inst_3 : MulAction α β
inst_4 : ContinuousInv α
inst_5 : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed[inst_1] t
hs : IsCompact s
Φ : Prod.{u, v} (↑s : Type u) β ≃ₜ Prod.{u, v} (↑s : Type u) β :=
  { toFun := fun (gx : Prod.{u, v} (↑s : Type u) β) ↦ (gx.1, (↑gx.1 : α) • gx.2),
    invFun := fun (gx : Prod.{u, v} (↑s : Type u) β) ↦ (gx.1, (↑gx.1 : α)⁻¹ • gx.2), left_inv := ⋯, right_inv := ⋯,
    continuous_toFun := ⋯, continuous_invFun := ⋯ }
this :
  s • t =
    image (α := Prod.{u, v} (↑s : Type u) β)
      (comp (β := Prod.{u, v} (↑s : Type u) β) snd (⇑Φ : (a : (↑s : Type u) × β) → (↑s : Type u) × β)) (snd ⁻¹' t)
rw :
  IsClosed[inst_1]
    (image (α := Prod.{u, v} (↑s : Type u) β)
      (comp (β := Prod.{u, v} (↑s : Type u) β) snd (⇑Φ : (a : (↑s : Type u) × β) → (↑s : Type u) × β)) (snd ⁻¹' t))
⊢ IsClosed[inst_1] (s • t)

Tactic:
rw [this]
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Group α
inst_3 : MulAction α β
inst_4 : ContinuousInv α
inst_5 : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed[inst_1] t
hs : IsCompact s
Φ : Prod.{u, v} (↑s : Type u) β ≃ₜ Prod.{u, v} (↑s : Type u) β :=
  { toFun := fun (gx : Prod.{u, v} (↑s : Type u) β) ↦ (gx.1, (↑gx.1 : α) • gx.2),
    invFun := fun (gx : Prod.{u, v} (↑s : Type u) β) ↦ (gx.1, (↑gx.1 : α)⁻¹ • gx.2), left_inv := ⋯, right_inv := ⋯,
    continuous_toFun := ⋯, continuous_invFun := ⋯ }
this :
  s • t =
    image (α := Prod.{u, v} (↑s : Type u) β)
      (comp (β := Prod.{u, v} (↑s : Type u) β) snd (⇑Φ : (a : (↑s : Type u) × β) → (↑s : Type u) × β)) (snd ⁻¹' t)
⊢ CompactSpace.{u} (↑s : Type u)

Tactic:
have : CompactSpace s := isCompact_iff_compactSpace.mp hs
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Group α
inst_3 : MulAction α β
inst_4 : ContinuousInv α
inst_5 : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed[inst_1] t
hs : IsCompact s
Φ : Prod.{u, v} (↑s : Type u) β ≃ₜ Prod.{u, v} (↑s : Type u) β :=
  { toFun := fun (gx : Prod.{u, v} (↑s : Type u) β) ↦ (gx.1, (↑gx.1 : α) • gx.2),
    invFun := fun (gx : Prod.{u, v} (↑s : Type u) β) ↦ (gx.1, (↑gx.1 : α)⁻¹ • gx.2), left_inv := ⋯, right_inv := ⋯,
    continuous_toFun := ⋯, continuous_invFun := ⋯ }
this_1 :
  s • t =
    image (α := Prod.{u, v} (↑s : Type u) β)
      (comp (β := Prod.{u, v} (↑s : Type u) β) snd (⇑Φ : (a : (↑s : Type u) × β) → (↑s : Type u) × β)) (snd ⁻¹' t)
this : CompactSpace.{u} (↑s : Type u)
⊢ IsClosed[inst_1]
    (image (α := Prod.{u, v} (↑s : Type u) β)
      (comp (β := Prod.{u, v} (↑s : Type u) β) snd (⇑Φ : (a : (↑s : Type u) × β) → (↑s : Type u) × β)) (snd ⁻¹' t))

Tactic:
(isProperMap_snd_of_compactSpace.comp Φ.isProperMap).isClosedMap _
    (ht.preimage continuous_snd)

Premises used: isProperMap_snd_of_compactSpace, IsProperMap.isClosedMap, Homeomorph.isProperMap, continuous_snd, IsClosed.preimage, IsProperMap.comp
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Group α
inst_3 : MulAction α β
inst_4 : ContinuousInv α
inst_5 : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed[inst_1] t
hs : IsCompact s
Φ : Prod.{u, v} (↑s : Type u) β ≃ₜ Prod.{u, v} (↑s : Type u) β :=
  { toFun := fun (gx : Prod.{u, v} (↑s : Type u) β) ↦ (gx.1, (↑gx.1 : α) • gx.2),
    invFun := fun (gx : Prod.{u, v} (↑s : Type u) β) ↦ (gx.1, (↑gx.1 : α)⁻¹ • gx.2), left_inv := ⋯, right_inv := ⋯,
    continuous_toFun := ⋯, continuous_invFun := ⋯ }
this_1 :
  s • t =
    image (α := Prod.{u, v} (↑s : Type u) β)
      (comp (β := Prod.{u, v} (↑s : Type u) β) snd (⇑Φ : (a : (↑s : Type u) × β) → (↑s : Type u) × β)) (snd ⁻¹' t)
this : CompactSpace.{u} (↑s : Type u)
⊢ IsClosed[inst_1]
    (image (α := Prod.{u, v} (↑s : Type u) β)
      (comp (β := Prod.{u, v} (↑s : Type u) β) snd (⇑Φ : (a : (↑s : Type u) × β) → (↑s : Type u) × β)) (snd ⁻¹' t))

Tactic:
exact (isProperMap_snd_of_compactSpace.comp Φ.isProperMap).isClosedMap _
    (ht.preimage continuous_snd)

Premises used: isProperMap_snd_of_compactSpace, IsProperMap.isClosedMap, Homeomorph.isProperMap, continuous_snd, IsClosed.preimage, IsProperMap.comp
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Group α
inst_3 : MulAction α β
inst_4 : ContinuousInv α
inst_5 : ContinuousSMul α β
inst_6 : CompactSpace α
t : Set β
ht : IsClosed[inst_1] t
rw : IsClosed[inst_1] (⋃ (g : α), (fun (x : β) ↦ g • x) '' t)
⊢ IsClosed[instTopologicalSpaceQuotient] (Quotient.mk' '' t)

Tactic:
rw [← isQuotientMap_quotient_mk'.isClosed_preimage,
    MulAction.quotient_preimage_image_eq_union_mul]

Premises used: isQuotientMap_quotient_mk', Topology.IsCoinducing.isClosed_preimage, Topology.IsQuotientMap.isCoinducing, MulAction.quotient_preimage_image_eq_union_mul
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Group α
inst_3 : MulAction α β
inst_4 : ContinuousInv α
inst_5 : ContinuousSMul α β
inst_6 : CompactSpace α
t : Set β
ht : IsClosed[inst_1] t
⊢ IsClosed[inst_1] (HSMul.hSMul.{u, v, v} (α := Set α) univ t)

Tactic:
ht.smul_left_of_isCompact (isCompact_univ (X := α))

Premises used: IsClosed.smul_left_of_isCompact, isCompact_univ
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Group α
inst_3 : MulAction α β
inst_4 : ContinuousInv α
inst_5 : ContinuousSMul α β
inst_6 : CompactSpace α
t : Set β
ht : IsClosed[inst_1] t
h : ⋃ (g : α), (fun (x : β) ↦ g • x) '' t = HSMul.hSMul.{u, v, v} (α := Set α) univ t
⊢ IsClosed[inst_1] (⋃ (g : α), (fun (x : β) ↦ g • x) '' t)

Tactic:
convert! ht.smul_left_of_isCompact (isCompact_univ (X := α))

Premises used: IsClosed.smul_left_of_isCompact, isCompact_univ
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Group α
inst_3 : MulAction α β
inst_4 : ContinuousInv α
inst_5 : ContinuousSMul α β
inst_6 : CompactSpace α
t : Set β
ht : IsClosed[inst_1] t
h :
  Eq.{v + 1} (α := Set β) (⋃ (x : α), ⋃ (_ : Membership.mem (γ := Set α) univ x), (fun (x_1 : β) ↦ x • x_1) '' t)
    (⋃ (a : α), ⋃ (_ : Membership.mem (γ := Set α) univ a), a • t)
⊢ ⋃ (g : α), (fun (x : β) ↦ g • x) '' t = HSMul.hSMul.{u, v, v} (α := Set α) univ t

Tactic:
rw [← biUnion_univ, ← iUnion_smul_left_image]

Premises used: Set.biUnion_univ, Set.iUnion_smul_left_image
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Group α
inst_3 : MulAction α β
inst_4 : ContinuousInv α
inst_5 : ContinuousSMul α β
inst_6 : CompactSpace α
t : Set β
ht : IsClosed[inst_1] t
⊢ Eq.{v + 1} (α := Set β) (⋃ (x : α), ⋃ (_ : Membership.mem (γ := Set α) univ x), (fun (x_1 : β) ↦ x • x_1) '' t)
    (⋃ (a : α), ⋃ (_ : Membership.mem (γ := Set α) univ a), a • t)

Tactic:
simp only [image_smul]

Premises used: Set.image_smul
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : ContinuousConstSMul α α
s t : Set α
⊢ IsOpen[inst] t → IsOpen[inst] (s * t)

Tactic:
IsOpen.smul_left

Premises used: IsOpen.smul_left
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : ContinuousConstSMul α α
s t : Set α
⊢ s * interior t ⊆ interior (s * t)

Tactic:
subset_interior_smul_right

Premises used: subset_interior_smul_right
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : ContinuousConstSMul α α
s t : Set α
⊢ interior s * interior t ⊆ interior (s * t)

Tactic:
subset_interior_smul

Premises used: subset_interior_smul
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : ContinuousConstSMul α α
s : Set α
a b : α
h : s ∈ 𝓝 b
rwa : {a} * s ∈ 𝓝 (a • b)
rwa₁ : HSMul.hSMul (α := Set α) {a} s ∈ 𝓝 (a • b)
rwa₂ : a • s ∈ 𝓝 (a • b)
rwa₃ rwa₄ rwa₅ rwa₆ : s ∈ 𝓝 b
⊢ {a} * s ∈ 𝓝 (a * b)

Tactic:
rwa [← smul_eq_mul, ← smul_eq_mul, singleton_smul, smul_mem_nhds_smul_iff]

Premises used: Set.singleton_smul, smul_mem_nhds_smul_iff, smul_eq_mul
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : ContinuousConstSMul α α
s : Set α
a : α
h : Membership.mem (γ := Filter α) (𝓝 1) s
⊢ {a} * s ∈ 𝓝 a

Tactic:
simpa only [mul_one] using singleton_mul_mem_nhds a h

Premises used: singleton_mul_mem_nhds, mul_one
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : ContinuousConstSMul αᵐᵒᵖ α
s t : Set α
hs : IsOpen[inst] s
rw : IsOpen[inst] (op '' t • s)
⊢ IsOpen[inst] (s * t)

Tactic:
rw [← image_op_smul]

Premises used: Set.image_op_smul
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : ContinuousConstSMul αᵐᵒᵖ α
s t : Set α
hs : IsOpen[inst] s
⊢ IsOpen[inst] (op '' t • s)

Tactic:
hs.smul_left

Premises used: IsOpen.smul_left
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : ContinuousConstSMul αᵐᵒᵖ α
s t : Set α
hs : IsOpen[inst] s
⊢ IsOpen[inst] (op '' t • s)

Tactic:
exact hs.smul_left

Premises used: IsOpen.smul_left
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : ContinuousConstSMul αᵐᵒᵖ α
s t : Set α
⊢ interior s * t ⊆ interior (s * t)

Tactic:
interior_maximal (Set.mul_subset_mul_right interior_subset) isOpen_interior.mul_right

Premises used: interior_subset, isOpen_interior, interior_maximal, Set.mul_subset_mul_right, IsOpen.mul_right
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : ContinuousConstSMul αᵐᵒᵖ α
s t : Set α
⊢ interior s * interior t ⊆ interior (s * t)

Tactic:
(Set.mul_subset_mul_left interior_subset).trans subset_interior_mul_left

Premises used: subset_interior_mul_left, interior_subset, HasSubset.Subset.trans, Set.mul_subset_mul_left
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : ContinuousConstSMul αᵐᵒᵖ α
s : Set α
a b : α
h : s ∈ 𝓝 b
rw : (fun (x : α) ↦ x * a) '' s ∈ 𝓝 (b * a)
⊢ s * {a} ∈ 𝓝 (b * a)

Tactic:
rw [mul_singleton]

Premises used: Set.mul_singleton
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : ContinuousConstSMul αᵐᵒᵖ α
s : Set α
a b : α
h : s ∈ 𝓝 b
⊢ (fun (x : α) ↦ x * a) '' s ∈ 𝓝 (b * a)

Tactic:
smul_mem_nhds_smul (op a) h

Premises used: Set.Mem, smul_mem_nhds_smul, MulOpposite.unop, MulOpposite.op
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : ContinuousConstSMul αᵐᵒᵖ α
s : Set α
a b : α
h : s ∈ 𝓝 b
⊢ (fun (x : α) ↦ x * a) '' s ∈ 𝓝 (b * a)

Tactic:
exact smul_mem_nhds_smul (op a) h

Premises used: smul_mem_nhds_smul, MulOpposite.op
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : ContinuousConstSMul αᵐᵒᵖ α
s : Set α
a : α
h : Membership.mem (γ := Filter α) (𝓝 1) s
⊢ s * {a} ∈ 𝓝 a

Tactic:
simpa only [one_mul] using mul_singleton_mem_nhds a h

Premises used: mul_singleton_mem_nhds, one_mul
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s t : Set G
ht : IsOpen[inst] t
rw : IsOpen[inst] (⋃ a ∈ s, (fun (x : G) ↦ a / x) '' t)
⊢ IsOpen[inst] (s / t)

Tactic:
rw [← iUnion_div_left_image]

Premises used: Set.iUnion_div_left_image
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s t : Set G
ht : IsOpen[inst] t
⊢ IsOpen[inst] (⋃ a ∈ s, (fun (x : G) ↦ a / x) '' t)

Tactic:
isOpen_biUnion fun a _ => isOpenMap_div_left a t ht

Premises used: isOpenMap_div_left, isOpen_biUnion
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s t : Set G
ht : IsOpen[inst] t
⊢ IsOpen[inst] (⋃ a ∈ s, (fun (x : G) ↦ a / x) '' t)

Tactic:
exact isOpen_biUnion fun a _ => isOpenMap_div_left a t ht

Premises used: isOpenMap_div_left, isOpen_biUnion
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s t : Set G
hs : IsOpen[inst] s
rw : IsOpen[inst] (⋃ a ∈ t, (fun (x : G) ↦ x / a) '' s)
⊢ IsOpen[inst] (s / t)

Tactic:
rw [← iUnion_div_right_image]

Premises used: Set.iUnion_div_right_image
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s t : Set G
hs : IsOpen[inst] s
⊢ IsOpen[inst] (⋃ a ∈ t, (fun (x : G) ↦ x / a) '' s)

Tactic:
isOpen_biUnion fun a _ => isOpenMap_div_right a s hs

Premises used: isOpenMap_div_right, isOpen_biUnion
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s t : Set G
hs : IsOpen[inst] s
⊢ IsOpen[inst] (⋃ a ∈ t, (fun (x : G) ↦ x / a) '' s)

Tactic:
exact isOpen_biUnion fun a _ => isOpenMap_div_right a s hs

Premises used: isOpenMap_div_right, isOpen_biUnion
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s t : Set G
⊢ interior s / t ⊆ interior (s / t)

Tactic:
interior_maximal (div_subset_div_right interior_subset) isOpen_interior.div_right

Premises used: interior_subset, isOpen_interior, Set.div_subset_div_right, interior_maximal, IsOpen.div_right
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s t : Set G
⊢ s / interior t ⊆ interior (s / t)

Tactic:
interior_maximal (div_subset_div_left interior_subset) isOpen_interior.div_left

Premises used: IsOpen.div_left, interior_subset, isOpen_interior, Set.div_subset_div_left, interior_maximal
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s t : Set G
⊢ interior s / interior t ⊆ interior (s / t)

Tactic:
(div_subset_div_left interior_subset).trans subset_interior_div_left

Premises used: interior_subset, Set.div_subset_div_left, HasSubset.Subset.trans, subset_interior_div_left
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s : Set G
hs : IsOpen[inst] s
t : Set G
⊢ s * closure[inst] t = s * t

Tactic:
(mul_subset_iff.2 fun a ha b hb => ?_).antisymm (mul_subset_mul_left subset_closure)

Premises used: Iff.mpr, subset_closure, Set.mul_subset_iff, HasSubset.Subset.antisymm, Set.mul_subset_mul_left