[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


[GOAL]
n : ℕ
⊢ ∀ (a b c : DihedralGroup n), a * b * c = a * (b * c)
[PROOFSTEP]
rintro (a | a) (b | b) (c | c)
[GOAL]
case r.r.r
n : ℕ
a b c : ZMod n
⊢ r a * r b * r c = r a * (r b * r c)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case r.r.sr
n : ℕ
a b c : ZMod n
⊢ r a * r b * sr c = r a * (r b * sr c)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case r.sr.r
n : ℕ
a b c : ZMod n
⊢ r a * sr b * r c = r a * (sr b * r c)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case r.sr.sr
n : ℕ
a b c : ZMod n
⊢ r a * sr b * sr c = r a * (sr b * sr c)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case sr.r.r
n : ℕ
a b c : ZMod n
⊢ sr a * r b * r c = sr a * (r b * r c)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case sr.r.sr
n : ℕ
a b c : ZMod n
⊢ sr a * r b * sr c = sr a * (r b * sr c)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case sr.sr.r
n : ℕ
a b c : ZMod n
⊢ sr a * sr b * r c = sr a * (sr b * r c)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case sr.sr.sr
n : ℕ
a b c : ZMod n
⊢ sr a * sr b * sr c = sr a * (sr b * sr c)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case r.r.r
n : ℕ
a b c : ZMod n
⊢ r (a + b + c) = r (a + (b + c))
[PROOFSTEP]
ring_nf
[GOAL]
case r.r.sr
n : ℕ
a b c : ZMod n
⊢ sr (c - (a + b)) = sr (c - b - a)
[PROOFSTEP]
ring_nf
[GOAL]
case r.sr.r
n : ℕ
a b c : ZMod n
⊢ sr (b - a + c) = sr (b + c - a)
[PROOFSTEP]
ring_nf
[GOAL]
case r.sr.sr
n : ℕ
a b c : ZMod n
⊢ r (c - (b - a)) = r (a + (c - b))
[PROOFSTEP]
ring_nf
[GOAL]
case sr.r.r
n : ℕ
a b c : ZMod n
⊢ sr (a + b + c) = sr (a + (b + c))
[PROOFSTEP]
ring_nf
[GOAL]
case sr.r.sr
n : ℕ
a b c : ZMod n
⊢ r (c - (a + b)) = r (c - b - a)
[PROOFSTEP]
ring_nf
[GOAL]
case sr.sr.r
n : ℕ
a b c : ZMod n
⊢ r (b - a + c) = r (b + c - a)
[PROOFSTEP]
ring_nf
[GOAL]
case sr.sr.sr
n : ℕ
a b c : ZMod n
⊢ sr (c - (b - a)) = sr (a + (c - b))
[PROOFSTEP]
ring_nf
[GOAL]
n : ℕ
⊢ ∀ (a : DihedralGroup n), 1 * a = a
[PROOFSTEP]
rintro (a | a)
[GOAL]
case r
n : ℕ
a : ZMod n
⊢ 1 * r a = r a
case sr n : ℕ a : ZMod n ⊢ 1 * sr a = sr a
[PROOFSTEP]
exact congr_arg r (zero_add a)
[GOAL]
case sr
n : ℕ
a : ZMod n
⊢ 1 * sr a = sr a
[PROOFSTEP]
exact congr_arg sr (sub_zero a)
[GOAL]
n : ℕ
⊢ ∀ (a : DihedralGroup n), a * 1 = a
[PROOFSTEP]
rintro (a | a)
[GOAL]
case r
n : ℕ
a : ZMod n
⊢ r a * 1 = r a
case sr n : ℕ a : ZMod n ⊢ sr a * 1 = sr a
[PROOFSTEP]
exact congr_arg r (add_zero a)
[GOAL]
case sr
n : ℕ
a : ZMod n
⊢ sr a * 1 = sr a
[PROOFSTEP]
exact congr_arg sr (add_zero a)
[GOAL]
n : ℕ
⊢ ∀ (a : DihedralGroup n), a⁻¹ * a = 1
[PROOFSTEP]
rintro (a | a)
[GOAL]
case r
n : ℕ
a : ZMod n
⊢ (r a)⁻¹ * r a = 1
case sr n : ℕ a : ZMod n ⊢ (sr a)⁻¹ * sr a = 1
[PROOFSTEP]
exact congr_arg r (neg_add_self a)
[GOAL]
case sr
n : ℕ
a : ZMod n
⊢ (sr a)⁻¹ * sr a = 1
[PROOFSTEP]
exact congr_arg r (sub_self a)
[GOAL]
n : ℕ
⊢ Function.LeftInverse
    (fun i =>
      match i with
      | r j => Sum.inl j
      | sr j => Sum.inr j)
    fun i =>
    match i with
    | Sum.inl j => r j
    | Sum.inr j => sr j
[PROOFSTEP]
rintro (x | x)
[GOAL]
case inl
n : ℕ
x : ZMod n
⊢ (fun i =>
        match i with
        | r j => Sum.inl j
        | sr j => Sum.inr j)
      ((fun i =>
          match i with
          | Sum.inl j => r j
          | Sum.inr j => sr j)
        (Sum.inl x)) =
    Sum.inl x
[PROOFSTEP]
rfl
[GOAL]
case inr
n : ℕ
x : ZMod n
⊢ (fun i =>
        match i with
        | r j => Sum.inl j
        | sr j => Sum.inr j)
      ((fun i =>
          match i with
          | Sum.inl j => r j
          | Sum.inr j => sr j)
        (Sum.inr x)) =
    Sum.inr x
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ Function.RightInverse
    (fun i =>
      match i with
      | r j => Sum.inl j
      | sr j => Sum.inr j)
    fun i =>
    match i with
    | Sum.inl j => r j
    | Sum.inr j => sr j
[PROOFSTEP]
rintro (x | x)
[GOAL]
case r
n : ℕ
x : ZMod n
⊢ (fun i =>
        match i with
        | Sum.inl j => r j
        | Sum.inr j => sr j)
      ((fun i =>
          match i with
          | r j => Sum.inl j
          | sr j => Sum.inr j)
        (r x)) =
    r x
[PROOFSTEP]
rfl
[GOAL]
case sr
n : ℕ
x : ZMod n
⊢ (fun i =>
        match i with
        | Sum.inl j => r j
        | Sum.inr j => sr j)
      ((fun i =>
          match i with
          | r j => Sum.inl j
          | sr j => Sum.inr j)
        (sr x)) =
    sr x
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ r 0 ≠ sr 0
[PROOFSTEP]
simp_rw [ne_eq]
[GOAL]
n : ℕ
inst✝ : NeZero n
⊢ Fintype.card (DihedralGroup n) = 2 * n
[PROOFSTEP]
rw [← Fintype.card_eq.mpr ⟨fintypeHelper⟩, Fintype.card_sum, ZMod.card, two_mul]
[GOAL]
n : ℕ
⊢ Nat.card (DihedralGroup n) = 2 * n
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ Nat.card (DihedralGroup Nat.zero) = 2 * Nat.zero
[PROOFSTEP]
rw [Nat.card_eq_zero_of_infinite]
[GOAL]
case succ
n✝ : ℕ
⊢ Nat.card (DihedralGroup (Nat.succ n✝)) = 2 * Nat.succ n✝
[PROOFSTEP]
rw [Nat.card_eq_fintype_card, card]
[GOAL]
n k : ℕ
⊢ r 1 ^ k = r ↑k
[PROOFSTEP]
induction' k with k IH
[GOAL]
case zero
n : ℕ
⊢ r 1 ^ Nat.zero = r ↑Nat.zero
[PROOFSTEP]
rw [Nat.cast_zero]
[GOAL]
case zero
n : ℕ
⊢ r 1 ^ Nat.zero = r 0
[PROOFSTEP]
rfl
[GOAL]
case succ
n k : ℕ
IH : r 1 ^ k = r ↑k
⊢ r 1 ^ Nat.succ k = r ↑(Nat.succ k)
[PROOFSTEP]
rw [pow_succ, IH, r_mul_r]
[GOAL]
case succ
n k : ℕ
IH : r 1 ^ k = r ↑k
⊢ r (1 + ↑k) = r ↑(Nat.succ k)
[PROOFSTEP]
congr 1
[GOAL]
case succ.e_a
n k : ℕ
IH : r 1 ^ k = r ↑k
⊢ 1 + ↑k = ↑(Nat.succ k)
[PROOFSTEP]
norm_cast
[GOAL]
case succ.e_a
n k : ℕ
IH : r 1 ^ k = r ↑k
⊢ ↑(1 + k) = ↑(Nat.succ k)
[PROOFSTEP]
rw [Nat.one_add]
[GOAL]
n : ℕ
⊢ r 1 ^ n = 1
[PROOFSTEP]
rw [r_one_pow, one_def]
[GOAL]
n : ℕ
⊢ r ↑n = r 0
[PROOFSTEP]
congr 1
[GOAL]
case e_a
n : ℕ
⊢ ↑n = 0
[PROOFSTEP]
exact ZMod.nat_cast_self _
[GOAL]
n : ℕ
i : ZMod n
⊢ sr i * sr i = 1
[PROOFSTEP]
rw [sr_mul_sr, sub_self, one_def]
[GOAL]
n : ℕ
i : ZMod n
⊢ orderOf (sr i) = 2
[PROOFSTEP]
apply orderOf_eq_prime
[GOAL]
case hg
n : ℕ
i : ZMod n
⊢ sr i ^ 2 = 1
[PROOFSTEP]
rw [sq, sr_mul_self]
[GOAL]
case hg1
n : ℕ
i : ZMod n
⊢ sr i ≠ 1
[PROOFSTEP]
revert n
[GOAL]
case hg1
⊢ ∀ {n : ℕ} (i : ZMod n), sr i ≠ 1
[PROOFSTEP]
simp_rw [one_def, ne_eq, forall_const]
[GOAL]
n : ℕ
⊢ orderOf (r 1) = n
[PROOFSTEP]
rcases eq_zero_or_neZero n with (rfl | hn)
[GOAL]
case inl
⊢ orderOf (r 1) = 0
[PROOFSTEP]
rw [orderOf_eq_zero_iff']
[GOAL]
case inl
⊢ ∀ (n : ℕ), 0 < n → r 1 ^ n ≠ 1
[PROOFSTEP]
intro n hn
[GOAL]
case inl
n : ℕ
hn : 0 < n
⊢ r 1 ^ n ≠ 1
[PROOFSTEP]
rw [r_one_pow, one_def]
[GOAL]
case inl
n : ℕ
hn : 0 < n
⊢ r ↑n ≠ r 0
[PROOFSTEP]
apply mt r.inj
[GOAL]
case inl
n : ℕ
hn : 0 < n
⊢ ¬↑n = 0
[PROOFSTEP]
simpa using hn.ne'
[GOAL]
case inr
n : ℕ
hn : NeZero n
⊢ orderOf (r 1) = n
[PROOFSTEP]
apply (Nat.le_of_dvd (NeZero.pos n) <| orderOf_dvd_of_pow_eq_one <| @r_one_pow_n n).lt_or_eq.resolve_left
[GOAL]
case inr
n : ℕ
hn : NeZero n
⊢ ¬orderOf (r 1) < n
[PROOFSTEP]
intro h
[GOAL]
case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
⊢ False
[PROOFSTEP]
have h1 : (r 1 : DihedralGroup n) ^ orderOf (r 1) = 1 := pow_orderOf_eq_one _
[GOAL]
case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
h1 : r 1 ^ orderOf (r 1) = 1
⊢ False
[PROOFSTEP]
rw [r_one_pow] at h1
[GOAL]
case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
h1 : r ↑(orderOf (r 1)) = 1
⊢ False
[PROOFSTEP]
injection h1 with h2
[GOAL]
case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
h2 : ↑(orderOf (r 1)) = 0
⊢ False
[PROOFSTEP]
rw [← ZMod.val_eq_zero, ZMod.val_nat_cast, Nat.mod_eq_of_lt h] at h2
[GOAL]
case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
h2 : orderOf (r 1) = 0
⊢ False
[PROOFSTEP]
exact absurd h2.symm (orderOf_pos _).ne
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod n
⊢ orderOf (r i) = n / Nat.gcd n (ZMod.val i)
[PROOFSTEP]
conv_lhs => rw [← ZMod.nat_cast_zmod_val i]
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod n
| orderOf (r i)
[PROOFSTEP]
rw [← ZMod.nat_cast_zmod_val i]
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod n
| orderOf (r i)
[PROOFSTEP]
rw [← ZMod.nat_cast_zmod_val i]
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod n
| orderOf (r i)
[PROOFSTEP]
rw [← ZMod.nat_cast_zmod_val i]
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod n
⊢ orderOf (r ↑(ZMod.val i)) = n / Nat.gcd n (ZMod.val i)
[PROOFSTEP]
rw [← r_one_pow, orderOf_pow, orderOf_r_one]
[GOAL]
n : ℕ
⊢ Monoid.exponent (DihedralGroup n) = lcm n 2
[PROOFSTEP]
rcases eq_zero_or_neZero n with (rfl | hn)
[GOAL]
case inl
⊢ Monoid.exponent (DihedralGroup 0) = lcm 0 2
[PROOFSTEP]
exact Monoid.exponent_eq_zero_of_order_zero orderOf_r_one
[GOAL]
case inr
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (DihedralGroup n) = lcm n 2
[PROOFSTEP]
apply Nat.dvd_antisymm
[GOAL]
case inr.a
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (DihedralGroup n) ∣ lcm n 2
[PROOFSTEP]
apply Monoid.exponent_dvd_of_forall_pow_eq_one
[GOAL]
case inr.a.hG
n : ℕ
hn : NeZero n
⊢ ∀ (g : DihedralGroup n), g ^ lcm n 2 = 1
[PROOFSTEP]
rintro (m | m)
[GOAL]
case inr.a.hG.r
n : ℕ
hn : NeZero n
m : ZMod n
⊢ r m ^ lcm n 2 = 1
[PROOFSTEP]
rw [← orderOf_dvd_iff_pow_eq_one, orderOf_r]
[GOAL]
case inr.a.hG.r
n : ℕ
hn : NeZero n
m : ZMod n
⊢ n / Nat.gcd n (ZMod.val m) ∣ lcm n 2
[PROOFSTEP]
refine' Nat.dvd_trans ⟨gcd n m.val, _⟩ (dvd_lcm_left n 2)
[GOAL]
case inr.a.hG.r
n : ℕ
hn : NeZero n
m : ZMod n
⊢ n = n / Nat.gcd n (ZMod.val m) * gcd n (ZMod.val m)
[PROOFSTEP]
exact (Nat.div_mul_cancel (Nat.gcd_dvd_left n m.val)).symm
[GOAL]
case inr.a.hG.sr
n : ℕ
hn : NeZero n
m : ZMod n
⊢ sr m ^ lcm n 2 = 1
[PROOFSTEP]
rw [← orderOf_dvd_iff_pow_eq_one, orderOf_sr]
[GOAL]
case inr.a.hG.sr
n : ℕ
hn : NeZero n
m : ZMod n
⊢ 2 ∣ lcm n 2
[PROOFSTEP]
exact dvd_lcm_right n 2
[GOAL]
case inr.a
n : ℕ
hn : NeZero n
⊢ lcm n 2 ∣ Monoid.exponent (DihedralGroup n)
[PROOFSTEP]
apply lcm_dvd
[GOAL]
case inr.a.hab
n : ℕ
hn : NeZero n
⊢ n ∣ Monoid.exponent (DihedralGroup n)
[PROOFSTEP]
convert Monoid.order_dvd_exponent (r (1 : ZMod n))
[GOAL]
case h.e'_3
n : ℕ
hn : NeZero n
⊢ n = orderOf (r 1)
[PROOFSTEP]
exact orderOf_r_one.symm
[GOAL]
case inr.a.hcb
n : ℕ
hn : NeZero n
⊢ 2 ∣ Monoid.exponent (DihedralGroup n)
[PROOFSTEP]
convert Monoid.order_dvd_exponent (sr (0 : ZMod n))
[GOAL]
case h.e'_3
n : ℕ
hn : NeZero n
⊢ 2 = orderOf (sr 0)
[PROOFSTEP]
exact (orderOf_sr 0).symm
[GOAL]
n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 (_ : Nat.coprime 2 n)
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h : Commute (r i, sr j).fst (r i, sr j).snd
⊢ (fun x =>
        match x with
        | Sum.inl i => { val := (sr i, r 0), property := (_ : sr (i + 0) = sr (i - 0)) }
        | Sum.inr (Sum.inl j) => { val := (r 0, sr j), property := (_ : sr (j - 0) = sr (j + 0)) }
        | Sum.inr (Sum.inr (Sum.inl k)) =>
          { val := (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)),
            property :=
              (_ :
                (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).fst * (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).snd =
                  (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).fst * (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).snd) }
        | Sum.inr (Sum.inr (Sum.inr (i, j))) => { val := (r i, r j), property := (_ : r (i + j) = r (j + i)) })
      ((fun x =>
          match x with
          | { val := (sr i, r a), property := property } => Sum.inl i
          | { val := (r a, sr j), property := property } => Sum.inr (Sum.inl j)
          | { val := (sr i, sr j), property := property } => Sum.inr (Sum.inr (Sum.inl (i + j)))
          | { val := (r i, r j), property := property } => Sum.inr (Sum.inr (Sum.inr (i, j))))
        { val := (r i, sr j), property := h }) =
    { val := (r i, sr j), property := h }
[PROOFSTEP]
simpa [sub_eq_add_neg, neg_eq_iff_add_eq_zero, hu, eq_comm (a := i) (b := 0)] using h.eq
[GOAL]
n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 (_ : Nat.coprime 2 n)
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h : Commute (sr i, r j).fst (sr i, r j).snd
⊢ (fun x =>
        match x with
        | Sum.inl i => { val := (sr i, r 0), property := (_ : sr (i + 0) = sr (i - 0)) }
        | Sum.inr (Sum.inl j) => { val := (r 0, sr j), property := (_ : sr (j - 0) = sr (j + 0)) }
        | Sum.inr (Sum.inr (Sum.inl k)) =>
          { val := (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)),
            property :=
              (_ :
                (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).fst * (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).snd =
                  (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).fst * (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).snd) }
        | Sum.inr (Sum.inr (Sum.inr (i, j))) => { val := (r i, r j), property := (_ : r (i + j) = r (j + i)) })
      ((fun x =>
          match x with
          | { val := (sr i, r a), property := property } => Sum.inl i
          | { val := (r a, sr j), property := property } => Sum.inr (Sum.inl j)
          | { val := (sr i, sr j), property := property } => Sum.inr (Sum.inr (Sum.inl (i + j)))
          | { val := (r i, r j), property := property } => Sum.inr (Sum.inr (Sum.inr (i, j))))
        { val := (sr i, r j), property := h }) =
    { val := (sr i, r j), property := h }
[PROOFSTEP]
simpa [sub_eq_add_neg, eq_neg_iff_add_eq_zero, hu, eq_comm (a := j) (b := 0)] using h.eq
[GOAL]
n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 (_ : Nat.coprime 2 n)
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h : Commute (sr i, sr j).fst (sr i, sr j).snd
⊢ (fun x =>
        match x with
        | Sum.inl i => { val := (sr i, r 0), property := (_ : sr (i + 0) = sr (i - 0)) }
        | Sum.inr (Sum.inl j) => { val := (r 0, sr j), property := (_ : sr (j - 0) = sr (j + 0)) }
        | Sum.inr (Sum.inr (Sum.inl k)) =>
          { val := (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)),
            property :=
              (_ :
                (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).fst * (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).snd =
                  (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).fst * (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).snd) }
        | Sum.inr (Sum.inr (Sum.inr (i, j))) => { val := (r i, r j), property := (_ : r (i + j) = r (j + i)) })
      ((fun x =>
          match x with
          | { val := (sr i, r a), property := property } => Sum.inl i
          | { val := (r a, sr j), property := property } => Sum.inr (Sum.inl j)
          | { val := (sr i, sr j), property := property } => Sum.inr (Sum.inr (Sum.inl (i + j)))
          | { val := (r i, r j), property := property } => Sum.inr (Sum.inr (Sum.inr (i, j))))
        { val := (sr i, sr j), property := h }) =
    { val := (sr i, sr j), property := h }
[PROOFSTEP]
replace h := r.inj h
[GOAL]
n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 (_ : Nat.coprime 2 n)
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h✝ : Commute (sr i, sr j).fst (sr i, sr j).snd
h : j - i = i - j
⊢ (fun x =>
        match x with
        | Sum.inl i => { val := (sr i, r 0), property := (_ : sr (i + 0) = sr (i - 0)) }
        | Sum.inr (Sum.inl j) => { val := (r 0, sr j), property := (_ : sr (j - 0) = sr (j + 0)) }
        | Sum.inr (Sum.inr (Sum.inl k)) =>
          { val := (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)),
            property :=
              (_ :
                (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).fst * (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).snd =
                  (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).fst * (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).snd) }
        | Sum.inr (Sum.inr (Sum.inr (i, j))) => { val := (r i, r j), property := (_ : r (i + j) = r (j + i)) })
      ((fun x =>
          match x with
          | { val := (sr i, r a), property := property } => Sum.inl i
          | { val := (r a, sr j), property := property } => Sum.inr (Sum.inl j)
          | { val := (sr i, sr j), property := property } => Sum.inr (Sum.inr (Sum.inl (i + j)))
          | { val := (r i, r j), property := property } => Sum.inr (Sum.inr (Sum.inr (i, j))))
        { val := (sr i, sr j), property := h✝ }) =
    { val := (sr i, sr j), property := h✝ }
[PROOFSTEP]
rw [← neg_sub, neg_eq_iff_add_eq_zero, hu, sub_eq_zero] at h
[GOAL]
n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 (_ : Nat.coprime 2 n)
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h✝ : Commute (sr i, sr j).fst (sr i, sr j).snd
h : i = j
⊢ (fun x =>
        match x with
        | Sum.inl i => { val := (sr i, r 0), property := (_ : sr (i + 0) = sr (i - 0)) }
        | Sum.inr (Sum.inl j) => { val := (r 0, sr j), property := (_ : sr (j - 0) = sr (j + 0)) }
        | Sum.inr (Sum.inr (Sum.inl k)) =>
          { val := (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)),
            property :=
              (_ :
                (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).fst * (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).snd =
                  (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).fst * (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).snd) }
        | Sum.inr (Sum.inr (Sum.inr (i, j))) => { val := (r i, r j), property := (_ : r (i + j) = r (j + i)) })
      ((fun x =>
          match x with
          | { val := (sr i, r a), property := property } => Sum.inl i
          | { val := (r a, sr j), property := property } => Sum.inr (Sum.inl j)
          | { val := (sr i, sr j), property := property } => Sum.inr (Sum.inr (Sum.inl (i + j)))
          | { val := (r i, r j), property := property } => Sum.inr (Sum.inr (Sum.inr (i, j))))
        { val := (sr i, sr j), property := h✝ }) =
    { val := (sr i, sr j), property := h✝ }
[PROOFSTEP]
rw [Subtype.ext_iff, Prod.ext_iff, sr.injEq, sr.injEq, h, and_self, ← two_mul]
[GOAL]
n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 (_ : Nat.coprime 2 n)
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h✝ : Commute (sr i, sr j).fst (sr i, sr j).snd
h : i = j
⊢ ↑u⁻¹ * (2 * j) = j
[PROOFSTEP]
exact u.inv_mul_cancel_left j
[GOAL]
n : ℕ
hn : Odd n
⊢ Nat.card { p // Commute p.fst p.snd } = n * (n + 3)
[PROOFSTEP]
have hn' : NeZero n := ⟨hn.pos.ne'⟩
[GOAL]
n : ℕ
hn : Odd n
hn' : NeZero n
⊢ Nat.card { p // Commute p.fst p.snd } = n * (n + 3)
[PROOFSTEP]
simp_rw [Nat.card_congr (OddCommuteEquiv hn), Nat.card_sum, Nat.card_prod, Nat.card_zmod]
[GOAL]
n : ℕ
hn : Odd n
hn' : NeZero n
⊢ n + (n + (n + n * n)) = n * (n + 3)
[PROOFSTEP]
ring
[GOAL]
n : ℕ
hn : Odd n
⊢ Nat.card (ConjClasses (DihedralGroup n)) = (n + 3) / 2
[PROOFSTEP]
rw [← Nat.mul_div_mul_left _ 2 hn.pos, ← card_commute_odd hn, mul_comm, card_comm_eq_card_conjClasses_mul_card,
  nat_card, Nat.mul_div_left _ (mul_pos two_pos hn.pos)]