internlm/Lean-Github huggingface dataset:
Theorem: factors_unique_prod'
Proof state before:
case h₂
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
⊢ Multiset.Rel Associated (p ::ₘ f) g
Tactic:
have hp := hf p (Multiset.mem_cons_self _ _)
Proof state after:
case h₂
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
⊢ Multiset.Rel Associated (p ::ₘ f) g
Theorem: factors_unique_prod'
Proof state before:
case h₂
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
⊢ Multiset.Rel Associated (p ::ₘ f) g
Tactic:
have hdvd : p ∣ g.prod :=
  by
  rw [← hfg.dvd_iff_dvd_right, Multiset.prod_cons]
  exact dvd_mul_right _ _
Proof state after:
case h₂
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
hdvd : p ∣ Multiset.prod g
⊢ Multiset.Rel Associated (p ::ₘ f) g
Theorem: factors_unique_prod'
Proof state before:
case h₂
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
hdvd : p ∣ Multiset.prod g
⊢ Multiset.Rel Associated (p ::ₘ f) g
Tactic:
obtain ⟨b, hbg, hb⟩ := exists_associated_mem_of_dvd_prod'' hp hg hdvd
Proof state after:
case h₂.intro.intro
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
hdvd : p ∣ Multiset.prod g
b : ℤ
hbg : b ∈ g
hb : Associated p b
⊢ Multiset.Rel Associated (p ::ₘ f) g
Theorem: factors_unique_prod'
Proof state before:
case h₂.intro.intro
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
hdvd : p ∣ Multiset.prod g
b : ℤ
hbg : b ∈ g
hb : Associated p b
⊢ Multiset.Rel Associated (p ::ₘ f) g
Tactic:
rw [← Multiset.cons_erase hbg]
Proof state after:
case h₂.intro.intro
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
hdvd : p ∣ Multiset.prod g
b : ℤ
hbg : b ∈ g
hb : Associated p b
⊢ Multiset.Rel Associated (p ::ₘ f) (b ::ₘ Multiset.erase g b)
Theorem: factors_unique_prod'
Proof state before:
case h₂.intro.intro
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
hdvd : p ∣ Multiset.prod g
b : ℤ
hbg : b ∈ g
hb : Associated p b
⊢ Multiset.Rel Associated (p ::ₘ f) (b ::ₘ Multiset.erase g b)
Tactic:
apply Multiset.Rel.cons hb
Proof state after:
case h₂.intro.intro
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
hdvd : p ∣ Multiset.prod g
b : ℤ
hbg : b ∈ g
hb : Associated p b
⊢ Multiset.Rel Associated f (Multiset.erase g b)
Theorem: factors_unique_prod'
Proof state before:
case h₂.intro.intro
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
hdvd : p ∣ Multiset.prod g
b : ℤ
hbg : b ∈ g
hb : Associated p b
⊢ Multiset.Rel Associated f (Multiset.erase g b)
Tactic:
apply ih _ _ _
Proof state after:
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
hdvd : p ∣ Multiset.prod g
b : ℤ
hbg : b ∈ g
hb : Associated p b
⊢ ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x

p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
hdvd : p ∣ Multiset.prod g
b : ℤ
hbg : b ∈ g
hb : Associated p b
⊢ ∀ (x : ℤ), x ∈ Multiset.erase g b → OddPrimeOrFour x

p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
hdvd : p ∣ Multiset.prod g
b : ℤ
hbg : b ∈ g
hb : Associated p b
⊢ Associated (Multiset.prod f) (Multiset.prod (Multiset.erase g b))
Theorem: factors_unique_prod'
Proof state before:
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
⊢ p ∣ Multiset.prod g
Tactic:
rw [← hfg.dvd_iff_dvd_right, Multiset.prod_cons]
Proof state after:
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
⊢ p ∣ p * Multiset.prod f
Theorem: factors_unique_prod'
Proof state before:
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
⊢ p ∣ p * Multiset.prod f
Tactic:
exact dvd_mul_right _ _
Proof state after:
no goals
Theorem: factors_unique_prod'
Proof state before:
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
hdvd : p ∣ Multiset.prod g
b : ℤ
hbg : b ∈ g
hb : Associated p b
⊢ ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
Tactic:
exact fun q hq => hf _ (Multiset.mem_cons_of_mem hq)
Proof state after:
no goals
Theorem: factors_unique_prod'
Proof state before:
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
hdvd : p ∣ Multiset.prod g
b : ℤ
hbg : b ∈ g
hb : Associated p b
⊢ ∀ (x : ℤ), x ∈ Multiset.erase g b → OddPrimeOrFour x
Tactic:
exact fun q (hq : q ∈ g.erase b) => hg q (Multiset.mem_of_mem_erase hq)
Proof state after:
no goals
Theorem: factors_unique_prod'
Proof state before:
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
hdvd : p ∣ Multiset.prod g
b : ℤ
hbg : b ∈ g
hb : Associated p b
⊢ Associated (Multiset.prod f) (Multiset.prod (Multiset.erase g b))
Tactic:
apply Associated.of_mul_left _ hb hp.ne_zero
Proof state after:
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
hdvd : p ∣ Multiset.prod g
b : ℤ
hbg : b ∈ g
hb : Associated p b
⊢ Associated (p * Multiset.prod f) (b * Multiset.prod (Multiset.erase g b))
Theorem: factors_unique_prod'
Proof state before:
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
hdvd : p ∣ Multiset.prod g
b : ℤ
hbg : b ∈ g
hb : Associated p b
⊢ Associated (p * Multiset.prod f) (b * Multiset.prod (Multiset.erase g b))
Tactic:
rwa [← Multiset.prod_cons, ← Multiset.prod_cons, Multiset.cons_erase hbg]
Proof state after:
no goals
Theorem: oddFactors.not_two_mem
Proof state before:
x : ℤ
⊢ ¬2 ∈ oddFactors x
Tactic:
simp only [oddFactors, even_bit0, not_true, not_false_iff, Int.odd_iff_not_even, and_false_iff,
  Multiset.mem_filter]
Proof state after:
no goals
Theorem: oddFactors.nonneg
Proof state before:
z a : ℤ
ha : a ∈ oddFactors z
⊢ 0 ≤ a
Tactic:
simp only [oddFactors, Multiset.mem_filter] at ha
Proof state after:
z a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors z ∧ Odd a
⊢ 0 ≤ a
Theorem: oddFactors.nonneg
Proof state before:
z a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors z ∧ Odd a
⊢ 0 ≤ a
Tactic:
exact
  Int.nonneg_of_normalize_eq_self (UniqueFactorizationMonoid.normalize_normalized_factor a ha.1)
Proof state after:
no goals
Theorem: oddFactors.pow
Proof state before:
z : ℤ
n : ℕ
⊢ oddFactors (z ^ n) = n • oddFactors z
Tactic:
simp only [oddFactors]
Proof state after:
z : ℤ
n : ℕ
⊢ Multiset.filter Odd (UniqueFactorizationMonoid.normalizedFactors (z ^ n)) =
    n • Multiset.filter Odd (UniqueFactorizationMonoid.normalizedFactors z)
Theorem: oddFactors.pow
Proof state before:
z : ℤ
n : ℕ
⊢ Multiset.filter Odd (UniqueFactorizationMonoid.normalizedFactors (z ^ n)) =
    n • Multiset.filter Odd (UniqueFactorizationMonoid.normalizedFactors z)
Tactic:
rw [UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.filter_nsmul]
Proof state after:
no goals
Theorem: evenFactorExp.pow
Proof state before:
z : ℤ
n : ℕ
⊢ evenFactorExp (z ^ n) = n * evenFactorExp z
Tactic:
simp only [evenFactorExp]
Proof state after:
z : ℤ
n : ℕ
⊢ Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors (z ^ n)) =
    n * Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors z)
Theorem: evenFactorExp.pow
Proof state before:
z : ℤ
n : ℕ
⊢ Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors (z ^ n)) =
    n * Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors z)
Tactic:
rw [UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.count_nsmul]
Proof state after:
no goals
Theorem: even_and_odd_factors''
Proof state before:
x : ℤ
⊢ UniqueFactorizationMonoid.normalizedFactors x =
    Multiset.filter (Eq 2) (UniqueFactorizationMonoid.normalizedFactors x) + oddFactors x
Tactic:
by_cases hx : x = 0
Proof 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
Theorem: even_and_odd_factors''
Proof state before:
case neg
x : ℤ
hx : ¬x = 0
⊢ UniqueFactorizationMonoid.normalizedFactors x =
    Multiset.filter (Eq 2) (UniqueFactorizationMonoid.normalizedFactors x) + oddFactors x
Tactic:
simp [evenFactorExp, oddFactors]
Proof state after:
case neg
x : ℤ
hx : ¬x = 0
⊢ UniqueFactorizationMonoid.normalizedFactors x =
    Multiset.filter (Eq 2) (UniqueFactorizationMonoid.normalizedFactors x) +
      Multiset.filter Odd (UniqueFactorizationMonoid.normalizedFactors x)
Theorem: even_and_odd_factors''
Proof 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]
Proof 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)
Theorem: even_and_odd_factors''
Proof 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
Proof 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
Theorem: even_and_odd_factors''
Proof 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]
Proof state after:
no goals
Theorem: even_and_odd_factors''
Proof 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
Proof state after:
case h.e'_2
x : ℤ
hx : ¬x = 0
⊢ Multiset.filter (fun a => 2 = a ∨ Odd a) (UniqueFactorizationMonoid.normalizedFactors x) =
    UniqueFactorizationMonoid.normalizedFactors x
Theorem: even_and_odd_factors''
Proof 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]
Proof state after:
case h.e'_2
x : ℤ
hx : ¬x = 0
⊢ ∀ (a : ℤ), a ∈ UniqueFactorizationMonoid.normalizedFactors x → 2 = a ∨ Odd a
Theorem: even_and_odd_factors''
Proof state before:
case h.e'_2
x : ℤ
hx : ¬x = 0
⊢ ∀ (a : ℤ), a ∈ UniqueFactorizationMonoid.normalizedFactors x → 2 = a ∨ Odd a
Tactic:
intro a ha
Proof state after:
case h.e'_2
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
⊢ 2 = a ∨ Odd a
Theorem: even_and_odd_factors''
Proof 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
Proof state after:
case h.e'_2
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Prime a
⊢ 2 = a ∨ Odd a
Theorem: even_and_odd_factors''
Proof 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
Proof 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
Theorem: even_and_odd_factors''
Proof 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
Proof 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
Theorem: even_and_odd_factors''
Proof 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]
Proof 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)
Theorem: even_and_odd_factors''
Proof 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
Proof 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)
Theorem: even_and_odd_factors''
Proof 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)
Proof 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)
Theorem: even_and_odd_factors''
Proof 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]
Proof state after:
no goals
Theorem: even_and_odd_factors''
Proof 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
Proof 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)
Theorem: even_and_odd_factors''
Proof 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]
Proof 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
Theorem: even_and_odd_factors''
Proof 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
Proof state after:
no goals
Theorem: even_and_odd_factors''
Proof 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]
Proof state after:
case h.e'_3.h.e'_6
x : ℤ
hx : ¬x = 0
⊢ ∀ (a : ℤ), a ∈ UniqueFactorizationMonoid.normalizedFactors x → ¬(2 = a ∧ Odd a)
Theorem: even_and_odd_factors''
Proof 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⟩
Proof state after:
case h.e'_3.h.e'_6.intro
x : ℤ
hx : ¬x = 0
ha : 2 ∈ UniqueFactorizationMonoid.normalizedFactors x
hodd : Odd 2
⊢ False
Theorem: even_and_odd_factors''
Proof 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
Proof state after:
no goals