Use a hypothesis¶

A hypothesis in the context, above the ⊢, is a proof we are allowed to use. This page shows the ways of using one, depending on its shape and on how closely it matches the goal.

An exact match¶

When a hypothesis, or a part of one, is exactly the goal, exact closes the goal with it. The parts of a conjunction are .1 and .2:

example {Strategy : Type} {payoffs : Strategy → Strategy → ℝ} {resident : Strategy}
    (stable : IsESSNashFirst payoffs resident) : IsSymmetricNash payoffs resident := by
  exact stable.1

A statement for every strategy¶

A hypothesis beginning with ∀ is a function. Giving it a particular strategy produces the statement for that strategy, and have records the result under a new name:

  have gap := strict opponent

The same goes for an implication: a hypothesis h : P → Q applied to a proof of P, written h p, is a proof of Q.

A near match¶

When the goal is the conclusion of a known lemma, apply uses the lemma and leaves its assumptions as the new goal. Here the goal is a weak inequality and the hypothesis a strict one, and le_of_lt : a < b → a ≤ b bridges the gap:

  have gap := strict opponent
  apply le_of_lt
  exact gap

After apply le_of_lt the goal is the strict inequality, which gap matches. The last two lines can be combined as exact le_of_lt gap, which is how the tutorial's capstone writes it.

A statement of existence¶

A hypothesis of the form ∃ x, P x gives a witness only after obtain takes it apart. It names the witness and the fact about it, which can then be used as above:

  obtain ⟨opponent, gap⟩ := weak.2
  exact ⟨opponent, ne_of_lt gap⟩

The angle brackets on the last line work the other way: they build a proof of an ∃ goal from a witness and a proof about it.

Arithmetic¶

A hypothesis about numbers can be simplified in place with at, as in norm_num [payoff] at tempted, and a goal that follows from several numerical hypotheses is usually a job for linarith. See Prove an inequality.