dsimp only at hm3
case h.intro
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
m : ℕ
hm1 : 0 < m
hm2 : p m
hm3 : (fun n => p (n + 1)) (m - 1) → m - 1 = n
⊢ m = n + 1
case h.intro
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
m : ℕ
hm1 : 0 < m
hm2 : p m
hm3 : p (m - 1 + 1) → m - 1 = n
⊢ m = n + 1