case pos
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : x = 0
⊢ IsPrimitiveClassified h

case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
⊢ IsPrimitiveClassified h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
⊢ IsPrimitiveClassified h
by_cases h0 : x = 0
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
⊢ IsPrimitiveClassified h
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
⊢ IsPrimitiveClassified h
let v := (x : ℚ) / z
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
⊢ IsPrimitiveClassified h
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
⊢ IsPrimitiveClassified h
let w := (y : ℚ) / z
case hz
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
⊢ z ≠ 0

case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
⊢ IsPrimitiveClassified h
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
⊢ IsPrimitiveClassified h
have hz : z ≠ 0
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
⊢ IsPrimitiveClassified h
case hz
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
⊢ z ≠ 0

case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
⊢ IsPrimitiveClassified h
apply ne_of_gt hzpos
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
⊢ IsPrimitiveClassified h
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
⊢ IsPrimitiveClassified h
have hq : v ^ 2 + w ^ 2 = 1 := by
  field_simp [hz, sq]
  norm_cast
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
⊢ IsPrimitiveClassified h
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
⊢ IsPrimitiveClassified h
have hvz : v ≠ 0 := by
  field_simp [hz]
  exact h0
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
⊢ IsPrimitiveClassified h
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
⊢ IsPrimitiveClassified h
have hw1 : w ≠ -1 := by
  contrapose! hvz with hw1
  replace hw1 : w = -1 := hw1; show v = 0
  rw [hw1, neg_sq, one_pow, add_left_eq_self] at hq
  exact pow_eq_zero hq
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
⊢ IsPrimitiveClassified h
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
⊢ IsPrimitiveClassified h
have hQ : ∀ x : ℚ, 1 + x ^ 2 ≠ 0 := by
  intro q
  apply ne_of_gt
  exact lt_add_of_pos_of_le zero_lt_one (sq_nonneg q)
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
⊢ IsPrimitiveClassified h
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
⊢ IsPrimitiveClassified h
have hp : (⟨v, w⟩ : ℚ × ℚ) ∈ { p : ℚ × ℚ | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 } := ⟨hq, hw1⟩
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
⊢ IsPrimitiveClassified h
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
⊢ IsPrimitiveClassified h
let q := (circleEquivGen hQ).symm ⟨⟨v, w⟩, hp⟩
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
⊢ IsPrimitiveClassified h
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
⊢ IsPrimitiveClassified h
have ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2) := by
  apply Prod.mk.inj
  have := ((circleEquivGen hQ).apply_symm_apply ⟨⟨v, w⟩, hp⟩).symm
  exact congr_arg Subtype.val this
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
⊢ IsPrimitiveClassified h
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
⊢ IsPrimitiveClassified h
let m := (q.den : ℤ)
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
⊢ IsPrimitiveClassified h
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
⊢ IsPrimitiveClassified h
let n := q.num
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
⊢ IsPrimitiveClassified h
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
⊢ IsPrimitiveClassified h
have hm0 : m ≠ 0 := by
  norm_cast
  apply Rat.den_nz q
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
⊢ IsPrimitiveClassified h
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
⊢ IsPrimitiveClassified h
have hq2 : q = n / m := (Rat.num_div_den q).symm
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
⊢ IsPrimitiveClassified h
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
⊢ IsPrimitiveClassified h
have hm2n2 : 0 < m ^ 2 + n ^ 2 := by
  apply lt_add_of_pos_of_le _ (sq_nonneg n)
  exact lt_of_le_of_ne (sq_nonneg m) (Ne.symm (pow_ne_zero 2 hm0))
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
⊢ IsPrimitiveClassified h
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
⊢ IsPrimitiveClassified h
have hm2n20 : (m : ℚ) ^ 2 + (n : ℚ) ^ 2 ≠ 0 := by
  norm_cast
  simpa only [Int.coe_nat_pow] using ne_of_gt hm2n2
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
⊢ IsPrimitiveClassified h
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
⊢ IsPrimitiveClassified h
have hx1 {j k : ℚ} (h₁ : k ≠ 0) (h₂ : k ^ 2 + j ^ 2 ≠ 0) :
    (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2) :=
  by field_simp
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
⊢ IsPrimitiveClassified h
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
⊢ IsPrimitiveClassified h
have hw2 : w = ((m : ℚ) ^ 2 - (n : ℚ) ^ 2) / ((m : ℚ) ^ 2 + (n : ℚ) ^ 2) := by
  calc
    w = (1 - q ^ 2) / (1 + q ^ 2) := by apply ht4.2
    _ = (1 - (↑n / ↑m) ^ 2) / (1 + (↑n / ↑m) ^ 2) := by rw [hq2]
    _ = _ := by exact hx1 (Int.cast_ne_zero.mpr hm0) hm2n20
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
⊢ IsPrimitiveClassified h
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
⊢ IsPrimitiveClassified h
have hx2 {j k : ℚ} (h₁ : k ≠ 0) (h₂ : k ^ 2 + j ^ 2 ≠ 0) :
    2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2) :=
  have h₃ : k * (k ^ 2 + j ^ 2) ≠ 0 := mul_ne_zero h₁ h₂
  by field_simp; ring
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
⊢ IsPrimitiveClassified h
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
⊢ IsPrimitiveClassified h
have hv2 : v = 2 * m * n / ((m : ℚ) ^ 2 + (n : ℚ) ^ 2) := by
  calc
    v = 2 * q / (1 + q ^ 2) := by apply ht4.1
    _ = 2 * (n / m) / (1 + (↑n / ↑m) ^ 2) := by rw [hq2]
    _ = _ := by exact hx2 (Int.cast_ne_zero.mpr hm0) hm2n20
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
⊢ IsPrimitiveClassified h
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
⊢ IsPrimitiveClassified h
have hnmcp : Int.gcd n m = 1 := q.reduced
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
⊢ IsPrimitiveClassified h
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
⊢ IsPrimitiveClassified h
have hmncp : Int.gcd m n = 1 := by
  rw [Int.gcd_comm]
  exact hnmcp
case neg.inl.inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 0
⊢ IsPrimitiveClassified h

case neg.inl.inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 1
⊢ IsPrimitiveClassified h

case neg.inr.inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 0
⊢ IsPrimitiveClassified h

case neg.inr.inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
⊢ IsPrimitiveClassified h
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
⊢ IsPrimitiveClassified h
cases' Int.emod_two_eq_zero_or_one m with hm2 hm2 <;>
  cases' Int.emod_two_eq_zero_or_one n with hn2 hn2
no goals
case pos
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : x = 0
⊢ IsPrimitiveClassified h
exact h.isPrimitiveClassified_of_coprime_of_zero_left hc h0
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
⊢ ↑x * ↑x + ↑y * ↑y = ↑z * ↑z
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
⊢ v ^ 2 + w ^ 2 = 1
field_simp [hz, sq]
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
⊢ ↑x * ↑x + ↑y * ↑y = ↑z * ↑z
norm_cast
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
⊢ ¬x = 0
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
⊢ v ≠ 0
field_simp [hz]
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
⊢ ¬x = 0
exact h0
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hw1 : ↑y / ↑z = -1
⊢ ↑x / ↑z = 0
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
⊢ w ≠ -1
contrapose! hvz with hw1
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hw1 : w = -1
⊢ ↑x / ↑z = 0
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hw1 : ↑y / ↑z = -1
⊢ ↑x / ↑z = 0
replace hw1 : w = -1 := hw1
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hw1 : w = -1
⊢ v = 0
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hw1 : w = -1
⊢ ↑x / ↑z = 0
show v = 0
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 = 0
hw1 : w = -1
⊢ v = 0
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hw1 : w = -1
⊢ v = 0
rw [hw1, neg_sq, one_pow, add_left_eq_self] at hq
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 = 0
hw1 : w = -1
⊢ v = 0
exact pow_eq_zero hq
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
q : ℚ
⊢ 1 + q ^ 2 ≠ 0
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
⊢ ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
intro q
case h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
q : ℚ
⊢ 0 < 1 + q ^ 2
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
q : ℚ
⊢ 1 + q ^ 2 ≠ 0
apply ne_of_gt
no goals
case h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
q : ℚ
⊢ 0 < 1 + q ^ 2
exact lt_add_of_pos_of_le zero_lt_one (sq_nonneg q)
case x
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
⊢ (v, w) = (2 * q / (1 + q ^ 2), (1 - q ^ 2) / (1 + q ^ 2))
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
⊢ v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
apply Prod.mk.inj
case x
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
this :
  { val := (v, w), property := hp } = ↑(circleEquivGen hQ) (↑(circleEquivGen hQ).symm { val := (v, w), property := hp })
⊢ (v, w) = (2 * q / (1 + q ^ 2), (1 - q ^ 2) / (1 + q ^ 2))
case x
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
⊢ (v, w) = (2 * q / (1 + q ^ 2), (1 - q ^ 2) / (1 + q ^ 2))
have := ((circleEquivGen hQ).apply_symm_apply ⟨⟨v, w⟩, hp⟩).symm
no goals
case x
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
this :
  { val := (v, w), property := hp } = ↑(circleEquivGen hQ) (↑(circleEquivGen hQ).symm { val := (v, w), property := hp })
⊢ (v, w) = (2 * q / (1 + q ^ 2), (1 - q ^ 2) / (1 + q ^ 2))
exact congr_arg Subtype.val this
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
⊢ ¬q.den = 0
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
⊢ m ≠ 0
norm_cast
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
⊢ ¬q.den = 0
apply Rat.den_nz q
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
⊢ 0 < m ^ 2
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
⊢ 0 < m ^ 2 + n ^ 2
apply lt_add_of_pos_of_le _ (sq_nonneg n)
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
⊢ 0 < m ^ 2
exact lt_of_le_of_ne (sq_nonneg m) (Ne.symm (pow_ne_zero 2 hm0))
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
⊢ ¬↑(q.den ^ 2) + n ^ 2 = 0
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
⊢ ↑m ^ 2 + ↑n ^ 2 ≠ 0
norm_cast
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
⊢ ¬↑(q.den ^ 2) + n ^ 2 = 0
simpa only [Int.coe_nat_pow] using ne_of_gt hm2n2
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
j k : ℚ
h₁ : k ≠ 0
h₂ : k ^ 2 + j ^ 2 ≠ 0
⊢ (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
field_simp
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
⊢ w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
calc
  w = (1 - q ^ 2) / (1 + q ^ 2) := by apply ht4.2
  _ = (1 - (↑n / ↑m) ^ 2) / (1 + (↑n / ↑m) ^ 2) := by rw [hq2]
  _ = _ := by exact hx1 (Int.cast_ne_zero.mpr hm0) hm2n20
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
⊢ w = (1 - q ^ 2) / (1 + q ^ 2)
apply ht4.2
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
⊢ (1 - q ^ 2) / (1 + q ^ 2) = (1 - (↑n / ↑m) ^ 2) / (1 + (↑n / ↑m) ^ 2)
rw [hq2]
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
⊢ (1 - (↑n / ↑m) ^ 2) / (1 + (↑n / ↑m) ^ 2) = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
exact hx1 (Int.cast_ne_zero.mpr hm0) hm2n20
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
j k : ℚ
h₁ : k ≠ 0
h₂ : k ^ 2 + j ^ 2 ≠ 0
h₃ : k * (k ^ 2 + j ^ 2) ≠ 0
⊢ 2 * j * k ^ 2 * (k ^ 2 + j ^ 2) = 2 * k * j * (k * (k ^ 2 + j ^ 2))
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
j k : ℚ
h₁ : k ≠ 0
h₂ : k ^ 2 + j ^ 2 ≠ 0
h₃ : k * (k ^ 2 + j ^ 2) ≠ 0
⊢ 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
field_simp
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
j k : ℚ
h₁ : k ≠ 0
h₂ : k ^ 2 + j ^ 2 ≠ 0
h₃ : k * (k ^ 2 + j ^ 2) ≠ 0
⊢ 2 * j * k ^ 2 * (k ^ 2 + j ^ 2) = 2 * k * j * (k * (k ^ 2 + j ^ 2))
ring
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
⊢ v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
calc
  v = 2 * q / (1 + q ^ 2) := by apply ht4.1
  _ = 2 * (n / m) / (1 + (↑n / ↑m) ^ 2) := by rw [hq2]
  _ = _ := by exact hx2 (Int.cast_ne_zero.mpr hm0) hm2n20
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
⊢ v = 2 * q / (1 + q ^ 2)
apply ht4.1
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
⊢ 2 * q / (1 + q ^ 2) = 2 * (↑n / ↑m) / (1 + (↑n / ↑m) ^ 2)
rw [hq2]
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
⊢ 2 * (↑n / ↑m) / (1 + (↑n / ↑m) ^ 2) = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
exact hx2 (Int.cast_ne_zero.mpr hm0) hm2n20
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
⊢ Int.gcd n m = 1
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
⊢ Int.gcd m n = 1
rw [Int.gcd_comm]
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
⊢ Int.gcd n m = 1
exact hnmcp
case neg.inl.inl.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 0
⊢ False
case neg.inl.inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 0
⊢ IsPrimitiveClassified h
exfalso
case neg.inl.inl.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 0
h1 : 2 ∣ ↑(Int.gcd n m)
⊢ False
case neg.inl.inl.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 0
⊢ False
have h1 : 2 ∣ (Int.gcd n m : ℤ) :=
  Int.dvd_gcd (Int.dvd_of_emod_eq_zero hn2) (Int.dvd_of_emod_eq_zero hm2)
case neg.inl.inl.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 0
h1 : 2 ∣ ↑1
⊢ False
case neg.inl.inl.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 0
h1 : 2 ∣ ↑(Int.gcd n m)
⊢ False
rw [hnmcp] at h1
case neg.inl.inl.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 0
⊢ 2 ∣ ↑1 → False
case neg.inl.inl.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 0
h1 : 2 ∣ ↑1
⊢ False
revert h1
no goals
case neg.inl.inl.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 0
⊢ 2 ∣ ↑1 → False
norm_num
case neg.inl.inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 1
⊢ m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0

x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 1
⊢ Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
case neg.inl.inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 1
⊢ IsPrimitiveClassified h
apply h.isPrimitiveClassified_aux hc hzpos hm2n2 hv2 hw2 _ hmncp
case neg.inl.inr.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 1
⊢ m % 2 = 0 ∧ n % 2 = 1
case neg.inl.inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 1
⊢ m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
apply Or.intro_left
no goals
case neg.inl.inr.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 1
⊢ m % 2 = 0 ∧ n % 2 = 1
exact And.intro hm2 hn2
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 1
⊢ Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
apply coprime_sq_sub_sq_add_of_even_odd hmncp hm2 hn2
case neg.inr.inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 0
⊢ m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0

x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 0
⊢ Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
case neg.inr.inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 0
⊢ IsPrimitiveClassified h
apply h.isPrimitiveClassified_aux hc hzpos hm2n2 hv2 hw2 _ hmncp
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 0
⊢ Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
apply coprime_sq_sub_sq_add_of_odd_even hmncp hm2 hn2
case neg.inr.inl.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 0
⊢ m % 2 = 1 ∧ n % 2 = 0
case neg.inr.inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 0
⊢ m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
apply Or.intro_right
no goals
case neg.inr.inl.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 0
⊢ m % 2 = 1 ∧ n % 2 = 0
exact And.intro hm2 hn2
case neg.inr.inr.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
⊢ False
case neg.inr.inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
⊢ IsPrimitiveClassified h
exfalso
case neg.inr.inr.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1
⊢ False
case neg.inr.inr.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
⊢ False
have h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧
      (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1 :=
  coprime_sq_sub_sq_sum_of_odd_odd hmncp hm2 hn2
case neg.inr.inr.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hyo : 0 = 1
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1
h2 : y = (m ^ 2 - n ^ 2) / 2 ∧ z = (m ^ 2 + n ^ 2) / 2
⊢ False
case neg.inr.inr.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1
h2 : y = (m ^ 2 - n ^ 2) / 2 ∧ z = (m ^ 2 + n ^ 2) / 2
⊢ False
rw [h2.1, h1.2.2.1] at hyo
case neg.inr.inr.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1
h2 : y = (m ^ 2 - n ^ 2) / 2 ∧ z = (m ^ 2 + n ^ 2) / 2
⊢ 0 = 1 → False
case neg.inr.inr.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hyo : 0 = 1
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1
h2 : y = (m ^ 2 - n ^ 2) / 2 ∧ z = (m ^ 2 + n ^ 2) / 2
⊢ False
revert hyo
no goals
case neg.inr.inr.h
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1
h2 : y = (m ^ 2 - n ^ 2) / 2 ∧ z = (m ^ 2 + n ^ 2) / 2
⊢ 0 = 1 → False
norm_num
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1
⊢ ↑y / ↑z = ↑((m ^ 2 - n ^ 2) / 2) / ↑((m ^ 2 + n ^ 2) / 2)

x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1
⊢ 0 < (m ^ 2 + n ^ 2) / 2
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1
⊢ y = (m ^ 2 - n ^ 2) / 2 ∧ z = (m ^ 2 + n ^ 2) / 2
apply Rat.div_int_inj hzpos _ (h.coprime_of_coprime hc) h1.2.2.2
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1
⊢ w = ↑((m ^ 2 - n ^ 2) / 2) / ↑((m ^ 2 + n ^ 2) / 2)
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1
⊢ ↑y / ↑z = ↑((m ^ 2 - n ^ 2) / 2) / ↑((m ^ 2 + n ^ 2) / 2)
show w = _
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1
⊢ w = Rat.divInt ((m ^ 2 - n ^ 2) / 2 * 2) ((m ^ 2 + n ^ 2) / 2 * 2)
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1
⊢ w = ↑((m ^ 2 - n ^ 2) / 2) / ↑((m ^ 2 + n ^ 2) / 2)
rw [← Rat.divInt_eq_div, ← Rat.divInt_mul_right (by norm_num : (2 : ℤ) ≠ 0)]
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1
⊢ (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2) = Rat.divInt (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2)
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1
⊢ w = Rat.divInt ((m ^ 2 - n ^ 2) / 2 * 2) ((m ^ 2 + n ^ 2) / 2 * 2)
rw [Int.ediv_mul_cancel h1.1, Int.ediv_mul_cancel h1.2.1, hw2]
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1
⊢ (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2) = Rat.divInt (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2)
norm_cast
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1
⊢ 2 ≠ 0
norm_num
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1
⊢ 0 * 2 < (m ^ 2 + n ^ 2) / 2 * 2
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1
⊢ 0 < (m ^ 2 + n ^ 2) / 2
apply (mul_lt_mul_right (by norm_num : 0 < (2 : ℤ))).mp
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1
⊢ 0 < m ^ 2 + n ^ 2
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1
⊢ 0 * 2 < (m ^ 2 + n ^ 2) / 2 * 2
rw [Int.ediv_mul_cancel h1.1, MulZeroClass.zero_mul]
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1
⊢ 0 < m ^ 2 + n ^ 2
exact hm2n2
no goals
x y z : ℤ
h : PythagoreanTriple x y z
hc : Int.gcd x y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hz : z ≠ 0
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.fst ^ 2 + p.snd ^ 2 = 1 ∧ p.snd ≠ -1}
q : (fun x => ℚ) { val := (v, w), property := hp } := ↑(circleEquivGen hQ).symm { val := (v, w), property := hp }
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : Int.gcd n m = 1
hmncp : Int.gcd m n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1
⊢ 0 < 2
norm_num