-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : y.gcd x = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
m n : ℤ
H :
  (y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ x = 2 * m * n ∨
      y = 2 * m * n ∧ x = 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 % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n →
            m % 2 = 0 →
              n % 2 = 1 →
                (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 % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n →
            m % 2 = 1 →
              n % 2 = 0 →
                (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 % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = 2 * m * n →
          x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
            m % 2 = 0 →
              n % 2 = 1 →
                (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 % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = 2 * m * n →
          x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
            m % 2 = 1 →
              n % 2 = 0 →
                (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 % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n →
            m % 2 = 0 →
              n % 2 = 1 →
                (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 % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n →
            m % 2 = 1 →
              n % 2 = 0 →
                (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 % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = 2 * m * n →
          x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
            m % 2 = 0 →
              n % 2 = 1 →
                (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 % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = 2 * m * n →
          x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
            m % 2 = 1 →
              n % 2 = 0 →
                (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 % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n →
            m % 2 = 0 →
              n % 2 = 1 →
                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
h₁₀ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 → x = 2 * m * n → m % 2 = 0 → n % 2 = 1 → m.gcd n = 1
h₁₁ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n → m % 2 = 0 → n % 2 = 1 → m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
h₁₂ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n →
            m % 2 = 1 →
              n % 2 = 0 →
                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
h₁₃ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 → x = 2 * m * n → m % 2 = 1 → n % 2 = 0 → m.gcd n = 1
h₁₄ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n → m % 2 = 1 → n % 2 = 0 → m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
h₁₅ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = 2 * m * n →
          x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
            m % 2 = 0 →
              n % 2 = 1 →
                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
h₁₆ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = 2 * m * n → x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 → m % 2 = 0 → n % 2 = 1 → m.gcd n = 1
h₁₇ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = 2 * m * n →
          x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
            m % 2 = 0 → n % 2 = 1 → m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
h₁₈ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = 2 * m * n →
          x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
            m % 2 = 1 →
              n % 2 = 0 →
                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
h₁₉ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = 2 * m * n → x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 → m % 2 = 1 → n % 2 = 0 → m.gcd n = 1
h₂₀ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = 2 * m * n →
          x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
            m % 2 = 1 → n % 2 = 0 → m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
h₂₁ h₂₂ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n →
            m % 2 = 0 →
              n % 2 = 1 →
                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
h₂₃ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n →
            m % 2 = 0 →
              n % 2 = 1 → ¬(x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n) → x = 2 * m * n
h₂₄ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n →
            m % 2 = 0 →
              n % 2 = 1 →
                ¬(x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n) →
                  y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
h₂₅ h₂₆ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n → m % 2 = 0 → n % 2 = 1 → m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
h₂₇ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n → m % 2 = 0 → n % 2 = 1 → ¬(m % 2 = 0 ∧ n % 2 = 1) → m % 2 = 1
h₂₈ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n → m % 2 = 0 → n % 2 = 1 → ¬(m % 2 = 0 ∧ n % 2 = 1) → n % 2 = 0
h₂₉ h₃₀ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n →
            m % 2 = 1 →
              n % 2 = 0 →
                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
h₃₁ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n →
            m % 2 = 1 →
              n % 2 = 0 → ¬(x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n) → x = 2 * m * n
h₃₂ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n →
            m % 2 = 1 →
              n % 2 = 0 →
                ¬(x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n) →
                  y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
h₃₃ h₃₄ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n → m % 2 = 1 → n % 2 = 0 → m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
h₃₅ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n → m % 2 = 1 → n % 2 = 0 → ¬(m % 2 = 0 ∧ n % 2 = 1) → m % 2 = 1
h₃₆ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n → m % 2 = 1 → n % 2 = 0 → ¬(m % 2 = 0 ∧ n % 2 = 1) → n % 2 = 0
h₃₇ h₃₈ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = 2 * m * n →
          x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
            m % 2 = 0 →
              n % 2 = 1 →
                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
h₃₉ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = 2 * m * n →
          x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
            m % 2 = 0 →
              n % 2 = 1 → ¬(x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n) → x = 2 * m * n
h₄₀ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = 2 * m * n →
          x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
            m % 2 = 0 →
              n % 2 = 1 →
                ¬(x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n) →
                  y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
h₄₁ h₄₂ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = 2 * m * n →
          x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
            m % 2 = 0 → n % 2 = 1 → m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
h₄₃ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = 2 * m * n →
          x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
            m % 2 = 0 → n % 2 = 1 → ¬(m % 2 = 0 ∧ n % 2 = 1) → m % 2 = 1
h₄₄ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = 2 * m * n →
          x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
            m % 2 = 0 → n % 2 = 1 → ¬(m % 2 = 0 ∧ n % 2 = 1) → n % 2 = 0
h₄₅ h₄₆ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = 2 * m * n →
          x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
            m % 2 = 1 →
              n % 2 = 0 →
                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
h₄₇ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = 2 * m * n →
          x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
            m % 2 = 1 →
              n % 2 = 0 → ¬(x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n) → x = 2 * m * n
h₄₈ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = 2 * m * n →
          x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
            m % 2 = 1 →
              n % 2 = 0 →
                ¬(x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n) →
                  y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
h₄₉ h₅₀ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = 2 * m * n →
          x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
            m % 2 = 1 → n % 2 = 0 → m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
h₅₁ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = 2 * m * n →
          x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
            m % 2 = 1 → n % 2 = 0 → ¬(m % 2 = 0 ∧ n % 2 = 1) → m % 2 = 1
h₅₂ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = 2 * m * n →
          x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
            m % 2 = 1 → n % 2 = 0 → ¬(m % 2 = 0 ∧ n % 2 = 1) → n % 2 = 0
h₅₃ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n → m % 2 = 0 → n % 2 = 1 → ¬m % 2 = 0 → m % 2 = 1
h₅₄ :
  x % 2 = 1 →
    y % 2 = 0 →
      m.gcd n = 1 →
        y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
          x = 2 * m * n → m % 2 = 0 → n % 2 = 1 → ¬n % 2 = 1 → m % 2 = 1
⊢ (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)
have h₅₅ : x % 2 = 1 →
  y % 2 = 0 →
    m.gcd n = 1 →
      y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 →
        x = 2 * m * n → m % 2 = 0 → n % 2 = 1 → ¬m % 2 = 0 → n % 2 = 0
Tactic: tauto
Cleared hypotheses: h2, H