Theorem: no_conj (FltRegular/FltThree/Edwards.lean)

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
State after:
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime s.prod.re s.prod.im
hp : p ∈ s ∧ star p ∈ s
⊢ IsUnit p

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
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

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
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

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
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

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
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

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
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

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]
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

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]
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

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]
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

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
State after:
no goals

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
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

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
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

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
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

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
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

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
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

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]
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

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]
State after:
no goals

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]
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)

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⟩
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

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
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

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
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

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
State after:
no goals

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
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

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
State after:
no goals