Number theory · hard

Statement, exactly as the model and Lean see it

theorem lg_target {n : ℕ} (hn : Even n) : AddSubmonoid.closure (Set.range fun x => x ^ n) = AddSubmonoid.nonneg ℤ := by

Mathlib declaration: Int.addSubmonoid_closure_range_pow
Held-out module: Mathlib.Data.Int.Star
Banned modules (itself + downstream): 8
Reference proof premises (reachable / held-out): 18 / 0

Traces

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

Not verified1 model calls · 1 Lean checks · $0.00011

Attempts

sample 0 · round 0Lean 3 syntax5.8 s model time

Proof

intro n hn
apply AddSubmonoid.closure_eq_nonneg
apply le_antisymm
· intro x hx
  cases hx with m hm
  rw [hm]
  apply Int.ofNat_nonneg
· intro x hx
  let m := (Int.ofNat x).natCast
  have h0 : 0 ≤ m := Int.ofNat_nonneg x
  have h1 : m ^ n = (Int.ofNat x) ^ n := by rw [Int.ofNat_pow]
  have h2 : (Int.ofNat x) ^ n ∈ Set.range (fun x => x ^ n) :=
    ⟨m, by rw [h1]⟩
  exact AddSubmonoid.closure_subset (Set.range (fun x => x ^ n)) h2

What Lean printed (this is all the model sees on repair)

8:19: error: unknown tactic

Reference proof

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

@[simp] lemma addSubmonoid_closure_range_pow {n : ℕ} (hn : Even n) :
    closure (range fun x : ℤ ↦ x ^ n) = nonneg _ := by
  refine le_antisymm (closure_le.2 <| range_subset_iff.2 hn.pow_nonneg) fun x hx ↦ ?_
  have : x = x.natAbs • 1 ^ n := by simpa [eq_comm (a := x)] using hx
  rw [this]
  exact nsmul_mem (subset_closure <| mem_range_self _) _