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

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

⊢ 4 ≠ 1

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

State before:
case inl

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

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