## Stream: new members

### Topic: Basic questions

#### Johan Commelin (Sep 08 2020 at 05:08):

Nope... we should make apply_fun more flexible, but isn't exactly what you are looking for.

#### Johan Commelin (Sep 08 2020 at 05:09):

Note that replace is like have but -- you know -- replaces a hypothesis

#### Benjamin (Sep 08 2020 at 05:33):

Sometimes when playing the natural number game, I encountered weird variables like ?m_1, ?m_2, and so on after using apply. What do these mean?

I also have a question about substituting some value into a theorem. I have the following: mul_pos (a b : mynat) : a ≠ 0 → b ≠ 0 → a * b ≠ 0. How can I use this theorem but substituting succ(a) and succ(b) into a and b respectively?

#### Mario Carneiro (Sep 08 2020 at 05:35):

they are metavariables, they are expressions that are concrete but not known yet. They often go away if you just pretend they already have the expression you want in there

#### Mario Carneiro (Sep 08 2020 at 05:36):

to substitute that theorem use mul_pos (succ a) (succ b)

#### Mario Carneiro (Sep 08 2020 at 05:37):

usually a and b will be implicit though (written like {a : mynat}), in which case you would have to write @mul_pos (succ a) (succ b), or let lean figure it out with mul_pos

#### Benjamin (Sep 08 2020 at 06:37):

Thanks. Another issue I ran into is I have the following two hypotheses: k : a * succ d = a * d → succ d = d, i : a * succ d = a * h. I want to do a rewrite do I type "rw i at k", which gives me the error "rewrite tactic failed, lemma lhs is a metavariable". What does this mean? And how do I fix it?

#### Kevin Buzzard (Sep 08 2020 at 06:44):

The error is surprising -- do you have more than one thing called i? But you look to me like you're in trouble with the maths here, not the lean. How can you use k when its hypothesis is almost always false?

#### Kevin Buzzard (Sep 08 2020 at 06:46):

If you want some help you should post an #mwe or, if you're doing the natural number game, send a link to the level you're on and post the code you wrote so far to solve it

#### Benjamin (Sep 08 2020 at 06:48):

I'm on the last level of the advanced multiplication part of the natural number game. Here's what I have so far (I renamed i to j2 to insure it wasn't causing any trouble): revert b, induction c with d hd, rw mul_zero, have p := mul_eq_zero_iff, intro h, intro j, cases h, refl, have i := mul_eq_zero_iff a (succ h), cases i with i1 i2, have i3 := i1(j), cc, intro h, have j := hd(h), have k := hd(succ d), intro j2, symmetry at j2, rw j2 at k,

#### Johan Commelin (Sep 08 2020 at 06:57):

@Benjamin pro tip: #backticks (-;

#### Ruben Van de Velde (Sep 08 2020 at 07:00):

https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=9&level=4

revert b,
induction c with d hd,
rw mul_zero,
have p := mul_eq_zero_iff,
intro h,
intro j,
cases h,
refl,
have i := mul_eq_zero_iff a (succ h),
cases i with i1 i2,
have i3 := i1(j),
cc,
intro h,
have j := hd(h),
have k := hd(succ d),
intro j2,
symmetry at j2,
rw j2 at k,


#### Ruben Van de Velde (Sep 08 2020 at 07:00):

That's certainly weird

#### Benjamin (Sep 08 2020 at 07:03):

I think my math is off anyway, but I don't know why rw didn't work there. FWIW, changing both with mul_suc and then doing rw worked.

#### Benjamin (Sep 08 2020 at 07:17):

I think I'm somewhat close up to cc. After that, did I go down the right path? I'm not sure whether I'm manipulating the universal statements right.

#### Ruben Van de Velde (Sep 08 2020 at 07:21):

Your k : a * succ d = a * d → succ d = d doesn't seem useful; the consequent is false

#### Ruben Van de Velde (Sep 08 2020 at 07:22):

I started with

intros b hb,
cases b,


Does that help?

#### Benjamin (Sep 08 2020 at 16:47):

Much obliged, I figured it out

#### Benjamin (Sep 08 2020 at 19:27):

How can I introduce an existential? For example, if I have a = succ(a) + c, I want to get the existential statement to get succ(a) <= a (this is for a proof by contradiction of course).

#### Ruben Van de Velde (Sep 08 2020 at 19:32):

Probably use c,

#### Ruben Van de Velde (Sep 08 2020 at 19:34):

That is,

have : \exists m, a = succ a + m,
{ use b, sorry },


#### Benjamin (Sep 08 2020 at 19:40):

I'm getting this error failed to instantiate goal with (frozen_name has_add.add) c1 c2 What I have is h2_h : a = succ a + c1 + c2 and I typed have p := ∃ m, a = succ a + m, {use c1 + c2},.

#### Ruben Van de Velde (Sep 08 2020 at 19:42):

:, not :=

#### Benjamin (Sep 08 2020 at 19:46):

That fixed one error, but now I think there's a problem because use acts on the goal, and I need it to act on h2_h. Is there a way to do that? The error is solve1 tactic failed, focused goal has not been solved.

#### Reid Barton (Sep 08 2020 at 19:50):

After use you still have a goal: to prove that the value you provided satisfies whatever property it's supposed to.

#### Benjamin (Sep 08 2020 at 19:54):

How can I say that it's true by h2_h? Also, is there a better way to go from a = succ a + c1 + c2, to succ a <= a?

#### Benjamin (Sep 08 2020 at 19:56):

Ah, nvm, I think I see how this works now

#### Benjamin (Sep 08 2020 at 19:57):

Got it! Thanks for the help.

Last updated: Dec 20 2023 at 11:08 UTC