-- 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
⊢ (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 = 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
Tactic: tauto
Cleared hypotheses: h2, H