Theorem: List1.IndView.sizeOf_toList1 (GMLInit/Data/List/List1.lean)

State before:
α : Type u_1
β : Type ?u.12658
xs : List1.IndView α
⊢ sizeOf xs.toList1 = 2 + sizeOf xs
Tactic:
induction xs with
| pure x => rw [toList1]; rfl
| cons x xs ih => rw [toList1, List1.sizeOf_cons, ←sizeOf_toList, ih, Nat.add_left_comm]; rfl
State after:
no goals

State before:
case pure
α : Type u_1
β : Type ?u.12658
x : α
⊢ sizeOf (pure x).toList1 = 2 + sizeOf (pure x)
Tactic:
rw [toList1]
State after:
case pure
α : Type u_1
β : Type ?u.12658
x : α
⊢ sizeOf (List1.cons x []) = 2 + sizeOf (pure x)

State before:
case pure
α : Type u_1
β : Type ?u.12658
x : α
⊢ sizeOf (List1.cons x []) = 2 + sizeOf (pure x)
Tactic:
rfl
State after:
no goals

State before:
case cons
α : Type u_1
β : Type ?u.12658
x : α
xs : List1.IndView α
ih : sizeOf xs.toList1 = 2 + sizeOf xs
⊢ sizeOf (cons x xs).toList1 = 2 + sizeOf (cons x xs)
Tactic:
rw [toList1, List1.sizeOf_cons, ←sizeOf_toList, ih, Nat.add_left_comm]
State after:
case cons
α : Type u_1
β : Type ?u.12658
x : α
xs : List1.IndView α
ih : sizeOf xs.toList1 = 2 + sizeOf xs
⊢ 2 + (1 + sizeOf xs) = 2 + sizeOf (cons x xs)

State before:
case cons
α : Type u_1
β : Type ?u.12658
x : α
xs : List1.IndView α
ih : sizeOf xs.toList1 = 2 + sizeOf xs
⊢ 2 + (1 + sizeOf xs) = 2 + sizeOf (cons x xs)
Tactic:
rfl
State after:
no goals