awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
refine_2 : count x s = s.card * if x = a then 1 else 0
⊢ count x s = count x (HSMul.hSMul (β := Multiset α) s.card {a})

Tactic:
rw [count_nsmul, count_singleton]

Premises used: Multiset.count_nsmul, Multiset.count_singleton
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
pos : ∀ (hx : x = a), count x s = s.card * if x = a then 1 else 0
neg : ∀ (hx : ¬x = a), count x s = s.card * if x = a then 1 else 0
⊢ count x s = s.card * if x = a then 1 else 0

Tactic:
by_cases hx : x = a
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
pos : ∀ x ∈ s, a = x
⊢ count x s = s.card * if x = a then 1 else 0

Tactic:
simp_rw [hx, ite_true, mul_one, count_eq_card]

Premises used: ite_true, mul_one, Multiset.count_eq_card
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
y : α
hy : y ∈ s
⊢ y = a

Tactic:
rw [← mem_toFinset, H, Finset.mem_singleton] at hy

Premises used: Finset.mem_singleton, Multiset.mem_toFinset
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
y : α
hy : y = a
⊢ a = y

Tactic:
hy.symm

Premises used: Eq.symm
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
y : α
hy : y = a
⊢ a = y

Tactic:
exact hy.symm

Premises used: Eq.symm
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : ¬x = a
h' : x ∈ s
rwa : ∀ (h' : x ∈ s.toFinset), x = a
rwa₁ : ∀ (h' : Membership.mem (γ := Finset α) {a} x), x = a
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h' : x = a), x = a
⊢ x = a

Tactic:
rwa [← mem_toFinset, H, Finset.mem_singleton] at h'

Premises used: Finset.mem_singleton, Multiset.mem_toFinset
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : ¬x = a
⊢ x ∉ s

Tactic:
have hx' : x ∉ s := fun h' ↦ hx <| by rwa [← mem_toFinset, H, Finset.mem_singleton] at h'
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : ¬x = a
hx' : x ∉ s
neg : 0 = s.card * if x = a then 1 else 0
neg₁ : 0 = s.card * if False then 1 else 0
neg₂ : 0 = s.card * 0
⊢ count x s = s.card * if x = a then 1 else 0

Tactic:
simp_rw [count_eq_zero_of_notMem hx', hx, ite_false, Nat.mul_zero]

Premises used: ite_false, Nat.mul_zero, Multiset.count_eq_zero_of_notMem
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.card ≠ 0 ∧ s = HSMul.hSMul (β := Multiset α) s.card {a}
⊢ s.toFinset = {a}

Tactic:
simpa only [toFinset_nsmul _ _ H.1, toFinset_singleton] using congr($(H.2).toFinset)

Premises used: Multiset.toFinset_nsmul, And.left, Multiset.toFinset_singleton
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
simp_rw : (∃ (a : α), s.toFinset = {a}) ↔ s.card ≠ 0 ∧ ∃ (a : α), s = HSMul.hSMul (β := Multiset α) s.card {a}
simp_rw₁ :
  (∃ (a : α), s.card ≠ 0 ∧ s = HSMul.hSMul (β := Multiset α) s.card {a}) ↔
    s.card ≠ 0 ∧ ∃ (a : α), s = HSMul.hSMul (β := Multiset α) s.card {a}
⊢ #s.toFinset = 1 ↔ s.card ≠ 0 ∧ ∃ (a : α), s = HSMul.hSMul (β := Multiset α) s.card {a}

Tactic:
simp_rw [Finset.card_eq_one, Multiset.toFinset_eq_singleton_iff, exists_and_left]

Premises used: Finset.card_eq_one, exists_and_left, Multiset.toFinset_eq_singleton_iff
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
ι : Type u_1
M : Type u_3
inst : LinearOrder M
inst_1 : Add M
inst_2 : AddRightMono M
s : Finset ι
a : WithBot M
f : ι → M
empty : fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) ∅ = fold max ⊥ (WithBot.some ∘ f) ∅ + a
insert :
  ∀ (a_1 : ι) (s : Finset ι),
    a_1 ∉ s →
      fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) s = fold max ⊥ (WithBot.some ∘ f) s + a →
        fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) (Insert.insert a_1 s) =
          fold max ⊥ (WithBot.some ∘ f) (Insert.insert a_1 s) + a
⊢ fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) s = fold max ⊥ (WithBot.some ∘ f) s + a

Tactic:
induction s using Finset.induction_on
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
ι : Type u_1
M : Type u_3
inst : LinearOrder M
inst_1 : Add M
inst_2 : AddRightMono M
a : WithBot M
f : ι → M
⊢ fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) ∅ = fold max ⊥ (WithBot.some ∘ f) ∅ + a

Tactic:
simp [*, max_add_add_right]

Premises used: max_add_add_right
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
ι : Type u_1
M : Type u_3
inst : LinearOrder M
inst_1 : Add M
inst_2 : AddRightMono M
a : WithBot M
f : ι → M
a_1 : ι
s : Finset ι
h : a_1 ∉ s
h_1 : fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) s = fold max ⊥ (WithBot.some ∘ f) s + a
⊢ fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) (insert a_1 s) = fold max ⊥ (WithBot.some ∘ f) (insert a_1 s) + a

Tactic:
simp [*, max_add_add_right]

Premises used: max_add_add_right
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
ι : Type u_1
M : Type u_3
inst : LinearOrder M
inst_1 : Add M
inst_2 : AddRightMono M
s : Finset ι
a : WithBot M
f : ι → M
empty : fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) ∅ = fold max ⊥ (WithBot.some ∘ f) ∅ + a
insert :
  ∀ (a_1 : ι) (s : Finset ι),
    a_1 ∉ s →
      fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) s = fold max ⊥ (WithBot.some ∘ f) s + a →
        fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) (Insert.insert a_1 s) =
          fold max ⊥ (WithBot.some ∘ f) (Insert.insert a_1 s) + a
empty₁ : fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) ∅ = fold max ⊥ (WithBot.some ∘ f) ∅ + a
insert₁ :
  ∀ (a_1 : ι) (s : Finset ι),
    a_1 ∉ s →
      fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) s = fold max ⊥ (WithBot.some ∘ f) s + a →
        fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) (Insert.insert a_1 s) =
          fold max ⊥ (WithBot.some ∘ f) (Insert.insert a_1 s) + a
empty₂ : fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) ∅ = fold max ⊥ (WithBot.some ∘ f) ∅ + a
insert₂ :
  ∀ (a_1 : ι) (s : Finset ι),
    a_1 ∉ s →
      fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) s = fold max ⊥ (WithBot.some ∘ f) s + a →
        fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) (Insert.insert a_1 s) =
          fold max ⊥ (WithBot.some ∘ f) (Insert.insert a_1 s) + a
empty₃ : fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) ∅ = fold max ⊥ (WithBot.some ∘ f) ∅ + a
insert₃ :
  ∀ (a_1 : ι) (s : Finset ι),
    a_1 ∉ s →
      fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) s = fold max ⊥ (WithBot.some ∘ f) s + a →
        fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) (Insert.insert a_1 s) =
          fold max ⊥ (WithBot.some ∘ f) (Insert.insert a_1 s) + a
⊢ fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) s = fold max ⊥ (WithBot.some ∘ f) s + a

Tactic:
classical induction s using Finset.induction_on <;> simp [*, max_add_add_right]

Premises used: max_add_add_right
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
ι : Type u_1
M : Type u_3
inst : LinearOrder M
inst_1 : Monoid M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s : Finset ι
f : ι → M
n : ℕ
hs : s.Nonempty
⊢ s.inf' hs f ^ n = s.inf' hs fun (a : ι) ↦ f a ^ n

Tactic:
map_finset_inf' (OrderHom.mk _ <| pow_left_mono n) hs _

Premises used: pow_left_mono, map_finset_inf', OrderHom.mk
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
ι : Type u_1
M : Type u_3
inst : LinearOrder M
inst_1 : Monoid M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s : Finset ι
f : ι → M
n : ℕ
hs : s.Nonempty
⊢ s.sup' hs f ^ n = s.sup' hs fun (a : ι) ↦ f a ^ n

Tactic:
map_finset_sup' (OrderHom.mk _ <| pow_left_mono n) hs _

Premises used: map_finset_sup', pow_left_mono, OrderHom.mk
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
inst_1 : LinearOrder G
inst_2 : MulRightMono G
s : Finset ι
f : ι → G
a : G
hs : s.Nonempty
⊢ s.sup' hs f * a = s.sup' hs fun (i : ι) ↦ f i * a

Tactic:
map_finset_sup' (OrderIso.mulRight a) hs f

Premises used: map_finset_sup', OrderIso.mulRight
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
inst_1 : LinearOrder G
inst_2 : MulLeftMono G
s : Finset ι
f : ι → G
a : G
hs : s.Nonempty
⊢ a * s.sup' hs f = s.sup' hs fun (i : ι) ↦ a * f i

Tactic:
map_finset_sup' (OrderIso.mulLeft a) hs f

Premises used: OrderIso.mulLeft, map_finset_sup'
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : CanonicallyOrderedAdd M
inst_3 : Sub M
inst_4 : AddLeftReflectLE M
inst_5 : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
a₁ : s.sup' hs f + a ≤ s.sup' hs fun (i : ι) ↦ f i + a
a₂ : (s.sup' hs fun (i : ι) ↦ f i + a) ≤ s.sup' hs f + a
⊢ s.sup' hs f + a = s.sup' hs fun (i : ι) ↦ f i + a

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : CanonicallyOrderedAdd M
inst_3 : Sub M
inst_4 : AddLeftReflectLE M
inst_5 : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
a₁ : a ≤ s.sup' hs fun (i : ι) ↦ f i + a
a₂ : s.sup' hs f ≤ (s.sup' hs fun (i : ι) ↦ f i + a) - a
⊢ s.sup' hs f + a ≤ s.sup' hs fun (i : ι) ↦ f i + a

Tactic:
apply add_le_of_le_tsub_right_of_le

Premises used: add_le_of_le_tsub_right_of_le
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : CanonicallyOrderedAdd M
inst_3 : Sub M
inst_4 : AddLeftReflectLE M
inst_5 : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ a ≤ s.sup' hs fun (i : ι) ↦ f i + a

Tactic:
Finset.le_sup'_of_le _ hs.choose_spec le_add_self

Premises used: Exists.choose_spec, Finset.le_sup'_of_le, le_add_self
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : CanonicallyOrderedAdd M
inst_3 : Sub M
inst_4 : AddLeftReflectLE M
inst_5 : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ a ≤ s.sup' hs fun (i : ι) ↦ f i + a

Tactic:
exact Finset.le_sup'_of_le _ hs.choose_spec le_add_self
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : CanonicallyOrderedAdd M
inst_3 : Sub M
inst_4 : AddLeftReflectLE M
inst_5 : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ s.sup' hs f ≤ (s.sup' hs fun (i : ι) ↦ f i + a) - a

Tactic:
Finset.sup'_le _ _ fun i hi ↦ le_tsub_of_add_le_right (Finset.le_sup' (f · + a) hi)

Premises used: Finset.sup'_le, HAdd.hAdd, le_tsub_of_add_le_right, Finset.le_sup'
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : CanonicallyOrderedAdd M
inst_3 : Sub M
inst_4 : AddLeftReflectLE M
inst_5 : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ s.sup' hs f ≤ (s.sup' hs fun (i : ι) ↦ f i + a) - a

Tactic:
exact Finset.sup'_le _ _ fun i hi ↦ le_tsub_of_add_le_right (Finset.le_sup' (f · + a) hi)

Premises used: Finset.sup'_le, le_tsub_of_add_le_right
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : CanonicallyOrderedAdd M
inst_3 : Sub M
inst_4 : AddLeftReflectLE M
inst_5 : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
i : ι
hi : i ∈ s
grw grw₁ : f i + a ≤ f i + a
⊢ f i + a ≤ s.sup' hs f + a

Tactic:
grw [← Finset.le_sup' _ hi]

Premises used: Finset.le_sup'
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : CanonicallyOrderedAdd M
inst_3 : Sub M
inst_4 : AddLeftReflectLE M
inst_5 : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ (s.sup' hs fun (i : ι) ↦ f i + a) ≤ s.sup' hs f + a

Tactic:
exact Finset.sup'_le _ _ fun i hi ↦ by grw [← Finset.le_sup' _ hi]

Premises used: Finset.sup'_le
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : CanonicallyOrderedAdd M
inst_3 : Sub M
inst_4 : AddLeftReflectLE M
inst_5 : OrderedSub M
s : Finset ι
hs : s.Nonempty
f : ι → M
a : M
simp_rw : s.sup' hs f + a = s.sup' ⋯ fun (x : ι) ↦ f x + a
⊢ a + s.sup' hs f = s.sup' hs fun (i : ι) ↦ a + f i

Tactic:
simp_rw [add_comm a, Finset.sup'_add']

Premises used: Finset.sup'_add', add_comm
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : CanonicallyOrderedAdd M
inst_3 : Sub M
inst_4 : AddLeftReflectLE M
inst_5 : OrderedSub M
s : Finset ι
inst_6 : OrderBot M
hs : s.Nonempty
f : ι → M
a : M
rw : s.sup' hs f + a = s.sup fun (i : ι) ↦ f i + a
rw₁ : s.sup' hs f + a = s.sup' hs fun (i : ι) ↦ f i + a
rw₂ rw₃ : Eq.{u_3 + 1} (α := M) (s.sup' hs fun (i : ι) ↦ f i + a) (s.sup' hs fun (i : ι) ↦ f i + a)
⊢ s.sup f + a = s.sup fun (i : ι) ↦ f i + a

Tactic:
rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, sup'_add']

Premises used: Finset.sup'_add', Finset.sup'_eq_sup
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : CanonicallyOrderedAdd M
inst_3 : Sub M
inst_4 : AddLeftReflectLE M
inst_5 : OrderedSub M
s : Finset ι
inst_6 : OrderBot M
hs : s.Nonempty
f : ι → M
a : M
rw : a + s.sup' hs f = s.sup fun (i : ι) ↦ a + f i
rw₁ : a + s.sup' hs f = s.sup' hs fun (i : ι) ↦ a + f i
rw₂ rw₃ : Eq.{u_3 + 1} (α := M) (s.sup' hs fun (i : ι) ↦ a + f i) (s.sup' hs fun (i : ι) ↦ a + f i)
⊢ a + s.sup f = s.sup fun (i : ι) ↦ a + f i

Tactic:
rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, add_sup'']

Premises used: Finset.sup'_eq_sup, Finset.add_sup''
-- Module: Mathlib.Algebra.Order.Group.Finset
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : CanonicallyOrderedAdd M
inst_3 : Sub M
inst_4 : AddLeftReflectLE M
inst_5 : OrderedSub M
s : Finset ι
t : Finset κ
inst_6 : OrderBot M
hs : s.Nonempty
ht : t.Nonempty
f : ι → M
g : κ → M
⊢ s.sup f + t.sup g = (s ×ˢ t).sup fun (ij : ι × κ) ↦ f ij.1 + g ij.2

Tactic:
simp only [Finset.sup_add hs, Finset.add_sup ht, Finset.sup_product_left]

Premises used: Finset.sup_product_left, Finset.add_sup, Finset.sup_add
-- Module: Mathlib.Algebra.Order.Group.Ideal
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
⊢ Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}

Tactic:
have hpwo := Set.isPWO_of_wellQuasiOrderedLE { x | x ∈ I }
-- Module: Mathlib.Algebra.Order.Group.Ideal
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}
⊢ I.FG

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

Premises used: setOf_minimal_subset, SemigroupIdeal.FG, And.intro, Exists.intro, setOf_minimal_antichain, IsAntichain.finite_of_partiallyWellOrderedOn, Set.IsPWO.mono
-- Module: Mathlib.Algebra.Order.Group.Ideal
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}
refine : I = closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ I} x) x}
⊢ I.FG

Tactic:
refine ⟨_, (setOf_minimal_antichain _).finite_of_partiallyWellOrderedOn
    (hpwo.mono (setOf_minimal_subset _)), ?_⟩
-- Module: Mathlib.Algebra.Order.Group.Ideal
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}
h :
  ∀ (x : M),
    x ∈ I ↔
      Membership.mem (γ := SubMulAction M M)
        (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ I} x) x}) x
⊢ I = closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ I} x) x}

Tactic:
ext x
-- Module: Mathlib.Algebra.Order.Group.Ideal
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}
x : M
h : x ∈ I ↔ ∃ (y : M) (z : M), Minimal (fun (x : M) ↦ x ∈ I) z ∧ y * z = x
⊢ x ∈ I ↔
    Membership.mem (γ := SubMulAction M M)
      (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ I} x) x}) x

Tactic:
simp only [mem_closure'', SetLike.setOf_mem_eq, SetLike.mem_coe, Set.mem_setOf_eq]

Premises used: SemigroupIdeal.mem_closure'', SetLike.setOf_mem_eq, Set.mem_setOf_eq, SetLike.mem_coe
-- Module: Mathlib.Algebra.Order.Group.Ideal
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}
x : M
h : x ∈ I → ∃ (y : M) (z : M), Minimal (fun (x : M) ↦ x ∈ I) z ∧ y * z = x
h₁ : (∃ (y : M) (z : M), Minimal (fun (x : M) ↦ x ∈ I) z ∧ y * z = x) → x ∈ I
⊢ x ∈ I ↔ ∃ (y : M) (z : M), Minimal (fun (x : M) ↦ x ∈ I) z ∧ y * z = x

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Group.Ideal
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}
x : M
hx : x ∈ I
h :
  ∀ (z : M) (hz : z ≤ x) (hz' : Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ I} x) z),
    ∃ (y : M) (z : M), Minimal (fun (x : M) ↦ x ∈ I) z ∧ y * z = x
⊢ ∃ (y : M) (z : M), Minimal (fun (x : M) ↦ x ∈ I) z ∧ y * z = x

Tactic:
rcases hpwo.exists_le_minimal hx with ⟨z, hz, hz'⟩

Premises used: Set.IsPWO.exists_le_minimal
-- Module: Mathlib.Algebra.Order.Group.Ideal
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}
x : M
hx : x ∈ I
z : M
hz : z ≤ x
hz' : Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ I} x) z
⊢ ∃ (c : M), x = c * z

Tactic:
rw [le_iff_exists_mul'] at hz

Premises used: le_iff_exists_mul'
-- Module: Mathlib.Algebra.Order.Group.Ideal
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}
x : M
hx : x ∈ I
z : M
hz : z ≤ x
hz' : Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ I} x) z
hz₁ : ∃ (c : M), x = c * z
⊢ Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ I} x) z

Tactic:
rw [le_iff_exists_mul'] at hz

Premises used: le_iff_exists_mul'
-- Module: Mathlib.Algebra.Order.Group.Ideal
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}
x : M
hx : x ∈ I
z : M
hz : ∃ (c : M), x = c * z
hz' : Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ I} x) z
h : ∀ (y : M) (hx : y * z ∈ I), ∃ (y_1 : M) (z_1 : M), Minimal (fun (x : M) ↦ x ∈ I) z_1 ∧ y_1 * z_1 = y * z
⊢ ∃ (y : M) (z : M), Minimal (fun (x : M) ↦ x ∈ I) z ∧ y * z = x

Tactic:
rcases hz with ⟨y, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Ideal
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}
z : M
hz' : Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ I} x) z
y : M
hx : y * z ∈ I
⊢ ∃ (y_1 : M) (z_1 : M), Minimal (fun (x : M) ↦ x ∈ I) z_1 ∧ y_1 * z_1 = y * z

Tactic:
⟨y, z, hz', rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Order.Group.Ideal
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}
z : M
hz' : Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ I} x) z
y : M
hx : y * z ∈ I
⊢ ∃ (y_1 : M) (z_1 : M), Minimal (fun (x : M) ↦ x ∈ I) z_1 ∧ y_1 * z_1 = y * z

Tactic:
exact ⟨y, z, hz', rfl⟩
-- Module: Mathlib.Algebra.Order.Group.Ideal
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}
y z : M
hz : Minimal (fun (x : M) ↦ x ∈ I) z
h : z ∈ I
⊢ y * z ∈ I

Tactic:
apply SubMulAction.smul_mem

Premises used: SubMulAction.smul_mem
-- Module: Mathlib.Algebra.Order.Group.Ideal
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}
y z : M
hz : Minimal (fun (x : M) ↦ x ∈ I) z
⊢ z ∈ I

Tactic:
hz.1

Premises used: Set.Mem, And.left
-- Module: Mathlib.Algebra.Order.Group.Ideal
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}
y z : M
hz : Minimal (fun (x : M) ↦ x ∈ I) z
⊢ z ∈ I

Tactic:
exact hz.1

Premises used: And.left
-- Module: Mathlib.Algebra.Order.Group.Ideal
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
rw :
  ∀ (a : ℕ →o SemigroupIdeal M),
    ∃ (n : ℕ),
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := SemigroupIdeal M) ((a : (a : ℕ) → SemigroupIdeal M) n : SemigroupIdeal M)
            ((a : (a : ℕ) → SemigroupIdeal M) m : SemigroupIdeal M)
⊢ WellFoundedGT.{u_1} (SemigroupIdeal M)

Tactic:
rw [wellFoundedGT_iff_monotone_chain_condition]

Premises used: wellFoundedGT_iff_monotone_chain_condition
-- Module: Mathlib.Algebra.Order.Group.Ideal
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
f : ℕ →o SemigroupIdeal M
rcases :
  ∀ (s : Finset M)
    (hI : Eq (α := SemigroupIdeal M) (⨆ (i : ℕ), (f : (a : ℕ) → SemigroupIdeal M) i) (closure (↑s : Set M))),
    ∃ (n : ℕ),
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) n : SemigroupIdeal M)
            ((f : (a : ℕ) → SemigroupIdeal M) m : SemigroupIdeal M)
⊢ ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := SemigroupIdeal M) ((f : (a : ℕ) → SemigroupIdeal M) n : SemigroupIdeal M)
          ((f : (a : ℕ) → SemigroupIdeal M) m : SemigroupIdeal M)

Tactic:
rcases fg_iff.1 (fg_of_wellQuasiOrderedLE (⨆ i, f i)) with ⟨s, hI⟩

Premises used: SemigroupIdeal.fg_of_wellQuasiOrderedLE, SemigroupIdeal.fg_iff, iSup, Iff.mp, DFunLike.coe
-- Module: Mathlib.Algebra.Order.Group.Ideal
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
f : ℕ →o SemigroupIdeal M
s : Finset M
hI : Eq (α := SemigroupIdeal M) (⨆ (i : ℕ), (f : (a : ℕ) → SemigroupIdeal M) i) (closure (↑s : Set M))
x : M
hx : x ∈ s
⊢ x ∈ (↑(closure (↑s : Set M)) : Set M)

Tactic:
apply subset_closure (s := (s : Set M)) at hx

Premises used: SemigroupIdeal.subset_closure