strange proof with ge_iff_le found by exact?

Stream: lean4

[Ted Hwa]

-- returns exact ge_iff_le
example (n k: Nat)(m: Fin n)(hk: k < n): ⟨k, hk⟩ ≤ m ↔ k ≤ m := by exact?

It's strange because there are no ≥ anywhere in the statement. In fact, just using rfl works.

[Kyle Miller]

a ≥ b is an abbreviation for b ≤ a, so it's not surprising a lemma about ≥ would appear, but this does amount to an indirect way to write Iff.rfl

[Kyle Miller]

It's too bad that ge_iff_le is necessary as a lemma. The issue is that, for example, you need to do rw [ge_iff_le] first if you want to rw using a lemma that's in terms of ≤.

[Ted Hwa]

But in the lemma statement, both sides of the iff were ≤ to begin with. There was no ≥.

[Yaël Dillies]

Yes, but exact ge_iff_le does work as a proof, which is all exact? cares about

[Kyle Miller]

It care a bit more than that. The deal is that when it searches for proofs, it peeks through abbreviations. To exact?, a ≥ b looks exactly like b ≤ a.