-- Mathlib/GroupTheory/Finiteness.lean
theorem Subgroup.fg_iff_submonoid_fg (P : Subgroup G) : P.FG ↔ P.toSubmonoid.FG

Proof state:
case mp
G : Type u_3
inst✝ : Group G
P : Subgroup G
⊢ P.FG → P.FG

Tactic:
rintro ⟨S, rfl⟩

Result:
case mp.intro
G : Type u_3
inst✝ : Group G
S : Finset G
⊢ (closure ↑S).FG

Proof state:
case mpr.intro.refine_2
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ P ≤ closure ↑S

Tactic:
rw [← Subgroup.toSubmonoid_le, ← hS, Submonoid.closure_le]

Result:
case mpr.intro.refine_2
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ ↑S ⊆ ↑(closure ↑S).toSubmonoid

Proof state:
case mp.intro
G : Type u_3
inst✝ : Group G
S : Finset G
⊢ ∃ S_1, Submonoid.closure S_1 = (closure ↑S).toSubmonoid ∧ S_1.Finite

Tactic:
refine ⟨S ∪ S⁻¹, ?_, S.finite_toSet.union S.finite_toSet.inv⟩

Result:
case mp.intro
G : Type u_3
inst✝ : Group G
S : Finset G
⊢ Submonoid.closure (↑S ∪ (↑S)⁻¹) = (closure ↑S).toSubmonoid

Proof state:
case mpr.intro
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ P.FG

Tactic:
refine ⟨S, le_antisymm ?_ ?_⟩

Result:
case mpr.intro.refine_1
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ closure ↑S ≤ P

case mpr.intro.refine_2
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ P ≤ closure ↑S

Proof state:
case mpr.intro.refine_2
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ ↑S ⊆ ↑(closure ↑S).toSubmonoid

Tactic:
exact Subgroup.subset_closure

Result:
no goals

Proof state:
case mpr.intro.refine_1
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ ↑S ⊆ ↑(Submonoid.closure ↑S)

Tactic:
exact Submonoid.subset_closure

Result:
no goals

Proof state:
G : Type u_3
inst✝ : Group G
P : Subgroup G
⊢ P.FG ↔ P.FG

Tactic:
constructor

Result:
case mp
G : Type u_3
inst✝ : Group G
P : Subgroup G
⊢ P.FG → P.FG

case mpr
G : Type u_3
inst✝ : Group G
P : Subgroup G
⊢ P.FG → P.FG

Proof state:
case mpr
G : Type u_3
inst✝ : Group G
P : Subgroup G
⊢ P.FG → P.FG

Tactic:
rintro ⟨S, hS⟩

Result:
case mpr.intro
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ P.FG

Proof state:
case mp.intro
G : Type u_3
inst✝ : Group G
S : Finset G
⊢ Submonoid.closure (↑S ∪ (↑S)⁻¹) = (closure ↑S).toSubmonoid

Tactic:
exact (Subgroup.closure_toSubmonoid _).symm

Result:
no goals

Proof state:
case mp.intro
G : Type u_3
inst✝ : Group G
S : Finset G
⊢ (closure ↑S).FG

Tactic:
rw [Submonoid.fg_iff]

Result:
case mp.intro
G : Type u_3
inst✝ : Group G
S : Finset G
⊢ ∃ S_1, Submonoid.closure S_1 = (closure ↑S).toSubmonoid ∧ S_1.Finite

Proof state:
case mpr.intro.refine_1
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ closure ↑S ≤ P

Tactic:
rw [Subgroup.closure_le, ← Subgroup.coe_toSubmonoid, ← hS]

Result:
case mpr.intro.refine_1
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ ↑S ⊆ ↑(Submonoid.closure ↑S)