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

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

⊢ 1 < abs 4

case inr.intro
z : ℤ
h : Prime z
⊢ 1 < abs z

State before:
case inl

⊢ 1 < abs 4
Tactic:
rw [Int.abs_eq_natAbs]
State after:
case inl

⊢ 1 < ↑(Int.natAbs 4)

State before:
case inl

⊢ 1 < ↑(Int.natAbs 4)
Tactic:
norm_num
State after:
no goals

State before:
case inr.intro
z : ℤ
h : Prime z
⊢ 1 < abs z
Tactic:
rw [Int.abs_eq_natAbs]
State after:
case inr.intro
z : ℤ
h : Prime z
⊢ 1 < ↑(Int.natAbs z)

State before:
case inr.intro
z : ℤ
h : Prime z
⊢ 1 < ↑(Int.natAbs z)
Tactic:
rw [Int.prime_iff_natAbs_prime] at h
State after:
case inr.intro
z : ℤ
h : Nat.Prime (Int.natAbs z)
⊢ 1 < ↑(Int.natAbs z)

State before:
case inr.intro
z : ℤ
h : Nat.Prime (Int.natAbs z)
⊢ 1 < ↑(Int.natAbs z)
Tactic:
norm_cast
State after:
case inr.intro
z : ℤ
h : Nat.Prime (Int.natAbs z)
⊢ 1 < Int.natAbs z

State before:
case inr.intro
z : ℤ
h : Nat.Prime (Int.natAbs z)
⊢ 1 < Int.natAbs z
Tactic:
exact h.one_lt
State after:
no goals