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

example (p q : Prop) : p ∧ q → p := by
  refine fun a => ?hp
  trace_state
  exact a.1

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

example (p q : Prop) : p ∧ q → p := by
  refine fun ⟨a, b⟩ => ?hp
  trace_state
  exact a

example (p q : Prop) : p ∧ q → p := by
  refine fun a => ?hp
  case hp => exact a.1

example (p q : Prop) : p ∧ q → p := by
  refine fun ⟨a, b⟩ => ?hp
  case hp => exact a

example (p q : Prop) : p ∧ q → p := by
  refine λ ⟨a, b⟩ => ?hp
  trace_state
  exact a