Functions · easy

Statement, exactly as the model and Lean see it

theorem lg_target (f : ℝ → ℝ) (hf : ∀ x, f x = 3 * x + 2) : Function.Injective f := by

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

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

Attempts

sample 0 · round 0Lean 3 syntax3.4 s model time

Proof

intro x y
rw [hf x, hf y]
assume h : 3 * x + 2 = 3 * y + 2
rw [sub_eq_zero] at h
have h1 : 3 * (x - y) = 0 := h
rw [mul_eq_zero] at h1
cases h1 with h2 h3
· rw [h2] at h1
  exact h1
· rw [h3] at h1
  exact h1

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

6:9: error: Unknown identifier `h`
6:11: error: unexpected token ':'; expected command

Reference proof

The proof we wrote and certified before any model ran.

intro a b h
rw [hf, hf] at h
linarith