Theorem: Int.add_comm (Table/BuiltinExtensions.lean)

State before:
⊢ ∀ (x y : Int), x + y = y + x
Tactic:
intros x y
State after:
x y : Int
⊢ x + y = y + x

State before:
x y : Int
⊢ x + y = y + x
Tactic:
unfold HAdd.hAdd
State after:
x y : Int
⊢ instHAdd.1 x y = instHAdd.1 y x

State before:
x y : Int
⊢ instHAdd.1 x y = instHAdd.1 y x
Tactic:
unfold instHAdd
State after:
x y : Int
⊢ { hAdd := fun a b => Add.add a b }.1 x y = { hAdd := fun a b => Add.add a b }.1 y x

State before:
x y : Int
⊢ { hAdd := fun a b => Add.add a b }.1 x y = { hAdd := fun a b => Add.add a b }.1 y x
Tactic:
unfold Add.add
State after:
x y : Int
⊢ { hAdd := fun a b => instAddInt.1 a b }.1 x y = { hAdd := fun a b => instAddInt.1 a b }.1 y x

State before:
x y : Int
⊢ { hAdd := fun a b => instAddInt.1 a b }.1 x y = { hAdd := fun a b => instAddInt.1 a b }.1 y x
Tactic:
unfold instAddInt
State after:
x y : Int
⊢ { hAdd := fun a b => { add := Int.add }.1 a b }.1 x y = { hAdd := fun a b => { add := Int.add }.1 a b }.1 y x

State before:
x y : Int
⊢ { hAdd := fun a b => { add := Int.add }.1 a b }.1 x y = { hAdd := fun a b => { add := Int.add }.1 a b }.1 y x
Tactic:
unfold Int.add
State after:
x y : Int
⊢ {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      x y =
    {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      y x

State before:
x y : Int
⊢ {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      x y =
    {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      y x
Tactic:
induction x with
| ofNat n =>
  cases y with
  | ofNat m => simp [Nat.add_comm]
  | negSucc m => simp
| negSucc n =>
  cases y with
  | ofNat m => simp
  | negSucc m => simp [Nat.add_comm]
State after:
no goals

State before:
case ofNat
y : Int
n : Nat
⊢ {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      (ofNat n) y =
    {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      y (ofNat n)
Tactic:
cases y with
| ofNat m => simp [Nat.add_comm]
| negSucc m => simp
State after:
no goals

State before:
case ofNat.ofNat
n m : Nat
⊢ {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      (ofNat n) (ofNat m) =
    {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      (ofNat m) (ofNat n)
Tactic:
simp [Nat.add_comm]
State after:
no goals

State before:
case ofNat.negSucc
n m : Nat
⊢ {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      (ofNat n) (negSucc m) =
    {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      (negSucc m) (ofNat n)
Tactic:
simp
State after:
no goals

State before:
case negSucc
y : Int
n : Nat
⊢ {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      (negSucc n) y =
    {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      y (negSucc n)
Tactic:
cases y with
| ofNat m => simp
| negSucc m => simp [Nat.add_comm]
State after:
no goals

State before:
case negSucc.ofNat
n m : Nat
⊢ {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      (negSucc n) (ofNat m) =
    {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      (ofNat m) (negSucc n)
Tactic:
simp
State after:
no goals

State before:
case negSucc.negSucc
n m : Nat
⊢ {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      (negSucc n) (negSucc m) =
    {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      (negSucc m) (negSucc n)
Tactic:
simp [Nat.add_comm]
State after:
no goals