tests/lean/1682.lean - third_party/github.com/leanprover/lean4 - Git at Google


            
            example : (p → q) ∧ r := by

            
              refine ⟨?a, ?b⟩


            example : (p → q) ∧ r := by

            
              refine ⟨fun h => ?a, ?b⟩
	example : (p → q) ∧ r := by
	refine ⟨?a, ?b⟩

	example : (p → q) ∧ r := by
	refine ⟨fun h => ?a, ?b⟩