case mp
M : Type ?u.69638
N : Type ?u.69641
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.69653
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
⊢ FG P → Submonoid.FG P.toSubmonoid

case mpr
M : Type ?u.69638
N : Type ?u.69641
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.69653
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
⊢ Submonoid.FG P.toSubmonoid → FG P
M : Type ?u.69638
N : Type ?u.69641
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.69653
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
⊢ FG P ↔ Submonoid.FG P.toSubmonoid
constructor
case mp.intro
M : Type ?u.69638
N : Type ?u.69641
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.69653
inst✝¹ : Group G
inst✝ : AddGroup H
S : Finset G
⊢ Submonoid.FG (closure ↑S).toSubmonoid
case mp
M : Type ?u.69638
N : Type ?u.69641
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.69653
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
⊢ FG P → Submonoid.FG P.toSubmonoid
rintro ⟨S, rfl⟩
case mp.intro
M : Type ?u.69638
N : Type ?u.69641
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.69653
inst✝¹ : Group G
inst✝ : AddGroup H
S : Finset G
⊢ ∃ S_1, Submonoid.closure S_1 = (closure ↑S).toSubmonoid ∧ Set.Finite S_1
case mp.intro
M : Type ?u.69638
N : Type ?u.69641
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.69653
inst✝¹ : Group G
inst✝ : AddGroup H
S : Finset G
⊢ Submonoid.FG (closure ↑S).toSubmonoid
rw [Submonoid.fg_iff]
case mp.intro
M : Type ?u.69638
N : Type ?u.69641
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.69653
inst✝¹ : Group G
inst✝ : AddGroup H
S : Finset G
⊢ Submonoid.closure (↑S ∪ (↑S)⁻¹) = (closure ↑S).toSubmonoid
case mp.intro
M : Type ?u.69638
N : Type ?u.69641
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.69653
inst✝¹ : Group G
inst✝ : AddGroup H
S : Finset G
⊢ ∃ S_1, Submonoid.closure S_1 = (closure ↑S).toSubmonoid ∧ Set.Finite S_1
refine' ⟨S ∪ S⁻¹, _, S.finite_toSet.union S.finite_toSet.inv⟩
no goals
case mp.intro
M : Type ?u.69638
N : Type ?u.69641
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.69653
inst✝¹ : Group G
inst✝ : AddGroup H
S : Finset G
⊢ Submonoid.closure (↑S ∪ (↑S)⁻¹) = (closure ↑S).toSubmonoid
exact (Subgroup.closure_toSubmonoid _).symm
case mpr.intro
M : Type ?u.69638
N : Type ?u.69641
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.69653
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ FG P
case mpr
M : Type ?u.69638
N : Type ?u.69641
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.69653
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
⊢ Submonoid.FG P.toSubmonoid → FG P
rintro ⟨S, hS⟩
case mpr.intro.refine'_1
M : Type ?u.69638
N : Type ?u.69641
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.69653
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ closure ↑S ≤ P

case mpr.intro.refine'_2
M : Type ?u.69638
N : Type ?u.69641
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.69653
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ P ≤ closure ↑S
case mpr.intro
M : Type ?u.69638
N : Type ?u.69641
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.69653
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ FG P
refine' ⟨S, le_antisymm _ _⟩
case mpr.intro.refine'_1
M : Type ?u.69638
N : Type ?u.69641
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.69653
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ ↑S ⊆ ↑(Submonoid.closure ↑S)
case mpr.intro.refine'_1
M : Type ?u.69638
N : Type ?u.69641
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.69653
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ closure ↑S ≤ P
rw [Subgroup.closure_le, ← Subgroup.coe_toSubmonoid, ← hS]
no goals
case mpr.intro.refine'_1
M : Type ?u.69638
N : Type ?u.69641
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.69653
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ ↑S ⊆ ↑(Submonoid.closure ↑S)
exact Submonoid.subset_closure
case mpr.intro.refine'_2
M : Type ?u.69638
N : Type ?u.69641
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.69653
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ ↑S ⊆ ↑(closure ↑S).toSubmonoid
case mpr.intro.refine'_2
M : Type ?u.69638
N : Type ?u.69641
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.69653
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ P ≤ closure ↑S
rw [← Subgroup.toSubmonoid_le, ← hS, Submonoid.closure_le]
no goals
case mpr.intro.refine'_2
M : Type ?u.69638
N : Type ?u.69641
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.69653
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ ↑S ⊆ ↑(closure ↑S).toSubmonoid
exact Subgroup.subset_closure