case nil
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf ([] ++ L2) < sizeOf ([] ++ (x, b) :: (x, !b) :: L2)

case cons
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
hd : α × Bool
tl : List (α × Bool)
ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
⊢ sizeOf (hd :: tl ++ L2) < sizeOf (hd :: tl ++ (x, b) :: (x, !b) :: L2)
α : Type u
L L₁ L₂ L₃ L₄ L1 L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf (L1 ++ L2) < sizeOf (L1 ++ (x, b) :: (x, !b) :: L2)
induction' L1 with hd tl ih
case cons
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
hd : α × Bool
tl : List (α × Bool)
ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
⊢ sizeOf (hd :: tl ++ L2) < sizeOf (hd :: tl ++ (x, b) :: (x, !b) :: L2)
case nil
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf ([] ++ L2) < sizeOf ([] ++ (x, b) :: (x, !b) :: L2)

case cons
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
hd : α × Bool
tl : List (α × Bool)
ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
⊢ sizeOf (hd :: tl ++ L2) < sizeOf (hd :: tl ++ (x, b) :: (x, !b) :: L2)
case nil =>
  dsimp
  simp only [Bool.sizeOf_eq_one]
  have H :
    1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2) =
      sizeOf L2 + (1 + ((1 + 1) + (1 + 1) + 1)) :=
    by ac_rfl
  rw [H]
  apply Nat.lt_add_of_pos_right
  apply Nat.lt_add_right
  apply Nat.zero_lt_one
no goals
case cons
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
hd : α × Bool
tl : List (α × Bool)
ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
⊢ sizeOf (hd :: tl ++ L2) < sizeOf (hd :: tl ++ (x, b) :: (x, !b) :: L2)
case cons =>
  dsimp
  exact Nat.add_lt_add_left ih _
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf L2 < 1 + (1 + sizeOf b) + (1 + (1 + sizeOf !b) + sizeOf L2)
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf ([] ++ L2) < sizeOf ([] ++ (x, b) :: (x, !b) :: L2)
dsimp
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf L2 < 1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2)
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf L2 < 1 + (1 + sizeOf b) + (1 + (1 + sizeOf !b) + sizeOf L2)
simp only [Bool.sizeOf_eq_one]
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
H : 1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2) = sizeOf L2 + (1 + (1 + 1 + (1 + 1) + 1))
⊢ sizeOf L2 < 1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2)
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf L2 < 1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2)
have H :
  1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2) =
    sizeOf L2 + (1 + ((1 + 1) + (1 + 1) + 1)) :=
  by ac_rfl
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
H : 1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2) = sizeOf L2 + (1 + (1 + 1 + (1 + 1) + 1))
⊢ sizeOf L2 < sizeOf L2 + (1 + (1 + 1 + (1 + 1) + 1))
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
H : 1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2) = sizeOf L2 + (1 + (1 + 1 + (1 + 1) + 1))
⊢ sizeOf L2 < 1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2)
rw [H]
case h
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
H : 1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2) = sizeOf L2 + (1 + (1 + 1 + (1 + 1) + 1))
⊢ 0 < 1 + (1 + 1 + (1 + 1) + 1)
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
H : 1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2) = sizeOf L2 + (1 + (1 + 1 + (1 + 1) + 1))
⊢ sizeOf L2 < sizeOf L2 + (1 + (1 + 1 + (1 + 1) + 1))
apply Nat.lt_add_of_pos_right
case h.h
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
H : 1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2) = sizeOf L2 + (1 + (1 + 1 + (1 + 1) + 1))
⊢ 0 < 1
case h
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
H : 1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2) = sizeOf L2 + (1 + (1 + 1 + (1 + 1) + 1))
⊢ 0 < 1 + (1 + 1 + (1 + 1) + 1)
apply Nat.lt_add_right
no goals
case h.h
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
H : 1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2) = sizeOf L2 + (1 + (1 + 1 + (1 + 1) + 1))
⊢ 0 < 1
apply Nat.zero_lt_one
no goals
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
⊢ 1 + (1 + 1) + (1 + (1 + 1) + sizeOf L2) = sizeOf L2 + (1 + (1 + 1 + (1 + 1) + 1))
ac_rfl
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
hd : α × Bool
tl : List (α × Bool)
ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
⊢ 1 + sizeOf hd + sizeOf (tl ++ L2) < 1 + sizeOf hd + sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
hd : α × Bool
tl : List (α × Bool)
ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
⊢ sizeOf (hd :: tl ++ L2) < sizeOf (hd :: tl ++ (x, b) :: (x, !b) :: L2)
dsimp
no goals
α : Type u
L L₁ L₂ L₃ L₄ L2 : List (α × Bool)
x : α
b : Bool
hd : α × Bool
tl : List (α × Bool)
ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
⊢ 1 + sizeOf hd + sizeOf (tl ++ L2) < 1 + sizeOf hd + sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
exact Nat.add_lt_add_left ih _