Using a forall hypothesis

Stream: new members

[JK]

I am not sure why the first proof works and the second doesn't:

import Mathlib
example {a : ℚ} (h : ∀ b : ℚ, a ≥ -3 + 4 * b - b ^ 2) : a ≥ -3 + 4*2 - 2^2 := by
  exact h 2

example {n : ℤ} (hn : ∀ m, 1 ≤ m → m ≤ 5 → m ∣ n) : 1 ≤ 3 → 3 ≤ 5 → 3 ∣ n := by
  exact hn 3

How can I start the proof in the second case?

[Weiyi Wang]

it is type annotation problem. You need to annotate m as \Z, otherwise it is inferred as Nat

[JK]

That doesn't solve it for me; the following still fails

import Mathlib
example {n : ℤ} (hn : ∀ m:ℤ, 1 ≤ m → m ≤ 5 → m ∣ n) : 1 ≤ 3 → 3 ≤ 5 → 3 ∣ n := by
  exact hn 3

[Chris Bailey]

example {n : ℤ} (hn : ∀ m, 1 ≤ m → m ≤ 5 → m ∣ n) : (1 : Int) ≤ 3 → (3 : Int) ≤ 5 → 3 ∣ n := by
  exact hn 3

The type errors are fairly helpful in this case.

[Weiyi Wang]

oops, I meant annotating 1

[Chris Bailey]

Without adding the curve ball of ℚ I think the paths for elaborating nat literals as Nat instead of something else are much more "in your face".

[JK]

What if I wanted to treat 1 as a Nat?

[Chris Bailey]

In some cases you'll need to be explicit about the types you want if you also want to use nat literals and other notation that doesn't immediately make clear what type it's working with.

[JK]

and why doesn't

example {n : ℤ} (hn : ∀ m, 1 ≤ m → m ≤ 5 → m ∣ n) : 1:ℤ ≤ 3 → 3:ℤ ≤ 5 → 3 ∣ n := by
  exact hn 3

work?

[JK]

Oh, I see with parentheses is does work

[Chris Bailey]

The error message strongly suggests a parse error: unexpected token ':'; expected ':=', 'where' or '|'

[Ruben Van de Velde]

You need the parentheses around the type ascription

[Ruben Van de Velde]

They're a fundamental part of the syntax