variable not working

Stream: new members

[Iván Renison]

Hi, do you know why is this not working? image.png

It seems that for some reason hn is not becoming an argument of hn', but I don't understand why

[Iván Renison]

Here the code:

import Mathlib

variable {n : ℕ} (hn : n ≠ 0)

lemma hn' : 1 < 2 * n + 1 := by
  refine Nat.lt_add_of_pos_left ?_
  refine Nat.succ_mul_pos 1 ?_
  apply Nat.zero_lt_of_ne_zero hn

[Ruben Van de Velde]

include hn

[Ruben Van de Velde]

Theorems don't pick up Prop hypotheses from variable unless they're used in the statement

[Kevin Buzzard]

include hn in
lemma hn' : 1 < 2 * n + 1 := by
  refine Nat.lt_add_of_pos_left ?_
  refine Nat.succ_mul_pos 1 ?_
  apply Nat.zero_lt_of_ne_zero hn

[Iván Renison]

Ruben Van de Velde said:

Theorems don't pick up Prop hypotheses from variable unless they're used in the statement

Ah, okay, thank you very much

[Philippe Duchon]

Ruben Van de Velde said:

Theorems don't pick up Prop hypotheses from variable unless they're used in the statement

Is this specific to Prop hypotheses? I thought it applied to all variable

[Ruben Van de Velde]

You may be right, yes. About the Prop ones I'm sure, at least :)