None theorem

Stream: new members

[Ken Roe]

Does someone know what tactic to use to prove the following:

theorem nonethm {t} : (none <|> none)=@none t:=
begin
    ...
end

[Chris Hughes]

theorem nonethm {t} : (none <|> none)=@none t:= rfl

[Mario Carneiro]

lol. by simp also works if you have import data.option

[Patrick Massot]

Chris, you lose: Ken asked for a tactic. The best answer was refl :yum:

[Patrick Massot]

A slightly more serious answer: I think stating the result as theorem nonethm {t} : (none <|> none)= (none : option t) makes it easier to read. I mention this because it's a general trick: you can often avoid using @ by adding a type ascription.

[Ken Roe]

Thanks. A couple more questions:
1) I found data/option.lean in mathlib. Where should I place the mathlib repository with respect to the Lean repository? How do I configure VSCode so that it starts Lean with the appropriate search path?

2) Next, how do I prove the theorem:

theorem nonethm {t} {x:option t} : (x <|> none)=x:= begin
    ...
end

[Kenny Lau]

theorem nonethm {t} {x : option t} : (x <|> none) = x :=
begin
  cases x; refl
end

[Bryan Gin-ge Chen]

For question 1 I recommend using leanpkg. The advice on the xena blog is a little old but still worked for me a month or so ago.