awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
X : Type u_5
inst : TopologicalSpace X
M : Type u_6
inst_1 : One M
f : ι → X → M
hf : LocallyFinite.{u_1, u_5} (X := X) fun (i : ι) ↦ mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : Set.Finite.{u_1} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ U).Nonempty}
y : X
hy : y ∈ U
i : ι
hi : Membership.mem (γ := Set ι) (mulSupport.{u_1, u_6} (M := M) fun (i : ι) ↦ f i y) i
⊢ Membership.mem (γ := Set ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ U).Nonempty} i

Tactic:
⟨y, hi, hy⟩

Premises used: Set.Mem, setOf, Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
X : Type u_5
inst : TopologicalSpace X
M : Type u_6
inst_1 : One M
f : ι → X → M
hf : LocallyFinite.{u_1, u_5} (X := X) fun (i : ι) ↦ mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : Set.Finite.{u_1} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ U).Nonempty}
y : X
hy : y ∈ U
i : ι
hi : Membership.mem (γ := Set ι) (mulSupport.{u_1, u_6} (M := M) fun (i : ι) ↦ f i y) i
⊢ Membership.mem (γ := Set ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ U).Nonempty} i

Tactic:
exact ⟨y, hi, hy⟩
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
X : Type u_5
inst : TopologicalSpace X
M : Type u_6
inst_1 : CommMonoid M
f : ι → X → M
hf : LocallyFinite.{u_1, u_5} (X := X) fun (i : ι) ↦ mulSupport (f i)
x : X
⊢ ∃ (s : Finset ι), ∀ᶠ (y : X) in 𝓝 x, Eq.{u_6 + 1} (α := M) (∏ᶠ (i : ι), f i y) (∏ i ∈ s, f i y)

Tactic:
let ⟨I, hI⟩ := hf.exists_finset_mulSupport x
  ⟨I, hI.mono fun _ hy => finprod_eq_prod_of_mulSupport_subset _ fun _ hi => hy hi⟩

Premises used: Filter.Eventually, Exists, nhds, _private.0.finprod_eventually_eq_prod.match_1, LocallyFinite.exists_finset_mulSupport, Finset.prod, Filter.Eventually.mono, finprod, Exists.intro, Eq, finprod_eq_prod_of_mulSupport_subset
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : CommMonoid M
inst_3 : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous[inst, inst_1] (f i)
hf : LocallyFinite.{u_1, u_5} (X := X) fun (i : ι) ↦ mulSupport (f i)
⊢ Continuous[inst, inst_1] fun (x : X) ↦ ∏ᶠ (i : ι), f i x

Tactic:
continuous_iff_continuousAt.2 fun x => ?_

Premises used: Iff.mpr, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : CommMonoid M
inst_3 : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous[inst, inst_1] (f i)
hf : LocallyFinite.{u_1, u_5} (X := X) fun (i : ι) ↦ mulSupport (f i)
refine : ∀ (x : X), ContinuousAt.{u_5, u_3} (Y := M) (fun (x : X) ↦ ∏ᶠ (i : ι), f i x) x
⊢ Continuous[inst, inst_1] fun (x : X) ↦ ∏ᶠ (i : ι), f i x

Tactic:
refine continuous_iff_continuousAt.2 fun x => ?_

Premises used: Iff.mpr, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : CommMonoid M
inst_3 : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous[inst, inst_1] (f i)
hf : LocallyFinite.{u_1, u_5} (X := X) fun (i : ι) ↦ mulSupport (f i)
x : X
rcases :
  ∀ (s : Finset ι) (hs : ∀ᶠ (y : X) in 𝓝 x, Eq.{u_3 + 1} (α := M) (∏ᶠ (i : ι), f i y) (∏ i ∈ s, f i y)),
    ContinuousAt.{u_5, u_3} (Y := M) (fun (x : X) ↦ ∏ᶠ (i : ι), f i x) x
⊢ ContinuousAt.{u_5, u_3} (Y := M) (fun (x : X) ↦ ∏ᶠ (i : ι), f i x) x

Tactic:
rcases finprod_eventually_eq_prod hf x with ⟨s, hs⟩

Premises used: finprod_eventually_eq_prod
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : CommMonoid M
inst_3 : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous[inst, inst_1] (f i)
hf : LocallyFinite.{u_1, u_5} (X := X) fun (i : ι) ↦ mulSupport (f i)
x : X
s : Finset ι
hs : ∀ᶠ (y : X) in 𝓝 x, Eq.{u_3 + 1} (α := M) (∏ᶠ (i : ι), f i y) (∏ i ∈ s, f i y)
⊢ ContinuousAt.{u_5, u_3} (Y := M) (fun (x : X) ↦ ∏ᶠ (i : ι), f i x) x

Tactic:
ContinuousAt.congr ?_ (EventuallyEq.symm hs)

Premises used: ContinuousAt.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : CommMonoid M
inst_3 : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous[inst, inst_1] (f i)
hf : LocallyFinite.{u_1, u_5} (X := X) fun (i : ι) ↦ mulSupport (f i)
x : X
s : Finset ι
hs : ∀ᶠ (y : X) in 𝓝 x, Eq.{u_3 + 1} (α := M) (∏ᶠ (i : ι), f i y) (∏ i ∈ s, f i y)
refine : ContinuousAt.{u_5, u_3} (Y := M) (fun (x : X) ↦ ∏ i ∈ s, f i x) x
⊢ ContinuousAt.{u_5, u_3} (Y := M) (fun (x : X) ↦ ∏ᶠ (i : ι), f i x) x

Tactic:
refine ContinuousAt.congr ?_ (EventuallyEq.symm hs)

Premises used: ContinuousAt.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : CommMonoid M
inst_3 : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous[inst, inst_1] (f i)
hf : LocallyFinite.{u_1, u_5} (X := X) fun (i : ι) ↦ mulSupport (f i)
x : X
s : Finset ι
hs : ∀ᶠ (y : X) in 𝓝 x, Eq.{u_3 + 1} (α := M) (∏ᶠ (i : ι), f i y) (∏ i ∈ s, f i y)
⊢ ContinuousAt.{u_5, u_3} (Y := M) (fun (x : X) ↦ ∏ i ∈ s, f i x) x

Tactic:
tendsto_finsetProd _ fun i _ => (hc i).continuousAt

Premises used: ContinuousAt, Continuous.continuousAt, tendsto_finsetProd
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : CommMonoid M
inst_3 : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous[inst, inst_1] (f i)
hf : LocallyFinite.{u_1, u_5} (X := X) fun (i : ι) ↦ mulSupport (f i)
x : X
s : Finset ι
hs : ∀ᶠ (y : X) in 𝓝 x, Eq.{u_3 + 1} (α := M) (∏ᶠ (i : ι), f i y) (∏ i ∈ s, f i y)
⊢ ContinuousAt.{u_5, u_3} (Y := M) (fun (x : X) ↦ ∏ i ∈ s, f i x) x

Tactic:
exact tendsto_finsetProd _ fun i _ => (hc i).continuousAt

Premises used: Continuous.continuousAt, tendsto_finsetProd
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : CommMonoid M
inst_3 : ContinuousMul M
f : ι → X → M
p : ι → Prop
hc : ∀ (i : ι), p i → Continuous[inst, inst_1] (f i)
hf : LocallyFinite.{u_1, u_5} (X := X) fun (i : ι) ↦ mulSupport (f i)
simp : Continuous[inst, inst_1] fun (x : X) ↦ ∏ᶠ (j : Subtype p), f (↑j : ι) x
⊢ Continuous[inst, inst_1] fun (x : X) ↦ ∏ᶠ (i : ι) (_ : p i), f i x

Tactic:
simp only [← finprod_subtype_eq_finprod_cond]

Premises used: finprod_subtype_eq_finprod_cond
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : CommMonoid M
inst_3 : ContinuousMul M
f : ι → X → M
p : ι → Prop
hc : ∀ (i : ι), p i → Continuous[inst, inst_1] (f i)
hf : LocallyFinite.{u_1, u_5} (X := X) fun (i : ι) ↦ mulSupport (f i)
⊢ Continuous[inst, inst_1] fun (x : X) ↦ ∏ᶠ (j : Subtype p), f (↑j : ι) x

Tactic:
continuous_finprod (fun i => hc i i.2) (hf.comp_injective Subtype.coe_injective)

Premises used: Subtype.coe_injective, LocallyFinite.comp_injective, Subtype.val, Subtype.property, continuous_finprod
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : CommMonoid M
inst_3 : ContinuousMul M
f : ι → X → M
p : ι → Prop
hc : ∀ (i : ι), p i → Continuous[inst, inst_1] (f i)
hf : LocallyFinite.{u_1, u_5} (X := X) fun (i : ι) ↦ mulSupport (f i)
⊢ Continuous[inst, inst_1] fun (x : X) ↦ ∏ᶠ (j : Subtype p), f (↑j : ι) x

Tactic:
exact continuous_finprod (fun i => hc i i.2) (hf.comp_injective Subtype.coe_injective)
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : Mul M
ts : Set (TopologicalSpace M)
h : ∀ t ∈ ts, ContinuousMul M
⊢ ContinuousMul M

Tactic:
letI := sInf ts
  { continuous_mul :=
      continuous_sInf_rng.2 fun t ht =>
        continuous_sInf_dom₂ ht ht (@ContinuousMul.continuous_mul M t _ (h t ht)) }

Premises used: continuous_sInf_dom₂, Iff.mpr, ContinuousMul.mk, ContinuousMul.continuous_mul, continuous_sInf_rng
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
ι' : Sort u_6
inst : Mul M
ts : ι' → TopologicalSpace M
h' : ∀ (i : ι'), ContinuousMul M
⊢ ContinuousMul M

Tactic:
continuousMul_sInf (Set.forall_mem_range.mpr h')

Premises used: Iff.mpr, continuousMul_sInf, Set.forall_mem_range
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
ι' : Sort u_6
inst : Mul M
ts : ι' → TopologicalSpace M
h' : ∀ (i : ι'), ContinuousMul M
⊢ ContinuousMul M

Tactic:
exact continuousMul_sInf (Set.forall_mem_range.mpr h')

Premises used: Iff.mpr, continuousMul_sInf, Set.forall_mem_range
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
rw : ContinuousMul M
⊢ ContinuousMul M

Tactic:
rw [inf_eq_iInf]

Premises used: inf_eq_iInf
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul M

Tactic:
continuousMul_iInf fun b => ?_

Premises used: continuousMul_iInf
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
refine : ∀ (b : Bool), ContinuousMul M
⊢ ContinuousMul M

Tactic:
refine continuousMul_iInf fun b => ?_

Premises used: continuousMul_iInf
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
b : Bool
false : ContinuousMul M
true : ContinuousMul M
⊢ ContinuousMul M

Tactic:
cases b
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul M

Tactic:
assumption
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
X : Type u_5
inst : TopologicalSpace X
inst_1 : Mul X
inst_2 : SeparatelyContinuousMul X
x : X
⊢ Eq (α := (a : X) → X) (⇑(ContinuousMap.mulRight x) : (a : X) → X) fun (y : X) ↦ y * x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
X : Type u_6
inst : Semigroup X
inst_1 : TopologicalSpace X
inst_2 : SeparatelyContinuousMul X
x y : X
h :
  ∀ (a : X),
    Eq (α := X) ((ContinuousMap.mulRight (x * y) : (a : X) → X) a : X)
      ((comp (ContinuousMap.mulRight y) (ContinuousMap.mulRight x) : (a : X) → X) a : X)
⊢ Eq (α := C(X, X)) (ContinuousMap.mulRight (x * y)) (comp (ContinuousMap.mulRight y) (ContinuousMap.mulRight x))

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
X : Type u_6
inst : Semigroup X
inst_1 : TopologicalSpace X
inst_2 : SeparatelyContinuousMul X
x y a : X
⊢ Eq (α := X) ((ContinuousMap.mulRight (x * y) : (a : X) → X) a : X)
    ((comp (ContinuousMap.mulRight y) (ContinuousMap.mulRight x) : (a : X) → X) a : X)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
X : Type u_5
inst : TopologicalSpace X
inst_1 : Mul X
inst_2 : SeparatelyContinuousMul X
x : X
⊢ Eq (α := (a : X) → X) (⇑(ContinuousMap.mulLeft x) : (a : X) → X) fun (y : X) ↦ x * y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
X : Type u_6
inst : Semigroup X
inst_1 : TopologicalSpace X
inst_2 : SeparatelyContinuousMul X
x y : X
h :
  ∀ (a : X),
    Eq (α := X) ((ContinuousMap.mulLeft (x * y) : (a : X) → X) a : X)
      ((comp (ContinuousMap.mulLeft x) (ContinuousMap.mulLeft y) : (a : X) → X) a : X)
⊢ Eq (α := C(X, X)) (ContinuousMap.mulLeft (x * y)) (comp (ContinuousMap.mulLeft x) (ContinuousMap.mulLeft y))

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
X : Type u_6
inst : Semigroup X
inst_1 : TopologicalSpace X
inst_2 : SeparatelyContinuousMul X
x y a : X
⊢ Eq (α := X) ((ContinuousMap.mulLeft (x * y) : (a : X) → X) a : X)
    ((comp (ContinuousMap.mulLeft x) (ContinuousMap.mulLeft y) : (a : X) → X) a : X)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_5
N : Type u_6
α : Type u_7
inst : Monoid N
inst_1 : SMul M N
inst_2 : MulAction N α
inst_3 : SMul M α
inst_4 : IsScalarTower M N α
inst_5 : TopologicalSpace M
inst_6 : TopologicalSpace N
inst_7 : TopologicalSpace α
inst_8 : ContinuousSMul M N
inst_9 : ContinuousSMul N α
this : Continuous[instTopologicalSpaceProd, inst_7] fun (p : M × α) ↦ HSMul.hSMul (β := N) p.1 1 • p.2
⊢ Continuous[instTopologicalSpaceProd, inst_7] fun (p : M × α) ↦ p.1 • p.2

Tactic:
simpa
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_5
N : Type u_6
α : Type u_7
inst : Monoid N
inst_1 : SMul M N
inst_2 : MulAction N α
inst_3 : SMul M α
inst_4 : IsScalarTower M N α
inst_5 : TopologicalSpace M
inst_6 : TopologicalSpace N
inst_7 : TopologicalSpace α
inst_8 : ContinuousSMul M N
inst_9 : ContinuousSMul N α
suffices : Continuous[instTopologicalSpaceProd, inst_7] fun (p : M × α) ↦ HSMul.hSMul (β := N) p.1 1 • p.2
⊢ Continuous[instTopologicalSpaceProd, inst_7] fun (p : M × α) ↦ p.1 • p.2

Tactic:
suffices Continuous (fun p : M × α ↦ (p.1 • (1 : N)) • p.2) by simpa
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_5
N : Type u_6
α : Type u_7
inst : Monoid N
inst_1 : SMul M N
inst_2 : MulAction N α
inst_3 : SMul M α
inst_4 : IsScalarTower M N α
inst_5 : TopologicalSpace M
inst_6 : TopologicalSpace N
inst_7 : TopologicalSpace α
inst_8 : ContinuousSMul M N
inst_9 : ContinuousSMul N α
⊢ Continuous[instTopologicalSpaceProd, inst_7] fun (p : M × α) ↦ HSMul.hSMul (β := N) p.1 1 • p.2

Tactic:
fun_prop
-- 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
⊢ ContinuousSMul (ULift.{u_5, u_1} M) X

Tactic:
⟨(continuous_smul (M := M)).comp₂ (continuous_uliftDown.comp continuous_fst) continuous_snd⟩

Premises used: Continuous.comp₂, Continuous.comp, continuous_snd, continuous_fst, continuous_uliftDown, ContinuousSMul.mk, ContinuousSMul.continuous_smul
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
R : Type u_5
α : Type u_6
β : Type u_7
F : Type u_8
inst : FunLike F α β
inst_1 : Semiring R
inst_2 : AddCommMonoid α
inst_3 : AddCommMonoid β
inst_4 : Module R α
inst_5 : Module R β
inst_6 : TopologicalSpace R
inst_7 : LinearMapClass F R α β
tβ : TopologicalSpace β
inst_8 : ContinuousSMul R β
f : F
tα : TopologicalSpace α := TopologicalSpace.induced (⇑f : (a : α) → β) tβ
⊢ ContinuousSMul R α

Tactic:
⟨continuous_induced_rng.2 ?_⟩

Premises used: Iff.mpr, ContinuousSMul.mk, continuous_induced_rng
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
R : Type u_5
α : Type u_6
β : Type u_7
F : Type u_8
inst : FunLike F α β
inst_1 : Semiring R
inst_2 : AddCommMonoid α
inst_3 : AddCommMonoid β
inst_4 : Module R α
inst_5 : Module R β
inst_6 : TopologicalSpace R
inst_7 : LinearMapClass F R α β
tβ : TopologicalSpace β
inst_8 : ContinuousSMul R β
f : F
tα : TopologicalSpace α := TopologicalSpace.induced (⇑f : (a : α) → β) tβ
refine :
  Continuous[instTopologicalSpaceProd, tβ] (Function.comp (β := α) (⇑f : (a : α) → β) fun (p : R × α) ↦ p.1 • p.2)
⊢ ContinuousSMul R α

Tactic:
refine ⟨continuous_induced_rng.2 ?_⟩
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
R : Type u_5
α : Type u_6
β : Type u_7
F : Type u_8
inst : FunLike F α β
inst_1 : Semiring R
inst_2 : AddCommMonoid α
inst_3 : AddCommMonoid β
inst_4 : Module R α
inst_5 : Module R β
inst_6 : TopologicalSpace R
inst_7 : LinearMapClass F R α β
tβ : TopologicalSpace β
inst_8 : ContinuousSMul R β
f : F
tα : TopologicalSpace α := TopologicalSpace.induced (⇑f : (a : α) → β) tβ
simp : Continuous[instTopologicalSpaceProd, tβ] fun (x : R × α) ↦ HSMul.hSMul (β := β) x.1 ((f : (a : α) → β) x.2 : β)
⊢ Continuous[instTopologicalSpaceProd, tβ] (Function.comp (β := α) (⇑f : (a : α) → β) fun (p : R × α) ↦ p.1 • p.2)

Tactic:
simp only [Function.comp_def, map_smul]

Premises used: Function.comp_def, map_smul
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
R : Type u_5
α : Type u_6
β : Type u_7
F : Type u_8
inst : FunLike F α β
inst_1 : Semiring R
inst_2 : AddCommMonoid α
inst_3 : AddCommMonoid β
inst_4 : Module R α
inst_5 : Module R β
inst_6 : TopologicalSpace R
inst_7 : LinearMapClass F R α β
tβ : TopologicalSpace β
inst_8 : ContinuousSMul R β
f : F
tα : TopologicalSpace α := TopologicalSpace.induced (⇑f : (a : α) → β) tβ
⊢ Continuous[instTopologicalSpaceProd, tβ] fun (x : R × α) ↦ HSMul.hSMul (β := β) x.1 ((f : (a : α) → β) x.2 : β)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
α : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : SMul M X
inst_3 : ContinuousSMul M X
f : α → M
g : α → X
l : Filter α
c : M
a : X
hf : Tendsto f l (𝓝 c)
hg : Tendsto g l (𝓝 a)
⊢ Tendsto (fun (x : α) ↦ f x • g x) l (𝓝 (c • a))

Tactic:
(continuous_smul.tendsto _).comp (hf.prodMk_nhds hg)

Premises used: Continuous.tendsto, ContinuousSMul.continuous_smul, Filter.Tendsto.comp, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
α : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : SMul M X
inst_3 : ContinuousSMul M X
f : α → M
l : Filter α
c : M
hf : Tendsto f l (𝓝 c)
a : X
⊢ Tendsto (fun (x : α) ↦ f x • a) l (𝓝 (c • a))

Tactic:
hf.smul tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.smul
-- 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
f : Y → M
g : Y → X
b : Y
s : Set Y
hf : ContinuousWithinAt f s b
hg : ContinuousWithinAt g s b
⊢ ContinuousWithinAt.{u_3, u_2} (Y := X) (fun (x : Y) ↦ f x • g x) s b

Tactic:
Filter.Tendsto.smul hf hg

Premises used: ContinuousWithinAt, Filter.Tendsto.smul
-- 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
f : Y → M
g : Y → X
b : Y
hf : ContinuousAt f b
hg : ContinuousAt g b
⊢ ContinuousAt.{u_3, u_2} (Y := X) (fun (x : Y) ↦ f x • g x) b

Tactic:
Filter.Tendsto.smul hf hg

Premises used: ContinuousAt, Filter.Tendsto.smul
-- 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
f : Y → M
g : Y → X
s : Set Y
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ ContinuousOn.{u_3, u_2} (Y := X) (fun (x : Y) ↦ f x • g x) s

Tactic:
fun x hx => (hf x hx).smul (hg x hx)

Premises used: ContinuousOn, ContinuousWithinAt.smul
-- 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
f : Y → M
g : Y → X
hf : Continuous[inst_2, inst] f
hg : Continuous[inst_2, inst_1] g
⊢ Continuous[inst_2, inst_1] fun (x : Y) ↦ f x • g x

Tactic:
continuous_smul.comp (hf.prodMk hg)

Premises used: Continuous.comp, ContinuousSMul.continuous_smul, 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
inst_3 : SMul M X
inst_4 : ContinuousSMul M X
f : Y → M
g : Y → X
b : Y
s : Set Y
inst_5 : SMul.{u_1, u_2} Mᵐᵒᵖ X
inst_6 : IsCentralScalar M X
suffices : Continuous[instTopologicalSpaceProd, inst_1] fun (p : M × X) ↦ MulOpposite.op p.1 • p.2
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (p : Prod.{u_1, u_2} Mᵐᵒᵖ X) ↦ p.1 • p.2

Tactic:
suffices Continuous fun p : M × X => MulOpposite.op p.fst • p.snd from
      this.comp (MulOpposite.continuous_unop.prodMap continuous_id)
-- 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 : Set Y
inst_5 : SMul.{u_1, u_2} Mᵐᵒᵖ X
inst_6 : IsCentralScalar M X
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (p : M × X) ↦ MulOpposite.op p.1 • p.2

Tactic:
simpa only [op_smul_eq_smul] using (continuous_smul : Continuous fun p : M × X => _)

Premises used: ContinuousSMul.continuous_smul, IsCentralScalar.op_smul_eq_smul
-- 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 : Set Y
⊢ ContinuousSMul.{u_1, u_2} M Xᵐᵒᵖ

Tactic:
⟨MulOpposite.continuous_op.comp <|
      continuous_smul.comp <| continuous_id.prodMap MulOpposite.continuous_unop⟩

Premises used: Continuous.prodMap, Continuous.comp, MulOpposite.continuous_unop, continuous_id, ContinuousSMul.mk, ContinuousSMul.continuous_smul, MulOpposite.continuous_op
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : SMul M X
inst_3 : ContinuousSMul M X
a b : M
x y : X
h₁ : a ⤳ b
h₂ : x ⤳ y
⊢ (a • x) ⤳ (b • y)

Tactic:
(h₁.prod h₂).map continuous_smul

Premises used: Specializes.prod, ContinuousSMul.continuous_smul, Specializes.map
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : SMul M X
inst_3 : ContinuousSMul M X
a b : M
x y : X
h₁ : Inseparable a b
h₂ : Inseparable x y
⊢ Inseparable (a • x) (b • y)

Tactic:
(h₁.prod h₂).map continuous_smul

Premises used: ContinuousSMul.continuous_smul, Inseparable.prod, Inseparable.map
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : SMul M X
inst_3 : ContinuousSMul M X
k : Set M
u : Set X
hk : IsCompact k
hu : IsCompact u
rw : IsCompact.{u_2} (X := X) ((fun (x : M × X) ↦ x.1 • x.2) '' k ×ˢ u)
⊢ IsCompact (k • u)

Tactic:
rw [← Set.image_smul_prod]

Premises used: Set.image_smul_prod
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : SMul M X
inst_3 : ContinuousSMul M X
k : Set M
u : Set X
hk : IsCompact k
hu : IsCompact u
⊢ IsCompact.{u_2} (X := X) ((fun (x : M × X) ↦ x.1 • x.2) '' k ×ˢ u)

Tactic:
IsCompact.image (hk.prod hu) continuous_smul

Premises used: IsCompact.prod, ContinuousSMul.continuous_smul, IsCompact.image
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : SMul M X
inst_3 : ContinuousSMul M X
k : Set M
u : Set X
hk : IsCompact k
hu : IsCompact u
⊢ IsCompact.{u_2} (X := X) ((fun (x : M × X) ↦ x.1 • x.2) '' k ×ˢ u)

Tactic:
exact IsCompact.image (hk.prod hu) continuous_smul

Premises used: IsCompact.prod, ContinuousSMul.continuous_smul, IsCompact.image
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : SMul M X
inst_3 : ContinuousSMul M X
K : Set M
L : Set X
⊢ closure[inst] K • closure[inst_1] L ⊆ closure[inst_1] (K • L)

Tactic:
Set.smul_subset_iff.2 fun _x hx _y hy ↦ map_mem_closure₂ continuous_smul hx hy fun _a ha _b hb ↦
    Set.smul_mem_smul ha hb

Premises used: Iff.mpr, map_mem_closure₂, Set.smul_mem_smul, Set.smul_subset_iff, ContinuousSMul.continuous_smul