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

State before:
sz : ℕ
n m : FinInt sz
⊢ addfull n m = addfull m n
Tactic:
induction sz <;> cases n <;> cases m <;> simp [addfull]
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)

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
State after:
no goals

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']
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)

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
State after:
no goals