a trivial question

Stream: new members

[Alex Zhang]

If I have

h: f = λ x, ...
x:ℕ

in the context,
is there any tactic that can change h to h : f x = ...?

[Eric Rodriguez]

(deleted)

[Eric Rodriguez]

i'd usually go with rw function.funext_iff at hf, specialize hf x but there may be better

[Alex Zhang]

Any more convenient way? How about change h to \all y, h y = ...?

[Eric Rodriguez]

that's what the rw does

[Eric Rodriguez]

usually you dan just rw h into wherever you need it, though

[Yakov Pechersky]

The answer to the first question is replace h := congr_fun h x

[Eric Wieser]

docs#congr_fun

[Eric Wieser]

The answer to the second question is replace h := congr_fun h without the x

[Alex Zhang]

import tactic

example {m n : ℕ+} :
  (↑m : ℕ)- 1 < ↑m :=
begin
  apply sub_one_lt ↑m,
end

Why does this fail ?
What is a convenient way to close this goal?

[Alex J. Best]

Firstly, it is quite often best to use an explicit type ascription rather than the up arrow, in this case lean doesn't even know what you want ↑m to mean which makes the error hard to understand, when we do this instead

import tactic

example {m n : ℕ+} :
  (m : ℕ)- 1 < (m:ℕ) :=
begin
  apply sub_one_lt (m:ℕ),
end

then the error message is much more readable

failed to synthesize type class instance for
m n : ℕ+
⊢ linear_ordered_ring ℕ
state:
m n : ℕ+
⊢ ↑m - 1 < ↑m

Lean is complaining that docs#sub_one_lt is a theorem about linear_ordered_rings and that nat isn't such a ring.

[Alex J. Best]

Here's one proof

import tactic

example {m n : ℕ+} :
  (m : ℕ) - 1 < (m:ℕ) :=
begin
  cases m,
  simp,
  exact nat.sub_lt_self m_property zero_lt_one,
end

[Alex Zhang]

I got a better one.

example {m n : ℕ+} :
  (↑m : ℕ)- 1 < ↑m := by  simp [nat.sub_lt]