Trying to understand "use" here

Stream: new members

[Kevin Cheung]

Why does use manage to solve the goal in the following?

example {p q : Prop} : p ∧ q → q ∧ p := by
  rintro ⟨hp, hq⟩
  use hq

[Damiano Testa]

use tries to close the resulting goals with the following tactics

macro_rules | `(tactic| use_discharger) => `(tactic| apply exists_prop.mpr <;> use_discharger)
macro_rules | `(tactic| use_discharger) => `(tactic| apply And.intro <;> use_discharger)
macro_rules | `(tactic| use_discharger) => `(tactic| rfl)
macro_rules | `(tactic| use_discharger) => `(tactic| assumption)
macro_rules | `(tactic| use_discharger) => `(tactic| apply True.intro)

(and maybe more.)

The relevant one is that it tries assumption.

[Damiano Testa]

See https://github.com/leanprover-community/mathlib4/blob/8b2dfa4e358ef9969cc5f519810315b205710e24/Mathlib/Tactic/Use.lean#L135-L137 for the actual code that takes care of the use_discharger.

[Kevin Cheung]

Thanks!

[Damiano Testa]

Btw, for the same reason, this is also a proof:

example {p q : Prop} : p ∧ q → q ∧ p := by
  rintro ⟨hp, hq⟩
  use

I doubt that this style is encouraged, though.

[Kevin Cheung]

That somehow didn't work for me. It complained about unexpected end of input.

[Damiano Testa]

Oops, you are right! I had missed that the error was referring to the use tactic! :man_facepalming: