How to apply a hypothesis about the integers to the natural

Stream: new members

[Mike]

I'm stumped. Does anyone know how to prove the following
example:

import Mathlib

example (n₁ n₂ : ℕ) (heq : Int.negSucc n₂ + Int.ofNat n₃ = Int.negSucc n₁) :
  Nat.succ n₂ = Nat.succ n₁ + n₃ := by
  sorry

If I try:

example (n₁ n₂ : ℕ) (heq : Int.negSucc n₂ + Int.ofNat n₃ = Int.negSucc n₁) :
  Nat.succ n₂ = Nat.succ n₁ + n₃ := by
  rw [←Int.ofNat_inj]
  rw [Int.ofNat_eq_cast] at heq
  rw [Int.negSucc_eq] at heq
  rw [Int.negSucc_eq] at heq
  simp
  ...

I'm left with:

heq: -(↑n₂ + 1) + ↑n₃ = -(↑n₁ + 1)
⊢ ↑n₂ + 1 = ↑n₁ + 1 + ↑n₃

This seems like it's very close to the end, but
I can't use some of the ↑n's in a calc or a have,
because then I get an error that says:

failed to synthesize instance
  Neg ℕLean 4

It looks like it won't synthesize a negative
-(↑n), which seems strange to me, because it
should be an element of ℤ.

Thanks!

[Ruben Van de Velde]

The up arrow is generic notation for a coercion from "something" to "something". Probably it can't come up with anything better than "Nat to itself". Use (n : \Z) instead

[Kyle Miller]

If you get lost with up arrows, there's a pretty printer option to show what they're hiding:

import Mathlib.Tactic

example (n : ℕ) : (n : ℤ) = (n : ℤ) := by
  -- ⊢ ↑n = ↑n
  rfl

set_option pp.coercions false

example (n : ℕ) : (n : ℤ) = (n : ℤ) := by
  -- ⊢ Nat.cast n = Nat.cast n
  rfl

You can also move your mouse over an up arrow in the info view and see the expression it stands for.

[Kyle Miller]

Regarding your question, I guess linarith handles it.

example (n₁ n₂ n₃ : ℕ) (heq : Int.negSucc n₂ + Int.ofNat n₃ = Int.negSucc n₁) :
  Nat.succ n₂ = Nat.succ n₁ + n₃ := by
  rw [←Int.ofNat_inj]
  rw [Int.ofNat_eq_cast] at heq
  rw [Int.negSucc_eq] at heq
  rw [Int.negSucc_eq] at heq
  simp
  linarith

[Mike]

Yeah, linarith did it! @Kyle Miller Thanks!!

[Kyle Miller]

linear_combination -1 * heq works in place of linarith too, if you want to be more explicit.