using lemmas

Stream: new members

[Arthur Paulino]

Suppose I have a lemma p → q and, in my current state goal I have h: p. How do I add q to my set of valid truths?

[Bolton Bailey]

You can use have hq := my_lemma h,

[Arthur Paulino]

Hm, it's not working. This is my lemma:

lemma is_tree_then_card_edges_le_card_vertices [fintype G.edge_set] [fintype V] :
  G.is_tree → G.edge_set.to_finset.card < card V

In my state I have h: G.is_tree

If I do have hq := is_tree_then_card_edges_le_card_vertices h I get the error:

type mismatch at application
  is_tree_then_card_edges_le_card_vertices h
term
  h
has type
  G.is_tree : Prop
but is expected to have type
  simple_graph ?m_1 : Type ?

[Anupam Nayak]

The lemma eats more arguments than it seems from the statement. The arguments must have been be declared above the lemma. Try putting underscores between is_... and h

[Arthur Paulino]

It works! thank you

[Anupam Nayak]

Infact, I think the problem is that those arguments to the lemma should have been implicit, but are needed explicitly because you used ()

[Scott Morrison]

Anytime you're putting in underscores to use something that you've written a moment ago, you should go back and consider changing the binders.

[Scott Morrison]

It take a little while to learn the correct binders, but once you do it's usually most efficient to get them right as you write the lemmas!