awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
Y : Type u_3
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : SMul M X
inst_4 : ContinuousSMul M X
g : Y → X
N : Type u_5
inst_5 : SMul N Y
inst_6 : TopologicalSpace N
f : N → M
hg : IsInducing g
hf : Continuous[inst_6, inst] f
hsmul : ∀ {c : N} {x : Y}, g (c • x) = f c • g x
⊢ Continuous[instTopologicalSpaceProd, inst_2] fun (p : N × Y) ↦ p.1 • p.2

Tactic:
simpa only [hg.continuous_iff, Function.comp_def, hsmul]
      using (hf.comp continuous_fst).smul <| hg.continuous.comp continuous_snd

Premises used: Topology.IsInducing.continuous_iff, Continuous.comp, continuous_snd, continuous_fst, Continuous.smul, Function.comp_def, Topology.IsInducing.continuous
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
Y : Type u_3
α : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : SMul M X
inst_4 : ContinuousSMul M X
f : Y → M
g : Y → X
b : Y
s_1 : Set Y
S : Type u_5
inst_5 : SetLike S X
inst_6 : SMulMemClass S M X
s : S
⊢ ContinuousSMul.{u_1, u_2} M ↥s

Tactic:
IsInducing.subtypeVal.continuousSMul continuous_id rfl

Premises used: Topology.IsInducing.continuousSMul, continuous_id, rfl, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
Y : Type u_3
α : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : Monoid M
inst_4 : MulAction M X
inst_5 : ContinuousSMul M X
⊢ ContinuousSMul.{u_1, u_2} Mˣ X

Tactic:
IsInducing.id.continuousSMul Units.continuous_val rfl

Premises used: Topology.IsInducing.id, Topology.IsInducing.continuousSMul, Units.continuous_val, rfl
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Monoid M
inst_3 : MulAction M X
inst_4 : ContinuousSMul M X
N : Type u_5
inst_5 : TopologicalSpace N
inst_6 : Monoid N
f : N →* M
hf : Continuous[inst_5, inst] (⇑f : (a : N) → M)
x : MulAction N X := compHom X f
⊢ ContinuousSMul N X

Tactic:
⟨(hf.comp continuous_fst).smul continuous_snd⟩

Premises used: Continuous.comp, continuous_snd, continuous_fst, Continuous.smul, ContinuousSMul.mk
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Monoid M
inst_3 : MulAction M X
inst_4 : ContinuousSMul M X
N : Type u_5
inst_5 : TopologicalSpace N
inst_6 : Monoid N
f : N →* M
hf : Continuous[inst_5, inst] (⇑f : (a : N) → M)
x : MulAction N X := compHom X f
⊢ ContinuousSMul N X

Tactic:
exact ⟨(hf.comp continuous_fst).smul continuous_snd⟩
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
Y : Type u_3
α : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : Monoid M
inst_4 : MulAction M X
inst_5 : ContinuousSMul M X
S : Submonoid M
⊢ ContinuousSMul.{u_1, u_2} (↥S) X

Tactic:
IsInducing.id.continuousSMul continuous_subtype_val rfl

Premises used: Topology.IsInducing.id, continuous_subtype_val, Topology.IsInducing.continuousSMul, rfl
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
Y : Type u_3
α : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : Group M
inst_4 : MulAction M X
inst_5 : ContinuousSMul M X
S : Subgroup M
⊢ ContinuousSMul.{u_1, u_2} (↥S) X

Tactic:
S.toSubmonoid.continuousSMul

Premises used: Set.Mem, Submonoid.continuousSMul
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Group M
inst_3 : MulAction M X
inst_4 : ContinuousSMul M X
inst_5 : DiscreteTopology X
x : X
⊢ Continuous[inst, inst_1] fun (g : M) ↦ g • x

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Group M
inst_3 : IsTopologicalGroup M
inst_4 : MulAction M X
inst_5 : DiscreteTopology X
⊢ ContinuousSMul M X ↔ ∀ (x : X), IsOpen[inst] (↑(MulAction.stabilizer M x) : Set M)

Tactic:
⟨fun _ _ ↦ stabilizer_isOpen .., fun h ↦ ⟨?_⟩⟩

Premises used: Iff.intro, ContinuousSMul.mk, stabilizer_isOpen
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Group M
inst_3 : IsTopologicalGroup M
inst_4 : MulAction M X
inst_5 : DiscreteTopology X
refine :
  ∀ (h : ∀ (x : X), IsOpen[inst] (↑(MulAction.stabilizer M x) : Set M)),
    Continuous[instTopologicalSpaceProd, inst_1] fun (p : M × X) ↦ p.1 • p.2
⊢ ContinuousSMul M X ↔ ∀ (x : X), IsOpen[inst] (↑(MulAction.stabilizer M x) : Set M)

Tactic:
refine ⟨fun _ _ ↦ stabilizer_isOpen .., fun h ↦ ⟨?_⟩⟩
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Group M
inst_3 : IsTopologicalGroup M
inst_4 : MulAction M X
inst_5 : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst] (↑(MulAction.stabilizer M x) : Set M)
rw : ∀ (b : X), Continuous[inst, inst_1] fun (x : M) ↦ (x, b).1 • (x, b).2
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (p : M × X) ↦ p.1 • p.2

Tactic:
rw [continuous_prod_of_discrete_right]

Premises used: continuous_prod_of_discrete_right
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Group M
inst_3 : IsTopologicalGroup M
inst_4 : MulAction M X
inst_5 : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst] (↑(MulAction.stabilizer M x) : Set M)
y : X
rw : ∀ (b : X), IsOpen[inst] (Set.preimage (β := X) (fun (x : M) ↦ (x, y).1 • (x, y).2) {b})
⊢ Continuous[inst, inst_1] fun (x : M) ↦ (x, y).1 • (x, y).2

Tactic:
rw [continuous_discrete_rng]

Premises used: continuous_discrete_rng
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Group M
inst_3 : IsTopologicalGroup M
inst_4 : MulAction M X
inst_5 : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst] (↑(MulAction.stabilizer M x) : Set M)
y x : X
U : Set M := {m' : M | m' • y = x}
pos : ∀ (hU' : U ≠ ∅), IsOpen[inst] U
neg : ∀ (hU' : ¬U ≠ ∅), IsOpen[inst] U
⊢ IsOpen[inst] U

Tactic:
by_cases hU' : U ≠ ∅
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Group M
inst_3 : IsTopologicalGroup M
inst_4 : MulAction M X
inst_5 : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst] (↑(MulAction.stabilizer M x) : Set M)
y x : X
U : Set M := {m' : M | m' • y = x}
hU' : U ≠ ∅
pos : ∀ (m : M) (hm : m • y = x), IsOpen[inst] U
⊢ IsOpen[inst] U

Tactic:
obtain ⟨m, (hm : m • y = x)⟩ := Set.nonempty_iff_empty_ne.mpr hU'.symm

Premises used: Iff.mpr, Ne.symm, Set.nonempty_iff_empty_ne
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Group M
inst_3 : IsTopologicalGroup M
inst_4 : MulAction M X
inst_5 : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst] (↑(MulAction.stabilizer M x) : Set M)
y x : X
U : Set M := {m' : M | m' • y = x}
hU' : U ≠ ∅
m : M
hm : m • y = x
⊢ Continuous[inst, inst] fun (m' : M) ↦ m' * m⁻¹

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Group M
inst_3 : IsTopologicalGroup M
inst_4 : MulAction M X
inst_5 : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst] (↑(MulAction.stabilizer M x) : Set M)
y x : X
U : Set M := {m' : M | m' • y = x}
hU' : U ≠ ∅
m : M
hm : m • y = x
h₁ : U = (fun (m' : M) ↦ m' * m⁻¹) ⁻¹' (↑(MulAction.stabilizer M x) : Set M)
⊢ IsOpen[inst] U

Tactic:
convert! (h x).preimage (by fun_prop : Continuous fun m' : M ↦ m' * m⁻¹)

Premises used: IsOpen.preimage
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Group M
inst_3 : IsTopologicalGroup M
inst_4 : MulAction M X
inst_5 : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst] (↑(MulAction.stabilizer M x) : Set M)
y x : X
U : Set M := {m' : M | m' • y = x}
hU' : U ≠ ∅
m : M
hm : m • y = x
h₁ :
  ∀ (x_1 : M),
    x_1 ∈ U ↔ Membership.mem (γ := Set M) ((fun (m' : M) ↦ m' * m⁻¹) ⁻¹' (↑(MulAction.stabilizer M x) : Set M)) x_1
⊢ U = (fun (m' : M) ↦ m' * m⁻¹) ⁻¹' (↑(MulAction.stabilizer M x) : Set M)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Group M
inst_3 : IsTopologicalGroup M
inst_4 : MulAction M X
inst_5 : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst] (↑(MulAction.stabilizer M x) : Set M)
y x : X
U : Set M := {m' : M | m' • y = x}
hU' : U ≠ ∅
m : M
hm : m • y = x
x_1 : M
⊢ x_1 ∈ U ↔ Membership.mem (γ := Set M) ((fun (m' : M) ↦ m' * m⁻¹) ⁻¹' (↑(MulAction.stabilizer M x) : Set M)) x_1

Tactic:
simp [← smul_smul, U, eq_inv_smul_iff.mpr hm]

Premises used: Iff.mpr, smul_smul, eq_inv_smul_iff
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Group M
inst_3 : IsTopologicalGroup M
inst_4 : MulAction M X
inst_5 : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst] (↑(MulAction.stabilizer M x) : Set M)
y x : X
U : Set M := {m' : M | m' • y = x}
hU' : ¬U ≠ ∅
⊢ IsOpen[inst] U

Tactic:
simp_all
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Group M
inst_3 : IsTopologicalGroup M
inst_4 : MulAction M X
inst_5 : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst] (↑(MulAction.stabilizer M x) : Set M)
y x : X
U : Set M := {m' : M | m' • y = x}
⊢ IsOpen[inst] U

Tactic:
have hU : IsOpen U := by
    by_cases hU' : U ≠ ∅
    · obtain ⟨m, (hm : m • y = x)⟩ := Set.nonempty_iff_empty_ne.mpr hU'.symm
      convert! (h x).preimage (by fun_prop : Continuous fun m' : M ↦ m' * m⁻¹)
      ext; simp [← smul_smul, U, eq_inv_smul_iff.mpr hm]
    simp_all
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Group M
inst_3 : IsTopologicalGroup M
inst_4 : MulAction M X
inst_5 : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst] (↑(MulAction.stabilizer M x) : Set M)
y x : X
U : Set M := {m' : M | m' • y = x}
hU : IsOpen[inst] U
⊢ IsOpen[inst] (Set.preimage (β := X) (fun (x : M) ↦ (x, y).1 • (x, y).2) {x})

Tactic:
simpa using hU
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
G₀ : Type u_5
X : Type u_6
inst : GroupWithZero G₀
inst_1 : Zero X
inst_2 : MulActionWithZero G₀ X
inst_3 : TopologicalSpace G₀
inst_4 : NeBot (α := G₀) (𝓝[≠] 0)
inst_5 : TopologicalSpace X
inst_6 : ContinuousSMul G₀ X
s : Set X
hs : Membership.mem (γ := Filter X) (𝓝 0) s
⊢ HSMul.hSMul.{u_5, u_6, u_6} (α := Set G₀) univ s = univ

Tactic:
Set.eq_univ_of_forall fun x ↦ ?_

Premises used: Set.eq_univ_of_forall
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
G₀ : Type u_5
X : Type u_6
inst : GroupWithZero G₀
inst_1 : Zero X
inst_2 : MulActionWithZero G₀ X
inst_3 : TopologicalSpace G₀
inst_4 : NeBot (α := G₀) (𝓝[≠] 0)
inst_5 : TopologicalSpace X
inst_6 : ContinuousSMul G₀ X
s : Set X
hs : Membership.mem (γ := Filter X) (𝓝 0) s
refine : ∀ (x : X), x ∈ HSMul.hSMul.{u_5, u_6, u_6} (α := Set G₀) univ s
⊢ HSMul.hSMul.{u_5, u_6, u_6} (α := Set G₀) univ s = univ

Tactic:
refine Set.eq_univ_of_forall fun x ↦ ?_

Premises used: Set.eq_univ_of_forall
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
G₀ : Type u_5
X : Type u_6
inst : GroupWithZero G₀
inst_1 : Zero X
inst_2 : MulActionWithZero G₀ X
inst_3 : TopologicalSpace G₀
inst_4 : NeBot (α := G₀) (𝓝[≠] 0)
inst_5 : TopologicalSpace X
inst_6 : ContinuousSMul G₀ X
s : Set X
hs : Membership.mem (γ := Filter X) (𝓝 0) s
x : X
⊢ Tendsto.{u_5, u_6} (β := X) (fun (x_1 : G₀) ↦ x_1 • x) (𝓝 0) (𝓝 0)

Tactic:
have : Tendsto (· • x) (𝓝 (0 : G₀)) (𝓝 0) :=
    zero_smul G₀ x ▸ tendsto_id.smul tendsto_const_nhds
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
G₀ : Type u_5
X : Type u_6
inst : GroupWithZero G₀
inst_1 : Zero X
inst_2 : MulActionWithZero G₀ X
inst_3 : TopologicalSpace G₀
inst_4 : NeBot (α := G₀) (𝓝[≠] 0)
inst_5 : TopologicalSpace X
inst_6 : ContinuousSMul G₀ X
s : Set X
hs : Membership.mem (γ := Filter X) (𝓝 0) s
x : X
this : Tendsto.{u_5, u_6} (β := X) (fun (x_1 : G₀) ↦ x_1 • x) (𝓝 0) (𝓝 0)
rcases :
  ∀ (c : G₀) (hc₀ : Membership.mem (γ := Set G₀) {0}ᶜ c)
    (hc : Membership.mem (γ := Set G₀) ((fun (x_1 : G₀) ↦ x_1 • x) ⁻¹' s) c),
    x ∈ HSMul.hSMul.{u_5, u_6, u_6} (α := Set G₀) univ s
⊢ x ∈ HSMul.hSMul.{u_5, u_6, u_6} (α := Set G₀) univ s

Tactic:
rcases Filter.nonempty_of_mem (inter_mem_nhdsWithin {0}ᶜ <| mem_map.1 <| this hs)
    with ⟨c, hc₀, hc⟩

Premises used: inter_mem_nhdsWithin, Compl.compl, Filter.nonempty_of_mem, Iff.mp, Singleton.singleton, OfNat.ofNat, Filter.mem_map
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
G₀ : Type u_5
X : Type u_6
inst : GroupWithZero G₀
inst_1 : Zero X
inst_2 : MulActionWithZero G₀ X
inst_3 : TopologicalSpace G₀
inst_4 : NeBot (α := G₀) (𝓝[≠] 0)
inst_5 : TopologicalSpace X
inst_6 : ContinuousSMul G₀ X
s : Set X
hs : Membership.mem (γ := Filter X) (𝓝 0) s
x : X
this : Tendsto.{u_5, u_6} (β := X) (fun (x_1 : G₀) ↦ x_1 • x) (𝓝 0) (𝓝 0)
c : G₀
hc₀ : Membership.mem (γ := Set G₀) {0}ᶜ c
hc : Membership.mem (γ := Set G₀) ((fun (x_1 : G₀) ↦ x_1 • x) ⁻¹' s) c
⊢ ¬c = 0

Tactic:
simp only [mem_compl_iff, mem_singleton_iff] at hc₀

Premises used: Set.mem_singleton_iff, Set.mem_compl_iff
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
G₀ : Type u_5
X : Type u_6
inst : GroupWithZero G₀
inst_1 : Zero X
inst_2 : MulActionWithZero G₀ X
inst_3 : TopologicalSpace G₀
inst_4 : NeBot (α := G₀) (𝓝[≠] 0)
inst_5 : TopologicalSpace X
inst_6 : ContinuousSMul G₀ X
s : Set X
hs : Membership.mem (γ := Filter X) (𝓝 0) s
x : X
this : Tendsto.{u_5, u_6} (β := X) (fun (x_1 : G₀) ↦ x_1 • x) (𝓝 0) (𝓝 0)
c : G₀
hc : Membership.mem (γ := Set G₀) ((fun (x_1 : G₀) ↦ x_1 • x) ⁻¹' s) c
hc₀ : ¬c = 0
simp : ∃ (x_1 : G₀), ∃ y ∈ s, x_1 • y = x
⊢ x ∈ HSMul.hSMul.{u_5, u_6, u_6} (α := Set G₀) univ s

Tactic:
simp only [mem_smul, mem_univ, true_and]

Premises used: Set.mem_smul, Set.mem_univ, true_and
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
G₀ : Type u_5
X : Type u_6
inst : GroupWithZero G₀
inst_1 : Zero X
inst_2 : MulActionWithZero G₀ X
inst_3 : TopologicalSpace G₀
inst_4 : NeBot (α := G₀) (𝓝[≠] 0)
inst_5 : TopologicalSpace X
inst_6 : ContinuousSMul G₀ X
s : Set X
hs : Membership.mem (γ := Filter X) (𝓝 0) s
x : X
this : Tendsto.{u_5, u_6} (β := X) (fun (x_1 : G₀) ↦ x_1 • x) (𝓝 0) (𝓝 0)
c : G₀
hc : Membership.mem (γ := Set G₀) ((fun (x_1 : G₀) ↦ x_1 • x) ⁻¹' s) c
hc₀ : ¬c = 0
⊢ ∃ (x_1 : G₀), ∃ y ∈ s, x_1 • y = x

Tactic:
⟨c⁻¹, c • x, hc, inv_smul_smul₀ hc₀ _⟩

Premises used: inv_smul_smul₀, Inv.inv, And.intro, Exists.intro, HSMul.hSMul
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
G₀ : Type u_5
X : Type u_6
inst : GroupWithZero G₀
inst_1 : Zero X
inst_2 : MulActionWithZero G₀ X
inst_3 : TopologicalSpace G₀
inst_4 : NeBot (α := G₀) (𝓝[≠] 0)
inst_5 : TopologicalSpace X
inst_6 : ContinuousSMul G₀ X
s : Set X
hs : Membership.mem (γ := Filter X) (𝓝 0) s
x : X
this : Tendsto.{u_5, u_6} (β := X) (fun (x_1 : G₀) ↦ x_1 • x) (𝓝 0) (𝓝 0)
c : G₀
hc : Membership.mem (γ := Set G₀) ((fun (x_1 : G₀) ↦ x_1 • x) ⁻¹' s) c
hc₀ : ¬c = 0
⊢ ∃ (x_1 : G₀), ∃ y ∈ s, x_1 • y = x

Tactic:
exact ⟨c⁻¹, c • x, hc, inv_smul_smul₀ hc₀ _⟩
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
G₀ : Type u_5
X : Type u_6
inst : GroupWithZero G₀
inst_1 : Zero X
inst_2 : MulActionWithZero G₀ X
inst_3 : TopologicalSpace G₀
inst_4 : NeBot (α := G₀) (𝓝[≠] 0)
inst_5 : TopologicalSpace X
inst_6 : ContinuousSMul G₀ X
rw :
  ∀ (i : Unit × Set X),
    True ∧ Membership.mem (γ := Filter X) (𝓝 0) i.2 →
      HSMul.hSMul.{u_5, u_6, u_6} (α := Set G₀) Set.univ (id i.2) = Set.univ
⊢ HSMul.hSMul.{u_5, u_6, u_6} (α := Filter G₀) (β := Filter X) ⊤ (𝓝 0) = ⊤

Tactic:
rw [(hasBasis_top.smul (basis_sets _)).eq_top_iff]

Premises used: Filter.HasBasis.eq_top_iff, Filter.basis_sets, Filter.HasBasis.smul, Filter.hasBasis_top
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
G₀ : Type u_5
X : Type u_6
inst : GroupWithZero G₀
inst_1 : Zero X
inst_2 : MulActionWithZero G₀ X
inst_3 : TopologicalSpace G₀
inst_4 : NeBot (α := G₀) (𝓝[≠] 0)
inst_5 : TopologicalSpace X
inst_6 : ContinuousSMul G₀ X
fst : Unit
s : Set X
hs : Membership.mem (γ := Filter X) (𝓝 0) (fst, s).2
⊢ HSMul.hSMul.{u_5, u_6, u_6} (α := Set G₀) Set.univ (id (fst, s).2) = Set.univ

Tactic:
Set.univ_smul_nhds_zero hs

Premises used: Set.univ_smul_nhds_zero
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
G₀ : Type u_5
X : Type u_6
inst : GroupWithZero G₀
inst_1 : Zero X
inst_2 : MulActionWithZero G₀ X
inst_3 : TopologicalSpace G₀
inst_4 : NeBot (α := G₀) (𝓝[≠] 0)
inst_5 : TopologicalSpace X
inst_6 : ContinuousSMul G₀ X
fst : Unit
s : Set X
hs : Membership.mem (γ := Filter X) (𝓝 0) (fst, s).2
⊢ HSMul.hSMul.{u_5, u_6, u_6} (α := Set G₀) Set.univ (id (fst, s).2) = Set.univ

Tactic:
exact Set.univ_smul_nhds_zero hs

Premises used: Set.univ_smul_nhds_zero
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
Y : Type u_3
α : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : SMul M X
inst_4 : SMul M Y
inst_5 : ContinuousSMul M X
inst_6 : ContinuousSMul M Y
⊢ ContinuousSMul M (X × Y)

Tactic:
⟨(continuous_fst.smul (continuous_fst.comp continuous_snd)).prodMk
      (continuous_fst.smul (continuous_snd.comp continuous_snd))⟩

Premises used: Continuous.comp, continuous_snd, continuous_fst, Continuous.smul, ContinuousSMul.mk, Continuous.prodMk
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
Y : Type u_3
α : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
ι : Type u_5
γ : ι → Type u_6
inst_3 : (i : ι) → TopologicalSpace (γ i)
inst_4 : (i : ι) → SMul.{u_1, u_6} M (γ i)
inst_5 : ∀ (i : ι), ContinuousSMul.{u_1, u_6} M (γ i)
⊢ ContinuousSMul M ((i : ι) → γ i)

Tactic:
⟨continuous_pi fun i =>
      (continuous_fst.smul continuous_snd).comp <|
        continuous_fst.prodMk ((continuous_apply i).comp continuous_snd)⟩

Premises used: Continuous.comp, continuous_snd, continuous_fst, continuous_pi, Continuous.smul, ContinuousSMul.mk, continuous_apply, Continuous.prodMk
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
Y : Type u_3
α : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
ι : Type u_5
γ : ι → Type u_6
inst_3 : (i : ι) → TopologicalSpace (γ i)
N : ι → Type u_7
inst_4 : (i : ι) → TopologicalSpace (N i)
inst_5 : (i : ι) → SMul.{u_7, u_6} (N i) (γ i)
inst_6 : ∀ (i : ι), ContinuousSMul.{u_7, u_6} (N i) (γ i)
⊢ ContinuousSMul ((i : ι) → N i) ((i : ι) → γ i)

Tactic:
⟨continuous_pi fun i ↦ ((continuous_apply i).comp continuous_id'.fst).smul
    ((continuous_apply i).comp continuous_id'.snd)⟩

Premises used: Continuous.snd, Continuous.comp, continuous_id', continuous_pi, Continuous.smul, ContinuousSMul.mk, continuous_apply, Continuous.fst
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_2
X : Type u_3
inst : TopologicalSpace M
inst_1 : SMul M X
ts : Set (TopologicalSpace X)
h : ∀ t ∈ ts, ContinuousSMul M X
x : TopologicalSpace X := sInf ts
rw : Continuous[instTopologicalSpaceProd, sInf ts] fun (p : M × X) ↦ p.1 • p.2
⊢ Continuous[instTopologicalSpaceProd, sInf ts] fun (p : M × X) ↦ p.1 • p.2

Tactic:
rw [← (sInf_singleton (a := ‹TopologicalSpace M›) :)]

Premises used: sInf_singleton
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_2
X : Type u_3
inst : TopologicalSpace M
inst_1 : SMul M X
ts : Set (TopologicalSpace X)
h : ∀ t ∈ ts, ContinuousSMul M X
x : TopologicalSpace X := sInf ts
⊢ Continuous[instTopologicalSpaceProd, sInf ts] fun (p : M × X) ↦ p.1 • p.2

Tactic:
continuous_sInf_rng.2 fun t ht =>
          continuous_sInf_dom₂ (Eq.refl _) ht
            (@ContinuousSMul.continuous_smul _ _ _ _ t (h t ht))

Premises used: continuous_sInf_dom₂, Iff.mpr, Eq.refl, ContinuousSMul.continuous_smul, continuous_sInf_rng
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_2
X : Type u_3
inst : TopologicalSpace M
inst_1 : SMul M X
ts : Set (TopologicalSpace X)
h : ∀ t ∈ ts, ContinuousSMul M X
x : TopologicalSpace X := sInf ts
⊢ Continuous[instTopologicalSpaceProd, sInf ts] fun (p : M × X) ↦ p.1 • p.2

Tactic:
exact
        continuous_sInf_rng.2 fun t ht =>
          continuous_sInf_dom₂ (Eq.refl _) ht
            (@ContinuousSMul.continuous_smul _ _ _ _ t (h t ht))

Premises used: continuous_sInf_dom₂, Iff.mpr, Eq.refl, ContinuousSMul.continuous_smul, continuous_sInf_rng
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
ι : Sort u_1
M : Type u_2
X : Type u_3
inst : TopologicalSpace M
inst_1 : SMul M X
ts' : ι → TopologicalSpace X
h : ∀ (i : ι), ContinuousSMul M X
⊢ ContinuousSMul M X

Tactic:
continuousSMul_sInf <| Set.forall_mem_range.mpr h

Premises used: Iff.mpr, iInf, Set.forall_mem_range, continuousSMul_sInf
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_2
X : Type u_3
inst : TopologicalSpace M
inst_1 : SMul M X
t₁ t₂ : TopologicalSpace X
inst_2 : ContinuousSMul M X
inst_3 : ContinuousSMul M X
rw : ContinuousSMul M X
⊢ ContinuousSMul M X

Tactic:
rw [inf_eq_iInf]

Premises used: inf_eq_iInf
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_2
X : Type u_3
inst : TopologicalSpace M
inst_1 : SMul M X
t₁ t₂ : TopologicalSpace X
inst_2 : ContinuousSMul M X
inst_3 : ContinuousSMul M X
⊢ ContinuousSMul M X

Tactic:
continuousSMul_iInf fun b => ?_

Premises used: continuousSMul_iInf
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_2
X : Type u_3
inst : TopologicalSpace M
inst_1 : SMul M X
t₁ t₂ : TopologicalSpace X
inst_2 : ContinuousSMul M X
inst_3 : ContinuousSMul M X
refine : ∀ (b : Bool), ContinuousSMul M X
⊢ ContinuousSMul M X

Tactic:
refine continuousSMul_iInf fun b => ?_

Premises used: continuousSMul_iInf
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_2
X : Type u_3
inst : TopologicalSpace M
inst_1 : SMul M X
t₁ t₂ : TopologicalSpace X
inst_2 : ContinuousSMul M X
inst_3 : ContinuousSMul M X
b : Bool
false : ContinuousSMul M X
true : ContinuousSMul M X
⊢ ContinuousSMul M X

Tactic:
cases b
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_2
X : Type u_3
inst : TopologicalSpace M
inst_1 : SMul M X
t₁ t₂ : TopologicalSpace X
inst_2 : ContinuousSMul M X
inst_3 : ContinuousSMul M X
⊢ ContinuousSMul M X

Tactic:
assumption
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
inst_2 : TopologicalSpace G
inst_3 : PreconnectedSpace G
inst_4 : TopologicalSpace P
inst_5 : ContinuousVAdd G P
⊢ IsPreconnected.{u_2} (α := P)
    (Set.image.{u_1, u_2} (α := G) (⇑(Equiv.vaddConst (Classical.arbitrary P)) : (a : G) → P) Set.univ)

Tactic:
isPreconnected_univ.image (Equiv.vaddConst (Classical.arbitrary P) : G → P)
          (continuous_id.vadd continuous_const).continuousOn

Premises used: Continuous.continuousOn, Equiv.vaddConst, continuous_const, IsPreconnected.image, continuous_id, Continuous.vadd, Classical.arbitrary, PreconnectedSpace.isPreconnected_univ, DFunLike.coe
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
inst_2 : TopologicalSpace G
inst_3 : PreconnectedSpace G
inst_4 : TopologicalSpace P
inst_5 : ContinuousVAdd G P
h :
  Eq.{u_2 + 1} (α := Set P) Set.univ
    (Set.image.{u_1, u_2} (α := G) (⇑(Equiv.vaddConst (Classical.arbitrary P)) : (a : G) → P) Set.univ)
⊢ IsPreconnected.{u_2} (α := P) Set.univ

Tactic:
convert!
        isPreconnected_univ.image (Equiv.vaddConst (Classical.arbitrary P) : G → P)
          (continuous_id.vadd continuous_const).continuousOn

Premises used: Continuous.continuousOn, Equiv.vaddConst, continuous_const, IsPreconnected.image, continuous_id, Continuous.vadd, Classical.arbitrary, PreconnectedSpace.isPreconnected_univ, DFunLike.coe