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

State before:
z : ℤ
h : OddPrimeOrFour z
⊢ OddPrimeOrFour (Abs.abs z)
Tactic:
obtain rfl | ⟨hp, ho⟩ := h
State after:
case inl

⊢ OddPrimeOrFour (Abs.abs 4)

case inr.intro
z : ℤ
hp : Prime z
ho : Odd z
⊢ OddPrimeOrFour (Abs.abs z)

State before:
case inl

⊢ OddPrimeOrFour (Abs.abs 4)
Tactic:
left
State after:
case inl.h

⊢ Abs.abs 4 = 4

State before:
case inl.h

⊢ Abs.abs 4 = 4
Tactic:
rw [abs_eq_self]
State after:
case inl.h

⊢ 0 ≤ 4

State before:
case inl.h

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

State before:
case inr.intro
z : ℤ
hp : Prime z
ho : Odd z
⊢ OddPrimeOrFour (Abs.abs z)
Tactic:
right
State after:
case inr.intro.h
z : ℤ
hp : Prime z
ho : Odd z
⊢ Prime (Abs.abs z) ∧ Odd (Abs.abs z)

State before:
case inr.intro.h
z : ℤ
hp : Prime z
ho : Odd z
⊢ Prime (Abs.abs z) ∧ Odd (Abs.abs z)
Tactic:
exact ⟨hp.abs, odd_abs.mpr ho⟩
State after:
no goals