Algebra · hard

Statement, exactly as the model and Lean see it

theorem lg_target {R : Type u_2} {a b : R} [CommRing R] {r : R} : (algebraMap R (QuadraticAlgebra R a b)) r ∈ nonZeroDivisors (QuadraticAlgebra R a b) ↔ r ∈ nonZeroDivisors R := by

Mathlib declaration: QuadraticAlgebra.algebraMap_mem_nonZeroDivisors_iff
Held-out module: Mathlib.Algebra.QuadraticAlgebra.Basic
Banned modules (itself + downstream): 2
Reference proof premises (reachable / held-out): 15 / 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.00010

Attempts

sample 0 · round 0Wrong tactic3.4 s model time

Proof

intro h
split
· intro hnz
  haveI : IsDomain (QuadraticAlgebra R a b) := nonZeroDivisors_iff_ne_zero.1 (nonZeroDivisors_subset_nonZeroDivisors _ _ hnz)
  haveI : IsDomain R := nonZeroDivisors_iff_ne_zero.1 hnz
  rw [nonZeroDivisors_iff_ne_zero] at h
  exact h
· intro hnz
  rw [nonZeroDivisors_iff_ne_zero] at hnz
  exact nonZeroDivisors_subset_nonZeroDivisors _ _ hnz

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

4:8: error: Tactic `introN` failed: There are no additional binders or `let` bindings in the goal to introduce

R : Type u_2
a b : R
inst✝ : CommRing R
r : R
⊢ (algebraMap R (QuadraticAlgebra R a b)) r ∈ nonZeroDivisors (QuadraticAlgebra R a b) ↔ r ∈ nonZeroDivisors R

Reference proof

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

theorem algebraMap_mem_nonZeroDivisors_iff {r : R} :
    algebraMap R (QuadraticAlgebra R a b) r ∈ (QuadraticAlgebra R a b)⁰ ↔ r ∈ R⁰ := by
  simp only [mem_nonZeroDivisors_iff_right]
  constructor
  · intro H x hxr
    rw [← algebraMap_inj, map_zero]
    apply H
    rw [← map_mul, hxr, map_zero]
  · intro h z hz
    rw [QuadraticAlgebra.ext_iff, re_zero, im_zero] at hz
    simp only [re_mul, algebraMap_re, algebraMap_im, mul_zero, add_zero, im_mul, zero_add] at hz
    simp [QuadraticAlgebra.ext_iff, re_zero, im_zero, h _ hz.left, h _ hz.right]