Inequalities · hard

Statement, exactly as the model and Lean see it

theorem lg_target {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a b c : α) : Multiset.map (fun x => c + x) (Multiset.Icc a b) = Multiset.Icc (c + a) (c + b) := by

Mathlib declaration: Multiset.map_add_left_Icc
Held-out module: Mathlib.Algebra.Order.Interval.Multiset
Banned modules (itself + downstream): 1
Reference proof premises (reachable / held-out): 8 / 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.00030

Attempts

sample 0 · round 0Hallucinated theorem29.8 s model time

Proof

induction on the multiset Icc a b
case empty =>
  show Multiset.map (fun x => c + x) ∅ = Multiset.Icc (c + a) (c + b)
  simp [Multiset.Icc, Multiset.map]
case cons x xs =>
  obtain h : x ≤ b := by exact Icc.mem_iff.1 (Multiset.Icc.mem_iff.2 ⟨x, rfl⟩)
  have h1 : x = a := by rw [Icc.eq_iff.1 (Multiset.Icc.eq_iff.2 ⟨x, rfl⟩)]
  have h2 : xs = Icc a b \ {x} := by rw [Icc.remove_singleton]
  have h3 : Multiset.map (fun x => c + x) (Icc a b) = Multiset.map (fun x => c + x) {x} ++ Multiset.map (fun x => c + x) xs :=
    by simp [Multiset.map, h2]
  have h4 : Multiset.map (fun x => c + x) {x} = {c + x} := by simp [Multiset.map]
  have h5 : Multiset.Icc (c + a) (c + b) = {c + a} ++ Multiset.Icc (c + a) (c + b) \ {c + a} :=
    by simp [Multiset.Icc]
  have h6 : Multiset.Icc (c + a) (c + b) \ {c + a} = Multiset.Icc (c + (a + 1)) (c + b) :=
    by rw [Icc.remove_singleton]
  have h7 : Multiset.map (fun x => c + x) xs = Multiset.Icc (c + (a + 1)) (c + b) :=
    by rw [h2, h3, h4, h5, h6]
  have h8 : Multiset.map (fun x => c + x) (Icc a b) = {c + a} ++ Multiset.Icc (c + (a + 1)) (c + b) :=
    by rw [h3, h4, h5, h7]
  have h9 : {c + a} ++ Multiset.Icc (c + (a + 1)) (c + b) = Multiset.Icc (c + a) (c + b) :=
    by rw [Icc.add_singleton]
  show Multiset.map (fun x => c + x) (Icc a b) = Multiset.Icc (c + a) (c + b)
  rw [h8, h9]

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

4:12: error: Unknown identifier `on`
4:2: error: Tactic `induction` failed: major premise type is not an inductive type
  ?m.29

Explanation: the `induction` tactic is for constructor-based reasoning as well as for applying custom induction principles with a 'using' clause or a registered '@[induction_eliminator]' theorem. The above type neither is an inductive type nor has a registered theorem.

α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
x✝ : ?m.29
⊢ Multiset.map (fun x => c + x) (Multiset.Icc a b) = Multiset.Icc (c + a) (c + b)

Reference proof

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

lemma map_add_left_Icc (a b c : α) : (Icc a b).map (c + ·) = Icc (c + a) (c + b) := by
  classical rw [Icc, Icc, ← Finset.image_add_left_Icc, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]