Nat.sub_add_cancel for positive numbers

Stream: new members

[Daniel Gavrila]

Hi all,

Calling Nat.sub_add_cancel for natural positive numbers, produces a complicated term as shown in infoview.  Why is happening this and what should I do to proof the lemma

lemma sub_add_cancel_pos ( n m : ℕ+) (h: m <= n ) : n - m + m = n := by

have h1 := Nat.sub_add_cancel h

Infoview : 

unsolved goals

n m : ℕ+

h : m ≤ n

h1 : (fun a ↦ ↑a) n - (fun a↦ ↑a) m + (fun a ↦ ↑a) m = (fun a ↦ ↑a) n

⊢ n - m + m = n

[Ruben Van de Velde]

Because you're using a hypothesis about ℕ+ when the lemma expects one about ℕ

[Ruben Van de Velde]

Also, please read #mwe and #backticks

[Ruben Van de Velde]

And note that your lemma is false:

import Mathlib

lemma sub_add_cancel_pos ( n m : ℕ+) (h: m <= n ) : n - m + m = n := by
  sorry

example : False := by
  have := sub_add_cancel_pos 1 1 le_rfl
  contradiction