Theorem: Day09.toDiffs_length_lt (Aoc2023/Day09.lean)

State before:
as : List Int
h : as ≠ []
⊢ List.length (toDiffs as h).snd < List.length as
Tactic:
match as with
| [] => exact False.elim (h rfl)
| _ :: [] => simp [toDiffs]
| head :: neck :: tail =>
  simp only [toDiffs]
  refine Nat.succ_lt_succ ?_
  calc _ < (neck :: tail).length := toDiffs_length_lt _ (by simp)
       _ = tail.length + 1 := by simp
State after:
no goals

State before:
as : List Int
h : [] ≠ []
⊢ List.length (toDiffs [] h).snd < List.length []
Tactic:
exact False.elim (h rfl)
State after:
no goals

State before:
as : List Int
head✝ : Int
h : [head✝] ≠ []
⊢ List.length (toDiffs [head✝] h).snd < List.length [head✝]
Tactic:
simp [toDiffs]
State after:
no goals

State before:
as : List Int
head neck : Int
tail : List Int
h : head :: neck :: tail ≠ []
⊢ List.length (toDiffs (head :: neck :: tail) h).snd < List.length (head :: neck :: tail)
Tactic:
simp only [toDiffs]
State after:
as : List Int
head neck : Int
tail : List Int
h : head :: neck :: tail ≠ []
⊢ List.length
      (((toDiffs (neck :: tail) (_ : ¬neck :: tail = [])).fst - head) ::
        (toDiffs (neck :: tail) (_ : ¬neck :: tail = [])).snd) <
    List.length (head :: neck :: tail)

State before:
as : List Int
head neck : Int
tail : List Int
h : head :: neck :: tail ≠ []
⊢ List.length
      (((toDiffs (neck :: tail) (_ : ¬neck :: tail = [])).fst - head) ::
        (toDiffs (neck :: tail) (_ : ¬neck :: tail = [])).snd) <
    List.length (head :: neck :: tail)
Tactic:
refine Nat.succ_lt_succ ?_
State after:
as : List Int
head neck : Int
tail : List Int
h : head :: neck :: tail ≠ []
⊢ List.length (toDiffs (neck :: tail) (_ : ¬neck :: tail = [])).snd < List.length (neck :: tail)

State before:
as : List Int
head neck : Int
tail : List Int
h : head :: neck :: tail ≠ []
⊢ List.length (toDiffs (neck :: tail) (_ : ¬neck :: tail = [])).snd < List.length (neck :: tail)
Tactic:
calc _ < (neck :: tail).length := toDiffs_length_lt _ (by simp)
     _ = tail.length + 1 := by simp
State after:
no goals

State before:
as : List Int
head neck : Int
tail : List Int
h : head :: neck :: tail ≠ []
⊢ neck :: tail ≠ []
Tactic:
simp
State after:
no goals

State before:
as : List Int
head neck : Int
tail : List Int
h : head :: neck :: tail ≠ []
⊢ List.length (neck :: tail) = List.length tail + 1
Tactic:
simp
State after:
no goals