internlm/Lean-Github huggingface dataset:
Theorem: step3
Proof state before:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
n✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = n✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {a : ℤ√(-3)},
        IsCoprime a.re a.im →
          Int.natAbs (Zsqrtd.norm a) = m →
            ∃ f,
              (a = Multiset.prod f ∨ a = -Multiset.prod f) ∧
                ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
h : Zsqrtd.norm a ≠ 1
U q : ℤ√(-3)
hc : 0 ≤ q.re
hd : q.im ≠ 0
hp : OddPrimeOrFour (Zsqrtd.norm q)
huv : a = q * U
huvcoprime : IsCoprime U.re U.im
descent : Int.natAbs (Zsqrtd.norm U) < n
g : Multiset (ℤ√(-3))
hgprod : U = Multiset.prod g ∨ U = -Multiset.prod g
hgfactors : ∀ (pq : ℤ√(-3)), pq ∈ g → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
⊢ ∀ (pq : ℤ√(-3)), pq ∈ q ::ₘ g → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
Tactic:
rintro pq hpq
Proof state after:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
n✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = n✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {a : ℤ√(-3)},
        IsCoprime a.re a.im →
          Int.natAbs (Zsqrtd.norm a) = m →
            ∃ f,
              (a = Multiset.prod f ∨ a = -Multiset.prod f) ∧
                ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
h : Zsqrtd.norm a ≠ 1
U q : ℤ√(-3)
hc : 0 ≤ q.re
hd : q.im ≠ 0
hp : OddPrimeOrFour (Zsqrtd.norm q)
huv : a = q * U
huvcoprime : IsCoprime U.re U.im
descent : Int.natAbs (Zsqrtd.norm U) < n
g : Multiset (ℤ√(-3))
hgprod : U = Multiset.prod g ∨ U = -Multiset.prod g
hgfactors : ∀ (pq : ℤ√(-3)), pq ∈ g → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
pq : ℤ√(-3)
hpq : pq ∈ q ::ₘ g
⊢ 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
Theorem: step3
Proof state before:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
n✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = n✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {a : ℤ√(-3)},
        IsCoprime a.re a.im →
          Int.natAbs (Zsqrtd.norm a) = m →
            ∃ f,
              (a = Multiset.prod f ∨ a = -Multiset.prod f) ∧
                ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
h : Zsqrtd.norm a ≠ 1
U q : ℤ√(-3)
hc : 0 ≤ q.re
hd : q.im ≠ 0
hp : OddPrimeOrFour (Zsqrtd.norm q)
huv : a = q * U
huvcoprime : IsCoprime U.re U.im
descent : Int.natAbs (Zsqrtd.norm U) < n
g : Multiset (ℤ√(-3))
hgprod : U = Multiset.prod g ∨ U = -Multiset.prod g
hgfactors : ∀ (pq : ℤ√(-3)), pq ∈ g → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
pq : ℤ√(-3)
hpq : pq ∈ q ::ₘ g
⊢ 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
Tactic:
rw [Multiset.mem_cons] at hpq
Proof state after:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
n✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = n✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {a : ℤ√(-3)},
        IsCoprime a.re a.im →
          Int.natAbs (Zsqrtd.norm a) = m →
            ∃ f,
              (a = Multiset.prod f ∨ a = -Multiset.prod f) ∧
                ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
h : Zsqrtd.norm a ≠ 1
U q : ℤ√(-3)
hc : 0 ≤ q.re
hd : q.im ≠ 0
hp : OddPrimeOrFour (Zsqrtd.norm q)
huv : a = q * U
huvcoprime : IsCoprime U.re U.im
descent : Int.natAbs (Zsqrtd.norm U) < n
g : Multiset (ℤ√(-3))
hgprod : U = Multiset.prod g ∨ U = -Multiset.prod g
hgfactors : ∀ (pq : ℤ√(-3)), pq ∈ g → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
pq : ℤ√(-3)
hpq : pq = q ∨ pq ∈ g
⊢ 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
Theorem: step3
Proof state before:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
n✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = n✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {a : ℤ√(-3)},
        IsCoprime a.re a.im →
          Int.natAbs (Zsqrtd.norm a) = m →
            ∃ f,
              (a = Multiset.prod f ∨ a = -Multiset.prod f) ∧
                ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
h : Zsqrtd.norm a ≠ 1
U q : ℤ√(-3)
hc : 0 ≤ q.re
hd : q.im ≠ 0
hp : OddPrimeOrFour (Zsqrtd.norm q)
huv : a = q * U
huvcoprime : IsCoprime U.re U.im
descent : Int.natAbs (Zsqrtd.norm U) < n
g : Multiset (ℤ√(-3))
hgprod : U = Multiset.prod g ∨ U = -Multiset.prod g
hgfactors : ∀ (pq : ℤ√(-3)), pq ∈ g → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
pq : ℤ√(-3)
hpq : pq = q ∨ pq ∈ g
⊢ 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
Tactic:
obtain rfl | ind := hpq
Proof state after:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.inl
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
n✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = n✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {a : ℤ√(-3)},
        IsCoprime a.re a.im →
          Int.natAbs (Zsqrtd.norm a) = m →
            ∃ f,
              (a = Multiset.prod f ∨ a = -Multiset.prod f) ∧
                ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
h : Zsqrtd.norm a ≠ 1
U : ℤ√(-3)
huvcoprime : IsCoprime U.re U.im
descent : Int.natAbs (Zsqrtd.norm U) < n
g : Multiset (ℤ√(-3))
hgprod : U = Multiset.prod g ∨ U = -Multiset.prod g
hgfactors : ∀ (pq : ℤ√(-3)), pq ∈ g → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
pq : ℤ√(-3)
hc : 0 ≤ pq.re
hd : pq.im ≠ 0
hp : OddPrimeOrFour (Zsqrtd.norm pq)
huv : a = pq * U
⊢ 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)

case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.inr
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
n✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = n✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {a : ℤ√(-3)},
        IsCoprime a.re a.im →
          Int.natAbs (Zsqrtd.norm a) = m →
            ∃ f,
              (a = Multiset.prod f ∨ a = -Multiset.prod f) ∧
                ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
h : Zsqrtd.norm a ≠ 1
U q : ℤ√(-3)
hc : 0 ≤ q.re
hd : q.im ≠ 0
hp : OddPrimeOrFour (Zsqrtd.norm q)
huv : a = q * U
huvcoprime : IsCoprime U.re U.im
descent : Int.natAbs (Zsqrtd.norm U) < n
g : Multiset (ℤ√(-3))
hgprod : U = Multiset.prod g ∨ U = -Multiset.prod g
hgfactors : ∀ (pq : ℤ√(-3)), pq ∈ g → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
pq : ℤ√(-3)
ind : pq ∈ g
⊢ 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
Theorem: step3
Proof state before:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.inl
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
n✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = n✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {a : ℤ√(-3)},
        IsCoprime a.re a.im →
          Int.natAbs (Zsqrtd.norm a) = m →
            ∃ f,
              (a = Multiset.prod f ∨ a = -Multiset.prod f) ∧
                ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
h : Zsqrtd.norm a ≠ 1
U : ℤ√(-3)
huvcoprime : IsCoprime U.re U.im
descent : Int.natAbs (Zsqrtd.norm U) < n
g : Multiset (ℤ√(-3))
hgprod : U = Multiset.prod g ∨ U = -Multiset.prod g
hgfactors : ∀ (pq : ℤ√(-3)), pq ∈ g → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
pq : ℤ√(-3)
hc : 0 ≤ pq.re
hd : pq.im ≠ 0
hp : OddPrimeOrFour (Zsqrtd.norm pq)
huv : a = pq * U
⊢ 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
Tactic:
exact ⟨hc, hd, hp⟩
Proof state after:
no goals
Theorem: step3
Proof state before:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.inr
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
n✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = n✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {a : ℤ√(-3)},
        IsCoprime a.re a.im →
          Int.natAbs (Zsqrtd.norm a) = m →
            ∃ f,
              (a = Multiset.prod f ∨ a = -Multiset.prod f) ∧
                ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
h : Zsqrtd.norm a ≠ 1
U q : ℤ√(-3)
hc : 0 ≤ q.re
hd : q.im ≠ 0
hp : OddPrimeOrFour (Zsqrtd.norm q)
huv : a = q * U
huvcoprime : IsCoprime U.re U.im
descent : Int.natAbs (Zsqrtd.norm U) < n
g : Multiset (ℤ√(-3))
hgprod : U = Multiset.prod g ∨ U = -Multiset.prod g
hgfactors : ∀ (pq : ℤ√(-3)), pq ∈ g → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
pq : ℤ√(-3)
ind : pq ∈ g
⊢ 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
Tactic:
exact hgfactors pq ind
Proof state after:
no goals
Theorem: step4_3
Proof state before:
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im
Tactic:
have hdvd : p'.norm ∣ p.norm := by rw [heq]
Proof state after:
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im
Theorem: step4_3
Proof state before:
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im
Tactic:
have him : p'.im ≠ 0 := by
  apply OddPrimeOrFour.im_ne_zero _ hcoprime'
  rwa [← heq]
Proof state after:
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im
Theorem: step4_3
Proof state before:
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
⊢ Zsqrtd.norm p' ∣ Zsqrtd.norm p
Tactic:
rw [heq]
Proof state after:
no goals
Theorem: step4_3
Proof state before:
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
⊢ p'.im ≠ 0
Tactic:
apply OddPrimeOrFour.im_ne_zero _ hcoprime'
Proof state after:
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
⊢ OddPrimeOrFour (Zsqrtd.norm p')
Theorem: step4_3
Proof state before:
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
⊢ OddPrimeOrFour (Zsqrtd.norm p')
Tactic:
rwa [← heq]
Proof state after:
no goals
Theorem: step4_3
Proof state before:
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
⊢ OddPrimeOrFour (Zsqrtd.norm p')
Tactic:
rwa [← heq]
Proof state after:
no goals
Theorem: step4_3
Proof state before:
case intro.intro.intro.inr
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : Zsqrtd.norm p = Zsqrtd.norm p' * Zsqrtd.norm u
H : p = star p' * u
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im
Tactic:
rw [heq] at h1
Proof state after:
case intro.intro.intro.inr
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : Zsqrtd.norm p' = Zsqrtd.norm p' * Zsqrtd.norm u
H : p = star p' * u
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im
Theorem: step4_3
Proof state before:
case intro.intro.intro.inr
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : Zsqrtd.norm p' = Zsqrtd.norm p' * Zsqrtd.norm u
H : p = star p' * u
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im
Tactic:
have := Int.eq_one_of_mul_eq_self_right (Spts.ne_zero_of_coprime' _ hcoprime') h1.symm
Proof state after:
case intro.intro.intro.inr
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : Zsqrtd.norm p' = Zsqrtd.norm p' * Zsqrtd.norm u
H : p = star p' * u
this : Zsqrtd.norm u = 1
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im
Theorem: step4_3
Proof state before:
case intro.intro.intro.inr
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : Zsqrtd.norm p' = Zsqrtd.norm p' * Zsqrtd.norm u
H : p = star p' * u
this : Zsqrtd.norm u = 1
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im
Tactic:
obtain ⟨ha, hb⟩ := Spts.eq_one this
Proof state after:
case intro.intro.intro.inr.intro
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : Zsqrtd.norm p' = Zsqrtd.norm p' * Zsqrtd.norm u
H : p = star p' * u
this : Zsqrtd.norm u = 1
ha : abs u.re = 1
hb : u.im = 0
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im
Theorem: step4_3
Proof state before:
case intro.intro.intro.inr.intro
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : Zsqrtd.norm p' = Zsqrtd.norm p' * Zsqrtd.norm u
H : p = star p' * u
this : Zsqrtd.norm u = 1
ha : abs u.re = 1
hb : u.im = 0
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im
Tactic:
simp only [hb, Zsqrtd.ext, Zsqrtd.mul_re, Zsqrtd.mul_im, add_zero, zero_add,
  MulZeroClass.mul_zero] at H
Proof state after:
case intro.intro.intro.inr.intro
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : Zsqrtd.norm p' = Zsqrtd.norm p' * Zsqrtd.norm u
this : Zsqrtd.norm u = 1
ha : abs u.re = 1
hb : u.im = 0
H : p.re = (star p').re * u.re ∧ p.im = (star p').im * u.re
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im
Theorem: step4_3
Proof state before:
case intro.intro.intro.inr.intro
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : Zsqrtd.norm p' = Zsqrtd.norm p' * Zsqrtd.norm u
this : Zsqrtd.norm u = 1
ha : abs u.re = 1
hb : u.im = 0
H : p.re = (star p').re * u.re ∧ p.im = (star p').im * u.re
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im
Tactic:
rw [H.1, H.2, abs_mul, abs_mul, ha, mul_one, mul_one]
Proof state after:
case intro.intro.intro.inr.intro
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : Zsqrtd.norm p' = Zsqrtd.norm p' * Zsqrtd.norm u
this : Zsqrtd.norm u = 1
ha : abs u.re = 1
hb : u.im = 0
H : p.re = (star p').re * u.re ∧ p.im = (star p').im * u.re
⊢ abs (star p').re = abs p'.re ∧ abs (star p').im = abs p'.im
Theorem: step4_3
Proof state before:
case intro.intro.intro.inr.intro
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : Zsqrtd.norm p' = Zsqrtd.norm p' * Zsqrtd.norm u
this : Zsqrtd.norm u = 1
ha : abs u.re = 1
hb : u.im = 0
H : p.re = (star p').re * u.re ∧ p.im = (star p').im * u.re
⊢ abs (star p').re = abs p'.re ∧ abs (star p').im = abs p'.im
Tactic:
simp
Proof state after:
no goals
Theorem: factors_unique_prod
Proof state before:
⊢ ∀ {f g : Multiset (ℤ√(-3))},
    (∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)) →
      (∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)) →
        Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g)) →
          Multiset.Rel Associated (Multiset.map Zsqrtd.norm f) (Multiset.map Zsqrtd.norm g)
Tactic:
intro f g hf hg hassoc
Proof state after:
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))
⊢ Multiset.Rel Associated (Multiset.map Zsqrtd.norm f) (Multiset.map Zsqrtd.norm g)
Theorem: factors_unique_prod
Proof state before:
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))
⊢ Multiset.Rel Associated (Multiset.map Zsqrtd.norm f) (Multiset.map Zsqrtd.norm g)
Tactic:
apply factors_unique_prod'
Proof state after:
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))
⊢ ∀ (x : ℤ), x ∈ Multiset.map Zsqrtd.norm f → OddPrimeOrFour x

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))
⊢ ∀ (x : ℤ), x ∈ Multiset.map Zsqrtd.norm g → OddPrimeOrFour x

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))
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))
⊢ ∀ (x : ℤ), x ∈ Multiset.map Zsqrtd.norm f → OddPrimeOrFour x
Tactic:
intro x hx
Proof state after:
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))
x : ℤ
hx : x ∈ Multiset.map Zsqrtd.norm f
⊢ OddPrimeOrFour x
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))
x : ℤ
hx : x ∈ Multiset.map Zsqrtd.norm f
⊢ OddPrimeOrFour x
Tactic:
rw [Multiset.mem_map] at hx
Proof state after:
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))
x : ℤ
hx : ∃ a, a ∈ f ∧ Zsqrtd.norm a = x
⊢ OddPrimeOrFour x
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))
x : ℤ
hx : ∃ a, a ∈ f ∧ Zsqrtd.norm a = x
⊢ OddPrimeOrFour x
Tactic:
obtain ⟨y, hy, rfl⟩ := hx
Proof state after:
case a.intro.intro
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))
y : ℤ√(-3)
hy : y ∈ f
⊢ OddPrimeOrFour (Zsqrtd.norm y)
Theorem: factors_unique_prod
Proof state before:
case a.intro.intro
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))
y : ℤ√(-3)
hy : y ∈ f
⊢ OddPrimeOrFour (Zsqrtd.norm y)
Tactic:
exact hf y hy
Proof state after:
no goals
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))
⊢ ∀ (x : ℤ), x ∈ Multiset.map Zsqrtd.norm g → OddPrimeOrFour x
Tactic:
intro x hx
Proof state after:
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))
x : ℤ
hx : x ∈ Multiset.map Zsqrtd.norm g
⊢ OddPrimeOrFour x
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))
x : ℤ
hx : x ∈ Multiset.map Zsqrtd.norm g
⊢ OddPrimeOrFour x
Tactic:
rw [Multiset.mem_map] at hx
Proof state after:
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))
x : ℤ
hx : ∃ a, a ∈ g ∧ Zsqrtd.norm a = x
⊢ OddPrimeOrFour x
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))
x : ℤ
hx : ∃ a, a ∈ g ∧ Zsqrtd.norm a = x
⊢ OddPrimeOrFour x
Tactic:
obtain ⟨y, hy, rfl⟩ := hx
Proof state after:
case a.intro.intro
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))
y : ℤ√(-3)
hy : y ∈ g
⊢ OddPrimeOrFour (Zsqrtd.norm y)
Theorem: factors_unique_prod
Proof state before:
case a.intro.intro
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))
y : ℤ√(-3)
hy : y ∈ g
⊢ OddPrimeOrFour (Zsqrtd.norm y)
Tactic:
exact hg y hy
Proof state after:
no goals