cf : Code
⊢ encodeCode cf < 2 * (2 * encodeCode cf + 1) + 1 + 4
cf : Code
⊢ encode cf < encode (rfind' cf)
simp [encodeCode_eq, encodeCode]
cf : Code
this : 1 * encodeCode cf ≤ 2 * 2 * encodeCode cf
⊢ encodeCode cf < 2 * (2 * encodeCode cf + 1) + 1 + 4
cf : Code
⊢ encodeCode cf < 2 * (2 * encodeCode cf + 1) + 1 + 4
have := Nat.mul_le_mul_right cf.encodeCode (by decide : 1 ≤ 2 * 2)
cf : Code
this : encodeCode cf ≤ 2 * (2 * encodeCode cf)
⊢ encodeCode cf < 2 * (2 * encodeCode cf + 1) + 1 + 4
cf : Code
this : 1 * encodeCode cf ≤ 2 * 2 * encodeCode cf
⊢ encodeCode cf < 2 * (2 * encodeCode cf + 1) + 1 + 4
rw [one_mul, mul_assoc] at this
cf : Code
this : encodeCode cf ≤ 2 * (2 * encodeCode cf)
⊢ 2 * (2 * encodeCode cf) ≤ 2 * (2 * encodeCode cf + 1) + 1
cf : Code
this : encodeCode cf ≤ 2 * (2 * encodeCode cf)
⊢ encodeCode cf < 2 * (2 * encodeCode cf + 1) + 1 + 4
refine' lt_of_le_of_lt (le_trans this _) (lt_add_of_pos_right _ (by decide : 0 < 4))
no goals
cf : Code
this : encodeCode cf ≤ 2 * (2 * encodeCode cf)
⊢ 2 * (2 * encodeCode cf) ≤ 2 * (2 * encodeCode cf + 1) + 1
exact le_of_lt (Nat.lt_succ_of_le <| Nat.mul_le_mul_left _ <| le_of_lt <|
  Nat.lt_succ_of_le <| Nat.mul_le_mul_left _ <| le_rfl)
no goals
cf : Code
⊢ 1 ≤ 2 * 2
decide
no goals
cf : Code
this : encodeCode cf ≤ 2 * (2 * encodeCode cf)
⊢ 0 < 4
decide