Inequalities · easy

Statement, exactly as the model and Lean see it

theorem lg_target {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [LE β] [Zero β] {v₁ : α₁ → β} {v₂ : α₂ → β} : 0 ≤ Sum.elim v₁ v₂ ↔ 0 ≤ v₁ ∧ 0 ≤ v₂ := by

Mathlib declaration: Sum.nonneg_elim_iff
Held-out module: Mathlib.Algebra.Order.Sum
Banned modules (itself + downstream): 1
Reference proof premises (reachable / held-out): 1 / 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.00006

Attempts

sample 0 · round 0Wrong tactic1.9 s model time

Proof

intro h
split
· rw [Sum.elim]
  intros
  exact h
· rw [Sum.elim]
  intro h'
  exact h'.1
  exact h'.2

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

α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
inst✝¹ : LE β
inst✝ : Zero β
v₁ : α₁ → β
v₂ : α₂ → β
⊢ 0 ≤ Sum.elim v₁ v₂ ↔ 0 ≤ v₁ ∧ 0 ≤ v₂

Reference proof

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

@[to_additive]