awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
p₁ p₂ : Submonoid M
simp_rw : p₁ ⊓ p₂ ≤ ⊥ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
simp_rw₁ : (∀ ⦃x : M⦄, x ∈ p₁ ⊓ p₂ → Membership.mem (γ := Submonoid M) ⊥ x) ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
simp_rw₂ : (∀ ⦃x : M⦄, x ∈ p₁ ∧ x ∈ p₂ → Membership.mem (γ := Submonoid M) ⊥ x) ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
simp_rw₃ : (∀ ⦃x : M⦄, x ∈ p₁ → x ∈ p₂ → Membership.mem (γ := Submonoid M) ⊥ x) ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
⊢ Disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1

Tactic:
simp_rw [disjoint_iff_inf_le, SetLike.le_def, mem_inf, and_imp, mem_bot]

Premises used: and_imp, SetLike.le_def, Submonoid.mem_bot, disjoint_iff_inf_le, Submonoid.mem_inf
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
p₁ p₂ : Submonoid M
⊢ Disjoint p₁ p₂ ↔ ∀ {x y : M}, x ∈ p₁ → y ∈ p₂ → x = y → x = 1

Tactic:
disjoint_def.trans ⟨fun h _ _ hx hy hxy => h hx <| hxy.symm ▸ hy, fun h _ hx hx' => h hx hx' rfl⟩

Premises used: Eq.rec, Iff.intro, Iff.trans, Eq.symm, Submonoid.disjoint_def, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s t : Set M
hts : t ⊆ (↑(closure (s \ t)) : Set M)
⊢ Eq (α := Submonoid M) (closure (s \ t)) (closure s)

Tactic:
(closure_mono Set.diff_subset).antisymm <| closure_le.mpr <| fun x hxs ↦ ?_

Premises used: Iff.mpr, Set.diff_subset, LE.le.antisymm, Submonoid.closure_mono, Submonoid.closure_le
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s t : Set M
hts : t ⊆ (↑(closure (s \ t)) : Set M)
refine : ∀ (x : M) (hxs : x ∈ s), x ∈ (↑(closure (s \ t)) : Set M)
⊢ Eq (α := Submonoid M) (closure (s \ t)) (closure s)

Tactic:
refine (closure_mono Set.diff_subset).antisymm <| closure_le.mpr <| fun x hxs ↦ ?_

Premises used: Iff.mpr, Set.diff_subset, LE.le.antisymm, Submonoid.closure_mono, Submonoid.closure_le
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s t : Set M
hts : t ⊆ (↑(closure (s \ t)) : Set M)
x : M
hxs : x ∈ s
pos : ∀ (hxt : x ∈ t), x ∈ (↑(closure (s \ t)) : Set M)
neg : ∀ (hxt : x ∉ t), x ∈ (↑(closure (s \ t)) : Set M)
⊢ x ∈ (↑(closure (s \ t)) : Set M)

Tactic:
by_cases hxt : x ∈ t
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s t : Set M
hts : t ⊆ (↑(closure (s \ t)) : Set M)
x : M
hxs : x ∈ s
hxt : x ∈ t
⊢ x ∈ (↑(closure (s \ t)) : Set M)

Tactic:
hts hxt
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s t : Set M
hts : t ⊆ (↑(closure (s \ t)) : Set M)
x : M
hxs : x ∈ s
hxt : x ∈ t
⊢ x ∈ (↑(closure (s \ t)) : Set M)

Tactic:
exact hts hxt
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s t : Set M
hts : t ⊆ (↑(closure (s \ t)) : Set M)
x : M
hxs : x ∈ s
hxt : x ∉ t
neg : ∀ (S : Submonoid M), s \ t ⊆ (↑S : Set M) → x ∈ S
⊢ x ∈ (↑(closure (s \ t)) : Set M)

Tactic:
rw [SetLike.mem_coe, Submonoid.mem_closure]

Premises used: Submonoid.mem_closure, SetLike.mem_coe
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s t : Set M
hts : t ⊆ (↑(closure (s \ t)) : Set M)
x : M
hxs : x ∈ s
hxt : x ∉ t
⊢ ∀ (S : Submonoid M), s \ t ⊆ (↑S : Set M) → x ∈ S

Tactic:
fun N hN ↦ hN <| Set.mem_diff_of_mem hxs hxt

Premises used: Set.mem_diff_of_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s t : Set M
hts : t ⊆ (↑(closure (s \ t)) : Set M)
x : M
hxs : x ∈ s
hxt : x ∉ t
⊢ ∀ (S : Submonoid M), s \ t ⊆ (↑S : Set M) → x ∈ S

Tactic:
exact fun N hN ↦ hN <| Set.mem_diff_of_mem hxs hxt
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
inst : MulOneClass M
s : Set M
⊢ {1} ⊆ (↑(closure (s \ {1})) : Set M)

Tactic:
simp [one_mem]

Premises used: OneMemClass.one_mem
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
f g : M →* N
s : Set M
h : Set.EqOn.{u_1, u_2} (β := N) (⇑f : (a : M) → N) (⇑g : (a : M) → N) s
⊢ Set.EqOn.{u_1, u_2} (β := N) (⇑f : (a : M) → N) (⇑g : (a : M) → N) (↑(closure s) : Set M)

Tactic:
show closure s ≤ f.eqLocusM g from closure_le.2 h

Premises used: Iff.mpr, Set.Mem, setOf, Set.EqOn, Submonoid.closure_le
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
s : Set M
hs : Eq (α := Submonoid M) (closure s) ⊤
f g : M →* N
h : Set.EqOn.{u_1, u_2} (β := N) (⇑f : (a : M) → N) (⇑g : (a : M) → N) s
⊢ f = g

Tactic:
eq_of_eqOn_topM <| hs ▸ eqOn_closureM h

Premises used: MonoidHom.eqOn_closureM, Eq.rec, MonoidHom.eq_of_eqOn_topM
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M_1 : Type u_1
N : Type u_2
A : Type u_3
inst : Monoid M_1
inst_1 : Monoid N
s : Set M_1
M : Type u_4
inst_2 : Monoid M
a b : M
ha : Membership.mem (γ := Set M) (setOf IsUnit) a
hb : Membership.mem (γ := Set M) (setOf IsUnit) b
⊢ IsUnit a

Tactic:
rw [Set.mem_setOf_eq] at *

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M_1 : Type u_1
N : Type u_2
A : Type u_3
inst : Monoid M_1
inst_1 : Monoid N
s : Set M_1
M : Type u_4
inst_2 : Monoid M
a b : M
ha : Membership.mem (γ := Set M) (setOf IsUnit) a
hb : Membership.mem (γ := Set M) (setOf IsUnit) b
ha₁ : IsUnit a
⊢ IsUnit b

Tactic:
rw [Set.mem_setOf_eq] at *

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M_1 : Type u_1
N : Type u_2
A : Type u_3
inst : Monoid M_1
inst_1 : Monoid N
s : Set M_1
M : Type u_4
inst_2 : Monoid M
a b : M
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a * b)

Tactic:
IsUnit.mul ha hb

Premises used: IsUnit.mul
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M_1 : Type u_1
N : Type u_2
A : Type u_3
inst : Monoid M_1
inst_1 : Monoid N
s : Set M_1
M : Type u_4
inst_2 : Monoid M
a b : M
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a * b)

Tactic:
exact IsUnit.mul ha hb

Premises used: IsUnit.mul
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M_1 : Type u_1
N : Type u_2
A : Type u_3
inst : Monoid M_1
inst_1 : Monoid N
s : Set M_1
M : Type u_4
inst_2 : Monoid M
⊢ Membership.mem (γ := Set M) (setOf IsUnit) 1

Tactic:
simp only [isUnit_one, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, isUnit_one
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_4
inst : Monoid M
a : M
rw rw₁ : IsUnit a ↔ IsUnit a
⊢ Membership.mem (γ := Set M) (setOf IsUnit) a ↔ IsUnit a

Tactic:
rw [Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M_1 : Type u_1
N_1 : Type u_2
A : Type u_3
inst : Monoid M_1
inst_1 : Monoid N_1
s_1 : Set M_1
M : Type u_4
N : Type u_5
inst_2 : Monoid M
inst_3 : Monoid N
s : Set M
f : M → N
hs : Eq (α := Submonoid M) (closure s) ⊤
h1 : f 1 = 1
hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y
x y : M
rw : f y = f 1 * f y
rw₁ : f y = 1 * f y
rw₂ rw₃ : f y = f y
⊢ f (1 * y) = f 1 * f y

Tactic:
rw [one_mul, h1, one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M_1 : Type u_1
N_1 : Type u_2
A : Type u_3
inst : Monoid M_1
inst_1 : Monoid N_1
s_1 : Set M_1
M : Type u_4
N : Type u_5
inst_2 : Monoid M
inst_3 : Monoid N
s : Set M
f : M → N
hs : Eq (α := Submonoid M) (closure s) ⊤
h1 : f 1 = 1
hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y
x a b : M
ha : ∀ (y : M), f (a * y) = f a * f y
hb : ∀ (y : M), f (b * y) = f b * f y
y : M
rw : f (a * (b * y)) = f (a * b) * f y
rw₁ : f a * f (b * y) = f (a * b) * f y
rw₂ : f a * f (b * y) = f a * f b * f y
rw₃ : f a * (f b * f y) = f a * f b * f y
rw₄ rw₅ : f a * (f b * f y) = f a * (f b * f y)
⊢ f (a * b * y) = f (a * b) * f y

Tactic:
rw [mul_assoc, ha, ha, hb, mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
s : Set M
f : M → N
hs : Eq (α := Submonoid M) (closure s) ⊤
h1 : f 1 = 1
hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y
⊢ (⇑(ofClosureMEqTopLeft (s := s) f hs h1 hmul) : (a : M) → N) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M_1 : Type u_1
N_1 : Type u_2
A : Type u_3
inst : Monoid M_1
inst_1 : Monoid N_1
s_1 : Set M_1
M : Type u_4
N : Type u_5
inst_2 : Monoid M
inst_3 : Monoid N
s : Set M
f : M → N
hs : Eq (α := Submonoid M) (closure s) ⊤
h1 : f 1 = 1
hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y
x y : M
⊢ ∀ (x : M), f (x * 1) = f x * f 1

Tactic:
simp [h1]
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M_1 : Type u_1
N_1 : Type u_2
A : Type u_3
inst : Monoid M_1
inst_1 : Monoid N_1
s_1 : Set M_1
M : Type u_4
N : Type u_5
inst_2 : Monoid M
inst_3 : Monoid N
s : Set M
f : M → N
hs : Eq (α := Submonoid M) (closure s) ⊤
h1 : f 1 = 1
hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y
x_1 y y₁ y₂ : M
h₁ : ∀ (x : M), f (x * y₁) = f x * f y₁
h₂ : ∀ (x : M), f (x * y₂) = f x * f y₂
x : M
⊢ f (x * (y₁ * y₂)) = f x * f (y₁ * y₂)

Tactic:
simp [← mul_assoc, h₁, h₂]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Submonoid.Basic
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
s : Set M
f : M → N
hs : Eq (α := Submonoid M) (closure s) ⊤
h1 : f 1 = 1
hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y
⊢ (⇑(ofClosureMEqTopRight (s := s) f hs h1 hmul) : (a : M) → N) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
B : Type u_3
inst : Monoid M
inst_1 : SetLike B M
inst_2 : SubmonoidClass B M
S : B
l : List ↥S
⊢ (↑l.prod : M) = (List.map (Subtype.val (p := fun (x : M) ↦ x ∈ S)) l).prod

Tactic:
map_list_prod (SubmonoidClass.subtype S : _ →* M) l

Premises used: map_list_prod, SubmonoidClass.subtype
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
B : Type u_3
S : B
M : Type u_4
inst : CommMonoid M
inst_1 : SetLike B M
inst_2 : SubmonoidClass B M
m : Multiset ↥S
⊢ (↑m.prod : M) = (Multiset.map (Subtype.val (p := fun (x : M) ↦ x ∈ S)) m).prod

Tactic:
(SubmonoidClass.subtype S : _ →* M).map_multiset_prod m

Premises used: SubmonoidClass.subtype, MonoidHom.map_multiset_prod
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
B : Type u_3
S : B
ι : Type u_4
M : Type u_5
inst : CommMonoid M
inst_1 : SetLike B M
inst_2 : SubmonoidClass B M
f : ι → ↥S
s : Finset ι
⊢ Eq.{u_5 + 1} (α := M) (↑(∏ i ∈ s, f i) : M) (∏ i ∈ s, (↑(f i) : M))

Tactic:
map_prod (SubmonoidClass.subtype S) f s

Premises used: SubmonoidClass.subtype, map_prod
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
B : Type u_3
inst : Monoid M
inst_1 : SetLike B M
inst_2 : SubmonoidClass B M
S : B
l : List M
hl : ∀ x ∈ l, x ∈ S
⊢ ∀ x ∈ l, x ∈ S

Tactic:
hl
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
B : Type u_3
inst : Monoid M
inst_1 : SetLike B M
inst_2 : SubmonoidClass B M
S : B
l : List M
hl : ∀ x ∈ l, x ∈ S
lift : ∀ (l : List ↥S), (List.map (Subtype.val (p := fun (x : M) ↦ x ∈ S)) l).prod ∈ S
⊢ l.prod ∈ S

Tactic:
lift l to List S using hl

Premises used: Membership.mem, Subtype, List
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
B : Type u_3
inst : Monoid M
inst_1 : SetLike B M
inst_2 : SubmonoidClass B M
S : B
l : List ↥S
rw : (↑l.prod : M) ∈ S
⊢ (List.map (Subtype.val (p := fun (x : M) ↦ x ∈ S)) l).prod ∈ S

Tactic:
rw [← coe_list_prod]

Premises used: SubmonoidClass.coe_list_prod
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
B : Type u_3
inst : Monoid M
inst_1 : SetLike B M
inst_2 : SubmonoidClass B M
S : B
l : List ↥S
⊢ (↑l.prod : M) ∈ S

Tactic:
l.prod.coe_prop

Premises used: Subtype.coe_prop, Set.Mem, List.prod
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
B : Type u_3
inst : Monoid M
inst_1 : SetLike B M
inst_2 : SubmonoidClass B M
S : B
l : List ↥S
⊢ (↑l.prod : M) ∈ S

Tactic:
exact l.prod.coe_prop

Premises used: Subtype.coe_prop, List.prod
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
B : Type u_3
S : B
M : Type u_4
inst : CommMonoid M
inst_1 : SetLike B M
inst_2 : SubmonoidClass B M
m : Multiset M
hm : ∀ a ∈ m, a ∈ S
⊢ ∀ x ∈ m, x ∈ S

Tactic:
hm
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
B : Type u_3
S : B
M : Type u_4
inst : CommMonoid M
inst_1 : SetLike B M
inst_2 : SubmonoidClass B M
m : Multiset M
hm : ∀ a ∈ m, a ∈ S
lift : ∀ (m : Multiset ↥S), (Multiset.map (Subtype.val (p := fun (x : M) ↦ x ∈ S)) m).prod ∈ S
⊢ m.prod ∈ S

Tactic:
lift m to Multiset S using hm

Premises used: Membership.mem, Multiset, Subtype
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
B : Type u_3
S : B
M : Type u_4
inst : CommMonoid M
inst_1 : SetLike B M
inst_2 : SubmonoidClass B M
m : Multiset ↥S
rw : (↑m.prod : M) ∈ S
⊢ (Multiset.map (Subtype.val (p := fun (x : M) ↦ x ∈ S)) m).prod ∈ S

Tactic:
rw [← coe_multiset_prod]

Premises used: SubmonoidClass.coe_multiset_prod
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
B : Type u_3
S : B
M : Type u_4
inst : CommMonoid M
inst_1 : SetLike B M
inst_2 : SubmonoidClass B M
m : Multiset ↥S
⊢ (↑m.prod : M) ∈ S

Tactic:
m.prod.coe_prop

Premises used: Subtype.coe_prop, Set.Mem, Multiset.prod
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
B : Type u_3
S : B
M : Type u_4
inst : CommMonoid M
inst_1 : SetLike B M
inst_2 : SubmonoidClass B M
m : Multiset ↥S
⊢ (↑m.prod : M) ∈ S

Tactic:
exact m.prod.coe_prop

Premises used: Subtype.coe_prop, Multiset.prod
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
B : Type u_3
S : B
M : Type u_4
inst : CommMonoid M
inst_1 : SetLike B M
inst_2 : SubmonoidClass B M
ι : Type u_5
t : Finset ι
f : ι → M
h : ∀ c ∈ t, f c ∈ S
⊢ ∏ c ∈ t, f c ∈ S

Tactic:
multiset_prod_mem (t.1.map f) fun _x hx =>
    let ⟨i, hi, hix⟩ := Multiset.mem_map.1 hx
    hix ▸ h i hi

Premises used: Multiset.map, Set.Mem, multiset_prod_mem, Multiset.mem_map, Membership.mem, Eq.rec, Finset.val, Finset.prod, Iff.mp, _private.0.prod_mem.match_1
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : Monoid M
s : Submonoid M
l : List ↥s
⊢ (↑l.prod : M) = (List.map (Subtype.val (p := fun (x : M) ↦ x ∈ s)) l).prod

Tactic:
map_list_prod s.subtype l

Premises used: map_list_prod, Submonoid.subtype
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_4
inst : CommMonoid M
S : Submonoid M
m : Multiset ↥S
⊢ (↑m.prod : M) = (Multiset.map (Subtype.val (p := fun (x : M) ↦ x ∈ S)) m).prod

Tactic:
S.subtype.map_multiset_prod m

Premises used: Submonoid.subtype, MonoidHom.map_multiset_prod
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
ι : Type u_4
M : Type u_5
inst : CommMonoid M
S : Submonoid M
f : ι → ↥S
s : Finset ι
⊢ Eq.{u_5 + 1} (α := M) (↑(∏ i ∈ s, f i) : M) (∏ i ∈ s, (↑(f i) : M))

Tactic:
map_prod S.subtype f s

Premises used: map_prod, Submonoid.subtype
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : Monoid M
s : Submonoid M
l : List M
hl : ∀ x ∈ l, x ∈ s
⊢ l.prod ∈ s

Tactic:
_root_.list_prod_mem hl

Premises used: list_prod_mem
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_4
inst : CommMonoid M
S : Submonoid M
m : Multiset M
hm : ∀ a ∈ m, a ∈ S
⊢ m.prod ∈ S

Tactic:
_root_.multiset_prod_mem m hm

Premises used: multiset_prod_mem
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
l : List M
comm : Set.Pairwise.{u_1} (α := M) {x : M | x ∈ ⟦l⟧} Commute
h : ∀ x ∈ ⟦l⟧, x ∈ S
⊢ Multiset.noncommProd ⟦l⟧ comm ∈ S

Tactic:
?_
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
m : Multiset M
comm : Set.Pairwise.{u_1} (α := M) {x : M | x ∈ m} Commute
h : ∀ x ∈ m, x ∈ S
h₁ :
  ∀ (l : List M) (comm : Set.Pairwise.{u_1} (α := M) {x : M | x ∈ ⟦l⟧} Commute) (h : ∀ x ∈ ⟦l⟧, x ∈ S),
    Multiset.noncommProd ⟦l⟧ comm ∈ S
⊢ m.noncommProd comm ∈ S

Tactic:
induction m using Quotient.inductionOn with | h l => ?_
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
l : List M
comm : Set.Pairwise.{u_1} (α := M) {x : M | x ∈ ⟦l⟧} Commute
h : ∀ x ∈ ⟦l⟧, x ∈ S
h₁ : l.prod ∈ S
⊢ Multiset.noncommProd ⟦l⟧ comm ∈ S

Tactic:
simp only [Multiset.quot_mk_to_coe, Multiset.noncommProd_coe]

Premises used: Multiset.noncommProd_coe, Multiset.quot_mk_to_coe
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
l : List M
comm : Set.Pairwise.{u_1} (α := M) {x : M | x ∈ ⟦l⟧} Commute
h : ∀ x ∈ ⟦l⟧, x ∈ S
⊢ l.prod ∈ S

Tactic:
Submonoid.list_prod_mem _ h

Premises used: Submonoid.list_prod_mem
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
l : List M
comm : Set.Pairwise.{u_1} (α := M) {x : M | x ∈ ⟦l⟧} Commute
h : ∀ x ∈ ⟦l⟧, x ∈ S
⊢ l.prod ∈ S

Tactic:
exact Submonoid.list_prod_mem _ h

Premises used: Submonoid.list_prod_mem
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_4
inst : CommMonoid M
S : Submonoid M
ι : Type u_5
t : Finset ι
f : ι → M
h : ∀ c ∈ t, f c ∈ S
⊢ ∏ c ∈ t, f c ∈ S

Tactic:
S.multiset_prod_mem (t.1.map f) fun _ hx =>
    let ⟨i, hi, hix⟩ := Multiset.mem_map.1 hx
    hix ▸ h i hi

Premises used: Multiset.map, Set.Mem, Multiset.mem_map, Membership.mem, Eq.rec, Finset.val, Finset.prod, Submonoid.multiset_prod_mem, Iff.mp, _private.0.prod_mem.match_1
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t : Set ι).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
h₁ : ∀ x ∈ Multiset.map f t.val, x ∈ S
⊢ t.noncommProd f comm ∈ S

Tactic:
apply multiset_noncommProd_mem

Premises used: Submonoid.multiset_noncommProd_mem
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t : Set ι).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
y : M
h₁ : (∃ a ∈ t.val, f a = y) → y ∈ S
⊢ y ∈ Multiset.map f t.val → y ∈ S

Tactic:
rw [Multiset.mem_map]

Premises used: Multiset.mem_map
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t : Set ι).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
x : ι
hx : x ∈ t.val
⊢ f x ∈ S

Tactic:
h x hx
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t : Set ι).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
x : ι
hx : x ∈ t.val
⊢ f x ∈ S

Tactic:
exact h x hx
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
⊢ (↑∅ : Set M) ⊆ s ∧
    Function.support (M := ℕ) 0 ⊆ (↑∅ : Set M) ∧ Eq.{u_1 + 1} (α := M) (∏ a ∈ ∅, HPow.hPow (β := ℕ) a (0 a)) 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
⊢ ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ Eq (α := M) (∏ a ∈ t, a ^ f a) 1

Tactic:
exact ⟨0, ∅, by simp⟩
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
x_1 : M
s : Set M
x : M
hx : x ∈ s
⊢ (↑{x} : Set M) ⊆ s ∧
    Function.support (M := ℕ) (Pi.single (M := fun (a : M) ↦ ℕ) x 1) ⊆ (↑{x} : Set M) ∧
      ∏ a ∈ {x}, HPow.hPow (β := ℕ) a (Pi.single (M := fun (a : M) ↦ ℕ) x 1 a : ℕ) = x

Tactic:
simp [hx, Pi.single_apply]

Premises used: Pi.single_apply
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
x_1 : M
s : Set M
x : M
hx : x ∈ s
⊢ ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x

Tactic:
exact ⟨Pi.single x 1, {x}, by simp [hx, Pi.single_apply]⟩
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
x_1 : M
s : Set M
x y : M
hx_1 : Membership.mem (γ := Submonoid M) (closure s) x
hy_1 : Membership.mem (γ := Submonoid M) (closure s) y
hx : ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x
hy : ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = y
mul :
  ∀ (f : M → ℕ) (t : Finset M) (hts : (↑t : Set M) ⊆ s) (hf : Function.support f ⊆ (↑t : Set M)),
    Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ f a) →
      ∃ (f_1 : M → ℕ) (t_1 : Finset M),
        (↑t_1 : Set M) ⊆ s ∧ Function.support f_1 ⊆ (↑t_1 : Set M) ∧ ∏ a ∈ t_1, a ^ f_1 a = (∏ a ∈ t, a ^ f a) * y
⊢ ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = x * y

Tactic:
obtain ⟨f, t, hts, hf, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
y : M
hy_1 : Membership.mem (γ := Submonoid M) (closure s) y
hy : ∃ (f : M → ℕ) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∏ a ∈ t, a ^ f a = y
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ s
hf : Function.support f ⊆ (↑t : Set M)
hx : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ f a)
mul :
  ∀ (g : M → ℕ) (u : Finset M) (hus : (↑u : Set M) ⊆ s) (hg : Function.support g ⊆ (↑u : Set M)),
    Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ u, a ^ g a) →
      ∃ (f_1 : M → ℕ) (t_1 : Finset M),
        (↑t_1 : Set M) ⊆ s ∧
          Function.support f_1 ⊆ (↑t_1 : Set M) ∧
            ∏ a ∈ t_1, a ^ f_1 a = HMul.hMul (α := M) (∏ a ∈ t, a ^ f a) (∏ a ∈ u, a ^ g a)
⊢ ∃ (f_1 : M → ℕ) (t_1 : Finset M),
    (↑t_1 : Set M) ⊆ s ∧ Function.support f_1 ⊆ (↑t_1 : Set M) ∧ ∏ a ∈ t_1, a ^ f_1 a = (∏ a ∈ t, a ^ f a) * y

Tactic:
obtain ⟨g, u, hus, hg, rfl⟩ := hy

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ s
hf : Function.support f ⊆ (↑t : Set M)
hx : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ f a)
g : M → ℕ
u : Finset M
hus : (↑u : Set M) ⊆ s
hg : Function.support g ⊆ (↑u : Set M)
hy : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ u, a ^ g a)
⊢ ∃ (f_1 : M → ℕ) (t_1 : Finset M),
    (↑t_1 : Set M) ⊆ s ∧
      Function.support f_1 ⊆ (↑t_1 : Set M) ∧
        ∏ a ∈ t_1, a ^ f_1 a = HMul.hMul (α := M) (∏ a ∈ t, a ^ f a) (∏ a ∈ u, a ^ g a)

Tactic:
⟨f + g, t ∪ u, mod_cast Set.union_subset hts hus,
      (Function.support_add _ _).trans <| mod_cast Set.union_subset_union hf hg, ?_⟩

Premises used: Set.union_subset_union, congrArg, Finset.coe_union._simp_1, cast, HasSubset.Subset.trans, HasSubset.Subset, Function.support_add, Set.union_subset, HAdd.hAdd, Function.support, And.intro, Exists.intro, congrFun', Union.union
-- Module: Mathlib.Algebra.Group.Submonoid.BigOperators
Goal:
M : Type u_1
inst : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : (↑t : Set M) ⊆ s
hf : Function.support f ⊆ (↑t : Set M)
hx : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ t, a ^ f a)
g : M → ℕ
u : Finset M
hus : (↑u : Set M) ⊆ s
hg : Function.support g ⊆ (↑u : Set M)
hy : Membership.mem (γ := Submonoid M) (closure s) (∏ a ∈ u, a ^ g a)
mul : ∏ a ∈ t ∪ u, a ^ (f + g) a = HMul.hMul (α := M) (∏ a ∈ t, a ^ f a) (∏ a ∈ u, a ^ g a)
⊢ ∃ (f_1 : M → ℕ) (t_1 : Finset M),
    (↑t_1 : Set M) ⊆ s ∧
      Function.support f_1 ⊆ (↑t_1 : Set M) ∧
        ∏ a ∈ t_1, a ^ f_1 a = HMul.hMul (α := M) (∏ a ∈ t, a ^ f a) (∏ a ∈ u, a ^ g a)

Tactic:
refine ⟨f + g, t ∪ u, mod_cast Set.union_subset hts hus,
      (Function.support_add _ _).trans <| mod_cast Set.union_subset_union hf hg, ?_⟩