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

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

⊢ 1 < 4

case inr.intro
z : ℕ
h : z.Prime
⊢ 1 < z

State before:
case inl

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

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