Functions · hard

Statement, exactly as the model and Lean see it

theorem lg_target (f : ℝ → ℝ) (hf : ∀ x y, f (x + y) = f x + f y) (x : ℝ) : f (-x) = -f x := by

Source: Written for LeanGraph, reference proof certified
Premises used by the reference proof: 39

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

Attempts

sample 0 · round 0Incorrect rewrite2.2 s model time

Proof

have : f 0 = 0 := by rw [hf 0 0, hf 0 0]
let x' := x
let y' := -x
rw [hf x' y', hf 0 y']
simp only [add_right_neg, this]

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

4:27: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  f (0 + 0)
in the target expression
  f 0 = 0

f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x + f y
x : ℝ
⊢ f 0 = 0
7:6: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  f (x' + y')
in the target expression
  f (-x) = -f x

f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x + f y
x : ℝ
this : f 0 = 0
x' : ℝ := x
y' : ℝ := -x
⊢ f (-x) = -f x

Reference proof

The proof we wrote and certified before any model ran.

have h0 : f 0 = 0 := by
  have h := hf 0 0
  simp at h
  linarith
have h := hf x (-x)
simp [h0] at h
linarith