elab12.lean:1:30: error: type expected at
  0
elab12.lean:1:38: error: function expected at
  rfl
Additional information:
elab12.lean:1:38: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  too many arguments
elab12.lean:2:2: error: function expected at
  H
λ (a : ℕ), have H : sorry, from sorry, sorry : ∀ (a : ℕ), a = a
elab12.lean:4:42: error: function expected at
  rfl
Additional information:
elab12.lean:4:42: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  too many arguments
elab12.lean:5:2: error: function expected at
  H
λ (a : ℕ), have H : a = a, from sorry, sorry : ∀ (a : ℕ), a = a
elab12.lean:7:44: error: invalid have-expression, expression
  a + 0
has type
  ℕ
but is expected to have type
  a = a
elab12.lean:8:2: error: function expected at
  H
λ (a : ℕ), have H : a = a, from sorry, sorry : ∀ (a : ℕ), a = a
elab12.lean:11:2: error: function expected at
  H
λ (a : ℕ), have H : a = a, from rfl, sorry : ∀ (a : ℕ), a = a
λ (a : ℕ), have H : a = a, from rfl, H : ∀ (a : ℕ), a = a
