internlm/Lean-Github huggingface dataset:
Theorem: IsPrimitiveRoot.associated_sub_one
Proof state before:
case intro.intro.intro.intro
n : ℕ+
K : Type u
L : Type v
A✝ : Type w
B : Type z
inst✝⁷ : CommRing A✝
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A✝ B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ nthRootsFinset p A
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ nthRootsFinset p A
e : ζ ^ i ≠ ζ ^ j
⊢ Associated (ζ - 1) (ζ ^ i - ζ ^ j)
Tactic:
have : i ≠ j := ne_of_apply_ne _ e
Proof state after:
case intro.intro.intro.intro
n : ℕ+
K : Type u
L : Type v
A✝ : Type w
B : Type z
inst✝⁷ : CommRing A✝
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A✝ B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ nthRootsFinset p A
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ nthRootsFinset p A
e : ζ ^ i ≠ ζ ^ j
this : i ≠ j
⊢ Associated (ζ - 1) (ζ ^ i - ζ ^ j)
Theorem: IsPrimitiveRoot.associated_sub_one
Proof state before:
case intro.intro.intro.intro
n : ℕ+
K : Type u
L : Type v
A✝ : Type w
B : Type z
inst✝⁷ : CommRing A✝
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A✝ B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ nthRootsFinset p A
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ nthRootsFinset p A
e : ζ ^ i ≠ ζ ^ j
this : i ≠ j
⊢ Associated (ζ - 1) (ζ ^ i - ζ ^ j)
Tactic:
obtain ⟨u, h⟩ := IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one A
  hp.two_le hp hi hj this hζ
Proof state after:
case intro.intro.intro.intro.intro
n : ℕ+
K : Type u
L : Type v
A✝ : Type w
B : Type z
inst✝⁷ : CommRing A✝
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A✝ B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ nthRootsFinset p A
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ nthRootsFinset p A
e : ζ ^ i ≠ ζ ^ j
this : i ≠ j
u : Aˣ
h : ζ ^ i - ζ ^ j = ↑u * (1 - ζ)
⊢ Associated (ζ - 1) (ζ ^ i - ζ ^ j)
Theorem: IsPrimitiveRoot.associated_sub_one
Proof state before:
case intro.intro.intro.intro.intro
n : ℕ+
K : Type u
L : Type v
A✝ : Type w
B : Type z
inst✝⁷ : CommRing A✝
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A✝ B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ nthRootsFinset p A
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ nthRootsFinset p A
e : ζ ^ i ≠ ζ ^ j
this : i ≠ j
u : Aˣ
h : ζ ^ i - ζ ^ j = ↑u * (1 - ζ)
⊢ Associated (ζ - 1) (ζ ^ i - ζ ^ j)
Tactic:
rw [h, associated_isUnit_mul_right_iff u.isUnit, ← associated_isUnit_mul_right_iff isUnit_one.neg,
  neg_one_mul, neg_sub]
Proof state after:
case intro.intro.intro.intro.intro
n : ℕ+
K : Type u
L : Type v
A✝ : Type w
B : Type z
inst✝⁷ : CommRing A✝
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A✝ B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ nthRootsFinset p A
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ nthRootsFinset p A
e : ζ ^ i ≠ ζ ^ j
this : i ≠ j
u : Aˣ
h : ζ ^ i - ζ ^ j = ↑u * (1 - ζ)
⊢ Associated (ζ - 1) (ζ - 1)
Theorem: IsPrimitiveRoot.associated_sub_one
Proof state before:
case intro.intro.intro.intro.intro
n : ℕ+
K : Type u
L : Type v
A✝ : Type w
B : Type z
inst✝⁷ : CommRing A✝
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A✝ B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ nthRootsFinset p A
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ nthRootsFinset p A
e : ζ ^ i ≠ ζ ^ j
this : i ≠ j
u : Aˣ
h : ζ ^ i - ζ ^ j = ↑u * (1 - ζ)
⊢ Associated (ζ - 1) (ζ - 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: Zsqrtd.associated_norm_of_associated
Proof state before:
d : ℤ
f g : ℤ√d
h : Associated f g
⊢ Associated f.norm g.norm
Tactic:
obtain ⟨u, rfl⟩ := h
Proof state after:
case intro
d : ℤ
f : ℤ√d
u : (ℤ√d)ˣ
⊢ Associated f.norm (f * ↑u).norm
Theorem: Zsqrtd.associated_norm_of_associated
Proof state before:
case intro
d : ℤ
f : ℤ√d
u : (ℤ√d)ˣ
⊢ Associated f.norm (f * ↑u).norm
Tactic:
have := (Zsqrtd.isUnit_iff_norm_isUnit u).mp u.isUnit
Proof state after:
case intro
d : ℤ
f : ℤ√d
u : (ℤ√d)ˣ
this : IsUnit (↑u).norm
⊢ Associated f.norm (f * ↑u).norm
Theorem: Zsqrtd.associated_norm_of_associated
Proof state before:
case intro
d : ℤ
f : ℤ√d
u : (ℤ√d)ˣ
this : IsUnit (↑u).norm
⊢ Associated f.norm (f * ↑u).norm
Tactic:
rw [Zsqrtd.norm_mul]
Proof state after:
case intro
d : ℤ
f : ℤ√d
u : (ℤ√d)ˣ
this : IsUnit (↑u).norm
⊢ Associated f.norm (f.norm * (↑u).norm)
Theorem: Zsqrtd.associated_norm_of_associated
Proof state before:
case intro
d : ℤ
f : ℤ√d
u : (ℤ√d)ˣ
this : IsUnit (↑u).norm
⊢ Associated f.norm (f.norm * (↑u).norm)
Tactic:
exact associated_mul_unit_right (Zsqrtd.norm f) _ this
Proof state after:
no goals
Theorem: OddPrimeOrFour.im_ne_zero
Proof state before:
p : ℤ√(-3)
h : OddPrimeOrFour p.norm.natAbs
hcoprime : IsCoprime p.re p.im
⊢ p.im ≠ 0
Tactic:
intro H
Proof state after:
p : ℤ√(-3)
h : OddPrimeOrFour p.norm.natAbs
hcoprime : IsCoprime p.re p.im
H : p.im = 0
⊢ False
Theorem: OddPrimeOrFour.im_ne_zero
Proof state before:
p : ℤ√(-3)
h : OddPrimeOrFour p.norm.natAbs
hcoprime : IsCoprime p.re p.im
H : p.im = 0
⊢ False
Tactic:
rw [Zsqrtd.norm_def, H, MulZeroClass.mul_zero, sub_zero, ← pow_two] at h
Proof state after:
p : ℤ√(-3)
h : OddPrimeOrFour (p.re ^ 2).natAbs
hcoprime : IsCoprime p.re p.im
H : p.im = 0
⊢ False
Theorem: OddPrimeOrFour.im_ne_zero
Proof state before:
p : ℤ√(-3)
h : OddPrimeOrFour (p.re ^ 2).natAbs
hcoprime : IsCoprime p.re p.im
H : p.im = 0
⊢ False
Tactic:
obtain h | ⟨hp, -⟩ := h
Proof state after:
case inl
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
H : p.im = 0
h : (p.re ^ 2).natAbs = 4
⊢ False

case inr.intro
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
H : p.im = 0
hp : (p.re ^ 2).natAbs.Prime
⊢ False
Theorem: OddPrimeOrFour.im_ne_zero
Proof state before:
case inl
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
H : p.im = 0
h : (p.re ^ 2).natAbs = 4
⊢ False
Tactic:
rw [H, isCoprime_zero_right, Int.isUnit_iff_abs_eq] at hcoprime
Proof state after:
case inl
p : ℤ√(-3)
hcoprime : |p.re| = 1
H : p.im = 0
h : (p.re ^ 2).natAbs = 4
⊢ False
Theorem: OddPrimeOrFour.im_ne_zero
Proof state before:
case inl
p : ℤ√(-3)
hcoprime : |p.re| = 1
H : p.im = 0
h : (p.re ^ 2).natAbs = 4
⊢ False
Tactic:
rw [← sq_abs, hcoprime] at h
Proof state after:
case inl
p : ℤ√(-3)
hcoprime : |p.re| = 1
H : p.im = 0
h : (1 ^ 2).natAbs = 4
⊢ False
Theorem: OddPrimeOrFour.im_ne_zero
Proof state before:
case inl
p : ℤ√(-3)
hcoprime : |p.re| = 1
H : p.im = 0
h : (1 ^ 2).natAbs = 4
⊢ False
Tactic:
norm_num at h
Proof state after:
no goals
Theorem: OddPrimeOrFour.im_ne_zero
Proof state before:
case inr.intro
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
H : p.im = 0
hp : (p.re ^ 2).natAbs.Prime
⊢ False
Tactic:
rw [Int.natAbs_pow] at hp
Proof state after:
case inr.intro
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
H : p.im = 0
hp : (p.re.natAbs ^ 2).Prime
⊢ False
Theorem: OddPrimeOrFour.im_ne_zero
Proof state before:
case inr.intro
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
H : p.im = 0
hp : (p.re.natAbs ^ 2).Prime
⊢ False
Tactic:
exact hp.not_prime_pow le_rfl
Proof state after:
no goals
Theorem: Zsqrt3.isUnit_iff
Proof state before:
z : ℤ√(-3)
⊢ IsUnit z ↔ |z.re| = 1 ∧ z.im = 0
Tactic:
rw [← Zsqrtd.norm_eq_one_iff, ← Int.natCast_inj, Int.ofNat_one,
  Int.natAbs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) z)]
Proof state after:
z : ℤ√(-3)
⊢ z.norm = 1 ↔ |z.re| = 1 ∧ z.im = 0
Theorem: Zsqrt3.isUnit_iff
Proof state before:
z : ℤ√(-3)
⊢ z.norm = 1 ↔ |z.re| = 1 ∧ z.im = 0
Tactic:
refine' ⟨Spts.eq_one, fun h => _⟩
Proof state after:
z : ℤ√(-3)
h : |z.re| = 1 ∧ z.im = 0
⊢ z.norm = 1
Theorem: Zsqrt3.isUnit_iff
Proof state before:
z : ℤ√(-3)
h : |z.re| = 1 ∧ z.im = 0
⊢ z.norm = 1
Tactic:
rw [Zsqrtd.norm_def, h.2, MulZeroClass.mul_zero, sub_zero, ← sq, ← sq_abs, h.1, one_pow]
Proof state after:
no goals
Theorem: Zsqrt3.isUnit_iff
Proof state before:
z : ℤ√(-3)
⊢ -3 ≤ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: Zsqrt3.coe_of_isUnit
Proof state before:
z : ℤ√(-3)
h : IsUnit z
⊢ ∃ u, z = ↑↑u
Tactic:
obtain ⟨u, hu⟩ := Zsqrt3.isUnit_iff.mp h
Proof state after:
case intro
z : ℤ√(-3)
h : IsUnit z
u : |z.re| = 1
hu : z.im = 0
⊢ ∃ u, z = ↑↑u
Theorem: Zsqrt3.coe_of_isUnit
Proof state before:
case intro
z : ℤ√(-3)
h : IsUnit z
u : |z.re| = 1
hu : z.im = 0
⊢ ∃ u, z = ↑↑u
Tactic:
obtain ⟨v, hv⟩ : IsUnit z.re := by rwa [Int.isUnit_iff_abs_eq]
Proof state after:
case intro.intro
z : ℤ√(-3)
h : IsUnit z
u : |z.re| = 1
hu : z.im = 0
v : ℤˣ
hv : ↑v = z.re
⊢ ∃ u, z = ↑↑u
Theorem: Zsqrt3.coe_of_isUnit
Proof state before:
case intro.intro
z : ℤ√(-3)
h : IsUnit z
u : |z.re| = 1
hu : z.im = 0
v : ℤˣ
hv : ↑v = z.re
⊢ ∃ u, z = ↑↑u
Tactic:
use v
Proof state after:
case h
z : ℤ√(-3)
h : IsUnit z
u : |z.re| = 1
hu : z.im = 0
v : ℤˣ
hv : ↑v = z.re
⊢ z = ↑↑v
Theorem: Zsqrt3.coe_of_isUnit
Proof state before:
case h
z : ℤ√(-3)
h : IsUnit z
u : |z.re| = 1
hu : z.im = 0
v : ℤˣ
hv : ↑v = z.re
⊢ z = ↑↑v
Tactic:
rw [Zsqrtd.ext_iff, hu, ← hv]
Proof state after:
case h
z : ℤ√(-3)
h : IsUnit z
u : |z.re| = 1
hu : z.im = 0
v : ℤˣ
hv : ↑v = z.re
⊢ ↑v = (↑↑v).re ∧ 0 = (↑↑v).im
Theorem: Zsqrt3.coe_of_isUnit
Proof state before:
case h
z : ℤ√(-3)
h : IsUnit z
u : |z.re| = 1
hu : z.im = 0
v : ℤˣ
hv : ↑v = z.re
⊢ ↑v = (↑↑v).re ∧ 0 = (↑↑v).im
Tactic:
simp only [Zsqrtd.intCast_re, and_true_iff, eq_self_iff_true, Zsqrtd.intCast_im]
Proof state after:
no goals
Theorem: Zsqrt3.coe_of_isUnit
Proof state before:
z : ℤ√(-3)
h : IsUnit z
u : |z.re| = 1
hu : z.im = 0
⊢ IsUnit z.re
Tactic:
rwa [Int.isUnit_iff_abs_eq]
Proof state after:
no goals
Theorem: Zsqrt3.coe_of_isUnit'
Proof state before:
z : ℤ√(-3)
h : IsUnit z
⊢ ∃ u, z = ↑u ∧ |u| = 1
Tactic:
obtain ⟨u, hu⟩ := Zsqrt3.coe_of_isUnit h
Proof state after:
case intro
z : ℤ√(-3)
h : IsUnit z
u : ℤˣ
hu : z = ↑↑u
⊢ ∃ u, z = ↑u ∧ |u| = 1
Theorem: Zsqrt3.coe_of_isUnit'
Proof state before:
case intro
z : ℤ√(-3)
h : IsUnit z
u : ℤˣ
hu : z = ↑↑u
⊢ ∃ u, z = ↑u ∧ |u| = 1
Tactic:
refine' ⟨u, _, _⟩
Proof state after:
case intro.refine'_1
z : ℤ√(-3)
h : IsUnit z
u : ℤˣ
hu : z = ↑↑u
⊢ z = ↑↑u

case intro.refine'_2
z : ℤ√(-3)
h : IsUnit z
u : ℤˣ
hu : z = ↑↑u
⊢ |↑u| = 1
Theorem: Zsqrt3.coe_of_isUnit'
Proof state before:
case intro.refine'_1
z : ℤ√(-3)
h : IsUnit z
u : ℤˣ
hu : z = ↑↑u
⊢ z = ↑↑u
Tactic:
rw [hu]
Proof state after:
no goals
Theorem: Zsqrt3.coe_of_isUnit'
Proof state before:
case intro.refine'_2
z : ℤ√(-3)
h : IsUnit z
u : ℤˣ
hu : z = ↑↑u
⊢ |↑u| = 1
Tactic:
exact Int.isUnit_iff_abs_eq.mp u.isUnit
Proof state after:
no goals
Theorem: Zsqrt3.norm_natAbs
Proof state before:
a : ℤ√(-3)
⊢ ↑a.norm.natAbs = a.norm
Tactic:
rw [Int.natAbs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) a)]
Proof state after:
no goals
Theorem: Zsqrt3.norm_natAbs
Proof state before:
a : ℤ√(-3)
⊢ -3 ≤ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: OddPrimeOrFour.factors
Proof state before:
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hx : OddPrimeOrFour x.natAbs
hfactor : x ∣ a.norm
⊢ ∃ c, |x| = c.norm ∧ 0 ≤ c.re ∧ c.im ≠ 0
Tactic:
obtain hx | ⟨hprime, hodd⟩ := hx
Proof state after:
case inl
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hx : x.natAbs = 4
⊢ ∃ c, |x| = c.norm ∧ 0 ≤ c.re ∧ c.im ≠ 0

case inr.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hprime : x.natAbs.Prime
hodd : Odd x.natAbs
⊢ ∃ c, |x| = c.norm ∧ 0 ≤ c.re ∧ c.im ≠ 0
Theorem: OddPrimeOrFour.factors
Proof state before:
case inl
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hx : x.natAbs = 4
⊢ ∃ c, |x| = c.norm ∧ 0 ≤ c.re ∧ c.im ≠ 0
Tactic:
refine' ⟨⟨1, 1⟩, _, zero_le_one, one_ne_zero⟩
Proof state after:
case inl
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hx : x.natAbs = 4
⊢ |x| = { re := 1, im := 1 }.norm
Theorem: OddPrimeOrFour.factors
Proof state before:
case inl
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hx : x.natAbs = 4
⊢ |x| = { re := 1, im := 1 }.norm
Tactic:
simp only [Zsqrtd.norm_def, mul_one, sub_neg_eq_add, Int.abs_eq_natAbs, hx]
Proof state after:
case inl
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hx : x.natAbs = 4
⊢ ↑4 = 1 + 3
Theorem: OddPrimeOrFour.factors
Proof state before:
case inl
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hx : x.natAbs = 4
⊢ ↑4 = 1 + 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: OddPrimeOrFour.factors
Proof state before:
case inr.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hprime : x.natAbs.Prime
hodd : Odd x.natAbs
⊢ ∃ c, |x| = c.norm ∧ 0 ≤ c.re ∧ c.im ≠ 0
Tactic:
rw [Int.natAbs_odd] at hodd
Proof state after:
case inr.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hprime : x.natAbs.Prime
hodd : Odd x
⊢ ∃ c, |x| = c.norm ∧ 0 ≤ c.re ∧ c.im ≠ 0
Theorem: OddPrimeOrFour.factors
Proof state before:
case inr.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hprime : x.natAbs.Prime
hodd : Odd x
⊢ ∃ c, |x| = c.norm ∧ 0 ≤ c.re ∧ c.im ≠ 0
Tactic:
obtain ⟨c, hc⟩ := _root_.factors a x hcoprime hodd hfactor
Proof state after:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hprime : x.natAbs.Prime
hodd : Odd x
c : ℤ√(-3)
hc : |x| = c.norm
⊢ ∃ c, |x| = c.norm ∧ 0 ≤ c.re ∧ c.im ≠ 0
Theorem: OddPrimeOrFour.factors
Proof state before:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hprime : x.natAbs.Prime
hodd : Odd x
c : ℤ√(-3)
hc : |x| = c.norm
⊢ ∃ c, |x| = c.norm ∧ 0 ≤ c.re ∧ c.im ≠ 0
Tactic:
rw [hc]
Proof state after:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hprime : x.natAbs.Prime
hodd : Odd x
c : ℤ√(-3)
hc : |x| = c.norm
⊢ ∃ c_1, c.norm = c_1.norm ∧ 0 ≤ c_1.re ∧ c_1.im ≠ 0
Theorem: OddPrimeOrFour.factors
Proof state before:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hprime : x.natAbs.Prime
hodd : Odd x
c : ℤ√(-3)
hc : |x| = c.norm
⊢ ∃ c_1, c.norm = c_1.norm ∧ 0 ≤ c_1.re ∧ c_1.im ≠ 0
Tactic:
apply Zsqrtd.exists c
Proof state after:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hprime : x.natAbs.Prime
hodd : Odd x
c : ℤ√(-3)
hc : |x| = c.norm
⊢ c.im ≠ 0
Theorem: OddPrimeOrFour.factors
Proof state before:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hprime : x.natAbs.Prime
hodd : Odd x
c : ℤ√(-3)
hc : |x| = c.norm
⊢ c.im ≠ 0
Tactic:
intro H
Proof state after:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hprime : x.natAbs.Prime
hodd : Odd x
c : ℤ√(-3)
hc : |x| = c.norm
H : c.im = 0
⊢ False
Theorem: OddPrimeOrFour.factors
Proof state before:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hprime : x.natAbs.Prime
hodd : Odd x
c : ℤ√(-3)
hc : |x| = c.norm
H : c.im = 0
⊢ False
Tactic:
rw [Zsqrtd.norm_def, H, MulZeroClass.mul_zero, sub_zero, ← pow_two, eq_comm, Int.abs_eq_natAbs]
  at hc
Proof state after:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hprime : x.natAbs.Prime
hodd : Odd x
c : ℤ√(-3)
hc : c.re ^ 2 = ↑x.natAbs
H : c.im = 0
⊢ False
Theorem: OddPrimeOrFour.factors
Proof state before:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hprime : x.natAbs.Prime
hodd : Odd x
c : ℤ√(-3)
hc : c.re ^ 2 = ↑x.natAbs
H : c.im = 0
⊢ False
Tactic:
rw [Nat.prime_iff_prime_int, ← hc] at hprime
Proof state after:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hodd : Odd x
c : ℤ√(-3)
hprime : Prime (c.re ^ 2)
hc : c.re ^ 2 = ↑x.natAbs
H : c.im = 0
⊢ False
Theorem: OddPrimeOrFour.factors
Proof state before:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hodd : Odd x
c : ℤ√(-3)
hprime : Prime (c.re ^ 2)
hc : c.re ^ 2 = ↑x.natAbs
H : c.im = 0
⊢ False
Tactic:
exact not_prime_pow one_lt_two.ne' hprime
Proof state after:
no goals
Theorem: step1a
Proof state before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
⊢ Odd a.re ∧ Odd a.im
Tactic:
rw [Int.odd_iff_not_even, Int.odd_iff_not_even]
Proof state after:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
⊢ ¬Even a.re ∧ ¬Even a.im
Theorem: step1a
Proof state before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
⊢ ¬Even a.re ∧ ¬Even a.im
Tactic:
have : Even a.re ↔ Even a.im := by
  have : ¬ Even (3 : ℤ) := by decide
  simpa [this, Zsqrtd.norm_def, parity_simps] using heven
Proof state after:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
this : Even a.re ↔ Even a.im
⊢ ¬Even a.re ∧ ¬Even a.im
Theorem: step1a
Proof state before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
this : Even a.re ↔ Even a.im
⊢ ¬Even a.re ∧ ¬Even a.im
Tactic:
apply (iff_iff_and_or_not_and_not.mp this).resolve_left
Proof state after:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
this : Even a.re ↔ Even a.im
⊢ ¬(Even a.re ∧ Even a.im)
Theorem: step1a
Proof state before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
this : Even a.re ↔ Even a.im
⊢ ¬(Even a.re ∧ Even a.im)
Tactic:
rw [even_iff_two_dvd, even_iff_two_dvd]
Proof state after:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
this : Even a.re ↔ Even a.im
⊢ ¬(2 ∣ a.re ∧ 2 ∣ a.im)
Theorem: step1a
Proof state before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
this : Even a.re ↔ Even a.im
⊢ ¬(2 ∣ a.re ∧ 2 ∣ a.im)
Tactic:
rintro ⟨hre, him⟩
Proof state after:
case intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
this : Even a.re ↔ Even a.im
hre : 2 ∣ a.re
him : 2 ∣ a.im
⊢ False
Theorem: step1a
Proof state before:
case intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
this : Even a.re ↔ Even a.im
hre : 2 ∣ a.re
him : 2 ∣ a.im
⊢ False
Tactic:
have := hcoprime.isUnit_of_dvd' hre him
Proof state after:
case intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
this✝ : Even a.re ↔ Even a.im
hre : 2 ∣ a.re
him : 2 ∣ a.im
this : IsUnit 2
⊢ False
Theorem: step1a
Proof state before:
case intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
this✝ : Even a.re ↔ Even a.im
hre : 2 ∣ a.re
him : 2 ∣ a.im
this : IsUnit 2
⊢ False
Tactic:
rw [isUnit_iff_dvd_one] at this
Proof state after:
case intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
this✝ : Even a.re ↔ Even a.im
hre : 2 ∣ a.re
him : 2 ∣ a.im
this : 2 ∣ 1
⊢ False
Theorem: step1a
Proof state before:
case intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
this✝ : Even a.re ↔ Even a.im
hre : 2 ∣ a.re
him : 2 ∣ a.im
this : 2 ∣ 1
⊢ False
Tactic:
norm_num at this
Proof state after:
no goals
Theorem: step1a
Proof state before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
⊢ Even a.re ↔ Even a.im
Tactic:
have : ¬ Even (3 : ℤ) := by decide
Proof state after:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
this : ¬Even 3
⊢ Even a.re ↔ Even a.im
Theorem: step1a
Proof state before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
this : ¬Even 3
⊢ Even a.re ↔ Even a.im
Tactic:
simpa [this, Zsqrtd.norm_def, parity_simps] using heven
Proof state after:
no goals
Theorem: step1a
Proof state before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
⊢ ¬Even 3
Tactic:
decide
Proof state after:
no goals
Theorem: step1
Proof state before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
⊢ ∃ u, a = { re := 1, im := 1 } * u ∨ a = { re := 1, im := -1 } * u
Tactic:
obtain ⟨ha, hb⟩ := step1a hcoprime heven
Proof state after:
case intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
ha : Odd a.re
hb : Odd a.im
⊢ ∃ u, a = { re := 1, im := 1 } * u ∨ a = { re := 1, im := -1 } * u
Theorem: step1
Proof state before:
case intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
ha : Odd a.re
hb : Odd a.im
⊢ ∃ u, a = { re := 1, im := 1 } * u ∨ a = { re := 1, im := -1 } * u
Tactic:
obtain hdvd | hdvd := Int.four_dvd_add_or_sub_of_odd ha hb
Proof state after:
case intro.inl
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
ha : Odd a.re
hb : Odd a.im
hdvd : 4 ∣ a.re + a.im
⊢ ∃ u, a = { re := 1, im := 1 } * u ∨ a = { re := 1, im := -1 } * u

case intro.inr
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
ha : Odd a.re
hb : Odd a.im
hdvd : 4 ∣ a.re - a.im
⊢ ∃ u, a = { re := 1, im := 1 } * u ∨ a = { re := 1, im := -1 } * u
Theorem: step1
Proof state before:
case intro.inl
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
ha : Odd a.re
hb : Odd a.im
hdvd : 4 ∣ a.re + a.im
⊢ ∃ u, a = { re := 1, im := 1 } * u ∨ a = { re := 1, im := -1 } * u
Tactic:
obtain ⟨v, hv⟩ := hdvd
Proof state after:
case intro.inl.intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
ha : Odd a.re
hb : Odd a.im
v : ℤ
hv : a.re + a.im = 4 * v
⊢ ∃ u, a = { re := 1, im := 1 } * u ∨ a = { re := 1, im := -1 } * u
Theorem: step1
Proof state before:
case intro.inl.intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
ha : Odd a.re
hb : Odd a.im
v : ℤ
hv : a.re + a.im = 4 * v
⊢ ∃ u, a = { re := 1, im := 1 } * u ∨ a = { re := 1, im := -1 } * u
Tactic:
rw [← eq_sub_iff_add_eq] at hv
Proof state after:
case intro.inl.intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
ha : Odd a.re
hb : Odd a.im
v : ℤ
hv : a.re = 4 * v - a.im
⊢ ∃ u, a = { re := 1, im := 1 } * u ∨ a = { re := 1, im := -1 } * u
Theorem: step1
Proof state before:
case intro.inl.intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
ha : Odd a.re
hb : Odd a.im
v : ℤ
hv : a.re = 4 * v - a.im
⊢ ∃ u, a = { re := 1, im := 1 } * u ∨ a = { re := 1, im := -1 } * u
Tactic:
use ⟨v - a.im, v⟩
Proof state after:
case h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
ha : Odd a.re
hb : Odd a.im
v : ℤ
hv : a.re = 4 * v - a.im
⊢ a = { re := 1, im := 1 } * { re := v - a.im, im := v } ∨ a = { re := 1, im := -1 } * { re := v - a.im, im := v }
Theorem: step1
Proof state before:
case h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
ha : Odd a.re
hb : Odd a.im
v : ℤ
hv : a.re = 4 * v - a.im
⊢ a = { re := 1, im := 1 } * { re := v - a.im, im := v } ∨ a = { re := 1, im := -1 } * { re := v - a.im, im := v }
Tactic:
right
Proof state after:
case h.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
ha : Odd a.re
hb : Odd a.im
v : ℤ
hv : a.re = 4 * v - a.im
⊢ a = { re := 1, im := -1 } * { re := v - a.im, im := v }
Theorem: step1
Proof state before:
case h.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
ha : Odd a.re
hb : Odd a.im
v : ℤ
hv : a.re = 4 * v - a.im
⊢ a = { re := 1, im := -1 } * { re := v - a.im, im := v }
Tactic:
rw [Zsqrtd.ext_iff, hv, Zsqrtd.mul_re, Zsqrtd.mul_im]
Proof state after:
case h.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
ha : Odd a.re
hb : Odd a.im
v : ℤ
hv : a.re = 4 * v - a.im
⊢ 4 * v - a.im =
      { re := 1, im := -1 }.re * { re := v - a.im, im := v }.re +
        -3 * { re := 1, im := -1 }.im * { re := v - a.im, im := v }.im ∧
    a.im =
      { re := 1, im := -1 }.re * { re := v - a.im, im := v }.im +
        { re := 1, im := -1 }.im * { re := v - a.im, im := v }.re