Theorem: OddPrimeOrFour.not_unit (FltRegular/FltThree/OddPrimeOrFour.lean)

State before:
z : ℕ
h : OddPrimeOrFour z
⊢ ¬IsUnit z
Tactic:
obtain rfl | ⟨h, -⟩ := h
State after:
case inl

⊢ ¬IsUnit 4

case inr.intro
z : ℕ
h : z.Prime
⊢ ¬IsUnit z

State before:
case inl

⊢ ¬IsUnit 4
Tactic:
rw [isUnit_iff_dvd_one]
State after:
case inl

⊢ ¬4 ∣ 1

State before:
case inl

⊢ ¬4 ∣ 1
Tactic:
norm_num
State after:
no goals

State before:
case inr.intro
z : ℕ
h : z.Prime
⊢ ¬IsUnit z
Tactic:
exact h.not_unit
State after:
no goals