a b c d k m : ℕ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = k * m
ha : 2 * a < m
hb : 2 * b < m
hc : 2 * c < m
hd : 2 * d < m
⊢ 2 ^ 2 * (k * m) < 2 ^ 2 * (m * m)
a b c d k m : ℕ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = k * m
ha : 2 * a < m
hb : 2 * b < m
hc : 2 * c < m
hd : 2 * d < m
⊢ k < m
refine lt_of_mul_lt_mul_right (lt_of_mul_lt_mul_left ?_ (zero_le (2 ^ 2))) (zero_le m)
no goals
a b c d k m : ℕ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = k * m
ha : 2 * a < m
hb : 2 * b < m
hc : 2 * c < m
hd : 2 * d < m
⊢ 2 ^ 2 * (k * m) < 2 ^ 2 * (m * m)
calc
  2 ^ 2 * (k * ↑m) = ∑ i : Fin 4, (2 * ![a, b, c, d] i) ^ 2 := by
    simp [← h, Fin.sum_univ_succ, mul_add, mul_pow, add_assoc]
  _ < ∑ _i : Fin 4, m ^ 2 := Finset.sum_lt_sum_of_nonempty Finset.univ_nonempty fun i _ ↦ by
    refine pow_lt_pow_of_lt_left ?_ (zero_le _) two_pos
    fin_cases i <;> assumption
  _ = 2 ^ 2 * (m * m) := by simp; ring
no goals
a b c d k m : ℕ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = k * m
ha : 2 * a < m
hb : 2 * b < m
hc : 2 * c < m
hd : 2 * d < m
⊢ 2 ^ 2 * (k * m) = ∑ i : Fin 4, (2 * Matrix.vecCons a ![b, c, d] i) ^ 2
simp [← h, Fin.sum_univ_succ, mul_add, mul_pow, add_assoc]
a b c d k m : ℕ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = k * m
ha : 2 * a < m
hb : 2 * b < m
hc : 2 * c < m
hd : 2 * d < m
i : Fin 4
x✝ : i ∈ univ
⊢ 2 * Matrix.vecCons a ![b, c, d] i < m
a b c d k m : ℕ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = k * m
ha : 2 * a < m
hb : 2 * b < m
hc : 2 * c < m
hd : 2 * d < m
i : Fin 4
x✝ : i ∈ univ
⊢ (2 * Matrix.vecCons a ![b, c, d] i) ^ 2 < m ^ 2
refine pow_lt_pow_of_lt_left ?_ (zero_le _) two_pos
no goals
a b c d k m : ℕ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = k * m
ha : 2 * a < m
hb : 2 * b < m
hc : 2 * c < m
hd : 2 * d < m
i : Fin 4
x✝ : i ∈ univ
⊢ 2 * Matrix.vecCons a ![b, c, d] i < m
fin_cases i <;> assumption
a b c d k m : ℕ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = k * m
ha : 2 * a < m
hb : 2 * b < m
hc : 2 * c < m
hd : 2 * d < m
⊢ 4 * m ^ 2 = 2 ^ 2 * (m * m)
a b c d k m : ℕ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = k * m
ha : 2 * a < m
hb : 2 * b < m
hc : 2 * c < m
hd : 2 * d < m
⊢ ∑ _i : Fin 4, m ^ 2 = 2 ^ 2 * (m * m)
simp
no goals
a b c d k m : ℕ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = k * m
ha : 2 * a < m
hb : 2 * b < m
hc : 2 * c < m
hd : 2 * d < m
⊢ 4 * m ^ 2 = 2 ^ 2 * (m * m)
ring