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

case intro.intro.intro.intro.inr.intro
z k l m n : ℤ
co : Int.gcd m n = 1
h : PythagoreanTriple (l * (2 * m * n)) (l * (m ^ 2 - n ^ 2)) z
⊢ IsClassified (_ : PythagoreanTriple (k * (l * (2 * m * n))) (k * (l * (m ^ 2 - n ^ 2))) (k * z))
x y z : ℤ
h : PythagoreanTriple x y z
k : ℤ
hc : IsClassified h
⊢ IsClassified (_ : PythagoreanTriple (k * x) (k * y) (k * z))
obtain ⟨l, m, n, ⟨⟨rfl, rfl⟩ | ⟨rfl, rfl⟩, co⟩⟩ := hc
case intro.intro.intro.intro.inl.intro
z k l m n : ℤ
co : Int.gcd m 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)) ∧
    Int.gcd m n = 1
case intro.intro.intro.intro.inl.intro
z k l m n : ℤ
co : Int.gcd m n = 1
h : PythagoreanTriple (l * (m ^ 2 - n ^ 2)) (l * (2 * m * n)) z
⊢ IsClassified (_ : PythagoreanTriple (k * (l * (m ^ 2 - n ^ 2))) (k * (l * (2 * m * n))) (k * z))
use k * l, m, n
z k l m n : ℤ
co : Int.gcd m 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)
case intro.intro.intro.intro.inl.intro
z k l m n : ℤ
co : Int.gcd m 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)) ∧
    Int.gcd m n = 1
apply And.intro _ co
case h
z k l m n : ℤ
co : Int.gcd m 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)
z k l m n : ℤ
co : Int.gcd m 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)
left
no goals
case h
z k l m n : ℤ
co : Int.gcd m 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)
constructor <;> ring
case intro.intro.intro.intro.inr.intro
z k l m n : ℤ
co : Int.gcd m 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)) ∧
    Int.gcd m n = 1
case intro.intro.intro.intro.inr.intro
z k l m n : ℤ
co : Int.gcd m n = 1
h : PythagoreanTriple (l * (2 * m * n)) (l * (m ^ 2 - n ^ 2)) z
⊢ IsClassified (_ : PythagoreanTriple (k * (l * (2 * m * n))) (k * (l * (m ^ 2 - n ^ 2))) (k * z))
use k * l, m, n
z k l m n : ℤ
co : Int.gcd m 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)
case intro.intro.intro.intro.inr.intro
z k l m n : ℤ
co : Int.gcd m 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)) ∧
    Int.gcd m n = 1
apply And.intro _ co
case h
z k l m n : ℤ
co : Int.gcd m 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)
z k l m n : ℤ
co : Int.gcd m 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)
right
no goals
case h
z k l m n : ℤ
co : Int.gcd m 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)
constructor <;> ring