Theorem: LoVe.Int.neg_neg (LoVe/LoVelib.lean)

State before:
⊢ Int.neg ∘ Int.neg = id
Tactic:
apply funext
State after:
case h

⊢ ∀ (x : ℤ), (Int.neg ∘ Int.neg) x = id x

State before:
case h

⊢ ∀ (x : ℤ), (Int.neg ∘ Int.neg) x = id x
Tactic:
intro i
State after:
case h
i : ℤ
⊢ (Int.neg ∘ Int.neg) i = id i

State before:
case h
i : ℤ
⊢ (Int.neg ∘ Int.neg) i = id i
Tactic:
simp
State after:
case h
i : ℤ
⊢ Int.neg (Int.neg i) = i

State before:
case h
i : ℤ
⊢ Int.neg (Int.neg i) = i
Tactic:
cases i with
| ofNat n =>
  { simp [Int.neg]
    cases n
    { simp }
    { simp [Int.negOfNat] } }
| negSucc n =>
  { simp [Int.neg]
    have hnp1 : (↑n + 1 : ℤ) = ↑(n + 1) :=
      by simp
    rw [hnp1]
    rfl }
State after:
no goals

State before:
case h.ofNat
n : ℕ
⊢ Int.neg (Int.neg (Int.ofNat n)) = Int.ofNat n
Tactic:
simp [Int.neg]
State after:
case h.ofNat
n : ℕ
⊢ (match Int.negOfNat n with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    ↑n

State before:
case h.ofNat
n : ℕ
⊢ (match Int.negOfNat n with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    ↑n
Tactic:
cases n
State after:
case h.ofNat.zero

⊢ (match Int.negOfNat Nat.zero with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    ↑Nat.zero

case h.ofNat.succ
n_1 : ℕ
⊢ (match Int.negOfNat (Nat.succ n_1) with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    ↑(Nat.succ n_1)

State before:
case h.ofNat.zero

⊢ (match Int.negOfNat Nat.zero with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    ↑Nat.zero

case h.ofNat.succ
n_1 : ℕ
⊢ (match Int.negOfNat (Nat.succ n_1) with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    ↑(Nat.succ n_1)
Tactic:
{ simp }
State after:
case h.ofNat.succ
n_1 : ℕ
⊢ (match Int.negOfNat (Nat.succ n_1) with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    ↑(Nat.succ n_1)

State before:
case h.ofNat.succ
n_1 : ℕ
⊢ (match Int.negOfNat (Nat.succ n_1) with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    ↑(Nat.succ n_1)
Tactic:
{ simp [Int.negOfNat] }
State after:
no goals

State before:
case h.ofNat.zero

⊢ (match Int.negOfNat Nat.zero with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    ↑Nat.zero
Tactic:
simp
State after:
no goals

State before:
case h.ofNat.succ
n_1 : ℕ
⊢ (match Int.negOfNat (Nat.succ n_1) with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    ↑(Nat.succ n_1)
Tactic:
simp [Int.negOfNat]
State after:
no goals

State before:
case h.negSucc
n : ℕ
⊢ Int.neg (Int.neg (Int.negSucc n)) = Int.negSucc n
Tactic:
simp [Int.neg]
State after:
case h.negSucc
n : ℕ
⊢ (match ↑n + 1 with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    Int.negSucc n

State before:
case h.negSucc
n : ℕ
⊢ (match ↑n + 1 with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    Int.negSucc n
Tactic:
have hnp1 : (↑n + 1 : ℤ) = ↑(n + 1) :=
  by simp
State after:
case h.negSucc
n : ℕ
hnp1 : ↑n + 1 = ↑(n + 1)
⊢ (match ↑n + 1 with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    Int.negSucc n

State before:
case h.negSucc
n : ℕ
hnp1 : ↑n + 1 = ↑(n + 1)
⊢ (match ↑n + 1 with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    Int.negSucc n
Tactic:
rw [hnp1]
State after:
case h.negSucc
n : ℕ
hnp1 : ↑n + 1 = ↑(n + 1)
⊢ (match ↑(n + 1) with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    Int.negSucc n

State before:
case h.negSucc
n : ℕ
hnp1 : ↑n + 1 = ↑(n + 1)
⊢ (match ↑(n + 1) with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    Int.negSucc n
Tactic:
rfl
State after:
no goals

State before:
n : ℕ
⊢ ↑n + 1 = ↑(n + 1)
Tactic:
simp
State after:
no goals