internlm/Lean-Github huggingface dataset:
Theorem: N.zero_add
Proof state before:
case succ
S : Type
image_zero : S
image_succ : N → S → S
n m a b c i : N
hi : 0 + i = i
⊢ 0 + succ i = succ i
Tactic:
rw [add_succ, hi]
Proof state after:
no goals
Theorem: N.zero_add'
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ zero + a = a
Tactic:
induction a with
| zero =>
  rw [add_zero']
| succ n hn =>
  rw [add_succ, hn]
Proof state after:
no goals
Theorem: N.zero_add'
Proof state before:
case zero
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ zero + zero = zero
Tactic:
rw [add_zero']
Proof state after:
no goals
Theorem: N.zero_add'
Proof state before:
case succ
S : Type
image_zero : S
image_succ : N → S → S
n✝ m a b c n : N
hn : zero + n = n
⊢ zero + succ n = succ n
Tactic:
rw [add_succ, hn]
Proof state after:
no goals
Theorem: N.add_assoc
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ a + b + c = a + (b + c)
Tactic:
induction c with
| zero =>
  change a + b + 0 = a + (b + 0)
  rw [add_zero, add_zero]
| succ c hrec =>
  rw [add_succ, add_succ, add_succ, hrec]
Proof state after:
no goals
Theorem: N.add_assoc
Proof state before:
case zero
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ a + b + zero = a + (b + zero)
Tactic:
change a + b + 0 = a + (b + 0)
Proof state after:
case zero
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ a + b + 0 = a + (b + 0)
Theorem: N.add_assoc
Proof state before:
case zero
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ a + b + 0 = a + (b + 0)
Tactic:
rw [add_zero, add_zero]
Proof state after:
no goals
Theorem: N.add_assoc
Proof state before:
case succ
S : Type
image_zero : S
image_succ : N → S → S
n m a b c✝ c : N
hrec : a + b + c = a + (b + c)
⊢ a + b + succ c = a + (b + succ c)
Tactic:
rw [add_succ, add_succ, add_succ, hrec]
Proof state after:
no goals
Theorem: N.succ_add
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ succ a + b = succ (a + b)
Tactic:
induction b with
| zero =>
  rfl
| succ b hb =>
  rw [add_succ, add_succ, hb]
Proof state after:
no goals
Theorem: N.succ_add
Proof state before:
case zero
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ succ a + zero = succ (a + zero)
Tactic:
rfl
Proof state after:
no goals
Theorem: N.succ_add
Proof state before:
case succ
S : Type
image_zero : S
image_succ : N → S → S
n m a b✝ c b : N
hb : succ a + b = succ (a + b)
⊢ succ a + succ b = succ (a + succ b)
Tactic:
rw [add_succ, add_succ, hb]
Proof state after:
no goals
Theorem: N.add_comm
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ a + b = b + a
Tactic:
induction a with
| zero =>
rw [zero_add',add_zero']
| succ a hrec =>
rw [succ_add,add_succ,hrec]
done
Proof state after:
no goals
Theorem: N.add_comm
Proof state before:
case zero
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ zero + b = b + zero
Tactic:
rw [zero_add',add_zero']
Proof state after:
no goals
Theorem: N.add_comm
Proof state before:
case succ
S : Type
image_zero : S
image_succ : N → S → S
n m a✝ b c a : N
hrec : a + b = b + a
⊢ succ a + b = b + succ a
Tactic:
rw [succ_add,add_succ,hrec]
Proof state after:
no goals
Theorem: N.succ_eq_add_one
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ succ a = a + 1
Tactic:
rw [one_eq_succ_zero, add_succ, add_zero]
Proof state after:
no goals
Theorem: N.add_right_comm
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ a + b + c = a + c + b
Tactic:
rw [add_assoc, add_comm b c, ← add_assoc]
Proof state after:
no goals
Theorem: N.zero_mul
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ 0 * a = 0
Tactic:
induction a with
| zero =>
  change 0 * 0 = _
  rw [mul_zero]
| succ n hn =>
  rw [mul_succ, hn, add_zero]
Proof state after:
no goals
Theorem: N.zero_mul
Proof state before:
case zero
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ 0 * zero = 0
Tactic:
change 0 * 0 = _
Proof state after:
case zero
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ 0 * 0 = 0
Theorem: N.zero_mul
Proof state before:
case zero
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ 0 * 0 = 0
Tactic:
rw [mul_zero]
Proof state after:
no goals
Theorem: N.zero_mul
Proof state before:
case succ
S : Type
image_zero : S
image_succ : N → S → S
a b c n : N
hn : 0 * n = 0
⊢ 0 * succ n = 0
Tactic:
rw [mul_succ, hn, add_zero]
Proof state after:
no goals
Theorem: N.mul_one
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a * 1 = a
Tactic:
rw [one_eq_succ_zero, mul_succ, mul_zero, zero_add]
Proof state after:
no goals
Theorem: N.one_mul
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ 1 * a = a
Tactic:
induction a with
| zero => rfl
| succ n hn =>
  rw [mul_succ, hn, one_eq_succ_zero, add_succ, add_zero]
Proof state after:
no goals
Theorem: N.one_mul
Proof state before:
case zero
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ 1 * zero = zero
Tactic:
rfl
Proof state after:
no goals
Theorem: N.one_mul
Proof state before:
case succ
S : Type
image_zero : S
image_succ : N → S → S
a b c n : N
hn : 1 * n = n
⊢ 1 * succ n = succ n
Tactic:
rw [mul_succ, hn, one_eq_succ_zero, add_succ, add_zero]
Proof state after:
no goals
Theorem: N.mul_add
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a * (b + c) = a * b + a * c
Tactic:
induction b with
| zero =>
  change a * (0 + c) = a * 0 + a * c
  rw [zero_add, mul_zero, zero_add]
| succ n hn =>
  rw [succ_add, mul_succ, hn, mul_succ, add_assoc, add_comm (a*c), add_assoc]
Proof state after:
no goals
Theorem: N.mul_add
Proof state before:
case zero
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a * (zero + c) = a * zero + a * c
Tactic:
change a * (0 + c) = a * 0 + a * c
Proof state after:
case zero
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a * (0 + c) = a * 0 + a * c
Theorem: N.mul_add
Proof state before:
case zero
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a * (0 + c) = a * 0 + a * c
Tactic:
rw [zero_add, mul_zero, zero_add]
Proof state after:
no goals
Theorem: N.mul_add
Proof state before:
case succ
S : Type
image_zero : S
image_succ : N → S → S
a b c n : N
hn : a * (n + c) = a * n + a * c
⊢ a * (succ n + c) = a * succ n + a * c
Tactic:
rw [succ_add, mul_succ, hn, mul_succ, add_assoc, add_comm (a*c), add_assoc]
Proof state after:
no goals
Theorem: N.mul_assoc
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a * b * c = a * (b * c)
Tactic:
induction c with
| zero =>
  rfl
| succ n hn =>
  rw [mul_succ, hn, mul_succ, mul_add]
Proof state after:
no goals
Theorem: N.mul_assoc
Proof state before:
case zero
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a * b * zero = a * (b * zero)
Tactic:
rfl
Proof state after:
no goals
Theorem: N.mul_assoc
Proof state before:
case succ
S : Type
image_zero : S
image_succ : N → S → S
a b c n : N
hn : a * b * n = a * (b * n)
⊢ a * b * succ n = a * (b * succ n)
Tactic:
rw [mul_succ, hn, mul_succ, mul_add]
Proof state after:
no goals
Theorem: N.succ_mul
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ succ a * b = a * b + b
Tactic:
induction b with
| zero => rfl
| succ n hn =>
  rw [mul_succ, mul_succ, hn, add_assoc, add_assoc, add_succ,
    add_succ, add_succ, add_succ, add_comm n a]
Proof state after:
no goals
Theorem: N.succ_mul
Proof state before:
case zero
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ succ a * zero = a * zero + zero
Tactic:
rfl
Proof state after:
no goals
Theorem: N.succ_mul
Proof state before:
case succ
S : Type
image_zero : S
image_succ : N → S → S
a b c n : N
hn : succ a * n = a * n + n
⊢ succ a * succ n = a * succ n + succ n
Tactic:
rw [mul_succ, mul_succ, hn, add_assoc, add_assoc, add_succ,
  add_succ, add_succ, add_succ, add_comm n a]
Proof state after:
no goals
Theorem: N.add_mul
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ (a + b) * c = a * c + b * c
Tactic:
induction c with
| zero => rfl
| succ n hn =>
  rw [mul_succ, mul_succ, hn, mul_succ, add_assoc, add_assoc]
  congr 1
  rw [← add_assoc, add_comm _ a, add_assoc]
Proof state after:
no goals
Theorem: N.add_mul
Proof state before:
case zero
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ (a + b) * zero = a * zero + b * zero
Tactic:
rfl
Proof state after:
no goals
Theorem: N.add_mul
Proof state before:
case succ
S : Type
image_zero : S
image_succ : N → S → S
a b c n : N
hn : (a + b) * n = a * n + b * n
⊢ (a + b) * succ n = a * succ n + b * succ n
Tactic:
rw [mul_succ, mul_succ, hn, mul_succ, add_assoc, add_assoc]
Proof state after:
case succ
S : Type
image_zero : S
image_succ : N → S → S
a b c n : N
hn : (a + b) * n = a * n + b * n
⊢ a * n + (b * n + (a + b)) = a * n + (a + (b * n + b))
Theorem: N.add_mul
Proof state before:
case succ
S : Type
image_zero : S
image_succ : N → S → S
a b c n : N
hn : (a + b) * n = a * n + b * n
⊢ a * n + (b * n + (a + b)) = a * n + (a + (b * n + b))
Tactic:
congr 1
Proof state after:
case succ.e_a
S : Type
image_zero : S
image_succ : N → S → S
a b c n : N
hn : (a + b) * n = a * n + b * n
⊢ b * n + (a + b) = a + (b * n + b)
Theorem: N.add_mul
Proof state before:
case succ.e_a
S : Type
image_zero : S
image_succ : N → S → S
a b c n : N
hn : (a + b) * n = a * n + b * n
⊢ b * n + (a + b) = a + (b * n + b)
Tactic:
rw [← add_assoc, add_comm _ a, add_assoc]
Proof state after:
no goals
Theorem: N.mul_comm
Proof state before:
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a * b = b * a
Tactic:
induction a with
| zero =>
  change 0 * b = a * 0
  rw [zero_mul, mul_zero]
| succ n hn =>
  rw [succ_mul, hn, mul_succ]
Proof state after:
no goals
Theorem: N.mul_comm
Proof state before:
case zero
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ zero * b = b * zero
Tactic:
change 0 * b = a * 0
Proof state after:
case zero
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ 0 * b = a * 0
Theorem: N.mul_comm
Proof state before:
case zero
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ 0 * b = a * 0
Tactic:
rw [zero_mul, mul_zero]
Proof state after:
no goals
Theorem: N.mul_comm
Proof state before:
case succ
S : Type
image_zero : S
image_succ : N → S → S
a b c n : N
hn : n * b = b * n
⊢ succ n * b = b * succ n
Tactic:
rw [succ_mul, hn, mul_succ]
Proof state after:
no goals
Theorem: Zsqrtd.associated_norm_of_associated
Proof state before:
d : ℤ
f g : ℤ√d
h : Associated f g
⊢ Associated (norm f) (norm g)
Tactic:
obtain ⟨u, rfl⟩ := h
Proof state after:
case intro
d : ℤ
f : ℤ√d
u : (ℤ√d)ˣ
⊢ Associated (norm f) (norm (f * ↑u))
Theorem: Zsqrtd.associated_norm_of_associated
Proof state before:
case intro
d : ℤ
f : ℤ√d
u : (ℤ√d)ˣ
⊢ Associated (norm f) (norm (f * ↑u))
Tactic:
have := (Zsqrtd.isUnit_iff_norm_isUnit u).mp u.isUnit
Proof state after:
case intro
d : ℤ
f : ℤ√d
u : (ℤ√d)ˣ
this : IsUnit (norm ↑u)
⊢ Associated (norm f) (norm (f * ↑u))
Theorem: Zsqrtd.associated_norm_of_associated
Proof state before:
case intro
d : ℤ
f : ℤ√d
u : (ℤ√d)ˣ
this : IsUnit (norm ↑u)
⊢ Associated (norm f) (norm (f * ↑u))
Tactic:
rw [Zsqrtd.norm_mul]
Proof state after:
case intro
d : ℤ
f : ℤ√d
u : (ℤ√d)ˣ
this : IsUnit (norm ↑u)
⊢ Associated (norm f) (norm f * norm ↑u)
Theorem: Zsqrtd.associated_norm_of_associated
Proof state before:
case intro
d : ℤ
f : ℤ√d
u : (ℤ√d)ˣ
this : IsUnit (norm ↑u)
⊢ Associated (norm f) (norm f * norm ↑u)
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 (Zsqrtd.norm p)
hcoprime : IsCoprime p.re p.im
⊢ p.im ≠ 0
Tactic:
intro H
Proof state after:
p : ℤ√(-3)
h : OddPrimeOrFour (Zsqrtd.norm p)
hcoprime : IsCoprime p.re p.im
H : p.im = 0
⊢ False
Theorem: OddPrimeOrFour.im_ne_zero
Proof state before:
p : ℤ√(-3)
h : OddPrimeOrFour (Zsqrtd.norm p)
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)
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)
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 = 4
⊢ False

case inr.intro
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
H : p.im = 0
hp : Prime (p.re ^ 2)
⊢ 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 = 4
⊢ False
Tactic:
rw [H, isCoprime_zero_right, Int.isUnit_iff_abs_eq] at hcoprime
Proof state after:
case inl
p : ℤ√(-3)
hcoprime : Abs.abs p.re = 1
H : p.im = 0
h : p.re ^ 2 = 4
⊢ False
Theorem: OddPrimeOrFour.im_ne_zero
Proof state before:
case inl
p : ℤ√(-3)
hcoprime : Abs.abs p.re = 1
H : p.im = 0
h : p.re ^ 2 = 4
⊢ False
Tactic:
rw [← sq_abs, hcoprime] at h
Proof state after:
case inl
p : ℤ√(-3)
hcoprime : Abs.abs p.re = 1
H : p.im = 0
h : 1 ^ 2 = 4
⊢ False
Theorem: OddPrimeOrFour.im_ne_zero
Proof state before:
case inl
p : ℤ√(-3)
hcoprime : Abs.abs p.re = 1
H : p.im = 0
h : 1 ^ 2 = 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 : Prime (p.re ^ 2)
⊢ False
Tactic:
exact pow_not_prime one_lt_two.ne' hp
Proof state after:
no goals
Theorem: Zsqrt3.isUnit_iff
Proof state before:
z : ℤ√(-3)
⊢ IsUnit z ↔ abs z.re = 1 ∧ z.im = 0
Tactic:
rw [← Zsqrtd.norm_eq_one_iff, ← Int.coe_nat_inj', Int.ofNat_one,
  Int.natAbs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) z)]
Proof state after:
z : ℤ√(-3)
⊢ Zsqrtd.norm z = 1 ↔ abs z.re = 1 ∧ z.im = 0
Theorem: Zsqrt3.isUnit_iff
Proof state before:
z : ℤ√(-3)
⊢ Zsqrtd.norm z = 1 ↔ abs z.re = 1 ∧ z.im = 0
Tactic:
refine' ⟨Spts.eq_one, fun h => _⟩
Proof state after:
z : ℤ√(-3)
h : abs z.re = 1 ∧ z.im = 0
⊢ Zsqrtd.norm z = 1
Theorem: Zsqrt3.isUnit_iff
Proof state before:
z : ℤ√(-3)
h : abs z.re = 1 ∧ z.im = 0
⊢ Zsqrtd.norm z = 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.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 : abs 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 : abs 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 : abs 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 : abs z.re = 1
hu : z.im = 0
v : ℤˣ
hv : ↑v = z.re
⊢ ∃ u, z = ↑↑u
Tactic:
use v
Proof state after:
case intro.intro
z : ℤ√(-3)
h : IsUnit z
u : abs z.re = 1
hu : z.im = 0
v : ℤˣ
hv : ↑v = z.re
⊢ z = ↑↑v
Theorem: Zsqrt3.coe_of_isUnit
Proof state before:
case intro.intro
z : ℤ√(-3)
h : IsUnit z
u : abs z.re = 1
hu : z.im = 0
v : ℤˣ
hv : ↑v = z.re
⊢ z = ↑↑v
Tactic:
rw [Zsqrtd.ext, hu, ← hv]
Proof state after:
case intro.intro
z : ℤ√(-3)
h : IsUnit z
u : abs 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 intro.intro
z : ℤ√(-3)
h : IsUnit z
u : abs z.re = 1
hu : z.im = 0
v : ℤˣ
hv : ↑v = z.re
⊢ ↑v = (↑↑v).re ∧ 0 = (↑↑v).im
Tactic:
simp only [Zsqrtd.coe_int_re, and_true_iff, eq_self_iff_true, Zsqrtd.coe_int_im]
Proof state after:
no goals
Theorem: Zsqrt3.coe_of_isUnit
Proof state before:
z : ℤ√(-3)
h : IsUnit z
u : abs 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 ∧ abs 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 ∧ abs u = 1
Theorem: Zsqrt3.coe_of_isUnit'
Proof state before:
case intro
z : ℤ√(-3)
h : IsUnit z
u : ℤˣ
hu : z = ↑↑u
⊢ ∃ u, z = ↑u ∧ abs 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
⊢ abs ↑u = 1
Theorem: Zsqrt3.coe_of_isUnit'
Proof state before:
case intro.refine'_2
z : ℤ√(-3)
h : IsUnit z
u : ℤˣ
hu : z = ↑↑u
⊢ abs ↑u = 1
Tactic:
exact Int.isUnit_iff_abs_eq.mp u.isUnit
Proof state after:
no goals
Theorem: OddPrimeOrFour.factors
Proof state before:
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hx : OddPrimeOrFour x
hfactor : x ∣ Zsqrtd.norm a
⊢ ∃ c, Abs.abs x = Zsqrtd.norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0
Tactic:
obtain rfl | ⟨hprime, hodd⟩ := hx
Proof state after:
case inl
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hfactor : 4 ∣ Zsqrtd.norm a
⊢ ∃ c, Abs.abs 4 = Zsqrtd.norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0

case inr.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
⊢ ∃ c, Abs.abs x = Zsqrtd.norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0
Theorem: OddPrimeOrFour.factors
Proof state before:
case inl
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hfactor : 4 ∣ Zsqrtd.norm a
⊢ ∃ c, Abs.abs 4 = Zsqrtd.norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0
Tactic:
refine' ⟨⟨1, 1⟩, _, zero_le_one, one_ne_zero⟩
Proof state after:
case inl
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hfactor : 4 ∣ Zsqrtd.norm a
⊢ Abs.abs 4 = Zsqrtd.norm { re := 1, im := 1 }
Theorem: OddPrimeOrFour.factors
Proof state before:
case inl
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hfactor : 4 ∣ Zsqrtd.norm a
⊢ Abs.abs 4 = Zsqrtd.norm { re := 1, im := 1 }
Tactic:
simp only [Zsqrtd.norm_def, mul_one, abs_of_pos, zero_lt_four, sub_neg_eq_add]
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 ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
⊢ ∃ c, Abs.abs x = Zsqrtd.norm c ∧ 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 ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : Abs.abs x = Zsqrtd.norm c
⊢ ∃ c, Abs.abs x = Zsqrtd.norm c ∧ 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 ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : Abs.abs x = Zsqrtd.norm c
⊢ ∃ c, Abs.abs x = Zsqrtd.norm c ∧ 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 ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : Abs.abs x = Zsqrtd.norm c
⊢ ∃ c_1, Zsqrtd.norm c = Zsqrtd.norm c_1 ∧ 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 ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : Abs.abs x = Zsqrtd.norm c
⊢ ∃ c_1, Zsqrtd.norm c = Zsqrtd.norm c_1 ∧ 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 ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : Abs.abs x = Zsqrtd.norm c
⊢ c.im ≠ 0
Theorem: OddPrimeOrFour.factors
Proof state before:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : Abs.abs x = Zsqrtd.norm c
⊢ c.im ≠ 0
Tactic:
intro H
Proof state after:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : Abs.abs x = Zsqrtd.norm c
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 ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : Abs.abs x = Zsqrtd.norm c
H : c.im = 0
⊢ False
Tactic:
rw [Zsqrtd.norm_def, H, MulZeroClass.mul_zero, sub_zero, ← pow_two, eq_comm] at hc
Proof state after:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : c.re ^ 2 = Abs.abs x
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 ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : c.re ^ 2 = Abs.abs x
H : c.im = 0
⊢ False
Tactic:
have := hprime.abs
Proof state after:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : c.re ^ 2 = Abs.abs x
H : c.im = 0
this : Prime (Abs.abs x)
⊢ False
Theorem: OddPrimeOrFour.factors
Proof state before:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : c.re ^ 2 = Abs.abs x
H : c.im = 0
this : Prime (Abs.abs x)
⊢ False
Tactic:
rw [←hc] at this
Proof state after:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : c.re ^ 2 = Abs.abs x
H : c.im = 0
this : Prime (c.re ^ 2)
⊢ False
Theorem: OddPrimeOrFour.factors
Proof state before:
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
hprime : Prime x
hodd : Odd x
c : ℤ√(-3)
hc : c.re ^ 2 = Abs.abs x
H : c.im = 0
this : Prime (c.re ^ 2)
⊢ False
Tactic:
exact pow_not_prime one_lt_two.ne' this
Proof state after:
no goals
Theorem: step1a
Proof state before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
⊢ 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 (Zsqrtd.norm a)
⊢ ¬Even a.re ∧ ¬Even a.im
Theorem: step1a
Proof state before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
⊢ ¬Even a.re ∧ ¬Even a.im
Tactic:
have : Even a.re ↔ Even a.im := by simpa [Zsqrtd.norm_def, parity_simps] using heven
Proof state after:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
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 (Zsqrtd.norm a)
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 (Zsqrtd.norm a)
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 (Zsqrtd.norm a)
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 (Zsqrtd.norm a)
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 (Zsqrtd.norm a)
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 (Zsqrtd.norm a)
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 (Zsqrtd.norm a)
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 (Zsqrtd.norm a)
this✝ : Even a.re ↔ Even a.im
hre : 2 ∣ a.re
him : 2 ∣ a.im
this : IsUnit 2
⊢ False