internlm/Lean-Github huggingface dataset:
Theorem: associated'_of_associated_norm
Proof state before:
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
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 x.norm y.norm
hx : IsCoprime x.re x.im
hy : IsCoprime y.re y.im
h' : OddPrimeOrFour x.norm.natAbs
⊢ -3 ≤ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: factorization'.associated'_of_norm_associated
Proof state before:
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Associated b.norm c.norm
⊢ 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 : Associated b.norm c.norm
⊢ Associated b.norm c.norm

case hx
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Associated b.norm c.norm
⊢ 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 : Associated b.norm c.norm
⊢ 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 : Associated b.norm c.norm
⊢ OddPrimeOrFour b.norm.natAbs
Theorem: factorization'.associated'_of_norm_associated
Proof state before:
case h
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Associated b.norm c.norm
⊢ Associated b.norm c.norm
Tactic:
exact hnorm
Proof state after:
no goals
Theorem: factorization'.associated'_of_norm_associated
Proof state before:
case hx
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Associated b.norm c.norm
⊢ IsCoprime b.re b.im
Tactic:
exact factorization'.coprime_of_mem h hbmem
Proof state after:
no goals
Theorem: factorization'.associated'_of_norm_associated
Proof state before:
case hy
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Associated b.norm c.norm
⊢ IsCoprime c.re c.im
Tactic:
exact factorization'.coprime_of_mem h hcmem
Proof state after:
no goals
Theorem: factorization'.associated'_of_norm_associated
Proof state before:
case h'
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Associated b.norm c.norm
⊢ OddPrimeOrFour b.norm.natAbs
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 ∈ f, OddPrimeOrFour x.norm.natAbs
hf' : ∀ x ∈ f, IsCoprime x.re x.im
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hg' : ∀ x ∈ g, IsCoprime x.re x.im
h : Associated f.prod g.prod
p : ∀ x ∈ f, ∀ y ∈ g, (Int.natAbs ∘ Zsqrtd.norm) x = (Int.natAbs ∘ 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 ∈ f, OddPrimeOrFour x.norm.natAbs
hf' : ∀ x ∈ f, IsCoprime x.re x.im
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hg' : ∀ x ∈ g, IsCoprime x.re x.im
h : Associated f.prod g.prod
p : ∀ x ∈ f, ∀ y ∈ g, (Int.natAbs ∘ Zsqrtd.norm) x = (Int.natAbs ∘ Zsqrtd.norm) y → Associated' x y
⊢ Multiset.Rel (fun a b => (Int.natAbs ∘ Zsqrtd.norm) a = (Int.natAbs ∘ Zsqrtd.norm) b) f g
Theorem: factors_unique
Proof state before:
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hf' : ∀ x ∈ f, IsCoprime x.re x.im
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hg' : ∀ x ∈ g, IsCoprime x.re x.im
h : Associated f.prod g.prod
p : ∀ x ∈ f, ∀ y ∈ g, (Int.natAbs ∘ Zsqrtd.norm) x = (Int.natAbs ∘ Zsqrtd.norm) y → Associated' x y
⊢ Multiset.Rel (fun a b => (Int.natAbs ∘ Zsqrtd.norm) a = (Int.natAbs ∘ Zsqrtd.norm) b) f g
Tactic:
rw [← Multiset.rel_map, factors_unique_prod hf hg <| Zsqrtd.associated_norm_of_associated h,
  Multiset.rel_eq]
Proof state after:
no goals
Theorem: factors_unique
Proof state before:
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hf' : ∀ x ∈ f, IsCoprime x.re x.im
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hg' : ∀ x ∈ g, IsCoprime x.re x.im
h : Associated f.prod g.prod
⊢ ∀ x ∈ f, ∀ y ∈ g, (Int.natAbs ∘ Zsqrtd.norm) x = (Int.natAbs ∘ Zsqrtd.norm) y → Associated' x y
Tactic:
intro x hx y hy hxy
Proof state after:
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hf' : ∀ x ∈ f, IsCoprime x.re x.im
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hg' : ∀ x ∈ g, IsCoprime x.re x.im
h : Associated f.prod g.prod
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : (Int.natAbs ∘ Zsqrtd.norm) x = (Int.natAbs ∘ Zsqrtd.norm) y
⊢ Associated' x y
Theorem: factors_unique
Proof state before:
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hf' : ∀ x ∈ f, IsCoprime x.re x.im
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hg' : ∀ x ∈ g, IsCoprime x.re x.im
h : Associated f.prod g.prod
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : (Int.natAbs ∘ Zsqrtd.norm) x = (Int.natAbs ∘ Zsqrtd.norm) y
⊢ Associated' x y
Tactic:
rw [Function.comp_apply, Function.comp_apply, ← Int.associated_iff_natAbs] at hxy
Proof state after:
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hf' : ∀ x ∈ f, IsCoprime x.re x.im
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hg' : ∀ x ∈ g, IsCoprime x.re x.im
h : Associated f.prod g.prod
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : Associated x.norm y.norm
⊢ Associated' x y
Theorem: factors_unique
Proof state before:
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hf' : ∀ x ∈ f, IsCoprime x.re x.im
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hg' : ∀ x ∈ g, IsCoprime x.re x.im
h : Associated f.prod g.prod
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : Associated x.norm y.norm
⊢ Associated' x y
Tactic:
apply associated'_of_associated_norm hxy
Proof state after:
case hx
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hf' : ∀ x ∈ f, IsCoprime x.re x.im
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hg' : ∀ x ∈ g, IsCoprime x.re x.im
h : Associated f.prod g.prod
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : Associated x.norm y.norm
⊢ IsCoprime x.re x.im

case hy
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hf' : ∀ x ∈ f, IsCoprime x.re x.im
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hg' : ∀ x ∈ g, IsCoprime x.re x.im
h : Associated f.prod g.prod
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : Associated x.norm y.norm
⊢ IsCoprime y.re y.im

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

case neg
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : ¬Even a.norm.natAbs
⊢ Even (evenFactorExp n)
Theorem: factors_2_even'
Proof state before:
case pos
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
⊢ Even (evenFactorExp n)
Tactic:
obtain ⟨u, huvcoprime, huvprod⟩ := step1' hcoprime (Int.natAbs_even.mp hparity)
Proof state after:
case pos.intro.intro
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
⊢ Even (evenFactorExp n)
Theorem: factors_2_even'
Proof state before:
case pos.intro.intro
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
⊢ Even (evenFactorExp n)
Tactic:
have huv := Spts.ne_zero_of_coprime' _ huvcoprime
Proof state after:
case pos.intro.intro
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
⊢ Even (evenFactorExp n)
Theorem: factors_2_even'
Proof state before:
case pos.intro.intro
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
⊢ Even (evenFactorExp n)
Tactic:
have h₄ : Int.natAbs 4 = 4 := by norm_num
Proof state after:
case pos.intro.intro
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
h₄ : Int.natAbs 4 = 4
⊢ Even (evenFactorExp n)
Theorem: factors_2_even'
Proof state before:
case pos.intro.intro
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
h₄ : Int.natAbs 4 = 4
⊢ Even (evenFactorExp n)
Tactic:
rw [← hn, huvprod, Int.natAbs_mul, h₄, factors_2_even (by simpa using huv), Nat.even_add]
Proof state after:
case pos.intro.intro
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
h₄ : Int.natAbs 4 = 4
⊢ Even 2 ↔ Even (evenFactorExp u.norm.natAbs)
Theorem: factors_2_even'
Proof state before:
case pos.intro.intro
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
h₄ : Int.natAbs 4 = 4
⊢ Even 2 ↔ Even (evenFactorExp u.norm.natAbs)
Tactic:
apply iff_of_true even_two
Proof state after:
case pos.intro.intro
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
h₄ : Int.natAbs 4 = 4
⊢ Even (evenFactorExp u.norm.natAbs)
Theorem: factors_2_even'
Proof state before:
case pos.intro.intro
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
h₄ : Int.natAbs 4 = 4
⊢ Even (evenFactorExp u.norm.natAbs)
Tactic:
apply ih _ _ huvcoprime rfl
Proof state after:
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
h₄ : Int.natAbs 4 = 4
⊢ u.norm.natAbs < n
Theorem: factors_2_even'
Proof state before:
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
h₄ : Int.natAbs 4 = 4
⊢ u.norm.natAbs < n
Tactic:
rw [← hn, huvprod, Int.natAbs_mul, lt_mul_iff_one_lt_left (Int.natAbs_pos.mpr huv)]
Proof state after:
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
h₄ : Int.natAbs 4 = 4
⊢ 1 < Int.natAbs 4
Theorem: factors_2_even'
Proof state before:
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
h₄ : Int.natAbs 4 = 4
⊢ 1 < Int.natAbs 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: factors_2_even'
Proof state before:
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
⊢ Int.natAbs 4 = 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: factors_2_even'
Proof state before:
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : Even a.norm.natAbs
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : a.norm = 4 * u.norm
huv : u.norm ≠ 0
h₄ : Int.natAbs 4 = 4
⊢ u.norm.natAbs ≠ 0
Tactic:
simpa using huv
Proof state after:
no goals
Theorem: factors_2_even'
Proof state before:
case neg
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : ¬Even a.norm.natAbs
⊢ Even (evenFactorExp n)
Tactic:
convert even_zero (α := ℕ)
Proof state after:
case h.e'_3
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : ¬Even a.norm.natAbs
⊢ evenFactorExp n = 0
Theorem: factors_2_even'
Proof state before:
case h.e'_3
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : ¬Even a.norm.natAbs
⊢ evenFactorExp n = 0
Tactic:
simp only [evenFactorExp, Multiset.count_eq_zero, hn]
Proof state after:
case h.e'_3
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : ¬Even a.norm.natAbs
⊢ 2 ∉ UniqueFactorizationMonoid.normalizedFactors n
Theorem: factors_2_even'
Proof state before:
case h.e'_3
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hparity : ¬Even a.norm.natAbs
⊢ 2 ∉ UniqueFactorizationMonoid.normalizedFactors n
Tactic:
contrapose! hparity with hfactor
Proof state after:
case h.e'_3
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hfactor : 2 ∈ UniqueFactorizationMonoid.normalizedFactors n
⊢ Even a.norm.natAbs
Theorem: factors_2_even'
Proof state before:
case h.e'_3
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hfactor : 2 ∈ UniqueFactorizationMonoid.normalizedFactors n
⊢ Even a.norm.natAbs
Tactic:
rw [hn, even_iff_two_dvd]
Proof state after:
case h.e'_3
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hfactor : 2 ∈ UniqueFactorizationMonoid.normalizedFactors n
⊢ 2 ∣ n
Theorem: factors_2_even'
Proof state before:
case h.e'_3
n : ℕ
ih : ∀ m < n, ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → a.norm.natAbs = m → Even (evenFactorExp m)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
hfactor : 2 ∈ UniqueFactorizationMonoid.normalizedFactors n
⊢ 2 ∣ n
Tactic:
exact UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors hfactor
Proof state after:
no goals
Theorem: factorsOddPrimeOrFour.unique
Proof state before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ factorsOddPrimeOrFour a.norm.natAbs = f
Tactic:
rw [← hassoc]
Proof state after:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ factorsOddPrimeOrFour f.prod = f
Theorem: factorsOddPrimeOrFour.unique
Proof state before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ factorsOddPrimeOrFour f.prod = f
Tactic:
refine factorsOddPrimeOrFour.unique' hf ?_ ?_
Proof state after:
case refine_1
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ 0 < f.prod

case refine_2
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ Even (evenFactorExp f.prod)
Theorem: factorsOddPrimeOrFour.unique
Proof state before:
case refine_1
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ 0 < f.prod
Tactic:
rw [hassoc, Int.natAbs_pos]
Proof state after:
case refine_1
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ a.norm ≠ 0
Theorem: factorsOddPrimeOrFour.unique
Proof state before:
case refine_1
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ a.norm ≠ 0
Tactic:
exact Spts.ne_zero_of_coprime' _ hcoprime
Proof state after:
no goals
Theorem: factorsOddPrimeOrFour.unique
Proof state before:
case refine_2
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ Even (evenFactorExp f.prod)
Tactic:
rw [hassoc]
Proof state after:
case refine_2
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ Even (evenFactorExp a.norm.natAbs)
Theorem: factorsOddPrimeOrFour.unique
Proof state before:
case refine_2
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ Even (evenFactorExp a.norm.natAbs)
Tactic:
exact factors_2_even' hcoprime
Proof state after:
no goals
Theorem: eq_or_eq_conj_of_associated_of_re_zero
Proof state before:
x A : ℤ√(-3)
hx : x.re = 0
h : Associated x A
⊢ x = A ∨ x = star A
Tactic:
obtain ⟨u, hu⟩ := h
Proof state after:
case intro
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
⊢ x = A ∨ x = star A
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 : |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 : |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.intCast_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 : |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 : |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:
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
Tactic:
cases' hv2 with hv2 hv2
Proof state after:
case intro.intro.intro.inl
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hA : A.re = 0
hv2 : v = 1
⊢ x = A ∨ x = star A

case intro.intro.intro.inr
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hA : A.re = 0
hv2 : v = -1
⊢ 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 : |v| = 1
⊢ A.re = 0
Tactic:
simp only [← hu, hv1, hx, add_zero, MulZeroClass.zero_mul, Zsqrtd.mul_re, MulZeroClass.mul_zero,
  Zsqrtd.intCast_im]
Proof state after:
no goals