-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem classification :
    PythagoreanTriple x y z ↔
      ∃ k m n,
        (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨
            x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
          (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

Proof state:
case h.intro.inr.intro
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) z
this : z ^ 2 = (k * (m ^ 2 + n ^ 2)) ^ 2
⊢ z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2)

Tactic:
simpa using eq_or_eq_neg_of_sq_eq_sq _ _ this

Result:
no goals

Proof state:
case mp
x y z : ℤ
⊢ PythagoreanTriple x y z →
    ∃ k m n,
      (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
        (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

Tactic:
intro h

Result:
case mp
x y z : ℤ
h : PythagoreanTriple x y z
⊢ ∃ k m n,
    (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
      (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

Proof state:
case mp.intro.intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
k m n : ℤ
H : (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧ m.gcd n = 1
⊢ ∃ k m n,
    (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
      (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

Tactic:
use k, m, n

Result:
case h
x y z : ℤ
h : PythagoreanTriple x y z
k m n : ℤ
H : (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧ m.gcd n = 1
⊢ (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
    (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

Proof state:
case h.intro.inr.intro
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) z
⊢ (k * (2 * m * n) = k * (m ^ 2 - n ^ 2) ∧ k * (m ^ 2 - n ^ 2) = k * (2 * m * n) ∨
      k * (2 * m * n) = k * (2 * m * n) ∧ k * (m ^ 2 - n ^ 2) = k * (m ^ 2 - n ^ 2)) ∧
    (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

Tactic:
refine ⟨Or.inr ⟨rfl, rfl⟩, ?_⟩

Result:
case h.intro.inr.intro
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) z
⊢ z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2)

Proof state:
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) z
⊢ k * (2 * m * n) * (k * (2 * m * n)) + k * (m ^ 2 - n ^ 2) * (k * (m ^ 2 - n ^ 2)) = (k * (m ^ 2 + n ^ 2)) ^ 2

Tactic:
ring

Result:
no goals

Proof state:
case h.intro.inl.intro
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (m ^ 2 - n ^ 2)) (k * (2 * m * n)) z
this : z ^ 2 = (k * (m ^ 2 + n ^ 2)) ^ 2
⊢ z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2)

Tactic:
simpa using eq_or_eq_neg_of_sq_eq_sq _ _ this

Result:
no goals

Proof state:
case h.intro.inl.intro
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (m ^ 2 - n ^ 2)) (k * (2 * m * n)) z
⊢ (k * (m ^ 2 - n ^ 2) = k * (m ^ 2 - n ^ 2) ∧ k * (2 * m * n) = k * (2 * m * n) ∨
      k * (m ^ 2 - n ^ 2) = k * (2 * m * n) ∧ k * (2 * m * n) = k * (m ^ 2 - n ^ 2)) ∧
    (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

Tactic:
refine ⟨Or.inl ⟨rfl, rfl⟩, ?_⟩

Result:
case h.intro.inl.intro
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (m ^ 2 - n ^ 2)) (k * (2 * m * n)) z
⊢ z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2)

Proof state:
case h
x y z : ℤ
h : PythagoreanTriple x y z
k m n : ℤ
H : (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧ m.gcd n = 1
⊢ (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
    (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

Tactic:
rcases H with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)

Result:
case h.intro.inl.intro
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (m ^ 2 - n ^ 2)) (k * (2 * m * n)) z
⊢ (k * (m ^ 2 - n ^ 2) = k * (m ^ 2 - n ^ 2) ∧ k * (2 * m * n) = k * (2 * m * n) ∨
      k * (m ^ 2 - n ^ 2) = k * (2 * m * n) ∧ k * (2 * m * n) = k * (m ^ 2 - n ^ 2)) ∧
    (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

case h.intro.inr.intro
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) z
⊢ (k * (2 * m * n) = k * (m ^ 2 - n ^ 2) ∧ k * (m ^ 2 - n ^ 2) = k * (2 * m * n) ∨
      k * (2 * m * n) = k * (2 * m * n) ∧ k * (m ^ 2 - n ^ 2) = k * (m ^ 2 - n ^ 2)) ∧
    (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

Proof state:
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) z
⊢ z ^ 2 = (k * (m ^ 2 + n ^ 2)) ^ 2

Tactic:
rw [sq, ← h.eq]

Result:
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) z
⊢ k * (2 * m * n) * (k * (2 * m * n)) + k * (m ^ 2 - n ^ 2) * (k * (m ^ 2 - n ^ 2)) = (k * (m ^ 2 + n ^ 2)) ^ 2

Proof state:
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (m ^ 2 - n ^ 2)) (k * (2 * m * n)) z
⊢ z ^ 2 = (k * (m ^ 2 + n ^ 2)) ^ 2

Tactic:
rw [sq, ← h.eq]

Result:
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (m ^ 2 - n ^ 2)) (k * (2 * m * n)) z
⊢ k * (m ^ 2 - n ^ 2) * (k * (m ^ 2 - n ^ 2)) + k * (2 * m * n) * (k * (2 * m * n)) = (k * (m ^ 2 + n ^ 2)) ^ 2

Proof state:
x y z : ℤ
⊢ PythagoreanTriple x y z ↔
    ∃ k m n,
      (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
        (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

Tactic:
constructor

Result:
case mp
x y z : ℤ
⊢ PythagoreanTriple x y z →
    ∃ k m n,
      (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
        (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

case mpr
x y z : ℤ
⊢ (∃ k m n,
      (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
        (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))) →
    PythagoreanTriple x y z

Proof state:
case h.intro.inl.intro
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (m ^ 2 - n ^ 2)) (k * (2 * m * n)) z
⊢ z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2)

Tactic:
have : z ^ 2 = (k * (m ^ 2 + n ^ 2)) ^ 2 := by
  rw [sq, ← h.eq]
  ring

Result:
case h.intro.inl.intro
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (m ^ 2 - n ^ 2)) (k * (2 * m * n)) z
this : z ^ 2 = (k * (m ^ 2 + n ^ 2)) ^ 2
⊢ z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2)

Proof state:
case mpr
x y z : ℤ
⊢ (∃ k m n,
      (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
        (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))) →
    PythagoreanTriple x y z

Tactic:
rintro ⟨k, m, n, ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩, rfl | rfl⟩ <;> delta PythagoreanTriple <;> ring

Result:
no goals

Proof state:
case h.intro.inr.intro
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) z
⊢ z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2)

Tactic:
have : z ^ 2 = (k * (m ^ 2 + n ^ 2)) ^ 2 := by
  rw [sq, ← h.eq]
  ring

Result:
case h.intro.inr.intro
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) z
this : z ^ 2 = (k * (m ^ 2 + n ^ 2)) ^ 2
⊢ z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2)