Theorem: FinInt.add_toUint_rem (MLIR/Util/FinInt.lean)

State before:
sz : ℕ
n m : FinInt sz
⊢ toUint (n + m) = if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz
Tactic:
simp [FinInt.add_toUint_msb]
State after:
sz : ℕ
n m : FinInt sz
⊢ (match addfull n m with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz) =
    if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz

State before:
sz : ℕ
n m : FinInt sz
⊢ (match addfull n m with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz) =
    if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz
Tactic:
cases h_full: addfull n m
State after:
case next
sz : ℕ
n m : FinInt sz
a✝¹ : Bool
a✝ : FinInt sz
h_full : addfull n m = next a✝¹ a✝
⊢ (match next a✝¹ a✝ with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz) =
    if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz

State before:
sz : ℕ
n m : FinInt sz
br : Bool
r' : FinInt sz
h_full : addfull n m = next br r'
⊢ (match next br r' with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz) =
    if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz
Tactic:
case next br r' =>
cases br <;> simp
. have h := O_lt r'; rw [←h_full] at h
  simp [FinInt.addfull_toUint] at h; simp [h]
. have h := I_not_lt r'; rw [←h_full] at h; sorry
State after:
no goals

State before:
sz : ℕ
n m : FinInt sz
br : Bool
r' : FinInt sz
h_full : addfull n m = next br r'
⊢ (match next br r' with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz) =
    if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz
Tactic:
cases br <;> simp
State after:
case false
sz : ℕ
n m r' : FinInt sz
h_full : addfull n m = next false r'
⊢ toUint n + toUint m = if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz

case true
sz : ℕ
n m r' : FinInt sz
h_full : addfull n m = next true r'
⊢ toUint n + toUint m - 2 ^ sz =
    if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz

State before:
case false
sz : ℕ
n m r' : FinInt sz
h_full : addfull n m = next false r'
⊢ toUint n + toUint m = if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz

case true
sz : ℕ
n m r' : FinInt sz
h_full : addfull n m = next true r'
⊢ toUint n + toUint m - 2 ^ sz =
    if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz
Tactic:
. have h := O_lt r'; rw [←h_full] at h
  simp [FinInt.addfull_toUint] at h; simp [h]
State after:
case true
sz : ℕ
n m r' : FinInt sz
h_full : addfull n m = next true r'
⊢ toUint n + toUint m - 2 ^ sz =
    if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz

State before:
case true
sz : ℕ
n m r' : FinInt sz
h_full : addfull n m = next true r'
⊢ toUint n + toUint m - 2 ^ sz =
    if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz
Tactic:
. have h := I_not_lt r'; rw [←h_full] at h; sorry
State after:
no goals