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

State before:
sz : ℕ
n m : FinInt sz
⊢ toUint (n + m) =
    match addfull n m with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz
Tactic:
match h: addfull n m with
| .next br r =>
  have h₁ := FinInt.addfull_toUint n m
  rw [h] at h₁
  have h₂: n+m = r := by simp [HAdd.hAdd, add, h]
  cases br <;> simp [h₂] at *
  . exact h₁
  . sorry_arith
State after:
no goals

State before:
sz : ℕ
n m : FinInt sz
br : Bool
r : FinInt sz
h : addfull n m = next br r
⊢ toUint (n + m) =
    match next br r with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz
Tactic:
have h₁ := FinInt.addfull_toUint n m
State after:
sz : ℕ
n m : FinInt sz
br : Bool
r : FinInt sz
h : addfull n m = next br r
h₁ : toUint (addfull n m) = toUint n + toUint m
⊢ toUint (n + m) =
    match next br r with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz

State before:
sz : ℕ
n m : FinInt sz
br : Bool
r : FinInt sz
h : addfull n m = next br r
h₁ : toUint (addfull n m) = toUint n + toUint m
⊢ toUint (n + m) =
    match next br r with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz
Tactic:
rw [h] at h₁
State after:
sz : ℕ
n m : FinInt sz
br : Bool
r : FinInt sz
h : addfull n m = next br r
h₁ : toUint (next br r) = toUint n + toUint m
⊢ toUint (n + m) =
    match next br r with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz

State before:
sz : ℕ
n m : FinInt sz
br : Bool
r : FinInt sz
h : addfull n m = next br r
h₁ : toUint (next br r) = toUint n + toUint m
⊢ toUint (n + m) =
    match next br r with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz
Tactic:
have h₂: n+m = r := by simp [HAdd.hAdd, add, h]
State after:
sz : ℕ
n m : FinInt sz
br : Bool
r : FinInt sz
h : addfull n m = next br r
h₁ : toUint (next br r) = toUint n + toUint m
h₂ : n + m = r
⊢ toUint (n + m) =
    match next br r with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz

State before:
sz : ℕ
n m : FinInt sz
br : Bool
r : FinInt sz
h : addfull n m = next br r
h₁ : toUint (next br r) = toUint n + toUint m
h₂ : n + m = r
⊢ toUint (n + m) =
    match next br r with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz
Tactic:
cases br <;> simp [h₂] at *
State after:
case false
sz : ℕ
n m r : FinInt sz
h : addfull n m = next false r
h₁ : toUint r = toUint n + toUint m
h₂ : True
⊢ toUint r = toUint n + toUint m

case true
sz : ℕ
n m r : FinInt sz
h : addfull n m = next true r
h₂ : True
h₁ : 2 ^ sz + toUint r = toUint n + toUint m
⊢ toUint r = toUint n + toUint m - 2 ^ sz

State before:
case false
sz : ℕ
n m r : FinInt sz
h : addfull n m = next false r
h₁ : toUint r = toUint n + toUint m
h₂ : True
⊢ toUint r = toUint n + toUint m

case true
sz : ℕ
n m r : FinInt sz
h : addfull n m = next true r
h₂ : True
h₁ : 2 ^ sz + toUint r = toUint n + toUint m
⊢ toUint r = toUint n + toUint m - 2 ^ sz
Tactic:
. exact h₁
State after:
case true
sz : ℕ
n m r : FinInt sz
h : addfull n m = next true r
h₂ : True
h₁ : 2 ^ sz + toUint r = toUint n + toUint m
⊢ toUint r = toUint n + toUint m - 2 ^ sz

State before:
case true
sz : ℕ
n m r : FinInt sz
h : addfull n m = next true r
h₂ : True
h₁ : 2 ^ sz + toUint r = toUint n + toUint m
⊢ toUint r = toUint n + toUint m - 2 ^ sz
Tactic:
. sorry_arith
State after:
no goals

State before:
sz : ℕ
n m : FinInt sz
br : Bool
r : FinInt sz
h : addfull n m = next br r
h₁ : toUint (next br r) = toUint n + toUint m
⊢ n + m = r
Tactic:
simp [HAdd.hAdd, add, h]
State after:
no goals