awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
h : Membership.mem (γ := Submonoid M) (closure (↑P : Set M)) x
⊢ x ∈ P

Tactic:
rw [← P.closure_eq]

Premises used: Submonoid.closure_eq
-- 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
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
⊢ Membership.mem (γ := Submonoid M) (closure (↑P : Set M)) x

Tactic:
closure_mono ((setOf_minimal_subset _).trans fun _ => And.left) hx

Premises used: HasSubset.Subset.trans, Submonoid.closure_mono, And.left, 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}
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
⊢ Membership.mem (γ := Submonoid M) (closure (↑P : Set M)) x

Tactic:
exact closure_mono ((setOf_minimal_subset _).trans fun _ => And.left) hx

Premises used: HasSubset.Subset.trans, Submonoid.closure_mono, And.left, 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}
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
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
⊢ 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
-- 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
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

Tactic:
simp [hx₂]
-- 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
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

Tactic:
hpwo.wellFoundedOn.induction ⟨hx₁, hx₂⟩ fun y ⟨hy₁, hy₂⟩ ih => ?_

Premises used: _private.0.Submonoid.fg_of_divisive.match_1, setOf, Membership.mem, Set.PartiallyWellOrderedOn.wellFoundedOn, Ne, And, Submonoid.closure, And.intro, Set.WellFoundedOn.induction, OfNat.ofNat, Minimal
-- 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
hx₁ : x ∈ P
hx₂ : ¬x = 1
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
⊢ 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:
refine hpwo.wellFoundedOn.induction ⟨hx₁, hx₂⟩ fun y ⟨hy₁, hy₂⟩ ih => ?_

Premises used: Set.PartiallyWellOrderedOn.wellFoundedOn, And.intro, Set.WellFoundedOn.induction
-- 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
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
⊢ ∀ 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

Premises used: and_imp, Set.mem_setOf_eq
-- 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
hx₁ : x ∈ P
hx₂ : ¬x = 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} y
hy₁ : y ∈ P
hy₂ : y ≠ 1
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
pos :
  ∀ (hy₃ : Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) y),
    Membership.mem (γ := Submonoid M)
      (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) y
neg :
  ∀ (hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) y),
    Membership.mem (γ := Submonoid M)
      (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) y
⊢ 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:
by_cases hy₃ : Minimal (· ∈ { x | x ∈ P ∧ x ≠ 1 }) y

Premises used: setOf, Membership.mem, Ne, And, OfNat.ofNat, Minimal
-- 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
hx₁ : x ∈ P
hx₂ : ¬x = 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} y
hy₁ : y ∈ P
hy₂ : y ≠ 1
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
hy₃ : Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) y
⊢ 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:
mem_closure_of_mem hy₃

Premises used: Submonoid.mem_closure_of_mem
-- 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
hx₁ : x ∈ P
hx₂ : ¬x = 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} y
hy₁ : y ∈ P
hy₂ : y ≠ 1
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
hy₃ : Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) y
⊢ 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:
exact mem_closure_of_mem hy₃
-- 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
hx₁ : x ∈ P
hx₂ : ¬x = 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} y
hy₁ : y ∈ P
hy₂ : y ≠ 1
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
hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) y
neg :
  ∀ (z : M) (hz₁ : z < y) (hz₂ : z ∈ P) (hz₃ : z ≠ 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
⊢ 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:
rcases exists_lt_of_not_minimal ⟨hy₁, hy₂⟩ hy₃ with ⟨z, hz₁, hz₂, hz₃⟩

Premises used: exists_lt_of_not_minimal
-- 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
hx₁ : x ∈ P
hx₂ : ¬x = 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} y
hy₁ : y ∈ P
hy₂ : y ≠ 1
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
hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) y
z : M
hz₁ : z < y
hz₂ : z ∈ P
hz₃ : z ≠ 1
neg :
  ∀ (y : M),
    Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} (z * y) →
      ∀ (hy₁ : z * y ∈ P) (hy₂ : z * y ≠ 1)
        (ih :
          ∀ z_1 ∈ P,
            z_1 ≠ 1 →
              z_1 ≤ z * y →
                ¬z * y ≤ z_1 →
                  Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z_1)
        (hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) (z * y))
        (hz₁ : z < z * y),
        Membership.mem (γ := Submonoid M)
          (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) (z * y)
⊢ 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:
rcases exists_mul_of_le hz₁.le with ⟨y, rfl⟩

Premises used: LT.lt.le, rfl, ExistsMulOfLE.exists_mul_of_le
-- 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
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} (z * y)
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih :
  ∀ z_1 ∈ P,
    z_1 ≠ 1 →
      z_1 ≤ z * y →
        ¬z * y ≤ z_1 → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z_1
hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) (z * y)
hz₁ : z < z * y
neg :
  Membership.mem (γ := Submonoid M)
    (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) z
neg₁ :
  Membership.mem (γ := Submonoid M)
    (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) y
⊢ Membership.mem (γ := Submonoid M)
    (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) (z * y)

Tactic:
apply mul_mem

Premises used: MulMemClass.mul_mem
-- 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
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} (z * y)
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih :
  ∀ z_1 ∈ P,
    z_1 ≠ 1 →
      z_1 ≤ z * y →
        ¬z * y ≤ z_1 → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z_1
hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) (z * y)
hz₁ : z < z * y
⊢ Membership.mem (γ := Submonoid M)
    (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) z

Tactic:
ih _ hz₂ hz₃ hz₁.le hz₁.not_ge

Premises used: Set.Mem, setOf, LT.lt.le, LT.lt.not_ge
-- 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
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} (z * y)
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih :
  ∀ z_1 ∈ P,
    z_1 ≠ 1 →
      z_1 ≤ z * y →
        ¬z * y ≤ z_1 → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z_1
hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) (z * y)
hz₁ : z < z * y
⊢ Membership.mem (γ := Submonoid M)
    (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) z

Tactic:
exact ih _ hz₂ hz₃ hz₁.le hz₁.not_ge

Premises used: LT.lt.le, LT.lt.not_ge
-- 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
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} (z * y)
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih :
  ∀ z_1 ∈ P,
    z_1 ≠ 1 →
      z_1 ≤ z * y →
        ¬z * y ≤ z_1 → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z_1
hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) (z * y)
hz₁ : z < z * y
neg : y ∈ P
neg₁ : y ≠ 1
neg₂ : y ≤ z * y
neg₃ : ¬z * y ≤ y
⊢ 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:
apply ih
-- 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
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} (z * y)
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih :
  ∀ z_1 ∈ P,
    z_1 ≠ 1 →
      z_1 ≤ z * y →
        ¬z * y ≤ z_1 → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z_1
hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) (z * y)
hz₁ : z < z * y
⊢ y ∈ P

Tactic:
hP _ hz₂ _ hy₁
-- 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
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} (z * y)
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih :
  ∀ z_1 ∈ P,
    z_1 ≠ 1 →
      z_1 ≤ z * y →
        ¬z * y ≤ z_1 → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z_1
hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) (z * y)
hz₁ : z < z * y
⊢ y ∈ P

Tactic:
exact hP _ hz₂ _ hy₁
-- 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
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} (z * y)
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih :
  ∀ z_1 ∈ P,
    z_1 ≠ 1 →
      z_1 ≤ z * y →
        ¬z * y ≤ z_1 → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z_1
hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) (z * y)
hz₁ : z < z * y
⊢ y ≠ 1

Tactic:
(one_lt_of_lt_mul_right hz₁).ne.symm

Premises used: Ne.symm, one_lt_of_lt_mul_right, LT.lt.ne
-- 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
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} (z * y)
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih :
  ∀ z_1 ∈ P,
    z_1 ≠ 1 →
      z_1 ≤ z * y →
        ¬z * y ≤ z_1 → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z_1
hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) (z * y)
hz₁ : z < z * y
⊢ y ≠ 1

Tactic:
exact (one_lt_of_lt_mul_right hz₁).ne.symm

Premises used: Ne.symm, one_lt_of_lt_mul_right, LT.lt.ne
-- 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
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} (z * y)
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih :
  ∀ z_1 ∈ P,
    z_1 ≠ 1 →
      z_1 ≤ z * y →
        ¬z * y ≤ z_1 → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z_1
hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) (z * y)
hz₁ : z < z * y
⊢ y ≤ z * y

Tactic:
le_mul_self

Premises used: le_mul_self
-- 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
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} (z * y)
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih :
  ∀ z_1 ∈ P,
    z_1 ≠ 1 →
      z_1 ≤ z * y →
        ¬z * y ≤ z_1 → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z_1
hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) (z * y)
hz₁ : z < z * y
⊢ y ≤ z * y

Tactic:
exact le_mul_self

Premises used: le_mul_self
-- 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
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} (z * y)
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih :
  ∀ z_1 ∈ P,
    z_1 ≠ 1 →
      z_1 ≤ z * y →
        ¬z * y ≤ z_1 → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z_1
hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) (z * y)
hz₁ : z < z * y
neg : ¬z ≤ 1
⊢ ¬z * y ≤ y

Tactic:
rw [mul_le_iff_le_one_left']

Premises used: mul_le_iff_le_one_left'
-- 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
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} (z * y)
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih :
  ∀ z_1 ∈ P,
    z_1 ≠ 1 →
      z_1 ≤ z * y →
        ¬z * y ≤ z_1 → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z_1
hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) (z * y)
hz₁ : z < z * y
⊢ ¬z ≤ 1

Tactic:
(one_lt_of_ne_one hz₃).not_ge

Premises used: one_lt_of_ne_one, LT.lt.not_ge
-- 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
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} (z * y)
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih :
  ∀ z_1 ∈ P,
    z_1 ≠ 1 →
      z_1 ≤ z * y →
        ¬z * y ≤ z_1 → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z_1
hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) (z * y)
hz₁ : z < z * y
⊢ ¬z ≤ 1

Tactic:
exact (one_lt_of_ne_one hz₃).not_ge

Premises used: one_lt_of_ne_one, LT.lt.not_ge
-- 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
⊢ ∀ (x : M),
    Membership.mem (γ := Submonoid M) ⊤ x →
      ∀ (y : M), Membership.mem (γ := Submonoid M) ⊤ (x * y) → Membership.mem (γ := Submonoid M) ⊤ y

Tactic:
simp