Theorem: even_and_odd_factors'' (Flt/OddPrimeOrFour.lean)

State before:
x : ℤ
⊢ UniqueFactorizationMonoid.normalizedFactors x =
    Multiset.filter (Eq 2) (UniqueFactorizationMonoid.normalizedFactors x) + oddFactors x
Tactic:
by_cases hx : x = 0
State after:
case pos
x : ℤ
hx : x = 0
⊢ UniqueFactorizationMonoid.normalizedFactors x =
    Multiset.filter (Eq 2) (UniqueFactorizationMonoid.normalizedFactors x) + oddFactors x

case neg
x : ℤ
hx : ¬x = 0
⊢ UniqueFactorizationMonoid.normalizedFactors x =
    Multiset.filter (Eq 2) (UniqueFactorizationMonoid.normalizedFactors x) + oddFactors x

State before:
case neg
x : ℤ
hx : ¬x = 0
⊢ UniqueFactorizationMonoid.normalizedFactors x =
    Multiset.filter (Eq 2) (UniqueFactorizationMonoid.normalizedFactors x) + oddFactors x
Tactic:
simp [evenFactorExp, oddFactors]
State after:
case neg
x : ℤ
hx : ¬x = 0
⊢ UniqueFactorizationMonoid.normalizedFactors x =
    Multiset.filter (Eq 2) (UniqueFactorizationMonoid.normalizedFactors x) +
      Multiset.filter Odd (UniqueFactorizationMonoid.normalizedFactors x)

State before:
case neg
x : ℤ
hx : ¬x = 0
⊢ UniqueFactorizationMonoid.normalizedFactors x =
    Multiset.filter (Eq 2) (UniqueFactorizationMonoid.normalizedFactors x) +
      Multiset.filter Odd (UniqueFactorizationMonoid.normalizedFactors x)
Tactic:
rw [Multiset.filter_add_filter]
State after:
case neg
x : ℤ
hx : ¬x = 0
⊢ UniqueFactorizationMonoid.normalizedFactors x =
    Multiset.filter (fun a => 2 = a ∨ Odd a) (UniqueFactorizationMonoid.normalizedFactors x) +
      Multiset.filter (fun a => 2 = a ∧ Odd a) (UniqueFactorizationMonoid.normalizedFactors x)

State before:
case neg
x : ℤ
hx : ¬x = 0
⊢ UniqueFactorizationMonoid.normalizedFactors x =
    Multiset.filter (fun a => 2 = a ∨ Odd a) (UniqueFactorizationMonoid.normalizedFactors x) +
      Multiset.filter (fun a => 2 = a ∧ Odd a) (UniqueFactorizationMonoid.normalizedFactors x)
Tactic:
convert (add_zero
  (Multiset.filter (fun a => 2 = a ∨ Odd a) (UniqueFactorizationMonoid.normalizedFactors x))).symm
State after:
case h.e'_2
x : ℤ
hx : ¬x = 0
⊢ UniqueFactorizationMonoid.normalizedFactors x =
    Multiset.filter (fun a => 2 = a ∨ Odd a) (UniqueFactorizationMonoid.normalizedFactors x)

case h.e'_3.h.e'_6
x : ℤ
hx : ¬x = 0
⊢ Multiset.filter (fun a => 2 = a ∧ Odd a) (UniqueFactorizationMonoid.normalizedFactors x) = 0

State before:
case pos
x : ℤ
hx : x = 0
⊢ UniqueFactorizationMonoid.normalizedFactors x =
    Multiset.filter (Eq 2) (UniqueFactorizationMonoid.normalizedFactors x) + oddFactors x
Tactic:
rw [hx, UniqueFactorizationMonoid.normalizedFactors_zero, oddFactors.zero, Multiset.filter_zero,
  add_zero]
State after:
no goals

State before:
case h.e'_2
x : ℤ
hx : ¬x = 0
⊢ UniqueFactorizationMonoid.normalizedFactors x =
    Multiset.filter (fun a => 2 = a ∨ Odd a) (UniqueFactorizationMonoid.normalizedFactors x)
Tactic:
symm
State after:
case h.e'_2
x : ℤ
hx : ¬x = 0
⊢ Multiset.filter (fun a => 2 = a ∨ Odd a) (UniqueFactorizationMonoid.normalizedFactors x) =
    UniqueFactorizationMonoid.normalizedFactors x

State before:
case h.e'_2
x : ℤ
hx : ¬x = 0
⊢ Multiset.filter (fun a => 2 = a ∨ Odd a) (UniqueFactorizationMonoid.normalizedFactors x) =
    UniqueFactorizationMonoid.normalizedFactors x
Tactic:
rw [Multiset.filter_eq_self]
State after:
case h.e'_2
x : ℤ
hx : ¬x = 0
⊢ ∀ (a : ℤ), a ∈ UniqueFactorizationMonoid.normalizedFactors x → 2 = a ∨ Odd a

State before:
case h.e'_2
x : ℤ
hx : ¬x = 0
⊢ ∀ (a : ℤ), a ∈ UniqueFactorizationMonoid.normalizedFactors x → 2 = a ∨ Odd a
Tactic:
intro a ha
State after:
case h.e'_2
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
⊢ 2 = a ∨ Odd a

State before:
case h.e'_2
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
⊢ 2 = a ∨ Odd a
Tactic:
have hprime : Prime a := UniqueFactorizationMonoid.prime_of_normalized_factor a ha
State after:
case h.e'_2
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Prime a
⊢ 2 = a ∨ Odd a

State before:
case h.e'_2
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Prime a
⊢ 2 = a ∨ Odd a
Tactic:
have := UniqueFactorizationMonoid.normalize_normalized_factor a ha
State after:
case h.e'_2
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Prime a
this : ↑normalize a = a
⊢ 2 = a ∨ Odd a

State before:
case h.e'_2
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Prime a
this : ↑normalize a = a
⊢ 2 = a ∨ Odd a
Tactic:
rw [← Int.abs_eq_normalize, ← Int.coe_natAbs] at this
State after:
case h.e'_2
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Prime a
this : ↑(Int.natAbs a) = a
⊢ 2 = a ∨ Odd a

State before:
case h.e'_2
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Prime a
this : ↑(Int.natAbs a) = a
⊢ 2 = a ∨ Odd a
Tactic:
rw [← this]
State after:
case h.e'_2
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Prime a
this : ↑(Int.natAbs a) = a
⊢ 2 = ↑(Int.natAbs a) ∨ Odd ↑(Int.natAbs a)

State before:
case h.e'_2
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Prime a
this : ↑(Int.natAbs a) = a
⊢ 2 = ↑(Int.natAbs a) ∨ Odd ↑(Int.natAbs a)
Tactic:
rw [Int.prime_iff_natAbs_prime] at hprime
State after:
case h.e'_2
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Nat.Prime (Int.natAbs a)
this : ↑(Int.natAbs a) = a
⊢ 2 = ↑(Int.natAbs a) ∨ Odd ↑(Int.natAbs a)

State before:
case h.e'_2
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Nat.Prime (Int.natAbs a)
this : ↑(Int.natAbs a) = a
⊢ 2 = ↑(Int.natAbs a) ∨ Odd ↑(Int.natAbs a)
Tactic:
rcases Nat.Prime.eq_two_or_odd' hprime with (h2 | hodd)
State after:
case h.e'_2.inl
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Nat.Prime (Int.natAbs a)
this : ↑(Int.natAbs a) = a
h2 : Int.natAbs a = 2
⊢ 2 = ↑(Int.natAbs a) ∨ Odd ↑(Int.natAbs a)

case h.e'_2.inr
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Nat.Prime (Int.natAbs a)
this : ↑(Int.natAbs a) = a
hodd : Odd (Int.natAbs a)
⊢ 2 = ↑(Int.natAbs a) ∨ Odd ↑(Int.natAbs a)

State before:
case h.e'_2.inl
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Nat.Prime (Int.natAbs a)
this : ↑(Int.natAbs a) = a
h2 : Int.natAbs a = 2
⊢ 2 = ↑(Int.natAbs a) ∨ Odd ↑(Int.natAbs a)
Tactic:
simp [h2]
State after:
no goals

State before:
case h.e'_2.inr
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Nat.Prime (Int.natAbs a)
this : ↑(Int.natAbs a) = a
hodd : Odd (Int.natAbs a)
⊢ 2 = ↑(Int.natAbs a) ∨ Odd ↑(Int.natAbs a)
Tactic:
right
State after:
case h.e'_2.inr.h
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Nat.Prime (Int.natAbs a)
this : ↑(Int.natAbs a) = a
hodd : Odd (Int.natAbs a)
⊢ Odd ↑(Int.natAbs a)

State before:
case h.e'_2.inr.h
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Nat.Prime (Int.natAbs a)
this : ↑(Int.natAbs a) = a
hodd : Odd (Int.natAbs a)
⊢ Odd ↑(Int.natAbs a)
Tactic:
rw [this]
State after:
case h.e'_2.inr.h
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Nat.Prime (Int.natAbs a)
this : ↑(Int.natAbs a) = a
hodd : Odd (Int.natAbs a)
⊢ Odd a

State before:
case h.e'_2.inr.h
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Nat.Prime (Int.natAbs a)
this : ↑(Int.natAbs a) = a
hodd : Odd (Int.natAbs a)
⊢ Odd a
Tactic:
exact Int.natAbs_odd.1 hodd
State after:
no goals

State before:
case h.e'_3.h.e'_6
x : ℤ
hx : ¬x = 0
⊢ Multiset.filter (fun a => 2 = a ∧ Odd a) (UniqueFactorizationMonoid.normalizedFactors x) = 0
Tactic:
rw [Multiset.filter_eq_nil]
State after:
case h.e'_3.h.e'_6
x : ℤ
hx : ¬x = 0
⊢ ∀ (a : ℤ), a ∈ UniqueFactorizationMonoid.normalizedFactors x → ¬(2 = a ∧ Odd a)

State before:
case h.e'_3.h.e'_6
x : ℤ
hx : ¬x = 0
⊢ ∀ (a : ℤ), a ∈ UniqueFactorizationMonoid.normalizedFactors x → ¬(2 = a ∧ Odd a)
Tactic:
rintro a ha ⟨rfl, hodd⟩
State after:
case h.e'_3.h.e'_6.intro
x : ℤ
hx : ¬x = 0
ha : 2 ∈ UniqueFactorizationMonoid.normalizedFactors x
hodd : Odd 2
⊢ False

State before:
case h.e'_3.h.e'_6.intro
x : ℤ
hx : ¬x = 0
ha : 2 ∈ UniqueFactorizationMonoid.normalizedFactors x
hodd : Odd 2
⊢ False
Tactic:
norm_num at hodd
State after:
no goals