Inequalities · easy

Statement, exactly as the model and Lean see it

theorem lg_target {n a : ℕ} : (∃ x, x ^ n = a) ↔ n = 0 ∧ a = 1 ∨ n ≠ 0 ∧ n.nthRoot a ^ n = a := by

Mathlib declaration: Nat.exists_pow_eq_iff
Held-out module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Banned modules (itself + downstream): 1
Reference proof premises (reachable / held-out): 1 / 1

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.00010

Attempts

sample 0 · round 0Lean 3 syntax4.0 s model time

Proof

intro h
split
· intro h1
  cases h1 with h2 h3
  constructor
  · exact h2
  · exact h3
· intro h1
  by_cases h2: n = 0
  · constructor
    · exact h2
    · exact (nat.one_pow n).symm
  · constructor
    · exact h1.1
    · rw [nat.nth_root_def]
      have h3: n ≠ 0 := h1.1
      have h4: a = n.nthRoot a ^ n := h1.2
      exact h4

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

7: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.

theorem exists_pow_eq_iff :
    (∃ x, x ^ n = a) ↔ ((n = 0 ∧ a = 1) ∨ (n ≠ 0 ∧ (nthRoot n a) ^ n = a)) := by
  rcases eq_or_ne n 0 with rfl | _ <;> grind [exists_pow_eq_iff']