internlm/Lean-Github huggingface dataset:
Theorem: FinInt.addfull_toSint
Proof state before:
sz : ℕ
bn : Bool
n' : FinInt sz
bm : Bool
m' : FinInt sz
⊢ toSint (addfull (next bn n') (next bm m')) =
    match next bn n', next bm m' with
    | next false n'_1, next false m'_1 => toSint (next bn n') + toSint (next bm m')
    | next false n'_1, next true m'_1 =>
      match addfull (next bn n') (next bm m') with
      | next false a => toSint (next bn n') + toSint (next bm m') + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint (next bm m') - 2 ^ (sz + 1)
    | next true n'_1, next false m'_1 =>
      match addfull (next bn n') (next bm m') with
      | next false a => toSint (next bn n') + toSint (next bm m') + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint (next bm m') - 2 ^ (sz + 1)
    | next true n'_1, next true m'_1 => toSint (next bn n') + toSint (next bm m')
Tactic:
cases bn <;> cases bm <;> simp [addfull]
Proof state after:
case false.false
sz : ℕ
n' m' : FinInt sz
⊢ toSint
      (match addfull n' m' with
      | next false r => next false (next false r)
      | next true r => next false (next true r)) =
    toSint (next false n') + toSint (next false m')

case false.true
sz : ℕ
n' m' : FinInt sz
⊢ toSint
      (match addfull n' m' with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r)) =
    match
      match addfull n' m' with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r) with
    | next false a => toSint (next false n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next false n') + toSint (next true m') - 2 ^ (sz + 1)

case true.false
sz : ℕ
n' m' : FinInt sz
⊢ toSint
      (match addfull n' m' with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r)) =
    match
      match addfull n' m' with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r) with
    | next false a => toSint (next true n') + toSint (next false m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next false m') - 2 ^ (sz + 1)

case true.true
sz : ℕ
n' m' : FinInt sz
⊢ toSint
      (match addfull n' m' with
      | next false r => next true (next false r)
      | next true r => next true (next true r)) =
    toSint (next true n') + toSint (next true m')
Theorem: FinInt.addfull_toSint
Proof state before:
sz : ℕ
n' m' : FinInt sz
⊢ toSint
      (match addfull n' m' with
      | next false r => next false (next false r)
      | next true r => next false (next true r)) =
    toSint (next false n') + toSint (next false m')
Tactic:
case false.false =>
  match h: addfull n' m' with
  | .next br r =>
    cases br <;> simp [toSint, ←FinInt.addfull_toUint, h]
Proof state after:
no goals
Theorem: FinInt.addfull_toSint
Proof state before:
sz : ℕ
n' m' : FinInt sz
⊢ toSint
      (match addfull n' m' with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r)) =
    match
      match addfull n' m' with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r) with
    | next false a => toSint (next false n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next false n') + toSint (next true m') - 2 ^ (sz + 1)
Tactic:
case false.true =>
  match h: addfull n' m' with
  | .next br r =>
    have h' := FinInt.addfull_toUint n' m'
    rw [h] at h'
    cases br <;> simp at h' <;> simp [toSint]
    . simp [h']; sorry_arith
    . sorry_arith
Proof state after:
no goals
Theorem: FinInt.addfull_toSint
Proof state before:
sz : ℕ
n' m' : FinInt sz
⊢ toSint
      (match addfull n' m' with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r)) =
    match
      match addfull n' m' with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r) with
    | next false a => toSint (next true n') + toSint (next false m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next false m') - 2 ^ (sz + 1)
Tactic:
case true.false =>
  match h: addfull n' m' with
  | .next br r =>
    have h' := FinInt.addfull_toUint n' m'
    rw [h] at h'
    cases br <;> simp at h' <;> simp [toSint]
    . simp [h']; sorry_arith
    . sorry_arith
Proof state after:
no goals
Theorem: FinInt.addfull_toSint
Proof state before:
sz : ℕ
n' m' : FinInt sz
⊢ toSint
      (match addfull n' m' with
      | next false r => next true (next false r)
      | next true r => next true (next true r)) =
    toSint (next true n') + toSint (next true m')
Tactic:
case true.true =>
  match h: addfull n' m' with
  | .next br r =>
    have h' := FinInt.addfull_toUint n' m'
    rw [h] at h'
    cases br <;> simp at h' <;> simp [toSint, h'] <;> sorry_arith
Proof state after:
no goals
Theorem: FinInt.addfull_toSint
Proof state before:
sz : ℕ
n' m' : FinInt sz
⊢ toSint
      (match addfull n' m' with
      | next false r => next false (next false r)
      | next true r => next false (next true r)) =
    toSint (next false n') + toSint (next false m')
Tactic:
match h: addfull n' m' with
| .next br r =>
  cases br <;> simp [toSint, ←FinInt.addfull_toUint, h]
Proof state after:
no goals
Theorem: FinInt.addfull_toSint
Proof state before:
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h : addfull n' m' = next br r
⊢ toSint
      (match next br r with
      | next false r => next false (next false r)
      | next true r => next false (next true r)) =
    toSint (next false n') + toSint (next false m')
Tactic:
cases br <;> simp [toSint, ←FinInt.addfull_toUint, h]
Proof state after:
no goals
Theorem: FinInt.addfull_toSint
Proof state before:
sz : ℕ
n' m' : FinInt sz
⊢ toSint
      (match addfull n' m' with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r)) =
    match
      match addfull n' m' with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r) with
    | next false a => toSint (next false n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next false n') + toSint (next true m') - 2 ^ (sz + 1)
Tactic:
match h: addfull n' m' with
| .next br r =>
  have h' := FinInt.addfull_toUint n' m'
  rw [h] at h'
  cases br <;> simp at h' <;> simp [toSint]
  . simp [h']; sorry_arith
  . sorry_arith
Proof state after:
no goals
Theorem: FinInt.addfull_toSint
Proof state before:
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h : addfull n' m' = next br r
⊢ toSint
      (match next br r with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r)) =
    match
      match next br r with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r) with
    | next false a => toSint (next false n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next false n') + toSint (next true m') - 2 ^ (sz + 1)
Tactic:
have h' := FinInt.addfull_toUint n' m'
Proof 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'
⊢ toSint
      (match next br r with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r)) =
    match
      match next br r with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r) with
    | next false a => toSint (next false n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next false n') + toSint (next true m') - 2 ^ (sz + 1)
Theorem: FinInt.addfull_toSint
Proof 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'
⊢ toSint
      (match next br r with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r)) =
    match
      match next br r with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r) with
    | next false a => toSint (next false n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next false n') + toSint (next true m') - 2 ^ (sz + 1)
Tactic:
rw [h] at h'
Proof 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'
⊢ toSint
      (match next br r with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r)) =
    match
      match next br r with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r) with
    | next false a => toSint (next false n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next false n') + toSint (next true m') - 2 ^ (sz + 1)
Theorem: FinInt.addfull_toSint
Proof 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'
⊢ toSint
      (match next br r with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r)) =
    match
      match next br r with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r) with
    | next false a => toSint (next false n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next false n') + toSint (next true m') - 2 ^ (sz + 1)
Tactic:
cases br <;> simp at h' <;> simp [toSint]
Proof state after:
case false
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next false r
h' : toUint r = toUint n' + toUint m'
⊢ 2 ^ sz + toUint r = toUint n' + (toUint m' - 2 ^ sz) + 2 ^ (sz + 1)

case true
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next true r
h' : 2 ^ sz + toUint r = toUint n' + toUint m'
⊢ toUint r = toUint n' + (toUint m' - 2 ^ sz)
Theorem: FinInt.addfull_toSint
Proof state before:
case false
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next false r
h' : toUint r = toUint n' + toUint m'
⊢ 2 ^ sz + toUint r = toUint n' + (toUint m' - 2 ^ sz) + 2 ^ (sz + 1)

case true
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next true r
h' : 2 ^ sz + toUint r = toUint n' + toUint m'
⊢ toUint r = toUint n' + (toUint m' - 2 ^ sz)
Tactic:
. simp [h']; sorry_arith
Proof state after:
case true
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next true r
h' : 2 ^ sz + toUint r = toUint n' + toUint m'
⊢ toUint r = toUint n' + (toUint m' - 2 ^ sz)
Theorem: FinInt.addfull_toSint
Proof state before:
case true
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next true r
h' : 2 ^ sz + toUint r = toUint n' + toUint m'
⊢ toUint r = toUint n' + (toUint m' - 2 ^ sz)
Tactic:
. sorry_arith
Proof state after:
no goals
Theorem: FinInt.addfull_toSint
Proof state before:
sz : ℕ
n' m' : FinInt sz
⊢ toSint
      (match addfull n' m' with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r)) =
    match
      match addfull n' m' with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r) with
    | next false a => toSint (next true n') + toSint (next false m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next false m') - 2 ^ (sz + 1)
Tactic:
match h: addfull n' m' with
| .next br r =>
  have h' := FinInt.addfull_toUint n' m'
  rw [h] at h'
  cases br <;> simp at h' <;> simp [toSint]
  . simp [h']; sorry_arith
  . sorry_arith
Proof state after:
no goals
Theorem: FinInt.addfull_toSint
Proof state before:
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h : addfull n' m' = next br r
⊢ toSint
      (match next br r with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r)) =
    match
      match next br r with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r) with
    | next false a => toSint (next true n') + toSint (next false m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next false m') - 2 ^ (sz + 1)
Tactic:
have h' := FinInt.addfull_toUint n' m'
Proof 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'
⊢ toSint
      (match next br r with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r)) =
    match
      match next br r with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r) with
    | next false a => toSint (next true n') + toSint (next false m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next false m') - 2 ^ (sz + 1)
Theorem: FinInt.addfull_toSint
Proof 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'
⊢ toSint
      (match next br r with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r)) =
    match
      match next br r with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r) with
    | next false a => toSint (next true n') + toSint (next false m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next false m') - 2 ^ (sz + 1)
Tactic:
rw [h] at h'
Proof 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'
⊢ toSint
      (match next br r with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r)) =
    match
      match next br r with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r) with
    | next false a => toSint (next true n') + toSint (next false m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next false m') - 2 ^ (sz + 1)
Theorem: FinInt.addfull_toSint
Proof 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'
⊢ toSint
      (match next br r with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r)) =
    match
      match next br r with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r) with
    | next false a => toSint (next true n') + toSint (next false m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next false m') - 2 ^ (sz + 1)
Tactic:
cases br <;> simp at h' <;> simp [toSint]
Proof state after:
case false
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next false r
h' : toUint r = toUint n' + toUint m'
⊢ 2 ^ sz + toUint r = toUint n' - 2 ^ sz + toUint m' + 2 ^ (sz + 1)

case true
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next true r
h' : 2 ^ sz + toUint r = toUint n' + toUint m'
⊢ toUint r = toUint n' - 2 ^ sz + toUint m'
Theorem: FinInt.addfull_toSint
Proof state before:
case false
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next false r
h' : toUint r = toUint n' + toUint m'
⊢ 2 ^ sz + toUint r = toUint n' - 2 ^ sz + toUint m' + 2 ^ (sz + 1)

case true
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next true r
h' : 2 ^ sz + toUint r = toUint n' + toUint m'
⊢ toUint r = toUint n' - 2 ^ sz + toUint m'
Tactic:
. simp [h']; sorry_arith
Proof state after:
case true
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next true r
h' : 2 ^ sz + toUint r = toUint n' + toUint m'
⊢ toUint r = toUint n' - 2 ^ sz + toUint m'
Theorem: FinInt.addfull_toSint
Proof state before:
case true
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next true r
h' : 2 ^ sz + toUint r = toUint n' + toUint m'
⊢ toUint r = toUint n' - 2 ^ sz + toUint m'
Tactic:
. sorry_arith
Proof state after:
no goals
Theorem: FinInt.addfull_toSint
Proof state before:
sz : ℕ
n' m' : FinInt sz
⊢ toSint
      (match addfull n' m' with
      | next false r => next true (next false r)
      | next true r => next true (next true r)) =
    toSint (next true n') + toSint (next true m')
Tactic:
match h: addfull n' m' with
| .next br r =>
  have h' := FinInt.addfull_toUint n' m'
  rw [h] at h'
  cases br <;> simp at h' <;> simp [toSint, h'] <;> sorry_arith
Proof state after:
no goals
Theorem: FinInt.addfull_toSint
Proof state before:
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h : addfull n' m' = next br r
⊢ toSint
      (match next br r with
      | next false r => next true (next false r)
      | next true r => next true (next true r)) =
    toSint (next true n') + toSint (next true m')
Tactic:
have h' := FinInt.addfull_toUint n' m'
Proof 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'
⊢ toSint
      (match next br r with
      | next false r => next true (next false r)
      | next true r => next true (next true r)) =
    toSint (next true n') + toSint (next true m')
Theorem: FinInt.addfull_toSint
Proof 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'
⊢ toSint
      (match next br r with
      | next false r => next true (next false r)
      | next true r => next true (next true r)) =
    toSint (next true n') + toSint (next true m')
Tactic:
rw [h] at h'
Proof 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'
⊢ toSint
      (match next br r with
      | next false r => next true (next false r)
      | next true r => next true (next true r)) =
    toSint (next true n') + toSint (next true m')
Theorem: FinInt.addfull_toSint
Proof 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'
⊢ toSint
      (match next br r with
      | next false r => next true (next false r)
      | next true r => next true (next true r)) =
    toSint (next true n') + toSint (next true m')
Tactic:
cases br <;> simp at h' <;> simp [toSint, h'] <;> sorry_arith
Proof state after:
no goals
Theorem: FinInt.addfull_comm
Proof state before:
sz : ℕ
n m : FinInt sz
⊢ addfull n m = addfull m n
Tactic:
induction sz <;> cases n <;> cases m <;> simp [addfull]
Proof state after:
case succ.next.next
n✝ : ℕ
a✝³ : Bool
a✝² : FinInt n✝
n_ih✝ : ∀ (n m : FinInt (Nat.add n✝ 0)), addfull n m = addfull m n
a✝¹ : Bool
a✝ : FinInt n✝
⊢ (match addfull a✝² a✝ with
    | next false r => next (a✝³ && a✝¹) (next (a✝³ != a✝¹) r)
    | next true r => next (a✝³ || a✝¹) (next (a✝³ == a✝¹) r)) =
    match addfull a✝ a✝² with
    | next false r => next (a✝¹ && a✝³) (next (a✝¹ != a✝³) r)
    | next true r => next (a✝¹ || a✝³) (next (a✝¹ == a✝³) r)
Theorem: FinInt.addfull_comm
Proof state before:
sz : ℕ
bn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), addfull n m = addfull m n
bm : Bool
m' : FinInt sz
⊢ (match addfull n' m' with
    | next false r => next (bn && bm) (next (bn != bm) r)
    | next true r => next (bn || bm) (next (bn == bm) r)) =
    match addfull m' n' with
    | next false r => next (bm && bn) (next (bm != bn) r)
    | next true r => next (bm || bn) (next (bm == bn) r)
Tactic:
case succ.next.next sz bn n' ih bm m' =>
  simp [ih n' m']
  split <;> cases bn <;> cases bm <;> rfl
Proof state after:
no goals
Theorem: FinInt.addfull_comm
Proof state before:
sz : ℕ
bn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), addfull n m = addfull m n
bm : Bool
m' : FinInt sz
⊢ (match addfull n' m' with
    | next false r => next (bn && bm) (next (bn != bm) r)
    | next true r => next (bn || bm) (next (bn == bm) r)) =
    match addfull m' n' with
    | next false r => next (bm && bn) (next (bm != bn) r)
    | next true r => next (bm || bn) (next (bm == bn) r)
Tactic:
simp [ih n' m']
Proof state after:
sz : ℕ
bn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), addfull n m = addfull m n
bm : Bool
m' : FinInt sz
⊢ (match addfull m' n' with
    | next false r => next (bn && bm) (next (bn != bm) r)
    | next true r => next (bn || bm) (next (bn == bm) r)) =
    match addfull m' n' with
    | next false r => next (bm && bn) (next (bm != bn) r)
    | next true r => next (bm || bn) (next (bm == bn) r)
Theorem: FinInt.addfull_comm
Proof state before:
sz : ℕ
bn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), addfull n m = addfull m n
bm : Bool
m' : FinInt sz
⊢ (match addfull m' n' with
    | next false r => next (bn && bm) (next (bn != bm) r)
    | next true r => next (bn || bm) (next (bn == bm) r)) =
    match addfull m' n' with
    | next false r => next (bm && bn) (next (bm != bn) r)
    | next true r => next (bm || bn) (next (bm == bn) r)
Tactic:
split <;> cases bn <;> cases bm <;> rfl
Proof state after:
no goals
Theorem: FinInt.addc_comm
Proof state before:
sz : ℕ
n m : FinInt sz
⊢ addc n m = addc m n
Tactic:
simp [addc, addfull_comm]
Proof state after:
no goals
Theorem: FinInt.add_comm'
Proof state before:
sz : ℕ
n m : FinInt sz
⊢ add n m = add m n
Tactic:
simp [add, addfull_comm]
Proof state after:
no goals
Theorem: FinInt.add_comm
Proof state before:
sz : ℕ
n m : FinInt sz
⊢ n + m = m + n
Tactic:
simp [HAdd.hAdd, add_comm']
Proof state after:
no goals
Theorem: FinInt.add_toUint_msb
Proof 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
Proof state after:
no goals
Theorem: FinInt.add_toUint_msb
Proof 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
Proof 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
Theorem: FinInt.add_toUint_msb
Proof 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₁
Proof 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
Theorem: FinInt.add_toUint_msb
Proof 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]
Proof 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