awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : SMul M α
inst_2 : ContinuousConstSMul M α
inst_3 : TopologicalSpace β
g : β → α
s : Set β
hg : ContinuousOn g s
c : M
⊢ ContinuousOn.{u_3, u_2} (Y := α) (fun (x : β) ↦ c • g x) s

Tactic:
fun x hx => (hg x hx).const_smul c

Premises used: ContinuousWithinAt.const_smul, ContinuousOn
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : SMul M α
inst_2 : ContinuousConstSMul M α
inst_3 : TopologicalSpace β
g : β → α
hg : Continuous[inst_3, inst] g
c : M
⊢ Continuous[inst_3, inst] fun (x : β) ↦ c • g x

Tactic:
(continuous_const_smul _).comp hg

Premises used: ContinuousConstSMul.continuous_const_smul, Continuous.comp
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : SMul M α
inst_2 : ContinuousConstSMul M α
inst_3 : TopologicalSpace β
g : β → α
b : β
s : Set β
inst_4 : SMul.{u_1, u_2} Mᵐᵒᵖ α
inst_5 : IsCentralScalar M α
c : M
⊢ Continuous[inst, inst] fun (x : α) ↦ MulOpposite.op c • x

Tactic:
simpa only [op_smul_eq_smul] using continuous_const_smul c

Premises used: ContinuousConstSMul.continuous_const_smul, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : SMul M α
inst_2 : ContinuousConstSMul M α
inst_3 : TopologicalSpace β
g : β → α
b : β
s : Set β
⊢ ContinuousConstSMul.{u_1, u_2} M αᵐᵒᵖ

Tactic:
⟨fun c => MulOpposite.continuous_op.comp <| MulOpposite.continuous_unop.const_smul c⟩

Premises used: Continuous.comp, MulOpposite.continuous_unop, ContinuousConstSMul.mk, Continuous.const_smul, MulOpposite.continuous_op
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : SMul M α
inst_2 : ContinuousConstSMul M α
inst_3 : TopologicalSpace β
g : β → α
b : β
s : Set β
inst_4 : SMul M β
inst_5 : ContinuousConstSMul M β
⊢ ContinuousConstSMul M (α × β)

Tactic:
⟨fun _ => (continuous_fst.const_smul _).prodMk (continuous_snd.const_smul _)⟩

Premises used: continuous_snd, continuous_fst, ContinuousConstSMul.mk, Continuous.const_smul, Continuous.prodMk
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : SMul M α
inst_2 : ContinuousConstSMul M α
inst_3 : TopologicalSpace β
g : β → α
b : β
s : Set β
ι : Type u_4
γ : ι → Type u_5
inst_4 : (i : ι) → TopologicalSpace (γ i)
inst_5 : (i : ι) → SMul.{u_1, u_5} M (γ i)
inst_6 : ∀ (i : ι), ContinuousConstSMul.{u_1, u_5} M (γ i)
⊢ ContinuousConstSMul M ((i : ι) → γ i)

Tactic:
⟨fun _ => continuous_pi fun i => (continuous_apply i).const_smul _⟩

Premises used: continuous_pi, ContinuousConstSMul.mk, continuous_apply, Continuous.const_smul
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_4
β : Type u_5
inst : SMul α β
inst_1 : TopologicalSpace β
inst_2 : ContinuousConstSMul α β
a : α
s : Set β
hs : IsCompact s
⊢ IsCompact (a • s)

Tactic:
hs.image (continuous_id.const_smul a)

Premises used: continuous_id, IsCompact.image, Continuous.const_smul
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : SMul M α
inst_2 : ContinuousConstSMul M α
x y : α
h : x ⤳ y
c : M
⊢ (c • x) ⤳ (c • y)

Tactic:
h.map (continuous_const_smul c)

Premises used: ContinuousConstSMul.continuous_const_smul, Specializes.map
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : SMul M α
inst_2 : ContinuousConstSMul M α
x y : α
h : Inseparable x y
c : M
⊢ Inseparable (c • x) (c • y)

Tactic:
h.map (continuous_const_smul c)

Premises used: ContinuousConstSMul.continuous_const_smul, Inseparable.map
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : SMul M α
inst_2 : ContinuousConstSMul M α
N : Type u_4
β : Type u_5
inst_3 : SMul N β
inst_4 : TopologicalSpace β
g : β → α
hg : IsInducing g
f : N → M
hf : ∀ {c : N} {x : β}, g (c • x) = f c • g x
c : N
⊢ Continuous[inst_4, inst_4] fun (x : β) ↦ c • x

Tactic:
simpa only [Function.comp_def, hf, hg.continuous_iff] using hg.continuous.const_smul (f c)

Premises used: Topology.IsInducing.continuous_iff, Function.comp_def, Topology.IsInducing.continuous, Continuous.const_smul
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : SMul M α
inst_2 : ContinuousConstSMul M α
c : M
s : Set α
⊢ c • closure[inst] s ⊆ closure[inst] (c • s)

Tactic:
((Set.mapsTo_image _ _).closure <| continuous_const_smul c).image_subset

Premises used: ContinuousConstSMul.continuous_const_smul, Set.MapsTo.closure, Set.mapsTo_image, Set.MapsTo.image_subset
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : SMul M α
inst_2 : ContinuousConstSMul M α
s : Set M
t : Set α
simp : Subset.{u_2} (α := Set α) (⋃ a ∈ s, a • closure[inst] t) (closure[inst] (⋃ a ∈ s, a • t))
⊢ s • closure[inst] t ⊆ closure[inst] (s • t)

Tactic:
simp only [← iUnion_smul_set]

Premises used: Set.iUnion_smul_set
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : SMul M α
inst_2 : ContinuousConstSMul M α
s : Set M
t : Set α
⊢ Subset.{u_2} (α := Set α) (⋃ a ∈ s, a • closure[inst] t) (closure[inst] (⋃ a ∈ s, a • t))

Tactic:
iUnion₂_subset fun c hc ↦ (smul_closure_subset c t).trans <| closure_mono <|
    subset_biUnion_of_mem (u := (· • t)) hc

Premises used: Set.iUnion₂_subset, Set.subset_biUnion_of_mem, HasSubset.Subset.trans, closure_mono, smul_closure_subset
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : SMul M α
inst_2 : ContinuousConstSMul M α
s : Set M
t : Set α
⊢ Subset.{u_2} (α := Set α) (⋃ a ∈ s, a • closure[inst] t) (closure[inst] (⋃ a ∈ s, a • t))

Tactic:
exact iUnion₂_subset fun c hc ↦ (smul_closure_subset c t).trans <| closure_mono <|
    subset_biUnion_of_mem (u := (· • t)) hc

Premises used: Set.iUnion₂_subset, Set.subset_biUnion_of_mem, HasSubset.Subset.trans, closure_mono, smul_closure_subset
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
N : Type u_4
α : Type u_5
β : Type u_6
inst : SMul M α
inst_1 : SMul N β
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : ContinuousConstSMul N β
σ : M → N
simp : IsClosed[Pi.topologicalSpace] (⋂ (i : M), ⋂ (i_1 : α), {x : α → β | x (i • i_1) = σ i • x i_1})
⊢ IsClosed[Pi.topologicalSpace] {f : α → β | ∀ (c : M) (x : α), f (c • x) = σ c • f x}

Tactic:
simp only [Set.setOf_forall]

Premises used: Set.setOf_forall
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
N : Type u_4
α : Type u_5
β : Type u_6
inst : SMul M α
inst_1 : SMul N β
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : ContinuousConstSMul N β
σ : M → N
⊢ IsClosed[Pi.topologicalSpace] (⋂ (i : M), ⋂ (i_1 : α), {x : α → β | x (i • i_1) = σ i • x i_1})

Tactic:
isClosed_iInter fun c => isClosed_iInter fun x =>
    isClosed_eq (continuous_apply _) ((continuous_apply _).const_smul _)

Premises used: isClosed_eq, isClosed_iInter
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
N : Type u_4
α : Type u_5
β : Type u_6
inst : SMul M α
inst_1 : SMul N β
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : ContinuousConstSMul N β
σ : M → N
⊢ IsClosed[Pi.topologicalSpace] (⋂ (i : M), ⋂ (i_1 : α), {x : α → β | x (i • i_1) = σ i • x i_1})

Tactic:
exact isClosed_iInter fun c => isClosed_iInter fun x =>
    isClosed_eq (continuous_apply _) ((continuous_apply _).const_smul _)

Premises used: isClosed_eq, continuous_apply, Continuous.const_smul, isClosed_iInter
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
inst_3 : ContinuousConstSMul M α
c : M
x : α
⊢ c • closure[inst] (MulAction.orbit M x) ⊆ closure[inst] (MulAction.orbit M x)

Tactic:
(smul_closure_subset c _).trans <| closure_mono <| MulAction.smul_orbit_subset _ _

Premises used: HasSubset.Subset.trans, MulAction.smul_orbit_subset, closure_mono, smul_closure_subset
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
β : Type u_3
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
f : β → α
l : Filter β
a : α
c : G
h : Tendsto (fun (x : β) ↦ c • f x) l (𝓝 (c • a))
⊢ Tendsto f l (𝓝 a)

Tactic:
simpa only [inv_smul_smul] using h.const_smul c⁻¹

Premises used: inv_smul_smul, Filter.Tendsto.const_smul, Inv.inv
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
β : Type u_3
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
inst_4 : TopologicalSpace β
f : β → α
b : β
s : Set β
c : G
⊢ ContinuousWithinAt.{u_3, u_2} (Y := α) (fun (x : β) ↦ c • f x) s b ↔ ContinuousWithinAt f s b

Tactic:
tendsto_const_smul_iff c

Premises used: ContinuousWithinAt, tendsto_const_smul_iff
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
β : Type u_3
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
inst_4 : TopologicalSpace β
f : β → α
s : Set β
c : G
⊢ ContinuousOn.{u_3, u_2} (Y := α) (fun (x : β) ↦ c • f x) s ↔ ContinuousOn f s

Tactic:
forall₂_congr fun _ _ => continuousWithinAt_const_smul_iff c

Premises used: continuousWithinAt_const_smul_iff, forall₂_congr, ContinuousOn
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
β : Type u_3
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
inst_4 : TopologicalSpace β
f : β → α
b : β
c : G
⊢ ContinuousAt.{u_3, u_2} (Y := α) (fun (x : β) ↦ c • f x) b ↔ ContinuousAt f b

Tactic:
tendsto_const_smul_iff c

Premises used: ContinuousAt, tendsto_const_smul_iff
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
β : Type u_3
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
inst_4 : TopologicalSpace β
f : β → α
c : G
⊢ (Continuous[inst_4, inst] fun (x : β) ↦ c • f x) ↔ Continuous[inst_4, inst] f

Tactic:
simp only [continuous_iff_continuousAt, continuousAt_const_smul_iff]

Premises used: continuous_iff_continuousAt, continuousAt_const_smul_iff
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
c : G
⊢ IsHomeomorph (Y := α) fun (x : α) ↦ c • x

Tactic:
(Homeomorph.smul c).isHomeomorph

Premises used: Homeomorph.smul, Homeomorph.isHomeomorph
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
c : G
⊢ IsOpenMap (Y := α) fun (x : α) ↦ c • x

Tactic:
(Homeomorph.smul c).isOpenMap

Premises used: Homeomorph.smul, Homeomorph.isOpenMap
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
s : Set α
hs : IsOpen[inst] s
c : G
⊢ IsOpen[inst] (c • s)

Tactic:
isOpenMap_smul c s hs

Premises used: isOpenMap_smul
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
c : G
⊢ IsClosedMap (Y := α) fun (x : α) ↦ c • x

Tactic:
(Homeomorph.smul c).isClosedMap

Premises used: Homeomorph.smul, Homeomorph.isClosedMap
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
s : Set α
hs : IsClosed[inst] s
c : G
⊢ IsClosed[inst] (c • s)

Tactic:
isClosedMap_smul c s hs

Premises used: isClosedMap_smul
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
c : G
s : Set α
⊢ closure[inst] (c • s) = c • closure[inst] s

Tactic:
((Homeomorph.smul c).image_closure s).symm

Premises used: Homeomorph.image_closure, Homeomorph.smul, Eq.symm
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
c : G
s : Set α
hs : Dense s
rw : ∀ (hs : closure[inst] s = univ), closure[inst] (c • s) = univ
⊢ Dense (c • s)

Tactic:
rw [dense_iff_closure_eq] at hs ⊢

Premises used: dense_iff_closure_eq
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
c : G
s : Set α
hs : closure[inst] s = univ
rw : c • closure[inst] s = univ
rw₁ : HSMul.hSMul (β := Set α) c univ = univ
rw₂ rw₃ : Eq.{u_2 + 1} (α := Set α) univ univ
⊢ closure[inst] (c • s) = univ

Tactic:
rw [closure_smul, hs, smul_set_univ]

Premises used: Set.smul_set_univ, closure_smul
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
c : G
s : Set α
⊢ interior (c • s) = c • interior s

Tactic:
((Homeomorph.smul c).image_interior s).symm

Premises used: Homeomorph.image_interior, Homeomorph.smul, Eq.symm
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
c : G
x : α
⊢ 𝓝 (c • x) = c • 𝓝 x

Tactic:
(Homeomorph.smul c).map_nhds_eq x |>.symm

Premises used: Homeomorph.map_nhds_eq, Homeomorph.smul, Eq.symm
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
c : G
x : α
⊢ 𝓝[≠] (c • x) = c • 𝓝[≠] x

Tactic:
(Homeomorph.smul c).map_punctured_nhds_eq x |>.symm

Premises used: Set.Mem, Homeomorph.map_punctured_nhds_eq, setOf, Homeomorph.smul, Eq.symm
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
s : Set G
t : Set α
ht : IsOpen[inst] t
rw : IsOpen[inst] (⋃ a ∈ s, a • t)
⊢ IsOpen[inst] (s • t)

Tactic:
rw [← iUnion_smul_set]

Premises used: Set.iUnion_smul_set
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
s : Set G
t : Set α
ht : IsOpen[inst] t
⊢ IsOpen[inst] (⋃ a ∈ s, a • t)

Tactic:
isOpen_biUnion fun a _ => ht.smul _

Premises used: IsOpen.smul, isOpen_biUnion
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
s : Set G
t : Set α
ht : IsOpen[inst] t
⊢ IsOpen[inst] (⋃ a ∈ s, a • t)

Tactic:
exact isOpen_biUnion fun a _ => ht.smul _

Premises used: IsOpen.smul, isOpen_biUnion
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
s : Set G
t : Set α
⊢ s • interior t ⊆ interior (s • t)

Tactic:
interior_maximal (Set.smul_subset_smul_left interior_subset) isOpen_interior.smul_left

Premises used: interior_subset, isOpen_interior, interior_maximal, Set.smul_subset_smul_left, IsOpen.smul_left
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
t : Set α
g : G
a : α
⊢ g • t ∈ 𝓝 (g • a) ↔ t ∈ 𝓝 a

Tactic:
(Homeomorph.smul g).isOpenEmbedding.image_mem_nhds

Premises used: Set.Mem, Topology.IsOpenEmbedding.image_mem_nhds, Homeomorph.smul, Homeomorph.isOpenEmbedding
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
G : Type u_4
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : ContinuousConstSMul G G
g : G
s : Set G
rw : g⁻¹ • g • s ∈ 𝓝 (g⁻¹ • g) ↔ Membership.mem (γ := Filter G) (𝓝 1) s
⊢ g • s ∈ 𝓝 g ↔ Membership.mem (γ := Filter G) (𝓝 1) s

Tactic:
rw [← smul_mem_nhds_smul_iff g⁻¹]

Premises used: smul_mem_nhds_smul_iff, Inv.inv
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
G : Type u_4
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : ContinuousConstSMul G G
g : G
s : Set G
⊢ g⁻¹ • g • s ∈ 𝓝 (g⁻¹ • g) ↔ Membership.mem (γ := Filter G) (𝓝 1) s

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
x : α
inst_4 : IsPretransitive G α
⊢ T1Space α ↔ IsClosed[inst] {x}

Tactic:
⟨fun H ↦ isClosed_singleton, fun hx ↦ ⟨fun y ↦ ?_⟩⟩

Premises used: T1Space.mk, Iff.intro, isClosed_singleton
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
x : α
inst_4 : IsPretransitive G α
refine : ∀ (hx : IsClosed[inst] {x}) (y : α), IsClosed[inst] {y}
⊢ T1Space α ↔ IsClosed[inst] {x}

Tactic:
refine ⟨fun H ↦ isClosed_singleton, fun hx ↦ ⟨fun y ↦ ?_⟩⟩
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
x : α
inst_4 : IsPretransitive G α
hx : IsClosed[inst] {x}
y : α
rcases : ∀ (g : G), IsClosed[inst] {g • x}
⊢ IsClosed[inst] {y}

Tactic:
rcases MulAction.exists_smul_eq G x y with ⟨g, rfl⟩

Premises used: MulAction.exists_smul_eq, rfl
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
x : α
inst_4 : IsPretransitive G α
hx : IsClosed[inst] {x}
g : G
rw : IsClosed[inst] (HSMul.hSMul (β := Set α) g {x})
⊢ IsClosed[inst] {g • x}

Tactic:
rw [← image_singleton, image_smul]

Premises used: Set.image_smul, Set.image_singleton
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
x : α
inst_4 : IsPretransitive G α
hx : IsClosed[inst] {x}
g : G
⊢ IsClosed[inst] (HSMul.hSMul (β := Set α) g {x})

Tactic:
hx.smul _

Premises used: IsClosed.smul
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
x : α
inst_4 : IsPretransitive G α
hx : IsClosed[inst] {x}
g : G
⊢ IsClosed[inst] (HSMul.hSMul (β := Set α) g {x})

Tactic:
exact hx.smul _

Premises used: IsClosed.smul
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
x : α
inst_4 : IsPretransitive G α
rw : (∀ (a : α), IsOpen[inst] {a}) ↔ IsOpen[inst] {x}
⊢ DiscreteTopology α ↔ IsOpen[inst] {x}

Tactic:
rw [discreteTopology_iff_isOpen_singleton]

Premises used: discreteTopology_iff_isOpen_singleton
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
x : α
inst_4 : IsPretransitive G α
⊢ (∀ (a : α), IsOpen[inst] {a}) ↔ IsOpen[inst] {x}

Tactic:
⟨fun H ↦ H _, fun hx y ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
x : α
inst_4 : IsPretransitive G α
refine : ∀ (hx : IsOpen[inst] {x}) (y : α), IsOpen[inst] {y}
⊢ (∀ (a : α), IsOpen[inst] {a}) ↔ IsOpen[inst] {x}

Tactic:
refine ⟨fun H ↦ H _, fun hx y ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
x : α
inst_4 : IsPretransitive G α
hx : IsOpen[inst] {x}
y : α
rcases : ∀ (g : G), IsOpen[inst] {g • x}
⊢ IsOpen[inst] {y}

Tactic:
rcases MulAction.exists_smul_eq G x y with ⟨g, rfl⟩

Premises used: MulAction.exists_smul_eq, rfl
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
x : α
inst_4 : IsPretransitive G α
hx : IsOpen[inst] {x}
g : G
rw : IsOpen[inst] (HSMul.hSMul (β := Set α) g {x})
⊢ IsOpen[inst] {g • x}

Tactic:
rw [← image_singleton, image_smul]

Premises used: Set.image_smul, Set.image_singleton
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
x : α
inst_4 : IsPretransitive G α
hx : IsOpen[inst] {x}
g : G
⊢ IsOpen[inst] (HSMul.hSMul (β := Set α) g {x})

Tactic:
hx.smul _

Premises used: IsOpen.smul
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
G : Type u_4
inst : TopologicalSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : ContinuousConstSMul G α
x : α
inst_4 : IsPretransitive G α
hx : IsOpen[inst] {x}
g : G
⊢ IsOpen[inst] (HSMul.hSMul (β := Set α) g {x})

Tactic:
exact hx.smul _

Premises used: IsOpen.smul
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
β : Type u_3
G₀ : Type u_4
inst : TopologicalSpace α
inst_1 : GroupWithZero G₀
inst_2 : MulAction G₀ α
inst_3 : ContinuousConstSMul G₀ α
f : β → α
l : Filter β
a : α
c : G₀
hc : c ≠ 0
⊢ Tendsto (fun (x : β) ↦ c • f x) l (𝓝 (c • a)) ↔ Tendsto f l (𝓝 a)

Tactic:
tendsto_const_smul_iff (Units.mk0 c hc)

Premises used: Units.mk0, tendsto_const_smul_iff
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
β : Type u_3
G₀ : Type u_4
inst : TopologicalSpace α
inst_1 : GroupWithZero G₀
inst_2 : MulAction G₀ α
inst_3 : ContinuousConstSMul G₀ α
inst_4 : TopologicalSpace β
f : β → α
b : β
c : G₀
s : Set β
hc : c ≠ 0
⊢ ContinuousWithinAt.{u_3, u_2} (Y := α) (fun (x : β) ↦ c • f x) s b ↔ ContinuousWithinAt f s b

Tactic:
tendsto_const_smul_iff (Units.mk0 c hc)

Premises used: ContinuousWithinAt, Units.mk0, tendsto_const_smul_iff
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
β : Type u_3
G₀ : Type u_4
inst : TopologicalSpace α
inst_1 : GroupWithZero G₀
inst_2 : MulAction G₀ α
inst_3 : ContinuousConstSMul G₀ α
inst_4 : TopologicalSpace β
f : β → α
c : G₀
s : Set β
hc : c ≠ 0
⊢ ContinuousOn.{u_3, u_2} (Y := α) (fun (x : β) ↦ c • f x) s ↔ ContinuousOn f s

Tactic:
continuousOn_const_smul_iff (Units.mk0 c hc)

Premises used: Units.mk0, continuousOn_const_smul_iff
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
β : Type u_3
G₀ : Type u_4
inst : TopologicalSpace α
inst_1 : GroupWithZero G₀
inst_2 : MulAction G₀ α
inst_3 : ContinuousConstSMul G₀ α
inst_4 : TopologicalSpace β
f : β → α
b : β
c : G₀
hc : c ≠ 0
⊢ ContinuousAt.{u_3, u_2} (Y := α) (fun (x : β) ↦ c • f x) b ↔ ContinuousAt f b

Tactic:
continuousAt_const_smul_iff (Units.mk0 c hc)

Premises used: Units.mk0, continuousAt_const_smul_iff
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
α : Type u_2
β : Type u_3
G₀ : Type u_4
inst : TopologicalSpace α
inst_1 : GroupWithZero G₀
inst_2 : MulAction G₀ α
inst_3 : ContinuousConstSMul G₀ α
inst_4 : TopologicalSpace β
f : β → α
c : G₀
hc : c ≠ 0
⊢ (Continuous[inst_4, inst] fun (x : β) ↦ c • f x) ↔ Continuous[inst_4, inst] f

Tactic:
continuous_const_smul_iff (Units.mk0 c hc)

Premises used: Units.mk0, continuous_const_smul_iff