How to apply a hypothesis about integers to natural numbers

Stream: new members

[Mike]

I'm stumped. I would like to prove the two examples:

import Mathlib

example (n₁ n₂ : ℕ) (h : -Int.negSucc n₁ = Int.ofNat n₂) : Nat.succ n₁ = n₂ := by
  sorry

example (n₁ n₂ n₃ : ℕ) (h : Int.ofNat n₂ * Int.ofNat n₃ = Int.ofNat n₁) : n₂ * n₃ = n₁ := by
  sorry

If I try:

example (n₁ n₂ : ℕ) (h : -Int.negSucc n₁ = Int.ofNat n₂) : Nat.succ n₁ = n₂ := by
  rw [Int.negSucc_eq] at h
  rw [Int.ofNat_eq_cast] at h

I'm left with:

n₁n₂: ℕ
h: - -(↑n₁ + 1) = ↑n₂
⊢ Nat.succ n₁ = n₂

but when I try to work with - -(↑n₁ + 1),
I get "failed to synthesize instance: Neg ℕ Lean 4"

Thanks for any help!

[Ruben Van de Velde]

Does it help if you start your proof with

  rw [← Int.ofNat_inj]

?

[Mike]

@Ruben Van de Velde Yeah, that works! The only thing left was to use tauto. Thanks!