case inl.inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0

case inl.inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 0
hy : y % 2 = 1
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0

case inr.inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 1
hy : y % 2 = 0
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0

case inr.inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 1
hy : y % 2 = 1
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
cases' Int.emod_two_eq_zero_or_one x with hx hx <;>
  cases' Int.emod_two_eq_zero_or_one y with hy hy
case inl.inl.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ False
case inl.inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
exfalso
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ 2 ∣ Int.natAbs x

x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ 2 ∣ Int.natAbs y
case inl.inl.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ False
apply Nat.not_coprime_of_dvd_of_dvd (by decide : 1 < 2) _ _ hc
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ 1 < 2
decide
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ ↑2 ∣ x
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ 2 ∣ Int.natAbs x
apply Int.coe_nat_dvd_left.1
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ ↑2 ∣ x
apply Int.dvd_of_emod_eq_zero hx
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ ↑2 ∣ y
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ 2 ∣ Int.natAbs y
apply Int.coe_nat_dvd_left.1
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ ↑2 ∣ y
apply Int.dvd_of_emod_eq_zero hy
case inl.inr.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 0
hy : y % 2 = 1
⊢ x % 2 = 0 ∧ y % 2 = 1
case inl.inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 0
hy : y % 2 = 1
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
left
no goals
case inl.inr.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 0
hy : y % 2 = 1
⊢ x % 2 = 0 ∧ y % 2 = 1
exact ⟨hx, hy⟩
case inr.inl.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 1
hy : y % 2 = 0
⊢ x % 2 = 1 ∧ y % 2 = 0
case inr.inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 1
hy : y % 2 = 0
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
right
no goals
case inr.inl.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 1
hy : y % 2 = 0
⊢ x % 2 = 1 ∧ y % 2 = 0
exact ⟨hx, hy⟩
case inr.inr.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 1
hy : y % 2 = 1
⊢ False
case inr.inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 1
hy : y % 2 = 1
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
exfalso
case inr.inr.h.intro.intro.intro
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : Int.gcd (x0 * 2 + 1) (y0 * 2 + 1) = 1
⊢ False
case inr.inr.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 1
hy : y % 2 = 1
⊢ False
obtain ⟨x0, y0, rfl, rfl⟩ : ∃ x0 y0, x = x0 * 2 + 1 ∧ y = y0 * 2 + 1 := by
  cases' exists_eq_mul_left_of_dvd (Int.dvd_sub_of_emod_eq hx) with x0 hx2
  cases' exists_eq_mul_left_of_dvd (Int.dvd_sub_of_emod_eq hy) with y0 hy2
  rw [sub_eq_iff_eq_add] at hx2 hy2
  exact ⟨x0, y0, hx2, hy2⟩
case inr.inr.h.intro.intro.intro
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : Int.gcd (x0 * 2 + 1) (y0 * 2 + 1) = 1
⊢ z * z % 4 = 2
case inr.inr.h.intro.intro.intro
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : Int.gcd (x0 * 2 + 1) (y0 * 2 + 1) = 1
⊢ False
apply Int.sq_ne_two_mod_four z
case inr.inr.h.intro.intro.intro
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : Int.gcd (x0 * 2 + 1) (y0 * 2 + 1) = 1
⊢ (4 * (x0 * x0 + x0 + y0 * y0 + y0) + 2) % 4 = 2
case inr.inr.h.intro.intro.intro
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : Int.gcd (x0 * 2 + 1) (y0 * 2 + 1) = 1
⊢ z * z % 4 = 2
rw [show z * z = 4 * (x0 * x0 + x0 + y0 * y0 + y0) + 2 by
    rw [← h.eq]
    ring]
no goals
case inr.inr.h.intro.intro.intro
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : Int.gcd (x0 * 2 + 1) (y0 * 2 + 1) = 1
⊢ (4 * (x0 * x0 + x0 + y0 * y0 + y0) + 2) % 4 = 2
field_simp [Int.add_emod]
case intro
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 1
hy : y % 2 = 1
x0 : ℤ
hx2 : x - 1 = x0 * 2
⊢ ∃ x0 y0, x = x0 * 2 + 1 ∧ y = y0 * 2 + 1
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 1
hy : y % 2 = 1
⊢ ∃ x0 y0, x = x0 * 2 + 1 ∧ y = y0 * 2 + 1
cases' exists_eq_mul_left_of_dvd (Int.dvd_sub_of_emod_eq hx) with x0 hx2
case intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 1
hy : y % 2 = 1
x0 : ℤ
hx2 : x - 1 = x0 * 2
y0 : ℤ
hy2 : y - 1 = y0 * 2
⊢ ∃ x0 y0, x = x0 * 2 + 1 ∧ y = y0 * 2 + 1
case intro
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 1
hy : y % 2 = 1
x0 : ℤ
hx2 : x - 1 = x0 * 2
⊢ ∃ x0 y0, x = x0 * 2 + 1 ∧ y = y0 * 2 + 1
cases' exists_eq_mul_left_of_dvd (Int.dvd_sub_of_emod_eq hy) with y0 hy2
case intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 1
hy : y % 2 = 1
x0 : ℤ
hx2 : x = x0 * 2 + 1
y0 : ℤ
hy2 : y = y0 * 2 + 1
⊢ ∃ x0 y0, x = x0 * 2 + 1 ∧ y = y0 * 2 + 1
case intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 1
hy : y % 2 = 1
x0 : ℤ
hx2 : x - 1 = x0 * 2
y0 : ℤ
hy2 : y - 1 = y0 * 2
⊢ ∃ x0 y0, x = x0 * 2 + 1 ∧ y = y0 * 2 + 1
rw [sub_eq_iff_eq_add] at hx2 hy2
no goals
case intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hx : x % 2 = 1
hy : y % 2 = 1
x0 : ℤ
hx2 : x = x0 * 2 + 1
y0 : ℤ
hy2 : y = y0 * 2 + 1
⊢ ∃ x0 y0, x = x0 * 2 + 1 ∧ y = y0 * 2 + 1
exact ⟨x0, y0, hx2, hy2⟩
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : Int.gcd (x0 * 2 + 1) (y0 * 2 + 1) = 1
⊢ (x0 * 2 + 1) * (x0 * 2 + 1) + (y0 * 2 + 1) * (y0 * 2 + 1) = 4 * (x0 * x0 + x0 + y0 * y0 + y0) + 2
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : Int.gcd (x0 * 2 + 1) (y0 * 2 + 1) = 1
⊢ z * z = 4 * (x0 * x0 + x0 + y0 * y0 + y0) + 2
rw [← h.eq]
no goals
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : Int.gcd (x0 * 2 + 1) (y0 * 2 + 1) = 1
⊢ (x0 * 2 + 1) * (x0 * 2 + 1) + (y0 * 2 + 1) * (y0 * 2 + 1) = 4 * (x0 * x0 + x0 + y0 * y0 + y0) + 2
ring