awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
hy : y % 2 = 1
inr :
  ∀ (x0 y0 : ℤ) (hx : (x0 * 2 + 1) % 2 = 1) (hy : (y0 * 2 + 1) % 2 = 1)
    (h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z) (hc : (x0 * 2 + 1).gcd (y0 * 2 + 1) = 1), False
⊢ False

Tactic:
obtain ⟨x0, y0, rfl, rfl⟩ : ∃ x0 y0, x = x0 * 2 + 1 ∧ y = y0 * 2 + 1 := by
      obtain ⟨x0, hx2⟩ := exists_eq_mul_left_of_dvd (Int.dvd_self_sub_of_emod_eq hx)
      obtain ⟨y0, hy2⟩ := exists_eq_mul_left_of_dvd (Int.dvd_self_sub_of_emod_eq hy)
      rw [sub_eq_iff_eq_add] at hx2 hy2
      exact ⟨x0, y0, hx2, hy2⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : (x0 * 2 + 1).gcd (y0 * 2 + 1) = 1
inr : z * z % 4 = 2
⊢ False

Tactic:
apply Int.sq_ne_two_mod_four z

Premises used: Int.sq_ne_two_mod_four
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : (x0 * 2 + 1).gcd (y0 * 2 + 1) = 1
rw : (x0 * 2 + 1) * (x0 * 2 + 1) + (y0 * 2 + 1) * (y0 * 2 + 1) = 4 * (x0 * x0 + x0 + y0 * y0 + y0) + 2
⊢ z * z = 4 * (x0 * x0 + x0 + y0 * y0 + y0) + 2

Tactic:
rw [← h.eq]

Premises used: PythagoreanTriple.eq
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : (x0 * 2 + 1).gcd (y0 * 2 + 1) = 1
⊢ (x0 * 2 + 1) * (x0 * 2 + 1) + (y0 * 2 + 1) * (y0 * 2 + 1) = 4 * (x0 * x0 + x0 + y0 * y0 + y0) + 2

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : (x0 * 2 + 1).gcd (y0 * 2 + 1) = 1
inr : (4 * (x0 * x0 + x0 + y0 * y0 + y0) + 2) % 4 = 2
⊢ z * z % 4 = 2

Tactic:
rw [show z * z = 4 * (x0 * x0 + x0 + y0 * y0 + y0) + 2 by
        rw [← h.eq]
        ring]
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : (x0 * 2 + 1).gcd (y0 * 2 + 1) = 1
inr : HMod.hMod (α := ℤ) 2 4 % 4 = 2
⊢ (4 * (x0 * x0 + x0 + y0 * y0 + y0) + 2) % 4 = 2

Tactic:
simp only [Int.add_emod, Int.mul_emod_right, zero_add]

Premises used: zero_add, Int.mul_emod_right, Int.add_emod
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : (x0 * 2 + 1).gcd (y0 * 2 + 1) = 1
⊢ HMod.hMod (α := ℤ) 2 4 % 4 = 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
pos : ∀ (h0 : x.gcd y = 0), (↑(x.gcd y) : ℤ) ∣ z
neg : ∀ (h0 : ¬x.gcd y = 0), (↑(x.gcd y) : ℤ) ∣ z
⊢ (↑(x.gcd y) : ℤ) ∣ z

Tactic:
by_cases h0 : Int.gcd x y = 0

Premises used: Int.gcd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
⊢ x = 0

Tactic:
obtain ⟨hx, hy⟩ := Int.gcd_eq_zero_iff.mp h0

Premises used: Int.gcd_eq_zero_iff, Iff.mp
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
⊢ y = 0

Tactic:
obtain ⟨hx, hy⟩ := Int.gcd_eq_zero_iff.mp h0

Premises used: Int.gcd_eq_zero_iff, Iff.mp
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
⊢ z = 0

Tactic:
simpa only [PythagoreanTriple, hx, hy, add_zero, zero_eq_mul, mul_zero,
        or_self_iff] using h

Premises used: or_self_iff, zero_eq_mul, MulZeroClass.mul_zero, PythagoreanTriple, add_zero
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
⊢ z = 0

Tactic:
have hz : z = 0 := by
      simpa only [PythagoreanTriple, hx, hy, add_zero, zero_eq_mul, mul_zero,
        or_self_iff] using h
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
hz : z = 0
⊢ (↑(x.gcd y) : ℤ) ∣ z

Tactic:
simp [h0, hz]
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
⊢ ∃ (k : ℕ) (x0 : ℤ) (y0 : ℤ), 0 < k ∧ x0.gcd y0 = 1 ∧ x = x0 * (↑k : ℤ) ∧ y = y0 * (↑k : ℤ)

Tactic:
Int.exists_gcd_one' (Nat.pos_of_ne_zero h0)

Premises used: Nat.pos_of_ne_zero, Int.exists_gcd_one'
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
neg :
  ∀ (k : ℕ) (x0 y0 : ℤ),
    0 < k →
      ∀ (h2 : x0.gcd y0 = 1) (h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) z)
        (h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0), (↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ) ∣ z
⊢ (↑(x.gcd y) : ℤ) ∣ z

Tactic:
obtain ⟨k, x0, y0, _, h2, rfl, rfl⟩ :
    ∃ (k : ℕ) (x0 y0 : _), 0 < k ∧ Int.gcd x0 y0 = 1 ∧ x = x0 * k ∧ y = y0 * k :=
    Int.exists_gcd_one' (Nat.pos_of_ne_zero h0)

Premises used: Nat.pos_of_ne_zero, Int.exists_gcd_one', rfl
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z : ℤ
k : ℕ
x0 y0 : ℤ
left : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) z
h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0
neg : (↑k : ℤ) ∣ z
⊢ (↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ) ∣ z

Tactic:
rw [Int.gcd_mul_right, h2, Int.natAbs_natCast, one_mul]

Premises used: Int.gcd_mul_right, Int.natAbs_natCast, one_mul
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z : ℤ
k : ℕ
x0 y0 : ℤ
left : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) z
h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0
neg : HPow.hPow (α := ℤ) (β := ℕ) (↑k : ℤ) 2 ∣ x0 * (↑k : ℤ) * (x0 * (↑k : ℤ)) + y0 * (↑k : ℤ) * (y0 * (↑k : ℤ))
⊢ (↑k : ℤ) ∣ z

Tactic:
rw [← Int.pow_dvd_pow_iff two_ne_zero, sq z, ← h.eq]

Premises used: sq, Int.pow_dvd_pow_iff, two_ne_zero, PythagoreanTriple.eq
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z : ℤ
k : ℕ
x0 y0 : ℤ
left : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) z
h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0
⊢ x0 * (↑k : ℤ) * (x0 * (↑k : ℤ)) + y0 * (↑k : ℤ) * (y0 * (↑k : ℤ)) =
    HPow.hPow (α := ℤ) (β := ℕ) (↑k : ℤ) 2 * (x0 * x0 + y0 * y0)

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z : ℤ
k : ℕ
x0 y0 : ℤ
left : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) z
h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0
neg : HPow.hPow (α := ℤ) (β := ℕ) (↑k : ℤ) 2 ∣ HPow.hPow (α := ℤ) (β := ℕ) (↑k : ℤ) 2 * (x0 * x0 + y0 * y0)
⊢ HPow.hPow (α := ℤ) (β := ℕ) (↑k : ℤ) 2 ∣ x0 * (↑k : ℤ) * (x0 * (↑k : ℤ)) + y0 * (↑k : ℤ) * (y0 * (↑k : ℤ))

Tactic:
rw [(by ring : x0 * k * (x0 * k) + y0 * k * (y0 * k) = (k : ℤ) ^ 2 * (x0 * x0 + y0 * y0))]
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z : ℤ
k : ℕ
x0 y0 : ℤ
left : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) z
h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0
⊢ HPow.hPow (α := ℤ) (β := ℕ) (↑k : ℤ) 2 ∣ HPow.hPow (α := ℤ) (β := ℕ) (↑k : ℤ) 2 * (x0 * x0 + y0 * y0)

Tactic:
dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z : ℤ
k : ℕ
x0 y0 : ℤ
left : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) z
h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0
⊢ HPow.hPow (α := ℤ) (β := ℕ) (↑k : ℤ) 2 ∣ HPow.hPow (α := ℤ) (β := ℕ) (↑k : ℤ) 2 * (x0 * x0 + y0 * y0)

Tactic:
exact dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
pos : ∀ (h0 : x.gcd y = 0), PythagoreanTriple (x / (↑(x.gcd y) : ℤ)) (y / (↑(x.gcd y) : ℤ)) (z / (↑(x.gcd y) : ℤ))
neg : ∀ (h0 : ¬x.gcd y = 0), PythagoreanTriple (x / (↑(x.gcd y) : ℤ)) (y / (↑(x.gcd y) : ℤ)) (z / (↑(x.gcd y) : ℤ))
⊢ PythagoreanTriple (x / (↑(x.gcd y) : ℤ)) (y / (↑(x.gcd y) : ℤ)) (z / (↑(x.gcd y) : ℤ))

Tactic:
by_cases h0 : Int.gcd x y = 0

Premises used: Int.gcd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
hz : z = 0
⊢ PythagoreanTriple (x / (↑(x.gcd y) : ℤ)) (y / (↑(x.gcd y) : ℤ)) (z / (↑(x.gcd y) : ℤ))

Tactic:
simpa [h0, hx, hy, hz] using zero

Premises used: PythagoreanTriple.zero
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
neg :
  ∀ (z0 : ℤ) (h : PythagoreanTriple x y ((↑(x.gcd y) : ℤ) * z0)),
    PythagoreanTriple (x / (↑(x.gcd y) : ℤ)) (y / (↑(x.gcd y) : ℤ)) ((↑(x.gcd y) : ℤ) * z0 / (↑(x.gcd y) : ℤ))
⊢ PythagoreanTriple (x / (↑(x.gcd y) : ℤ)) (y / (↑(x.gcd y) : ℤ)) (z / (↑(x.gcd y) : ℤ))

Tactic:
rcases h.gcd_dvd with ⟨z0, rfl⟩

Premises used: PythagoreanTriple.gcd_dvd, rfl
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y : ℤ
h0 : ¬x.gcd y = 0
z0 : ℤ
h : PythagoreanTriple x y ((↑(x.gcd y) : ℤ) * z0)
⊢ ∃ (k : ℕ) (x0 : ℤ) (y0 : ℤ), 0 < k ∧ x0.gcd y0 = 1 ∧ x = x0 * (↑k : ℤ) ∧ y = y0 * (↑k : ℤ)

Tactic:
Int.exists_gcd_one' (Nat.pos_of_ne_zero h0)

Premises used: Nat.pos_of_ne_zero, Int.exists_gcd_one'
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y : ℤ
h0 : ¬x.gcd y = 0
z0 : ℤ
h : PythagoreanTriple x y ((↑(x.gcd y) : ℤ) * z0)
neg :
  ∀ (k : ℕ) (x0 y0 : ℤ) (k0 : 0 < k) (h2 : x0.gcd y0 = 1) (h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0)
    (h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) ((↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ) * z0)),
    PythagoreanTriple (x0 * (↑k : ℤ) / (↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ))
      (y0 * (↑k : ℤ) / (↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ))
      ((↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ) * z0 / (↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ))
⊢ PythagoreanTriple (x / (↑(x.gcd y) : ℤ)) (y / (↑(x.gcd y) : ℤ)) ((↑(x.gcd y) : ℤ) * z0 / (↑(x.gcd y) : ℤ))

Tactic:
obtain ⟨k, x0, y0, k0, h2, rfl, rfl⟩ :
    ∃ (k : ℕ) (x0 y0 : _), 0 < k ∧ Int.gcd x0 y0 = 1 ∧ x = x0 * k ∧ y = y0 * k :=
    Int.exists_gcd_one' (Nat.pos_of_ne_zero h0)

Premises used: Nat.pos_of_ne_zero, Int.exists_gcd_one', rfl
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : x0.gcd y0 = 1
h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0
h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) ((↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ) * z0)
norm_cast : ¬k = 0
⊢ Ne (α := ℤ) (↑k : ℤ) 0

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : x0.gcd y0 = 1
h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0
h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) ((↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ) * z0)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (k0 : k ≠ 0) (h2 : x0.gcd y0 = 1) (h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0)
    (h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) ((↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ) * z0)), ¬k = 0
⊢ ¬k = 0

Tactic:
rwa [pos_iff_ne_zero] at k0

Premises used: pos_iff_ne_zero
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : x0.gcd y0 = 1
h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0
h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) ((↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ) * z0)
⊢ Ne (α := ℤ) (↑k : ℤ) 0

Tactic:
have hk : (k : ℤ) ≠ 0 := by
    norm_cast
    rwa [pos_iff_ne_zero] at k0
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : x0.gcd y0 = 1
h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0
h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) ((↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ) * z0)
hk : Ne (α := ℤ) (↑k : ℤ) 0
neg :
  ∀ (h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) ((↑k : ℤ) * z0)) (hk : Ne (α := ℤ) (↑k : ℤ) 0),
    PythagoreanTriple (x0 * (↑k : ℤ) / (↑k : ℤ)) (y0 * (↑k : ℤ) / (↑k : ℤ)) ((↑k : ℤ) * z0 / (↑k : ℤ))
⊢ PythagoreanTriple (x0 * (↑k : ℤ) / (↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ))
    (y0 * (↑k : ℤ) / (↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ))
    ((↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ) * z0 / (↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ))

Tactic:
rw [Int.gcd_mul_right, h2, Int.natAbs_natCast, one_mul] at h ⊢

Premises used: Int.gcd_mul_right, Int.natAbs_natCast, one_mul
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : x0.gcd y0 = 1
h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0
h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) ((↑k : ℤ) * z0)
hk : Ne (α := ℤ) (↑k : ℤ) 0
⊢ PythagoreanTriple x0 y0 z0

Tactic:
rw [mul_comm x0, mul_comm y0, mul_iff k hk] at h

Premises used: Nat.cast, PythagoreanTriple.mul_iff, mul_comm
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : x0.gcd y0 = 1
h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0
h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) ((↑k : ℤ) * z0)
hk : Ne (α := ℤ) (↑k : ℤ) 0
h₁ : PythagoreanTriple x0 y0 z0
⊢ Ne (α := ℤ) (↑k : ℤ) 0

Tactic:
rw [mul_comm x0, mul_comm y0, mul_iff k hk] at h

Premises used: Nat.cast, PythagoreanTriple.mul_iff, mul_comm
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : x0.gcd y0 = 1
h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0
h : PythagoreanTriple x0 y0 z0
hk : Ne (α := ℤ) (↑k : ℤ) 0
neg : PythagoreanTriple x0 (y0 * (↑k : ℤ) / (↑k : ℤ)) ((↑k : ℤ) * z0 / (↑k : ℤ))
neg₁ : PythagoreanTriple x0 y0 ((↑k : ℤ) * z0 / (↑k : ℤ))
neg₂ neg₃ neg₄ neg₅ : PythagoreanTriple x0 y0 z0
⊢ PythagoreanTriple (x0 * (↑k : ℤ) / (↑k : ℤ)) (y0 * (↑k : ℤ) / (↑k : ℤ)) ((↑k : ℤ) * z0 / (↑k : ℤ))

Tactic:
rwa [Int.mul_ediv_cancel _ hk, Int.mul_ediv_cancel _ hk, Int.mul_ediv_cancel_left _ hk]

Premises used: Int.mul_ediv_cancel, Int.mul_ediv_cancel_left
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hp : h.IsPrimitiveClassified
obtain :
  ∀ (m n : ℤ)
    (H :
      (x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n ∨
          x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
        m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)),
    h.IsClassified
⊢ h.IsClassified

Tactic:
obtain ⟨m, n, H⟩ := hp
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
m n : ℤ
H :
  (x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n ∨
      x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
    m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
h₁ :
  (x = 1 * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = 1 * (2 * m * n) ∨
      x = 1 * (2 * m * n) ∧ y = 1 * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
    m.gcd n = 1
⊢ h.IsClassified

Tactic:
use 1, m, n
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
m n : ℤ
H :
  (x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n ∨
      x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
    m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
⊢ (x = 1 * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = 1 * (2 * m * n) ∨
      x = 1 * (2 * m * n) ∧ y = 1 * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
    m.gcd n = 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
⊢ IsClassified (x := (↑(x.gcd y) : ℤ) * (x / (↑(x.gcd y) : ℤ))) ⋯

Tactic:
h.normalize.mul_isClassified (Int.gcd x y)
      (isClassified_of_isPrimitiveClassified h.normalize hc)

Premises used: Int.gcd, Nat.cast, PythagoreanTriple.mul_isClassified, PythagoreanTriple.normalize, PythagoreanTriple.isClassified_of_isPrimitiveClassified
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
h₁ : x = (↑(x.gcd y) : ℤ) * (x / (↑(x.gcd y) : ℤ))
h₂ : y = (↑(x.gcd y) : ℤ) * (y / (↑(x.gcd y) : ℤ))
h₃ : z = (↑(x.gcd y) : ℤ) * (z / (↑(x.gcd y) : ℤ))
⊢ h.IsClassified

Tactic:
convert!
    h.normalize.mul_isClassified (Int.gcd x y)
      (isClassified_of_isPrimitiveClassified h.normalize hc)

Premises used: Int.gcd, Nat.cast, PythagoreanTriple.mul_isClassified, PythagoreanTriple.normalize, PythagoreanTriple.isClassified_of_isPrimitiveClassified
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
h₁ : (↑(x.gcd y) : ℤ) ∣ x
⊢ x = (↑(x.gcd y) : ℤ) * (x / (↑(x.gcd y) : ℤ))

Tactic:
rw [Int.mul_ediv_cancel']

Premises used: Int.mul_ediv_cancel'
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
h₁ : (↑(x.gcd y) : ℤ) ∣ y
⊢ y = (↑(x.gcd y) : ℤ) * (y / (↑(x.gcd y) : ℤ))

Tactic:
rw [Int.mul_ediv_cancel']

Premises used: Int.mul_ediv_cancel'
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
h₁ : (↑(x.gcd y) : ℤ) ∣ z
⊢ z = (↑(x.gcd y) : ℤ) * (z / (↑(x.gcd y) : ℤ))

Tactic:
rw [Int.mul_ediv_cancel']

Premises used: Int.mul_ediv_cancel'
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
⊢ (↑(x.gcd y) : ℤ) ∣ x

Tactic:
Int.gcd_dvd_left ..

Premises used: Int.gcd_dvd_left
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
⊢ (↑(x.gcd y) : ℤ) ∣ x

Tactic:
exact Int.gcd_dvd_left ..

Premises used: Int.gcd_dvd_left
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
⊢ (↑(x.gcd y) : ℤ) ∣ y

Tactic:
Int.gcd_dvd_right ..

Premises used: Int.gcd_dvd_right
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
⊢ (↑(x.gcd y) : ℤ) ∣ y

Tactic:
exact Int.gcd_dvd_right ..

Premises used: Int.gcd_dvd_right
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
⊢ (↑(x.gcd y) : ℤ) ∣ z

Tactic:
h.gcd_dvd

Premises used: PythagoreanTriple.gcd_dvd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
⊢ (↑(x.gcd y) : ℤ) ∣ z

Tactic:
exact h.gcd_dvd

Premises used: PythagoreanTriple.gcd_dvd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y : ℤ
hc : x.gcd y = 1
h : PythagoreanTriple x y 0
this : 0 < HMul.hMul (α := ℤ) 0 0
⊢ False

Tactic:
norm_num at this
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
suffices : 0 < z * z
⊢ z ≠ 0

Tactic:
suffices 0 < z * z by
    rintro rfl
    norm_num at this
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
rw : 0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
⊢ 0 < z * z

Tactic:
rw [← h.eq, ← sq, ← sq]

Premises used: sq, PythagoreanTriple.eq
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
rw : Ne (α := ℕ) 1 0
⊢ x.gcd y ≠ 0

Tactic:
rw [hc]
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ Ne (α := ℕ) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ Ne (α := ℕ) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ x.gcd y ≠ 0

Tactic:
have hc' : Int.gcd x y ≠ 0 := by
    rw [hc]
    exact one_ne_zero
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hc' : x.gcd y ≠ 0
inl : ∀ (hxz : x ≠ 0), 0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
inr : ∀ (hyz : y ≠ 0), 0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
⊢ 0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2

Tactic:
rcases Int.ne_zero_of_gcd hc' with hxz | hyz

Premises used: Int.ne_zero_of_gcd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hc' : x.gcd y ≠ 0
hxz : x ≠ 0
⊢ 0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2

Tactic:
apply lt_add_of_pos_of_le (sq_pos_of_ne_zero hxz) (sq_nonneg y)

Premises used: lt_add_of_pos_of_le, sq_nonneg, sq_pos_of_ne_zero
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hc' : x.gcd y ≠ 0
hyz : y ≠ 0
⊢ 0 < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2

Tactic:
apply lt_add_of_le_of_pos (sq_nonneg x) (sq_pos_of_ne_zero hyz)

Premises used: sq_nonneg, lt_add_of_le_of_pos, sq_pos_of_ne_zero
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x = 0
subst : ∀ (h : PythagoreanTriple 0 y z) (hc : Int.gcd 0 y = 1), h.IsPrimitiveClassified
⊢ h.IsPrimitiveClassified

Tactic:
subst x
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Int.gcd 0 y = 1
⊢ Nat.gcd 0 y.natAbs = 1

Tactic:
change Nat.gcd 0 (Int.natAbs y) = 1 at hc

Premises used: Nat.gcd, Int.natAbs, OfNat.ofNat
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Nat.gcd 0 y.natAbs = 1
⊢ y.natAbs = 1

Tactic:
rw [Nat.gcd_zero_left (Int.natAbs y)] at hc

Premises used: Int.natAbs, Nat.gcd_zero_left
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
inl : ∀ (hy : y = (↑y.natAbs : ℤ)), h.IsPrimitiveClassified
inr : ∀ (hy : y = -(↑y.natAbs : ℤ)), h.IsPrimitiveClassified
⊢ h.IsPrimitiveClassified

Tactic:
rcases Int.natAbs_eq y with hy | hy

Premises used: Int.natAbs_eq
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = (↑y.natAbs : ℤ)
h₁ :
  (0 = HPow.hPow (α := ℤ) (β := ℕ) 1 2 - HPow.hPow (α := ℤ) (β := ℕ) 0 2 ∧ y = HMul.hMul (α := ℤ) 2 1 * 0 ∨
      0 = HMul.hMul (α := ℤ) 2 1 * 0 ∧ y = HPow.hPow (α := ℤ) (β := ℕ) 1 2 - HPow.hPow (α := ℤ) (β := ℕ) 0 2) ∧
    Int.gcd 1 0 = 1 ∧
      (HMod.hMod (α := ℤ) 1 2 = 0 ∧ HMod.hMod (α := ℤ) 0 2 = 1 ∨
        HMod.hMod (α := ℤ) 1 2 = 1 ∧ HMod.hMod (α := ℤ) 0 2 = 0)
⊢ h.IsPrimitiveClassified

Tactic:
use 1, 0
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = (↑y.natAbs : ℤ)
h₁ :
  (0 = HPow.hPow (α := ℤ) (β := ℕ) 1 2 - HPow.hPow (α := ℤ) (β := ℕ) 0 2 ∧ (↑1 : ℤ) = HMul.hMul (α := ℤ) 2 1 * 0 ∨
      0 = HMul.hMul (α := ℤ) 2 1 * 0 ∧ (↑1 : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) 1 2 - HPow.hPow (α := ℤ) (β := ℕ) 0 2) ∧
    Int.natAbs 1 = 1 ∧
      (HMod.hMod (α := ℤ) 1 2 = 0 ∧ HMod.hMod (α := ℤ) 0 2 = 1 ∨
        HMod.hMod (α := ℤ) 1 2 = 1 ∧ HMod.hMod (α := ℤ) 0 2 = 0)
⊢ (0 = HPow.hPow (α := ℤ) (β := ℕ) 1 2 - HPow.hPow (α := ℤ) (β := ℕ) 0 2 ∧ y = HMul.hMul (α := ℤ) 2 1 * 0 ∨
      0 = HMul.hMul (α := ℤ) 2 1 * 0 ∧ y = HPow.hPow (α := ℤ) (β := ℕ) 1 2 - HPow.hPow (α := ℤ) (β := ℕ) 0 2) ∧
    Int.gcd 1 0 = 1 ∧
      (HMod.hMod (α := ℤ) 1 2 = 0 ∧ HMod.hMod (α := ℤ) 0 2 = 1 ∨
        HMod.hMod (α := ℤ) 1 2 = 1 ∧ HMod.hMod (α := ℤ) 0 2 = 0)

Tactic:
rw [hy, hc, Int.gcd_zero_right]

Premises used: Int.gcd_zero_right
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = (↑y.natAbs : ℤ)
⊢ (0 = HPow.hPow (α := ℤ) (β := ℕ) 1 2 - HPow.hPow (α := ℤ) (β := ℕ) 0 2 ∧ (↑1 : ℤ) = HMul.hMul (α := ℤ) 2 1 * 0 ∨
      0 = HMul.hMul (α := ℤ) 2 1 * 0 ∧ (↑1 : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) 1 2 - HPow.hPow (α := ℤ) (β := ℕ) 0 2) ∧
    Int.natAbs 1 = 1 ∧
      (HMod.hMod (α := ℤ) 1 2 = 0 ∧ HMod.hMod (α := ℤ) 0 2 = 1 ∨
        HMod.hMod (α := ℤ) 1 2 = 1 ∧ HMod.hMod (α := ℤ) 0 2 = 0)

Tactic:
decide