internlm/Lean-Github huggingface dataset:
Theorem: Int.factor_div
Proof state before:
case neg.refine'_2
a x : ℤ
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑(natAbs x) ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < abs x
heqtwomul : ↑(natAbs x) = 2 * (a % x)
⊢ ¬Odd x
Tactic:
rw [← Int.even_iff_not_odd, ← Int.natAbs_even, ← Int.even_coe_nat, even_iff_two_dvd]
Proof state after:
case neg.refine'_2
a x : ℤ
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑(natAbs x) ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < abs x
heqtwomul : ↑(natAbs x) = 2 * (a % x)
⊢ 2 ∣ ↑(natAbs x)
Theorem: Int.factor_div
Proof state before:
case neg.refine'_2
a x : ℤ
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑(natAbs x) ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < abs x
heqtwomul : ↑(natAbs x) = 2 * (a % x)
⊢ 2 ∣ ↑(natAbs x)
Tactic:
exact ⟨_, heqtwomul⟩
Proof state after:
no goals
Theorem: two_not_cube
Proof state before:
r : ℕ
⊢ r ^ 3 ≠ 2
Tactic:
have : 1 ≤ 3 := by norm_num
Proof state after:
r : ℕ
this : 1 ≤ 3
⊢ r ^ 3 ≠ 2
Theorem: two_not_cube
Proof state before:
r : ℕ
this : 1 ≤ 3
⊢ r ^ 3 ≠ 2
Tactic:
apply Monotone.ne_of_lt_of_lt_nat (Nat.pow_left_strictMono this).monotone 1 <;> norm_num
Proof state after:
no goals
Theorem: two_not_cube
Proof state before:
r : ℕ
⊢ 1 ≤ 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: Int.two_not_cube
Proof state before:
r : ℤ
H : r ^ 3 = 2
⊢ False
Tactic:
apply two_not_cube r.natAbs
Proof state after:
r : ℤ
H : r ^ 3 = 2
⊢ natAbs r ^ 3 = 2
Theorem: Int.two_not_cube
Proof state before:
r : ℤ
H : r ^ 3 = 2
⊢ natAbs r ^ 3 = 2
Tactic:
rw [← Int.natAbs_pow, H]
Proof state after:
r : ℤ
H : r ^ 3 = 2
⊢ natAbs 2 = 2
Theorem: Zsqrtd.exists
Proof state before:
d : ℤ
a : ℤ√d
him : a.im ≠ 0
⊢ ∃ c, norm a = norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0
Tactic:
cases' le_or_lt a.re 0 with hre hre
Proof state after:
case inl
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : a.re ≤ 0
⊢ ∃ c, norm a = norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0

case inr
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : 0 < a.re
⊢ ∃ c, norm a = norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0
Theorem: Zsqrtd.exists
Proof state before:
case inl
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : a.re ≤ 0
⊢ ∃ c, norm a = norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0
Tactic:
use -a
Proof state after:
case inl
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : a.re ≤ 0
⊢ norm a = norm (-a) ∧ 0 ≤ (-a).re ∧ (-a).im ≠ 0
Theorem: Zsqrtd.exists
Proof state before:
case inl
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : a.re ≤ 0
⊢ norm a = norm (-a) ∧ 0 ≤ (-a).re ∧ (-a).im ≠ 0
Tactic:
simp only [hre, him, Zsqrtd.norm_neg, eq_self_iff_true, Zsqrtd.neg_im, Zsqrtd.neg_re,
  and_self_iff, neg_nonneg, Ne.def, not_false_iff, neg_eq_zero]
Proof state after:
no goals
Theorem: Zsqrtd.exists
Proof state before:
case inr
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : 0 < a.re
⊢ ∃ c, norm a = norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0
Tactic:
use a
Proof state after:
case inr
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : 0 < a.re
⊢ norm a = norm a ∧ 0 ≤ a.re ∧ a.im ≠ 0
Theorem: Zsqrtd.exists
Proof state before:
case inr
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : 0 < a.re
⊢ norm a = norm a ∧ 0 ≤ a.re ∧ a.im ≠ 0
Tactic:
simp only [hre.le, him, eq_self_iff_true, and_self_iff, Ne.def, not_false_iff]
Proof state after:
no goals
Theorem: factors2
Proof state before:
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
Tactic:
have hparity : Even a.re ↔ Even a.im := by
  simpa [two_ne_zero, Zsqrtd.norm_def, parity_simps] using heven
Proof state after:
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hparity : Even a.re ↔ Even a.im
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
Theorem: factors2
Proof state before:
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hparity : Even a.re ↔ Even a.im
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
Tactic:
simp only [iff_iff_and_or_not_and_not, ← Int.odd_iff_not_even] at hparity
Proof state after:
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hparity : Even a.re ∧ Even a.im ∨ Odd a.re ∧ Odd a.im
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
Theorem: factors2
Proof state before:
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hparity : Even a.re ∧ Even a.im ∨ Odd a.re ∧ Odd a.im
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
Tactic:
obtain ⟨⟨c, hc⟩, ⟨d, hd⟩⟩ | ⟨hre, him⟩ := hparity
Proof state after:
case inl.intro.intro.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
c : ℤ
hc : a.re = c + c
d : ℤ
hd : a.im = d + d
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b

case inr.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
Theorem: factors2
Proof state before:
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
⊢ Even a.re ↔ Even a.im
Tactic:
simpa [two_ne_zero, Zsqrtd.norm_def, parity_simps] using heven
Proof state after:
no goals
Theorem: factors2
Proof state before:
case inl.intro.intro.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
c : ℤ
hc : a.re = c + c
d : ℤ
hd : a.im = d + d
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
Tactic:
use ⟨c, d⟩
Proof state after:
case inl.intro.intro.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
c : ℤ
hc : a.re = c + c
d : ℤ
hd : a.im = d + d
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm { re := c, im := d }
Theorem: factors2
Proof state before:
case inl.intro.intro.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
c : ℤ
hc : a.re = c + c
d : ℤ
hd : a.im = d + d
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm { re := c, im := d }
Tactic:
simp only [Zsqrtd.norm_def, hc, hd]
Proof state after:
case inl.intro.intro.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
c : ℤ
hc : a.re = c + c
d : ℤ
hd : a.im = d + d
⊢ (c + c) * (c + c) - -3 * (d + d) * (d + d) = 4 * (c * c - -3 * d * d)
Theorem: factors2
Proof state before:
case inl.intro.intro.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
c : ℤ
hc : a.re = c + c
d : ℤ
hd : a.im = d + d
⊢ (c + c) * (c + c) - -3 * (d + d) * (d + d) = 4 * (c * c - -3 * d * d)
Tactic:
ring
Proof state after:
no goals
Theorem: factors2
Proof state before:
case inr.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
Tactic:
cases' Int.four_dvd_add_or_sub_of_odd hre him with h4 h4
Proof state after:
case inr.intro.inl
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
h4 : 4 ∣ a.re + a.im
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b

case inr.intro.inr
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
h4 : 4 ∣ a.re - a.im
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
Theorem: factors2
Proof state before:
case inr.intro.inl
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
h4 : 4 ∣ a.re + a.im
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
Tactic:
obtain ⟨v, hv⟩ := h4
Proof state after:
case inr.intro.inl.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re + a.im = 4 * v
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
Theorem: factors2
Proof state before:
case inr.intro.inl.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re + a.im = 4 * v
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
Tactic:
use ⟨v - a.im, v⟩
Proof state after:
case inr.intro.inl.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re + a.im = 4 * v
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm { re := v - a.im, im := v }
Theorem: factors2
Proof state before:
case inr.intro.inl.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re + a.im = 4 * v
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm { re := v - a.im, im := v }
Tactic:
rw [eq_comm, ← sub_eq_iff_eq_add] at hv
Proof state after:
case inr.intro.inl.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : 4 * v - a.im = a.re
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm { re := v - a.im, im := v }
Theorem: factors2
Proof state before:
case inr.intro.inl.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : 4 * v - a.im = a.re
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm { re := v - a.im, im := v }
Tactic:
simp only [Zsqrtd.norm_def, ← hv]
Proof state after:
case inr.intro.inl.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : 4 * v - a.im = a.re
⊢ (4 * v - a.im) * (4 * v - a.im) - -3 * a.im * a.im = 4 * ((v - a.im) * (v - a.im) - -3 * v * v)
Theorem: factors2
Proof state before:
case inr.intro.inl.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : 4 * v - a.im = a.re
⊢ (4 * v - a.im) * (4 * v - a.im) - -3 * a.im * a.im = 4 * ((v - a.im) * (v - a.im) - -3 * v * v)
Tactic:
ring
Proof state after:
no goals
Theorem: factors2
Proof state before:
case inr.intro.inr
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
h4 : 4 ∣ a.re - a.im
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
Tactic:
obtain ⟨v, hv⟩ := h4
Proof state after:
case inr.intro.inr.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re - a.im = 4 * v
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
Theorem: factors2
Proof state before:
case inr.intro.inr.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re - a.im = 4 * v
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
Tactic:
use ⟨v + a.im, v⟩
Proof state after:
case inr.intro.inr.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re - a.im = 4 * v
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm { re := v + a.im, im := v }
Theorem: factors2
Proof state before:
case inr.intro.inr.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re - a.im = 4 * v
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm { re := v + a.im, im := v }
Tactic:
rw [sub_eq_iff_eq_add] at hv
Proof state after:
case inr.intro.inr.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re = 4 * v + a.im
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm { re := v + a.im, im := v }
Theorem: factors2
Proof state before:
case inr.intro.inr.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re = 4 * v + a.im
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm { re := v + a.im, im := v }
Tactic:
simp only [Zsqrtd.norm_def, hv]
Proof state after:
case inr.intro.inr.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re = 4 * v + a.im
⊢ (4 * v + a.im) * (4 * v + a.im) - -3 * a.im * a.im = 4 * ((v + a.im) * (v + a.im) - -3 * v * v)
Theorem: factors2
Proof state before:
case inr.intro.inr.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re = 4 * v + a.im
⊢ (4 * v + a.im) * (4 * v + a.im) - -3 * a.im * a.im = 4 * ((v + a.im) * (v + a.im) - -3 * v * v)
Tactic:
ring
Proof state after:
no goals
Theorem: Spts.mul_of_dvd'
Proof state before:
a p : ℤ√(-3)
hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm a
hpprime : Prime (Zsqrtd.norm p)
⊢ ∃ u, a = p * u ∨ a = star p * u
Tactic:
obtain ⟨f, hf⟩ := hdvd
Proof state after:
case intro
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
⊢ ∃ u, a = p * u ∨ a = star p * u
Theorem: Spts.mul_of_dvd'
Proof state before:
case intro
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im ∨ Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
⊢ ∃ u, a = p * u ∨ a = star p * u
Tactic:
obtain ⟨A, HA⟩ : ∃ A : Units ℤ, p.norm ∣ p.re * a.im + A * a.re * p.im := by
  cases' h0 with h0 h0 <;> [(use -1), (use 1)] <;> convert h0 using 1 <;>
    simp only [Units.val_neg, Units.val_one, neg_mul, one_mul]
  ring
Proof state after:
case intro.intro
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im ∨ Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : Zsqrtd.norm p ∣ p.re * a.im + ↑A * a.re * p.im
⊢ ∃ u, a = p * u ∨ a = star p * u
Theorem: Spts.mul_of_dvd'
Proof state before:
case intro.intro
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im ∨ Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : Zsqrtd.norm p ∣ p.re * a.im + ↑A * a.re * p.im
⊢ ∃ u, a = p * u ∨ a = star p * u
Tactic:
have HAsq : (A : ℤ) ^ 2 = 1 := by
  calc
    (A : ℤ) ^ 2 = ((A ^ 2 : Units ℤ) : ℤ) := (Units.val_pow_eq_pow_val _ _).symm
    _ = ((1 : Units ℤ) : ℤ) := (congr_arg _ (Int.units_sq A))
    _ = 1 := Units.val_one
Proof state after:
case intro.intro
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im ∨ Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : Zsqrtd.norm p ∣ p.re * a.im + ↑A * a.re * p.im
HAsq : ↑A ^ 2 = 1
⊢ ∃ u, a = p * u ∨ a = star p * u
Theorem: Spts.mul_of_dvd'
Proof state before:
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
⊢ Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im ∨ Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
Tactic:
apply hpprime.dvd_or_dvd
Proof state after:
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
⊢ Zsqrtd.norm p ∣ (p.re * a.im - a.re * p.im) * (p.re * a.im + a.re * p.im)
Theorem: Spts.mul_of_dvd'
Proof state before:
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
⊢ Zsqrtd.norm p ∣ (p.re * a.im - a.re * p.im) * (p.re * a.im + a.re * p.im)
Tactic:
convert dvd_mul_right p.norm (a.im ^ 2 - p.im ^ 2 * f) using 1
Proof state after:
case h.e'_4
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
⊢ (p.re * a.im - a.re * p.im) * (p.re * a.im + a.re * p.im) = Zsqrtd.norm p * (a.im ^ 2 - p.im ^ 2 * f)
Theorem: Spts.mul_of_dvd'
Proof state before:
case h.e'_4
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
⊢ (p.re * a.im - a.re * p.im) * (p.re * a.im + a.re * p.im) = Zsqrtd.norm p * (a.im ^ 2 - p.im ^ 2 * f)
Tactic:
trans a.im ^ 2 * p.norm - p.im ^ 2 * (p.norm * f)
Proof state after:
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
⊢ (p.re * a.im - a.re * p.im) * (p.re * a.im + a.re * p.im) = a.im ^ 2 * Zsqrtd.norm p - p.im ^ 2 * (Zsqrtd.norm p * f)

a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
⊢ a.im ^ 2 * Zsqrtd.norm p - p.im ^ 2 * (Zsqrtd.norm p * f) = Zsqrtd.norm p * (a.im ^ 2 - p.im ^ 2 * f)
Theorem: Spts.mul_of_dvd'
Proof state before:
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
⊢ (p.re * a.im - a.re * p.im) * (p.re * a.im + a.re * p.im) = a.im ^ 2 * Zsqrtd.norm p - p.im ^ 2 * (Zsqrtd.norm p * f)
Tactic:
rw [← hf, Zsqrtd.norm_def, Zsqrtd.norm_def]
Proof state after:
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
⊢ (p.re * a.im - a.re * p.im) * (p.re * a.im + a.re * p.im) =
    a.im ^ 2 * (p.re * p.re - -3 * p.im * p.im) - p.im ^ 2 * (a.re * a.re - -3 * a.im * a.im)
Theorem: Spts.mul_of_dvd'
Proof state before:
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
⊢ (p.re * a.im - a.re * p.im) * (p.re * a.im + a.re * p.im) =
    a.im ^ 2 * (p.re * p.re - -3 * p.im * p.im) - p.im ^ 2 * (a.re * a.re - -3 * a.im * a.im)
Tactic:
ring
Proof state after:
no goals
Theorem: Spts.mul_of_dvd'
Proof state before:
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
⊢ a.im ^ 2 * Zsqrtd.norm p - p.im ^ 2 * (Zsqrtd.norm p * f) = Zsqrtd.norm p * (a.im ^ 2 - p.im ^ 2 * f)
Tactic:
rw [Zsqrtd.norm_def]
Proof state after:
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
⊢ a.im ^ 2 * (p.re * p.re - -3 * p.im * p.im) - p.im ^ 2 * ((p.re * p.re - -3 * p.im * p.im) * f) =
    (p.re * p.re - -3 * p.im * p.im) * (a.im ^ 2 - p.im ^ 2 * f)
Theorem: Spts.mul_of_dvd'
Proof state before:
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
⊢ a.im ^ 2 * (p.re * p.re - -3 * p.im * p.im) - p.im ^ 2 * ((p.re * p.re - -3 * p.im * p.im) * f) =
    (p.re * p.re - -3 * p.im * p.im) * (a.im ^ 2 - p.im ^ 2 * f)
Tactic:
ring
Proof state after:
no goals
Theorem: Spts.mul_of_dvd'
Proof state before:
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im ∨ Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
⊢ ∃ A, Zsqrtd.norm p ∣ p.re * a.im + ↑A * a.re * p.im
Tactic:
cases' h0 with h0 h0 <;> [(use -1), (use 1)] <;> convert h0 using 1 <;>
  simp only [Units.val_neg, Units.val_one, neg_mul, one_mul]
Proof state after:
case h.e'_4
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im
⊢ p.re * a.im + -(a.re * p.im) = p.re * a.im - a.re * p.im
Theorem: Spts.mul_of_dvd'
Proof state before:
case h.e'_4
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im
⊢ p.re * a.im + -(a.re * p.im) = p.re * a.im - a.re * p.im
Tactic:
ring
Proof state after:
no goals
Theorem: Spts.mul_of_dvd'
Proof state before:
case inl
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im
⊢ ∃ A, Zsqrtd.norm p ∣ p.re * a.im + ↑A * a.re * p.im
Tactic:
use -1
Proof state after:
case inl
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im
⊢ Zsqrtd.norm p ∣ p.re * a.im + ↑(-1) * a.re * p.im
Theorem: Spts.mul_of_dvd'
Proof state before:
case inr
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
⊢ ∃ A, Zsqrtd.norm p ∣ p.re * a.im + ↑A * a.re * p.im
Tactic:
use 1
Proof state after:
case inr
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
⊢ Zsqrtd.norm p ∣ p.re * a.im + ↑1 * a.re * p.im
Theorem: Spts.mul_of_dvd'
Proof state before:
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im ∨ Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : Zsqrtd.norm p ∣ p.re * a.im + ↑A * a.re * p.im
⊢ ↑A ^ 2 = 1
Tactic:
calc
  (A : ℤ) ^ 2 = ((A ^ 2 : Units ℤ) : ℤ) := (Units.val_pow_eq_pow_val _ _).symm
  _ = ((1 : Units ℤ) : ℤ) := (congr_arg _ (Int.units_sq A))
  _ = 1 := Units.val_one
Proof state after:
no goals
Theorem: Spts.mul_of_dvd'
Proof state before:
case intro.intro
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im ∨ Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : Zsqrtd.norm p ∣ p.re * a.im + ↑A * a.re * p.im
HAsq : ↑A ^ 2 = 1
⊢ ∃ u, a = p * u ∨ a = star p * u
Tactic:
set X : ℤ√(-3) := ⟨p.re * a.re - A * 3 * p.im * a.im, p.re * a.im + A * a.re * p.im⟩ with HX
Proof state after:
case intro.intro
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im ∨ Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : Zsqrtd.norm p ∣ p.re * a.im + ↑A * a.re * p.im
HAsq : ↑A ^ 2 = 1
X : ℤ√(-3) := { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
HX : X = { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
⊢ ∃ u, a = p * u ∨ a = star p * u
Theorem: Spts.mul_of_dvd'
Proof state before:
case intro.intro.intro
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im ∨ Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : Zsqrtd.norm p ∣ p.re * a.im + ↑A * a.re * p.im
HAsq : ↑A ^ 2 = 1
X : ℤ√(-3) := { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
HX : X = { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
U : ℤ√(-3)
HU : X = ↑(Zsqrtd.norm p) * U
⊢ ∃ u, a = p * u ∨ a = star p * u
Tactic:
use U
Proof state after:
case intro.intro.intro
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im ∨ Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : Zsqrtd.norm p ∣ p.re * a.im + ↑A * a.re * p.im
HAsq : ↑A ^ 2 = 1
X : ℤ√(-3) := { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
HX : X = { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
U : ℤ√(-3)
HU : X = ↑(Zsqrtd.norm p) * U
⊢ a = p * U ∨ a = star p * U
Theorem: Spts.mul_of_dvd'
Proof state before:
case intro.intro.intro
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im ∨ Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : Zsqrtd.norm p ∣ p.re * a.im + ↑A * a.re * p.im
HAsq : ↑A ^ 2 = 1
X : ℤ√(-3) := { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
HX : X = { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
U : ℤ√(-3)
HU : X = ↑(Zsqrtd.norm p) * U
⊢ a = p * U ∨ a = star p * U
Tactic:
suffices a = ⟨p.re, -A * p.im⟩ * U by
  apply Or.imp _ _ (Int.units_eq_one_or A).symm <;> rintro rfl <;> simpa [Zsqrtd.ext] using this
Proof state after:
case intro.intro.intro
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im ∨ Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : Zsqrtd.norm p ∣ p.re * a.im + ↑A * a.re * p.im
HAsq : ↑A ^ 2 = 1
X : ℤ√(-3) := { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
HX : X = { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
U : ℤ√(-3)
HU : X = ↑(Zsqrtd.norm p) * U
⊢ a = { re := p.re, im := -↑A * p.im } * U
Theorem: Spts.mul_of_dvd'
Proof state before:
case intro.intro.intro
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im ∨ Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : Zsqrtd.norm p ∣ p.re * a.im + ↑A * a.re * p.im
HAsq : ↑A ^ 2 = 1
X : ℤ√(-3) := { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
HX : X = { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
U : ℤ√(-3)
HU : X = ↑(Zsqrtd.norm p) * U
⊢ a = { re := p.re, im := -↑A * p.im } * U
Tactic:
apply Zsqrtd.eq_of_smul_eq_smul_left hpprime.ne_zero
Proof state after:
case intro.intro.intro
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im ∨ Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : Zsqrtd.norm p ∣ p.re * a.im + ↑A * a.re * p.im
HAsq : ↑A ^ 2 = 1
X : ℤ√(-3) := { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
HX : X = { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
U : ℤ√(-3)
HU : X = ↑(Zsqrtd.norm p) * U
⊢ ↑(Zsqrtd.norm p) * a = ↑(Zsqrtd.norm p) * ({ re := p.re, im := -↑A * p.im } * U)