awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
h : ∀ (i : ι), Membership.mem (γ := List ι) [] i → Tendsto (f i) x (𝓝 (a i))
⊢ Tendsto (fun (b : α) ↦ List.prod (List.map (fun (c : ι) ↦ f c b) [])) x (𝓝 (List.map a []).prod)

Tactic:
simp [tendsto_const_nhds]

Premises used: tendsto_const_nhds
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : ContinuousMul M
f_1 : ι → α → M
x : Filter α
a : ι → M
f : ι
l : List ι
h : ∀ i ∈ f :: l, Tendsto (f_1 i) x (𝓝 (a i))
simp :
  Tendsto (fun (b : α) ↦ f_1 f b * List.prod (List.map (fun (c : ι) ↦ f_1 c b) l)) x (𝓝 (a f * (List.map a l).prod))
⊢ Tendsto (fun (b : α) ↦ List.prod (List.map (fun (c : ι) ↦ f_1 c b) (f :: l))) x (𝓝 (List.map a (f :: l)).prod)

Tactic:
simp only [List.map_cons, List.prod_cons]

Premises used: List.map_cons, List.prod_cons
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : ContinuousMul M
f_1 : ι → α → M
x : Filter α
a : ι → M
f : ι
l : List ι
h : ∀ i ∈ f :: l, Tendsto (f_1 i) x (𝓝 (a i))
⊢ Tendsto (fun (b : α) ↦ f_1 f b * List.prod (List.map (fun (c : ι) ↦ f_1 c b) l)) x (𝓝 (a f * (List.map a l).prod))

Tactic:
(h f List.mem_cons_self).mul
        (tendsto_list_prod l fun c hc => h c (List.mem_cons_of_mem _ hc))

Premises used: List.mem_cons_of_mem, Filter.Tendsto.mul, List.mem_cons_self
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : ContinuousMul M
f_1 : ι → α → M
x : Filter α
a : ι → M
f : ι
l : List ι
h : ∀ i ∈ f :: l, Tendsto (f_1 i) x (𝓝 (a i))
⊢ Tendsto (fun (b : α) ↦ f_1 f b * List.prod (List.map (fun (c : ι) ↦ f_1 c b) l)) x (𝓝 (a f * (List.map a l).prod))

Tactic:
exact
      (h f List.mem_cons_self).mul
        (tendsto_list_prod l fun c hc => h c (List.mem_cons_of_mem _ hc))

Premises used: List.mem_cons_of_mem, Filter.Tendsto.mul, List.mem_cons_self
-- 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 : Monoid M
inst_3 : ContinuousMul M
f : ι → X → M
l : List ι
h : ∀ i ∈ l, Continuous[inst, inst_1] (f i)
⊢ Continuous[inst, inst_1] fun (a : X) ↦ List.prod (List.map (fun (i : ι) ↦ f i a) l)

Tactic:
continuous_iff_continuousAt.2 fun x =>
    tendsto_list_prod l fun c hc => continuous_iff_continuousAt.1 (h c hc) x

Premises used: tendsto_list_prod, Iff.mpr, Iff.mp, 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 : Monoid M
inst_3 : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ i ∈ l, ContinuousOn (f i) t
x : X
hx : x ∈ t
rw :
  ContinuousAt.{u_5, u_3} (Y := M)
    (t.restrict (π := fun (a : X) ↦ M) fun (a : X) ↦ List.prod (List.map (fun (i : ι) ↦ f i a) l))
    (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx)
⊢ ContinuousWithinAt.{u_5, u_3} (Y := M) (fun (a : X) ↦ List.prod (List.map (fun (i : ι) ↦ f i a) l)) t x

Tactic:
rw [continuousWithinAt_iff_continuousAt_restrict _ hx]

Premises used: continuousWithinAt_iff_continuousAt_restrict
-- 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 : Monoid M
inst_3 : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ i ∈ l, ContinuousOn (f i) t
x : X
hx : x ∈ t
⊢ ContinuousAt.{u_5, u_3} (Y := M)
    (t.restrict (π := fun (a : X) ↦ M) fun (a : X) ↦ List.prod (List.map (fun (i : ι) ↦ f i a) l))
    (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx)

Tactic:
tendsto_list_prod _ fun i hi => ?_

Premises used: tendsto_list_prod, ContinuousAt, Set.restrict
-- 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 : Monoid M
inst_3 : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ i ∈ l, ContinuousOn (f i) t
x : X
hx : x ∈ t
refine :
  ∀ (i : ι) (hi : i ∈ l),
    Tendsto (fun (b : (↑t : Type u_5)) ↦ f i (↑b : X)) (𝓝 (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx))
      (𝓝 (f i (↑(Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx) : X)))
⊢ ContinuousAt.{u_5, u_3} (Y := M)
    (t.restrict (π := fun (a : X) ↦ M) fun (a : X) ↦ List.prod (List.map (fun (i : ι) ↦ f i a) l))
    (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx)

Tactic:
refine tendsto_list_prod _ fun i hi => ?_

Premises used: tendsto_list_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 : Monoid M
inst_3 : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ i ∈ l, ContinuousOn (f i) t
x : X
hx : x ∈ t
i : ι
hi : i ∈ l
⊢ ContinuousWithinAt (f i) t x

Tactic:
specialize h i hi x hx
-- 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 : Monoid M
inst_3 : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
x : X
hx : x ∈ t
i : ι
hi : i ∈ l
h : ContinuousWithinAt (f i) t x
⊢ ContinuousAt (t.restrict (π := fun (a : X) ↦ M) (f i)) (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx)

Tactic:
rw [continuousWithinAt_iff_continuousAt_restrict _ hx] at h

Premises used: continuousWithinAt_iff_continuousAt_restrict
-- 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 : Monoid M
inst_3 : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
x : X
hx : x ∈ t
i : ι
hi : i ∈ l
h : ContinuousAt (t.restrict (π := fun (a : X) ↦ M) (f i)) (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx)
⊢ Tendsto (fun (b : (↑t : Type u_5)) ↦ f i (↑b : X)) (𝓝 (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx))
    (𝓝 (f i (↑(Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx) : X)))

Tactic:
h

Premises used: ContinuousAt, Set.restrict
-- 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 : Monoid M
inst_3 : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
x : X
hx : x ∈ t
i : ι
hi : i ∈ l
h : ContinuousAt (t.restrict (π := fun (a : X) ↦ M) (f i)) (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx)
⊢ Tendsto (fun (b : (↑t : Type u_5)) ↦ f i (↑b : X)) (𝓝 (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx))
    (𝓝 (f i (↑(Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx) : X)))

Tactic:
exact h
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : ContinuousMul M
⊢ Continuous[inst, inst] fun (a : M) ↦ HPow.hPow (β := ℕ) a 0

Tactic:
simpa using continuous_const

Premises used: continuous_const
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : ContinuousMul M
k : ℕ
simp : Continuous[inst, inst] fun (a : M) ↦ a * a ^ k
⊢ Continuous[inst, inst] fun (a : M) ↦ a ^ (k + 1)

Tactic:
simp only [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : ContinuousMul M
k : ℕ
⊢ Continuous[inst, inst] fun (a : M) ↦ a * a ^ k

Tactic:
continuous_id.mul (continuous_pow _)

Premises used: Continuous.mul, continuous_id
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : ContinuousMul M
k : ℕ
⊢ Continuous[inst, inst] fun (a : M) ↦ a * a ^ k

Tactic:
exact continuous_id.mul (continuous_pow _)

Premises used: Continuous.mul, continuous_id
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Monoid M
inst_3 : ContinuousMul M
A : Type u_6
inst_4 : AddMonoid A
inst_5 : TopologicalSpace A
inst_6 : ContinuousAdd A
⊢ ContinuousConstSMul ℕ A

Tactic:
⟨continuous_nsmul⟩

Premises used: continuous_nsmul, ContinuousConstSMul.mk
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Monoid M
inst_3 : ContinuousMul M
A : Type u_6
inst_4 : AddMonoid A
inst_5 : TopologicalSpace A
inst_6 : ContinuousAdd A
⊢ ContinuousSMul ℕ A

Tactic:
⟨continuous_prod_of_discrete_left.mpr continuous_nsmul⟩

Premises used: Iff.mpr, continuous_nsmul, continuous_prod_of_discrete_left, ContinuousSMul.mk
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Monoid M
inst_3 : ContinuousMul M
f : X → M
h : Continuous[inst, inst_1] f
n : ℕ
⊢ Continuous[inst, inst_1] fun (b : X) ↦ f b ^ n

Tactic:
(continuous_pow n).comp h

Premises used: Continuous.comp, continuous_pow
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : ContinuousMul M
s : Set M
n : ℕ
⊢ ContinuousOn (Y := M) (fun (x : M) ↦ x ^ n) s

Tactic:
(continuous_pow n).continuousOn

Premises used: Continuous.continuousOn, continuous_pow
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : ContinuousMul M
x : M
n : ℕ
⊢ ContinuousAt (Y := M) (fun (x : M) ↦ x ^ n) x

Tactic:
(continuous_pow n).continuousAt

Premises used: Continuous.continuousAt, continuous_pow
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
α : Type u_2
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : ContinuousMul M
l : Filter α
f : α → M
x : M
hf : Tendsto f l (𝓝 x)
n : ℕ
⊢ Tendsto (fun (x : α) ↦ f x ^ n) l (𝓝 (x ^ n))

Tactic:
(continuousAt_pow _ _).tendsto.comp hf

Premises used: ContinuousAt.tendsto, Filter.Tendsto.comp, continuousAt_pow
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Monoid M
inst_3 : ContinuousMul M
f : X → M
x : X
s : Set X
hf : ContinuousWithinAt f s x
n : ℕ
⊢ ContinuousWithinAt.{u_5, u_3} (Y := M) (fun (x : X) ↦ f x ^ n) s x

Tactic:
Filter.Tendsto.pow hf n

Premises used: ContinuousWithinAt, Filter.Tendsto.pow
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Monoid M
inst_3 : ContinuousMul M
f : X → M
x : X
hf : ContinuousAt f x
n : ℕ
⊢ ContinuousAt.{u_5, u_3} (Y := M) (fun (x : X) ↦ f x ^ n) x

Tactic:
Filter.Tendsto.pow hf n

Premises used: ContinuousAt, Filter.Tendsto.pow
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Monoid M
inst_3 : ContinuousMul M
f : X → M
s : Set X
hf : ContinuousOn f s
n : ℕ
⊢ ContinuousOn.{u_5, u_3} (Y := M) (fun (x : X) ↦ f x ^ n) s

Tactic:
fun x hx => (hf x hx).pow n

Premises used: ContinuousWithinAt.pow, ContinuousOn
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Monoid M
inst_3 : ContinuousMul M
R : Type u_6
A : Type u_7
inst_4 : Monoid A
inst_5 : SMul R A
inst_6 : IsScalarTower R A A
inst_7 : TopologicalSpace A
inst_8 : SeparatelyContinuousMul A
q : R
simp : Continuous[inst_7, inst_7] fun (x : A) ↦ HSMul.hSMul (β := A) q 1 * x
⊢ Continuous[inst_7, inst_7] fun (x : A) ↦ q • x

Tactic:
simp +singlePass only [← smul_one_mul q (_ : A)]

Premises used: smul_one_mul
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Monoid M
inst_3 : ContinuousMul M
R : Type u_6
A : Type u_7
inst_4 : Monoid A
inst_5 : SMul R A
inst_6 : IsScalarTower R A A
inst_7 : TopologicalSpace A
inst_8 : SeparatelyContinuousMul A
q : R
⊢ Continuous[inst_7, inst_7] fun (x : A) ↦ HSMul.hSMul (β := A) q 1 * x

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Monoid M
inst_3 : ContinuousMul M
R : Type u_6
A : Type u_7
inst_4 : Monoid A
inst_5 : SMul R A
inst_6 : SMulCommClass R A A
inst_7 : TopologicalSpace A
inst_8 : SeparatelyContinuousMul A
q : R
simp : Continuous[inst_7, inst_7] fun (x : A) ↦ x * HSMul.hSMul (β := A) q 1
⊢ Continuous[inst_7, inst_7] fun (x : A) ↦ q • x

Tactic:
simp +singlePass only [← mul_smul_one q (_ : A)]

Premises used: mul_smul_one
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Monoid M
inst_3 : ContinuousMul M
R : Type u_6
A : Type u_7
inst_4 : Monoid A
inst_5 : SMul R A
inst_6 : SMulCommClass R A A
inst_7 : TopologicalSpace A
inst_8 : SeparatelyContinuousMul A
q : R
⊢ Continuous[inst_7, inst_7] fun (x : A) ↦ x * HSMul.hSMul (β := A) q 1

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace α
inst_2 : Monoid α
inst_3 : ContinuousMul α
⊢ ContinuousMul.{u_2} αˣ

Tactic:
isInducing_embedProduct.continuousMul (embedProduct α)

Premises used: Topology.IsInducing.continuousMul, Units.embedProduct, Units.isInducing_embedProduct
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
N : Type u_4
inst : Monoid M
inst_1 : Monoid N
inst_2 : TopologicalSpace M
inst_3 : TopologicalSpace N
f : M →* N
hf : Continuous[inst_2, inst_3] (⇑f : (a : M) → N)
⊢ Continuous[Units.instTopologicalSpaceUnits, Units.instTopologicalSpaceUnits] (⇑(Units.map f) : (a : Mˣ) → Nˣ)

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

Premises used: Iff.mpr, Units.continuous_val, Continuous.comp, Units.continuous_iff, And.intro, Units.continuous_coe_inv
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : CommMonoid M
S : Submonoid M
oS : IsOpen[inst] (↑S : Set M)
⊢ Membership.mem (γ := Filter M) (𝓝 1) (↑S : Set M)

Tactic:
IsOpen.mem_nhds oS S.one_mem

Premises used: Submonoid.one_mem, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
inst : TopologicalSpace M
inst_1 : CommMonoid M
inst_2 : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
s : Multiset ι
mk :
  ∀ (l : List ι),
    (∀ (i : ι),
        Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) i →
          Tendsto (f i) x (𝓝 (a i))) →
      Tendsto
        (fun (b : α) ↦
          Multiset.prod (Multiset.map (fun (c : ι) ↦ f c b) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)))
        x (𝓝 (Multiset.map a (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)).prod)
⊢ (∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) →
    Tendsto (fun (b : α) ↦ Multiset.prod (Multiset.map (fun (c : ι) ↦ f c b) s)) x (𝓝 (Multiset.map a s).prod)

Tactic:
rcases s with ⟨l⟩
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
inst : TopologicalSpace M
inst_1 : CommMonoid M
inst_2 : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
s : Multiset ι
l : List ι
⊢ (∀ (i : ι),
      Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) i →
        Tendsto (f i) x (𝓝 (a i))) →
    Tendsto
      (fun (b : α) ↦
        Multiset.prod (Multiset.map (fun (c : ι) ↦ f c b) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)))
      x (𝓝 (Multiset.map a (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)).prod)

Tactic:
simpa using tendsto_list_prod l

Premises used: tendsto_list_prod
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
inst : TopologicalSpace M
inst_1 : CommMonoid M
inst_2 : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
s : Finset ι
⊢ (∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) → Tendsto.{u_2, u_3} (β := M) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))

Tactic:
tendsto_multiset_prod _

Premises used: tendsto_multiset_prod, Set.Mem, setOf, Finset.prod, Multiset.Mem
-- 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
s : Multiset ι
mk :
  ∀ (l : List ι),
    (∀ (i : ι),
        Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) i →
          Continuous[inst, inst_1] (f i)) →
      Continuous[inst, inst_1] fun (a : X) ↦
        Multiset.prod (Multiset.map (fun (i : ι) ↦ f i a) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l))
⊢ (∀ i ∈ s, Continuous[inst, inst_1] (f i)) →
    Continuous[inst, inst_1] fun (a : X) ↦ Multiset.prod (Multiset.map (fun (i : ι) ↦ f i a) s)

Tactic:
rcases s with ⟨l⟩
-- 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
s : Multiset ι
l : List ι
⊢ (∀ (i : ι),
      Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) i →
        Continuous[inst, inst_1] (f i)) →
    Continuous[inst, inst_1] fun (a : X) ↦
      Multiset.prod (Multiset.map (fun (i : ι) ↦ f i a) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l))

Tactic:
simpa using continuous_list_prod l

Premises used: continuous_list_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
s : Multiset ι
t : Set X
mk :
  ∀ (l : List ι),
    (∀ (i : ι),
        Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) i →
          ContinuousOn (f i) t) →
      ContinuousOn.{u_5, u_3} (Y := M)
        (fun (a : X) ↦
          Multiset.prod (Multiset.map (fun (i : ι) ↦ f i a) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)))
        t
⊢ (∀ i ∈ s, ContinuousOn (f i) t) →
    ContinuousOn.{u_5, u_3} (Y := M) (fun (a : X) ↦ Multiset.prod (Multiset.map (fun (i : ι) ↦ f i a) s)) t

Tactic:
rcases s with ⟨l⟩
-- 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
s : Multiset ι
t : Set X
l : List ι
⊢ (∀ (i : ι),
      Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) i →
        ContinuousOn (f i) t) →
    ContinuousOn.{u_5, u_3} (Y := M)
      (fun (a : X) ↦
        Multiset.prod (Multiset.map (fun (i : ι) ↦ f i a) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)))
      t

Tactic:
simpa using continuousOn_list_prod l

Premises used: continuousOn_list_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
s : Finset ι
⊢ (∀ i ∈ s, Continuous[inst, inst_1] (f i)) → Continuous[inst, inst_1] fun (a : X) ↦ ∏ i ∈ s, f i a

Tactic:
continuous_multiset_prod _

Premises used: Set.Mem, setOf, Finset.prod, continuous_multiset_prod, Multiset.Mem
-- 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
s : Finset ι
t : Set X
⊢ (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn.{u_5, u_3} (Y := M) (fun (a : X) ↦ ∏ i ∈ s, f i a) t

Tactic:
continuousOn_multiset_prod _

Premises used: Set.Mem, setOf, Finset.prod, Multiset.Mem, continuousOn_multiset_prod
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
X : Type u_6
M : Type u_7
inst : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ i ∈ s, f i =ᶠ[l] g i
rwa rwa₁ rwa₂ rwa₃ : ∀ i ∈ s, ∀ᶠ (x : X) in l, f i x = g i x
⊢ ∀ᶠ (x : X) in l, ∀ i ∈ s, f i x = g i x

Tactic:
rwa [eventually_all_finset]

Premises used: Filter.eventually_all_finset
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
X : Type u_6
M : Type u_7
inst : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ i ∈ s, f i =ᶠ[l] g i
⊢ ∀ᶠ (x : X) in l, ∀ i ∈ s, f i x = g i x

Tactic:
replace hs : ∀ᶠ x in l, ∀ i ∈ s, f i x = g i x := by rwa [eventually_all_finset]
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
X : Type u_6
M : Type u_7
inst : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ᶠ (x : X) in l, ∀ i ∈ s, f i x = g i x
h : ∀ (x : X) (hx : ∀ i ∈ s, f i x = g i x), Eq.{u_7 + 1} (α := M) ((∏ i ∈ s, f i) x) ((∏ i ∈ s, g i) x)
⊢ EventuallyEq.{u_6, u_7} (β := M) l (∏ i ∈ s, f i) (∏ i ∈ s, g i)

Tactic:
filter_upwards [hs] with x hx
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
X : Type u_6
M : Type u_7
inst : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ᶠ (x : X) in l, ∀ i ∈ s, f i x = g i x
x : X
hx : ∀ i ∈ s, f i x = g i x
⊢ Eq.{u_7 + 1} (α := M) ((∏ i ∈ s, f i) x) ((∏ i ∈ s, g i) x)

Tactic:
simp only [Finset.prod_apply, Finset.prod_congr rfl hx]

Premises used: Finset.prod_apply, Finset.prod_congr, rfl
-- 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
rcases :
  ∀ (U : Set X) (hxU : U ∈ 𝓝 x₀)
    (hUf : Set.Finite.{u_1} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ U).Nonempty}),
    ∃ (I : Finset ι), ∀ᶠ (x : X) in 𝓝 x₀, (mulSupport.{u_1, u_6} (M := M) fun (i : ι) ↦ f i x) ⊆ (↑I : Set ι)
⊢ ∃ (I : Finset ι), ∀ᶠ (x : X) in 𝓝 x₀, (mulSupport.{u_1, u_6} (M := M) fun (i : ι) ↦ f i x) ⊆ (↑I : Set ι)

Tactic:
rcases hf x₀ with ⟨U, hxU, hUf⟩
-- 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}
⊢ ∃ (I : Finset ι), ∀ᶠ (x : X) in 𝓝 x₀, (mulSupport.{u_1, u_6} (M := M) fun (i : ι) ↦ f i x) ⊆ (↑I : Set ι)

Tactic:
⟨hUf.toFinset, mem_of_superset hxU fun y hy i hi => ?_⟩

Premises used: Set.Finite.toFinset, Exists.intro, Filter.mem_of_superset
-- 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}
refine :
  ∀ (y : X) (hy : y ∈ U) (i : ι)
    (hi : Membership.mem (γ := Set ι) (mulSupport.{u_1, u_6} (M := M) fun (i : ι) ↦ f i y) i),
    i ∈ (↑(hUf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ U).Nonempty})) : Set ι)
⊢ ∃ (I : Finset ι), ∀ᶠ (x : X) in 𝓝 x₀, (mulSupport.{u_1, u_6} (M := M) fun (i : ι) ↦ f i x) ⊆ (↑I : Set ι)

Tactic:
refine ⟨hUf.toFinset, mem_of_superset hxU fun y hy i hi => ?_⟩
-- 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
rw : Membership.mem (γ := Set ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ U).Nonempty} i
⊢ i ∈ (↑(hUf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ U).Nonempty})) : Set ι)

Tactic:
rw [hUf.coe_toFinset]

Premises used: Set.Finite.coe_toFinset