Applying only one side of a conjuction

Stream: new members

[Duncan Skahan]

Is there a way to apply just one side of a conclusion of the form A ∧ B. (I.e. is there a working version of the below proof script?)

theorem g (P Q R A B : Prop) (p : P) (q: Q) (r: R) : A := by
  have h (_ : P) (_ : Q) (_ : R) : A ∧ B := by sorry
  apply left h

[Riccardo Brasca]

h.1?

[Riccardo Brasca]

No sorry, I didn't read carefully.

[Markus Himmel]

Perhaps

theorem g (P Q R A B : Prop) (p : P) (q: Q) (r: R) : A := by
  have h (_ : P) (_ : Q) (_ : R) : A ∧ B := by sorry
  apply (h p q r).left

is what you're looking for?

[Riccardo Brasca]

Also refine (h ?_ ?_ ?_).1 does what you want

[Duncan Skahan]

I was hoping for something that would create goals for P Q R.

[Riccardo Brasca]

refine does it. It allows you to precisely control what you want to prove later.

[Duncan Skahan]

How does ?_ differ from _?

[Riccardo Brasca]

_ means "Lean, please fill it for me", ?_ means "I will fill it later".

[Kevin Buzzard]

i.e. ?_ means "create a goal", which is what you want.