Theorem: even_and_odd_factors'' (FltRegular/FltThree/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 ∈ UniqueFactorizationMonoid.normalizedFactors x, 2 = a ∨ Odd a

State before:
case h.e'_2
x : ℕ
hx : ¬x = 0
⊢ ∀ 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:
rw [eq_comm]
State after:
case h.e'_2
x : ℕ
hx : ¬x = 0
a : ℕ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
⊢ a = 2 ∨ Odd a

State before:
case h.e'_2
x : ℕ
hx : ¬x = 0
a : ℕ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
⊢ a = 2 ∨ 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
⊢ a = 2 ∨ Odd a

State before:
case h.e'_2
x : ℕ
hx : ¬x = 0
a : ℕ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Prime a
⊢ a = 2 ∨ Odd a
Tactic:
exact hprime.nat_prime.eq_two_or_odd'
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 ∈ UniqueFactorizationMonoid.normalizedFactors x, ¬(2 = a ∧ Odd a)

State before:
case h.e'_3.h.e'_6
x : ℕ
hx : ¬x = 0
⊢ ∀ 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