Probability · medium

Statement, exactly as the model and Lean see it

theorem lg_target {r x : ℝ} : HasDerivAt (fun a => -Real.exp (-(r * a))) (r * Real.exp (-(r * x))) x := by

Mathlib declaration: ProbabilityTheory.hasDerivAt_neg_exp_mul_exp
Held-out module: Mathlib.Probability.Distributions.Exponential
Banned modules (itself + downstream): 1
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.00012

Attempts

sample 0 · round 0Wrong tactic5.1 s model time

Proof

intros x;
have h : DifferentiableAt ℝ (fun a => -Real.exp (-(r * a))) x := by
  apply differentiable_at_const_mul;
  apply differentiable_at_neg;
  apply differentiable_at_exp;
  apply differentiable_at_const_mul;
  apply differentiable_at_id;
  exact x;
have h' : Deriv (fun a => -Real.exp (-(r * a))) x = r * Real.exp (-(r * x)) := by
  rw [deriv_neg, deriv_exp, deriv_const_mul, mul_assoc];
  rw [mul_left_comm r (Real.exp (-(r * x))) (-1)];
  rw [mul_neg]; -- -1 * r = -r
  rw [neg_neg]; -- --r = r
  rw [mul_assoc];
  rw [mul_one];
  exact rfl;
exact HasDerivAt.of_differentiable_at_and_deriv h h'

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

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

r x : ℝ
⊢ HasDerivAt (fun a => -Real.exp (-(r * a))) (r * Real.exp (-(r * x))) x

Reference proof

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

lemma hasDerivAt_neg_exp_mul_exp {r x : ℝ} :
    HasDerivAt (fun a ↦ -exp (-(r * a))) (r * exp (-(r * x))) x := by
  convert! (((hasDerivAt_id x).const_mul (-r)).exp.const_mul (-1)) using 1
  · simp only [one_mul, id_eq, neg_mul]
  simp only [id_eq, neg_mul, mul_one, mul_neg, one_mul, neg_neg, mul_comm]