-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem mul_isClassified (k : ℤ) (hc : h.IsClassified) : (h.mul k).IsClassified

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
k : ℤ
hc : h.IsClassified
⊢ ⋯.IsClassified

Tactic:
obtain ⟨l, m, n, ⟨⟨rfl, rfl⟩ | ⟨rfl, rfl⟩, co⟩⟩ := hc

Result:
case intro.intro.intro.intro.inl.intro
z k l m n : ℤ
co : m.gcd n = 1
h : PythagoreanTriple (l * (m ^ 2 - n ^ 2)) (l * (2 * m * n)) z
⊢ ⋯.IsClassified

case intro.intro.intro.intro.inr.intro
z k l m n : ℤ
co : m.gcd n = 1
h : PythagoreanTriple (l * (2 * m * n)) (l * (m ^ 2 - n ^ 2)) z
⊢ ⋯.IsClassified

Proof state:
case h
z k l m n : ℤ
co : m.gcd n = 1
h : PythagoreanTriple (l * (m ^ 2 - n ^ 2)) (l * (2 * m * n)) z
⊢ k * (l * (m ^ 2 - n ^ 2)) = k * l * (m ^ 2 - n ^ 2) ∧ k * (l * (2 * m * n)) = k * l * (2 * m * n)

Tactic:
constructor <;> ring

Result:
no goals

Proof state:
case intro.intro.intro.intro.inl.intro
z k l m n : ℤ
co : m.gcd n = 1
h : PythagoreanTriple (l * (m ^ 2 - n ^ 2)) (l * (2 * m * n)) z
⊢ ⋯.IsClassified

Tactic:
use k * l, m, n

Result:
case h
z k l m n : ℤ
co : m.gcd n = 1
h : PythagoreanTriple (l * (m ^ 2 - n ^ 2)) (l * (2 * m * n)) z
⊢ (k * (l * (m ^ 2 - n ^ 2)) = k * l * (m ^ 2 - n ^ 2) ∧ k * (l * (2 * m * n)) = k * l * (2 * m * n) ∨
      k * (l * (m ^ 2 - n ^ 2)) = k * l * (2 * m * n) ∧ k * (l * (2 * m * n)) = k * l * (m ^ 2 - n ^ 2)) ∧
    m.gcd n = 1

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

Tactic:
apply And.intro _ co

Result:
z k l m n : ℤ
co : m.gcd n = 1
h : PythagoreanTriple (l * (2 * m * n)) (l * (m ^ 2 - n ^ 2)) z
⊢ k * (l * (2 * m * n)) = k * l * (m ^ 2 - n ^ 2) ∧ k * (l * (m ^ 2 - n ^ 2)) = k * l * (2 * m * n) ∨
    k * (l * (2 * m * n)) = k * l * (2 * m * n) ∧ k * (l * (m ^ 2 - n ^ 2)) = k * l * (m ^ 2 - n ^ 2)

Proof state:
case h
z k l m n : ℤ
co : m.gcd n = 1
h : PythagoreanTriple (l * (2 * m * n)) (l * (m ^ 2 - n ^ 2)) z
⊢ k * (l * (2 * m * n)) = k * l * (2 * m * n) ∧ k * (l * (m ^ 2 - n ^ 2)) = k * l * (m ^ 2 - n ^ 2)

Tactic:
constructor <;> ring

Result:
no goals

Proof state:
z k l m n : ℤ
co : m.gcd n = 1
h : PythagoreanTriple (l * (2 * m * n)) (l * (m ^ 2 - n ^ 2)) z
⊢ k * (l * (2 * m * n)) = k * l * (m ^ 2 - n ^ 2) ∧ k * (l * (m ^ 2 - n ^ 2)) = k * l * (2 * m * n) ∨
    k * (l * (2 * m * n)) = k * l * (2 * m * n) ∧ k * (l * (m ^ 2 - n ^ 2)) = k * l * (m ^ 2 - n ^ 2)

Tactic:
right

Result:
case h
z k l m n : ℤ
co : m.gcd n = 1
h : PythagoreanTriple (l * (2 * m * n)) (l * (m ^ 2 - n ^ 2)) z
⊢ k * (l * (2 * m * n)) = k * l * (2 * m * n) ∧ k * (l * (m ^ 2 - n ^ 2)) = k * l * (m ^ 2 - n ^ 2)

Proof state:
z k l m n : ℤ
co : m.gcd n = 1
h : PythagoreanTriple (l * (m ^ 2 - n ^ 2)) (l * (2 * m * n)) z
⊢ k * (l * (m ^ 2 - n ^ 2)) = k * l * (m ^ 2 - n ^ 2) ∧ k * (l * (2 * m * n)) = k * l * (2 * m * n) ∨
    k * (l * (m ^ 2 - n ^ 2)) = k * l * (2 * m * n) ∧ k * (l * (2 * m * n)) = k * l * (m ^ 2 - n ^ 2)

Tactic:
left

Result:
case h
z k l m n : ℤ
co : m.gcd n = 1
h : PythagoreanTriple (l * (m ^ 2 - n ^ 2)) (l * (2 * m * n)) z
⊢ k * (l * (m ^ 2 - n ^ 2)) = k * l * (m ^ 2 - n ^ 2) ∧ k * (l * (2 * m * n)) = k * l * (2 * m * n)

Proof state:
case intro.intro.intro.intro.inr.intro
z k l m n : ℤ
co : m.gcd n = 1
h : PythagoreanTriple (l * (2 * m * n)) (l * (m ^ 2 - n ^ 2)) z
⊢ ⋯.IsClassified

Tactic:
use k * l, m, n

Result:
case h
z k l m n : ℤ
co : m.gcd n = 1
h : PythagoreanTriple (l * (2 * m * n)) (l * (m ^ 2 - n ^ 2)) z
⊢ (k * (l * (2 * m * n)) = k * l * (m ^ 2 - n ^ 2) ∧ k * (l * (m ^ 2 - n ^ 2)) = k * l * (2 * m * n) ∨
      k * (l * (2 * m * n)) = k * l * (2 * m * n) ∧ k * (l * (m ^ 2 - n ^ 2)) = k * l * (m ^ 2 - n ^ 2)) ∧
    m.gcd n = 1

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

Tactic:
apply And.intro _ co

Result:
z k l m n : ℤ
co : m.gcd n = 1
h : PythagoreanTriple (l * (m ^ 2 - n ^ 2)) (l * (2 * m * n)) z
⊢ k * (l * (m ^ 2 - n ^ 2)) = k * l * (m ^ 2 - n ^ 2) ∧ k * (l * (2 * m * n)) = k * l * (2 * m * n) ∨
    k * (l * (m ^ 2 - n ^ 2)) = k * l * (2 * m * n) ∧ k * (l * (2 * m * n)) = k * l * (m ^ 2 - n ^ 2)