no goals
α : Type u
β : Type v
γ : Type w
as : List α
n : Nat
⊢ length as + n = lengthTRAux as n
induction as generalizing n with
| nil  => simp [length, lengthTRAux]
| cons a as ih =>
  simp [length, lengthTRAux, ← ih, Nat.succ_add]
  rfl
no goals
case nil
α : Type u
β : Type v
γ : Type w
n : Nat
⊢ length nil + n = lengthTRAux nil n
simp [length, lengthTRAux]
case cons
α : Type u
β : Type v
γ : Type w
a : α
as : List α
ih : ∀ (n : Nat), length as + n = lengthTRAux as n
n : Nat
⊢ Nat.succ (length as + n) = length as + Nat.succ n
case cons
α : Type u
β : Type v
γ : Type w
a : α
as : List α
ih : ∀ (n : Nat), length as + n = lengthTRAux as n
n : Nat
⊢ length (a :: as) + n = lengthTRAux (a :: as) n
simp [length, lengthTRAux, ← ih, Nat.succ_add]
no goals
case cons
α : Type u
β : Type v
γ : Type w
a : α
as : List α
ih : ∀ (n : Nat), length as + n = lengthTRAux as n
n : Nat
⊢ Nat.succ (length as + n) = length as + Nat.succ n
rfl