[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
x y z : M
x✝¹ : y ∈ powers x
x✝ : z ∈ powers x
n₁ : ℕ
h₁ : x ^ n₁ = y
n₂ : ℕ
h₂ : x ^ n₂ = z
⊢ x ^ (n₁ + n₂) = y * z
[PROOFSTEP]
simp only [pow_add, *]
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
⊢ IsSubmonoid Set.univ
[PROOFSTEP]
constructor
[GOAL]
case one_mem
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
⊢ 1 ∈ Set.univ
[PROOFSTEP]
simp
[GOAL]
case mul_mem
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
⊢ ∀ {a b : M}, a ∈ Set.univ → b ∈ Set.univ → a * b ∈ Set.univ
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
inst✝² : Monoid M
s✝ : Set M
A : Type u_2
inst✝¹ : AddMonoid A
t : Set A
N : Type u_3
inst✝ : Monoid N
f : M → N
hf : IsMonoidHom f
s : Set N
hs : IsSubmonoid s
⊢ f 1 ∈ s
[PROOFSTEP]
rw [IsMonoidHom.map_one hf]
[GOAL]
M : Type u_1
inst✝² : Monoid M
s✝ : Set M
A : Type u_2
inst✝¹ : AddMonoid A
t : Set A
N : Type u_3
inst✝ : Monoid N
f : M → N
hf : IsMonoidHom f
s : Set N
hs : IsSubmonoid s
⊢ 1 ∈ s
[PROOFSTEP]
exact hs.one_mem
[GOAL]
M : Type u_1
inst✝² : Monoid M
s✝ : Set M
A : Type u_2
inst✝¹ : AddMonoid A
t : Set A
N : Type u_3
inst✝ : Monoid N
f : M → N
hf : IsMonoidHom f
s : Set N
hs : IsSubmonoid s
a b : M
ha : f a ∈ s
hb : f b ∈ s
⊢ f (a * b) ∈ s
[PROOFSTEP]
rw [IsMonoidHom.map_mul' hf]
[GOAL]
M : Type u_1
inst✝² : Monoid M
s✝ : Set M
A : Type u_2
inst✝¹ : AddMonoid A
t : Set A
N : Type u_3
inst✝ : Monoid N
f : M → N
hf : IsMonoidHom f
s : Set N
hs : IsSubmonoid s
a b : M
ha : f a ∈ s
hb : f b ∈ s
⊢ f a * f b ∈ s
[PROOFSTEP]
exact hs.mul_mem ha hb
[GOAL]
M : Type u_1
inst✝² : Monoid M
s✝ : Set M
A : Type u_2
inst✝¹ : AddMonoid A
t : Set A
γ : Type u_3
inst✝ : Monoid γ
f : M → γ
hf : IsMonoidHom f
s : Set M
hs : IsSubmonoid s
a b : γ
x✝¹ : a ∈ f '' s
x✝ : b ∈ f '' s
x : M
hx : x ∈ s ∧ f x = a
y : M
hy : y ∈ s ∧ f y = b
⊢ f (x * y) = a * b
[PROOFSTEP]
rw [hf.map_mul, hx.2, hy.2]
[GOAL]
M : Type u_1
inst✝² : Monoid M
s : Set M
A : Type u_2
inst✝¹ : AddMonoid A
t : Set A
γ : Type u_3
inst✝ : Monoid γ
f : M → γ
hf : IsMonoidHom f
⊢ IsSubmonoid (Set.range f)
[PROOFSTEP]
rw [← Set.image_univ]
[GOAL]
M : Type u_1
inst✝² : Monoid M
s : Set M
A : Type u_2
inst✝¹ : AddMonoid A
t : Set A
γ : Type u_3
inst✝ : Monoid γ
f : M → γ
hf : IsMonoidHom f
⊢ IsSubmonoid (f '' Set.univ)
[PROOFSTEP]
exact Univ.isSubmonoid.image hf
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
a : M
hs : IsSubmonoid s
h : a ∈ s
⊢ a ^ 0 ∈ s
[PROOFSTEP]
rw [pow_zero]
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
a : M
hs : IsSubmonoid s
h : a ∈ s
⊢ 1 ∈ s
[PROOFSTEP]
exact hs.one_mem
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
a : M
hs : IsSubmonoid s
h : a ∈ s
n : ℕ
⊢ a ^ (n + 1) ∈ s
[PROOFSTEP]
rw [pow_succ]
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
a : M
hs : IsSubmonoid s
h : a ∈ s
n : ℕ
⊢ a * a ^ n ∈ s
[PROOFSTEP]
exact hs.mul_mem h (IsSubmonoid.pow_mem hs h)
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
hs : IsSubmonoid s
a : M
l : List M
h : ∀ (x : M), x ∈ a :: l → x ∈ s
⊢ a ∈ s ∧ ∀ (x : M), x ∈ l → x ∈ s
[PROOFSTEP]
simpa using h
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
hs : IsSubmonoid s
a : M
l : List M
h : ∀ (x : M), x ∈ a :: l → x ∈ s
this : a * List.prod l ∈ s
⊢ List.prod (a :: l) ∈ s
[PROOFSTEP]
simpa
[GOAL]
M✝ : Type u_1
inst✝² : Monoid M✝
s✝ : Set M✝
A : Type u_2
inst✝¹ : AddMonoid A
t : Set A
M : Type u_3
inst✝ : CommMonoid M
s : Set M
hs : IsSubmonoid s
m : Multiset M
⊢ (∀ (a : M), a ∈ m → a ∈ s) → Multiset.prod m ∈ s
[PROOFSTEP]
refine' Quotient.inductionOn m fun l hl => _
[GOAL]
M✝ : Type u_1
inst✝² : Monoid M✝
s✝ : Set M✝
A : Type u_2
inst✝¹ : AddMonoid A
t : Set A
M : Type u_3
inst✝ : CommMonoid M
s : Set M
hs : IsSubmonoid s
m : Multiset M
l : List M
hl : ∀ (a : M), a ∈ Quotient.mk (List.isSetoid M) l → a ∈ s
⊢ Multiset.prod (Quotient.mk (List.isSetoid M) l) ∈ s
[PROOFSTEP]
rw [Multiset.quot_mk_to_coe, Multiset.coe_prod]
[GOAL]
M✝ : Type u_1
inst✝² : Monoid M✝
s✝ : Set M✝
A : Type u_2
inst✝¹ : AddMonoid A
t : Set A
M : Type u_3
inst✝ : CommMonoid M
s : Set M
hs : IsSubmonoid s
m : Multiset M
l : List M
hl : ∀ (a : M), a ∈ Quotient.mk (List.isSetoid M) l → a ∈ s
⊢ List.prod l ∈ s
[PROOFSTEP]
exact list_prod_mem hs hl
[GOAL]
M✝ : Type u_1
inst✝² : Monoid M✝
s✝ : Set M✝
A✝ : Type u_2
inst✝¹ : AddMonoid A✝
t : Set A✝
M : Type u_3
A : Type u_4
inst✝ : CommMonoid M
s : Set M
hs : IsSubmonoid s
f : A → M
m : Multiset A
hm : Multiset.Nodup m
x✝ : ∀ (b : A), b ∈ { val := m, nodup := hm } → f b ∈ s
⊢ ∀ (a : M), a ∈ Multiset.map (fun b => f b) { val := m, nodup := hm }.val → a ∈ s
[PROOFSTEP]
simpa
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t✝ : Set A
s t : Set M
ht : IsSubmonoid t
h : s ⊆ t
a : M
ha : a ∈ Closure s
⊢ a ∈ t
[PROOFSTEP]
induction ha
[GOAL]
case basic
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t✝ : Set A
s t : Set M
ht : IsSubmonoid t
h : s ⊆ t
a a✝¹ : M
a✝ : a✝¹ ∈ s
⊢ a✝¹ ∈ t
[PROOFSTEP]
simp [h _, *, IsSubmonoid.one_mem, IsSubmonoid.mul_mem]
[GOAL]
case one
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t✝ : Set A
s t : Set M
ht : IsSubmonoid t
h : s ⊆ t
a : M
⊢ 1 ∈ t
[PROOFSTEP]
simp [h _, *, IsSubmonoid.one_mem, IsSubmonoid.mul_mem]
[GOAL]
case mul
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t✝ : Set A
s t : Set M
ht : IsSubmonoid t
h : s ⊆ t
a a✝² b✝ : M
a✝¹ : InClosure s a✝²
a✝ : InClosure s b✝
a_ih✝¹ : a✝² ∈ t
a_ih✝ : b✝ ∈ t
⊢ a✝² * b✝ ∈ t
[PROOFSTEP]
simp [h _, *, IsSubmonoid.one_mem, IsSubmonoid.mul_mem]
[GOAL]
M : Type u_1
inst✝² : Monoid M
s✝ : Set M
A✝ : Type u_2
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_3
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
⊢ f '' Closure s ≤ Closure (f '' s)
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
M : Type u_1
inst✝² : Monoid M
s✝ : Set M
A✝ : Type u_2
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_3
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
x : M
hx : x ∈ Closure s
⊢ f x ∈ Closure (f '' s)
[PROOFSTEP]
induction' hx with z hz
[GOAL]
case intro.intro.basic
M : Type u_1
inst✝² : Monoid M
s✝ : Set M
A✝ : Type u_2
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_3
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
x z : M
hz : z ∈ s
⊢ f z ∈ Closure (f '' s)
[PROOFSTEP]
solve_by_elim [subset_closure, Set.mem_image_of_mem]
[GOAL]
case intro.intro.one
M : Type u_1
inst✝² : Monoid M
s✝ : Set M
A✝ : Type u_2
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_3
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
x : M
⊢ f 1 ∈ Closure (f '' s)
[PROOFSTEP]
rw [hf.map_one]
[GOAL]
case intro.intro.one
M : Type u_1
inst✝² : Monoid M
s✝ : Set M
A✝ : Type u_2
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_3
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
x : M
⊢ 1 ∈ Closure (f '' s)
[PROOFSTEP]
apply IsSubmonoid.one_mem (closure.isSubmonoid (f '' s))
[GOAL]
case intro.intro.mul
M : Type u_1
inst✝² : Monoid M
s✝ : Set M
A✝ : Type u_2
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_3
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
x a✝² b✝ : M
a✝¹ : InClosure s a✝²
a✝ : InClosure s b✝
a_ih✝¹ : f a✝² ∈ Closure (f '' s)
a_ih✝ : f b✝ ∈ Closure (f '' s)
⊢ f (a✝² * b✝) ∈ Closure (f '' s)
[PROOFSTEP]
rw [hf.map_mul]
[GOAL]
case intro.intro.mul
M : Type u_1
inst✝² : Monoid M
s✝ : Set M
A✝ : Type u_2
inst✝¹ : AddMonoid A✝
t : Set A✝
A : Type u_3
inst✝ : Monoid A
f : M → A
hf : IsMonoidHom f
s : Set M
x a✝² b✝ : M
a✝¹ : InClosure s a✝²
a✝ : InClosure s b✝
a_ih✝¹ : f a✝² ∈ Closure (f '' s)
a_ih✝ : f b✝ ∈ Closure (f '' s)
⊢ f a✝² * f b✝ ∈ Closure (f '' s)
[PROOFSTEP]
solve_by_elim [(closure.isSubmonoid _).mul_mem]
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a : M
h : a ∈ Closure s
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a
[PROOFSTEP]
induction h
[GOAL]
case basic
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a a✝¹ : M
a✝ : a✝¹ ∈ s
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a✝¹
case one
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a : M
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = 1
case mul
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a a✝² b✝ : M
a✝¹ : InClosure s a✝²
a✝ : InClosure s b✝
a_ih✝¹ : ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a✝²
a_ih✝ : ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = b✝
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a✝² * b✝
[PROOFSTEP]
case basic a ha => exists [a]; simp [ha]
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a✝ a : M
ha : a ∈ s
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a
[PROOFSTEP]
case basic a ha => exists [a]; simp [ha]
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a✝ a : M
ha : a ∈ s
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a
[PROOFSTEP]
exists [a]
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a✝ a : M
ha : a ∈ s
⊢ (∀ (x : M), x ∈ [a] → x ∈ s) ∧ List.prod [a] = a
[PROOFSTEP]
simp [ha]
[GOAL]
case one
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a : M
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = 1
case mul
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a a✝² b✝ : M
a✝¹ : InClosure s a✝²
a✝ : InClosure s b✝
a_ih✝¹ : ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a✝²
a_ih✝ : ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = b✝
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a✝² * b✝
[PROOFSTEP]
case one => exists []; simp
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a : M
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = 1
[PROOFSTEP]
case one => exists []; simp
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a : M
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = 1
[PROOFSTEP]
exists []
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a : M
⊢ (∀ (x : M), x ∈ [] → x ∈ s) ∧ List.prod [] = 1
[PROOFSTEP]
simp
[GOAL]
case mul
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a a✝² b✝ : M
a✝¹ : InClosure s a✝²
a✝ : InClosure s b✝
a_ih✝¹ : ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a✝²
a_ih✝ : ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = b✝
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a✝² * b✝
[PROOFSTEP]
case mul a b _ _ ha hb =>
  rcases ha with ⟨la, ha, eqa⟩
  rcases hb with ⟨lb, hb, eqb⟩
  exists la ++ lb
  simp [eqa.symm, eqb.symm, or_imp]
  exact fun a => ⟨ha a, hb a⟩
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a✝² a b : M
a✝¹ : InClosure s a
a✝ : InClosure s b
ha : ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a
hb : ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = b
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a * b
[PROOFSTEP]
case mul a b _ _ ha hb =>
  rcases ha with ⟨la, ha, eqa⟩
  rcases hb with ⟨lb, hb, eqb⟩
  exists la ++ lb
  simp [eqa.symm, eqb.symm, or_imp]
  exact fun a => ⟨ha a, hb a⟩
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a✝² a b : M
a✝¹ : InClosure s a
a✝ : InClosure s b
ha : ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a
hb : ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = b
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a * b
[PROOFSTEP]
rcases ha with ⟨la, ha, eqa⟩
[GOAL]
case intro.intro
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a✝² a b : M
a✝¹ : InClosure s a
a✝ : InClosure s b
hb : ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = b
la : List M
ha : ∀ (x : M), x ∈ la → x ∈ s
eqa : List.prod la = a
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a * b
[PROOFSTEP]
rcases hb with ⟨lb, hb, eqb⟩
[GOAL]
case intro.intro.intro.intro
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a✝² a b : M
a✝¹ : InClosure s a
a✝ : InClosure s b
la : List M
ha : ∀ (x : M), x ∈ la → x ∈ s
eqa : List.prod la = a
lb : List M
hb : ∀ (x : M), x ∈ lb → x ∈ s
eqb : List.prod lb = b
⊢ ∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a * b
[PROOFSTEP]
exists la ++ lb
[GOAL]
case intro.intro.intro.intro
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a✝² a b : M
a✝¹ : InClosure s a
a✝ : InClosure s b
la : List M
ha : ∀ (x : M), x ∈ la → x ∈ s
eqa : List.prod la = a
lb : List M
hb : ∀ (x : M), x ∈ lb → x ∈ s
eqb : List.prod lb = b
⊢ (∀ (x : M), x ∈ la ++ lb → x ∈ s) ∧ List.prod (la ++ lb) = a * b
[PROOFSTEP]
simp [eqa.symm, eqb.symm, or_imp]
[GOAL]
case intro.intro.intro.intro
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
s : Set M
a✝² a b : M
a✝¹ : InClosure s a
a✝ : InClosure s b
la : List M
ha : ∀ (x : M), x ∈ la → x ∈ s
eqa : List.prod la = a
lb : List M
hb : ∀ (x : M), x ∈ lb → x ∈ s
eqb : List.prod lb = b
⊢ ∀ (x : M), (x ∈ la → x ∈ s) ∧ (x ∈ lb → x ∈ s)
[PROOFSTEP]
exact fun a => ⟨ha a, hb a⟩
[GOAL]
M✝ : Type u_1
inst✝² : Monoid M✝
s✝ : Set M✝
A : Type u_2
inst✝¹ : AddMonoid A
t✝ : Set A
M : Type u_3
inst✝ : CommMonoid M
s t : Set M
x : M
hx : x ∈ Closure (s ∪ t)
L : List M
HL1✝ : ∀ (x : M), x ∈ L → x ∈ s ∪ t
HL2 : List.prod L = x
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → x ∈ s ∪ t) → ∃ y, y ∈ Closure s ∧ ∃ z, z ∈ Closure t ∧ y * z = List.prod tl
HL1 : ∀ (x : M), x ∈ hd :: tl → x ∈ s ∪ t
y : M
hy : y ∈ Closure s
z : M
hz : z ∈ Closure t
hyzx : y * z = List.prod tl
hs : hd ∈ s
⊢ hd * y * z = List.prod (hd :: tl)
[PROOFSTEP]
rw [mul_assoc, List.prod_cons, ← hyzx]
[GOAL]
M✝ : Type u_1
inst✝² : Monoid M✝
s✝ : Set M✝
A : Type u_2
inst✝¹ : AddMonoid A
t✝ : Set A
M : Type u_3
inst✝ : CommMonoid M
s t : Set M
x : M
hx : x ∈ Closure (s ∪ t)
L : List M
HL1✝ : ∀ (x : M), x ∈ L → x ∈ s ∪ t
HL2 : List.prod L = x
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → x ∈ s ∪ t) → ∃ y, y ∈ Closure s ∧ ∃ z, z ∈ Closure t ∧ y * z = List.prod tl
HL1 : ∀ (x : M), x ∈ hd :: tl → x ∈ s ∪ t
y : M
hy : y ∈ Closure s
z : M
hz : z ∈ Closure t
hyzx : y * z = List.prod tl
ht : hd ∈ t
⊢ y * (z * hd) = List.prod (hd :: tl)
[PROOFSTEP]
rw [← mul_assoc, List.prod_cons, ← hyzx, mul_comm hd]
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type u_2
inst✝ : AddMonoid A
t : Set A
S : Submonoid M
⊢ IsSubmonoid ↑S
[PROOFSTEP]
refine' ⟨S.2, S.1.2⟩
