awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
h1 : fib (n + 1) = ∑ p ∈ @Finset.antidiagonal _ instAddMonoid _ n, p.1.choose p.2
h2 : fib (n + 1 + 1) = ∑ p ∈ @Finset.antidiagonal _ instAddMonoid _ (n + 1), p.1.choose p.2
⊢ HAdd.hAdd (α := ℕ) (∑ p ∈ @Finset.antidiagonal _ instAddMonoid _ n, p.1.choose p.2)
      (∑
        p ∈
          Finset.cons (n + 1, 0)
            (Finset.map ((Function.Embedding.refl ℕ).prodMap { toFun := succ, inj' := succ_injective : ℕ ↪ ℕ })
              (@Finset.antidiagonal _ instAddMonoid _ n))
            ⋯,
        p.1.choose p.2) =
    ∑
      p ∈
        Finset.cons (0, n + 2)
          (Finset.cons (n + 2, 0)
            (Finset.map
              ({ toFun := succ, inj' := succ_injective : ℕ ↪ ℕ }.prodMap
                { toFun := succ, inj' := succ_injective : ℕ ↪ ℕ })
              (@Finset.antidiagonal _ instAddMonoid _ n))
            ⋯)
          ⋯,
      p.1.choose p.2

Tactic:
simp [choose_succ_succ, Finset.sum_add_distrib, add_left_comm]

Premises used: add_left_comm, Finset.sum_add_distrib, Nat.choose_succ_succ
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
⊢ fib (HAdd.hAdd (α := ℕ) 0 1) = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range 0, fib k) 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
ih : fib (n + 1) = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range n, fib k) 1
⊢ fib (n + 2) = fib n + fib (n + 1)

Tactic:
fib_add_two

Premises used: Nat.fib_add_two
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
ih : fib (n + 1) = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range n, fib k) 1
rw : fib n + HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range n, fib k) 1 = fib n + ∑ k ∈ Finset.range n, fib k + 1
rw₁ rw₂ :
  fib n + HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range n, fib k) 1 =
    fib n + HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range n, fib k) 1
⊢ fib n + fib (n + 1) = fib n + ∑ k ∈ Finset.range n, fib k + 1

Tactic:
rw [ih, add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
ih : fib (n + 1) = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range n, fib k) 1
⊢ fib n + ∑ k ∈ Finset.range n, fib k + 1 = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range (n + 1), fib k) 1

Tactic:
simp [Finset.range_add_one]

Premises used: Finset.range_add_one
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
ih : Nat.fib (n + 1) = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range n, Nat.fib k) 1
fib : Nat.fib n + Nat.fib (n + 1) = Nat.fib n + ∑ k ∈ Finset.range n, Nat.fib k + 1
fib₁ : Nat.fib n + ∑ k ∈ Finset.range n, Nat.fib k + 1 = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range (n + 1), Nat.fib k) 1
⊢ Nat.fib (n + 1 + 1) = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range (n + 1), Nat.fib k) 1

Tactic:
calc
      fib (n + 2) = fib n + fib (n + 1) := fib_add_two
      _ = (fib n + ∑ k ∈ Finset.range n, fib k) + 1 := by rw [ih, add_assoc]
      _ = (∑ k ∈ Finset.range (n + 1), fib k) + 1 := by simp [Finset.range_add_one]

Premises used: Nat.fib_add_two, Finset.range, HAdd.hAdd, Nat.fib, OfNat.ofNat, Finset.sum
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
zero : fib (HAdd.hAdd (α := ℕ) 0 1) = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range 0, fib k) 1
succ :
  ∀ (n : ℕ) (ih : fib (n + 1) = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range n, fib k) 1),
    fib (n + 1 + 1) = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range (n + 1), fib k) 1
⊢ fib (n + 1) = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range n, fib k) 1

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    calc
      fib (n + 2) = fib n + fib (n + 1) := fib_add_two
      _ = (fib n + ∑ k ∈ Finset.range n, fib k) + 1 := by rw [ih, add_assoc]
      _ = (∑ k ∈ Finset.range (n + 1), fib k) + 1 := by simp [Finset.range_add_one]

Premises used: Nat.fib_add_two, Finset.range, HAdd.hAdd, Nat.fib, Nat.zero, OfNat.ofNat, Nat.succ, Finset.sum
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
⊢ IsZeckendorfRep []

Tactic:
simp [IsZeckendorfRep]

Premises used: List.IsZeckendorfRep
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n a : ℕ
l : List ℕ
hl : (a :: l).IsZeckendorfRep
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
⊢ (∀ a' ∈ l ++ [0], a' + 2 ≤ a) ∧ Pairwise (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])

Tactic:
simp only [IsZeckendorfRep, cons_append, isChain_iff_pairwise, pairwise_cons] at hl

Premises used: List.IsZeckendorfRep, List.pairwise_cons, List.isChain_iff_pairwise, List.cons_append
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
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])
⊢ ∀ b ∈ (l ++ [0]).head?, b < a - 1

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
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
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
⊢ ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])

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

Premises used: forall_eq, or_imp, List.mem_singleton, zero_add, List.mem_append, List.isChain_iff_pairwise, forall_and
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
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) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
bc : (map fib l).sum < fib (a - 1)
⊢ fib a + (map fib l).sum < fib a + fib (a - 1)

Tactic:
gcongr
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
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) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
⊢ (map fib l).sum < fib (a - 1)

Tactic:
sum_fib_lt hl.2 this

Premises used: And.right
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
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) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
⊢ (map fib l).sum < fib (a - 1)

Tactic:
exact sum_fib_lt hl.2 this

Premises used: And.right
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
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) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
rw : fib (a + 1) ≤ fib n
⊢ fib a + fib (a - 1) ≤ fib n

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

Premises used: add_comm, LT.lt.ne', And.right, LE.le.trans_lt', And.left, zero_lt_two, Nat.fib_add_one
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
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) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
⊢ fib (a + 1) ≤ fib n

Tactic:
fib_mono (hn _ rfl)

Premises used: Nat.fib_mono, rfl
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
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) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
⊢ fib (a + 1) ≤ fib n

Tactic:
exact fib_mono (hn _ rfl)

Premises used: Nat.fib_mono, rfl
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
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) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
fib : Nat.fib a + (map Nat.fib l).sum < Nat.fib a + Nat.fib (a - 1)
fib₁ : Nat.fib a + Nat.fib (a - 1) ≤ Nat.fib n
⊢ (map Nat.fib (a :: l)).sum < Nat.fib n

Tactic:
calc
      fib a + (map fib l).sum < fib a + fib (a - 1) := by gcongr; exact sum_fib_lt hl.2 this
      _ ≤ fib n := by
        rw [add_comm, ← fib_add_one (hl.1.2.trans_lt' zero_lt_two).ne']; exact fib_mono (hn _ rfl)

Premises used: List.map, List.sum, HSub.hSub, Nat.fib, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n : ℕ
⊢ fib n.greatestFib ≤ n

Tactic:
findGreatest_spec (P := (fun k ↦ fib k ≤ n)) (zero_le _) <| zero_le _

Premises used: Nat.zero_le, Nat.findGreatest_spec, Nat.greatestFib
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
_a _b : ℕ
hab : _a ≤ _b
⊢ _a + 1 ≤ _b + 1

Tactic:
gcongr
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
m n : ℕ
h : fib m ≤ n
⊢ fib m + 1 ≤ n + 1

Tactic:
gcongr
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
m n : ℕ
⊢ m.greatestFib < n ↔ m < fib n

Tactic:
lt_iff_lt_of_le_iff_le le_greatestFib

Premises used: Nat.le_greatestFib, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n : ℕ
⊢ n < fib (n.greatestFib + 1)

Tactic:
greatestFib_lt.1 <| lt_succ_self _

Premises used: Nat.greatestFib_lt, Nat.lt_succ_self, Iff.mp
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n : ℕ
h : n.greatestFib = 0
⊢ n = 0

Tactic:
simpa using findGreatest_eq_zero_iff.1 h zero_lt_one le_add_self

Premises used: Nat.findGreatest_eq_zero_iff, zero_lt_one, Iff.mp, le_add_self
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
⊢ greatestFib 0 = 0

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n : ℕ
⊢ n.greatestFib ≠ 0 ↔ n ≠ 0

Tactic:
greatestFib_eq_zero.not

Premises used: Iff.not, Nat.greatestFib_eq_zero
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n : ℕ
⊢ 0 < n.greatestFib ↔ 0 < n

Tactic:
simp [pos_iff_ne_zero]

Premises used: pos_iff_ne_zero
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n : ℕ
hn : n ≠ 0
rw : n < fib (n.greatestFib + 1)
rw₁ : n.greatestFib ≠ 0
rw₂ : n.greatestFib - 1 ≠ 0
⊢ (n - fib n.greatestFib).greatestFib ≤ n.greatestFib - 2

Tactic:
rw [← Nat.lt_succ_iff, greatestFib_lt, tsub_lt_iff_right n.fib_greatestFib_le, Nat.sub_succ,
    succ_pred, ← fib_add_one]

Premises used: Nat.greatestFib_lt, Nat.succ_pred, Nat.fib_greatestFib_le, tsub_lt_iff_right, Nat.sub_succ, Nat.lt_succ_iff, Nat.fib_add_one
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n : ℕ
hn : n ≠ 0
⊢ n < fib (n.greatestFib + 1)

Tactic:
n.lt_fib_greatestFib_add_one

Premises used: Nat.lt_fib_greatestFib_add_one
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n : ℕ
hn : n ≠ 0
⊢ n < fib (n.greatestFib + 1)

Tactic:
exact n.lt_fib_greatestFib_add_one

Premises used: Nat.lt_fib_greatestFib_add_one
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n : ℕ
hn : n ≠ 0
⊢ n.greatestFib ≠ 0

Tactic:
simpa
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n : ℕ
hn : n ≠ 0
⊢ n.greatestFib - 1 ≠ 0

Tactic:
simpa [← succ_le_iff, tsub_eq_zero_iff_le] using hn.bot_lt

Premises used: tsub_eq_zero_iff_le, Nat.succ_le_iff, Ne.bot_lt
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
m : ℕ
hm : 0 < m
⊢ m - fib m.greatestFib < m

Tactic:
tsub_lt_self hm <| fib_pos.2 <| findGreatest_pos.2 ⟨1, zero_lt_one, le_add_self, hm⟩

Premises used: Iff.mpr, Nat.findGreatest_pos, Nat.fib_pos, zero_lt_one, And.intro, Exists.intro, OfNat.ofNat, le_add_self, tsub_lt_self
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
m n : ℕ
h : m = n + 1
subst_vars : n + 1 - fib (n + 1).greatestFib < n + 1
⊢ m - fib m.greatestFib < n + 1

Tactic:
subst_vars
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n : ℕ
⊢ n + 1 - fib (n + 1).greatestFib < n + 1

Tactic:
apply zeckendorf_aux (zero_lt_succ _)

Premises used: Nat.zero_lt_succ, _private.0.Nat.zeckendorf_aux
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
m n : ℕ
h : m = n + 1
decreasing_by decreasing_by₁ : m - fib m.greatestFib < n + 1
decreasing_by₂ decreasing_by₃ : n + 1 - fib (n + 1).greatestFib < n + 1
⊢ m - fib m.greatestFib < namedPattern m n.succ h

Tactic:
decreasing_by simp_wf; subst_vars; apply zeckendorf_aux (zero_lt_succ _)

Premises used: Nat.zero_lt_succ, _private.0.Nat.zeckendorf_aux
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
⊢ zeckendorf 0 = []

Tactic:
zeckendorf.eq_1 ..

Premises used: Nat.zeckendorf.eq_1
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n : ℕ
⊢ (n + 1).zeckendorf = (n + 1).greatestFib :: (n + 1 - fib (n + 1).greatestFib).zeckendorf

Tactic:
zeckendorf.eq_2 ..

Premises used: Nat.zeckendorf.eq_2
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
⊢ (zeckendorf 0).IsZeckendorfRep

Tactic:
simp only [zeckendorf_zero, IsZeckendorfRep_nil]

Premises used: List.IsZeckendorfRep_nil, Nat.zeckendorf_zero
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n : ℕ
rw : IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) ((n + 1).greatestFib :: ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]))
⊢ (n + 1).zeckendorf.IsZeckendorfRep

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

Premises used: List.IsZeckendorfRep, Nat.zeckendorf_succ, List.cons_append
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n : ℕ
⊢ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) ((n + 1).greatestFib :: ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]))

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

Premises used: List.IsChain.cons
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n : ℕ
refine : ∀ (a : ℕ) (ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?), a + 2 ≤ (n + 1).greatestFib
⊢ IsChain (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 ↦ ?_)

Premises used: List.IsChain.cons
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n a : ℕ
ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?
inl : ∀ (h : n + 1 - fib (n + 1).greatestFib = 0), a + 2 ≤ (n + 1).greatestFib
inr : ∀ (h : n + 1 - fib (n + 1).greatestFib > 0), a + 2 ≤ (n + 1).greatestFib
⊢ a + 2 ≤ (n + 1).greatestFib

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

Premises used: HSub.hSub, Nat.greatestFib, HAdd.hAdd, Nat.fib, OfNat.ofNat, Nat.eq_zero_or_pos
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n a : ℕ
ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?
h : n + 1 - fib (n + 1).greatestFib = 0
⊢ 0 = a

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

Premises used: Nat.zeckendorf_zero, List.head?_cons, List.nil_append, Option.mem_some_iff
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n a : ℕ
h : n + 1 - fib (n + 1).greatestFib = 0
ha : 0 = a
inl : HAdd.hAdd (α := ℕ) 0 2 ≤ (n + 1).greatestFib
⊢ a + 2 ≤ (n + 1).greatestFib

Tactic:
subst ha
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n : ℕ
h : n + 1 - fib (n + 1).greatestFib = 0
⊢ HAdd.hAdd (α := ℕ) 0 2 ≤ (n + 1).greatestFib

Tactic:
le_greatestFib.2 le_add_self

Premises used: Iff.mpr, Nat.le_greatestFib, le_add_self
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n : ℕ
h : n + 1 - fib (n + 1).greatestFib = 0
⊢ HAdd.hAdd (α := ℕ) 0 2 ≤ (n + 1).greatestFib

Tactic:
exact le_greatestFib.2 le_add_self

Premises used: Iff.mpr, Nat.le_greatestFib, le_add_self
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n a : ℕ
ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?
h : n + 1 - fib (n + 1).greatestFib > 0
⊢ (n + 1 - fib (n + 1).greatestFib).greatestFib = a

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

Premises used: List.head?_cons, Option.mem_some_iff, Nat.zeckendorf_of_pos, List.cons_append
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n a : ℕ
ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?
h : n + 1 - fib (n + 1).greatestFib > 0
ha₁ : (n + 1 - fib (n + 1).greatestFib).greatestFib = a
⊢ n + 1 - fib (n + 1).greatestFib > 0

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

Premises used: List.head?_cons, Option.mem_some_iff, Nat.zeckendorf_of_pos, List.cons_append
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n a : ℕ
ha : (n + 1 - fib (n + 1).greatestFib).greatestFib = a
h : n + 1 - fib (n + 1).greatestFib > 0
inr : (n + 1 - fib (n + 1).greatestFib).greatestFib + 2 ≤ (n + 1).greatestFib
⊢ a + 2 ≤ (n + 1).greatestFib

Tactic:
subst a
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n : ℕ
h : n + 1 - fib (n + 1).greatestFib > 0
⊢ (n + 1 - fib (n + 1).greatestFib).greatestFib + 2 ≤ (n + 1).greatestFib

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

Premises used: Iff.mpr, Nat.greatestFib_sub_fib_greatestFib_le_greatestFib, add_le_of_le_tsub_right_of_le, Nat.succ_ne_zero, Nat.le_greatestFib, le_add_self
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
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)

Premises used: Iff.mpr, Nat.greatestFib_sub_fib_greatestFib_le_greatestFib, add_le_of_le_tsub_right_of_le, Nat.succ_ne_zero, Nat.le_greatestFib, le_add_self
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
h : IsZeckendorfRep []
⊢ (map fib []).sum.zeckendorf = []

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

Premises used: List.sum_nil, Nat.zeckendorf_zero, List.map_nil
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
a : ℕ
l : List ℕ
hl : (a :: l).IsZeckendorfRep
⊢ (a :: l).IsZeckendorfRep

Tactic:
have hl' := hl
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
a : ℕ
l : List ℕ
hl hl' : (a :: l).IsZeckendorfRep
⊢ ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ List.Pairwise (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])

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

Premises used: List.IsZeckendorfRep, forall_eq, or_imp, List.mem_singleton, zero_add, List.pairwise_cons, List.mem_append, List.isChain_iff_pairwise, List.cons_append, forall_and
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
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])
⊢ ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])

Tactic:
rw [← isChain_iff_pairwise] at hl

Premises used: List.isChain_iff_pairwise
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
⊢ 0 < a

Tactic:
have ha : 0 < a := hl.1.2.trans_lt' zero_lt_two
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (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]

Premises used: Iff.mpr, true_or, List.map, add_tsub_cancel_left, Nat.fib_pos, And.right, List.sum_cons, add_pos_iff, Nat.zeckendorf_of_pos
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
ha : 0 < a
suffices : (fib a + (map fib l).sum).greatestFib = 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]
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
ha : 0 < a
simp :
  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
⊢ (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]

Premises used: not_le, zero_le, forall_true_left, add_assoc, ne_eq, add_comm, LT.lt.ne', Nat.greatestFib, not_false_eq_true, Nat.findGreatest_eq_iff, le_add_iff_nonneg_left, true_and
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (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:
⟨le_add_of_le_right <| le_fib_add_one _, fun n hn _ ↦ ?_⟩

Premises used: le_add_of_le_right, And.intro, Nat.le_fib_add_one
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
ha : 0 < a
refine : ∀ (n : ℕ) (hn : a < n), n ≤ (map fib l).sum + (fib a + 1) → (map fib l).sum + fib a < fib n
⊢ 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 _ ↦ ?_⟩
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
ha : 0 < a
n : ℕ
hn : a < n
h : n ≤ (map fib l).sum + (fib a + 1)
rw : (map fib (a :: l)).sum < fib n
⊢ (map fib l).sum + fib a < fib n

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

Premises used: List.map_cons, add_comm, List.sum_cons
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
ha : 0 < a
n : ℕ
hn : a < n
h : n ≤ (map fib l).sum + (fib a + 1)
⊢ ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n

Tactic:
simpa
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
ha : 0 < a
n : ℕ
hn : a < n
h : n ≤ (map fib l).sum + (fib a + 1)
⊢ (map fib (a :: l)).sum < fib n

Tactic:
exact hl'.sum_fib_lt (by simpa)

Premises used: List.IsZeckendorfRep.sum_fib_lt
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n : ℕ
case1 : (map fib (zeckendorf 0)).sum = 0
case2 :
  ∀ (n : ℕ),
    (map fib (n + 1 - fib (n + 1).greatestFib).zeckendorf).sum = n + 1 - fib (n + 1).greatestFib →
      (map fib n.succ.zeckendorf).sum = n.succ
⊢ (map fib n.zeckendorf).sum = n

Tactic:
induction n using zeckendorf.induct

Premises used: Nat.zeckendorf.induct
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
⊢ (map fib (zeckendorf 0)).sum = 0

Tactic:
simp_all [fib_greatestFib_le]

Premises used: Nat.fib_greatestFib_le
-- Module: Mathlib.Data.Nat.Fib.Zeckendorf
Goal:
n : ℕ
ih1 : (map fib (n + 1 - fib (n + 1).greatestFib).zeckendorf).sum = n + 1 - fib (n + 1).greatestFib
⊢ (map fib n.succ.zeckendorf).sum = n.succ

Tactic:
simp_all [fib_greatestFib_le]

Premises used: Nat.fib_greatestFib_le
-- Module: Mathlib.Data.Nat.Find
Goal:
m_1 n_1 k_1 : ℕ
p q : ℕ → Prop
inst : DecidablePred p
H : ∃ (n : ℕ), p n
n : ℕ
pn : p n
m_2 m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc (lbp (p := p)) k
k : ℕ
kn : n ≤ k + m.succ
y : ℕ
r : y.lbp (p := p) k
_a : ∀ (k_2 : ℕ), k_2 ≤ k → ¬p k_2
rw : n ≤ k + m + 1
⊢ n ≤ k + 1 + m

Tactic:
rw [Nat.add_right_comm]

Premises used: Nat.add_right_comm
-- Module: Mathlib.Data.Nat.Find
Goal:
m_1 n_1 k_1 : ℕ
p q : ℕ → Prop
inst : DecidablePred p
H : ∃ (n : ℕ), p n
n : ℕ
pn : p n
m_2 m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc (lbp (p := p)) k
k : ℕ
kn : n ≤ k + m.succ
y : ℕ
r : y.lbp (p := p) k
_a : ∀ (k_2 : ℕ), k_2 ≤ k → ¬p k_2
⊢ n ≤ k + m + 1

Tactic:
kn
-- Module: Mathlib.Data.Nat.Find
Goal:
m_1 n_1 k_1 : ℕ
p q : ℕ → Prop
inst : DecidablePred p
H : ∃ (n : ℕ), p n
n : ℕ
pn : p n
m_2 m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc (lbp (p := p)) k
k : ℕ
kn : n ≤ k + m.succ
y : ℕ
r : y.lbp (p := p) k
_a : ∀ (k_2 : ℕ), k_2 ≤ k → ¬p k_2
⊢ n ≤ k + m + 1

Tactic:
exact kn
-- Module: Mathlib.Data.Nat.Find
Goal:
m_1 n_1 k : ℕ
p q : ℕ → Prop
inst : DecidablePred p
H : ∃ (n : ℕ), p n
m : ℕ
IH :
  (y : ℕ) → y.lbp (p := p) m → (fun (k : ℕ) ↦ (∀ (n : ℕ), n < k → ¬p n) → { n : ℕ // p n ∧ ∀ (m : ℕ), m < n → ¬p m }) y
al : ∀ (n : ℕ), n < m → ¬p n
pm : ¬p m
n : ℕ
h : n ≤ m
e : n = m
rw : ¬p m
⊢ ¬p n

Tactic:
rw [e]