NeZero t not definitionally equivalent to t \ne 0?

Stream: new members

[JK]

I am stuck with proving the following

import Mathlib

example {t:ℝ} : t=0 ∨ t ≠ 0  := by
  obtain tzero | tnzero := eq_zero_or_neZero t
  right
  exact tzero
  left

I would have thought that NeZero t was definitionally equivalent to t ≠ 0. In any case I can't find the correct lemma to apply to either get the desired hypothesis in the first place, or to claim that NeZero t → t ≠ 0

[Aaron Liu]

docs#neZero_iff

[Aaron Liu]

the lemma is docs#eq_or_ne

[JK]

Thanks for that, I was not able to find it using apply?

[Kenny Lau]

use loogle instead

[JK]

I have not had much luck with loogle at all, TBH

[Etienne Marion]

@loogle NeZero, _ ≠ 0

[loogle]

:search: NeZero.mk, NeZero.ne, and 72 more

[Kenny Lau]

@JK next time you are stuck on Loogle, tell me what you want to find and ping me, and I'll show you the correct input to Loogle.

[Junyan Xu]

NeZero n is a class, in particular a structure (an inductive type with a single constructor), and you always need to apply the constructor to obtain a term whose type is a structure. If h : n ≠ 0 then ⟨h⟩ is of type NeZero n.

[Dan Velleman]

By the way, although it's good to know about NeZero and how to use it, I wouldn't use it for this example. Here are two ways to do it that I think are more straightforward:

import Mathlib

example {t:ℝ} : t=0 ∨ t ≠ 0 := em (t=0)

example {t:ℝ} : t=0 ∨ t ≠ 0 := by
  by_cases h : t = 0
  · left
    exact h
  · right
    exact h

Note that em is the law of excluded middle.

[Kenny Lau]

import Mathlib

example {t : ℝ} : t = 0 ∨ t ≠ 0 :=
  if h : t = 0 then Or.inl h else Or.inr h

example {t : ℝ} : t = 0 ∨ t ≠ 0 := by
  if h : t = 0 then ?_ else ?_
  · left
    exact h
  · right
    exact h

[Wuyang]

@leanfinder NeZero, _ ≠ 0

[leanfinder]

Here’s what I found:

• For an element $n$ of a type $R$, if $n$ is a non-zero element (i.e., $\text{NeZero } n$), then $n \neq 0$. (score: 0.821)
• For an element $n$ in a type $R$, the class NeZero represents the proposition that $n \neq 0$. This is a type-class version of stating that $n$ is not zero. (score: 0.816)
• For an element $n$ of a type $R$, if $n$ is a non-zero element (denoted as $\text{NeZero } n$), then $0 \neq n$. This follows from the definition of non-zero elements. (score: 0.808)
• For an element $n$ of a type $R$, the statement that $n$ is a non-zero element (i.e., $\text{NeZero } n$) is equivalent to $n \neq 0$. (score: 0.798)
• Let $M$ be a type with a preorder and a zero element. For any element $x$ in $M$ such that $0 < x$, we have that $x$ is nonzero (i.e., $x \neq 0$). (score: 0.785)
• Let $M$ be an additively canonically ordered monoid with a partial order and a zero element. For any nonzero element $a \in M$, we have $0 < a$. (score: 0.783)
• For any natural number $n$ that is nonzero (i.e., satisfies NeZero n), we have $1 \leq n$. (score: 0.780)
• If a natural number $n$ is not zero, then $n$ is positive, i.e., $0 < n$. This follows from the assumption that $n$ is nonzero, denoted by \text{NeZero} n. This is a basic property of natural numbers. (score: 0.779)
• In any additive monoid with one $M$ of characteristic zero, the element $2$ is nonzero. (score: 0.778)
• For any type $\alpha$ with a zero element, the statement $\text{NeZero}(0)$ is equivalent to $\text{False}$. In other words, zero cannot be non-zero. (score: 0.777)

[Wuyang]

@JK You may also try leanfinder