awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
⊢ FG M ↔
    ∃ (S : Set M) (_ : S.Finite) (φ : FreeMonoid (↑S : Type u_1) →* M),
      Function.Surjective (α := FreeMonoid (↑S : Type u_1)) (β := M) (⇑φ : (a : FreeMonoid (↑S : Type u_1)) → M)

Tactic:
⟨fun ⟨S, hS⟩ ↦ ⟨S, S.finite_toSet, FreeMonoid.lift Subtype.val, ?_⟩, ?_⟩

Premises used: FreeMonoid.lift, Exists, SetLike.coe, Iff.intro, Exists.intro, _private.0.Monoid.fg_iff_exists_freeMonoid_hom_surjective.match_1, Finset.finite_toSet, Subtype.val, DFunLike.coe, Function.Surjective
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
refine_1 :
  FG M →
    ∀ (S : Finset M) (hS : Eq (α := Submonoid M) (Submonoid.closure (↑S : Set M)) ⊤),
      Function.Surjective.{u_1 + 1, u_1 + 1} (α := FreeMonoid (↑(↑S : Set M) : Type u_1)) (β := M)
        (⇑((FreeMonoid.lift : (a : (↑(↑S : Set M) : Type u_1) → M) → FreeMonoid (↑(↑S : Set M) : Type u_1) →* M)
                (Subtype.val (p := fun (x : M) ↦ x ∈ (↑S : Set M))) :
              FreeMonoid (↑(↑S : Set M) : Type u_1) →* M) :
          (a : FreeMonoid (↑(↑S : Set M) : Type u_1)) → M)
refine_2 :
  (∃ (S : Set M) (_ : S.Finite) (φ : FreeMonoid (↑S : Type u_1) →* M),
      Function.Surjective (α := FreeMonoid (↑S : Type u_1)) (β := M) (⇑φ : (a : FreeMonoid (↑S : Type u_1)) → M)) →
    FG M
⊢ FG M ↔
    ∃ (S : Set M) (_ : S.Finite) (φ : FreeMonoid (↑S : Type u_1) →* M),
      Function.Surjective (α := FreeMonoid (↑S : Type u_1)) (β := M) (⇑φ : (a : FreeMonoid (↑S : Type u_1)) → M)

Tactic:
refine ⟨fun ⟨S, hS⟩ ↦ ⟨S, S.finite_toSet, FreeMonoid.lift Subtype.val, ?_⟩, ?_⟩
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
h : FG M
S : Finset M
hS : Eq (α := Submonoid M) (Submonoid.closure (↑S : Set M)) ⊤
refine_1 :
  Eq (α := Submonoid M)
    (MonoidHom.mrange (F := FreeMonoid (↑(↑S : Set M) : Type u_1) →* M)
      ((FreeMonoid.lift : (a : (↑(↑S : Set M) : Type u_1) → M) → FreeMonoid (↑(↑S : Set M) : Type u_1) →* M)
          (Subtype.val (p := fun (x : M) ↦ x ∈ (↑S : Set M))) :
        FreeMonoid (↑(↑S : Set M) : Type u_1) →* M))
    ⊤
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : Eq (α := Submonoid M) (Submonoid.closure (↑S : Set M)) ⊤
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := FreeMonoid (↑(↑S : Set M) : Type u_1)) (β := M)
    (⇑((FreeMonoid.lift : (a : (↑(↑S : Set M) : Type u_1) → M) → FreeMonoid (↑(↑S : Set M) : Type u_1) →* M)
            (Subtype.val (p := fun (x : M) ↦ x ∈ (↑S : Set M))) :
          FreeMonoid (↑(↑S : Set M) : Type u_1) →* M) :
      (a : FreeMonoid (↑(↑S : Set M) : Type u_1)) → M)

Tactic:
rwa [← MonoidHom.mrange_eq_top, ← Submonoid.closure_eq_mrange]

Premises used: MonoidHom.mrange_eq_top, Submonoid.closure_eq_mrange
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
S : Set M
hfin : Finite.{u_1 + 1} (↑S : Type u_1)
φ : FreeMonoid (↑S : Type u_1) →* M
hφ : Function.Surjective (α := FreeMonoid (↑S : Type u_1)) (β := M) (⇑φ : (a : FreeMonoid (↑S : Type u_1)) → M)
⊢ FG M

Tactic:
fg_iff.mpr ⟨φ '' Set.range FreeMonoid.of, ?_, Set.toFinite _⟩

Premises used: Iff.mpr, Set.toFinite, Monoid.fg_iff, FreeMonoid.of, And.intro, Exists.intro, Set.image, Set.range, DFunLike.coe
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
S : Set M
hfin : Finite.{u_1 + 1} (↑S : Type u_1)
φ : FreeMonoid (↑S : Type u_1) →* M
hφ : Function.Surjective (α := FreeMonoid (↑S : Type u_1)) (β := M) (⇑φ : (a : FreeMonoid (↑S : Type u_1)) → M)
refine_2 :
  Eq (α := Submonoid M)
    (Submonoid.closure
      (Set.image (α := FreeMonoid (↑S : Type u_1)) (⇑φ : (a : FreeMonoid (↑S : Type u_1)) → M)
        (Set.range FreeMonoid.of)))
    ⊤
⊢ FG M

Tactic:
refine fg_iff.mpr ⟨φ '' Set.range FreeMonoid.of, ?_, Set.toFinite _⟩

Premises used: Iff.mpr, Set.toFinite, Monoid.fg_iff, FreeMonoid.of, And.intro, Exists.intro, Set.image, Set.range, DFunLike.coe
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
S : Set M
hfin : Finite.{u_1 + 1} (↑S : Type u_1)
φ : FreeMonoid (↑S : Type u_1) →* M
hφ : Function.Surjective (α := FreeMonoid (↑S : Type u_1)) (β := M) (⇑φ : (a : FreeMonoid (↑S : Type u_1)) → M)
⊢ Eq (α := Submonoid M)
    (Submonoid.closure
      (Set.image (α := FreeMonoid (↑S : Type u_1)) (⇑φ : (a : FreeMonoid (↑S : Type u_1)) → M)
        (Set.range FreeMonoid.of)))
    ⊤

Tactic:
simp [← MonoidHom.map_mclosure, hφ, FreeMonoid.closure_range_of, ← MonoidHom.mrange_eq_map]

Premises used: MonoidHom.mrange_eq_map, FreeMonoid.closure_range_of, MonoidHom.map_mclosure
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
mp :
  FG M →
    ∃ (α : Type) (_ : Finite α) (φ : FreeMonoid α →* M),
      Function.Surjective (α := FreeMonoid α) (β := M) (⇑φ : (a : FreeMonoid α) → M)
mpr :
  (∃ (α : Type) (_ : Finite α) (φ : FreeMonoid α →* M),
      Function.Surjective (α := FreeMonoid α) (β := M) (⇑φ : (a : FreeMonoid α) → M)) →
    FG M
⊢ FG M ↔
    ∃ (α : Type) (_ : Finite α) (φ : FreeMonoid α →* M),
      Function.Surjective (α := FreeMonoid α) (β := M) (⇑φ : (a : FreeMonoid α) → M)

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
mp :
  (∃ (S : Set M) (_ : S.Finite) (φ : FreeMonoid (↑S : Type u_1) →* M),
      Function.Surjective (α := FreeMonoid (↑S : Type u_1)) (β := M) (⇑φ : (a : FreeMonoid (↑S : Type u_1)) → M)) →
    ∃ (α : Type) (_ : Finite α) (φ : FreeMonoid α →* M),
      Function.Surjective (α := FreeMonoid α) (β := M) (⇑φ : (a : FreeMonoid α) → M)
⊢ FG M →
    ∃ (α : Type) (_ : Finite α) (φ : FreeMonoid α →* M),
      Function.Surjective (α := FreeMonoid α) (β := M) (⇑φ : (a : FreeMonoid α) → M)

Tactic:
rw [fg_iff_exists_freeMonoid_hom_surjective]

Premises used: Monoid.fg_iff_exists_freeMonoid_hom_surjective
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
S : Set M
hS : S.Finite
φ : FreeMonoid (↑S : Type u_1) →* M
hφ : Function.Surjective (α := FreeMonoid (↑S : Type u_1)) (β := M) (⇑φ : (a : FreeMonoid (↑S : Type u_1)) → M)
mp :
  ∀ (n : ℕ) (e : (↑S : Type u_1) ≃ Fin n),
    ∃ (α : Type) (_ : Finite α) (φ : FreeMonoid α →* M),
      Function.Surjective (α := FreeMonoid α) (β := M) (⇑φ : (a : FreeMonoid α) → M)
⊢ ∃ (α : Type) (_ : Finite α) (φ : FreeMonoid α →* M),
    Function.Surjective (α := FreeMonoid α) (β := M) (⇑φ : (a : FreeMonoid α) → M)

Tactic:
obtain ⟨n, ⟨e⟩⟩ := hS.exists_equiv_fin S

Premises used: Set.Elem, Finite.exists_equiv_fin
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
S : Set M
hS : S.Finite
φ : FreeMonoid (↑S : Type u_1) →* M
hφ : Function.Surjective (α := FreeMonoid (↑S : Type u_1)) (β := M) (⇑φ : (a : FreeMonoid (↑S : Type u_1)) → M)
n : ℕ
e : (↑S : Type u_1) ≃ Fin n
⊢ ∃ (α : Type) (_ : Finite α) (φ : FreeMonoid α →* M),
    Function.Surjective (α := FreeMonoid α) (β := M) (⇑φ : (a : FreeMonoid α) → M)

Tactic:
⟨Fin n, inferInstance, φ.comp (FreeMonoid.freeMonoidCongr e).symm,
      hφ.comp (FreeMonoid.freeMonoidCongr e).symm.surjective⟩

Premises used: inferInstance, MonoidHomClass.toMonoidHom, MonoidHom.comp, MulEquiv.surjective, Exists.intro, Function.Surjective.comp, FreeMonoid.freeMonoidCongr, MulEquiv.symm, Fin
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
S : Set M
hS : S.Finite
φ : FreeMonoid (↑S : Type u_1) →* M
hφ : Function.Surjective (α := FreeMonoid (↑S : Type u_1)) (β := M) (⇑φ : (a : FreeMonoid (↑S : Type u_1)) → M)
n : ℕ
e : (↑S : Type u_1) ≃ Fin n
⊢ ∃ (α : Type) (_ : Finite α) (φ : FreeMonoid α →* M),
    Function.Surjective (α := FreeMonoid α) (β := M) (⇑φ : (a : FreeMonoid α) → M)

Tactic:
exact ⟨Fin n, inferInstance, φ.comp (FreeMonoid.freeMonoidCongr e).symm,
      hφ.comp (FreeMonoid.freeMonoidCongr e).symm.surjective⟩
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
α : Type
w : Finite α
φ : FreeMonoid α →* M
hφ : Function.Surjective (α := FreeMonoid α) (β := M) (⇑φ : (a : FreeMonoid α) → M)
⊢ FG M

Tactic:
Monoid.fg_of_surjective _ hφ

Premises used: Monoid.fg_of_surjective
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
α : Type
w : Finite α
φ : FreeMonoid α →* M
hφ : Function.Surjective (α := FreeMonoid α) (β := M) (⇑φ : (a : FreeMonoid α) → M)
⊢ FG M

Tactic:
exact Monoid.fg_of_surjective _ hφ

Premises used: Monoid.fg_of_surjective
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
inst : Monoid M
r : M
⊢ FG (powers r)

Tactic:
⟨{r}, (Finset.coe_singleton r).symm ▸ (Submonoid.powers_eq_closure r).symm⟩

Premises used: Finset.coe_singleton, Eq.rec, Submonoid.powers_eq_closure, Exists.intro, Submonoid.FG, Singleton.singleton, Eq.symm
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
r : M
⊢ FG.{u_1} ↥(Submonoid.powers r)

Tactic:
(Monoid.fg_iff_submonoid_fg _).mpr (Submonoid.powers_fg r)

Premises used: Iff.mpr, Monoid.fg_iff_submonoid_fg, Submonoid.powers_fg
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
s : Finset M
⊢ FG.{u_1} ↥(Submonoid.closure (↑s : Set M))

Tactic:
⟨⟨s.preimage Subtype.val Subtype.coe_injective.injOn, ?_⟩⟩

Premises used: Monoid.FG.mk, Function.Injective.injOn, Subtype.coe_injective, Finset.preimage, Exists.intro, Subtype.val
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
s : Finset M
refine :
  Eq (α := Submonoid ↥(Submonoid.closure (↑s : Set M)))
    (Submonoid.closure
      (↑(s.preimage
            (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (Submonoid.closure (↑s : Set M)) x)) ⋯) :
        Set ↥(Submonoid.closure (↑s : Set M))))
    ⊤
⊢ FG.{u_1} ↥(Submonoid.closure (↑s : Set M))

Tactic:
refine ⟨⟨s.preimage Subtype.val Subtype.coe_injective.injOn, ?_⟩⟩
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
s : Finset M
rw :
  Eq (α := Submonoid ↥(Submonoid.closure (↑s : Set M)))
    (Submonoid.closure
      (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (Submonoid.closure (↑s : Set M)) x) ⁻¹'
        (↑s : Set M)))
    ⊤
rw₁ rw₂ : Eq.{u_1 + 1} (α := Submonoid ↥(Submonoid.closure (↑s : Set M))) ⊤ ⊤
⊢ Eq (α := Submonoid ↥(Submonoid.closure (↑s : Set M)))
    (Submonoid.closure
      (↑(s.preimage
            (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (Submonoid.closure (↑s : Set M)) x)) ⋯) :
        Set ↥(Submonoid.closure (↑s : Set M))))
    ⊤

Tactic:
rw [Finset.coe_preimage, Submonoid.closure_closure_coe_preimage]

Premises used: Finset.coe_preimage, Submonoid.closure_closure_coe_preimage
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
s : Set M
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ FG.{u_1} ↥(Submonoid.closure s)

Tactic:
haveI := Fintype.ofFinite s
  s.coe_toFinset ▸ Monoid.closure_finset_fg s.toFinset

Premises used: Eq.rec, Set.toFinset, Monoid.closure_finset_fg, Set.coe_toFinset
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
P : Subgroup G
h : ∃ (S : Set G), closure S = P ∧ S.Finite
S : Set G
hS : closure S = P
hf : S.Finite
⊢ closure (↑(hf.toFinset (s := S)) : Set G) = P

Tactic:
simp [hS]
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
P : Subgroup G
mp : P.FG → P.FG
mpr : P.FG → P.FG
⊢ P.FG ↔ P.FG

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
S : Finset G
mp : ∃ (S_1 : Set G), Eq (α := Submonoid G) (Submonoid.closure S_1) (toSubmonoid (closure (↑S : Set G))) ∧ S_1.Finite
⊢ Submonoid.FG (toSubmonoid (closure (↑S : Set G)))

Tactic:
rw [Submonoid.fg_iff]

Premises used: Submonoid.fg_iff
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
S : Finset G
⊢ ∃ (S_1 : Set G), Eq (α := Submonoid G) (Submonoid.closure S_1) (toSubmonoid (closure (↑S : Set G))) ∧ S_1.Finite

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

Premises used: Set.Finite.union, Inv.inv, SetLike.coe, Set.Finite.inv, And.intro, Exists.intro, Finset.finite_toSet, Union.union
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
S : Finset G
mp : Eq (α := Submonoid G) (Submonoid.closure ((↑S : Set G) ∪ (↑S : Set G)⁻¹)) (toSubmonoid (closure (↑S : Set G)))
⊢ ∃ (S_1 : Set G), Eq (α := Submonoid G) (Submonoid.closure S_1) (toSubmonoid (closure (↑S : Set G))) ∧ S_1.Finite

Tactic:
refine ⟨S ∪ S⁻¹, ?_, S.finite_toSet.union S.finite_toSet.inv⟩
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
S : Finset G
⊢ Eq (α := Submonoid G) (Submonoid.closure ((↑S : Set G) ∪ (↑S : Set G)⁻¹)) (toSubmonoid (closure (↑S : Set G)))

Tactic:
(Subgroup.closure_toSubmonoid _).symm

Premises used: Subgroup.closure_toSubmonoid, Eq.symm
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
S : Finset G
⊢ Eq (α := Submonoid G) (Submonoid.closure ((↑S : Set G) ∪ (↑S : Set G)⁻¹)) (toSubmonoid (closure (↑S : Set G)))

Tactic:
exact (Subgroup.closure_toSubmonoid _).symm

Premises used: Subgroup.closure_toSubmonoid, Eq.symm
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure (↑S : Set G) = P.toSubmonoid
⊢ P.FG

Tactic:
⟨S, le_antisymm ?_ ?_⟩

Premises used: le_antisymm, Subgroup.FG, Exists.intro
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure (↑S : Set G) = P.toSubmonoid
mpr : closure (↑S : Set G) ≤ P
mpr₁ : P ≤ closure (↑S : Set G)
⊢ P.FG

Tactic:
refine ⟨S, le_antisymm ?_ ?_⟩
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure (↑S : Set G) = P.toSubmonoid
mpr : (↑S : Set G) ⊆ (↑(Submonoid.closure (↑S : Set G)) : Set G)
⊢ closure (↑S : Set G) ≤ P

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

Premises used: Subgroup.closure_le, Subgroup.coe_toSubmonoid
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure (↑S : Set G) = P.toSubmonoid
⊢ (↑S : Set G) ⊆ (↑(Submonoid.closure (↑S : Set G)) : Set G)

Tactic:
Submonoid.subset_closure

Premises used: Submonoid.subset_closure
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure (↑S : Set G) = P.toSubmonoid
⊢ (↑S : Set G) ⊆ (↑(Submonoid.closure (↑S : Set G)) : Set G)

Tactic:
exact Submonoid.subset_closure

Premises used: Submonoid.subset_closure
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure (↑S : Set G) = P.toSubmonoid
mpr : (↑S : Set G) ⊆ (↑(toSubmonoid (closure (↑S : Set G))) : Set G)
⊢ P ≤ closure (↑S : Set G)

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

Premises used: Subgroup.toSubmonoid_le, Submonoid.closure_le
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure (↑S : Set G) = P.toSubmonoid
⊢ (↑S : Set G) ⊆ (↑(toSubmonoid (closure (↑S : Set G))) : Set G)

Tactic:
Subgroup.subset_closure

Premises used: Subgroup.subset_closure
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure (↑S : Set G) = P.toSubmonoid
⊢ (↑S : Set G) ⊆ (↑(toSubmonoid (closure (↑S : Set G))) : Set G)

Tactic:
exact Subgroup.subset_closure

Premises used: Subgroup.subset_closure
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
P : Subgroup G
rw :
  P.FG ↔
    AddSubmonoid.FG.{u_3} (M := Additive G)
      (AddSubgroup.toAddSubmonoid ((toAddSubgroup : (a : Subgroup G) → AddSubgroup (Additive G)) P))
⊢ P.FG ↔ AddSubgroup.FG.{u_3} (G := Additive G) ((toAddSubgroup : (a : Subgroup G) → AddSubgroup (Additive G)) P)

Tactic:
rw [Subgroup.fg_iff_submonoid_fg, AddSubgroup.fg_iff_addSubmonoid_fg]

Premises used: Subgroup.fg_iff_submonoid_fg, AddSubgroup.fg_iff_addSubmonoid_fg
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
P : Subgroup G
⊢ P.FG ↔
    AddSubmonoid.FG.{u_3} (M := Additive G)
      (AddSubgroup.toAddSubmonoid ((toAddSubgroup : (a : Subgroup G) → AddSubgroup (Additive G)) P))

Tactic:
(Subgroup.toSubmonoid P).fg_iff_add_fg

Premises used: Submonoid.fg_iff_add_fg, Subgroup.toSubmonoid
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
P : Subgroup G
⊢ P.FG ↔
    AddSubmonoid.FG.{u_3} (M := Additive G)
      (AddSubgroup.toAddSubmonoid ((toAddSubgroup : (a : Subgroup G) → AddSubgroup (Additive G)) P))

Tactic:
exact (Subgroup.toSubmonoid P).fg_iff_add_fg

Premises used: Submonoid.fg_iff_add_fg, Subgroup.toSubmonoid
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
H : Type u_4
inst : AddGroup H
P : AddSubgroup H
rw :
  P.FG ↔
    Submonoid.FG.{u_4} (M := Multiplicative H)
      (Subgroup.toSubmonoid ((toSubgroup : (a : AddSubgroup H) → Subgroup (Multiplicative H)) P))
⊢ P.FG ↔ Subgroup.FG.{u_4} (G := Multiplicative H) ((toSubgroup : (a : AddSubgroup H) → Subgroup (Multiplicative H)) P)

Tactic:
rw [AddSubgroup.fg_iff_addSubmonoid_fg, Subgroup.fg_iff_submonoid_fg]

Premises used: Subgroup.fg_iff_submonoid_fg, AddSubgroup.fg_iff_addSubmonoid_fg
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
H : Type u_4
inst : AddGroup H
P : AddSubgroup H
⊢ P.FG ↔
    Submonoid.FG.{u_4} (M := Multiplicative H)
      (Subgroup.toSubmonoid ((toSubgroup : (a : AddSubgroup H) → Subgroup (Multiplicative H)) P))

Tactic:
AddSubmonoid.fg_iff_mul_fg (AddSubgroup.toAddSubmonoid P)

Premises used: AddSubgroup.toAddSubmonoid, AddSubmonoid.fg_iff_mul_fg
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
H : Type u_4
inst : AddGroup H
P : AddSubgroup H
⊢ P.FG ↔
    Submonoid.FG.{u_4} (M := Multiplicative H)
      (Subgroup.toSubmonoid ((toSubgroup : (a : AddSubgroup H) → Subgroup (Multiplicative H)) P))

Tactic:
exact AddSubmonoid.fg_iff_mul_fg (AddSubgroup.toAddSubmonoid P)

Premises used: AddSubgroup.toAddSubmonoid, AddSubmonoid.fg_iff_mul_fg
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
⊢ Eq (α := Subgroup G) (closure (↑∅ : Set G)) ⊥

Tactic:
simp
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
P Q : Subgroup G
hP : P.FG
hQ : Q.FG
rcases : ∀ (s : Finset G), (closure (↑s : Set G) ⊔ Q).FG
⊢ (P ⊔ Q).FG

Tactic:
rcases hP with ⟨s, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
Q : Subgroup G
hQ : Q.FG
s : Finset G
rcases : ∀ (t : Finset G), FG (closure (↑s : Set G) ⊔ closure (↑t : Set G))
⊢ (closure (↑s : Set G) ⊔ Q).FG

Tactic:
rcases hQ with ⟨t, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
s t : Finset G
⊢ Eq (α := Subgroup G) (closure (↑(s ∪ t) : Set G)) (closure (↑s : Set G) ⊔ closure (↑t : Set G))

Tactic:
simp [closure_union]

Premises used: Subgroup.closure_union
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
s t : Finset G
⊢ FG (closure (↑s : Set G) ⊔ closure (↑t : Set G))

Tactic:
exact ⟨s ∪ t, by simp [closure_union]⟩
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
P Q : Subgroup G
hP : P.FG
hQ : Q.FG
rcases : ∀ (s : Finset G), (closure (↑s : Set G) ⊔ Q).FG
rcases₁ : ∀ (s t : Finset G), FG (closure (↑s : Set G) ⊔ closure (↑t : Set G))
⊢ (P ⊔ Q).FG

Tactic:
classical
  rcases hP with ⟨s, rfl⟩
  rcases hQ with ⟨t, rfl⟩
  exact ⟨s ∪ t, by simp [closure_union]⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
ι : Type u_5
s : Finset ι
P : ι → Subgroup G
hP : ∀ i ∈ s, (P i).FG
⊢ (s.sup P).FG

Tactic:
Finset.sup_induction bot (fun _ ha _ hb => ha.sup hb) hP

Premises used: Finset.sup_induction, Subgroup.FG.sup, Subgroup.FG.bot
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
ι : Type u_5
s : Finset ι
P : ι → Subgroup G
hP : ∀ i ∈ s, (P i).FG
⊢ FG.{u_3} (G := G) (⨆ i ∈ s, P i)

Tactic:
simpa only [Finset.sup_eq_iSup] using finset_sup s P hP

Premises used: Subgroup.FG.finset_sup, Finset.sup_eq_iSup
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
ι : Type u_5
s : Set ι
hs : s.Finite
P : ι → Subgroup G
hP : ∀ i ∈ s, (P i).FG
⊢ ∀ i ∈ hs.toFinset (s := s), (P i).FG

Tactic:
simpa
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
ι : Type u_5
s : Set ι
hs : s.Finite
P : ι → Subgroup G
hP : ∀ i ∈ s, (P i).FG
⊢ FG.{u_3} (G := G) (⨆ i ∈ s, P i)

Tactic:
simpa using biSup_finset hs.toFinset P (by simpa)

Premises used: Subgroup.FG.biSup_finset, Set.Finite.toFinset
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
ι : Sort u_5
inst_1 : Finite ι
P : ι → Subgroup G
hP : ∀ (i : ι), (P i).FG
⊢ (_root_.iSup P).FG

Tactic:
simpa [iSup_plift_down] using biSup Set.finite_univ (P ∘ PLift.down) fun i _ => hP i.down

Premises used: Subgroup.FG.biSup, iSup_plift_down, Function.comp, PLift.down, Set.finite_univ
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
G' : Type u_5
inst_1 : Group G'
P : Subgroup G
Q : Subgroup G'
hP : P.FG
hQ : Q.FG
rw : ∀ (hP : P.FG) (hQ : Q.FG), (P.prod Q).FG
⊢ (P.prod Q).FG

Tactic:
rw [fg_iff_submonoid_fg] at *

Premises used: Subgroup.fg_iff_submonoid_fg
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
G' : Type u_5
inst_1 : Group G'
P : Subgroup G
Q : Subgroup G'
hP : P.FG
hQ : Q.FG
⊢ (P.prod Q).FG

Tactic:
hP.prod hQ

Premises used: Submonoid.FG.prod, Submonoid.prod
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
G' : Type u_5
inst_1 : Group G'
P : Subgroup G
Q : Subgroup G'
hP : P.FG
hQ : Q.FG
⊢ (P.prod Q).FG

Tactic:
exact hP.prod hQ

Premises used: Submonoid.FG.prod
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
ι : Type u_5
inst : Finite ι
G : ι → Type u_6
inst_1 : (i : ι) → Group (G i)
P : (i : ι) → Subgroup (G i)
hP : ∀ (i : ι), (P i).FG
simp_rw : ∀ (hP : ∀ (i : ι), (P i).FG), (Subgroup.pi (f := G) Set.univ P).FG
⊢ (Subgroup.pi (f := G) Set.univ P).FG

Tactic:
simp_rw [fg_iff_submonoid_fg] at *

Premises used: Subgroup.fg_iff_submonoid_fg
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
ι : Type u_5
inst : Finite ι
G : ι → Type u_6
inst_1 : (i : ι) → Group (G i)
P : (i : ι) → Subgroup (G i)
hP : ∀ (i : ι), (P i).FG
⊢ (Subgroup.pi (f := G) Set.univ P).FG

Tactic:
.pi hP

Premises used: Submonoid.pi, Submonoid.FG.pi
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
ι : Type u_5
inst : Finite ι
G : ι → Type u_6
inst_1 : (i : ι) → Group (G i)
P : (i : ι) → Subgroup (G i)
hP : ∀ (i : ι), (P i).FG
⊢ (Subgroup.pi (f := G) Set.univ P).FG

Tactic:
exact .pi hP
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
⊢ FG G ↔ Subgroup.FG.{u_3} (G := G) ⊤

Tactic:
⟨fun h => h.1, fun h => ⟨h⟩⟩

Premises used: Iff.intro, Group.FG.mk, Group.FG.out
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
H : Type u_4
inst : AddGroup H
⊢ FG H ↔ AddSubgroup.FG.{u_4} (G := H) ⊤

Tactic:
⟨fun h => h.1, fun h => ⟨h⟩⟩

Premises used: AddGroup.FG.mk, AddGroup.FG.out, Iff.intro
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
⊢ FG G ↔ ∃ (S : Set G), Eq (α := Subgroup G) (Subgroup.closure S) ⊤ ∧ S.Finite

Tactic:
⟨fun h => (Subgroup.fg_iff ⊤).1 h.out, fun h => ⟨(Subgroup.fg_iff ⊤).2 h⟩⟩

Premises used: Iff.mpr, Subgroup.fg_iff, Iff.intro, Group.FG.mk, Iff.mp, Group.FG.out, Top.top
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
⊢ FG G ↔ ∃ (n : ℕ) (S : Finset G), S.card = n ∧ Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤

Tactic:
Group.fg_def.trans ⟨fun ⟨S, hS⟩ => ⟨S.card, S, rfl, hS⟩, fun ⟨_n, S, _hn, hS⟩ => ⟨S, hS⟩⟩

Premises used: Subgroup.closure, Group.fg_def, Exists, _private.0.Group.fg_iff'.match_1, And, SetLike.coe, Subgroup.FG, And.intro, Iff.intro, Exists.intro, Finset.card, Iff.trans, Top.top, Eq, rfl, _private.0.Group.fg_iff'.match_2