[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
l : List M
hl : ∀ (x : M), x ∈ l → x ∈ S
⊢ List.prod l ∈ S
[PROOFSTEP]
lift l to List S using hl
[GOAL]
case intro
M : Type u_1
A : Type u_2
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
l : List { x // x ∈ S }
⊢ List.prod (List.map Subtype.val l) ∈ S
[PROOFSTEP]
rw [← coe_list_prod]
[GOAL]
case intro
M : Type u_1
A : Type u_2
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
l : List { x // x ∈ S }
⊢ ↑(List.prod l) ∈ S
[PROOFSTEP]
exact l.prod.coe_prop
[GOAL]
M✝ : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : Monoid M✝
inst✝⁴ : SetLike B M✝
inst✝³ : SubmonoidClass B M✝
S : B
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
m : Multiset M
hm : ∀ (a : M), a ∈ m → a ∈ S
⊢ Multiset.prod m ∈ S
[PROOFSTEP]
lift m to Multiset S using hm
[GOAL]
case intro
M✝ : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : Monoid M✝
inst✝⁴ : SetLike B M✝
inst✝³ : SubmonoidClass B M✝
S : B
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
m : Multiset { x // x ∈ S }
⊢ Multiset.prod (Multiset.map Subtype.val m) ∈ S
[PROOFSTEP]
rw [← coe_multiset_prod]
[GOAL]
case intro
M✝ : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : Monoid M✝
inst✝⁴ : SetLike B M✝
inst✝³ : SubmonoidClass B M✝
S : B
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
m : Multiset { x // x ∈ S }
⊢ ↑(Multiset.prod m) ∈ S
[PROOFSTEP]
exact m.prod.coe_prop
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
s : Submonoid M
l : List M
hl : ∀ (x : M), x ∈ l → x ∈ s
⊢ List.prod l ∈ s
[PROOFSTEP]
lift l to List s using hl
[GOAL]
case intro
M : Type u_1
A : Type u_2
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
s : Submonoid M
l : List { x // x ∈ s }
⊢ List.prod (List.map Subtype.val l) ∈ s
[PROOFSTEP]
rw [← coe_list_prod]
[GOAL]
case intro
M : Type u_1
A : Type u_2
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
s : Submonoid M
l : List { x // x ∈ s }
⊢ ↑(List.prod l) ∈ s
[PROOFSTEP]
exact l.prod.coe_prop
[GOAL]
M✝ : Type u_1
A : Type u_2
B : Type u_3
inst✝³ : Monoid M✝
inst✝² : SetLike B M✝
inst✝¹ : SubmonoidClass B M✝
S✝ : B
s : Submonoid M✝
M : Type u_4
inst✝ : CommMonoid M
S : Submonoid M
m : Multiset M
hm : ∀ (a : M), a ∈ m → a ∈ S
⊢ Multiset.prod m ∈ S
[PROOFSTEP]
lift m to Multiset S using hm
[GOAL]
case intro
M✝ : Type u_1
A : Type u_2
B : Type u_3
inst✝³ : Monoid M✝
inst✝² : SetLike B M✝
inst✝¹ : SubmonoidClass B M✝
S✝ : B
s : Submonoid M✝
M : Type u_4
inst✝ : CommMonoid M
S : Submonoid M
m : Multiset { x // x ∈ S }
⊢ Multiset.prod (Multiset.map Subtype.val m) ∈ S
[PROOFSTEP]
rw [← coe_multiset_prod]
[GOAL]
case intro
M✝ : Type u_1
A : Type u_2
B : Type u_3
inst✝³ : Monoid M✝
inst✝² : SetLike B M✝
inst✝¹ : SubmonoidClass B M✝
S✝ : B
s : Submonoid M✝
M : Type u_4
inst✝ : CommMonoid M
S : Submonoid M
m : Multiset { x // x ∈ S }
⊢ ↑(Multiset.prod m) ∈ S
[PROOFSTEP]
exact m.prod.coe_prop
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S✝ : B
s S : Submonoid M
m : Multiset M
comm : Set.Pairwise {x | x ∈ m} Commute
h : ∀ (x : M), x ∈ m → x ∈ S
⊢ Multiset.noncommProd m comm ∈ S
[PROOFSTEP]
induction' m using Quotient.inductionOn with l
[GOAL]
case h
M : Type u_1
A : Type u_2
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S✝ : B
s S : Submonoid M
m : Multiset M
comm✝ : Set.Pairwise {x | x ∈ m} Commute
h✝ : ∀ (x : M), x ∈ m → x ∈ S
l : List M
comm : Set.Pairwise {x | x ∈ Quotient.mk (List.isSetoid M) l} Commute
h : ∀ (x : M), x ∈ Quotient.mk (List.isSetoid M) l → x ∈ S
⊢ Multiset.noncommProd (Quotient.mk (List.isSetoid M) l) comm ∈ S
[PROOFSTEP]
simp only [Multiset.quot_mk_to_coe, Multiset.noncommProd_coe]
[GOAL]
case h
M : Type u_1
A : Type u_2
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S✝ : B
s S : Submonoid M
m : Multiset M
comm✝ : Set.Pairwise {x | x ∈ m} Commute
h✝ : ∀ (x : M), x ∈ m → x ∈ S
l : List M
comm : Set.Pairwise {x | x ∈ Quotient.mk (List.isSetoid M) l} Commute
h : ∀ (x : M), x ∈ Quotient.mk (List.isSetoid M) l → x ∈ S
⊢ List.prod l ∈ S
[PROOFSTEP]
exact Submonoid.list_prod_mem _ h
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S✝ : B
s S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : Set.Pairwise ↑t fun a b => Commute (f a) (f b)
h : ∀ (c : ι), c ∈ t → f c ∈ S
⊢ Finset.noncommProd t f comm ∈ S
[PROOFSTEP]
apply multiset_noncommProd_mem
[GOAL]
case h
M : Type u_1
A : Type u_2
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S✝ : B
s S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : Set.Pairwise ↑t fun a b => Commute (f a) (f b)
h : ∀ (c : ι), c ∈ t → f c ∈ S
⊢ ∀ (x : M), x ∈ Multiset.map f t.val → x ∈ S
[PROOFSTEP]
intro y
[GOAL]
case h
M : Type u_1
A : Type u_2
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S✝ : B
s S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : Set.Pairwise ↑t fun a b => Commute (f a) (f b)
h : ∀ (c : ι), c ∈ t → f c ∈ S
y : M
⊢ y ∈ Multiset.map f t.val → y ∈ S
[PROOFSTEP]
rw [Multiset.mem_map]
[GOAL]
case h
M : Type u_1
A : Type u_2
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S✝ : B
s S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : Set.Pairwise ↑t fun a b => Commute (f a) (f b)
h : ∀ (c : ι), c ∈ t → f c ∈ S
y : M
⊢ (∃ a, a ∈ t.val ∧ f a = y) → y ∈ S
[PROOFSTEP]
rintro ⟨x, ⟨hx, rfl⟩⟩
[GOAL]
case h.intro.intro
M : Type u_1
A : Type u_2
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S✝ : B
s S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : Set.Pairwise ↑t fun a b => Commute (f a) (f b)
h : ∀ (c : ι), c ∈ t → f c ∈ S
x : ι
hx : x ∈ t.val
⊢ f x ∈ S
[PROOFSTEP]
exact h x hx
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
ι : Sort u_4
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ ⨆ (i : ι), S i ↔ ∃ i, x ∈ S i
[PROOFSTEP]
refine' ⟨_, fun ⟨i, hi⟩ => (SetLike.le_def.1 <| le_iSup S i) hi⟩
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
ι : Sort u_4
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ ⨆ (i : ι), S i → ∃ i, x ∈ S i
[PROOFSTEP]
suffices x ∈ closure (⋃ i, (S i : Set M)) → ∃ i, x ∈ S i by simpa only [closure_iUnion, closure_eq (S _)] using this
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
ι : Sort u_4
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
this : x ∈ closure (⋃ (i : ι), ↑(S i)) → ∃ i, x ∈ S i
⊢ x ∈ ⨆ (i : ι), S i → ∃ i, x ∈ S i
[PROOFSTEP]
simpa only [closure_iUnion, closure_eq (S _)] using this
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
ι : Sort u_4
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ closure (⋃ (i : ι), ↑(S i)) → ∃ i, x ∈ S i
[PROOFSTEP]
refine' fun hx => closure_induction hx (fun _ => mem_iUnion.1) _ _
[GOAL]
case refine'_1
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
ι : Sort u_4
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
⊢ ∃ i, 1 ∈ S i
[PROOFSTEP]
exact hι.elim fun i => ⟨i, (S i).one_mem⟩
[GOAL]
case refine'_2
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
ι : Sort u_4
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
⊢ ∀ (x y : M), (∃ i, x ∈ S i) → (∃ i, y ∈ S i) → ∃ i, x * y ∈ S i
[PROOFSTEP]
rintro x y ⟨i, hi⟩ ⟨j, hj⟩
[GOAL]
case refine'_2.intro.intro
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
ι : Sort u_4
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x x_1 => x ≤ x_1) S
x✝ : M
hx : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
x y : M
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
⊢ ∃ i, x * y ∈ S i
[PROOFSTEP]
rcases hS i j with ⟨k, hki, hkj⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
ι : Sort u_4
hι : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x x_1 => x ≤ x_1) S
x✝ : M
hx : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
x y : M
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
k : ι
hki : S i ≤ S k
hkj : S j ≤ S k
⊢ ∃ i, x * y ∈ S i
[PROOFSTEP]
exact ⟨k, (S k).mul_mem (hki hi) (hkj hj)⟩
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ ↑(⨆ (i : ι), S i) ↔ x ∈ ⋃ (i : ι), ↑(S i)
[PROOFSTEP]
simp [mem_iSup_of_directed hS]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
S : Set (Submonoid M)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
[PROOFSTEP]
haveI : Nonempty S := Sne.to_subtype
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
S : Set (Submonoid M)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : M
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
[PROOFSTEP]
simp [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists, Subtype.coe_mk]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
S : Set (Submonoid M)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ ↑(sSup S) ↔ x ∈ ⋃ (s : Submonoid M) (_ : s ∈ S), ↑s
[PROOFSTEP]
simp [mem_sSup_of_directedOn Sne hS]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
S T : Submonoid M
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T
[PROOFSTEP]
rw [← SetLike.le_def]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
S T : Submonoid M
⊢ S ≤ S ⊔ T
[PROOFSTEP]
exact le_sup_left
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
S T : Submonoid M
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T
[PROOFSTEP]
rw [← SetLike.le_def]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
S T : Submonoid M
⊢ T ≤ S ⊔ T
[PROOFSTEP]
exact le_sup_right
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
i : ι
⊢ ∀ {x : M}, x ∈ S i → x ∈ iSup S
[PROOFSTEP]
rw [← SetLike.le_def]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
i : ι
⊢ S i ≤ iSup S
[PROOFSTEP]
exact le_iSup _ _
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
S : Set (Submonoid M)
s : Submonoid M
hs : s ∈ S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S
[PROOFSTEP]
rw [← SetLike.le_def]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
S : Set (Submonoid M)
s : Submonoid M
hs : s ∈ S
⊢ s ≤ sSup S
[PROOFSTEP]
exact le_sSup hs
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : M → Prop
x : M
hx : x ∈ ⨆ (i : ι), S i
hp : ∀ (i : ι) (x : M), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : M), C x → C y → C (x * y)
⊢ C x
[PROOFSTEP]
rw [iSup_eq_closure] at hx 
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : M → Prop
x : M
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : M), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : M), C x → C y → C (x * y)
⊢ C x
[PROOFSTEP]
refine closure_induction hx (fun x hx => ?_) h1 hmul
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : M → Prop
x✝ : M
hx✝ : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : M), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : M), C x → C y → C (x * y)
x : M
hx : x ∈ ⋃ (i : ι), ↑(S i)
⊢ C x
[PROOFSTEP]
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
[GOAL]
case intro
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : M → Prop
x✝ : M
hx✝ : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : M), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : M), C x → C y → C (x * y)
x : M
hx : x ∈ ⋃ (i : ι), ↑(S i)
i : ι
hi : x ∈ ↑(S i)
⊢ C x
[PROOFSTEP]
exact hp _ _ hi
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : (x : M) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x : M
hx : x ∈ ⨆ (i : ι), S i
⊢ C x hx
[PROOFSTEP]
refine' Exists.elim (_ : ∃ Hx, C x Hx) fun (hx : x ∈ ⨆ i, S i) (hc : C x hx) => hc
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : (x : M) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x : M
hx : x ∈ ⨆ (i : ι), S i
⊢ ∃ Hx, C x Hx
[PROOFSTEP]
refine' @iSup_induction _ _ ι S (fun m => ∃ hm, C m hm) _ hx (fun i x hx => _) _ fun x y => _
[GOAL]
case refine'_1
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : (x : M) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x✝ : M
hx✝ : x✝ ∈ ⨆ (i : ι), S i
i : ι
x : M
hx : x ∈ S i
⊢ (fun m => ∃ hm, C m hm) x
[PROOFSTEP]
exact ⟨_, hp _ _ hx⟩
[GOAL]
case refine'_2
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : (x : M) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x : M
hx : x ∈ ⨆ (i : ι), S i
⊢ (fun m => ∃ hm, C m hm) 1
[PROOFSTEP]
exact ⟨_, h1⟩
[GOAL]
case refine'_3
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : (x : M) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x✝ : M
hx : x✝ ∈ ⨆ (i : ι), S i
x y : M
⊢ (fun m => ∃ hm, C m hm) x → (fun m => ∃ hm, C m hm) y → (fun m => ∃ hm, C m hm) (x * y)
[PROOFSTEP]
rintro ⟨_, Cx⟩ ⟨_, Cy⟩
[GOAL]
case refine'_3.intro.intro
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
C : (x : M) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x✝ : M
hx : x✝ ∈ ⨆ (i : ι), S i
x y : M
w✝¹ : x ∈ ⨆ (i : ι), S i
Cx : C x w✝¹
w✝ : y ∈ ⨆ (i : ι), S i
Cy : C y w✝
⊢ ∃ hm, C (x * y) hm
[PROOFSTEP]
refine' ⟨_, hmul _ _ _ _ Cx Cy⟩
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
x y : M
⊢ y ∈ closure {x} ↔ ∃ n, x ^ n = y
[PROOFSTEP]
rw [closure_singleton_eq, mem_mrange]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
x y : M
⊢ (∃ x_1, ↑(↑(powersHom M) x) x_1 = y) ↔ ∃ n, x ^ n = y
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
⊢ closure {1} = ⊥
[PROOFSTEP]
simp [eq_bot_iff_forall, mem_closure_singleton]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
α : Type u_4
f : α → M
⊢ mrange (↑FreeMonoid.lift f) = closure (Set.range f)
[PROOFSTEP]
rw [mrange_eq_map, ← FreeMonoid.closure_range_of, map_mclosure, ← Set.range_comp, FreeMonoid.lift_comp_of]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
s : Set M
⊢ closure s = mrange (↑FreeMonoid.lift Subtype.val)
[PROOFSTEP]
rw [FreeMonoid.mrange_lift, Subtype.range_coe]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
s : Set M
⊢ ↑(closure s) = List.prod '' {l | ∀ (x : M), x ∈ l → x ∈ s}
[PROOFSTEP]
rw [closure_eq_mrange, coe_mrange, ← Set.range_list_map_coe, ← Set.range_comp]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
s : Set M
⊢ Set.range ↑(↑FreeMonoid.lift Subtype.val) = Set.range (List.prod ∘ List.map Subtype.val)
[PROOFSTEP]
exact congrArg _ (funext <| FreeMonoid.lift_apply _)
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
s : Set M
x : M
hx : x ∈ closure s
⊢ ∃ l x_1, List.prod l = x
[PROOFSTEP]
rwa [← SetLike.mem_coe, closure_eq_image_prod, Set.mem_image_iff_bex] at hx 
[GOAL]
M✝ : Type u_1
A : Type u_2
B : Type u_3
inst✝¹ : Monoid M✝
M : Type u_4
inst✝ : CommMonoid M
s : Set M
x : M
hx : x ∈ closure s
⊢ ∃ l x_1, Multiset.prod l = x
[PROOFSTEP]
obtain ⟨l, h1, h2⟩ := exists_list_of_mem_closure hx
[GOAL]
case intro.intro
M✝ : Type u_1
A : Type u_2
B : Type u_3
inst✝¹ : Monoid M✝
M : Type u_4
inst✝ : CommMonoid M
s : Set M
x : M
hx : x ∈ closure s
l : List M
h1 : ∀ (y : M), y ∈ l → y ∈ s
h2 : List.prod l = x
⊢ ∃ l x_1, Multiset.prod l = x
[PROOFSTEP]
exact ⟨l, h1, (Multiset.coe_prod l).trans h2⟩
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
s : Set M
p : M → Prop
x : M
h : x ∈ closure s
H1 : p 1
Hmul : ∀ (x : M), x ∈ s → ∀ (y : M), p y → p (x * y)
⊢ p x
[PROOFSTEP]
rw [closure_eq_mrange] at h 
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
s : Set M
p : M → Prop
x : M
h : x ∈ mrange (↑FreeMonoid.lift Subtype.val)
H1 : p 1
Hmul : ∀ (x : M), x ∈ s → ∀ (y : M), p y → p (x * y)
⊢ p x
[PROOFSTEP]
obtain ⟨l, rfl⟩ := h
[GOAL]
case intro
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
s : Set M
p : M → Prop
H1 : p 1
Hmul : ∀ (x : M), x ∈ s → ∀ (y : M), p y → p (x * y)
l : FreeMonoid { x // x ∈ s }
⊢ p (↑(↑FreeMonoid.lift Subtype.val) l)
[PROOFSTEP]
induction' l using FreeMonoid.recOn with x y ih
[GOAL]
case intro.h0
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
s : Set M
p : M → Prop
H1 : p 1
Hmul : ∀ (x : M), x ∈ s → ∀ (y : M), p y → p (x * y)
⊢ p (↑(↑FreeMonoid.lift Subtype.val) 1)
[PROOFSTEP]
exact H1
[GOAL]
case intro.ih
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
s : Set M
p : M → Prop
H1 : p 1
Hmul : ∀ (x : M), x ∈ s → ∀ (y : M), p y → p (x * y)
x : { x // x ∈ s }
y : FreeMonoid { x // x ∈ s }
ih : p (↑(↑FreeMonoid.lift Subtype.val) y)
⊢ p (↑(↑FreeMonoid.lift Subtype.val) (FreeMonoid.of x * y))
[PROOFSTEP]
simpa only [map_mul, FreeMonoid.lift_eval_of] using Hmul _ x.prop _ ih
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
s : Set M
p : M → Prop
hs : closure s = ⊤
x : M
H1 : p 1
Hmul : ∀ (x : M), x ∈ s → ∀ (y : M), p y → p (x * y)
⊢ x ∈ closure s
[PROOFSTEP]
rw [hs]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
s : Set M
p : M → Prop
hs : closure s = ⊤
x : M
H1 : p 1
Hmul : ∀ (x : M), x ∈ s → ∀ (y : M), p y → p (x * y)
⊢ x ∈ ⊤
[PROOFSTEP]
exact mem_top _
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
s : Set M
p : M → Prop
hs : closure s = ⊤
x : M
H1 : p 1
Hmul : ∀ (x y : M), y ∈ s → p x → p (x * y)
⊢ x ∈ closure s
[PROOFSTEP]
rw [hs]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
s : Set M
p : M → Prop
hs : closure s = ⊤
x : M
H1 : p 1
Hmul : ∀ (x y : M), y ∈ s → p x → p (x * y)
⊢ x ∈ ⊤
[PROOFSTEP]
exact mem_top _
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
n✝ n : M
i : ℕ
⊢ (fun x x_1 => x ^ x_1) n✝ i = n ↔ ↑(↑(powersHom M) n✝) i = n
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
n✝ n : M
i : ℕ
⊢ n✝ ^ i = n ↔ n✝ ^ ↑Multiplicative.toAdd i = n
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
n : M
⊢ powers n = closure {n}
[PROOFSTEP]
ext
[GOAL]
case h
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
n x✝ : M
⊢ x✝ ∈ powers n ↔ x✝ ∈ closure {n}
[PROOFSTEP]
exact mem_closure_singleton.symm
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝¹ : Monoid M
inst✝ : DecidableEq M
n : M
h : Function.Injective fun m => n ^ m
x✝¹ x✝ : Multiplicative ℕ
⊢ Equiv.toFun
      { toFun := fun m => pow n (↑Multiplicative.toAdd m), invFun := fun m => ↑Multiplicative.ofAdd (log m),
        left_inv := (_ : ∀ (m : ℕ), log (pow n m) = m),
        right_inv := (_ : ∀ (p : { x // x ∈ powers n }), pow n (log p) = p) }
      (x✝¹ * x✝) =
    Equiv.toFun
        { toFun := fun m => pow n (↑Multiplicative.toAdd m), invFun := fun m => ↑Multiplicative.ofAdd (log m),
          left_inv := (_ : ∀ (m : ℕ), log (pow n m) = m),
          right_inv := (_ : ∀ (p : { x // x ∈ powers n }), pow n (log p) = p) }
        x✝¹ *
      Equiv.toFun
        { toFun := fun m => pow n (↑Multiplicative.toAdd m), invFun := fun m => ↑Multiplicative.ofAdd (log m),
          left_inv := (_ : ∀ (m : ℕ), log (pow n m) = m),
          right_inv := (_ : ∀ (p : { x // x ∈ powers n }), pow n (log p) = p) }
        x✝
[PROOFSTEP]
simp only [pow, map_mul, ofAdd_add, toAdd_mul]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝² : Monoid M
N : Type u_4
F : Type u_5
inst✝¹ : Monoid N
inst✝ : MonoidHomClass F M N
f : F
m : M
⊢ map f (powers m) = powers (↑f m)
[PROOFSTEP]
simp only [powers_eq_closure, map_mclosure f, Set.image_singleton]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
s : Set M
hcomm : ∀ (a : M), a ∈ s → ∀ (b : M), b ∈ s → a * b = b * a
src✝ : Monoid { x // x ∈ closure s } := toMonoid (closure s)
x y : { x // x ∈ closure s }
⊢ x * y = y * x
[PROOFSTEP]
ext
[GOAL]
case a
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
s : Set M
hcomm : ∀ (a : M), a ∈ s → ∀ (b : M), b ∈ s → a * b = b * a
src✝ : Monoid { x // x ∈ closure s } := toMonoid (closure s)
x y : { x // x ∈ closure s }
⊢ ↑(x * y) = ↑(y * x)
[PROOFSTEP]
simp only [Submonoid.coe_mul]
[GOAL]
case a
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
s : Set M
hcomm : ∀ (a : M), a ∈ s → ∀ (b : M), b ∈ s → a * b = b * a
src✝ : Monoid { x // x ∈ closure s } := toMonoid (closure s)
x y : { x // x ∈ closure s }
⊢ ↑x * ↑y = ↑y * ↑x
[PROOFSTEP]
exact
  closure_induction₂ x.prop y.prop hcomm Commute.one_left Commute.one_right (fun x y z => Commute.mul_left) fun x y z =>
    Commute.mul_right
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), (x • y) • z = x • y • z
⊢ IsScalarTower M N α
[PROOFSTEP]
refine' ⟨fun x => Submonoid.induction_of_closure_eq_top_left htop x _ _⟩
[GOAL]
case refine'_1
M : Type u_1
A : Type u_2
B : Type u_3
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), (x • y) • z = x • y • z
x : M
⊢ ∀ (y : N) (z : α), (1 • y) • z = 1 • y • z
[PROOFSTEP]
intro y z
[GOAL]
case refine'_1
M : Type u_1
A : Type u_2
B : Type u_3
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), (x • y) • z = x • y • z
x : M
y : N
z : α
⊢ (1 • y) • z = 1 • y • z
[PROOFSTEP]
rw [one_smul, one_smul]
[GOAL]
case refine'_2
M : Type u_1
A : Type u_2
B : Type u_3
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), (x • y) • z = x • y • z
x : M
⊢ ∀ (x : M),
    x ∈ s →
      ∀ (y : M),
        (∀ (y_1 : N) (z : α), (y • y_1) • z = y • y_1 • z) →
          ∀ (y_1 : N) (z : α), ((x * y) • y_1) • z = (x * y) • y_1 • z
[PROOFSTEP]
clear x
[GOAL]
case refine'_2
M : Type u_1
A : Type u_2
B : Type u_3
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), (x • y) • z = x • y • z
⊢ ∀ (x : M),
    x ∈ s →
      ∀ (y : M),
        (∀ (y_1 : N) (z : α), (y • y_1) • z = y • y_1 • z) →
          ∀ (y_1 : N) (z : α), ((x * y) • y_1) • z = (x * y) • y_1 • z
[PROOFSTEP]
intro x hx x' hx' y z
[GOAL]
case refine'_2
M : Type u_1
A : Type u_2
B : Type u_3
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), (x • y) • z = x • y • z
x : M
hx : x ∈ s
x' : M
hx' : ∀ (y : N) (z : α), (x' • y) • z = x' • y • z
y : N
z : α
⊢ ((x * x') • y) • z = (x * x') • y • z
[PROOFSTEP]
rw [mul_smul, mul_smul, hs x hx, hx']
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), x • y • z = y • x • z
⊢ SMulCommClass M N α
[PROOFSTEP]
refine' ⟨fun x => Submonoid.induction_of_closure_eq_top_left htop x _ _⟩
[GOAL]
case refine'_1
M : Type u_1
A : Type u_2
B : Type u_3
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
⊢ ∀ (n : N) (a : α), 1 • n • a = n • 1 • a
[PROOFSTEP]
intro y z
[GOAL]
case refine'_1
M : Type u_1
A : Type u_2
B : Type u_3
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
y : N
z : α
⊢ 1 • y • z = y • 1 • z
[PROOFSTEP]
rw [one_smul, one_smul]
[GOAL]
case refine'_2
M : Type u_1
A : Type u_2
B : Type u_3
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
⊢ ∀ (x : M),
    x ∈ s → ∀ (y : M), (∀ (n : N) (a : α), y • n • a = n • y • a) → ∀ (n : N) (a : α), (x * y) • n • a = n • (x * y) • a
[PROOFSTEP]
clear x
[GOAL]
case refine'_2
M : Type u_1
A : Type u_2
B : Type u_3
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), x • y • z = y • x • z
⊢ ∀ (x : M),
    x ∈ s → ∀ (y : M), (∀ (n : N) (a : α), y • n • a = n • y • a) → ∀ (n : N) (a : α), (x * y) • n • a = n • (x * y) • a
[PROOFSTEP]
intro x hx x' hx' y z
[GOAL]
case refine'_2
M : Type u_1
A : Type u_2
B : Type u_3
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
hx : x ∈ s
x' : M
hx' : ∀ (n : N) (a : α), x' • n • a = n • x' • a
y : N
z : α
⊢ (x * x') • y • z = y • (x * x') • z
[PROOFSTEP]
rw [mul_smul, mul_smul, hx', hs x hx]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
N : Type u_4
inst✝ : CommMonoid N
s t : Submonoid N
⊢ s ⊔ t = mrange (coprod (subtype s) (subtype t))
[PROOFSTEP]
rw [mrange_eq_map, ← mrange_inl_sup_mrange_inr, map_sup, map_mrange, coprod_comp_inl, map_mrange, coprod_comp_inr,
  range_subtype, range_subtype]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
N : Type u_4
inst✝ : CommMonoid N
s t : Submonoid N
x : N
⊢ x ∈ s ⊔ t ↔ ∃ y, y ∈ s ∧ ∃ z, z ∈ t ∧ y * z = x
[PROOFSTEP]
simp only [ge_iff_le, sup_eq_range, mem_mrange, coprod_apply, coe_subtype, Prod.exists, Subtype.exists, exists_prop]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : AddMonoid A
x y : A
⊢ y ∈ closure {x} ↔ ∃ n, n • x = y
[PROOFSTEP]
rw [closure_singleton_eq, AddMonoidHom.mem_mrange]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : AddMonoid A
x y : A
⊢ (∃ x_1, ↑(↑(multiplesHom A) x) x_1 = y) ↔ ∃ n, n • x = y
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : AddMonoid A
⊢ closure {0} = ⊥
[PROOFSTEP]
simp [eq_bot_iff_forall, mem_closure_singleton, nsmul_zero]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : AddMonoid A
x n : A
i : ℕ
⊢ (fun i => i • x) i = n ↔ ↑(↑(multiplesHom A) x) i = n
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
R : Type u_4
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a b : R
ha : a ∈ AddSubmonoid.closure ↑S
hb : b ∈ S
⊢ a * b ∈ AddSubmonoid.closure ↑S
[PROOFSTEP]
revert b
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
R : Type u_4
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a : R
ha : a ∈ AddSubmonoid.closure ↑S
⊢ ∀ {b : R}, b ∈ S → a * b ∈ AddSubmonoid.closure ↑S
[PROOFSTEP]
refine' @AddSubmonoid.closure_induction _ _ _ (fun z => ∀ (b : R), b ∈ S → z * b ∈ AddSubmonoid.closure S) _ ha _ _ _
[GOAL]
case refine'_1
M : Type u_1
A : Type u_2
B : Type u_3
R : Type u_4
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a : R
ha : a ∈ AddSubmonoid.closure ↑S
⊢ ∀ (x : R), x ∈ ↑S → (fun z => ∀ (b : R), b ∈ S → z * b ∈ AddSubmonoid.closure ↑S) x
[PROOFSTEP]
clear ha a
[GOAL]
case refine'_2
M : Type u_1
A : Type u_2
B : Type u_3
R : Type u_4
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a : R
ha : a ∈ AddSubmonoid.closure ↑S
⊢ (fun z => ∀ (b : R), b ∈ S → z * b ∈ AddSubmonoid.closure ↑S) 0
[PROOFSTEP]
clear ha a
[GOAL]
case refine'_3
M : Type u_1
A : Type u_2
B : Type u_3
R : Type u_4
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a : R
ha : a ∈ AddSubmonoid.closure ↑S
⊢ ∀ (x y : R),
    (fun z => ∀ (b : R), b ∈ S → z * b ∈ AddSubmonoid.closure ↑S) x →
      (fun z => ∀ (b : R), b ∈ S → z * b ∈ AddSubmonoid.closure ↑S) y →
        (fun z => ∀ (b : R), b ∈ S → z * b ∈ AddSubmonoid.closure ↑S) (x + y)
[PROOFSTEP]
clear ha a
[GOAL]
case refine'_1
M : Type u_1
A : Type u_2
B : Type u_3
R : Type u_4
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
⊢ ∀ (x : R), x ∈ ↑S → (fun z => ∀ (b : R), b ∈ S → z * b ∈ AddSubmonoid.closure ↑S) x
[PROOFSTEP]
exact fun r hr b hb => AddSubmonoid.mem_closure.mpr fun y hy => hy (mul_mem hr hb)
[GOAL]
case refine'_2
M : Type u_1
A : Type u_2
B : Type u_3
R : Type u_4
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
⊢ (fun z => ∀ (b : R), b ∈ S → z * b ∈ AddSubmonoid.closure ↑S) 0
[PROOFSTEP]
exact fun b _ => by simp only [zero_mul, (AddSubmonoid.closure (S : Set R)).zero_mem]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
R : Type u_4
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
b : R
x✝ : b ∈ S
⊢ 0 * b ∈ AddSubmonoid.closure ↑S
[PROOFSTEP]
simp only [zero_mul, (AddSubmonoid.closure (S : Set R)).zero_mem]
[GOAL]
case refine'_3
M : Type u_1
A : Type u_2
B : Type u_3
R : Type u_4
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
⊢ ∀ (x y : R),
    (fun z => ∀ (b : R), b ∈ S → z * b ∈ AddSubmonoid.closure ↑S) x →
      (fun z => ∀ (b : R), b ∈ S → z * b ∈ AddSubmonoid.closure ↑S) y →
        (fun z => ∀ (b : R), b ∈ S → z * b ∈ AddSubmonoid.closure ↑S) (x + y)
[PROOFSTEP]
simp_rw [add_mul]
[GOAL]
case refine'_3
M : Type u_1
A : Type u_2
B : Type u_3
R : Type u_4
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
⊢ ∀ (x y : R),
    (∀ (b : R), b ∈ S → x * b ∈ AddSubmonoid.closure ↑S) →
      (∀ (b : R), b ∈ S → y * b ∈ AddSubmonoid.closure ↑S) → ∀ (b : R), b ∈ S → x * b + y * b ∈ AddSubmonoid.closure ↑S
[PROOFSTEP]
exact fun r s hr hs b hb => (AddSubmonoid.closure (S : Set R)).add_mem (hr _ hb) (hs _ hb)
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
R : Type u_4
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a b : R
ha : a ∈ AddSubmonoid.closure ↑S
hb : b ∈ AddSubmonoid.closure ↑S
⊢ a * b ∈ AddSubmonoid.closure ↑S
[PROOFSTEP]
revert a
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
R : Type u_4
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
b : R
hb : b ∈ AddSubmonoid.closure ↑S
⊢ ∀ {a : R}, a ∈ AddSubmonoid.closure ↑S → a * b ∈ AddSubmonoid.closure ↑S
[PROOFSTEP]
refine'
  @AddSubmonoid.closure_induction _ _ _
    (fun z => ∀ {a : R}, a ∈ AddSubmonoid.closure ↑S → a * z ∈ AddSubmonoid.closure ↑S) _ hb _ _ _
[GOAL]
case refine'_1
M : Type u_1
A : Type u_2
B : Type u_3
R : Type u_4
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
b : R
hb : b ∈ AddSubmonoid.closure ↑S
⊢ ∀ (x : R), x ∈ ↑S → (fun z => ∀ {a : R}, a ∈ AddSubmonoid.closure ↑S → a * z ∈ AddSubmonoid.closure ↑S) x
[PROOFSTEP]
clear hb b
[GOAL]
case refine'_2
M : Type u_1
A : Type u_2
B : Type u_3
R : Type u_4
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
b : R
hb : b ∈ AddSubmonoid.closure ↑S
⊢ (fun z => ∀ {a : R}, a ∈ AddSubmonoid.closure ↑S → a * z ∈ AddSubmonoid.closure ↑S) 0
[PROOFSTEP]
clear hb b
[GOAL]
case refine'_3
M : Type u_1
A : Type u_2
B : Type u_3
R : Type u_4
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
b : R
hb : b ∈ AddSubmonoid.closure ↑S
⊢ ∀ (x y : R),
    (fun z => ∀ {a : R}, a ∈ AddSubmonoid.closure ↑S → a * z ∈ AddSubmonoid.closure ↑S) x →
      (fun z => ∀ {a : R}, a ∈ AddSubmonoid.closure ↑S → a * z ∈ AddSubmonoid.closure ↑S) y →
        (fun z => ∀ {a : R}, a ∈ AddSubmonoid.closure ↑S → a * z ∈ AddSubmonoid.closure ↑S) (x + y)
[PROOFSTEP]
clear hb b
[GOAL]
case refine'_1
M : Type u_1
A : Type u_2
B : Type u_3
R : Type u_4
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
⊢ ∀ (x : R), x ∈ ↑S → (fun z => ∀ {a : R}, a ∈ AddSubmonoid.closure ↑S → a * z ∈ AddSubmonoid.closure ↑S) x
[PROOFSTEP]
exact fun r hr b hb => MulMemClass.mul_right_mem_add_closure hb hr
[GOAL]
case refine'_2
M : Type u_1
A : Type u_2
B : Type u_3
R : Type u_4
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
⊢ (fun z => ∀ {a : R}, a ∈ AddSubmonoid.closure ↑S → a * z ∈ AddSubmonoid.closure ↑S) 0
[PROOFSTEP]
exact fun _ => by simp only [mul_zero, (AddSubmonoid.closure (S : Set R)).zero_mem]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
R : Type u_4
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a✝ : R
x✝ : a✝ ∈ AddSubmonoid.closure ↑S
⊢ a✝ * 0 ∈ AddSubmonoid.closure ↑S
[PROOFSTEP]
simp only [mul_zero, (AddSubmonoid.closure (S : Set R)).zero_mem]
[GOAL]
case refine'_3
M : Type u_1
A : Type u_2
B : Type u_3
R : Type u_4
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
⊢ ∀ (x y : R),
    (fun z => ∀ {a : R}, a ∈ AddSubmonoid.closure ↑S → a * z ∈ AddSubmonoid.closure ↑S) x →
      (fun z => ∀ {a : R}, a ∈ AddSubmonoid.closure ↑S → a * z ∈ AddSubmonoid.closure ↑S) y →
        (fun z => ∀ {a : R}, a ∈ AddSubmonoid.closure ↑S → a * z ∈ AddSubmonoid.closure ↑S) (x + y)
[PROOFSTEP]
simp_rw [mul_add]
[GOAL]
case refine'_3
M : Type u_1
A : Type u_2
B : Type u_3
R : Type u_4
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
⊢ ∀ (x y : R),
    (∀ {a : R}, a ∈ AddSubmonoid.closure ↑S → a * x ∈ AddSubmonoid.closure ↑S) →
      (∀ {a : R}, a ∈ AddSubmonoid.closure ↑S → a * y ∈ AddSubmonoid.closure ↑S) →
        ∀ {a : R}, a ∈ AddSubmonoid.closure ↑S → a * x + a * y ∈ AddSubmonoid.closure ↑S
[PROOFSTEP]
exact fun r s hr hs b hb => (AddSubmonoid.closure (S : Set R)).add_mem (hr hb) (hs hb)
[GOAL]
M : Type u_1
A✝ : Type u_2
B : Type u_3
A : Type u_4
inst✝ : CommMonoid A
a b c : A
⊢ c ∈ closure {a, b} ↔ ∃ m n, a ^ m * b ^ n = c
[PROOFSTEP]
rw [← Set.singleton_union, Submonoid.closure_union, mem_sup]
[GOAL]
M : Type u_1
A✝ : Type u_2
B : Type u_3
A : Type u_4
inst✝ : CommMonoid A
a b c : A
⊢ (∃ y, y ∈ closure {a} ∧ ∃ z, z ∈ closure {b} ∧ y * z = c) ↔ ∃ m n, a ^ m * b ^ n = c
[PROOFSTEP]
simp_rw [mem_closure_singleton, exists_exists_eq_and]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
x : M
⊢ ↑Additive.ofMul '' ↑(Submonoid.powers x) = ↑(AddSubmonoid.multiples (↑Additive.ofMul x))
[PROOFSTEP]
ext
[GOAL]
case h
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
x : M
x✝ : Additive M
⊢ x✝ ∈ ↑Additive.ofMul '' ↑(Submonoid.powers x) ↔ x✝ ∈ ↑(AddSubmonoid.multiples (↑Additive.ofMul x))
[PROOFSTEP]
constructor
[GOAL]
case h.mp
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
x : M
x✝ : Additive M
⊢ x✝ ∈ ↑Additive.ofMul '' ↑(Submonoid.powers x) → x✝ ∈ ↑(AddSubmonoid.multiples (↑Additive.ofMul x))
[PROOFSTEP]
rintro ⟨y, ⟨n, hy1⟩, hy2⟩
[GOAL]
case h.mp.intro.intro.intro
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
x : M
x✝ : Additive M
y : M
hy2 : ↑Additive.ofMul y = x✝
n : ℕ
hy1 : (fun x x_1 => x ^ x_1) x n = y
⊢ x✝ ∈ ↑(AddSubmonoid.multiples (↑Additive.ofMul x))
[PROOFSTEP]
use n
[GOAL]
case h
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
x : M
x✝ : Additive M
y : M
hy2 : ↑Additive.ofMul y = x✝
n : ℕ
hy1 : (fun x x_1 => x ^ x_1) x n = y
⊢ (fun i => i • ↑Additive.ofMul x) n = x✝
[PROOFSTEP]
simpa [← ofMul_pow, hy1]
[GOAL]
case h.mpr
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
x : M
x✝ : Additive M
⊢ x✝ ∈ ↑(AddSubmonoid.multiples (↑Additive.ofMul x)) → x✝ ∈ ↑Additive.ofMul '' ↑(Submonoid.powers x)
[PROOFSTEP]
rintro ⟨n, hn⟩
[GOAL]
case h.mpr.intro
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
x : M
x✝ : Additive M
n : ℕ
hn : (fun i => i • ↑Additive.ofMul x) n = x✝
⊢ x✝ ∈ ↑Additive.ofMul '' ↑(Submonoid.powers x)
[PROOFSTEP]
refine' ⟨x ^ n, ⟨n, rfl⟩, _⟩
[GOAL]
case h.mpr.intro
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
x : M
x✝ : Additive M
n : ℕ
hn : (fun i => i • ↑Additive.ofMul x) n = x✝
⊢ ↑Additive.ofMul (x ^ n) = x✝
[PROOFSTEP]
rwa [ofMul_pow]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : AddMonoid A
x : A
⊢ ↑Multiplicative.ofAdd '' ↑(AddSubmonoid.multiples x) = ↑(Submonoid.powers (↑Multiplicative.ofAdd x))
[PROOFSTEP]
symm
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : AddMonoid A
x : A
⊢ ↑(Submonoid.powers (↑Multiplicative.ofAdd x)) = ↑Multiplicative.ofAdd '' ↑(AddSubmonoid.multiples x)
[PROOFSTEP]
rw [Equiv.eq_image_iff_symm_image_eq]
[GOAL]
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : AddMonoid A
x : A
⊢ ↑Multiplicative.ofAdd.symm '' ↑(Submonoid.powers (↑Multiplicative.ofAdd x)) = ↑(AddSubmonoid.multiples x)
[PROOFSTEP]
exact ofMul_image_powers_eq_multiples_ofMul
