awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
m : ℕ
ihn : ∀ m_1 < m + m + 1, ∀ (hn : m_1 ≠ 0), m_1# < HPow.hPow (α := ℕ) 4 m_1
hn : m + m + 1 ≠ 0
hm : m > 0
⊢ (m + 1)# * (m + 1 + m).choose (m + 1) = (m + 1)# * (2 * m + 1).choose m
have rw : (m + 1)# * (m + 1 + m).choose m = (m + 1)# * (2 * m + 1).choose m
Tactic: rw [choose_symm_add, two_mul, add_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
m : ℕ
ihn : ∀ m_1 < m + m + 1, ∀ (hn : m_1 ≠ 0), m_1# < HPow.hPow (α := ℕ) 4 m_1
hn : m + m + 1 ≠ 0
hm : m > 0
rw : (m + 1)# * (m + 1 + m).choose m = (m + 1)# * (2 * m + 1).choose m
⊢ (m + 1)# * (m + 1 + m).choose (m + 1) = (m + 1)# * (2 * m + 1).choose m
have rw₁ : (m + 1)# * (m + 1 + m).choose m = (m + 1)# * (m + m + 1).choose m
Tactic: rw [choose_symm_add, two_mul, add_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
m : ℕ
ihn : ∀ m_1 < m + m + 1, ∀ (hn : m_1 ≠ 0), m_1# < HPow.hPow (α := ℕ) 4 m_1
hn : m + m + 1 ≠ 0
hm : m > 0
rw : (m + 1)# * (m + 1 + m).choose m = (m + 1)# * (2 * m + 1).choose m
rw₁ : (m + 1)# * (m + 1 + m).choose m = (m + 1)# * (m + m + 1).choose m
⊢ (m + 1)# * (m + 1 + m).choose (m + 1) = (m + 1)# * (2 * m + 1).choose m
have rw₂ : (m + 1)# * (m + m + 1).choose m = (m + 1)# * (m + m + 1).choose m
Tactic: rw [choose_symm_add, two_mul, add_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
m : ℕ
ihn : ∀ m_1 < m + m + 1, ∀ (hn : m_1 ≠ 0), m_1# < HPow.hPow (α := ℕ) 4 m_1
hn : m + m + 1 ≠ 0
hm : m > 0
⊢ HPow.hPow (α := ℕ) 4 (m + 1) * HPow.hPow (α := ℕ) 4 m ≤ HPow.hPow (α := ℕ) 4 (m + m + 1)
have rw : HPow.hPow (α := ℕ) 4 (m + 1 + m) ≤ HPow.hPow (α := ℕ) 4 (m + m + 1)
Tactic: rw [← pow_add, add_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
m : ℕ
ihn : ∀ m_1 < m + m + 1, ∀ (hn : m_1 ≠ 0), m_1# < HPow.hPow (α := ℕ) 4 m_1
hn : m + m + 1 ≠ 0
hm : m > 0
rw : HPow.hPow (α := ℕ) 4 (m + 1 + m) ≤ HPow.hPow (α := ℕ) 4 (m + m + 1)
⊢ HPow.hPow (α := ℕ) 4 (m + 1) * HPow.hPow (α := ℕ) 4 m ≤ HPow.hPow (α := ℕ) 4 (m + m + 1)
have rw₁ : HPow.hPow (α := ℕ) 4 (m + m + 1) ≤ HPow.hPow (α := ℕ) 4 (m + m + 1)
Tactic: rw [← pow_add, add_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
m : ℕ
ihn : ∀ m_1 < m + m + 1, ∀ (hn : m_1 ≠ 0), m_1# < HPow.hPow (α := ℕ) 4 m_1
hn : m + m + 1 ≠ 0
hm : m > 0
⊢ (m + m + 1)# < HPow.hPow (α := ℕ) 4 (m + m + 1)
have m₁ : (m + m + 1)# = (m + 1 + m)#
Tactic: calc
      (m + m + 1)# = (m + 1 + m)# := by rw [add_right_comm]
      _ ≤ (m + 1)# * choose (m + 1 + m) (m + 1) := primorial_add_le m.le_succ
      _ = (m + 1)# * choose (2 * m + 1) m := by rw [choose_symm_add, two_mul, add_right_comm]
      _ < 4 ^ (m + 1) * 4 ^ m :=
        Nat.mul_lt_mul_of_lt_of_le (ihn _ (by lia) (by lia)) (choose_middle_le_pow _) (by simp)
      _ ≤ 4 ^ (m + m + 1) := by rw [← pow_add, add_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
m : ℕ
ihn : ∀ m_1 < m + m + 1, ∀ (hn : m_1 ≠ 0), m_1# < HPow.hPow (α := ℕ) 4 m_1
hn : m + m + 1 ≠ 0
hm : m > 0
m₁ : (m + m + 1)# = (m + 1 + m)#
⊢ (m + m + 1)# < HPow.hPow (α := ℕ) 4 (m + m + 1)
have m₂ : (m + 1)# * (m + 1 + m).choose (m + 1) = (m + 1)# * (2 * m + 1).choose m
Tactic: calc
      (m + m + 1)# = (m + 1 + m)# := by rw [add_right_comm]
      _ ≤ (m + 1)# * choose (m + 1 + m) (m + 1) := primorial_add_le m.le_succ
      _ = (m + 1)# * choose (2 * m + 1) m := by rw [choose_symm_add, two_mul, add_right_comm]
      _ < 4 ^ (m + 1) * 4 ^ m :=
        Nat.mul_lt_mul_of_lt_of_le (ihn _ (by lia) (by lia)) (choose_middle_le_pow _) (by simp)
      _ ≤ 4 ^ (m + m + 1) := by rw [← pow_add, add_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
m : ℕ
ihn : ∀ m_1 < m + m + 1, ∀ (hn : m_1 ≠ 0), m_1# < HPow.hPow (α := ℕ) 4 m_1
hn : m + m + 1 ≠ 0
hm : m > 0
m₁ : (m + m + 1)# = (m + 1 + m)#
m₂ : (m + 1)# * (m + 1 + m).choose (m + 1) = (m + 1)# * (2 * m + 1).choose m
⊢ (m + m + 1)# < HPow.hPow (α := ℕ) 4 (m + m + 1)
have m₃ : HPow.hPow (α := ℕ) 4 (m + 1) * HPow.hPow (α := ℕ) 4 m ≤ HPow.hPow (α := ℕ) 4 (m + m + 1)
Tactic: calc
      (m + m + 1)# = (m + 1 + m)# := by rw [add_right_comm]
      _ ≤ (m + 1)# * choose (m + 1 + m) (m + 1) := primorial_add_le m.le_succ
      _ = (m + 1)# * choose (2 * m + 1) m := by rw [choose_symm_add, two_mul, add_right_comm]
      _ < 4 ^ (m + 1) * 4 ^ m :=
        Nat.mul_lt_mul_of_lt_of_le (ihn _ (by lia) (by lia)) (choose_middle_le_pow _) (by simp)
      _ ≤ 4 ^ (m + m + 1) := by rw [← pow_add, add_right_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
n : ℕ
ihn : ∀ m < n + 1, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m
hn : n + 1 ≠ 0
ho : Odd n
⊢ (n + 1)# < HPow.hPow (α := ℕ) 4 (n + 1)
have h : ∀ (ihn : ∀ m < HAdd.hAdd (α := ℕ) 1 1, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m) (hn : HAdd.hAdd (α := ℕ) 1 1 ≠ 0)
  (ho : Odd (α := ℕ) 1), HAdd.hAdd (α := ℕ) 1 1# < HPow.hPow (α := ℕ) 4 (HAdd.hAdd (α := ℕ) 1 1)
Tactic: rcases Decidable.eq_or_ne n 1 with rfl | hn
Cleared hypotheses: n, ihn, hn, ho
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
n : ℕ
ihn : ∀ m < n + 1, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m
hn : n + 1 ≠ 0
ho : Odd n
h :
  ∀ (ihn : ∀ m < HAdd.hAdd (α := ℕ) 1 1, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m) (hn : HAdd.hAdd (α := ℕ) 1 1 ≠ 0)
    (ho : Odd (α := ℕ) 1), HAdd.hAdd (α := ℕ) 1 1# < HPow.hPow (α := ℕ) 4 (HAdd.hAdd (α := ℕ) 1 1)
⊢ (n + 1)# < HPow.hPow (α := ℕ) 4 (n + 1)
have h₁ : ∀ (hn : n ≠ 1), (n + 1)# < HPow.hPow (α := ℕ) 4 (n + 1)
Tactic: rcases Decidable.eq_or_ne n 1 with rfl | hn
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ n# < HPow.hPow (α := ℕ) 4 n
have h : ∀ (n : ℕ) (ihn : ∀ m < n, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m) (hn : n ≠ 0), n# < HPow.hPow (α := ℕ) 4 n
Tactic: induction n using Nat.strong_induction_on with | h n ihn =>
  rcases n with - | n; · grind
  rcases n.even_or_odd with ⟨m, rfl⟩ | ho
  · rcases m.eq_zero_or_pos with rfl | hm
    · decide
    calc
      (m + m + 1)# = (m + 1 + m)# := by rw [add_right_comm]
      _ ≤ (m + 1)# * choose (m + 1 + m) (m + 1) := primorial_add_le m.le_succ
      _ = (m + 1)# * choose (2 * m + 1) m := by rw [choose_symm_add, two_mul, add_right_comm]
      _ < 4 ^ (m + 1) * 4 ^ m :=
        Nat.mul_lt_mul_of_lt_of_le (ihn _ (by lia) (by lia)) (choose_middle_le_pow _) (by simp)
      _ ≤ 4 ^ (m + m + 1) := by rw [← pow_add, add_right_comm]
  · rcases Decidable.eq_or_ne n 1 with rfl | hn
    · decide
    · calc
        (n + 1)# = n# := primorial_succ hn ho
        _ < 4 ^ n := ihn n n.lt_succ_self (by grind)
        _ ≤ 4 ^ (n + 1) := Nat.pow_le_pow_right four_pos n.le_succ
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
n : ℕ
⊢ n# ≤ HPow.hPow (α := ℕ) 4 n
have inl : 0# ≤ HPow.hPow (α := ℕ) (β := ℕ) 4 0
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
n : ℕ
inl : 0# ≤ HPow.hPow (α := ℕ) (β := ℕ) 4 0
⊢ n# ≤ HPow.hPow (α := ℕ) 4 n
have inr : ∀ (hn : n ≠ 0), n# ≤ HPow.hPow (α := ℕ) 4 n
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
z : ZMod 4
⊢ z * z ≠ 2
have change : ∀ (z : Fin 4), z * z ≠ 2
Tactic: change Fin 4 at z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
z : Fin 4
⊢ z * z ≠ 2
have 0 : HMul.hMul (α := ZMod 4) ((fun (i : Fin 4) ↦ i) (⟨0, sorry⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨0, sorry⟩ : Fin 4)) ≠ 2
Tactic: fin_cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
z : Fin 4
0 : HMul.hMul (α := ZMod 4) ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4)) ≠ 2
⊢ z * z ≠ 2
have 1 : HMul.hMul (α := ZMod 4) ((fun (i : Fin 4) ↦ i) (⟨1, sorry⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨1, sorry⟩ : Fin 4)) ≠ 2
Tactic: fin_cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
z : Fin 4
0 : HMul.hMul (α := ZMod 4) ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4)) ≠ 2
1 : HMul.hMul (α := ZMod 4) ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4)) ≠ 2
⊢ z * z ≠ 2
have 2 : HMul.hMul (α := ZMod 4) ((fun (i : Fin 4) ↦ i) (⟨2, sorry⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨2, sorry⟩ : Fin 4)) ≠ 2
Tactic: fin_cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
z : Fin 4
0 : HMul.hMul (α := ZMod 4) ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4)) ≠ 2
1 : HMul.hMul (α := ZMod 4) ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4)) ≠ 2
2 : HMul.hMul (α := ZMod 4) ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4)) ≠ 2
⊢ z * z ≠ 2
have 3 : HMul.hMul (α := ZMod 4) ((fun (i : Fin 4) ↦ i) (⟨3, sorry⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨3, sorry⟩ : Fin 4)) ≠ 2
Tactic: fin_cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
z : ℤ
⊢ ¬z * z % (↑4 : ℤ) = HMod.hMod (α := ℤ) 2 (↑4 : ℤ)
have rw : ¬Eq (α := ZMod 4) (↑(z * z) : ZMod 4) (↑2 : ZMod 4)
Tactic: rw [← ZMod.intCast_eq_intCast_iff']
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
⊢ x * x + y * y = z * z ↔ y * y + x * x = z * z
have rw : y * y + x * x = z * z ↔ y * y + x * x = z * z
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
k : ℤ
⊢ HPow.hPow (β := ℕ) k 2 * (x * x + y * y) = HPow.hPow (β := ℕ) k 2 * (z * z)
have rw : HPow.hPow (β := ℕ) k 2 * (z * z) = HPow.hPow (β := ℕ) k 2 * (z * z)
Tactic: rw [h.eq]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z k : ℤ
hk : k ≠ 0
⊢ PythagoreanTriple (k * x) (k * y) (k * z) ↔ PythagoreanTriple x y z
have refine : PythagoreanTriple (k * x) (k * y) (k * z) → PythagoreanTriple x y z
Tactic: refine ⟨?_, fun h => h.mul k⟩
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z k : ℤ
hk : k ≠ 0
h : k * x * (k * x) + k * y * (k * y) = k * z * (k * z)
⊢ x * x + y * y = z * z
have rw : (x * x + y * y) * (k * k) = z * z * (k * k)
Tactic: rw [← mul_left_inj' (mul_ne_zero hk hk)]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z k : ℤ
hk : k ≠ 0
h : k * x * (k * x) + k * y * (k * y) = k * z * (k * z)
⊢ (x * x + y * y) * (k * k) = z * z * (k * k)
have h₁ : (x * x + y * y) * (k * k) = k * x * (k * x) + k * y * (k * y)
Tactic: convert! h using 1
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z k : ℤ
hk : k ≠ 0
h : k * x * (k * x) + k * y * (k * y) = k * z * (k * z)
h₁ : (x * x + y * y) * (k * k) = k * x * (k * x) + k * y * (k * y)
⊢ (x * x + y * y) * (k * k) = z * z * (k * k)
have h₂ : z * z * (k * k) = k * z * (k * z)
Tactic: convert! h using 1
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
k : ℤ
hc : h.IsClassified
⊢ ⋯.IsClassified
have inl : ∀ (l m n : ℤ) (co : m.gcd n = 1)
  (h : PythagoreanTriple (l * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) (l * (2 * m * n)) z), sorry.IsClassified
Tactic: obtain ⟨l, m, n, ⟨⟨rfl, rfl⟩ | ⟨rfl, rfl⟩, co⟩⟩ := hc
Cleared hypotheses: x, y, h, hc
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
k : ℤ
hc : h.IsClassified
inl :
  ∀ (l m n : ℤ) (co : m.gcd n = 1)
    (h : PythagoreanTriple (l * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) (l * (2 * m * n)) z), ⋯.IsClassified
⊢ ⋯.IsClassified
have inr : ∀ (l m n : ℤ) (co : m.gcd n = 1)
  (h : PythagoreanTriple (l * (2 * m * n)) (l * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) z), sorry.IsClassified
Tactic: obtain ⟨l, m, n, ⟨⟨rfl, rfl⟩ | ⟨rfl, rfl⟩, co⟩⟩ := hc
Cleared hypotheses: x, y, h, hc
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
z k l m n : ℤ
co : m.gcd n = 1
h : PythagoreanTriple (l * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) (l * (2 * m * n)) z
⊢ ⋯.IsClassified
have h₁ : (k * (l * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) =
        k * l * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
      k * (l * (2 * m * n)) = k * l * (2 * m * n) ∨
    k * (l * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) = k * l * (2 * m * n) ∧
      k * (l * (2 * m * n)) = k * l * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
  m.gcd n = 1
Tactic: use k * l, m, n
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
z k l m n : ℤ
co : m.gcd n = 1
h : PythagoreanTriple (l * (2 * m * n)) (l * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) z
⊢ ⋯.IsClassified
have h₁ : (k * (l * (2 * m * n)) = k * l * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
      k * (l * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) = k * l * (2 * m * n) ∨
    k * (l * (2 * m * n)) = k * l * (2 * m * n) ∧
      k * (l * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) =
        k * l * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
  m.gcd n = 1
Tactic: use k * l, m, n
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
have inl : ∀ (hx : x % 2 = 0), x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
Tactic: rcases Int.emod_two_eq_zero_or_one x with hx | hx
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
inl : ∀ (hx : x % 2 = 0), x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
have inr : ∀ (hx : x % 2 = 1), x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
Tactic: rcases Int.emod_two_eq_zero_or_one x with hx | hx
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
have inl : ∀ (hy : y % 2 = 0), x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
Tactic: rcases Int.emod_two_eq_zero_or_one y with hy | hy
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
inl : ∀ (hy : y % 2 = 0), x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
have inl₁ : ∀ (hy : y % 2 = 1), x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
Tactic: rcases Int.emod_two_eq_zero_or_one y with hy | hy
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
have inr : ∀ (hy : y % 2 = 0), x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
Tactic: rcases Int.emod_two_eq_zero_or_one y with hy | hy
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
inr : ∀ (hy : y % 2 = 0), x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
have inr₁ : ∀ (hy : y % 2 = 1), x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
Tactic: rcases Int.emod_two_eq_zero_or_one y with hy | hy
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
have inl : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ False
have apply : 2 ∣ x.natAbs
Tactic: apply Nat.not_coprime_of_dvd_of_dvd (by decide : 1 < 2) _ _ hc
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 0
apply : 2 ∣ x.natAbs
⊢ False
have apply₁ : 2 ∣ y.natAbs
Tactic: apply Nat.not_coprime_of_dvd_of_dvd (by decide : 1 < 2) _ _ hc
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ 2 ∣ x.natAbs
have apply : (↑2 : ℤ) ∣ x
Tactic: apply Int.natCast_dvd.1
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ 2 ∣ y.natAbs
have apply : (↑2 : ℤ) ∣ y
Tactic: apply Int.natCast_dvd.1
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 1
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
have inl : x % 2 = 0 ∧ y % 2 = 1
Tactic: left
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
hy : y % 2 = 0
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
have inr : x % 2 = 1 ∧ y % 2 = 0
Tactic: right
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
hy : y % 2 = 1
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
have inr : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
hy : y % 2 = 1
⊢ ∃ (x0 : ℤ) (y0 : ℤ), x = x0 * 2 + 1 ∧ y = y0 * 2 + 1
have obtain : ∀ (x0 : ℤ) (hx2 : x - 1 = x0 * 2), ∃ (x0 : ℤ) (y0 : ℤ), x = x0 * 2 + 1 ∧ y = y0 * 2 + 1
Tactic: obtain ⟨x0, hx2⟩ := exists_eq_mul_left_of_dvd (Int.dvd_self_sub_of_emod_eq hx)
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
hy : y % 2 = 1
x0 : ℤ
hx2 : x - 1 = x0 * 2
⊢ ∃ (x0 : ℤ) (y0 : ℤ), x = x0 * 2 + 1 ∧ y = y0 * 2 + 1
have obtain : ∀ (y0 : ℤ) (hy2 : y - 1 = y0 * 2), ∃ (x0 : ℤ) (y0 : ℤ), x = x0 * 2 + 1 ∧ y = y0 * 2 + 1
Tactic: obtain ⟨y0, hy2⟩ := exists_eq_mul_left_of_dvd (Int.dvd_self_sub_of_emod_eq hy)
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
hy : y % 2 = 1
x0 : ℤ
hx2 : x - 1 = x0 * 2
y0 : ℤ
hy2 : y - 1 = y0 * 2
⊢ ∃ (x0 : ℤ) (y0 : ℤ), x = x0 * 2 + 1 ∧ y = y0 * 2 + 1
have rw : ∀ (hx2 : x = x0 * 2 + 1) (y0 : ℤ) (hy2 : y = y0 * 2 + 1), ∃ (x0 : ℤ) (y0 : ℤ), x = x0 * 2 + 1 ∧ y = y0 * 2 + 1
Tactic: rw [sub_eq_iff_eq_add] at hx2 hy2
Cleared hypotheses: hx2, y0, hy2
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
hy : y % 2 = 1
⊢ False
have inr : ∀ (x0 y0 : ℤ) (hx : (x0 * 2 + 1) % 2 = 1) (hy : (y0 * 2 + 1) % 2 = 1)
  (h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z) (hc : (x0 * 2 + 1).gcd (y0 * 2 + 1) = 1), False
Tactic: obtain ⟨x0, y0, rfl, rfl⟩ : ∃ x0 y0, x = x0 * 2 + 1 ∧ y = y0 * 2 + 1 := by
      obtain ⟨x0, hx2⟩ := exists_eq_mul_left_of_dvd (Int.dvd_self_sub_of_emod_eq hx)
      obtain ⟨y0, hy2⟩ := exists_eq_mul_left_of_dvd (Int.dvd_self_sub_of_emod_eq hy)
      rw [sub_eq_iff_eq_add] at hx2 hy2
      exact ⟨x0, y0, hx2, hy2⟩
Cleared hypotheses: x, y, h, hc, hx, hy
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : (x0 * 2 + 1).gcd (y0 * 2 + 1) = 1
⊢ False
have inr : z * z % 4 = 2
Tactic: apply Int.sq_ne_two_mod_four z
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : (x0 * 2 + 1).gcd (y0 * 2 + 1) = 1
⊢ z * z = 4 * (x0 * x0 + x0 + y0 * y0 + y0) + 2
have rw : (x0 * 2 + 1) * (x0 * 2 + 1) + (y0 * 2 + 1) * (y0 * 2 + 1) = 4 * (x0 * x0 + x0 + y0 * y0 + y0) + 2
Tactic: rw [← h.eq]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : (x0 * 2 + 1).gcd (y0 * 2 + 1) = 1
⊢ z * z % 4 = 2
have inr : (4 * (x0 * x0 + x0 + y0 * y0 + y0) + 2) % 4 = 2
Tactic: rw [show z * z = 4 * (x0 * x0 + x0 + y0 * y0 + y0) + 2 by
        rw [← h.eq]
        ring]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : (x0 * 2 + 1).gcd (y0 * 2 + 1) = 1
⊢ (4 * (x0 * x0 + x0 + y0 * y0 + y0) + 2) % 4 = 2
have inr : HMod.hMod (α := ℤ) 2 4 % 4 = 2
Tactic: simp only [Int.add_emod, Int.mul_emod_right, zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
⊢ (↑(x.gcd y) : ℤ) ∣ z
have pos : ∀ (h0 : x.gcd y = 0), (↑(x.gcd y) : ℤ) ∣ z
Tactic: by_cases h0 : Int.gcd x y = 0
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
pos : ∀ (h0 : x.gcd y = 0), (↑(x.gcd y) : ℤ) ∣ z
⊢ (↑(x.gcd y) : ℤ) ∣ z
have neg : ∀ (h0 : ¬x.gcd y = 0), (↑(x.gcd y) : ℤ) ∣ z
Tactic: by_cases h0 : Int.gcd x y = 0
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
⊢ (↑(x.gcd y) : ℤ) ∣ z
have hx : x = 0
Tactic: obtain ⟨hx, hy⟩ := Int.gcd_eq_zero_iff.mp h0
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
⊢ (↑(x.gcd y) : ℤ) ∣ z
have hy : y = 0
Tactic: obtain ⟨hx, hy⟩ := Int.gcd_eq_zero_iff.mp h0
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (hypothesis)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
⊢ (↑(x.gcd y) : ℤ) ∣ z
have hz : z = 0
Tactic: have hz : z = 0 := by
      simpa only [PythagoreanTriple, hx, hy, add_zero, zero_eq_mul, mul_zero,
        or_self_iff] using h
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
⊢ (↑(x.gcd y) : ℤ) ∣ z
have neg : ∀ (k : ℕ) (x0 y0 : ℤ),
  0 < k →
    ∀ (h2 : x0.gcd y0 = 1) (h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) z)
      (h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0), (↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ) ∣ z
Tactic: obtain ⟨k, x0, y0, _, h2, rfl, rfl⟩ :
    ∃ (k : ℕ) (x0 y0 : _), 0 < k ∧ Int.gcd x0 y0 = 1 ∧ x = x0 * k ∧ y = y0 * k :=
    Int.exists_gcd_one' (Nat.pos_of_ne_zero h0)
Cleared hypotheses: x, y, h, h0
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
z : ℤ
k : ℕ
x0 y0 : ℤ
left : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) z
h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0
⊢ (↑((x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ))) : ℤ) ∣ z
have neg : (↑k : ℤ) ∣ z
Tactic: rw [Int.gcd_mul_right, h2, Int.natAbs_natCast, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.PythagoreanTriples (goal)
Goal:
z : ℤ
k : ℕ
x0 y0 : ℤ
left : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * (↑k : ℤ)) (y0 * (↑k : ℤ)) z
h0 : ¬(x0 * (↑k : ℤ)).gcd (y0 * (↑k : ℤ)) = 0
⊢ (↑k : ℤ) ∣ z
have neg : HPow.hPow (α := ℤ) (β := ℕ) (↑k : ℤ) 2 ∣ x0 * (↑k : ℤ) * (x0 * (↑k : ℤ)) + y0 * (↑k : ℤ) * (y0 * (↑k : ℤ))
Tactic: rw [← Int.pow_dvd_pow_iff two_ne_zero, sq z, ← h.eq]