awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
G : Type u_3
inst : Group G
S : Finset G
⊢ Submonoid.FG (toSubmonoid (closure (↑S : Set G)))
have mp : ∃ (S_1 : Set G), Eq (α := Submonoid G) (Submonoid.closure S_1) (toSubmonoid (closure (↑S : Set G))) ∧ S_1.Finite
Tactic: rw [Submonoid.fg_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
have mp : Eq (α := Submonoid G) (Submonoid.closure ((↑S : Set G) ∪ (↑S : Set G)⁻¹)) (toSubmonoid (closure (↑S : Set G)))
Tactic: refine ⟨S ∪ S⁻¹, ?_, S.finite_toSet.union S.finite_toSet.inv⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
G : Type u_3
inst : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure (↑S : Set G) = P.toSubmonoid
⊢ P.FG
have mpr : closure (↑S : Set G) ≤ P
Tactic: refine ⟨S, le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
⊢ P.FG
have mpr₁ : P ≤ closure (↑S : Set G)
Tactic: refine ⟨S, le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
G : Type u_3
inst : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure (↑S : Set G) = P.toSubmonoid
⊢ closure (↑S : Set G) ≤ P
have mpr : (↑S : Set G) ⊆ (↑(Submonoid.closure (↑S : Set G)) : Set G)
Tactic: rw [Subgroup.closure_le, ← Subgroup.coe_toSubmonoid, ← hS]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
G : Type u_3
inst : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure (↑S : Set G) = P.toSubmonoid
⊢ P ≤ closure (↑S : Set G)
have mpr : (↑S : Set G) ⊆ (↑(toSubmonoid (closure (↑S : Set G))) : Set G)
Tactic: rw [← Subgroup.toSubmonoid_le, ← hS, Submonoid.closure_le]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
G : Type u_3
inst : Group G
P : Subgroup G
⊢ P.FG ↔ AddSubgroup.FG.{u_3} (G := Additive G) ((toAddSubgroup : (a : Subgroup G) → AddSubgroup (Additive G)) P)
have rw : P.FG ↔
  AddSubmonoid.FG.{u_3} (M := Additive G)
    (AddSubgroup.toAddSubmonoid ((toAddSubgroup : (a : Subgroup G) → AddSubgroup (Additive G)) P))
Tactic: rw [Subgroup.fg_iff_submonoid_fg, AddSubgroup.fg_iff_addSubmonoid_fg]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
H : Type u_4
inst : AddGroup H
P : AddSubgroup H
⊢ P.FG ↔ Subgroup.FG.{u_4} (G := Multiplicative H) ((toSubgroup : (a : AddSubgroup H) → Subgroup (Multiplicative H)) P)
have rw : P.FG ↔
  Submonoid.FG.{u_4} (M := Multiplicative H)
    (Subgroup.toSubmonoid ((toSubgroup : (a : AddSubgroup H) → Subgroup (Multiplicative H)) P))
Tactic: rw [AddSubgroup.fg_iff_addSubmonoid_fg, Subgroup.fg_iff_submonoid_fg]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
G : Type u_3
inst : Group G
P Q : Subgroup G
hP : P.FG
hQ : Q.FG
⊢ (P ⊔ Q).FG
have rcases : ∀ (s : Finset G), (closure (↑s : Set G) ⊔ Q).FG
Tactic: rcases hP with ⟨s, rfl⟩
Cleared hypotheses: P, hP
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
G : Type u_3
inst : Group G
Q : Subgroup G
hQ : Q.FG
s : Finset G
⊢ (closure (↑s : Set G) ⊔ Q).FG
have rcases : ∀ (t : Finset G), FG (closure (↑s : Set G) ⊔ closure (↑t : Set G))
Tactic: rcases hQ with ⟨t, rfl⟩
Cleared hypotheses: Q, hQ
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
G : Type u_3
inst : Group G
P Q : Subgroup G
hP : P.FG
hQ : Q.FG
⊢ (P ⊔ Q).FG
have rcases : ∀ (s : Finset G), (closure (↑s : Set G) ⊔ Q).FG
Tactic: classical
  rcases hP with ⟨s, rfl⟩
  rcases hQ with ⟨t, rfl⟩
  exact ⟨s ∪ t, by simp [closure_union]⟩
Cleared hypotheses: P, hP
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
have rcases₁ : ∀ (s t : Finset G), FG (closure (↑s : Set G) ⊔ closure (↑t : Set G))
Tactic: classical
  rcases hP with ⟨s, rfl⟩
  rcases hQ with ⟨t, rfl⟩
  exact ⟨s ∪ t, by simp [closure_union]⟩
Cleared hypotheses: P, Q, hP, hQ
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
have rw : ∀ (hP : P.FG) (hQ : Q.FG), (P.prod Q).FG
Tactic: rw [fg_iff_submonoid_fg] at *
Cleared hypotheses: hP, hQ
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
have simp_rw : ∀ (hP : ∀ (i : ι), (P i).FG), (Subgroup.pi (f := G) Set.univ P).FG
Tactic: simp_rw [fg_iff_submonoid_fg] at *
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
⊢ FG G
have intro : ∀ (val : Fintype G), FG G
Tactic: cases nonempty_fintype G
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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 (α := Subgroup G) (Subgroup.closure (↑Finset.univ : Set G)) ⊤
have rw : Eq.{u_3 + 1} (α := Subgroup G) (Subgroup.closure Set.univ) ⊤
Tactic: rw [Finset.coe_univ]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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)
have 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)
Tactic: refine ⟨fun ⟨S, hS⟩ ↦ ⟨S, S.finite_toSet, FreeGroup.lift Subtype.val, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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)
⊢ 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)
have 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
Tactic: refine ⟨fun ⟨S, hS⟩ ↦ ⟨S, S.finite_toSet, FreeGroup.lift Subtype.val, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
G : Type u_3
inst : Group G
h : 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)
have 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)))))
  ⊤
Tactic: rwa [← MonoidHom.range_eq_top, ← FreeGroup.closure_eq_range]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
G : Type u_3
inst : Group G
⊢ FG G ↔
    ∃ (α : Type) (_ : Finite α) (φ : FreeGroup α →* G),
      Function.Surjective (α := FreeGroup α) (β := G) (⇑φ : (a : FreeGroup α) → G)
have mp : FG G →
  ∃ (α : Type) (_ : Finite α) (φ : FreeGroup α →* G),
    Function.Surjective (α := FreeGroup α) (β := G) (⇑φ : (a : FreeGroup α) → G)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
G : Type u_3
inst : Group G
mp :
  FG 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)
have mpr : (∃ (α : Type) (_ : Finite α) (φ : FreeGroup α →* G),
    Function.Surjective (α := FreeGroup α) (β := G) (⇑φ : (a : FreeGroup α) → G)) →
  FG G
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
G : Type u_3
inst : Group G
⊢ FG G →
    ∃ (α : Type) (_ : Finite α) (φ : FreeGroup α →* G),
      Function.Surjective (α := FreeGroup α) (β := G) (⇑φ : (a : FreeGroup α) → G)
have 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)
Tactic: rw [fg_iff_exists_freeGroup_hom_surjective]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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)
⊢ ∃ (α : Type) (_ : Finite α) (φ : FreeGroup α →* G),
    Function.Surjective (α := FreeGroup α) (β := G) (⇑φ : (a : FreeGroup α) → G)
have mp : ∀ (n : ℕ) (e : (↑S : Type u_3) ≃ Fin n),
  ∃ (α : Type) (_ : Finite α) (φ : FreeGroup α →* G),
    Function.Surjective (α := FreeGroup α) (β := G) (⇑φ : (a : FreeGroup α) → G)
Tactic: obtain ⟨n, ⟨e⟩⟩ := hS.exists_equiv_fin S
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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))
have 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))
          sorry) :
      Set ↥(Subgroup.closure (↑s : Set G))))
  ⊤
Tactic: refine ⟨⟨s.preimage Subtype.val Subtype.coe_injective.injOn, ?_⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
⊢ 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))))
    ⊤
have 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)))
  ⊤
Tactic: rw [Finset.coe_preimage, ← Subgroup.coe_subtype, Subgroup.closure_preimage_eq_top]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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)))
    ⊤
⊢ 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))))
    ⊤
have 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)))
  ⊤
Tactic: rw [Finset.coe_preimage, ← Subgroup.coe_subtype, Subgroup.closure_preimage_eq_top]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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)))
    ⊤
⊢ 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))))
    ⊤
have rw₂ : Eq.{u_3 + 1} (α := Subgroup ↥(Subgroup.closure (↑s : Set G))) ⊤ ⊤
Tactic: rw [Finset.coe_preimage, ← Subgroup.coe_subtype, Subgroup.closure_preimage_eq_top]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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) ⊤
have rw : Submonoid.FG (M := M × N) (Submonoid.prod ⊤ ⊤)
Tactic: rw [← Submonoid.top_prod_top]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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') ⊤
have rw : Subgroup.FG (G := G × G') (Subgroup.prod ⊤ ⊤)
Tactic: rw [← Subgroup.top_prod_top]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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) ⊤
have rw : Submonoid.FG (M := (i : ι) → M i) (Submonoid.pi (M := M) Set.univ fun (i : ι) ↦ ⊤)
Tactic: rw [← Submonoid.pi_top Set.univ]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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) ⊤
have rw : Subgroup.FG (G := (i : ι) → G i) (Subgroup.pi (f := G) Set.univ fun (i : ι) ↦ ⊤)
Tactic: rw [← Subgroup.pi_top Set.univ]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (hypothesis)
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
⊢ P.FG
have hpwo : Set.IsPWO.{u_5} (α := M) {x : M | x ∈ P ∧ x ≠ 1}
Tactic: have hpwo := Set.isPWO_of_wellQuasiOrderedLE { x | x ∈ P ∧ x ≠ 1 }
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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}
⊢ P.FG
have rw : ∃ (S : Set M), closure S = P ∧ S.Finite
Tactic: rw [fg_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
have refine : closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x} = P
Tactic: refine ⟨_, ?_, (setOf_minimal_antichain _).finite_of_partiallyWellOrderedOn
    (hpwo.mono (setOf_minimal_subset _))⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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}
⊢ closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x} = P
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
hx :
  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
have h : Membership.mem (γ := Submonoid M) (closure (↑P : Set M)) x
Tactic: rw [← P.closure_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
hx₁ : 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
have pos : ∀ (hx₂ : x = 1),
  Membership.mem (γ := Submonoid M)
    (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) x
Tactic: by_cases hx₂ : x = 1
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
hx₁ : x ∈ P
pos :
  ∀ (hx₂ : x = 1),
    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
have neg : ∀ (hx₂ : ¬x = 1),
  Membership.mem (γ := Submonoid M)
    (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) x
Tactic: by_cases hx₂ : x = 1
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
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
hx₁ : x ∈ P
hx₂ : ¬x = 1
⊢ Membership.mem (γ := Submonoid M)
    (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) x
have neg : ∀ (y : M),
  Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} y →
    ∀
      (ih :
        ∀ (z : M),
          Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} z →
            z ≤ y ∧ ¬y ≤ z →
              Membership.mem (γ := Submonoid M)
                (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) z)
      (hy₁ : y ∈ P) (hy₂ : y ≠ 1),
      Membership.mem (γ := Submonoid M)
        (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) y
Tactic: refine hpwo.wellFoundedOn.induction ⟨hx₁, hx₂⟩ fun y ⟨hy₁, hy₂⟩ ih => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (hypothesis)
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
hx₁ : x ∈ P
hx₂ : ¬x = 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} y
ih :
  ∀ (z : M),
    Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} z →
      z ≤ y ∧ ¬y ≤ z →
        Membership.mem (γ := Submonoid M)
          (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) z
hy₁ : y ∈ P
hy₂ : y ≠ 1
⊢ Membership.mem (γ := Submonoid M)
    (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) y
have ih₁ : ∀ z ∈ P,
  z ≠ 1 →
    z ≤ y → ¬y ≤ z → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z
Tactic: simp only [Set.mem_setOf_eq, and_imp] at ih
Cleared hypotheses: ih