have a hypothesis that has multiple premises

[Qinggao1729]

mul_ne_zero is defined as (a b : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0.
So, in line 13, hne should be ha ∧ hb → a * succ d ≠ 0
But instead, it displays ha → hb → a * succ d ≠ 0

I encounter this problem whenever I use have to introduce a hypothesis with multiple premises.

[joneugster]

That seems corrwct as-is and how Lean works.

i.e. a "theorem" with assumptions is just another syntax to write a sequence of implications. (or foralls if they are dependent).

"And" on the other hand is a different inductive type which isnt definitionally equivalent to what's displayed

Is there anything the Natural Number Game could improve in its text which would have helped you understand better?