awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
⊢ FG G ↔ Monoid.FG G

Tactic:
⟨fun h => Monoid.fg_def.2 <| (Subgroup.fg_iff_submonoid_fg ⊤).1 (Group.fg_def.1 h), fun h =>
    Group.fg_def.2 <| (Subgroup.fg_iff_submonoid_fg ⊤).2 (Monoid.fg_def.1 h)⟩

Premises used: Iff.mpr, Group.fg_def, Subgroup.fg_iff_submonoid_fg, Iff.intro, Iff.mp, Top.top, Monoid.fg_def
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
inst_3 : Group.FG G
⊢ FG G

Tactic:
Group.fg_iff_monoid_fg.1 ‹_›

Premises used: Group.fg_iff_monoid_fg, Iff.mp
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
H : Subgroup G
⊢ FG.{u_3} ↥H ↔ H.FG

Tactic:
(fg_iff_monoid_fg.trans (Monoid.fg_iff_submonoid_fg _)).trans
    (Subgroup.fg_iff_submonoid_fg _).symm

Premises used: Subgroup.fg_iff_submonoid_fg, Group.fg_iff_monoid_fg, Iff.trans, Iff.symm
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
⊢ Group.FG G ↔ AddGroup.FG.{u_3} (Additive G)

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

Premises used: Iff.mpr, Subgroup.fg_iff_add_fg, AddGroup.FG.mk, AddGroup.FG.out, Iff.intro, Group.FG.mk, Iff.mp, Group.FG.out, Top.top
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
H : Type u_4
inst : AddGroup H
⊢ FG H ↔ Group.FG.{u_4} (Multiplicative H)

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

Premises used: Iff.mpr, AddGroup.FG.mk, AddGroup.FG.out, Iff.intro, Group.FG.mk, Iff.mp, AddSubgroup.fg_iff_mul_fg, Group.FG.out, Top.top
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
inst_3 : Group.FG G
⊢ FG.{u_3} (Additive G)

Tactic:
GroupFG.iff_add_fg.1 ‹_›

Premises used: GroupFG.iff_add_fg, Iff.mp
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
inst_3 : AddGroup.FG H
⊢ FG.{u_4} (Multiplicative H)

Tactic:
AddGroup.fg_iff_mul_fg.1 ‹_›

Premises used: AddGroup.fg_iff_mul_fg, Iff.mp
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
inst_3 : Finite G
intro : ∀ (val : Fintype G), FG G
⊢ FG G

Tactic:
cases nonempty_fintype G

Premises used: nonempty_fintype
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
inst_3 : Finite G
val : Fintype G
rw : Eq.{u_3 + 1} (α := Subgroup G) (Subgroup.closure Set.univ) ⊤
⊢ Eq (α := Subgroup G) (Subgroup.closure (↑Finset.univ : Set G)) ⊤

Tactic:
rw [Finset.coe_univ]

Premises used: Finset.coe_univ
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
inst_3 : Finite G
val : Fintype G
⊢ Eq.{u_3 + 1} (α := Subgroup G) (Subgroup.closure Set.univ) ⊤

Tactic:
Subgroup.closure_univ

Premises used: Subgroup.closure_univ
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
inst_3 : Finite G
val : Fintype G
⊢ Eq.{u_3 + 1} (α := Subgroup G) (Subgroup.closure Set.univ) ⊤

Tactic:
exact Subgroup.closure_univ

Premises used: Subgroup.closure_univ
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
inst_3 : Finite G
val : Fintype G
⊢ FG G

Tactic:
exact ⟨⟨Finset.univ, by rw [Finset.coe_univ]; exact Subgroup.closure_univ⟩⟩
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
G' : Type u_5
inst_1 : Group G'
hG : FG G
f : G →* G'
hf : Function.Surjective.{u_3 + 1, u_5 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
⊢ FG G'

Tactic:
Group.fg_iff_monoid_fg.mpr <|
    @Monoid.fg_of_surjective G _ G' _ (Group.fg_iff_monoid_fg.mp hG) f hf

Premises used: Iff.mpr, Group.fg_iff_monoid_fg, Monoid.fg_of_surjective
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
α : Type u_5
inst_3 : Finite α
⊢ Group.FG.{u_5} (FreeGroup α)

Tactic:
Group.fg_iff.mpr ⟨Set.range of, closure_range_of α, Set.finite_range of⟩

Premises used: Iff.mpr, FreeGroup.of, FreeGroup.closure_range_of, Set.finite_range, Group.fg_iff, And.intro, Exists.intro, Set.range
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
⊢ FG G ↔
    ∃ (S : Set G) (_ : S.Finite) (φ : FreeGroup (↑S : Type u_3) →* G),
      Function.Surjective (α := FreeGroup (↑S : Type u_3)) (β := G) (⇑φ : (a : FreeGroup (↑S : Type u_3)) → G)

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

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

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

Tactic:
rwa [← MonoidHom.range_eq_top, ← FreeGroup.closure_eq_range]

Premises used: FreeGroup.closure_eq_range, MonoidHom.range_eq_top
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
S : Set G
hfin : Finite.{u_3 + 1} (↑S : Type u_3)
φ : FreeGroup (↑S : Type u_3) →* G
hφ : Function.Surjective (α := FreeGroup (↑S : Type u_3)) (β := G) (⇑φ : (a : FreeGroup (↑S : Type u_3)) → G)
⊢ FG G

Tactic:
Group.fg_of_surjective hφ

Premises used: Group.fg_of_surjective
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
S : Set G
hfin : Finite.{u_3 + 1} (↑S : Type u_3)
φ : FreeGroup (↑S : Type u_3) →* G
hφ : Function.Surjective (α := FreeGroup (↑S : Type u_3)) (β := G) (⇑φ : (a : FreeGroup (↑S : Type u_3)) → G)
⊢ FG G

Tactic:
exact Group.fg_of_surjective hφ

Premises used: Group.fg_of_surjective
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
mp :
  FG G →
    ∃ (α : Type) (_ : Finite α) (φ : FreeGroup α →* G),
      Function.Surjective (α := FreeGroup α) (β := G) (⇑φ : (a : FreeGroup α) → G)
mpr :
  (∃ (α : Type) (_ : Finite α) (φ : FreeGroup α →* G),
      Function.Surjective (α := FreeGroup α) (β := G) (⇑φ : (a : FreeGroup α) → G)) →
    FG G
⊢ FG G ↔
    ∃ (α : Type) (_ : Finite α) (φ : FreeGroup α →* G),
      Function.Surjective (α := FreeGroup α) (β := G) (⇑φ : (a : FreeGroup α) → G)

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

Tactic:
rw [fg_iff_exists_freeGroup_hom_surjective]

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

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

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

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

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

Tactic:
exact ⟨Fin n, inferInstance, φ.comp (FreeGroup.freeGroupCongr e).symm,
      hφ.comp (FreeGroup.freeGroupCongr e).symm.surjective⟩
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
α : Type
w : Finite α
φ : FreeGroup α →* G
hφ : Function.Surjective (α := FreeGroup α) (β := G) (⇑φ : (a : FreeGroup α) → G)
⊢ FG G

Tactic:
Group.fg_of_surjective hφ

Premises used: Group.fg_of_surjective
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
G : Type u_3
inst : Group G
α : Type
w : Finite α
φ : FreeGroup α →* G
hφ : Function.Surjective (α := FreeGroup α) (β := G) (⇑φ : (a : FreeGroup α) → G)
⊢ FG G

Tactic:
exact Group.fg_of_surjective hφ

Premises used: Group.fg_of_surjective
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
G' : Type u_5
inst_3 : Group G'
inst_4 : FG G
f : G →* G'
⊢ FG.{u_5} ↥f.range

Tactic:
Group.fg_of_surjective f.rangeRestrict_surjective

Premises used: Group.fg_of_surjective, MonoidHom.rangeRestrict_surjective
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
s : Finset G
⊢ FG.{u_3} ↥(Subgroup.closure (↑s : Set G))

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

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

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
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
s : Finset G
rw :
  Eq (α := Subgroup ↥(Subgroup.closure (↑s : Set G)))
    (Subgroup.closure
      (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (Subgroup.closure (↑s : Set G)) x) ⁻¹'
        (↑s : Set G)))
    ⊤
rw₁ :
  Eq (α := Subgroup ↥(Subgroup.closure (↑s : Set G)))
    (Subgroup.closure
      ((⇑(Subgroup.subtype (Subgroup.closure (↑s : Set G))) : (a : ↥(Subgroup.closure (↑s : Set G))) → G) ⁻¹'
        (↑s : Set G)))
    ⊤
rw₂ rw₃ : Eq.{u_3 + 1} (α := Subgroup ↥(Subgroup.closure (↑s : Set G))) ⊤ ⊤
⊢ Eq (α := Subgroup ↥(Subgroup.closure (↑s : Set G)))
    (Subgroup.closure
      (↑(s.preimage
            (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (Subgroup.closure (↑s : Set G)) x)) ⋯) :
        Set ↥(Subgroup.closure (↑s : Set G))))
    ⊤

Tactic:
rw [Finset.coe_preimage, ← Subgroup.coe_subtype, Subgroup.closure_preimage_eq_top]

Premises used: Subgroup.coe_subtype, Finset.coe_preimage, Subgroup.closure_preimage_eq_top
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
s : Set G
inst_3 : Finite.{u_3 + 1} (↑s : Type u_3)
⊢ FG.{u_3} ↥(Subgroup.closure s)

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

Premises used: Eq.rec, Set.toFinset, Group.closure_finset_fg, Set.coe_toFinset
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N_1 : Type u_2
inst : Monoid M
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
inst_3 : Group.FG G
N : Subgroup G
inst_4 : N.Normal
⊢ Group.FG.{u_3} (G ⧸ N)

Tactic:
Group.fg_of_surjective <| QuotientGroup.mk'_surjective N

Premises used: Group.fg_of_surjective, QuotientGroup.mk'_surjective
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
inst_3 : Monoid N
G' : Type u_5
inst_4 : Group G'
inst_5 : FG M
inst_6 : FG N
rw : Submonoid.FG (M := M × N) (Submonoid.prod ⊤ ⊤)
⊢ Submonoid.FG (M := M × N) ⊤

Tactic:
rw [← Submonoid.top_prod_top]

Premises used: Submonoid.top_prod_top
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
inst_3 : Monoid N
G' : Type u_5
inst_4 : Group G'
inst_5 : FG M
inst_6 : FG N
⊢ Submonoid.FG (M := M × N) (Submonoid.prod ⊤ ⊤)

Tactic:
‹FG M›.fg_top.prod ‹FG N›.fg_top

Premises used: Monoid.FG.fg_top, Submonoid.FG.prod
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
inst_3 : Monoid N
G' : Type u_5
inst_4 : Group G'
inst_5 : FG M
inst_6 : FG N
⊢ Submonoid.FG (M := M × N) (Submonoid.prod ⊤ ⊤)

Tactic:
exact ‹FG M›.fg_top.prod ‹FG N›.fg_top

Premises used: Monoid.FG.fg_top, Submonoid.FG.prod
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
inst_3 : Monoid N
G' : Type u_5
inst_4 : Group G'
inst_5 : FG G
inst_6 : FG G'
rw : Subgroup.FG (G := G × G') (Subgroup.prod ⊤ ⊤)
⊢ Subgroup.FG (G := G × G') ⊤

Tactic:
rw [← Subgroup.top_prod_top]

Premises used: Subgroup.top_prod_top
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
inst_3 : Monoid N
G' : Type u_5
inst_4 : Group G'
inst_5 : FG G
inst_6 : FG G'
⊢ Subgroup.FG (G := G × G') (Subgroup.prod ⊤ ⊤)

Tactic:
‹FG G›.out.prod ‹FG G'›.out

Premises used: Subgroup.FG.prod, Group.FG.out
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
inst_3 : Monoid N
G' : Type u_5
inst_4 : Group G'
inst_5 : FG G
inst_6 : FG G'
⊢ Subgroup.FG (G := G × G') (Subgroup.prod ⊤ ⊤)

Tactic:
exact ‹FG G›.out.prod ‹FG G'›.out

Premises used: Subgroup.FG.prod, Group.FG.out
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M_1 : Type u_1
N : Type u_2
inst : Monoid M_1
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
ι : Type u_5
inst_3 : Finite ι
M : ι → Type u_6
inst_4 : (i : ι) → Monoid (M i)
inst_5 : ∀ (i : ι), Monoid.FG.{u_6} (M i)
rw : Submonoid.FG (M := (i : ι) → M i) (Submonoid.pi (M := M) Set.univ fun (i : ι) ↦ ⊤)
⊢ Submonoid.FG (M := (i : ι) → M i) ⊤

Tactic:
rw [← Submonoid.pi_top Set.univ]

Premises used: Submonoid.pi_top, Set.univ
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M_1 : Type u_1
N : Type u_2
inst : Monoid M_1
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
ι : Type u_5
inst_3 : Finite ι
M : ι → Type u_6
inst_4 : (i : ι) → Monoid (M i)
inst_5 : ∀ (i : ι), Monoid.FG.{u_6} (M i)
⊢ Submonoid.FG (M := (i : ι) → M i) (Submonoid.pi (M := M) Set.univ fun (i : ι) ↦ ⊤)

Tactic:
.pi fun i => Monoid.FG.fg_top

Premises used: Monoid.FG.fg_top, Submonoid.FG.pi
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M_1 : Type u_1
N : Type u_2
inst : Monoid M_1
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
ι : Type u_5
inst_3 : Finite ι
M : ι → Type u_6
inst_4 : (i : ι) → Monoid (M i)
inst_5 : ∀ (i : ι), Monoid.FG.{u_6} (M i)
⊢ Submonoid.FG (M := (i : ι) → M i) (Submonoid.pi (M := M) Set.univ fun (i : ι) ↦ ⊤)

Tactic:
exact .pi fun i => Monoid.FG.fg_top
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
G_1 : Type u_3
H : Type u_4
inst_1 : Group G_1
inst_2 : AddGroup H
ι : Type u_5
inst_3 : Finite ι
G : ι → Type u_6
inst_4 : (i : ι) → Group (G i)
inst_5 : ∀ (i : ι), Group.FG.{u_6} (G i)
rw : Subgroup.FG (G := (i : ι) → G i) (Subgroup.pi (f := G) Set.univ fun (i : ι) ↦ ⊤)
⊢ Subgroup.FG (G := (i : ι) → G i) ⊤

Tactic:
rw [← Subgroup.pi_top Set.univ]

Premises used: Subgroup.pi_top, Set.univ
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
G_1 : Type u_3
H : Type u_4
inst_1 : Group G_1
inst_2 : AddGroup H
ι : Type u_5
inst_3 : Finite ι
G : ι → Type u_6
inst_4 : (i : ι) → Group (G i)
inst_5 : ∀ (i : ι), Group.FG.{u_6} (G i)
⊢ Subgroup.FG (G := (i : ι) → G i) (Subgroup.pi (f := G) Set.univ fun (i : ι) ↦ ⊤)

Tactic:
.pi fun i => Group.FG.out

Premises used: Subgroup.FG.pi, Group.FG.out
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
G_1 : Type u_3
H : Type u_4
inst_1 : Group G_1
inst_2 : AddGroup H
ι : Type u_5
inst_3 : Finite ι
G : ι → Type u_6
inst_4 : (i : ι) → Group (G i)
inst_5 : ∀ (i : ι), Group.FG.{u_6} (G i)
⊢ Subgroup.FG (G := (i : ι) → G i) (Subgroup.pi (f := G) Set.univ fun (i : ι) ↦ ⊤)

Tactic:
exact .pi fun i => Group.FG.out
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
⊢ Eq (α := AddSubmonoid ℕ) (AddSubmonoid.closure (↑{1} : Set ℕ)) ⊤

Tactic:
simp
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
G : Type u_3
H : Type u_4
inst_1 : Group G
inst_2 : AddGroup H
⊢ Eq (α := AddSubgroup ℤ) (AddSubgroup.closure (↑{1} : Set ℤ)) ⊤

Tactic:
simp
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelMonoid M
inst_4 : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
⊢ Set.IsPWO.{u_5} (α := M) {x : M | x ∈ P ∧ x ≠ 1}

Tactic:
have hpwo := Set.isPWO_of_wellQuasiOrderedLE { x | x ∈ P ∧ x ≠ 1 }
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelMonoid M
inst_4 : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : Set.IsPWO.{u_5} (α := M) {x : M | x ∈ P ∧ x ≠ 1}
rw : ∃ (S : Set M), closure S = P ∧ S.Finite
⊢ P.FG

Tactic:
rw [fg_iff]

Premises used: Submonoid.fg_iff
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelMonoid M
inst_4 : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : Set.IsPWO.{u_5} (α := M) {x : M | x ∈ P ∧ x ≠ 1}
⊢ ∃ (S : Set M), closure S = P ∧ S.Finite

Tactic:
⟨_, ?_, (setOf_minimal_antichain _).finite_of_partiallyWellOrderedOn
    (hpwo.mono (setOf_minimal_subset _))⟩

Premises used: setOf_minimal_subset, And.intro, Exists.intro, setOf_minimal_antichain, IsAntichain.finite_of_partiallyWellOrderedOn, Set.IsPWO.mono
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelMonoid M
inst_4 : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : Set.IsPWO.{u_5} (α := M) {x : M | x ∈ P ∧ x ≠ 1}
refine : closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x} = P
⊢ ∃ (S : Set M), closure S = P ∧ S.Finite

Tactic:
refine ⟨_, ?_, (setOf_minimal_antichain _).finite_of_partiallyWellOrderedOn
    (hpwo.mono (setOf_minimal_subset _))⟩
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelMonoid M
inst_4 : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : Set.IsPWO.{u_5} (α := M) {x : M | x ∈ P ∧ x ≠ 1}
h :
  ∀ (x : M),
    Membership.mem (γ := Submonoid M)
        (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) x ↔
      x ∈ P
⊢ closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x} = P

Tactic:
ext x
-- Module: Mathlib.GroupTheory.Finiteness
Goal:
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelMonoid M
inst_4 : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : Set.IsPWO.{u_5} (α := M) {x : M | x ∈ P ∧ x ≠ 1}
x : M
h :
  Membership.mem (γ := Submonoid M)
      (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) x →
    x ∈ P
h₁ :
  x ∈ P →
    Membership.mem (γ := Submonoid M)
      (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) x
⊢ Membership.mem (γ := Submonoid M)
      (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) x ↔
    x ∈ P

Tactic:
constructor