awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h₁ :
  ∀ (h_pos : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2),
    z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
      (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
⊢ z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
    (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
have h₂ : ∀ (h_neg : z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)),
  z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
    (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
Tactic: rcases ht2 with h_pos | h_neg
Cleared hypotheses: ht2
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos_1 : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_pos : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
⊢ z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
    (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
have h₁ : (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
Tactic: apply And.intro h_pos
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos_1 : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_pos : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
⊢ (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
have h₁ : (-m).gcd (-n) = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos_1 : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_pos : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
h₁ : (-m).gcd (-n) = 1
⊢ (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
have h₂ : (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos_1 : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_pos : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
⊢ (-m).natAbs.gcd (-n).natAbs = 1
have h₁ : m.natAbs.gcd n.natAbs = 1
Tactic: rw [Int.natAbs_neg, Int.natAbs_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos_1 : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_pos : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
⊢ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
have h₁ : (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ -m
Tactic: rw [Int.neg_emod_two, Int.neg_emod_two]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos_1 : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_pos : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2
⊢ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ -m
have h₁ : 0 ≤ -m
Tactic: apply And.intro ht4
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_neg : z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
⊢ z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∧
    (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
have h₁ : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_neg : z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
⊢ False
have h₁ : ∀ (h_pos : 0 < z), False
Tactic: revert h_pos
Cleared hypotheses: h_pos
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2 ∧ y = 2 * m * n
h_neg : z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
⊢ ∀ (h_pos : 0 < z), False
have h₁ : ∀ (h_pos : 0 < -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)), False
Tactic: rw [h_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_even : x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
⊢ x = HPow.hPow (β := ℕ) (-m) 2 - HPow.hPow (β := ℕ) (-n) 2 ∧
    y = 2 * -m * -n ∧
      z = HPow.hPow (β := ℕ) (-m) 2 + HPow.hPow (β := ℕ) (-n) 2 ∧
        (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
have h₁ : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_even : x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
⊢ False
have h₁ : PythagoreanTriple (2 * m * n) y z
Tactic: rcases h_even with ⟨rfl, -⟩
Cleared hypotheses: x, h, h_coprime, h_parity, h_even
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_even : x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
h₁ : PythagoreanTriple (2 * m * n) y z
⊢ False
have h_coprime₁ : (2 * m * n).gcd y = 1
Tactic: rcases h_even with ⟨rfl, -⟩
Cleared hypotheses: x, h, h_coprime, h_parity, h_even
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_even : x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
h₁ : PythagoreanTriple (2 * m * n) y z
h_coprime₁ : (2 * m * n).gcd y = 1
⊢ False
have h_parity₁ : 2 * m * n % 2 = 1
Tactic: rcases h_even with ⟨rfl, -⟩
Cleared hypotheses: x, h, h_coprime, h_parity, h_even
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
y z : ℤ
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h : PythagoreanTriple (2 * m * n) y z
h_coprime : (2 * m * n).gcd y = 1
h_parity : 2 * m * n % 2 = 1
⊢ False
have h_parity₁ : Eq (α := ℤ) 0 1
Tactic: rw [mul_assoc, Int.mul_emod_right] at h_parity
Cleared hypotheses: h_parity
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
⊢ PythagoreanTriple x y z ↔
    ∃ (k : ℤ) (m : ℤ) (n : ℤ),
      (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
          x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
        (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
          z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))
have mp : PythagoreanTriple x y z →
  ∃ (k : ℤ) (m : ℤ) (n : ℤ),
    (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
        x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
      (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
        z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
mp :
  PythagoreanTriple x y z →
    ∃ (k : ℤ) (m : ℤ) (n : ℤ),
      (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
          x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
        (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
          z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))
⊢ PythagoreanTriple x y z ↔
    ∃ (k : ℤ) (m : ℤ) (n : ℤ),
      (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
          x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
        (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
          z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))
have mpr : (∃ (k : ℤ) (m : ℤ) (n : ℤ),
    (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
        x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
      (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
        z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))) →
  PythagoreanTriple x y z
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
⊢ ∃ (k : ℤ) (m : ℤ) (n : ℤ),
    (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
        x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
      (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
        z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))
have mp : ∀ (k m n : ℤ)
  (H :
    (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
        x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
      m.gcd n = 1),
  ∃ (k : ℤ) (m : ℤ) (n : ℤ),
    (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
        x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
      (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
        z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))
Tactic: obtain ⟨k, m, n, H⟩ := h.classified
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
k m n : ℤ
H :
  (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
      x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
    m.gcd n = 1
⊢ ∃ (k : ℤ) (m : ℤ) (n : ℤ),
    (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
        x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
      (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
        z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))
have h₁ : (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
    x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
  (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
    z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))
Tactic: use k, m, n
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
k m n : ℤ
H :
  (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
      x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
    m.gcd n = 1
⊢ (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
      x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
    (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
      z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))
have h₁ : m.gcd n = 1 →
  ∀ (h : PythagoreanTriple (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) (k * (2 * m * n)) z),
    (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
          k * (2 * m * n) = k * (2 * m * n) ∨
        k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = k * (2 * m * n) ∧
          k * (2 * m * n) = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
      (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
        z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))
Tactic: rcases H with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
Cleared hypotheses: x, y, h, H
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
k m n : ℤ
H :
  (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
      x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
    m.gcd n = 1
h₁ :
  m.gcd n = 1 →
    ∀ (h : PythagoreanTriple (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) (k * (2 * m * n)) z),
      (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
            k * (2 * m * n) = k * (2 * m * n) ∨
          k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = k * (2 * m * n) ∧
            k * (2 * m * n) = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
        (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
          z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))
⊢ (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
      x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
    (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
      z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))
have h₂ : m.gcd n = 1 →
  ∀ (h : PythagoreanTriple (k * (2 * m * n)) (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) z),
    (k * (2 * m * n) = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
          k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = k * (2 * m * n) ∨
        k * (2 * m * n) = k * (2 * m * n) ∧
          k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) =
            k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
      (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
        z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))
Tactic: rcases H with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
Cleared hypotheses: x, y, h, H
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
z k m n : ℤ
right : m.gcd n = 1
h : PythagoreanTriple (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) (k * (2 * m * n)) z
⊢ (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
        k * (2 * m * n) = k * (2 * m * n) ∨
      k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = k * (2 * m * n) ∧
        k * (2 * m * n) = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
    (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
      z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))
have h₁ : z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨ z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
Tactic: refine ⟨Or.inl ⟨rfl, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
z k m n : ℤ
right : m.gcd n = 1
h : PythagoreanTriple (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) (k * (2 * m * n)) z
⊢ HPow.hPow (β := ℕ) z 2 = HPow.hPow (β := ℕ) (k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)) 2
have rw : k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) +
    k * (2 * m * n) * (k * (2 * m * n)) =
  HPow.hPow (β := ℕ) (k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)) 2
Tactic: rw [sq, ← h.eq]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
z k m n : ℤ
right : m.gcd n = 1
h : PythagoreanTriple (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) (k * (2 * m * n)) z
⊢ z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨ z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
have this : HPow.hPow (β := ℕ) z 2 = HPow.hPow (β := ℕ) (k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)) 2
Tactic: have : z ^ 2 = (k * (m ^ 2 + n ^ 2)) ^ 2 := by
        rw [sq, ← h.eq]
        ring
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
z k m n : ℤ
right : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) z
⊢ (k * (2 * m * n) = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
        k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = k * (2 * m * n) ∨
      k * (2 * m * n) = k * (2 * m * n) ∧
        k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
    (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
      z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))
have h₁ : z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨ z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
Tactic: refine ⟨Or.inr ⟨rfl, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
z k m n : ℤ
right : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) z
⊢ HPow.hPow (β := ℕ) z 2 = HPow.hPow (β := ℕ) (k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)) 2
have rw : k * (2 * m * n) * (k * (2 * m * n)) +
    k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) =
  HPow.hPow (β := ℕ) (k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)) 2
Tactic: rw [sq, ← h.eq]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
z k m n : ℤ
right : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) z
⊢ z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨ z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
have this : HPow.hPow (β := ℕ) z 2 = HPow.hPow (β := ℕ) (k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)) 2
Tactic: have : z ^ 2 = (k * (m ^ 2 + n ^ 2)) ^ 2 := by
        rw [sq, ← h.eq]
        ring
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
⊢ Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
have rw : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L)
  (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap R K)) : (a : R) → L)
Tactic: rw [IsScalarTower.algebraMap_eq R K L]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
⊢ Eq.{u_2 + 1} (α := Submodule K L) (Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' b)) ⊤
have hRL : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
Tactic: have hRL : Function.Injective (algebraMap R L) := by
    rw [IsScalarTower.algebraMap_eq R K L]
    exact (algebraMap K L).injective.comp (FaithfulSMul.algebraMap_injective R K)
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
hRL : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
M : Submodule R S := Submodule.span R b
⊢ Eq.{u_2 + 1} (α := Submodule K L) (Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' b)) ⊤
have obtain : ∀ (n : ℕ) (a : Fin n → S ⧸ M) (ha : Eq (α := Submodule R (S ⧸ M)) (Submodule.span R (Set.range a)) ⊤),
  Eq.{u_2 + 1} (α := Submodule K L) (Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' b)) ⊤
Tactic: obtain ⟨n, a, ha⟩ := @Module.Finite.exists_fin R (S ⧸ M) _ _ _ _