awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
hn : 2 < n
⊢ n ≤ n#

Tactic:
(lt_primorial_self hn).le

Premises used: lt_primorial_self, LT.lt.le
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
hn : 2 < n
⊢ n ≤ n#

Tactic:
exact (lt_primorial_self hn).le

Premises used: lt_primorial_self, LT.lt.le
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
ihn : ∀ m < n, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m
hn : n ≠ 0
h :
  ∀ (ihn : ∀ m < 0, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m) (hn : Ne (α := ℕ) 0 0),
    0# < HPow.hPow (α := ℕ) (β := ℕ) 4 0
h₁ :
  ∀ (n : ℕ) (ihn : ∀ m < n + 1, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m) (hn : n + 1 ≠ 0),
    (n + 1)# < HPow.hPow (α := ℕ) 4 (n + 1)
⊢ n# < HPow.hPow (α := ℕ) 4 n

Tactic:
rcases n with - | n
-- Module: Mathlib.NumberTheory.Primorial
Goal:
ihn : ∀ m < 0, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m
hn : Ne (α := ℕ) 0 0
⊢ 0# < HPow.hPow (α := ℕ) (β := ℕ) 4 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
ihn : ∀ m < n + 1, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m
hn : n + 1 ≠ 0
h :
  ∀ (m : ℕ) (ihn : ∀ m_1 < m + m + 1, ∀ (hn : m_1 ≠ 0), m_1# < HPow.hPow (α := ℕ) 4 m_1) (hn : m + m + 1 ≠ 0),
    (m + m + 1)# < HPow.hPow (α := ℕ) 4 (m + m + 1)
h₁ : ∀ (ho : Odd n), (n + 1)# < HPow.hPow (α := ℕ) 4 (n + 1)
⊢ (n + 1)# < HPow.hPow (α := ℕ) 4 (n + 1)

Tactic:
rcases n.even_or_odd with ⟨m, rfl⟩ | ho

Premises used: Nat.even_or_odd, rfl
-- Module: Mathlib.NumberTheory.Primorial
Goal:
m : ℕ
ihn : ∀ m_1 < m + m + 1, ∀ (hn : m_1 ≠ 0), m_1# < HPow.hPow (α := ℕ) 4 m_1
hn : m + m + 1 ≠ 0
h :
  ∀ (ihn : ∀ m < HAdd.hAdd (α := ℕ) 0 0 + 1, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m)
    (hn : HAdd.hAdd (α := ℕ) 0 0 + 1 ≠ 0),
    (HAdd.hAdd (α := ℕ) 0 0 + 1)# < HPow.hPow (α := ℕ) 4 (HAdd.hAdd (α := ℕ) 0 0 + 1)
h₁ : ∀ (hm : m > 0), (m + m + 1)# < HPow.hPow (α := ℕ) 4 (m + m + 1)
⊢ (m + m + 1)# < HPow.hPow (α := ℕ) 4 (m + m + 1)

Tactic:
rcases m.eq_zero_or_pos with rfl | hm

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.NumberTheory.Primorial
Goal:
ihn : ∀ m < HAdd.hAdd (α := ℕ) 0 0 + 1, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m
hn : HAdd.hAdd (α := ℕ) 0 0 + 1 ≠ 0
⊢ (HAdd.hAdd (α := ℕ) 0 0 + 1)# < HPow.hPow (α := ℕ) 4 (HAdd.hAdd (α := ℕ) 0 0 + 1)

Tactic:
decide
-- Module: Mathlib.NumberTheory.Primorial
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 rw₁ : (m + 1 + m)# = (m + 1 + m)#
⊢ (m + m + 1)# = (m + 1 + m)#

Tactic:
rw [add_right_comm]

Premises used: add_right_comm
-- Module: Mathlib.NumberTheory.Primorial
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)# ≤ (m + 1)# * (m + 1 + m).choose (m + 1)

Tactic:
primorial_add_le m.le_succ

Premises used: Nat.le_succ, primorial_add_le
-- Module: Mathlib.NumberTheory.Primorial
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
rw₂ rw₃ : (m + 1)# * (m + m + 1).choose m = (m + 1)# * (m + m + 1).choose m
⊢ (m + 1)# * (m + 1 + m).choose (m + 1) = (m + 1)# * (2 * m + 1).choose m

Tactic:
rw [choose_symm_add, two_mul, add_right_comm]

Premises used: two_mul, add_right_comm, Nat.choose_symm_add
-- Module: Mathlib.NumberTheory.Primorial
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 + m + 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.Primorial
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 ≠ 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.Primorial
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
⊢ 0 < HPow.hPow (α := ℕ) 4 m

Tactic:
simp
-- Module: Mathlib.NumberTheory.Primorial
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)
rw₁ rw₂ : HPow.hPow (α := ℕ) 4 (m + m + 1) ≤ HPow.hPow (α := ℕ) 4 (m + m + 1)
⊢ HPow.hPow (α := ℕ) 4 (m + 1) * HPow.hPow (α := ℕ) 4 m ≤ HPow.hPow (α := ℕ) 4 (m + m + 1)

Tactic:
rw [← pow_add, add_right_comm]

Premises used: pow_add, add_right_comm
-- Module: Mathlib.NumberTheory.Primorial
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₃ : HPow.hPow (α := ℕ) 4 (m + 1) * HPow.hPow (α := ℕ) 4 m ≤ HPow.hPow (α := ℕ) 4 (m + m + 1)
⊢ (m + m + 1)# < 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]

Premises used: Nat.choose, HMul.hMul, Nat.mul_lt_mul_of_lt_of_le, Nat.choose_middle_le_pow, Nat.le_succ, HAdd.hAdd, primorial_add_le, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Primorial
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)
h₁ : ∀ (hn : n ≠ 1), (n + 1)# < HPow.hPow (α := ℕ) 4 (n + 1)
⊢ (n + 1)# < HPow.hPow (α := ℕ) 4 (n + 1)

Tactic:
rcases Decidable.eq_or_ne n 1 with rfl | hn

Premises used: Decidable.eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Primorial
Goal:
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:
decide
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
ihn : ∀ m < n + 1, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m
hn_1 : n + 1 ≠ 0
ho : Odd n
hn : n ≠ 1
⊢ (n + 1)# = n#

Tactic:
primorial_succ hn ho

Premises used: primorial_succ
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
ihn : ∀ m < n + 1, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m
hn_1 : n + 1 ≠ 0
ho : Odd n
hn : n ≠ 1
⊢ n ≠ 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
ihn : ∀ m < n + 1, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m
hn_1 : n + 1 ≠ 0
ho : Odd n
hn : n ≠ 1
⊢ HPow.hPow (α := ℕ) 4 n ≤ HPow.hPow (α := ℕ) 4 (n + 1)

Tactic:
Nat.pow_le_pow_right four_pos n.le_succ

Premises used: four_pos, Nat.le_succ, Nat.pow_le_pow_right
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
ihn : ∀ m < n + 1, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m
hn_1 : n + 1 ≠ 0
ho : Odd n
hn : n ≠ 1
⊢ (n + 1)# < HPow.hPow (α := ℕ) 4 (n + 1)

Tactic:
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

Premises used: four_pos, primorial_succ, Nat.lt_succ_self, Nat.le_succ, Nat.pow_le_pow_right, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
hn : n ≠ 0
h : ∀ (n : ℕ) (ihn : ∀ m < n, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m) (hn : n ≠ 0), n# < HPow.hPow (α := ℕ) 4 n
⊢ 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

Premises used: four_pos, Decidable.eq_or_ne, Nat.le_succ, Nat.pow_le_pow_right, HAdd.hAdd, OfNat.ofNat, Nat.even_or_odd, rfl
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
inl : 0# ≤ HPow.hPow (α := ℕ) (β := ℕ) 4 0
inr : ∀ (hn : n ≠ 0), n# ≤ HPow.hPow (α := ℕ) 4 n
⊢ n# ≤ HPow.hPow (α := ℕ) 4 n

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Primorial
Goal:
⊢ 0# ≤ HPow.hPow (α := ℕ) (β := ℕ) 4 0

Tactic:
decide
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
hn : n ≠ 0
⊢ n# ≤ HPow.hPow (α := ℕ) 4 n

Tactic:
(primorial_lt_four_pow n hn).le

Premises used: primorial_lt_four_pow, LT.lt.le
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
hn : n ≠ 0
⊢ n# ≤ HPow.hPow (α := ℕ) 4 n

Tactic:
exact (primorial_lt_four_pow n hn).le

Premises used: primorial_lt_four_pow, LT.lt.le
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z : ZMod 4
change : ∀ (z : Fin 4), z * z ≠ 2
⊢ z * z ≠ 2

Tactic:
change Fin 4 at z

Premises used: OfNat.ofNat, Fin
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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
3 : HMul.hMul (α := ZMod 4) ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4)) ≠ 2
⊢ z * z ≠ 2

Tactic:
fin_cases z
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
⊢ HMul.hMul (α := ZMod 4) ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4)) ≠ 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
⊢ HMul.hMul (α := ZMod 4) ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4)) ≠ 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
⊢ HMul.hMul (α := ZMod 4) ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4)) ≠ 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
⊢ HMul.hMul (α := ZMod 4) ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4)) ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4)) ≠ 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z : ℤ
this : ¬z * z % (↑4 : ℤ) = HMod.hMod (α := ℤ) 2 (↑4 : ℤ)
⊢ z * z % 4 ≠ 2

Tactic:
this

Premises used: Int.emod
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z : ℤ
this : ¬z * z % (↑4 : ℤ) = HMod.hMod (α := ℤ) 2 (↑4 : ℤ)
⊢ z * z % 4 ≠ 2

Tactic:
exact this
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z : ℤ
rw : ¬Eq (α := ZMod 4) (↑(z * z) : ZMod 4) (↑2 : ZMod 4)
⊢ ¬z * z % (↑4 : ℤ) = HMod.hMod (α := ℤ) 2 (↑4 : ℤ)

Tactic:
rw [← ZMod.intCast_eq_intCast_iff']

Premises used: ZMod.intCast_eq_intCast_iff'
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z : ℤ
⊢ ¬Eq (α := ZMod 4) (↑(z * z) : ZMod 4) (↑2 : ZMod 4)

Tactic:
simpa using sq_ne_two_fin_zmod_four _

Premises used: sq_ne_two_fin_zmod_four
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
rw rw₁ : y * y + x * x = z * z ↔ y * y + x * x = z * z
⊢ x * x + y * y = z * z ↔ y * y + x * x = z * z

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
⊢ PythagoreanTriple 0 0 0

Tactic:
simp only [PythagoreanTriple, zero_mul, zero_add]

Premises used: MulZeroClass.zero_mul, zero_add, PythagoreanTriple
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
⊢ x * x + y * y = z * z

Tactic:
h

Premises used: PythagoreanTriple
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h rwa rwa₁ rwa₂ rwa₃ : PythagoreanTriple x y z
⊢ PythagoreanTriple y x z

Tactic:
rwa [pythagoreanTriple_comm]

Premises used: pythagoreanTriple_comm
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
k : ℤ
⊢ k * x * (k * x) + k * y * (k * y) = HPow.hPow (β := ℕ) k 2 * (x * x + y * y)

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
k : ℤ
rw rw₁ : HPow.hPow (β := ℕ) k 2 * (z * z) = HPow.hPow (β := ℕ) k 2 * (z * z)
⊢ HPow.hPow (β := ℕ) k 2 * (x * x + y * y) = HPow.hPow (β := ℕ) k 2 * (z * z)

Tactic:
rw [h.eq]

Premises used: PythagoreanTriple.eq
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
k : ℤ
⊢ HPow.hPow (β := ℕ) k 2 * (z * z) = k * z * (k * z)

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z k : ℤ
hk : k ≠ 0
⊢ PythagoreanTriple (k * x) (k * y) (k * z) ↔ PythagoreanTriple x y z

Tactic:
⟨?_, fun h => h.mul k⟩

Premises used: PythagoreanTriple.mul, Iff.intro
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z k : ℤ
hk : k ≠ 0
refine : PythagoreanTriple (k * x) (k * y) (k * z) → PythagoreanTriple x y z
⊢ PythagoreanTriple (k * x) (k * y) (k * z) ↔ PythagoreanTriple x y z

Tactic:
refine ⟨?_, fun h => h.mul k⟩
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z k : ℤ
hk : k ≠ 0
h : k * x * (k * x) + k * y * (k * y) = k * z * (k * z)
rw : (x * x + y * y) * (k * k) = z * z * (k * k)
⊢ x * x + y * y = z * z

Tactic:
rw [← mul_left_inj' (mul_ne_zero hk hk)]

Premises used: mul_ne_zero, mul_left_inj'
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z k : ℤ
hk : k ≠ 0
h : k * x * (k * x) + k * y * (k * y) = k * z * (k * z)
⊢ k * x * (k * x) + k * y * (k * y) = k * z * (k * z)

Tactic:
h
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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)
h₂ : z * z * (k * k) = k * z * (k * z)
⊢ (x * x + y * y) * (k * k) = z * z * (k * k)

Tactic:
convert! h using 1
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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) = k * x * (k * x) + k * y * (k * y)

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z k : ℤ
hk : k ≠ 0
h : k * x * (k * x) + k * y * (k * y) = k * z * (k * z)
⊢ z * z * (k * k) = k * z * (k * z)

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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
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), ⋯.IsClassified
⊢ ⋯.IsClassified

Tactic:
obtain ⟨l, m, n, ⟨⟨rfl, rfl⟩ | ⟨rfl, rfl⟩, co⟩⟩ := hc

Premises used: rfl
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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
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
⊢ ⋯.IsClassified

Tactic:
use k * l, m, n
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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
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
⊢ ⋯.IsClassified

Tactic:
use k * l, m, n
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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
⊢ (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:
grind
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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
⊢ (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:
grind
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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
inr : ∀ (hx : x % 2 = 1), x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 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

Premises used: Int.emod_two_eq_zero_or_one
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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
inl₁ : ∀ (hy : y % 2 = 1), x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ 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

Premises used: Int.emod_two_eq_zero_or_one
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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
inr₁ : ∀ (hy : y % 2 = 1), x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ 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

Premises used: Int.emod_two_eq_zero_or_one
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 0
inl : False
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0

Tactic:
exfalso
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ LT.lt (α := ℕ) 1 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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
apply₁ : 2 ∣ y.natAbs
⊢ False

Tactic:
apply Nat.not_coprime_of_dvd_of_dvd (by decide : 1 < 2) _ _ hc

Premises used: Nat.not_coprime_of_dvd_of_dvd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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
⊢ 2 ∣ x.natAbs

Tactic:
apply Int.natCast_dvd.1

Premises used: Iff.mp, Int.natCast_dvd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ (↑2 : ℤ) ∣ x

Tactic:
apply Int.dvd_of_emod_eq_zero hx

Premises used: Int.dvd_of_emod_eq_zero
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 0
apply : (↑2 : ℤ) ∣ y
⊢ 2 ∣ y.natAbs

Tactic:
apply Int.natCast_dvd.1

Premises used: Iff.mp, Int.natCast_dvd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ (↑2 : ℤ) ∣ y

Tactic:
apply Int.dvd_of_emod_eq_zero hy

Premises used: Int.dvd_of_emod_eq_zero
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 1
inl : x % 2 = 0 ∧ y % 2 = 1
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0

Tactic:
left
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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

Tactic:
⟨hx, hy⟩

Premises used: And.intro
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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

Tactic:
exact ⟨hx, hy⟩
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
hy : y % 2 = 0
inr : x % 2 = 1 ∧ y % 2 = 0
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0

Tactic:
right
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
hy : y % 2 = 0
⊢ x % 2 = 1 ∧ y % 2 = 0

Tactic:
⟨hx, hy⟩

Premises used: And.intro
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
hy : y % 2 = 0
⊢ x % 2 = 1 ∧ y % 2 = 0

Tactic:
exact ⟨hx, hy⟩
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
hy : y % 2 = 1
inr : False
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0

Tactic:
exfalso
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
hy : y % 2 = 1
obtain : ∀ (x0 : ℤ) (hx2 : x - 1 = x0 * 2), ∃ (x0 : ℤ) (y0 : ℤ), x = x0 * 2 + 1 ∧ y = y0 * 2 + 1
⊢ ∃ (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)

Premises used: Int.dvd_self_sub_of_emod_eq, exists_eq_mul_left_of_dvd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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
obtain : ∀ (y0 : ℤ) (hy2 : y - 1 = y0 * 2), ∃ (x0 : ℤ) (y0 : ℤ), x = x0 * 2 + 1 ∧ y = y0 * 2 + 1
⊢ ∃ (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)

Premises used: Int.dvd_self_sub_of_emod_eq, exists_eq_mul_left_of_dvd
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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
rw : ∀ (hx2 : x = x0 * 2 + 1) (y0 : ℤ) (hy2 : y = y0 * 2 + 1), ∃ (x0 : ℤ) (y0 : ℤ), x = x0 * 2 + 1 ∧ y = y0 * 2 + 1
⊢ ∃ (x0 : ℤ) (y0 : ℤ), x = x0 * 2 + 1 ∧ y = y0 * 2 + 1

Tactic:
rw [sub_eq_iff_eq_add] at hx2 hy2

Premises used: sub_eq_iff_eq_add
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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 = x0 * 2 + 1
y0 : ℤ
hy2 : y = y0 * 2 + 1
⊢ ∃ (x0 : ℤ) (y0 : ℤ), x = x0 * 2 + 1 ∧ y = y0 * 2 + 1

Tactic:
⟨x0, y0, hx2, hy2⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.PythagoreanTriples
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 = x0 * 2 + 1
y0 : ℤ
hy2 : y = y0 * 2 + 1
⊢ ∃ (x0 : ℤ) (y0 : ℤ), x = x0 * 2 + 1 ∧ y = y0 * 2 + 1

Tactic:
exact ⟨x0, y0, hx2, hy2⟩