-- Mathlib/Data/Nat/Fib/Zeckendorf.lean
lemma zeckendorf_sum_fib : ∀ {l}, IsZeckendorfRep l → zeckendorf (l.map fib).sum = l
  | [], _ => by simp only [map_nil, List.sum_nil, zeckendorf_zero]
  | a :: l, hl => by
    have hl' := hl
    simp only [IsZeckendorfRep, cons_append, chain'_iff_pairwise, pairwise_cons, mem_append,
      mem_singleton, or_imp, forall_and, forall_eq, zero_add] at hl
    rw [← chain'_iff_pairwise] at hl
    have ha : 0 < a := hl.1.2.trans_lt' zero_lt_two
    suffices h : greatestFib (fib a + sum (map fib l)) = a by
      simp only [map, List.sum_cons, add_pos_iff, fib_pos.2 ha, true_or, zeckendorf_of_pos, h,
      add_tsub_cancel_left, zeckendorf_sum_fib hl.2]
    simp only [add_comm, add_assoc, greatestFib, findGreatest_eq_iff, ne_eq, ha.ne',
      not_false_eq_true, le_add_iff_nonneg_left, _root_.zero_le, forall_true_left, not_le, true_and]
    refine ⟨le_add_of_le_right <| le_fib_add_one _, fun n hn _ ↦ ?_⟩
    rw [add_comm, ← List.sum_cons, ← map_cons]
    exact hl'.sum_fib_lt (by simpa)

Proof state:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])
ha : 0 < a
⊢ a ≤ (map fib l).sum + (fib a + 1) ∧
    ∀ ⦃n : ℕ⦄, a < n → n ≤ (map fib l).sum + (fib a + 1) → (map fib l).sum + fib a < fib n

Tactic:
refine ⟨le_add_of_le_right <| le_fib_add_one _, fun n hn _ ↦ ?_⟩

Result:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])
ha : 0 < a
n : ℕ
hn : a < n
x✝ : n ≤ (map fib l).sum + (fib a + 1)
⊢ (map fib l).sum + fib a < fib n

Proof state:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])
ha : 0 < a
n : ℕ
hn : a < n
x✝ : n ≤ (map fib l).sum + (fib a + 1)
⊢ ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n

Tactic:
simpa

Result:
no goals

Proof state:
a : ℕ
l : List ℕ
hl : (a :: l).IsZeckendorfRep
⊢ (map fib (a :: l)).sum.zeckendorf = a :: l

Tactic:
have hl' := hl

Result:
a : ℕ
l : List ℕ
hl hl' : (a :: l).IsZeckendorfRep
⊢ (map fib (a :: l)).sum.zeckendorf = a :: l

Proof state:
a : ℕ
l : List ℕ
hl hl' : (a :: l).IsZeckendorfRep
⊢ (map fib (a :: l)).sum.zeckendorf = a :: l

Tactic:
simp only [IsZeckendorfRep, cons_append, chain'_iff_pairwise, pairwise_cons, mem_append,
  mem_singleton, or_imp, forall_and, forall_eq, zero_add] at hl

Result:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ List.Pairwise (fun a b => b + 2 ≤ a) (l ++ [0])
⊢ (map fib (a :: l)).sum.zeckendorf = a :: l

Proof state:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])
ha : 0 < a
h : (fib a + (map fib l).sum).greatestFib = a
⊢ (map fib (a :: l)).sum.zeckendorf = a :: l

Tactic:
simp only [map, List.sum_cons, add_pos_iff, fib_pos.2 ha, true_or, zeckendorf_of_pos, h,
add_tsub_cancel_left, zeckendorf_sum_fib hl.2]

Result:
no goals

Proof state:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])
ha : 0 < a
n : ℕ
hn : a < n
x✝ : n ≤ (map fib l).sum + (fib a + 1)
⊢ (map fib (a :: l)).sum < fib n

Tactic:
exact hl'.sum_fib_lt (by simpa)

Result:
no goals

Proof state:
x✝ : [].IsZeckendorfRep
⊢ (map fib []).sum.zeckendorf = []

Tactic:
simp only [map_nil, List.sum_nil, zeckendorf_zero]

Result:
no goals

Proof state:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])
⊢ (map fib (a :: l)).sum.zeckendorf = a :: l

Tactic:
have ha : 0 < a := hl.1.2.trans_lt' zero_lt_two

Result:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])
ha : 0 < a
⊢ (map fib (a :: l)).sum.zeckendorf = a :: l

Proof state:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ List.Pairwise (fun a b => b + 2 ≤ a) (l ++ [0])
⊢ (map fib (a :: l)).sum.zeckendorf = a :: l

Tactic:
rw [← chain'_iff_pairwise] at hl

Result:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])
⊢ (map fib (a :: l)).sum.zeckendorf = a :: l

Proof state:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])
ha : 0 < a
n : ℕ
hn : a < n
x✝ : n ≤ (map fib l).sum + (fib a + 1)
⊢ (map fib l).sum + fib a < fib n

Tactic:
rw [add_comm, ← List.sum_cons, ← map_cons]

Result:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])
ha : 0 < a
n : ℕ
hn : a < n
x✝ : n ≤ (map fib l).sum + (fib a + 1)
⊢ (map fib (a :: l)).sum < fib n

Proof state:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])
ha : 0 < a
⊢ (fib a + (map fib l).sum).greatestFib = a

Tactic:
simp only [add_comm, add_assoc, greatestFib, findGreatest_eq_iff, ne_eq, ha.ne',
  not_false_eq_true, le_add_iff_nonneg_left, _root_.zero_le, forall_true_left, not_le, true_and]

Result:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])
ha : 0 < a
⊢ a ≤ (map fib l).sum + (fib a + 1) ∧
    ∀ ⦃n : ℕ⦄, a < n → n ≤ (map fib l).sum + (fib a + 1) → (map fib l).sum + fib a < fib n

Proof state:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])
ha : 0 < a
⊢ (map fib (a :: l)).sum.zeckendorf = a :: l

Tactic:
suffices h : greatestFib (fib a + sum (map fib l)) = a by
  simp only [map, List.sum_cons, add_pos_iff, fib_pos.2 ha, true_or, zeckendorf_of_pos, h,
  add_tsub_cancel_left, zeckendorf_sum_fib hl.2]

Result:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])
ha : 0 < a
⊢ (fib a + (map fib l).sum).greatestFib = a