Theorem: testGoalNotEqualityMustFail (playground/tactic.lean)

State before:
⊢ Nat → Int → Nat → Nat
Tactic:
intros a b c
State after:
a : Nat
b : Int
c : Nat
⊢ Nat