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

State before:
sz : ℕ
n m : FinInt (sz + 1)
⊢ addv n m = addv m n
Tactic:
simp [addv]
State after:
sz : ℕ
n m : FinInt (sz + 1)
⊢ (match n, m with
    | next false n', next false m' =>
      match n + m with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match n + m with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (n + m, false)) =
    match m, n with
    | next false n', next false m' =>
      match m + n with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match m + n with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (m + n, false)

State before:
sz : ℕ
n m : FinInt (sz + 1)
⊢ (match n, m with
    | next false n', next false m' =>
      match n + m with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match n + m with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (n + m, false)) =
    match m, n with
    | next false n', next false m' =>
      match m + n with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match m + n with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (m + n, false)
Tactic:
cases n
State after:
case next
sz : ℕ
m : FinInt (sz + 1)
a✝¹ : Bool
a✝ : FinInt sz
⊢ (match next a✝¹ a✝, m with
    | next false n', next false m' =>
      match next a✝¹ a✝ + m with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match next a✝¹ a✝ + m with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next a✝¹ a✝ + m, false)) =
    match m, next a✝¹ a✝ with
    | next false n', next false m' =>
      match m + next a✝¹ a✝ with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match m + next a✝¹ a✝ with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (m + next a✝¹ a✝, false)

State before:
case next
sz : ℕ
m : FinInt (sz + 1)
a✝¹ : Bool
a✝ : FinInt sz
⊢ (match next a✝¹ a✝, m with
    | next false n', next false m' =>
      match next a✝¹ a✝ + m with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match next a✝¹ a✝ + m with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next a✝¹ a✝ + m, false)) =
    match m, next a✝¹ a✝ with
    | next false n', next false m' =>
      match m + next a✝¹ a✝ with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match m + next a✝¹ a✝ with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (m + next a✝¹ a✝, false)
Tactic:
cases m
State after:
case next.next
sz : ℕ
a✝³ : Bool
a✝² : FinInt sz
a✝¹ : Bool
a✝ : FinInt sz
⊢ (match next a✝³ a✝², next a✝¹ a✝ with
    | next false n', next false m' =>
      match next a✝³ a✝² + next a✝¹ a✝ with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match next a✝³ a✝² + next a✝¹ a✝ with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next a✝³ a✝² + next a✝¹ a✝, false)) =
    match next a✝¹ a✝, next a✝³ a✝² with
    | next false n', next false m' =>
      match next a✝¹ a✝ + next a✝³ a✝² with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match next a✝¹ a✝ + next a✝³ a✝² with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next a✝¹ a✝ + next a✝³ a✝², false)

State before:
sz : ℕ
bn : Bool
n' : FinInt sz
bm : Bool
m' : FinInt sz
⊢ (match next bn n', next bm m' with
    | next false n'_1, next false m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', msb)
    | next true n'_1, next true m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next bn n' + next bm m', false)) =
    match next bm m', next bn n' with
    | next false n'_1, next false m'_1 =>
      match next bm m' + next bn n' with
      | next msb r' => (next msb r', msb)
    | next true n'_1, next true m'_1 =>
      match next bm m' + next bn n' with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next bm m' + next bn n', false)
Tactic:
case next.next bn n' bm m' =>
simp [add_comm]; cases bn <;> cases bm <;> rfl
State after:
no goals

State before:
sz : ℕ
bn : Bool
n' : FinInt sz
bm : Bool
m' : FinInt sz
⊢ (match next bn n', next bm m' with
    | next false n'_1, next false m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', msb)
    | next true n'_1, next true m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next bn n' + next bm m', false)) =
    match next bm m', next bn n' with
    | next false n'_1, next false m'_1 =>
      match next bm m' + next bn n' with
      | next msb r' => (next msb r', msb)
    | next true n'_1, next true m'_1 =>
      match next bm m' + next bn n' with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next bm m' + next bn n', false)
Tactic:
simp [add_comm]
State after:
sz : ℕ
bn : Bool
n' : FinInt sz
bm : Bool
m' : FinInt sz
⊢ (match next bn n', next bm m' with
    | next false n'_1, next false m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', msb)
    | next true n'_1, next true m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next bn n' + next bm m', false)) =
    match next bm m', next bn n' with
    | next false n'_1, next false m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', msb)
    | next true n'_1, next true m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next bn n' + next bm m', false)

State before:
sz : ℕ
bn : Bool
n' : FinInt sz
bm : Bool
m' : FinInt sz
⊢ (match next bn n', next bm m' with
    | next false n'_1, next false m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', msb)
    | next true n'_1, next true m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next bn n' + next bm m', false)) =
    match next bm m', next bn n' with
    | next false n'_1, next false m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', msb)
    | next true n'_1, next true m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next bn n' + next bm m', false)
Tactic:
cases bn <;> cases bm <;> rfl
State after:
no goals