4 proofs from The Mechanics

Stream: new members

[Michael Bucko]

I wrote 4 more proofs from chapter 4 from The Mechanics.. How can I optimize them?

4 proofs

import Mathlib
import Lean

example {n : ℤ} (hn : ∀ m, 1 ≤ m → m ≤ 5 → m ∣ n) : 15 ∣ n := by
  have h3 : 3 ∣ n := by
    exact hn 3 (by linarith) (by linarith)
  have h5 : 5 ∣ n := by
    exact hn 5 (by linarith) (by linarith)
  have h15 : lcm 3 5 ∣ n := lcm_dvd h3 h5
  exact h15

example {a b : ℝ} (ha1 : a ^ 2 ≤ 2) (hb1 : b ^ 2 ≤ 2)
    (ha2 : ∀ y, y ^ 2 ≤ 2 → y ≤ a)
    (hb2 : ∀ y, y ^ 2 ≤ 2 → y ≤ b) :
    a = b := by
  apply le_antisymm
  · apply hb2
    apply ha1
  · apply ha2
    apply hb1

example {a : ℚ} (h : ∀ b : ℚ, a ≥ -3 + 4 * b - b ^ 2) : a ≥ 1 :=
calc
  a ≥  -3 + 4 * 2 - 2^2  := h 2
  _ ≥ 1 := by norm_num

example : ∃ n : ℕ, ∀ m : ℕ, n ≤ m := by
  use 0
  intro m
  exact zero_le m

[Bjørn Kjos-Hanssen]

example : ∃ n : ℕ, ∀ m : ℕ, n ≤ m := ⟨0, zero_le⟩

[Ilmārs Cīrulis]

I don't know if this is much of optimization, but here's the first example.
(All the by exact was removed.) And it seems that I can replace linarith with omega, too.

example {n : ℤ} (hn : ∀ m, 1 ≤ m → m ≤ 5 → m ∣ n) : 15 ∣ n := by
  have h3 : 3 ∣ n := hn 3 (by linarith) (by linarith)
  have h5 : 5 ∣ n := hn 5 (by linarith) (by linarith)
  exact lcm_dvd h3 h5

[Ilmārs Cīrulis]

I don't believe that anything else can be optimized, except post by Bjørn (and maybe mine).

[Michael Bucko]

Both your example and Bjørn's are great improvements from my perspective. :thank_you:

Is there any way to write such a chain (by linarith) (by linarith) differently? Perhaps using ⟨⟩?

Also, I'll learn more about omega, too.

[Ruben Van de Velde]

You could write by apply hn 3 <;> linarith