gt_iff_lt proves a weird goal

Stream: mathlib4

[Jireh Loreaux]

Found this with exact?%. I'm so confused. The kernel accepts the proof.

import Mathlib

open unitInterval

lemma coe_pos {x : I} : (0 : ℝ) < x ↔ 0 < x := gt_iff_lt

[Yaël Dillies]

gt_iff_lt is just Iff.rfl specialised to a < b. (0 : ℝ) < x ↔ 0 < x is defeq to (0 : ℝ) < x ↔ (0 : ℝ) < x. So it works.

[Jireh Loreaux]

lol I tried rfl instead of Iff.rfl without thinking before I did exact?%. Thanks. I'm just being stupid.