internlm/Lean-Github huggingface dataset:
Theorem: factors_unique_prod'
Proof state before:
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ ∀ 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 ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ ∀ x ∈ g.erase p, OddPrimeOrFour x
Tactic:
exact fun q hq => 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 ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ f.prod = (g.erase p).prod
Tactic:
apply mul_left_cancel₀ hp.ne_zero
Proof state after:
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ p * f.prod = p * (g.erase p).prod
Theorem: factors_unique_prod'
Proof state before:
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ p * f.prod = p * (g.erase p).prod
Tactic:
rwa [Multiset.prod_erase hbg, ← Multiset.prod_cons]
Proof state after:
no goals
Theorem: oddFactors.zero
Proof state before:
⊢ oddFactors 0 = 0
Tactic:
simp [oddFactors]
Proof state after:
no goals
Theorem: oddFactors.not_two_mem
Proof state before:
x : ℕ
⊢ 2 ∉ oddFactors x
Tactic:
simp [oddFactors]
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.zero
Proof state before:
⊢ evenFactorExp 0 = 0
Tactic:
simp [evenFactorExp]
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 ∈ UniqueFactorizationMonoid.normalizedFactors x, 2 = a ∨ Odd a
Theorem: even_and_odd_factors''
Proof state before:
case h.e'_2
x : ℕ
hx : ¬x = 0
⊢ ∀ 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:
rw [eq_comm]
Proof state after:
case h.e'_2
x : ℕ
hx : ¬x = 0
a : ℕ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
⊢ a = 2 ∨ Odd a
Theorem: even_and_odd_factors''
Proof 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
Proof state after:
case h.e'_2
x : ℕ
hx : ¬x = 0
a : ℕ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Prime a
⊢ a = 2 ∨ 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
⊢ a = 2 ∨ Odd a
Tactic:
exact hprime.nat_prime.eq_two_or_odd'
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 ∈ 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 ∈ 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
Theorem: even_and_odd_factors'
Proof state before:
x : ℕ
⊢ UniqueFactorizationMonoid.normalizedFactors x = Multiset.replicate (evenFactorExp x) 2 + oddFactors x
Tactic:
convert even_and_odd_factors'' x
Proof state after:
case h.e'_3.h.e'_5
x : ℕ
⊢ Multiset.replicate (evenFactorExp x) 2 = Multiset.filter (Eq 2) (UniqueFactorizationMonoid.normalizedFactors x)
Theorem: even_and_odd_factors'
Proof state before:
case h.e'_3.h.e'_5
x : ℕ
⊢ Multiset.replicate (evenFactorExp x) 2 = Multiset.filter (Eq 2) (UniqueFactorizationMonoid.normalizedFactors x)
Tactic:
simp [evenFactorExp, ← Multiset.filter_eq]
Proof state after:
no goals
Theorem: even_and_oddFactors
Proof state before:
x : ℕ
hx : x ≠ 0
⊢ Associated x (2 ^ evenFactorExp x * (oddFactors x).prod)
Tactic:
convert(UniqueFactorizationMonoid.normalizedFactors_prod hx).symm
Proof state after:
case h.e'_4
x : ℕ
hx : x ≠ 0
⊢ 2 ^ evenFactorExp x * (oddFactors x).prod = (UniqueFactorizationMonoid.normalizedFactors x).prod
Theorem: even_and_oddFactors
Proof state before:
case h.e'_4
x : ℕ
hx : x ≠ 0
⊢ 2 ^ evenFactorExp x * (oddFactors x).prod = (UniqueFactorizationMonoid.normalizedFactors x).prod
Tactic:
simp [evenFactorExp]
Proof state after:
case h.e'_4
x : ℕ
hx : x ≠ 0
⊢ 2 ^ Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors x) * (oddFactors x).prod =
    (UniqueFactorizationMonoid.normalizedFactors x).prod
Theorem: even_and_oddFactors
Proof state before:
case h.e'_4
x : ℕ
hx : x ≠ 0
⊢ 2 ^ Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors x) * (oddFactors x).prod =
    (UniqueFactorizationMonoid.normalizedFactors x).prod
Tactic:
rw [Multiset.pow_count, ← Multiset.prod_add, ← even_and_odd_factors'' x]
Proof state after:
no goals
Theorem: factors_2_even
Proof state before:
z : ℕ
hz : z ≠ 0
⊢ evenFactorExp (4 * z) = 2 + evenFactorExp z
Tactic:
have h₀ : (4 : ℕ) ≠ 0 := four_ne_zero
Proof state after:
z : ℕ
hz : z ≠ 0
h₀ : 4 ≠ 0
⊢ evenFactorExp (4 * z) = 2 + evenFactorExp z
Theorem: factors_2_even
Proof state before:
z : ℕ
hz : z ≠ 0
h₀ : 4 ≠ 0
⊢ evenFactorExp (4 * z) = 2 + evenFactorExp z
Tactic:
have h₁ : (2 : ℕ) ^ 2 = 4 := by norm_num
Proof state after:
z : ℕ
hz : z ≠ 0
h₀ : 4 ≠ 0
h₁ : 2 ^ 2 = 4
⊢ evenFactorExp (4 * z) = 2 + evenFactorExp z
Theorem: factors_2_even
Proof state before:
z : ℕ
hz : z ≠ 0
h₀ : 4 ≠ 0
h₁ : 2 ^ 2 = 4
⊢ evenFactorExp (4 * z) = 2 + evenFactorExp z
Tactic:
simp [evenFactorExp]
Proof state after:
z : ℕ
hz : z ≠ 0
h₀ : 4 ≠ 0
h₁ : 2 ^ 2 = 4
⊢ Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors (4 * z)) =
    2 + Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors z)
Theorem: factors_2_even
Proof state before:
z : ℕ
hz : z ≠ 0
h₀ : 4 ≠ 0
h₁ : 2 ^ 2 = 4
⊢ Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors (4 * z)) =
    2 + Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors z)
Tactic:
rw [UniqueFactorizationMonoid.normalizedFactors_mul h₀ hz, Multiset.count_add, ← h₁,
  UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.count_nsmul,
  UniqueFactorizationMonoid.normalizedFactors_irreducible Nat.prime_two,
  normalize_eq, Multiset.count_singleton_self, mul_one]
Proof state after:
no goals
Theorem: factors_2_even
Proof state before:
z : ℕ
hz : z ≠ 0
h₀ : 4 ≠ 0
⊢ 2 ^ 2 = 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: factorsOddPrimeOrFour.prod'
Proof state before:
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ (factorsOddPrimeOrFour a).prod = a
Tactic:
have h₁ : (2 : ℕ) ^ 2 = 4 := by norm_num
Proof state after:
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
⊢ (factorsOddPrimeOrFour a).prod = a
Theorem: factorsOddPrimeOrFour.prod'
Proof state before:
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
⊢ (factorsOddPrimeOrFour a).prod = a
Tactic:
have := UniqueFactorizationMonoid.normalizedFactors_prod ha.ne'
Proof state after:
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
this : Associated (UniqueFactorizationMonoid.normalizedFactors a).prod a
⊢ (factorsOddPrimeOrFour a).prod = a
Theorem: factorsOddPrimeOrFour.prod'
Proof state before:
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
this : Associated (UniqueFactorizationMonoid.normalizedFactors a).prod a
⊢ (factorsOddPrimeOrFour a).prod = a
Tactic:
rw [associated_eq_eq] at this
Proof state after:
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
this : (UniqueFactorizationMonoid.normalizedFactors a).prod = a
⊢ (factorsOddPrimeOrFour a).prod = a
Theorem: factorsOddPrimeOrFour.prod'
Proof state before:
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
this : (UniqueFactorizationMonoid.normalizedFactors a).prod = a
⊢ (factorsOddPrimeOrFour a).prod = a
Tactic:
conv_rhs => rw [←this]
Proof state after:
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
this : (UniqueFactorizationMonoid.normalizedFactors a).prod = a
⊢ (factorsOddPrimeOrFour a).prod = (UniqueFactorizationMonoid.normalizedFactors a).prod
Theorem: factorsOddPrimeOrFour.prod'
Proof state before:
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
this : (UniqueFactorizationMonoid.normalizedFactors a).prod = a
⊢ (factorsOddPrimeOrFour a).prod = (UniqueFactorizationMonoid.normalizedFactors a).prod
Tactic:
obtain ⟨m, hm⟩ := even_iff_two_dvd.mp heven
Proof state after:
case intro
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
this : (UniqueFactorizationMonoid.normalizedFactors a).prod = a
m : ℕ
hm : evenFactorExp a = 2 * m
⊢ (factorsOddPrimeOrFour a).prod = (UniqueFactorizationMonoid.normalizedFactors a).prod
Theorem: factorsOddPrimeOrFour.prod'
Proof state before:
case intro
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
this : (UniqueFactorizationMonoid.normalizedFactors a).prod = a
m : ℕ
hm : evenFactorExp a = 2 * m
⊢ (factorsOddPrimeOrFour a).prod = (UniqueFactorizationMonoid.normalizedFactors a).prod
Tactic:
rw [even_and_odd_factors' _, Multiset.prod_add, factorsOddPrimeOrFour, Multiset.prod_add, hm,
  Nat.mul_div_right _ zero_lt_two, Multiset.prod_replicate, Multiset.prod_replicate, pow_mul, h₁]
Proof state after:
no goals
Theorem: factorsOddPrimeOrFour.prod'
Proof state before:
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ 2 ^ 2 = 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: factorsOddPrimeOrFour.unique'
Proof state before:
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
ha : 0 < f.prod
heven : Even (evenFactorExp f.prod)
⊢ factorsOddPrimeOrFour f.prod = f
Tactic:
refine factors_unique_prod' ?_ hf (factorsOddPrimeOrFour.prod' ha heven)
Proof state after:
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
ha : 0 < f.prod
heven : Even (evenFactorExp f.prod)
⊢ ∀ x ∈ factorsOddPrimeOrFour f.prod, OddPrimeOrFour x
Theorem: factorsOddPrimeOrFour.unique'
Proof state before:
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
ha : 0 < f.prod
heven : Even (evenFactorExp f.prod)
⊢ ∀ x ∈ factorsOddPrimeOrFour f.prod, OddPrimeOrFour x
Tactic:
intro x hx
Proof state after:
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
ha : 0 < f.prod
heven : Even (evenFactorExp f.prod)
x : ℕ
hx : x ∈ factorsOddPrimeOrFour f.prod
⊢ OddPrimeOrFour x
Theorem: factorsOddPrimeOrFour.unique'
Proof state before:
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
ha : 0 < f.prod
heven : Even (evenFactorExp f.prod)
x : ℕ
hx : x ∈ factorsOddPrimeOrFour f.prod
⊢ OddPrimeOrFour x
Tactic:
simp only [factorsOddPrimeOrFour, Multiset.mem_add] at hx
Proof state after:
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
ha : 0 < f.prod
heven : Even (evenFactorExp f.prod)
x : ℕ
hx : x ∈ Multiset.replicate (evenFactorExp f.prod / 2) 4 ∨ x ∈ oddFactors f.prod
⊢ OddPrimeOrFour x
Theorem: factorsOddPrimeOrFour.unique'
Proof state before:
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
ha : 0 < f.prod
heven : Even (evenFactorExp f.prod)
x : ℕ
hx : x ∈ Multiset.replicate (evenFactorExp f.prod / 2) 4 ∨ x ∈ oddFactors f.prod
⊢ OddPrimeOrFour x
Tactic:
apply Or.imp _ _ hx
Proof state after:
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
ha : 0 < f.prod
heven : Even (evenFactorExp f.prod)
x : ℕ
hx : x ∈ Multiset.replicate (evenFactorExp f.prod / 2) 4 ∨ x ∈ oddFactors f.prod
⊢ x ∈ Multiset.replicate (evenFactorExp f.prod / 2) 4 → x = 4

f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
ha : 0 < f.prod
heven : Even (evenFactorExp f.prod)
x : ℕ
hx : x ∈ Multiset.replicate (evenFactorExp f.prod / 2) 4 ∨ x ∈ oddFactors f.prod
⊢ x ∈ oddFactors f.prod → x.Prime ∧ Odd x
Theorem: factorsOddPrimeOrFour.unique'
Proof state before:
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
ha : 0 < f.prod
heven : Even (evenFactorExp f.prod)
x : ℕ
hx : x ∈ Multiset.replicate (evenFactorExp f.prod / 2) 4 ∨ x ∈ oddFactors f.prod
⊢ x ∈ Multiset.replicate (evenFactorExp f.prod / 2) 4 → x = 4
Tactic:
exact Multiset.eq_of_mem_replicate
Proof state after:
no goals
Theorem: factorsOddPrimeOrFour.unique'
Proof state before:
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
ha : 0 < f.prod
heven : Even (evenFactorExp f.prod)
x : ℕ
hx : x ∈ Multiset.replicate (evenFactorExp f.prod / 2) 4 ∨ x ∈ oddFactors f.prod
⊢ x ∈ oddFactors f.prod → x.Prime ∧ Odd x
Tactic:
simp only [oddFactors, Multiset.mem_filter]
Proof state after:
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
ha : 0 < f.prod
heven : Even (evenFactorExp f.prod)
x : ℕ
hx : x ∈ Multiset.replicate (evenFactorExp f.prod / 2) 4 ∨ x ∈ oddFactors f.prod
⊢ x ∈ UniqueFactorizationMonoid.normalizedFactors f.prod ∧ Odd x → x.Prime ∧ Odd x
Theorem: factorsOddPrimeOrFour.unique'
Proof state before:
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
ha : 0 < f.prod
heven : Even (evenFactorExp f.prod)
x : ℕ
hx : x ∈ Multiset.replicate (evenFactorExp f.prod / 2) 4 ∨ x ∈ oddFactors f.prod
⊢ x ∈ UniqueFactorizationMonoid.normalizedFactors f.prod ∧ Odd x → x.Prime ∧ Odd x
Tactic:
exact And.imp_left <| Prime.nat_prime ∘ (UniqueFactorizationMonoid.prime_of_normalized_factor _)
Proof state after:
no goals
Theorem: factorsOddPrimeOrFour.pow
Proof state before:
z n : ℕ
hz : Even (evenFactorExp z)
⊢ factorsOddPrimeOrFour (z ^ n) = n • factorsOddPrimeOrFour z
Tactic:
simp only [factorsOddPrimeOrFour, nsmul_add, Multiset.nsmul_replicate, evenFactorExp.pow,
  Nat.mul_div_assoc _ (even_iff_two_dvd.mp hz), oddFactors.pow]
Proof state after:
no goals
Theorem: Zsqrtd.exists
Proof state before:
d : ℤ
a : ℤ√d
him : a.im ≠ 0
⊢ ∃ c, a.norm = c.norm ∧ 0 ≤ c.re ∧ c.im ≠ 0
Tactic:
cases' le_or_lt a.re 0 with hre hre
Proof state after:
case inl
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : a.re ≤ 0
⊢ ∃ c, a.norm = c.norm ∧ 0 ≤ c.re ∧ c.im ≠ 0

case inr
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : 0 < a.re
⊢ ∃ c, a.norm = c.norm ∧ 0 ≤ c.re ∧ c.im ≠ 0
Theorem: Zsqrtd.exists
Proof state before:
case inl
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : a.re ≤ 0
⊢ ∃ c, a.norm = c.norm ∧ 0 ≤ c.re ∧ c.im ≠ 0
Tactic:
use -a
Proof state after:
case h
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : a.re ≤ 0
⊢ a.norm = (-a).norm ∧ 0 ≤ (-a).re ∧ (-a).im ≠ 0
Theorem: Zsqrtd.exists
Proof state before:
case h
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : a.re ≤ 0
⊢ a.norm = (-a).norm ∧ 0 ≤ (-a).re ∧ (-a).im ≠ 0
Tactic:
simp only [hre, him, Zsqrtd.norm_neg, eq_self_iff_true, Zsqrtd.neg_im, Zsqrtd.neg_re,
  and_self_iff, neg_nonneg, Ne, not_false_iff, neg_eq_zero]
Proof state after:
no goals
Theorem: Zsqrtd.exists
Proof state before:
case inr
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : 0 < a.re
⊢ ∃ c, a.norm = c.norm ∧ 0 ≤ c.re ∧ c.im ≠ 0
Tactic:
use a
Proof state after:
case h
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : 0 < a.re
⊢ a.norm = a.norm ∧ 0 ≤ a.re ∧ a.im ≠ 0
Theorem: Zsqrtd.exists
Proof state before:
case h
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : 0 < a.re
⊢ a.norm = a.norm ∧ 0 ≤ a.re ∧ a.im ≠ 0
Tactic:
simp only [hre.le, him, eq_self_iff_true, and_self_iff, Ne, not_false_iff]
Proof state after:
no goals
Theorem: factors2
Proof state before:
a : ℤ√(-3)
heven : Even a.norm
⊢ ∃ b, a.norm = 4 * b.norm
Tactic:
have hparity : Even a.re ↔ Even a.im := by
  have : ¬ Even (3 : ℤ) := by decide
  simpa [this, two_ne_zero, Zsqrtd.norm_def, parity_simps] using heven
Proof state after:
a : ℤ√(-3)
heven : Even a.norm
hparity : Even a.re ↔ Even a.im
⊢ ∃ b, a.norm = 4 * b.norm
Theorem: factors2
Proof state before:
a : ℤ√(-3)
heven : Even a.norm
hparity : Even a.re ↔ Even a.im
⊢ ∃ b, a.norm = 4 * b.norm
Tactic:
simp only [iff_iff_and_or_not_and_not, ← Int.odd_iff_not_even] at hparity
Proof state after:
a : ℤ√(-3)
heven : Even a.norm
hparity : Even a.re ∧ Even a.im ∨ Odd a.re ∧ Odd a.im
⊢ ∃ b, a.norm = 4 * b.norm
Theorem: factors2
Proof state before:
a : ℤ√(-3)
heven : Even a.norm
hparity : Even a.re ∧ Even a.im ∨ Odd a.re ∧ Odd a.im
⊢ ∃ b, a.norm = 4 * b.norm
Tactic:
obtain ⟨⟨c, hc⟩, ⟨d, hd⟩⟩ | ⟨hre, him⟩ := hparity
Proof state after:
case inl.intro.intro.intro
a : ℤ√(-3)
heven : Even a.norm
c : ℤ
hc : a.re = c + c
d : ℤ
hd : a.im = d + d
⊢ ∃ b, a.norm = 4 * b.norm

case inr.intro
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
⊢ ∃ b, a.norm = 4 * b.norm
Theorem: factors2
Proof state before:
a : ℤ√(-3)
heven : Even a.norm
⊢ Even a.re ↔ Even a.im
Tactic:
have : ¬ Even (3 : ℤ) := by decide
Proof state after:
a : ℤ√(-3)
heven : Even a.norm
this : ¬Even 3
⊢ Even a.re ↔ Even a.im
Theorem: factors2
Proof state before:
a : ℤ√(-3)
heven : Even a.norm
this : ¬Even 3
⊢ Even a.re ↔ Even a.im
Tactic:
simpa [this, two_ne_zero, Zsqrtd.norm_def, parity_simps] using heven
Proof state after:
no goals
Theorem: factors2
Proof state before:
a : ℤ√(-3)
heven : Even a.norm
⊢ ¬Even 3
Tactic:
decide
Proof state after:
no goals
Theorem: factors2
Proof state before:
case inl.intro.intro.intro
a : ℤ√(-3)
heven : Even a.norm
c : ℤ
hc : a.re = c + c
d : ℤ
hd : a.im = d + d
⊢ ∃ b, a.norm = 4 * b.norm
Tactic:
use ⟨c, d⟩
Proof state after:
case h
a : ℤ√(-3)
heven : Even a.norm
c : ℤ
hc : a.re = c + c
d : ℤ
hd : a.im = d + d
⊢ a.norm = 4 * { re := c, im := d }.norm
Theorem: factors2
Proof state before:
case h
a : ℤ√(-3)
heven : Even a.norm
c : ℤ
hc : a.re = c + c
d : ℤ
hd : a.im = d + d
⊢ a.norm = 4 * { re := c, im := d }.norm
Tactic:
simp only [Zsqrtd.norm_def, hc, hd]
Proof state after:
case h
a : ℤ√(-3)
heven : Even a.norm
c : ℤ
hc : a.re = c + c
d : ℤ
hd : a.im = d + d
⊢ (c + c) * (c + c) - -3 * (d + d) * (d + d) = 4 * (c * c - -3 * d * d)
Theorem: factors2
Proof state before:
case h
a : ℤ√(-3)
heven : Even a.norm
c : ℤ
hc : a.re = c + c
d : ℤ
hd : a.im = d + d
⊢ (c + c) * (c + c) - -3 * (d + d) * (d + d) = 4 * (c * c - -3 * d * d)
Tactic:
ring
Proof state after:
no goals
Theorem: factors2
Proof state before:
case inr.intro
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
⊢ ∃ b, a.norm = 4 * b.norm
Tactic:
cases' Int.four_dvd_add_or_sub_of_odd hre him with h4 h4
Proof state after:
case inr.intro.inl
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
h4 : 4 ∣ a.re + a.im
⊢ ∃ b, a.norm = 4 * b.norm

case inr.intro.inr
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
h4 : 4 ∣ a.re - a.im
⊢ ∃ b, a.norm = 4 * b.norm