aesop and an inequality

Stream: mathlib4

[Kevin Buzzard]

My mental model of Aesop wasn't expecting this:

import Mathlib.Tactic

example (X : Type*) (t : TopologicalSpace X) : t ≤ t := by aesop -- works

example (X : Type*) (t : TopologicalSpace X) :
    t ≤ t.coinduced (fun x ↦ x) := by
  -- aesop -- fails
  apply le_of_eq
  aesop -- now works

I'm doing some work now which I think aesop should be some help in, and I'm trying to learn how to use it better. By the way, solve_by_elim solves the goal directly.

[Yury G. Kudryashov]

Is le_of_eq an aesop rule?

[Anand Rao Tadipatri]

Adding the rfl tactic to aesop's set of rules makes this example work, although it is not necessarily the most robust approach:

import Mathlib.Tactic

add_aesop_rules safe [(by rfl)] -- this allows `aesop` to prove goals by reflexivity

example (X : Type*) (t : TopologicalSpace X) : t ≤ t := by aesop -- works

example (X : Type*) (t : TopologicalSpace X) :
    t ≤ t.coinduced (fun x ↦ x) := by
  aesop -- now works

[Jannis Limperg]

There's actually no reason why by rfl shouldn't be in the default Aesop rule set, so I've put it in.

[Jireh Loreaux]

@Jannis Limperg I disagree, that can be quite expensive, no? How about by with_reducible rfl?

[Jannis Limperg]

Maybe, although it shouldn't be much more expensive than the variant that's currently in. I'm down for the with_reducible variant if nobody objects. This may break some existing proofs because it's weaker than the current variant in some situations.