I'm trying to proof (a ↔ a) → a in lean, but I can't figure out which lemmas/tactics to use. Proving a → (a ↔ a) is something I can do.
Can someone guide me with the steps necessary to take to solve the goal?
example (a : Prop) : (a ↔ a) → a :=
begin
intros h,
end