internlm/Lean-Github huggingface dataset:
Theorem: factors_unique_prod
Proof state before:
⊢ ∀ {f g : Multiset (ℤ√(-3))},
    (∀ x ∈ f, OddPrimeOrFour x.norm.natAbs) →
      (∀ x ∈ g, OddPrimeOrFour x.norm.natAbs) →
        Associated f.prod.norm g.prod.norm →
          Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f = Multiset.map (Int.natAbs ∘ Zsqrtd.norm) g
Tactic:
intro f g hf hg hassoc
Proof state after:
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
⊢ Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f = Multiset.map (Int.natAbs ∘ Zsqrtd.norm) g
Theorem: factors_unique_prod
Proof state before:
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
⊢ Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f = Multiset.map (Int.natAbs ∘ Zsqrtd.norm) g
Tactic:
refine factors_unique_prod' ?_ ?_ ?_
Proof state after:
case refine_1
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
⊢ ∀ x ∈ Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f, OddPrimeOrFour x

case refine_2
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
⊢ ∀ x ∈ Multiset.map (Int.natAbs ∘ Zsqrtd.norm) g, OddPrimeOrFour x

case refine_3
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
⊢ (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f).prod = (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) g).prod
Theorem: factors_unique_prod
Proof state before:
case refine_1
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
⊢ ∀ x ∈ Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f, OddPrimeOrFour x
Tactic:
intro x hx
Proof state after:
case refine_1
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
x : ℕ
hx : x ∈ Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f
⊢ OddPrimeOrFour x
Theorem: factors_unique_prod
Proof state before:
case refine_1
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
x : ℕ
hx : x ∈ Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f
⊢ OddPrimeOrFour x
Tactic:
rw [Multiset.mem_map] at hx
Proof state after:
case refine_1
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
x : ℕ
hx : ∃ a ∈ f, (Int.natAbs ∘ Zsqrtd.norm) a = x
⊢ OddPrimeOrFour x
Theorem: factors_unique_prod
Proof state before:
case refine_1
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
x : ℕ
hx : ∃ a ∈ f, (Int.natAbs ∘ Zsqrtd.norm) a = x
⊢ OddPrimeOrFour x
Tactic:
obtain ⟨y, hy, rfl⟩ := hx
Proof state after:
case refine_1.intro.intro
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
y : ℤ√(-3)
hy : y ∈ f
⊢ OddPrimeOrFour ((Int.natAbs ∘ Zsqrtd.norm) y)
Theorem: factors_unique_prod
Proof state before:
case refine_1.intro.intro
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
y : ℤ√(-3)
hy : y ∈ f
⊢ OddPrimeOrFour ((Int.natAbs ∘ Zsqrtd.norm) y)
Tactic:
exact hf y hy
Proof state after:
no goals
Theorem: factors_unique_prod
Proof state before:
case refine_2
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
⊢ ∀ x ∈ Multiset.map (Int.natAbs ∘ Zsqrtd.norm) g, OddPrimeOrFour x
Tactic:
intro x hx
Proof state after:
case refine_2
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
x : ℕ
hx : x ∈ Multiset.map (Int.natAbs ∘ Zsqrtd.norm) g
⊢ OddPrimeOrFour x
Theorem: factors_unique_prod
Proof state before:
case refine_2
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
x : ℕ
hx : x ∈ Multiset.map (Int.natAbs ∘ Zsqrtd.norm) g
⊢ OddPrimeOrFour x
Tactic:
rw [Multiset.mem_map] at hx
Proof state after:
case refine_2
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
x : ℕ
hx : ∃ a ∈ g, (Int.natAbs ∘ Zsqrtd.norm) a = x
⊢ OddPrimeOrFour x
Theorem: factors_unique_prod
Proof state before:
case refine_2
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
x : ℕ
hx : ∃ a ∈ g, (Int.natAbs ∘ Zsqrtd.norm) a = x
⊢ OddPrimeOrFour x
Tactic:
obtain ⟨y, hy, rfl⟩ := hx
Proof state after:
case refine_2.intro.intro
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
y : ℤ√(-3)
hy : y ∈ g
⊢ OddPrimeOrFour ((Int.natAbs ∘ Zsqrtd.norm) y)
Theorem: factors_unique_prod
Proof state before:
case refine_2.intro.intro
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
y : ℤ√(-3)
hy : y ∈ g
⊢ OddPrimeOrFour ((Int.natAbs ∘ Zsqrtd.norm) y)
Tactic:
exact hg y hy
Proof state after:
no goals
Theorem: factors_unique_prod
Proof state before:
case refine_3
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
⊢ (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f).prod = (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) g).prod
Tactic:
simp_rw [← Multiset.map_map, prod_map_natAbs, prod_map_norm, ← Int.associated_iff_natAbs]
Proof state after:
case refine_3
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
⊢ Associated f.prod.norm g.prod.norm
Theorem: factors_unique_prod
Proof state before:
case refine_3
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
⊢ Associated f.prod.norm g.prod.norm
Tactic:
exact hassoc
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 = (factorization' h).prod ∨ a = -(factorization' h).prod
⊢ 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 = (factorization' h).prod ∨ a = -(factorization' h).prod
⊢ 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 = f.prod ∨ a = -f.prod
⊢ 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 = f.prod ∨ a = -f.prod
⊢ 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 = f.prod ∨ a = -f.prod
⊢ 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 = f.prod ∨ a = -f.prod
⊢ 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 = f.prod ∨ a = -f.prod
⊢ f.prod ∣ 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 = f.prod ∨ a = -f.prod
⊢ f.prod ∣ 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 = -f.prod
⊢ f.prod ∣ -f.prod
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 = -f.prod
⊢ f.prod ∣ -f.prod
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 = -f.prod
⊢ f.prod ∣ f.prod
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 = -f.prod
⊢ f.prod ∣ f.prod
Tactic:
rfl
Proof state after:
no goals
Theorem: no_conj
Proof state before:
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hp : ¬IsUnit p
hcoprime : IsCoprime s.prod.re s.prod.im
⊢ ¬(p ∈ s ∧ star p ∈ s)
Tactic:
contrapose! hp
Proof state after:
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime s.prod.re s.prod.im
hp : p ∈ s ∧ star p ∈ s
⊢ IsUnit p
Theorem: no_conj
Proof state before:
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime s.prod.re s.prod.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 s.prod.re s.prod.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 s.prod.re s.prod.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 s.prod.re s.prod.im
h1 : p ∈ s
h2 : star p ∈ s
him : p.im = 0
⊢ IsUnit p

case neg
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime s.prod.re s.prod.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 s.prod.re s.prod.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 (p ::ₘ t).prod.re (p ::ₘ t).prod.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 ::ₘ t).prod.re (p ::ₘ t).prod.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 * t.prod).re (p * t.prod).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 * t.prod).re (p * t.prod).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 * t.prod.re) (p.re * t.prod.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 * t.prod.re) (p.re * t.prod.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 * t.prod.re) (p.re * t.prod.im)
⊢ |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 * t.prod.re) (p.re * t.prod.im)
⊢ |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 * t.prod.re) (p.re * t.prod.im)
⊢ |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 * t.prod.re) (p.re * t.prod.im)
⊢ |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 * t.prod.re) (p.re * t.prod.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 * t.prod.re) (p.re * t.prod.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 s.prod.re s.prod.im
h1 : p ∈ s
h2 : star p ∈ s
him : ¬p.im = 0
⊢ IsUnit p
Tactic:
have : star p ≠ p := by
  rw [Ne, Zsqrtd.ext_iff]
  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 s.prod.re s.prod.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 s.prod.re s.prod.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 (p ::ₘ t1).prod.re (p ::ₘ t1).prod.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 (p ::ₘ t1).prod.re (p ::ₘ t1).prod.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 (p ::ₘ t1).prod.re (p ::ₘ t1).prod.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 (p ::ₘ t1).prod.re (p ::ₘ t1).prod.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 (p ::ₘ star p ::ₘ t2).prod.re (p ::ₘ star p ::ₘ t2).prod.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 (p ::ₘ star p ::ₘ t2).prod.re (p ::ₘ star p ::ₘ t2).prod.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 (↑p.norm * t2.prod).re (↑p.norm * t2.prod).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 (↑p.norm * t2.prod).re (↑p.norm * t2.prod).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 (↑p.norm * t2.prod).re (↑p.norm * t2.prod).im
h1 : p ∈ p ::ₘ star p ::ₘ t2
h2 : star p ∈ p ::ₘ star p ::ₘ t2
this : star p ∈ star p ::ₘ t2
⊢ IsUnit p.norm
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 (↑p.norm * t2.prod).re (↑p.norm * t2.prod).im
h1 : p ∈ p ::ₘ star p ::ₘ t2
h2 : star p ∈ p ::ₘ star p ::ₘ t2
this : star p ∈ star p ::ₘ t2
⊢ IsUnit p.norm
Tactic:
apply IsCoprime.isUnit_of_dvd' hcoprime <;>
  simp only [add_zero, Zsqrtd.intCast_re, MulZeroClass.zero_mul, dvd_mul_right, Zsqrtd.mul_re,
    MulZeroClass.mul_zero, Zsqrtd.mul_im, Zsqrtd.intCast_im]
Proof state after:
no goals
Theorem: no_conj
Proof state before:
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime s.prod.re s.prod.im
h1 : p ∈ s
h2 : star p ∈ s
him : ¬p.im = 0
⊢ star p ≠ p
Tactic:
rw [Ne, Zsqrtd.ext_iff]
Proof state after:
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime s.prod.re s.prod.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 s.prod.re s.prod.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 s.prod.re s.prod.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 s.prod.re s.prod.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 s.prod.re s.prod.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 s.prod.re s.prod.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 s.prod.re s.prod.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 s.prod.re s.prod.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 (p ::ₘ t1).prod.re (p ::ₘ t1).prod.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 (p ::ₘ t1).prod.re (p ::ₘ t1).prod.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 (p ::ₘ t1).prod.re (p ::ₘ t1).prod.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'.refl
Proof state before:
x : ℤ√(-3)
⊢ Associated x x
Tactic:
rfl
Proof state after:
no goals
Theorem: Associated'.norm_eq
Proof state before:
x y : ℤ√(-3)
h : Associated' x y
⊢ x.norm = y.norm
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'.norm_eq
Proof state before:
x y : ℤ√(-3)
h : Associated x (star y)
⊢ -3 ≤ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: associated'_of_abs_eq
Proof state before:
x y : ℤ√(-3)
hre : |x.re| = |y.re|
him : |x.im| = |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_iff, h1, h2]
Proof state after:
no goals
Theorem: associated'_of_abs_eq
Proof state before:
case inl.inl
x y : ℤ√(-3)
h1 : x.re = y.re
h2 : x.im = y.im
⊢ Associated' x y
Tactic:
left
Proof state after:
case inl.inl.h
x y : ℤ√(-3)
h1 : x.re = y.re
h2 : x.im = y.im
⊢ Associated x y
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 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
x y : ℤ√(-3)
h1 : x.re = y.re
h2 : x.im = -y.im
⊢ Associated' x y
Tactic:
right
Proof state after:
case inl.inr.h
x y : ℤ√(-3)
h1 : x.re = y.re
h2 : x.im = -y.im
⊢ Associated x (star 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 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
x y : ℤ√(-3)
h1 : x.re = -y.re
h2 : x.im = y.im
⊢ Associated' x y
Tactic:
right
Proof state after:
case inr.inl.h
x y : ℤ√(-3)
h1 : x.re = -y.re
h2 : x.im = y.im
⊢ Associated x (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 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
x y : ℤ√(-3)
h1 : x.re = -y.re
h2 : x.im = -y.im
⊢ Associated' x y
Tactic:
left
Proof state after:
case inr.inr.h
x y : ℤ√(-3)
h1 : x.re = -y.re
h2 : x.im = -y.im
⊢ Associated x 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 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 x.norm y.norm
hx : IsCoprime x.re x.im
hy : IsCoprime y.re y.im
h' : OddPrimeOrFour x.norm.natAbs
⊢ 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 x.norm y.norm
hx : IsCoprime x.re x.im
hy : IsCoprime y.re y.im
h' : OddPrimeOrFour x.norm.natAbs
heq : x.norm = y.norm
⊢ Associated' x y
Theorem: associated'_of_associated_norm
Proof state before:
x y : ℤ√(-3)
h : Associated x.norm y.norm
hx : IsCoprime x.re x.im
hy : IsCoprime y.re y.im
h' : OddPrimeOrFour x.norm.natAbs
heq : x.norm = y.norm
⊢ Associated' x y
Tactic:
obtain ⟨hre, him⟩ := step4_3 hx hy h' heq
Proof state after:
case intro
x y : ℤ√(-3)
h : Associated x.norm y.norm
hx : IsCoprime x.re x.im
hy : IsCoprime y.re y.im
h' : OddPrimeOrFour x.norm.natAbs
heq : x.norm = y.norm
hre : |x.re| = |y.re|
him : |x.im| = |y.im|
⊢ Associated' x y