How to prove it with lean

Stream: new members

[Shubham Kumar 🦀 (he/him)]

I'm trying to go through How to prove it with lean but there seem to be some outdated tactic like assume which SO mentions is now intro but how would I specifiy what I want to intro - for eg. assume h2 : ¬R should be intro h2 : ¬R but : is not syntactically valid for this statement.

TL;DR : What should I be syntactically the correct way to write assume h2 : ¬R in lean4?

[Yagub Aliyev]

Shubham Kumar 🦀 (he/him) said:

I'm trying to go through How to prove it with lean but there seem to be some outdated tactic like assume which SO mentions is now intro but how would I specifiy what I want to intro - for eg. assume h2 : ¬R should be intro h2 : ¬R but : is not syntactically valid for this statement.

TL;DR : What should I be syntactically the correct way to write assume h2 : ¬R in lean4?

Have you tried suffices h : P?
have and revert can also be helpful. Here are instructions from Set Theory Game https://adam.math.hhu.de/#/

Use intro to introduce either a new assumption or a new object into your proof.

There are two situations in which you can use the intro tactic:

If you are proving a statement of the form P → Q, then you can use the tactic intro h to introduce the assumption h : P and set Q as the goal. Be sure to use an identifier that is not already in use.
If you are proving a statement of the form ∀ x, P x, where P x is some statement about x, then you can use the tactic intro x to introduce a new object x into the proof. Be sure to use a variable name that is not already in use. The goal will then be P x.
You can do multiple introductions in one step: for example, intro x h has the same effect as doing intro x followed by intro h.

[Shubham Kumar 🦀 (he/him)]

Thanks! one question so when you mention object you mean parameter passed to a proposition, right?

[Shubham Kumar 🦀 (he/him)]

also the following 2 statements are syntactically incorrect way I'm guessing because it doesn't expect suffices after the hypothesis

  suffices h2 : ¬R
  suffices h3 : P

[Shubham Kumar 🦀 (he/him)]

unexpected token 'suffices'; expected 'by' or 'from'Lean 4

[Ruben Van de Velde]

suffices is not a correct replacement for assume; you want intro

[Shubham Kumar 🦀 (he/him)]

can I specify proposition I want to intro?
For eg. intro h2 : P ?

[Ruben Van de Velde]

I think that might work with the rintro variant, e.g. rintro (h2 : P)

[Shubham Kumar 🦀 (he/him)]

because : => unexpected token ':'; expected commandLean 4

[Shubham Kumar 🦀 (he/him)]

Thanks, I need to lookup rintro/intro diff

[Shubham Kumar 🦀 (he/him)]

Found it : https://leanprover-community.github.io/mathlib4_docs/Std/Tactic/RCases.html#Std.Tactic.RCases.rcases
for my future self

[Shubham Kumar 🦀 (he/him)]

oops cannot find rintro do I need to import Std ?

[Shubham Kumar 🦀 (he/him)]

ok so I need to make Std available in lakefile because it's not available as prelude or equivalent

[Dan Velleman]

@Shubham Kumar 🦀 (he/him) How To Prove It with Lean requires a Lean package that you have to download. That package defines a number of tactics that are used in the book, including assume. See the preface, the section on installing Lean.