Theorem: OddPrimeOrFour.ne_zero (Flt/OddPrimeOrFour.lean)

State before:
z : ℤ
h : OddPrimeOrFour z
⊢ z ≠ 0
Tactic:
obtain rfl | ⟨h, -⟩ := h
State after:
case inl

⊢ 4 ≠ 0

case inr.intro
z : ℤ
h : Prime z
⊢ z ≠ 0

State before:
case inl

⊢ 4 ≠ 0
Tactic:
norm_num
State after:
no goals

State before:
case inr.intro
z : ℤ
h : Prime z
⊢ z ≠ 0
Tactic:
exact h.ne_zero
State after:
no goals