Inequalities · hard

Statement, exactly as the model and Lean see it

theorem lg_target {α : Type u_1} {β : Type u_2} [Preorder α] [Add α] [Sub α] [OrderedSub α] [Preorder β] [Add β] [Sub β] [OrderedSub β] (f : α →ₙ+ β) (hf : Monotone ⇑f) (a b : α) : f a - f b ≤ f (a - b) := by

Mathlib declaration: AddHom.le_map_tsub
Held-out module: Mathlib.Algebra.Order.Sub.Unbundled.Hom
Banned modules (itself + downstream): 3
Reference proof premises (reachable / held-out): 3 / 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.00005

Attempts

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

Proof

intro a b
apply (le_of_sub_le f a b)
apply hf
apply le_refl

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
inst✝⁷ : Preorder α
inst✝⁶ : Add α
inst✝⁵ : Sub α
inst✝⁴ : OrderedSub α
inst✝³ : Preorder β
inst✝² : Add β
inst✝¹ : Sub β
inst✝ : OrderedSub β
f : α →ₙ+ β
hf : Monotone ⇑f
a b : α
⊢ f a - f b ≤ f (a - b)

Reference proof

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

theorem AddHom.le_map_tsub [Preorder β] [Add β] [Sub β] [OrderedSub β] (f : AddHom α β)
    (hf : Monotone f) (a b : α) : f a - f b ≤ f (a - b) := by
  rw [tsub_le_iff_right, ← f.map_add]
  exact hf le_tsub_add