internlm/Lean-Github huggingface dataset:
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
⊢ Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))
Tactic:
exact Zsqrtd.associated_norm_of_associated h
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)
⊢ ∀ (x : ℤ√(-3)), x ∈ f → ∀ (y : ℤ√(-3)), y ∈ g → Associated (Zsqrtd.norm x) (Zsqrtd.norm y) → Associated' x y
Tactic:
intro x hx y hy hxy
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)
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)
⊢ Associated' x y
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)
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)
⊢ Associated' x y
Tactic:
apply associated'_of_associated_norm hxy
Proof state after:
case hx
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)
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)
⊢ IsCoprime x.re x.im

case hy
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)
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)
⊢ IsCoprime y.re y.im

case h'
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)
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)
⊢ OddPrimeOrFour (Zsqrtd.norm x)
Theorem: factors_unique
Proof state before:
case hx
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)
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)
⊢ IsCoprime x.re x.im
Tactic:
exact hf' x hx
Proof state after:
no goals
Theorem: factors_unique
Proof state before:
case hy
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)
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)
⊢ IsCoprime y.re y.im
Tactic:
exact hg' y hy
Proof state after:
no goals
Theorem: factors_unique
Proof state before:
case h'
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)
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)
⊢ OddPrimeOrFour (Zsqrtd.norm x)
Tactic:
exact hf x hx
Proof state after:
no goals
Theorem: factors_2_even'
Proof state before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ Even (evenFactorExp (Zsqrtd.norm a))
Tactic:
induction' hn : a.norm.natAbs using Nat.strong_induction_on with n ih generalizing a
Proof state after:
case h
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
⊢ Even (evenFactorExp (Zsqrtd.norm a))
Theorem: factors_2_even'
Proof state before:
case h
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
⊢ Even (evenFactorExp (Zsqrtd.norm a))
Tactic:
by_cases hparity : Even a.norm
Proof state after:
case pos
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hparity : Even (Zsqrtd.norm a)
⊢ Even (evenFactorExp (Zsqrtd.norm a))

case neg
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hparity : ¬Even (Zsqrtd.norm a)
⊢ Even (evenFactorExp (Zsqrtd.norm a))
Theorem: factors_2_even'
Proof state before:
case pos
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hparity : Even (Zsqrtd.norm a)
⊢ Even (evenFactorExp (Zsqrtd.norm a))
Tactic:
obtain ⟨u, huvcoprime, huvprod⟩ := step1' hcoprime hparity
Proof state after:
case pos.intro.intro
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hparity : Even (Zsqrtd.norm a)
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : Zsqrtd.norm a = 4 * Zsqrtd.norm u
⊢ Even (evenFactorExp (Zsqrtd.norm a))
Theorem: factors_2_even'
Proof state before:
case pos.intro.intro
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hparity : Even (Zsqrtd.norm a)
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : Zsqrtd.norm a = 4 * Zsqrtd.norm u
⊢ Even (evenFactorExp (Zsqrtd.norm a))
Tactic:
have huv := Spts.ne_zero_of_coprime' _ huvcoprime
Proof state after:
case pos.intro.intro
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hparity : Even (Zsqrtd.norm a)
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : Zsqrtd.norm a = 4 * Zsqrtd.norm u
huv : Zsqrtd.norm u ≠ 0
⊢ Even (evenFactorExp (Zsqrtd.norm a))
Theorem: factors_2_even'
Proof state before:
case pos.intro.intro
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hparity : Even (Zsqrtd.norm a)
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : Zsqrtd.norm a = 4 * Zsqrtd.norm u
huv : Zsqrtd.norm u ≠ 0
⊢ Even (evenFactorExp (Zsqrtd.norm a))
Tactic:
rw [huvprod, factors_2_even huv, Nat.even_add]
Proof state after:
case pos.intro.intro
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hparity : Even (Zsqrtd.norm a)
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : Zsqrtd.norm a = 4 * Zsqrtd.norm u
huv : Zsqrtd.norm u ≠ 0
⊢ Even 2 ↔ Even (evenFactorExp (Zsqrtd.norm u))
Theorem: factors_2_even'
Proof state before:
case pos.intro.intro
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hparity : Even (Zsqrtd.norm a)
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : Zsqrtd.norm a = 4 * Zsqrtd.norm u
huv : Zsqrtd.norm u ≠ 0
⊢ Even 2 ↔ Even (evenFactorExp (Zsqrtd.norm u))
Tactic:
apply iff_of_true even_two
Proof state after:
case pos.intro.intro
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hparity : Even (Zsqrtd.norm a)
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : Zsqrtd.norm a = 4 * Zsqrtd.norm u
huv : Zsqrtd.norm u ≠ 0
⊢ Even (evenFactorExp (Zsqrtd.norm u))
Theorem: factors_2_even'
Proof state before:
case pos.intro.intro
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hparity : Even (Zsqrtd.norm a)
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : Zsqrtd.norm a = 4 * Zsqrtd.norm u
huv : Zsqrtd.norm u ≠ 0
⊢ Even (evenFactorExp (Zsqrtd.norm u))
Tactic:
apply ih _ _ huvcoprime rfl
Proof state after:
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hparity : Even (Zsqrtd.norm a)
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : Zsqrtd.norm a = 4 * Zsqrtd.norm u
huv : Zsqrtd.norm u ≠ 0
⊢ Int.natAbs (Zsqrtd.norm u) < n
Theorem: factors_2_even'
Proof state before:
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hparity : Even (Zsqrtd.norm a)
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : Zsqrtd.norm a = 4 * Zsqrtd.norm u
huv : Zsqrtd.norm u ≠ 0
⊢ Int.natAbs (Zsqrtd.norm u) < n
Tactic:
rw [← hn, huvprod, Int.natAbs_mul, lt_mul_iff_one_lt_left (Int.natAbs_pos.mpr huv)]
Proof state after:
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hparity : Even (Zsqrtd.norm a)
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : Zsqrtd.norm a = 4 * Zsqrtd.norm u
huv : Zsqrtd.norm u ≠ 0
⊢ 1 < Int.natAbs 4
Theorem: factors_2_even'
Proof state before:
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hparity : Even (Zsqrtd.norm a)
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : Zsqrtd.norm a = 4 * Zsqrtd.norm u
huv : Zsqrtd.norm u ≠ 0
⊢ 1 < Int.natAbs 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: factors_2_even'
Proof state before:
case neg
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hparity : ¬Even (Zsqrtd.norm a)
⊢ Even (evenFactorExp (Zsqrtd.norm a))
Tactic:
convert even_zero (α := ℕ)
Proof state after:
case h.e'_3
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hparity : ¬Even (Zsqrtd.norm a)
⊢ evenFactorExp (Zsqrtd.norm a) = 0
Theorem: factors_2_even'
Proof state before:
case h.e'_3
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hparity : ¬Even (Zsqrtd.norm a)
⊢ evenFactorExp (Zsqrtd.norm a) = 0
Tactic:
simp only [evenFactorExp, Multiset.count_eq_zero, hn]
Proof state after:
case h.e'_3
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hparity : ¬Even (Zsqrtd.norm a)
⊢ ¬2 ∈ UniqueFactorizationMonoid.normalizedFactors (Zsqrtd.norm a)
Theorem: factors_2_even'
Proof state before:
case h.e'_3
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hparity : ¬Even (Zsqrtd.norm a)
⊢ ¬2 ∈ UniqueFactorizationMonoid.normalizedFactors (Zsqrtd.norm a)
Tactic:
contrapose! hparity with hfactor
Proof state after:
case h.e'_3
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hfactor : 2 ∈ UniqueFactorizationMonoid.normalizedFactors (Zsqrtd.norm a)
⊢ Even (Zsqrtd.norm a)
Theorem: factors_2_even'
Proof state before:
case h.e'_3
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hfactor : 2 ∈ UniqueFactorizationMonoid.normalizedFactors (Zsqrtd.norm a)
⊢ Even (Zsqrtd.norm a)
Tactic:
rw [even_iff_two_dvd]
Proof state after:
case h.e'_3
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hfactor : 2 ∈ UniqueFactorizationMonoid.normalizedFactors (Zsqrtd.norm a)
⊢ 2 ∣ Zsqrtd.norm a
Theorem: factors_2_even'
Proof state before:
case h.e'_3
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hfactor : 2 ∈ UniqueFactorizationMonoid.normalizedFactors (Zsqrtd.norm a)
⊢ 2 ∣ Zsqrtd.norm a
Tactic:
exact UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors hfactor
Proof state after:
no goals
Theorem: eq_or_eq_conj_of_associated_of_re_zero
Proof state before:
case intro
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
⊢ x = A ∨ x = star A
Tactic:
obtain ⟨v, hv1, hv2⟩ := Zsqrt3.coe_of_isUnit' u.isUnit
Proof state after:
case intro.intro.intro
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hv2 : abs v = 1
⊢ x = A ∨ x = star A
Theorem: eq_or_eq_conj_of_associated_of_re_zero
Proof state before:
case intro.intro.intro
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hv2 : abs v = 1
⊢ x = A ∨ x = star A
Tactic:
have hA : A.re = 0 := by
  simp only [← hu, hv1, hx, add_zero, MulZeroClass.zero_mul, Zsqrtd.mul_re, MulZeroClass.mul_zero,
    Zsqrtd.coe_int_im]
Proof state after:
case intro.intro.intro
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hv2 : abs v = 1
hA : A.re = 0
⊢ x = A ∨ x = star A
Theorem: eq_or_eq_conj_of_associated_of_re_zero
Proof state before:
case intro.intro.intro
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hv2 : abs v = 1
hA : A.re = 0
⊢ x = A ∨ x = star A
Tactic:
rw [abs_eq <| zero_le_one' ℤ] at hv2
Proof state after:
case intro.intro.intro
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hv2 : v = 1 ∨ v = -1
hA : A.re = 0
⊢ x = A ∨ x = star A
Theorem: eq_or_eq_conj_of_associated_of_re_zero
Proof state before:
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hv2 : abs v = 1
⊢ A.re = 0
Tactic:
simp only [← hu, hv1, hx, add_zero, MulZeroClass.zero_mul, Zsqrtd.mul_re, MulZeroClass.mul_zero,
  Zsqrtd.coe_int_im]
Proof state after:
no goals
Theorem: eq_or_eq_conj_of_associated_of_re_zero
Proof state before:
case intro.intro.intro.inr.h
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hA : A.re = 0
hv2 : v = -1
hu : -x = A
⊢ x = star A
Tactic:
simp [← hu, hx, Zsqrtd.ext]
Proof state after:
no goals
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof state before:
case mp
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
⊢ Associated' x A → x = A ∨ x = star A
Tactic:
rintro (⟨u, hu⟩ | ⟨u, hu⟩) <;> obtain ⟨v, hv1, hv2⟩ := Zsqrt3.coe_of_isUnit' u.isUnit
Proof state after:
case mp.inl.intro.intro.intro
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hv2 : abs v = 1
⊢ x = A ∨ x = star A

case mp.inr.intro.intro.intro
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
hu : x * ↑u = star A
v : ℤ
hv1 : ↑u = ↑v
hv2 : abs v = 1
⊢ x = A ∨ x = star A
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof state before:
case mp.inl.intro.intro.intro
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hv2 : abs v = 1
⊢ x = A ∨ x = star A
Tactic:
by_cases hxre : x.re = 0
Proof state after:
case pos
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hv2 : abs v = 1
hxre : x.re = 0
⊢ x = A ∨ x = star A

case neg
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hv2 : abs v = 1
hxre : ¬x.re = 0
⊢ x = A ∨ x = star A
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof state before:
case pos
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hv2 : abs v = 1
hxre : x.re = 0
⊢ x = A ∨ x = star A
Tactic:
apply eq_or_eq_conj_of_associated_of_re_zero hxre ⟨u, hu⟩
Proof state after:
no goals
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof state before:
case neg
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hv2 : abs v = 1
hxre : ¬x.re = 0
⊢ x = A ∨ x = star A
Tactic:
rw [hv1] at hu
Proof state after:
case neg
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hu : x * ↑v = A
hv1 : ↑u = ↑v
hv2 : abs v = 1
hxre : ¬x.re = 0
⊢ x = A ∨ x = star A
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof state before:
case neg
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hu : x * ↑v = A
hv1 : ↑u = ↑v
hv2 : abs v = 1
hxre : ¬x.re = 0
⊢ x = A ∨ x = star A
Tactic:
rw [abs_eq <| zero_le_one' ℤ] at hv2
Proof state after:
case neg
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hu : x * ↑v = A
hv1 : ↑u = ↑v
hv2 : v = 1 ∨ v = -1
hxre : ¬x.re = 0
⊢ x = A ∨ x = star A
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof state before:
case neg.inr
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hu : x * ↑v = A
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
⊢ x = A ∨ x = star A
Tactic:
exfalso
Proof state after:
case neg.inr.h
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hu : x * ↑v = A
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
⊢ False
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof state before:
case neg.inr.h
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hu : x * ↑v = A
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
⊢ False
Tactic:
simp only [habsv, mul_one, Int.cast_one, mul_neg, Int.cast_neg] at hu
Proof state after:
case neg.inr.h
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = A
⊢ False
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof state before:
case neg.inr.h
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = A
⊢ False
Tactic:
apply lt_irrefl (0 : ℤ)
Proof state after:
case neg.inr.h
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = A
⊢ 0 < 0
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof state before:
case neg.inr.h
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = A
⊢ 0 < 0
Tactic:
calc
  0 ≤ A.re := hA
  _ = -x.re := ?_
  _ < 0 := ?_
Proof state after:
case neg.inr.h.calc_1
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = A
⊢ A.re = -x.re

case neg.inr.h.calc_2
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = A
⊢ -x.re < 0