Theorem: factorsOddPrimeOrFour.nonneg (Flt/OddPrimeOrFour.lean)

State before:
z a : ℤ
ha : a ∈ factorsOddPrimeOrFour z
⊢ 0 ≤ a
Tactic:
simp only [factorsOddPrimeOrFour, Multiset.mem_add] at ha
State after:
z a : ℤ
ha : a ∈ Multiset.replicate (evenFactorExp z / 2) 4 ∨ a ∈ oddFactors z
⊢ 0 ≤ a

State before:
z a : ℤ
ha : a ∈ Multiset.replicate (evenFactorExp z / 2) 4 ∨ a ∈ oddFactors z
⊢ 0 ≤ a
Tactic:
cases ha with
| inl ha =>
  rw [Multiset.eq_of_mem_replicate ha]
  norm_num
| inr ha =>
  exact oddFactors.nonneg ha
State after:
no goals

State before:
case inl
z a : ℤ
ha : a ∈ Multiset.replicate (evenFactorExp z / 2) 4
⊢ 0 ≤ a
Tactic:
rw [Multiset.eq_of_mem_replicate ha]
State after:
case inl
z a : ℤ
ha : a ∈ Multiset.replicate (evenFactorExp z / 2) 4
⊢ 0 ≤ 4

State before:
case inl
z a : ℤ
ha : a ∈ Multiset.replicate (evenFactorExp z / 2) 4
⊢ 0 ≤ 4
Tactic:
norm_num
State after:
no goals

State before:
case inr
z a : ℤ
ha : a ∈ oddFactors z
⊢ 0 ≤ a
Tactic:
exact oddFactors.nonneg ha
State after:
no goals