Theorem: step1 (Flt/Edwards.lean)

State before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
⊢ ∃ u, a = { re := 1, im := 1 } * u ∨ a = { re := 1, im := -1 } * u
Tactic:
obtain ⟨ha, hb⟩ := step1a hcoprime heven
State after:
case intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
ha : Odd a.re
hb : Odd a.im
⊢ ∃ u, a = { re := 1, im := 1 } * u ∨ a = { re := 1, im := -1 } * u

State before:
case intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
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
State after:
case intro.inl
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
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 (Zsqrtd.norm a)
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

State before:
case intro.inl
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
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
State after:
case intro.inl.intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
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

State before:
case intro.inl.intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
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
State after:
case intro.inl.intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
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

State before:
case intro.inl.intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
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⟩
State after:
case intro.inl.intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
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 }

State before:
case intro.inl.intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
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
State after:
case intro.inl.intro.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
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 }

State before:
case intro.inl.intro.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
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, hv, Zsqrtd.mul_re, Zsqrtd.mul_im]
State after:
case intro.inl.intro.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
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

State before:
case intro.inl.intro.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
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
Tactic:
dsimp only
State after:
case intro.inl.intro.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
ha : Odd a.re
hb : Odd a.im
v : ℤ
hv : a.re = 4 * v - a.im
⊢ 4 * v - a.im = 1 * (v - a.im) + -3 * -1 * v ∧ a.im = 1 * v + -1 * (v - a.im)

State before:
case intro.inl.intro.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
ha : Odd a.re
hb : Odd a.im
v : ℤ
hv : a.re = 4 * v - a.im
⊢ 4 * v - a.im = 1 * (v - a.im) + -3 * -1 * v ∧ a.im = 1 * v + -1 * (v - a.im)
Tactic:
constructor <;> ring
State after:
no goals

State before:
case intro.inr
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
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
State after:
case intro.inr.intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
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

State before:
case intro.inr.intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
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 [sub_eq_iff_eq_add] at hv
State after:
case intro.inr.intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
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

State before:
case intro.inr.intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
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 ⟨a.im + v, -v⟩
State after:
case intro.inr.intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
ha : Odd a.re
hb : Odd a.im
v : ℤ
hv : a.re = 4 * v + a.im
⊢ a = { re := 1, im := 1 } * { re := a.im + v, im := -v } ∨ a = { re := 1, im := -1 } * { re := a.im + v, im := -v }

State before:
case intro.inr.intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
ha : Odd a.re
hb : Odd a.im
v : ℤ
hv : a.re = 4 * v + a.im
⊢ a = { re := 1, im := 1 } * { re := a.im + v, im := -v } ∨ a = { re := 1, im := -1 } * { re := a.im + v, im := -v }
Tactic:
left
State after:
case intro.inr.intro.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
ha : Odd a.re
hb : Odd a.im
v : ℤ
hv : a.re = 4 * v + a.im
⊢ a = { re := 1, im := 1 } * { re := a.im + v, im := -v }

State before:
case intro.inr.intro.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
ha : Odd a.re
hb : Odd a.im
v : ℤ
hv : a.re = 4 * v + a.im
⊢ a = { re := 1, im := 1 } * { re := a.im + v, im := -v }
Tactic:
rw [Zsqrtd.ext, hv, Zsqrtd.mul_re, Zsqrtd.mul_im]
State after:
case intro.inr.intro.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
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 := a.im + v, im := -v }.re +
        -3 * { re := 1, im := 1 }.im * { re := a.im + v, im := -v }.im ∧
    a.im =
      { re := 1, im := 1 }.re * { re := a.im + v, im := -v }.im +
        { re := 1, im := 1 }.im * { re := a.im + v, im := -v }.re

State before:
case intro.inr.intro.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
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 := a.im + v, im := -v }.re +
        -3 * { re := 1, im := 1 }.im * { re := a.im + v, im := -v }.im ∧
    a.im =
      { re := 1, im := 1 }.re * { re := a.im + v, im := -v }.im +
        { re := 1, im := 1 }.im * { re := a.im + v, im := -v }.re
Tactic:
dsimp only
State after:
case intro.inr.intro.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
ha : Odd a.re
hb : Odd a.im
v : ℤ
hv : a.re = 4 * v + a.im
⊢ 4 * v + a.im = 1 * (a.im + v) + -3 * 1 * -v ∧ a.im = 1 * -v + 1 * (a.im + v)

State before:
case intro.inr.intro.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
ha : Odd a.re
hb : Odd a.im
v : ℤ
hv : a.re = 4 * v + a.im
⊢ 4 * v + a.im = 1 * (a.im + v) + -3 * 1 * -v ∧ a.im = 1 * -v + 1 * (a.im + v)
Tactic:
constructor <;> ring
State after:
no goals