internlm/Lean-Github huggingface dataset:
Theorem: factors_unique_prod
Proof state before:
case a
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hassoc : Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))
⊢ Associated (Multiset.prod (Multiset.map Zsqrtd.norm f)) (Multiset.prod (Multiset.map Zsqrtd.norm g))
Tactic:
rwa [prod_map_norm, prod_map_norm]
Proof state after:
no goals
Theorem: factorization'.coprime_of_mem
Proof state before:
a b : ℤ√(-3)
h : IsCoprime a.re a.im
hmem : b ∈ factorization' h
⊢ IsCoprime b.re b.im
Tactic:
obtain ⟨h1, -⟩ := factorization'_prop h
Proof state after:
case intro
a b : ℤ√(-3)
h : IsCoprime a.re a.im
hmem : b ∈ factorization' h
h1 : a = Multiset.prod (factorization' h) ∨ a = -Multiset.prod (factorization' h)
⊢ IsCoprime b.re b.im
Theorem: factorization'.coprime_of_mem
Proof state before:
case intro
a b : ℤ√(-3)
h : IsCoprime a.re a.im
hmem : b ∈ factorization' h
h1 : a = Multiset.prod (factorization' h) ∨ a = -Multiset.prod (factorization' h)
⊢ IsCoprime b.re b.im
Tactic:
set f := factorization' h
Proof state after:
case intro
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
⊢ IsCoprime b.re b.im
Theorem: factorization'.coprime_of_mem
Proof state before:
case intro
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
⊢ IsCoprime b.re b.im
Tactic:
apply Zsqrtd.coprime_of_dvd_coprime h
Proof state after:
case intro
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
⊢ b ∣ a
Theorem: factorization'.coprime_of_mem
Proof state before:
case intro
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
⊢ b ∣ a
Tactic:
apply (Multiset.dvd_prod hmem).trans
Proof state after:
case intro
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
⊢ Multiset.prod f ∣ a
Theorem: factorization'.coprime_of_mem
Proof state before:
case intro
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
⊢ Multiset.prod f ∣ a
Tactic:
cases' h1 with h1 h1 <;> rw [h1]
Proof state after:
case intro.inr
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = -Multiset.prod f
⊢ Multiset.prod f ∣ -Multiset.prod f
Theorem: factorization'.coprime_of_mem
Proof state before:
case intro.inr
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = -Multiset.prod f
⊢ Multiset.prod f ∣ -Multiset.prod f
Tactic:
simp only [dvd_neg]
Proof state after:
case intro.inr
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = -Multiset.prod f
⊢ Multiset.prod (factorization' h) ∣ Multiset.prod (factorization' h)
Theorem: factorization'.coprime_of_mem
Proof state before:
case intro.inr
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = -Multiset.prod f
⊢ Multiset.prod (factorization' h) ∣ Multiset.prod (factorization' h)
Tactic:
rfl
Proof state after:
no goals
Theorem: no_conj
Proof state before:
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hp : ¬IsUnit p
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
⊢ ¬(p ∈ s ∧ star p ∈ s)
Tactic:
contrapose! hp
Proof state after:
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
hp : p ∈ s ∧ star p ∈ s
⊢ IsUnit p
Theorem: no_conj
Proof state before:
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
hp : p ∈ s ∧ star p ∈ s
⊢ IsUnit p
Tactic:
obtain ⟨h1, h2⟩ := hp
Proof state after:
case intro
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
h1 : p ∈ s
h2 : star p ∈ s
⊢ IsUnit p
Theorem: no_conj
Proof state before:
case intro
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
h1 : p ∈ s
h2 : star p ∈ s
⊢ IsUnit p
Tactic:
by_cases him : p.im = 0
Proof state after:
case pos
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
h1 : p ∈ s
h2 : star p ∈ s
him : p.im = 0
⊢ IsUnit p

case neg
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
h1 : p ∈ s
h2 : star p ∈ s
him : ¬p.im = 0
⊢ IsUnit p
Theorem: no_conj
Proof state before:
case pos
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
h1 : p ∈ s
h2 : star p ∈ s
him : p.im = 0
⊢ IsUnit p
Tactic:
obtain ⟨t, rfl⟩ := Multiset.exists_cons_of_mem h1
Proof state after:
case pos.intro
p : ℤ√(-3)
him : p.im = 0
t : Multiset (ℤ√(-3))
hcoprime : IsCoprime (Multiset.prod (p ::ₘ t)).re (Multiset.prod (p ::ₘ t)).im
h1 : p ∈ p ::ₘ t
h2 : star p ∈ p ::ₘ t
⊢ IsUnit p
Theorem: no_conj
Proof state before:
case pos.intro
p : ℤ√(-3)
him : p.im = 0
t : Multiset (ℤ√(-3))
hcoprime : IsCoprime (Multiset.prod (p ::ₘ t)).re (Multiset.prod (p ::ₘ t)).im
h1 : p ∈ p ::ₘ t
h2 : star p ∈ p ::ₘ t
⊢ IsUnit p
Tactic:
rw [Multiset.prod_cons] at hcoprime
Proof state after:
case pos.intro
p : ℤ√(-3)
him : p.im = 0
t : Multiset (ℤ√(-3))
hcoprime : IsCoprime (p * Multiset.prod t).re (p * Multiset.prod t).im
h1 : p ∈ p ::ₘ t
h2 : star p ∈ p ::ₘ t
⊢ IsUnit p
Theorem: no_conj
Proof state before:
case pos.intro
p : ℤ√(-3)
him : p.im = 0
t : Multiset (ℤ√(-3))
hcoprime : IsCoprime (p * Multiset.prod t).re (p * Multiset.prod t).im
h1 : p ∈ p ::ₘ t
h2 : star p ∈ p ::ₘ t
⊢ IsUnit p
Tactic:
simp only [him, add_zero, MulZeroClass.zero_mul, Zsqrtd.mul_im, Zsqrtd.mul_re,
  MulZeroClass.mul_zero] at hcoprime
Proof state after:
case pos.intro
p : ℤ√(-3)
him : p.im = 0
t : Multiset (ℤ√(-3))
h1 : p ∈ p ::ₘ t
h2 : star p ∈ p ::ₘ t
hcoprime : IsCoprime (p.re * (Multiset.prod t).re) (p.re * (Multiset.prod t).im)
⊢ IsUnit p
Theorem: no_conj
Proof state before:
case pos.intro
p : ℤ√(-3)
him : p.im = 0
t : Multiset (ℤ√(-3))
h1 : p ∈ p ::ₘ t
h2 : star p ∈ p ::ₘ t
hcoprime : IsCoprime (p.re * (Multiset.prod t).re) (p.re * (Multiset.prod t).im)
⊢ IsUnit p
Tactic:
rw [Zsqrt3.isUnit_iff]
Proof state after:
case pos.intro
p : ℤ√(-3)
him : p.im = 0
t : Multiset (ℤ√(-3))
h1 : p ∈ p ::ₘ t
h2 : star p ∈ p ::ₘ t
hcoprime : IsCoprime (p.re * (Multiset.prod t).re) (p.re * (Multiset.prod t).im)
⊢ abs p.re = 1 ∧ p.im = 0
Theorem: no_conj
Proof state before:
case pos.intro
p : ℤ√(-3)
him : p.im = 0
t : Multiset (ℤ√(-3))
h1 : p ∈ p ::ₘ t
h2 : star p ∈ p ::ₘ t
hcoprime : IsCoprime (p.re * (Multiset.prod t).re) (p.re * (Multiset.prod t).im)
⊢ abs p.re = 1 ∧ p.im = 0
Tactic:
simp only [him, and_true_iff, eq_self_iff_true]
Proof state after:
case pos.intro
p : ℤ√(-3)
him : p.im = 0
t : Multiset (ℤ√(-3))
h1 : p ∈ p ::ₘ t
h2 : star p ∈ p ::ₘ t
hcoprime : IsCoprime (p.re * (Multiset.prod t).re) (p.re * (Multiset.prod t).im)
⊢ abs p.re = 1
Theorem: no_conj
Proof state before:
case pos.intro
p : ℤ√(-3)
him : p.im = 0
t : Multiset (ℤ√(-3))
h1 : p ∈ p ::ₘ t
h2 : star p ∈ p ::ₘ t
hcoprime : IsCoprime (p.re * (Multiset.prod t).re) (p.re * (Multiset.prod t).im)
⊢ abs p.re = 1
Tactic:
rw [← Int.isUnit_iff_abs_eq]
Proof state after:
case pos.intro
p : ℤ√(-3)
him : p.im = 0
t : Multiset (ℤ√(-3))
h1 : p ∈ p ::ₘ t
h2 : star p ∈ p ::ₘ t
hcoprime : IsCoprime (p.re * (Multiset.prod t).re) (p.re * (Multiset.prod t).im)
⊢ IsUnit p.re
Theorem: no_conj
Proof state before:
case pos.intro
p : ℤ√(-3)
him : p.im = 0
t : Multiset (ℤ√(-3))
h1 : p ∈ p ::ₘ t
h2 : star p ∈ p ::ₘ t
hcoprime : IsCoprime (p.re * (Multiset.prod t).re) (p.re * (Multiset.prod t).im)
⊢ IsUnit p.re
Tactic:
apply IsCoprime.isUnit_of_dvd' hcoprime <;> apply dvd_mul_right
Proof state after:
no goals
Theorem: no_conj
Proof state before:
case neg
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
h1 : p ∈ s
h2 : star p ∈ s
him : ¬p.im = 0
⊢ IsUnit p
Tactic:
have : star p ≠ p := by
  rw [Ne.def, Zsqrtd.ext]
  rintro ⟨-, H⟩
  apply him
  apply eq_zero_of_neg_eq
  simpa using H
Proof state after:
case neg
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
h1 : p ∈ s
h2 : star p ∈ s
him : ¬p.im = 0
this : star p ≠ p
⊢ IsUnit p
Theorem: no_conj
Proof state before:
case neg
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
h1 : p ∈ s
h2 : star p ∈ s
him : ¬p.im = 0
this : star p ≠ p
⊢ IsUnit p
Tactic:
obtain ⟨t1, rfl⟩ := Multiset.exists_cons_of_mem h1
Proof state after:
case neg.intro
p : ℤ√(-3)
him : ¬p.im = 0
this : star p ≠ p
t1 : Multiset (ℤ√(-3))
hcoprime : IsCoprime (Multiset.prod (p ::ₘ t1)).re (Multiset.prod (p ::ₘ t1)).im
h1 : p ∈ p ::ₘ t1
h2 : star p ∈ p ::ₘ t1
⊢ IsUnit p
Theorem: no_conj
Proof state before:
case neg.intro
p : ℤ√(-3)
him : ¬p.im = 0
this : star p ≠ p
t1 : Multiset (ℤ√(-3))
hcoprime : IsCoprime (Multiset.prod (p ::ₘ t1)).re (Multiset.prod (p ::ₘ t1)).im
h1 : p ∈ p ::ₘ t1
h2 : star p ∈ p ::ₘ t1
⊢ IsUnit p
Tactic:
have : star p ∈ t1 := by
  rw [Multiset.mem_cons] at h2
  exact h2.resolve_left this
Proof state after:
case neg.intro
p : ℤ√(-3)
him : ¬p.im = 0
this✝ : star p ≠ p
t1 : Multiset (ℤ√(-3))
hcoprime : IsCoprime (Multiset.prod (p ::ₘ t1)).re (Multiset.prod (p ::ₘ t1)).im
h1 : p ∈ p ::ₘ t1
h2 : star p ∈ p ::ₘ t1
this : star p ∈ t1
⊢ IsUnit p
Theorem: no_conj
Proof state before:
case neg.intro
p : ℤ√(-3)
him : ¬p.im = 0
this✝ : star p ≠ p
t1 : Multiset (ℤ√(-3))
hcoprime : IsCoprime (Multiset.prod (p ::ₘ t1)).re (Multiset.prod (p ::ₘ t1)).im
h1 : p ∈ p ::ₘ t1
h2 : star p ∈ p ::ₘ t1
this : star p ∈ t1
⊢ IsUnit p
Tactic:
obtain ⟨t2, rfl⟩ := Multiset.exists_cons_of_mem this
Proof state after:
case neg.intro.intro
p : ℤ√(-3)
him : ¬p.im = 0
this✝ : star p ≠ p
t2 : Multiset (ℤ√(-3))
hcoprime : IsCoprime (Multiset.prod (p ::ₘ star p ::ₘ t2)).re (Multiset.prod (p ::ₘ star p ::ₘ t2)).im
h1 : p ∈ p ::ₘ star p ::ₘ t2
h2 : star p ∈ p ::ₘ star p ::ₘ t2
this : star p ∈ star p ::ₘ t2
⊢ IsUnit p
Theorem: no_conj
Proof state before:
case neg.intro.intro
p : ℤ√(-3)
him : ¬p.im = 0
this✝ : star p ≠ p
t2 : Multiset (ℤ√(-3))
hcoprime : IsCoprime (Multiset.prod (p ::ₘ star p ::ₘ t2)).re (Multiset.prod (p ::ₘ star p ::ₘ t2)).im
h1 : p ∈ p ::ₘ star p ::ₘ t2
h2 : star p ∈ p ::ₘ star p ::ₘ t2
this : star p ∈ star p ::ₘ t2
⊢ IsUnit p
Tactic:
rw [Multiset.prod_cons, Multiset.prod_cons, ← mul_assoc, ← Zsqrtd.norm_eq_mul_conj] at hcoprime
Proof state after:
case neg.intro.intro
p : ℤ√(-3)
him : ¬p.im = 0
this✝ : star p ≠ p
t2 : Multiset (ℤ√(-3))
hcoprime : IsCoprime (↑(Zsqrtd.norm p) * Multiset.prod t2).re (↑(Zsqrtd.norm p) * Multiset.prod t2).im
h1 : p ∈ p ::ₘ star p ::ₘ t2
h2 : star p ∈ p ::ₘ star p ::ₘ t2
this : star p ∈ star p ::ₘ t2
⊢ IsUnit p
Theorem: no_conj
Proof state before:
case neg.intro.intro
p : ℤ√(-3)
him : ¬p.im = 0
this✝ : star p ≠ p
t2 : Multiset (ℤ√(-3))
hcoprime : IsCoprime (↑(Zsqrtd.norm p) * Multiset.prod t2).re (↑(Zsqrtd.norm p) * Multiset.prod t2).im
h1 : p ∈ p ::ₘ star p ::ₘ t2
h2 : star p ∈ p ::ₘ star p ::ₘ t2
this : star p ∈ star p ::ₘ t2
⊢ IsUnit p
Tactic:
rw [Zsqrtd.isUnit_iff_norm_isUnit]
Proof state after:
case neg.intro.intro
p : ℤ√(-3)
him : ¬p.im = 0
this✝ : star p ≠ p
t2 : Multiset (ℤ√(-3))
hcoprime : IsCoprime (↑(Zsqrtd.norm p) * Multiset.prod t2).re (↑(Zsqrtd.norm p) * Multiset.prod t2).im
h1 : p ∈ p ::ₘ star p ::ₘ t2
h2 : star p ∈ p ::ₘ star p ::ₘ t2
this : star p ∈ star p ::ₘ t2
⊢ IsUnit (Zsqrtd.norm p)
Theorem: no_conj
Proof state before:
case neg.intro.intro
p : ℤ√(-3)
him : ¬p.im = 0
this✝ : star p ≠ p
t2 : Multiset (ℤ√(-3))
hcoprime : IsCoprime (↑(Zsqrtd.norm p) * Multiset.prod t2).re (↑(Zsqrtd.norm p) * Multiset.prod t2).im
h1 : p ∈ p ::ₘ star p ::ₘ t2
h2 : star p ∈ p ::ₘ star p ::ₘ t2
this : star p ∈ star p ::ₘ t2
⊢ IsUnit (Zsqrtd.norm p)
Tactic:
apply IsCoprime.isUnit_of_dvd' hcoprime <;>
  simp only [add_zero, Zsqrtd.coe_int_re, MulZeroClass.zero_mul, dvd_mul_right, Zsqrtd.mul_re,
    MulZeroClass.mul_zero, Zsqrtd.mul_im, Zsqrtd.coe_int_im]
Proof state after:
no goals
Theorem: no_conj
Proof state before:
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
h1 : p ∈ s
h2 : star p ∈ s
him : ¬p.im = 0
⊢ star p ≠ p
Tactic:
rw [Ne.def, Zsqrtd.ext]
Proof state after:
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
h1 : p ∈ s
h2 : star p ∈ s
him : ¬p.im = 0
⊢ ¬((star p).re = p.re ∧ (star p).im = p.im)
Theorem: no_conj
Proof state before:
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
h1 : p ∈ s
h2 : star p ∈ s
him : ¬p.im = 0
⊢ ¬((star p).re = p.re ∧ (star p).im = p.im)
Tactic:
rintro ⟨-, H⟩
Proof state after:
case intro
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
h1 : p ∈ s
h2 : star p ∈ s
him : ¬p.im = 0
H : (star p).im = p.im
⊢ False
Theorem: no_conj
Proof state before:
case intro
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
h1 : p ∈ s
h2 : star p ∈ s
him : ¬p.im = 0
H : (star p).im = p.im
⊢ False
Tactic:
apply him
Proof state after:
case intro
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
h1 : p ∈ s
h2 : star p ∈ s
him : ¬p.im = 0
H : (star p).im = p.im
⊢ p.im = 0
Theorem: no_conj
Proof state before:
case intro
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
h1 : p ∈ s
h2 : star p ∈ s
him : ¬p.im = 0
H : (star p).im = p.im
⊢ p.im = 0
Tactic:
apply eq_zero_of_neg_eq
Proof state after:
case intro.h
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
h1 : p ∈ s
h2 : star p ∈ s
him : ¬p.im = 0
H : (star p).im = p.im
⊢ -p.im = p.im
Theorem: no_conj
Proof state before:
case intro.h
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
h1 : p ∈ s
h2 : star p ∈ s
him : ¬p.im = 0
H : (star p).im = p.im
⊢ -p.im = p.im
Tactic:
simpa using H
Proof state after:
no goals
Theorem: no_conj
Proof state before:
p : ℤ√(-3)
him : ¬p.im = 0
this : star p ≠ p
t1 : Multiset (ℤ√(-3))
hcoprime : IsCoprime (Multiset.prod (p ::ₘ t1)).re (Multiset.prod (p ::ₘ t1)).im
h1 : p ∈ p ::ₘ t1
h2 : star p ∈ p ::ₘ t1
⊢ star p ∈ t1
Tactic:
rw [Multiset.mem_cons] at h2
Proof state after:
p : ℤ√(-3)
him : ¬p.im = 0
this : star p ≠ p
t1 : Multiset (ℤ√(-3))
hcoprime : IsCoprime (Multiset.prod (p ::ₘ t1)).re (Multiset.prod (p ::ₘ t1)).im
h1 : p ∈ p ::ₘ t1
h2 : star p = p ∨ star p ∈ t1
⊢ star p ∈ t1
Theorem: no_conj
Proof state before:
p : ℤ√(-3)
him : ¬p.im = 0
this : star p ≠ p
t1 : Multiset (ℤ√(-3))
hcoprime : IsCoprime (Multiset.prod (p ::ₘ t1)).re (Multiset.prod (p ::ₘ t1)).im
h1 : p ∈ p ::ₘ t1
h2 : star p = p ∨ star p ∈ t1
⊢ star p ∈ t1
Tactic:
exact h2.resolve_left this
Proof state after:
no goals
Theorem: Associated'.norm_eq
Proof state before:
x y : ℤ√(-3)
h : Associated' x y
⊢ Zsqrtd.norm x = Zsqrtd.norm y
Tactic:
cases' h with h h <;> simp only [Zsqrtd.norm_eq_of_associated (by norm_num) h, Zsqrtd.norm_conj]
Proof state after:
no goals
Theorem: associated'_of_abs_eq
Proof state before:
x y : ℤ√(-3)
hre : abs x.re = abs y.re
him : abs x.im = abs y.im
⊢ Associated' x y
Tactic:
rw [abs_eq_abs] at hre him
Proof state after:
x y : ℤ√(-3)
hre : x.re = y.re ∨ x.re = -y.re
him : x.im = y.im ∨ x.im = -y.im
⊢ Associated' x y
Theorem: associated'_of_abs_eq
Proof state before:
x y : ℤ√(-3)
hre : x.re = y.re ∨ x.re = -y.re
him : x.im = y.im ∨ x.im = -y.im
⊢ Associated' x y
Tactic:
cases' hre with h1 h1 <;> cases' him with h2 h2 <;>
  [
    (left; use 1),
    (right; use 1),
    (right; use -1),
    (left; use -1)
  ] <;>
  simp [Zsqrtd.ext, h1, h2]
Proof state after:
no goals
Theorem: associated'_of_abs_eq
Proof state before:
case inl.inl.h
x y : ℤ√(-3)
h1 : x.re = y.re
h2 : x.im = y.im
⊢ Associated x y
Tactic:
use 1
Proof state after:
case inl.inl.h
x y : ℤ√(-3)
h1 : x.re = y.re
h2 : x.im = y.im
⊢ x * ↑1 = y
Theorem: associated'_of_abs_eq
Proof state before:
case inl.inr.h
x y : ℤ√(-3)
h1 : x.re = y.re
h2 : x.im = -y.im
⊢ Associated x (star y)
Tactic:
use 1
Proof state after:
case inl.inr.h
x y : ℤ√(-3)
h1 : x.re = y.re
h2 : x.im = -y.im
⊢ x * ↑1 = star y
Theorem: associated'_of_abs_eq
Proof state before:
case inr.inl.h
x y : ℤ√(-3)
h1 : x.re = -y.re
h2 : x.im = y.im
⊢ Associated x (star y)
Tactic:
use -1
Proof state after:
case inr.inl.h
x y : ℤ√(-3)
h1 : x.re = -y.re
h2 : x.im = y.im
⊢ x * ↑(-1) = star y
Theorem: associated'_of_abs_eq
Proof state before:
case inr.inr.h
x y : ℤ√(-3)
h1 : x.re = -y.re
h2 : x.im = -y.im
⊢ Associated x y
Tactic:
use -1
Proof state after:
case inr.inr.h
x y : ℤ√(-3)
h1 : x.re = -y.re
h2 : x.im = -y.im
⊢ x * ↑(-1) = y
Theorem: associated'_of_associated_norm
Proof state before:
x y : ℤ√(-3)
h : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)
hx : IsCoprime x.re x.im
hy : IsCoprime y.re y.im
h' : OddPrimeOrFour (Zsqrtd.norm x)
⊢ Associated' x y
Tactic:
have heq : x.norm = y.norm :=
  haveI hd : (-3 : ℤ) ≤ 0 := by norm_num
  Int.eq_of_associated_of_nonneg h (Zsqrtd.norm_nonneg hd _) (Zsqrtd.norm_nonneg hd _)
Proof state after:
x y : ℤ√(-3)
h : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)
hx : IsCoprime x.re x.im
hy : IsCoprime y.re y.im
h' : OddPrimeOrFour (Zsqrtd.norm x)
heq : Zsqrtd.norm x = Zsqrtd.norm y
⊢ Associated' x y
Theorem: associated'_of_associated_norm
Proof state before:
x y : ℤ√(-3)
h : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)
hx : IsCoprime x.re x.im
hy : IsCoprime y.re y.im
h' : OddPrimeOrFour (Zsqrtd.norm x)
heq : Zsqrtd.norm x = Zsqrtd.norm y
⊢ Associated' x y
Tactic:
obtain ⟨hre, him⟩ := step4_3 hx hy h' heq
Proof state after:
case intro
x y : ℤ√(-3)
h : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)
hx : IsCoprime x.re x.im
hy : IsCoprime y.re y.im
h' : OddPrimeOrFour (Zsqrtd.norm x)
heq : Zsqrtd.norm x = Zsqrtd.norm y
hre : abs x.re = abs y.re
him : abs x.im = abs y.im
⊢ Associated' x y
Theorem: associated'_of_associated_norm
Proof state before:
case intro
x y : ℤ√(-3)
h : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)
hx : IsCoprime x.re x.im
hy : IsCoprime y.re y.im
h' : OddPrimeOrFour (Zsqrtd.norm x)
heq : Zsqrtd.norm x = Zsqrtd.norm y
hre : abs x.re = abs y.re
him : abs x.im = abs y.im
⊢ Associated' x y
Tactic:
exact associated'_of_abs_eq hre him
Proof state after:
no goals
Theorem: associated'_of_associated_norm
Proof state before:
x y : ℤ√(-3)
h : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)
hx : IsCoprime x.re x.im
hy : IsCoprime y.re y.im
h' : OddPrimeOrFour (Zsqrtd.norm x)
⊢ -3 ≤ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: factorization'.associated'_of_norm_eq
Proof state before:
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Zsqrtd.norm b = Zsqrtd.norm c
⊢ Associated' b c
Tactic:
apply associated'_of_associated_norm
Proof state after:
case h
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Zsqrtd.norm b = Zsqrtd.norm c
⊢ Associated (Zsqrtd.norm b) (Zsqrtd.norm c)

case hx
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Zsqrtd.norm b = Zsqrtd.norm c
⊢ IsCoprime b.re b.im

case hy
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Zsqrtd.norm b = Zsqrtd.norm c
⊢ IsCoprime c.re c.im

case h'
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Zsqrtd.norm b = Zsqrtd.norm c
⊢ OddPrimeOrFour (Zsqrtd.norm b)
Theorem: factorization'.associated'_of_norm_eq
Proof state before:
case h
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Zsqrtd.norm b = Zsqrtd.norm c
⊢ Associated (Zsqrtd.norm b) (Zsqrtd.norm c)
Tactic:
rw [hnorm]
Proof state after:
no goals
Theorem: factorization'.associated'_of_norm_eq
Proof state before:
case hx
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Zsqrtd.norm b = Zsqrtd.norm c
⊢ IsCoprime b.re b.im
Tactic:
exact factorization'.coprime_of_mem h hbmem
Proof state after:
no goals
Theorem: factorization'.associated'_of_norm_eq
Proof state before:
case hy
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Zsqrtd.norm b = Zsqrtd.norm c
⊢ IsCoprime c.re c.im
Tactic:
exact factorization'.coprime_of_mem h hcmem
Proof state after:
no goals
Theorem: factorization'.associated'_of_norm_eq
Proof state before:
case h'
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Zsqrtd.norm b = Zsqrtd.norm c
⊢ OddPrimeOrFour (Zsqrtd.norm b)
Tactic:
exact ((factorization'_prop h).2 b hbmem).2.2
Proof state after:
no goals
Theorem: factors_unique
Proof state before:
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hf' : ∀ (x : ℤ√(-3)), x ∈ f → IsCoprime x.re x.im
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hg' : ∀ (x : ℤ√(-3)), x ∈ g → IsCoprime x.re x.im
h : Associated (Multiset.prod f) (Multiset.prod g)
p : ∀ (x : ℤ√(-3)), x ∈ f → ∀ (y : ℤ√(-3)), y ∈ g → Associated (Zsqrtd.norm x) (Zsqrtd.norm y) → Associated' x y
⊢ Multiset.Rel Associated' f g
Tactic:
refine' Multiset.Rel.mono _ p
Proof state after:
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hf' : ∀ (x : ℤ√(-3)), x ∈ f → IsCoprime x.re x.im
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hg' : ∀ (x : ℤ√(-3)), x ∈ g → IsCoprime x.re x.im
h : Associated (Multiset.prod f) (Multiset.prod g)
p : ∀ (x : ℤ√(-3)), x ∈ f → ∀ (y : ℤ√(-3)), y ∈ g → Associated (Zsqrtd.norm x) (Zsqrtd.norm y) → Associated' x y
⊢ Multiset.Rel (fun a b => Associated (Zsqrtd.norm a) (Zsqrtd.norm b)) f g
Theorem: factors_unique
Proof state before:
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hf' : ∀ (x : ℤ√(-3)), x ∈ f → IsCoprime x.re x.im
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hg' : ∀ (x : ℤ√(-3)), x ∈ g → IsCoprime x.re x.im
h : Associated (Multiset.prod f) (Multiset.prod g)
p : ∀ (x : ℤ√(-3)), x ∈ f → ∀ (y : ℤ√(-3)), y ∈ g → Associated (Zsqrtd.norm x) (Zsqrtd.norm y) → Associated' x y
⊢ Multiset.Rel (fun a b => Associated (Zsqrtd.norm a) (Zsqrtd.norm b)) f g
Tactic:
rw [← Multiset.rel_map]
Proof state after:
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hf' : ∀ (x : ℤ√(-3)), x ∈ f → IsCoprime x.re x.im
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hg' : ∀ (x : ℤ√(-3)), x ∈ g → IsCoprime x.re x.im
h : Associated (Multiset.prod f) (Multiset.prod g)
p : ∀ (x : ℤ√(-3)), x ∈ f → ∀ (y : ℤ√(-3)), y ∈ g → Associated (Zsqrtd.norm x) (Zsqrtd.norm y) → Associated' x y
⊢ Multiset.Rel Associated (Multiset.map (fun a => Zsqrtd.norm a) f) (Multiset.map (fun b => Zsqrtd.norm b) g)
Theorem: factors_unique
Proof state before:
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hf' : ∀ (x : ℤ√(-3)), x ∈ f → IsCoprime x.re x.im
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hg' : ∀ (x : ℤ√(-3)), x ∈ g → IsCoprime x.re x.im
h : Associated (Multiset.prod f) (Multiset.prod g)
p : ∀ (x : ℤ√(-3)), x ∈ f → ∀ (y : ℤ√(-3)), y ∈ g → Associated (Zsqrtd.norm x) (Zsqrtd.norm y) → Associated' x y
⊢ Multiset.Rel Associated (Multiset.map (fun a => Zsqrtd.norm a) f) (Multiset.map (fun b => Zsqrtd.norm b) g)
Tactic:
apply factors_unique_prod hf hg
Proof state after:
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hf' : ∀ (x : ℤ√(-3)), x ∈ f → IsCoprime x.re x.im
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hg' : ∀ (x : ℤ√(-3)), x ∈ g → IsCoprime x.re x.im
h : Associated (Multiset.prod f) (Multiset.prod g)
p : ∀ (x : ℤ√(-3)), x ∈ f → ∀ (y : ℤ√(-3)), y ∈ g → Associated (Zsqrtd.norm x) (Zsqrtd.norm y) → Associated' x y
⊢ Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))