-- Mathlib/Data/Nat/Fib/Zeckendorf.lean
lemma IsZeckendorfRep.sum_fib_lt : ∀ {n l}, IsZeckendorfRep l → (∀ a ∈ (l ++ [0]).head?, a < n) →
    (l.map fib).sum < fib n
  | _, [], _, hn => fib_pos.2 <| hn _ rfl
  | n, a :: l, hl, hn => by
    simp only [IsZeckendorfRep, cons_append, chain'_iff_pairwise, pairwise_cons] at hl
    have : ∀ b, b ∈ head? (l ++ [0]) → b < a - 1 :=
      fun b hb ↦ lt_tsub_iff_right.2 <| hl.1 _ <| mem_of_mem_head? hb
    simp only [mem_append, mem_singleton, ← chain'_iff_pairwise, or_imp, forall_and, forall_eq,
      zero_add] at hl
    simp only [map, List.sum_cons]
    refine (add_lt_add_left (sum_fib_lt hl.2 this) _).trans_le ?_
    rw [add_comm, ← fib_add_one (hl.1.2.trans_lt' zero_lt_two).ne']
    exact fib_mono (hn _ rfl)

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

Tactic:
refine (add_lt_add_left (sum_fib_lt hl.2 this) _).trans_le ?_

Result:
n a : ℕ
l : List ℕ
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
this : ∀ b ∈ (l ++ [0]).head?, b < a - 1
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])
⊢ fib a + fib (a - 1) ≤ fib n

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

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

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

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

Tactic:
rw [add_comm, ← fib_add_one (hl.1.2.trans_lt' zero_lt_two).ne']

Result:
n a : ℕ
l : List ℕ
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
this : ∀ b ∈ (l ++ [0]).head?, b < a - 1
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])
⊢ fib (a + 1) ≤ fib n

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

Tactic:
simp only [map, List.sum_cons]

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

Proof state:
n a : ℕ
l : List ℕ
hl : (a :: l).IsZeckendorfRep
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
⊢ (map fib (a :: l)).sum < fib n

Tactic:
simp only [IsZeckendorfRep, cons_append, chain'_iff_pairwise, pairwise_cons] at hl

Result:
n a : ℕ
l : List ℕ
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
hl : (∀ a' ∈ l ++ [0], a' + 2 ≤ a) ∧ Pairwise (fun a b => b + 2 ≤ a) (l ++ [0])
⊢ (map fib (a :: l)).sum < fib n

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

Tactic:
have : ∀ b, b ∈ head? (l ++ [0]) → b < a - 1 :=
  fun b hb ↦ lt_tsub_iff_right.2 <| hl.1 _ <| mem_of_mem_head? hb

Result:
n a : ℕ
l : List ℕ
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
hl : (∀ a' ∈ l ++ [0], a' + 2 ≤ a) ∧ Pairwise (fun a b => b + 2 ≤ a) (l ++ [0])
this : ∀ b ∈ (l ++ [0]).head?, b < a - 1
⊢ (map fib (a :: l)).sum < fib n

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

Tactic:
exact fib_mono (hn _ rfl)

Result:
no goals