awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
N k m : ℕ
tauto tauto₁ : ∀ (P Q : Prop), P ∧ (P → Q) ↔ P ∧ Q
mp : ∀ (P Q : Prop), P ∧ (P → Q) → P ∧ Q
mpr : ∀ (P Q : Prop), P ∧ Q → P ∧ (P → Q)
mp₁ mp₂ : ∀ (P Q : Prop), P → (P → Q) → P ∧ Q
mp₃ : ∀ (P Q : Prop), P → (P → Q) → P
mp₄ : ∀ (P Q : Prop), P → (P → Q) → Q
mpr₁ mpr₂ : ∀ (P Q : Prop), P → Q → P ∧ (P → Q)
mpr₃ : ∀ (P Q : Prop), P → Q → P
⊢ ∀ (P Q : Prop), P ∧ (P → Q) ↔ P ∧ Q
have mpr₄ : ∀ (P Q : Prop), P → Q → P → Q
Tactic: tauto
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
N k m : ℕ
tauto tauto₁ : ∀ (P Q : Prop), P ∧ (P → Q) ↔ P ∧ Q
mp : ∀ (P Q : Prop), P ∧ (P → Q) → P ∧ Q
mpr : ∀ (P Q : Prop), P ∧ Q → P ∧ (P → Q)
mp₁ mp₂ : ∀ (P Q : Prop), P → (P → Q) → P ∧ Q
mp₃ : ∀ (P Q : Prop), P → (P → Q) → P
mp₄ : ∀ (P Q : Prop), P → (P → Q) → Q
mpr₁ mpr₂ : ∀ (P Q : Prop), P → Q → P ∧ (P → Q)
mpr₃ : ∀ (P Q : Prop), P → Q → P
mpr₄ : ∀ (P Q : Prop), P → Q → P → Q
⊢ ∀ (P Q : Prop), P ∧ (P → Q) ↔ P ∧ Q
have mp₅ : ∀ (P Q : Prop), P → ¬P → Q
Tactic: tauto
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
N k m : ℕ
tauto tauto₁ : ∀ (P Q : Prop), P ∧ (P → Q) ↔ P ∧ Q
mp : ∀ (P Q : Prop), P ∧ (P → Q) → P ∧ Q
mpr : ∀ (P Q : Prop), P ∧ Q → P ∧ (P → Q)
mp₁ mp₂ : ∀ (P Q : Prop), P → (P → Q) → P ∧ Q
mp₃ : ∀ (P Q : Prop), P → (P → Q) → P
mp₄ : ∀ (P Q : Prop), P → (P → Q) → Q
mpr₁ mpr₂ : ∀ (P Q : Prop), P → Q → P ∧ (P → Q)
mpr₃ : ∀ (P Q : Prop), P → Q → P
mpr₄ : ∀ (P Q : Prop), P → Q → P → Q
mp₅ : ∀ (P Q : Prop), P → ¬P → Q
⊢ ∀ (P Q : Prop), P ∧ (P → Q) ↔ P ∧ Q
have mp₆ : ∀ (P Q : Prop), P → Q → Q
Tactic: tauto
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
N k m : ℕ
⊢ m ∈ N.roughNumbersUpTo k ↔
    Membership.mem (γ := Finset ℕ)
      (((N + 1).primesBelow \ k.primesBelow).biUnion fun (p : ℕ) ↦ {m ∈ Finset.range (N + 1) | m ≠ 0 ∧ p ∣ m}) m
have h : (m < N + 1 ∧ m ≠ 0 ∧ ∃ x ≤ m, Prime x ∧ x ∣ m ∧ k ≤ x) ↔
  ∃ (a : ℕ), ((a < N + 1 ∧ Prime a) ∧ (a < k → ¬Prime a)) ∧ m < N + 1 ∧ m ≠ 0 ∧ a ∣ m
Tactic: simp only [roughNumbersUpTo, mem_smoothNumbers_iff_forall_le, not_and, not_forall,
    not_lt, exists_prop, Finset.mem_range, Finset.mem_filter,
    Finset.mem_biUnion, Finset.mem_sdiff, mem_primesBelow,
    show ∀ P Q : Prop, P ∧ (P → Q) ↔ P ∧ Q by tauto]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
N k m : ℕ
⊢ (m < N + 1 ∧ m ≠ 0 ∧ ∃ x ≤ m, Prime x ∧ x ∣ m ∧ k ≤ x) ↔
    ∃ (a : ℕ), ((a < N + 1 ∧ Prime a) ∧ (a < k → ¬Prime a)) ∧ m < N + 1 ∧ m ≠ 0 ∧ a ∣ m
have h : (∃ (x : ℕ), m < N + 1 ∧ m ≠ 0 ∧ ¬m < x ∧ Prime x ∧ x ∣ m ∧ ¬x < k) ↔
  ∃ (a : ℕ), ((a < N + 1 ∧ Prime a) ∧ (a < k → ¬Prime a)) ∧ m < N + 1 ∧ m ≠ 0 ∧ a ∣ m
Tactic: simp_rw [← exists_and_left, ← not_lt]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
N k m : ℕ
⊢ (∃ (x : ℕ), m < N + 1 ∧ m ≠ 0 ∧ ¬m < x ∧ Prime x ∧ x ∣ m ∧ ¬x < k) ↔
    ∃ (a : ℕ), ((a < N + 1 ∧ Prime a) ∧ (a < k → ¬Prime a)) ∧ m < N + 1 ∧ m ≠ 0 ∧ a ∣ m
have h : ∀ (p : ℕ),
  m < N + 1 ∧ m ≠ 0 ∧ ¬m < p ∧ Prime p ∧ p ∣ m ∧ ¬p < k ↔
    ((p < N + 1 ∧ Prime p) ∧ (p < k → ¬Prime p)) ∧ m < N + 1 ∧ m ≠ 0 ∧ p ∣ m
Tactic: refine exists_congr fun p ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
N k m p : ℕ
⊢ m < N + 1 ∧ m ≠ 0 ∧ ¬m < p ∧ Prime p ∧ p ∣ m ∧ ¬p < k ↔
    ((p < N + 1 ∧ Prime p) ∧ (p < k → ¬Prime p)) ∧ m < N + 1 ∧ m ≠ 0 ∧ p ∣ m
have H : m ≠ 0 → p ∣ m → ¬m < p
Tactic: have H : m ≠ 0 → p ∣ m → ¬ m < p :=
    fun h₁ h₂ ↦ not_lt.mpr <| le_of_dvd (Nat.pos_of_ne_zero h₁) h₂
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
N k : ℕ
⊢ #(N.roughNumbersUpTo k) ≤ ∑ p ∈ (N + 1).primesBelow \ k.primesBelow, N / p
have rw : Finset.card (α := ℕ)
    (((N + 1).primesBelow \ k.primesBelow).biUnion fun (p : ℕ) ↦ {m ∈ Finset.range (N + 1) | m ≠ 0 ∧ p ∣ m}) ≤
  ∑ p ∈ (N + 1).primesBelow \ k.primesBelow, N / p
Tactic: rw [roughNumbersUpTo_eq_biUnion]
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
a b c d x y z w : ℕ
⊢ HPow.hPow (β := ℕ)
            (HMul.hMul (α := ℤ) (↑a : ℤ) (↑x : ℤ) - HMul.hMul (α := ℤ) (↑b : ℤ) (↑y : ℤ) -
                  HMul.hMul (α := ℤ) (↑c : ℤ) (↑z : ℤ) -
                HMul.hMul (α := ℤ) (↑d : ℤ) (↑w : ℤ)).natAbs
            2 +
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := ℤ) (↑a : ℤ) (↑y : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑x : ℤ) +
                  HMul.hMul (α := ℤ) (↑c : ℤ) (↑w : ℤ) -
                HMul.hMul (α := ℤ) (↑d : ℤ) (↑z : ℤ)).natAbs
            2 +
        HPow.hPow (β := ℕ)
          (HMul.hMul (α := ℤ) (↑a : ℤ) (↑z : ℤ) - HMul.hMul (α := ℤ) (↑b : ℤ) (↑w : ℤ) +
                HMul.hMul (α := ℤ) (↑c : ℤ) (↑x : ℤ) +
              HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ)).natAbs
          2 +
      HPow.hPow (β := ℕ)
        (HMul.hMul (α := ℤ) (↑a : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑z : ℤ) -
              HMul.hMul (α := ℤ) (↑c : ℤ) (↑y : ℤ) +
            HMul.hMul (α := ℤ) (↑d : ℤ) (↑x : ℤ)).natAbs
        2 =
    (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2) *
      (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 + HPow.hPow (β := ℕ) w 2)
have rw : Eq (α := ℤ)
  (↑(HPow.hPow (β := ℕ)
              (HMul.hMul (α := ℤ) (↑a : ℤ) (↑x : ℤ) - HMul.hMul (α := ℤ) (↑b : ℤ) (↑y : ℤ) -
                    HMul.hMul (α := ℤ) (↑c : ℤ) (↑z : ℤ) -
                  HMul.hMul (α := ℤ) (↑d : ℤ) (↑w : ℤ)).natAbs
              2 +
            HPow.hPow (β := ℕ)
              (HMul.hMul (α := ℤ) (↑a : ℤ) (↑y : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑x : ℤ) +
                    HMul.hMul (α := ℤ) (↑c : ℤ) (↑w : ℤ) -
                  HMul.hMul (α := ℤ) (↑d : ℤ) (↑z : ℤ)).natAbs
              2 +
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := ℤ) (↑a : ℤ) (↑z : ℤ) - HMul.hMul (α := ℤ) (↑b : ℤ) (↑w : ℤ) +
                  HMul.hMul (α := ℤ) (↑c : ℤ) (↑x : ℤ) +
                HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ)).natAbs
            2 +
        HPow.hPow (β := ℕ)
          (HMul.hMul (α := ℤ) (↑a : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑z : ℤ) -
                HMul.hMul (α := ℤ) (↑c : ℤ) (↑y : ℤ) +
              HMul.hMul (α := ℤ) (↑d : ℤ) (↑x : ℤ)).natAbs
          2) :
    ℤ)
  (↑((HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2) *
        (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 + HPow.hPow (β := ℕ) w 2)) :
    ℤ)
Tactic: rw [← Int.natCast_inj]
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
a b c d x y z w : ℕ
⊢ Eq (α := ℤ)
    (↑(HPow.hPow (β := ℕ)
                (HMul.hMul (α := ℤ) (↑a : ℤ) (↑x : ℤ) - HMul.hMul (α := ℤ) (↑b : ℤ) (↑y : ℤ) -
                      HMul.hMul (α := ℤ) (↑c : ℤ) (↑z : ℤ) -
                    HMul.hMul (α := ℤ) (↑d : ℤ) (↑w : ℤ)).natAbs
                2 +
              HPow.hPow (β := ℕ)
                (HMul.hMul (α := ℤ) (↑a : ℤ) (↑y : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑x : ℤ) +
                      HMul.hMul (α := ℤ) (↑c : ℤ) (↑w : ℤ) -
                    HMul.hMul (α := ℤ) (↑d : ℤ) (↑z : ℤ)).natAbs
                2 +
            HPow.hPow (β := ℕ)
              (HMul.hMul (α := ℤ) (↑a : ℤ) (↑z : ℤ) - HMul.hMul (α := ℤ) (↑b : ℤ) (↑w : ℤ) +
                    HMul.hMul (α := ℤ) (↑c : ℤ) (↑x : ℤ) +
                  HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ)).natAbs
              2 +
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := ℤ) (↑a : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑z : ℤ) -
                  HMul.hMul (α := ℤ) (↑c : ℤ) (↑y : ℤ) +
                HMul.hMul (α := ℤ) (↑d : ℤ) (↑x : ℤ)).natAbs
            2) :
      ℤ)
    (↑((HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2) *
          (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 + HPow.hPow (β := ℕ) w 2)) :
      ℤ)
have push_cast : HPow.hPow (β := ℕ)
          |HMul.hMul (α := ℤ) (↑a : ℤ) (↑x : ℤ) - HMul.hMul (α := ℤ) (↑b : ℤ) (↑y : ℤ) -
                HMul.hMul (α := ℤ) (↑c : ℤ) (↑z : ℤ) -
              HMul.hMul (α := ℤ) (↑d : ℤ) (↑w : ℤ)|
          2 +
        HPow.hPow (β := ℕ)
          |HMul.hMul (α := ℤ) (↑a : ℤ) (↑y : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑x : ℤ) +
                HMul.hMul (α := ℤ) (↑c : ℤ) (↑w : ℤ) -
              HMul.hMul (α := ℤ) (↑d : ℤ) (↑z : ℤ)|
          2 +
      HPow.hPow (β := ℕ)
        |HMul.hMul (α := ℤ) (↑a : ℤ) (↑z : ℤ) - HMul.hMul (α := ℤ) (↑b : ℤ) (↑w : ℤ) +
              HMul.hMul (α := ℤ) (↑c : ℤ) (↑x : ℤ) +
            HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ)|
        2 +
    HPow.hPow (β := ℕ)
      |HMul.hMul (α := ℤ) (↑a : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑z : ℤ) -
            HMul.hMul (α := ℤ) (↑c : ℤ) (↑y : ℤ) +
          HMul.hMul (α := ℤ) (↑d : ℤ) (↑x : ℤ)|
      2 =
  (HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 +
        HPow.hPow (α := ℤ) (β := ℕ) (↑c : ℤ) 2 +
      HPow.hPow (α := ℤ) (β := ℕ) (↑d : ℤ) 2) *
    (HPow.hPow (α := ℤ) (β := ℕ) (↑x : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑y : ℤ) 2 +
        HPow.hPow (α := ℤ) (β := ℕ) (↑z : ℤ) 2 +
      HPow.hPow (α := ℤ) (β := ℕ) (↑w : ℤ) 2)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
m x y : ℤ
h : 2 * m = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
this : Even (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2)
⊢ HMul.hMul (α := ℤ) 2 2 * m = HPow.hPow (β := ℕ) (x - y) 2 + HPow.hPow (β := ℕ) (x + y) 2
have rw : 2 * (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) = HPow.hPow (β := ℕ) (x - y) 2 + HPow.hPow (β := ℕ) (x + y) 2
Tactic: rw [mul_assoc, h]
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
m x y : ℤ
h : 2 * m = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
this : Even (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2)
⊢ HPow.hPow (β := ℕ) (x - y) 2 + HPow.hPow (β := ℕ) (x + y) 2 =
    HPow.hPow (β := ℕ) (2 * ((x - y) / 2)) 2 + HPow.hPow (β := ℕ) (2 * ((x + y) / 2)) 2
have rw : 2 ∣ x + y
Tactic: rw [Int.mul_ediv_cancel' _, Int.mul_ediv_cancel' _]
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
m x y : ℤ
h : 2 * m = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
this : Even (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2)
rw : 2 ∣ x + y
⊢ HPow.hPow (β := ℕ) (x - y) 2 + HPow.hPow (β := ℕ) (x + y) 2 =
    HPow.hPow (β := ℕ) (2 * ((x - y) / 2)) 2 + HPow.hPow (β := ℕ) (2 * ((x + y) / 2)) 2
have rw₁ : 2 ∣ x - y
Tactic: rw [Int.mul_ediv_cancel' _, Int.mul_ediv_cancel' _]
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
m x y : ℤ
h : 2 * m = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
this : Even (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2)
⊢ HPow.hPow (β := ℕ) (2 * ((x - y) / 2)) 2 + HPow.hPow (β := ℕ) (2 * ((x + y) / 2)) 2 =
    HMul.hMul (α := ℤ) 2 2 * (HPow.hPow (β := ℕ) ((x - y) / 2) 2 + HPow.hPow (β := ℕ) ((x + y) / 2) 2)
have nlinarith : HPow.hPow (β := ℕ) (2 * ((x - y) / 2)) 2 + HPow.hPow (β := ℕ) (2 * ((x + y) / 2)) 2 <
    HMul.hMul (α := ℤ) 2 2 * (HPow.hPow (β := ℕ) ((x - y) / 2) 2 + HPow.hPow (β := ℕ) ((x + y) / 2) 2) →
  -1 +
      (HPow.hPow (β := ℕ) (2 * ((x - y) / 2)) 2 + HPow.hPow (β := ℕ) (2 * ((x + y) / 2)) 2 + 1 -
        HMul.hMul (α := ℤ) 2 2 * (HPow.hPow (β := ℕ) ((x - y) / 2) 2 + HPow.hPow (β := ℕ) ((x + y) / 2) 2)) =
    0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
m x y : ℤ
h : 2 * m = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
this : Even (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2)
nlinarith :
  HPow.hPow (β := ℕ) (2 * ((x - y) / 2)) 2 + HPow.hPow (β := ℕ) (2 * ((x + y) / 2)) 2 <
      HMul.hMul (α := ℤ) 2 2 * (HPow.hPow (β := ℕ) ((x - y) / 2) 2 + HPow.hPow (β := ℕ) ((x + y) / 2) 2) →
    -1 +
        (HPow.hPow (β := ℕ) (2 * ((x - y) / 2)) 2 + HPow.hPow (β := ℕ) (2 * ((x + y) / 2)) 2 + 1 -
          HMul.hMul (α := ℤ) 2 2 * (HPow.hPow (β := ℕ) ((x - y) / 2) 2 + HPow.hPow (β := ℕ) ((x + y) / 2) 2)) =
      0
⊢ HPow.hPow (β := ℕ) (2 * ((x - y) / 2)) 2 + HPow.hPow (β := ℕ) (2 * ((x + y) / 2)) 2 =
    HMul.hMul (α := ℤ) 2 2 * (HPow.hPow (β := ℕ) ((x - y) / 2) 2 + HPow.hPow (β := ℕ) ((x + y) / 2) 2)
have nlinarith₁ : HMul.hMul (α := ℤ) 2 2 * (HPow.hPow (β := ℕ) ((x - y) / 2) 2 + HPow.hPow (β := ℕ) ((x + y) / 2) 2) <
    HPow.hPow (β := ℕ) (2 * ((x - y) / 2)) 2 + HPow.hPow (β := ℕ) (2 * ((x + y) / 2)) 2 →
  -1 +
      (HMul.hMul (α := ℤ) 2 2 * (HPow.hPow (β := ℕ) ((x - y) / 2) 2 + HPow.hPow (β := ℕ) ((x + y) / 2) 2) + 1 -
        (HPow.hPow (β := ℕ) (2 * ((x - y) / 2)) 2 + HPow.hPow (β := ℕ) (2 * ((x + y) / 2)) 2)) =
    0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
a b c d k m : ℕ
h : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = k * m
ha : 2 * a < m
hb : 2 * b < m
hc : 2 * c < m
hd : 2 * d < m
⊢ k < m
have nlinarith : m ≤ k →
  HMul.hMul (α := ℤ) 4 (-1) + 10 * HSub.hSub (α := ℤ) 0 (↑a : ℤ) + 2 * HSub.hSub (α := ℤ) 0 (↑b : ℤ) +
                              2 * HSub.hSub (α := ℤ) 0 (↑c : ℤ) +
                            2 * HSub.hSub (α := ℤ) 0 (↑d : ℤ) +
                          4 *
                            -(HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 +
                                    HPow.hPow (α := ℤ) (β := ℕ) (↑c : ℤ) 2 +
                                  HPow.hPow (α := ℤ) (β := ℕ) (↑d : ℤ) 2 -
                                HMul.hMul (α := ℤ) (↑k : ℤ) (↑m : ℤ)) +
                        4 * (HMul.hMul (α := ℤ) 2 (↑a : ℤ) + 1 - (↑m : ℤ)) +
                      (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * (HMul.hMul (α := ℤ) 2 (↑a : ℤ) + 1 - (↑m : ℤ))) +
                    (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * (HMul.hMul (α := ℤ) 2 (↑b : ℤ) + 1 - (↑m : ℤ))) +
                  (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * (HMul.hMul (α := ℤ) 2 (↑c : ℤ) + 1 - (↑m : ℤ))) +
                (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * (HMul.hMul (α := ℤ) 2 (↑d : ℤ) + 1 - (↑m : ℤ))) +
              4 * (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * HSub.hSub (α := ℤ) (↑m : ℤ) (↑k : ℤ)) +
            2 * (0 - HSub.hSub (α := ℤ) 0 (↑a : ℤ) * (HMul.hMul (α := ℤ) 2 (↑a : ℤ) + 1 - (↑m : ℤ))) +
          2 * (0 - HSub.hSub (α := ℤ) 0 (↑b : ℤ) * (HMul.hMul (α := ℤ) 2 (↑b : ℤ) + 1 - (↑m : ℤ))) +
        2 * (0 - HSub.hSub (α := ℤ) 0 (↑c : ℤ) * (HMul.hMul (α := ℤ) 2 (↑c : ℤ) + 1 - (↑m : ℤ))) +
      2 * (0 - HSub.hSub (α := ℤ) 0 (↑d : ℤ) * (HMul.hMul (α := ℤ) 2 (↑d : ℤ) + 1 - (↑m : ℤ))) =
    0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
a b c d k m : ℕ
h : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = k * m
ha : 2 * a < m
hb : 2 * b < m
hc : 2 * c < m
hd : 2 * d < m
nlinarith :
  m ≤ k →
    HMul.hMul (α := ℤ) 4 (-1) + 10 * HSub.hSub (α := ℤ) 0 (↑a : ℤ) + 2 * HSub.hSub (α := ℤ) 0 (↑b : ℤ) +
                                2 * HSub.hSub (α := ℤ) 0 (↑c : ℤ) +
                              2 * HSub.hSub (α := ℤ) 0 (↑d : ℤ) +
                            4 *
                              -(HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 +
                                      HPow.hPow (α := ℤ) (β := ℕ) (↑c : ℤ) 2 +
                                    HPow.hPow (α := ℤ) (β := ℕ) (↑d : ℤ) 2 -
                                  HMul.hMul (α := ℤ) (↑k : ℤ) (↑m : ℤ)) +
                          4 * (HMul.hMul (α := ℤ) 2 (↑a : ℤ) + 1 - (↑m : ℤ)) +
                        (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * (HMul.hMul (α := ℤ) 2 (↑a : ℤ) + 1 - (↑m : ℤ))) +
                      (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * (HMul.hMul (α := ℤ) 2 (↑b : ℤ) + 1 - (↑m : ℤ))) +
                    (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * (HMul.hMul (α := ℤ) 2 (↑c : ℤ) + 1 - (↑m : ℤ))) +
                  (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * (HMul.hMul (α := ℤ) 2 (↑d : ℤ) + 1 - (↑m : ℤ))) +
                4 * (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * HSub.hSub (α := ℤ) (↑m : ℤ) (↑k : ℤ)) +
              2 * (0 - HSub.hSub (α := ℤ) 0 (↑a : ℤ) * (HMul.hMul (α := ℤ) 2 (↑a : ℤ) + 1 - (↑m : ℤ))) +
            2 * (0 - HSub.hSub (α := ℤ) 0 (↑b : ℤ) * (HMul.hMul (α := ℤ) 2 (↑b : ℤ) + 1 - (↑m : ℤ))) +
          2 * (0 - HSub.hSub (α := ℤ) 0 (↑c : ℤ) * (HMul.hMul (α := ℤ) 2 (↑c : ℤ) + 1 - (↑m : ℤ))) +
        2 * (0 - HSub.hSub (α := ℤ) 0 (↑d : ℤ) * (HMul.hMul (α := ℤ) 2 (↑d : ℤ) + 1 - (↑m : ℤ))) =
      0
⊢ k < m
have nlinarith₁ : m ≤ k → GT.gt (α := ℤ) 4 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
a b c d k m : ℕ
h : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = k * m
ha : 2 * a < m
hb : 2 * b < m
hc : 2 * c < m
hd : 2 * d < m
nlinarith :
  m ≤ k →
    HMul.hMul (α := ℤ) 4 (-1) + 10 * HSub.hSub (α := ℤ) 0 (↑a : ℤ) + 2 * HSub.hSub (α := ℤ) 0 (↑b : ℤ) +
                                2 * HSub.hSub (α := ℤ) 0 (↑c : ℤ) +
                              2 * HSub.hSub (α := ℤ) 0 (↑d : ℤ) +
                            4 *
                              -(HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 +
                                      HPow.hPow (α := ℤ) (β := ℕ) (↑c : ℤ) 2 +
                                    HPow.hPow (α := ℤ) (β := ℕ) (↑d : ℤ) 2 -
                                  HMul.hMul (α := ℤ) (↑k : ℤ) (↑m : ℤ)) +
                          4 * (HMul.hMul (α := ℤ) 2 (↑a : ℤ) + 1 - (↑m : ℤ)) +
                        (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * (HMul.hMul (α := ℤ) 2 (↑a : ℤ) + 1 - (↑m : ℤ))) +
                      (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * (HMul.hMul (α := ℤ) 2 (↑b : ℤ) + 1 - (↑m : ℤ))) +
                    (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * (HMul.hMul (α := ℤ) 2 (↑c : ℤ) + 1 - (↑m : ℤ))) +
                  (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * (HMul.hMul (α := ℤ) 2 (↑d : ℤ) + 1 - (↑m : ℤ))) +
                4 * (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * HSub.hSub (α := ℤ) (↑m : ℤ) (↑k : ℤ)) +
              2 * (0 - HSub.hSub (α := ℤ) 0 (↑a : ℤ) * (HMul.hMul (α := ℤ) 2 (↑a : ℤ) + 1 - (↑m : ℤ))) +
            2 * (0 - HSub.hSub (α := ℤ) 0 (↑b : ℤ) * (HMul.hMul (α := ℤ) 2 (↑b : ℤ) + 1 - (↑m : ℤ))) +
          2 * (0 - HSub.hSub (α := ℤ) 0 (↑c : ℤ) * (HMul.hMul (α := ℤ) 2 (↑c : ℤ) + 1 - (↑m : ℤ))) +
        2 * (0 - HSub.hSub (α := ℤ) 0 (↑d : ℤ) * (HMul.hMul (α := ℤ) 2 (↑d : ℤ) + 1 - (↑m : ℤ))) =
      0
nlinarith₁ : m ≤ k → GT.gt (α := ℤ) 4 0
⊢ k < m
have nlinarith₂ : m ≤ k → GT.gt (α := ℤ) 10 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
a b c d k m : ℕ
h : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = k * m
ha : 2 * a < m
hb : 2 * b < m
hc : 2 * c < m
hd : 2 * d < m
nlinarith :
  m ≤ k →
    HMul.hMul (α := ℤ) 4 (-1) + 10 * HSub.hSub (α := ℤ) 0 (↑a : ℤ) + 2 * HSub.hSub (α := ℤ) 0 (↑b : ℤ) +
                                2 * HSub.hSub (α := ℤ) 0 (↑c : ℤ) +
                              2 * HSub.hSub (α := ℤ) 0 (↑d : ℤ) +
                            4 *
                              -(HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 +
                                      HPow.hPow (α := ℤ) (β := ℕ) (↑c : ℤ) 2 +
                                    HPow.hPow (α := ℤ) (β := ℕ) (↑d : ℤ) 2 -
                                  HMul.hMul (α := ℤ) (↑k : ℤ) (↑m : ℤ)) +
                          4 * (HMul.hMul (α := ℤ) 2 (↑a : ℤ) + 1 - (↑m : ℤ)) +
                        (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * (HMul.hMul (α := ℤ) 2 (↑a : ℤ) + 1 - (↑m : ℤ))) +
                      (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * (HMul.hMul (α := ℤ) 2 (↑b : ℤ) + 1 - (↑m : ℤ))) +
                    (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * (HMul.hMul (α := ℤ) 2 (↑c : ℤ) + 1 - (↑m : ℤ))) +
                  (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * (HMul.hMul (α := ℤ) 2 (↑d : ℤ) + 1 - (↑m : ℤ))) +
                4 * (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * HSub.hSub (α := ℤ) (↑m : ℤ) (↑k : ℤ)) +
              2 * (0 - HSub.hSub (α := ℤ) 0 (↑a : ℤ) * (HMul.hMul (α := ℤ) 2 (↑a : ℤ) + 1 - (↑m : ℤ))) +
            2 * (0 - HSub.hSub (α := ℤ) 0 (↑b : ℤ) * (HMul.hMul (α := ℤ) 2 (↑b : ℤ) + 1 - (↑m : ℤ))) +
          2 * (0 - HSub.hSub (α := ℤ) 0 (↑c : ℤ) * (HMul.hMul (α := ℤ) 2 (↑c : ℤ) + 1 - (↑m : ℤ))) +
        2 * (0 - HSub.hSub (α := ℤ) 0 (↑d : ℤ) * (HMul.hMul (α := ℤ) 2 (↑d : ℤ) + 1 - (↑m : ℤ))) =
      0
nlinarith₁ : m ≤ k → GT.gt (α := ℤ) 4 0
nlinarith₂ : m ≤ k → GT.gt (α := ℤ) 10 0
⊢ k < m
have nlinarith₃ : m ≤ k → GT.gt (α := ℤ) 2 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < p ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * p
have inl : ∀ [hp : Fact (Nat.Prime 2)],
  ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < 2 ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * 2
Tactic: rcases hp.1.eq_two_or_odd' with (rfl | hodd)
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
inl :
  ∀ [hp : Fact (Nat.Prime 2)],
    ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < 2 ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * 2
⊢ ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < p ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * p
have inr : ∀ (hodd : Odd p), ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < p ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * p
Tactic: rcases hp.1.eq_two_or_odd' with (rfl | hodd)
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
hp : Fact (Nat.Prime 2)
⊢ ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < 2 ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * 2
have h : LT.lt (α := ℕ) 0 1 ∧
  LT.lt (α := ℕ) 1 2 ∧ HPow.hPow (α := ℕ) (β := ℕ) 1 2 + HPow.hPow (α := ℕ) (β := ℕ) 0 2 + 1 = HMul.hMul (α := ℕ) 1 2
Tactic: use 1, 0, 1
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
⊢ ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < p ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * p
have inr : ∀ (a b : ℕ) (ha : a ≤ p / 2) (hb : b ≤ p / 2)
  (hab : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ -1 [ZMOD (↑p : ℤ)]),
  ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < p ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * p
Tactic: rcases Nat.sq_add_sq_zmodEq p (-1) with ⟨a, b, ha, hb, hab⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ -1 [ZMOD (↑p : ℤ)]
⊢ ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < p ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * p
have inr : ∀ (k : ℤ) (hk : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 - -1 = (↑p : ℤ) * k),
  ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < p ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * p
Tactic: rcases Int.modEq_iff_dvd.1 hab.symm with ⟨k, hk⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ -1 [ZMOD (↑p : ℤ)]
k : ℤ
hk : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 - -1 = (↑p : ℤ) * k
⊢ ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < p ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * p
have hk₁ : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 + 1 = k * (↑p : ℤ)
Tactic: rw [sub_neg_eq_add, mul_comm] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ -1 [ZMOD (↑p : ℤ)]
k : ℤ
hk : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 + 1 = k * (↑p : ℤ)
⊢ 0 < k
have refine : 0 < k * (↑p : ℤ)
Tactic: refine pos_of_mul_pos_left ?_ (Nat.cast_nonneg p)