meaning of Init.Core._auxLemma.4

Stream: lean4

[Scott N. Walck]

Hi folks,

I like to try to learn more about lean by writing tactics and
seeing what sort of proof term is created. For this little
theorem,

theorem zero_not_one : 0 = 1 -> False := by simp
#print zero_not_one

I get

theorem zero_not_one : 0 = 1 → False :=
of_eq_true (Eq.trans (implies_congr (eq_false_of_decide (Eq.refl false)) (Eq.refl False)) Init.Core._auxLemma.4)

but what is Init.Core._auxLemma.4 ? I looked in the source code
for such a thing, but I couldn't find anything like it.

A second question: Is there a tactic similar to Coq's
discriminate, one that could conclude a proof from a hypothesis
of the form c1 x = c2 y, where c1 and c2 are different
constructors of some data type?

Thanks!

[Kevin Buzzard]

Discussion of this question is now taking place at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Something.20like.20Coq's.20discriminate