Inequalities · hard

Statement, exactly as the model and Lean see it

theorem lg_target {M : Type u_1} [CommMonoid M] [PartialOrder M] [WellQuasiOrderedLE M] [CanonicallyOrderedMul M] : WellFoundedGT (SemigroupIdeal M) := by

Mathlib declaration: SemigroupIdeal.instWellFoundedGT
Held-out module: Mathlib.Algebra.Order.Group.Ideal
Banned modules (itself + downstream): 3
Reference proof premises (reachable / held-out): 13 / 1

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

No configuration has attempted this theorem yet.

Reference proof

Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.

/-- In a canonically ordered and well-quasi-ordered monoid, the semigroup ideals satisfy the
ascending chain condition. -/
@[to_additive /-- A canonically ordered and well-quasi-ordered additive monoid, the semigroup ideals
satisfy the ascending chain condition. -/]
instance : WellFoundedGT (SemigroupIdeal M) := by
  rw [wellFoundedGT_iff_monotone_chain_condition]
  intro f
  rcases fg_iff.1 (fg_of_wellQuasiOrderedLE (⨆ i, f i)) with ⟨s, hI⟩
  have hs : ∀ x ∈ s, ∃ i, x ∈ f i := by
    intro x hx
    apply subset_closure (s := (s : Set M)) at hx
    simpa [← hI] using hx
  choose! g hg using hs
  exists s.sup g
  intro n hn
  apply (f.mono hn).antisymm
  apply (le_iSup f n).trans
  intro x hx
  rw [hI, mem_closure''] at hx
  rcases hx with ⟨y, z, hz, rfl⟩
  exact SemigroupIdeal.mul_mem _ _ (f.mono (Finset.le_sup hz) (hg _ hz))