-- Mathlib/Data/Nat/Fib/Zeckendorf.lean
lemma isZeckendorfRep_zeckendorf : ∀ n, (zeckendorf n).IsZeckendorfRep
  | 0 => by simp only [zeckendorf_zero, IsZeckendorfRep_nil]
  | n + 1 => by
    rw [zeckendorf_succ, IsZeckendorfRep, List.cons_append]
    refine (isZeckendorfRep_zeckendorf _).cons' (fun a ha ↦ ?_)
    obtain h | h := eq_zero_or_pos (n + 1 - fib (greatestFib (n + 1)))
    · simp only [h, zeckendorf_zero, nil_append, head?_cons, Option.mem_some_iff] at ha
      subst ha
      exact le_greatestFib.2 le_add_self
    rw [zeckendorf_of_pos h, cons_append, head?_cons, Option.mem_some_iff] at ha
    subst a
    exact add_le_of_le_tsub_right_of_le (le_greatestFib.2 le_add_self)
      (greatestFib_sub_fib_greatestFib_le_greatestFib n.succ_ne_zero)

Proof state:
n a : ℕ
ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?
⊢ a + 2 ≤ (n + 1).greatestFib

Tactic:
obtain h | h := eq_zero_or_pos (n + 1 - fib (greatestFib (n + 1)))

Result:
case inl
n a : ℕ
ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?
h : n + 1 - fib (n + 1).greatestFib = 0
⊢ a + 2 ≤ (n + 1).greatestFib

case inr
n a : ℕ
ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?
h : n + 1 - fib (n + 1).greatestFib > 0
⊢ a + 2 ≤ (n + 1).greatestFib

Proof state:
n : ℕ
⊢ (n + 1).zeckendorf.IsZeckendorfRep

Tactic:
rw [zeckendorf_succ, IsZeckendorfRep, List.cons_append]

Result:
n : ℕ
⊢ Chain' (fun a b => b + 2 ≤ a) ((n + 1).greatestFib :: ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]))

Proof state:
case inr
n a : ℕ
ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?
h : n + 1 - fib (n + 1).greatestFib > 0
⊢ a + 2 ≤ (n + 1).greatestFib

Tactic:
rw [zeckendorf_of_pos h, cons_append, head?_cons, Option.mem_some_iff] at ha

Result:
case inr
n a : ℕ
ha : (n + 1 - fib (n + 1).greatestFib).greatestFib = a
h : n + 1 - fib (n + 1).greatestFib > 0
⊢ a + 2 ≤ (n + 1).greatestFib

Proof state:
n : ℕ
⊢ Chain' (fun a b => b + 2 ≤ a) ((n + 1).greatestFib :: ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]))

Tactic:
refine (isZeckendorfRep_zeckendorf _).cons' (fun a ha ↦ ?_)

Result:
n a : ℕ
ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?
⊢ a + 2 ≤ (n + 1).greatestFib

Proof state:
case inl
n a : ℕ
h : n + 1 - fib (n + 1).greatestFib = 0
ha : 0 = a
⊢ a + 2 ≤ (n + 1).greatestFib

Tactic:
subst ha

Result:
case inl
n : ℕ
h : n + 1 - fib (n + 1).greatestFib = 0
⊢ 0 + 2 ≤ (n + 1).greatestFib

Proof state:
case inr
n : ℕ
h : n + 1 - fib (n + 1).greatestFib > 0
⊢ (n + 1 - fib (n + 1).greatestFib).greatestFib + 2 ≤ (n + 1).greatestFib

Tactic:
exact add_le_of_le_tsub_right_of_le (le_greatestFib.2 le_add_self)
  (greatestFib_sub_fib_greatestFib_le_greatestFib n.succ_ne_zero)

Result:
no goals

Proof state:
⊢ (zeckendorf 0).IsZeckendorfRep

Tactic:
simp only [zeckendorf_zero, IsZeckendorfRep_nil]

Result:
no goals

Proof state:
case inl
n : ℕ
h : n + 1 - fib (n + 1).greatestFib = 0
⊢ 0 + 2 ≤ (n + 1).greatestFib

Tactic:
exact le_greatestFib.2 le_add_self

Result:
no goals

Proof state:
case inr
n a : ℕ
ha : (n + 1 - fib (n + 1).greatestFib).greatestFib = a
h : n + 1 - fib (n + 1).greatestFib > 0
⊢ a + 2 ≤ (n + 1).greatestFib

Tactic:
subst a

Result:
case inr
n : ℕ
h : n + 1 - fib (n + 1).greatestFib > 0
⊢ (n + 1 - fib (n + 1).greatestFib).greatestFib + 2 ≤ (n + 1).greatestFib

Proof state:
case inl
n a : ℕ
ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?
h : n + 1 - fib (n + 1).greatestFib = 0
⊢ a + 2 ≤ (n + 1).greatestFib

Tactic:
simp only [h, zeckendorf_zero, nil_append, head?_cons, Option.mem_some_iff] at ha

Result:
case inl
n a : ℕ
h : n + 1 - fib (n + 1).greatestFib = 0
ha : 0 = a
⊢ a + 2 ≤ (n + 1).greatestFib