## Stream: new members

### Topic: a trivial question

#### Alex Zhang (Jun 24 2021 at 11:02):

If I have

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


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

(deleted)

#### Eric Rodriguez (Jun 24 2021 at 11:07):

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

#### Alex Zhang (Jun 24 2021 at 11:23):

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

#### Eric Rodriguez (Jun 24 2021 at 11:27):

that's what the rw does

#### Eric Rodriguez (Jun 24 2021 at 11:28):

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

#### Yakov Pechersky (Jun 24 2021 at 12:37):

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

docs#congr_fun

#### Eric Wieser (Jun 24 2021 at 13:44):

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

#### Alex Zhang (Jun 27 2021 at 08:35):

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 (Jun 27 2021 at 08:49):

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 (Jun 27 2021 at 08:53):

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 (Jun 27 2021 at 09:33):

I got a better one.

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


Last updated: Dec 20 2023 at 11:08 UTC