Inequalities · medium

Statement, exactly as the model and Lean see it

theorem lg_target {ι : Type u_1} {G : Type u_2} [AddGroup G] [ConditionallyCompleteLattice G] [Nonempty ι] {f : ι → G} [AddLeftMono G] (hf : BddAbove (Set.range f)) (a : G) : a + ⨆ i, f i = ⨆ i, a + f i := by

Mathlib declaration: add_ciSup
Held-out module: Mathlib.Algebra.Order.Group.CompleteLattice
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.00005

Attempts

sample 0 · round 0Hallucinated theorem1.3 s model time

Proof

rw [supr_add]
exact supr_add' hf

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

4:6: error: Unknown identifier `supr_add`
3:206: error: unsolved goals
ι : Type u_1
G : Type u_2
inst✝³ : AddGroup G
inst✝² : ConditionallyCompleteLattice G
inst✝¹ : Nonempty ι
f : ι → G
inst✝ : AddLeftMono G
hf : BddAbove (Set.range f)
a : G
⊢ a + ⨆ i, f i = ⨆ i, a + f i

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]