Theorem: OddPrimeOrFour.ne_one (FltRegular/FltThree/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 : z.Prime
⊢ z ≠ 1

State before:
case inl

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

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