ring vs ring_nf

Stream: general

[Damiano Testa]

Another quiz: I was somewhat surprised by Lean's conclusions with the three proofs below.

Can you guess whether Lean accepts them, discards them, or does a mix?

import tactic.ring

lemma zero_le_zero_mul_zero1 : 0 ≤ 0 * 0 := by ring
lemma zero_le_zero_mul_zero2 : 0 ≤ 0 * 0 := by ring_nf
lemma zero_le_zero_mul_zero3 : 0 ≤ 0 * 0 := le_of_eq (by ring)