`aesop?` with a custom `TacGen` suggests a proof that does not work

[dwrensha]

I expect aesop? to only suggest things that actually close the proof. However, here is an example where it returns something that fails:

import Mathlib.Data.Real.Basic
import Mathlib.Algebra.Order.Positive.Field

abbrev PosReal : Type := { x : ℝ // 0 < x }

notation "ℝ+" => PosReal

abbrev solution_set : Set (ℝ+ → ℝ+) := { fun x ↦ x + 1 }

def myTacGen : Aesop.TacGen := fun _ => do
  return #[("exact ⟨val - f { val := val, property := property }, fun a ha => by simpa⟩",
            0.9)]

macro "foo" : tactic => `(tactic| aesop? (add 90% myTacGen))

theorem usa2023_p2b (f : ℝ+ → ℝ+)
    (P : ∀ x y, f (x * y + (f x)) = x * (f y) + ⟨2, two_pos⟩) :
    f ∈ solution_set := by
  suffices h : ∃ a b : ℝ, 0 < a ∧ ∀ x, (f x).val = a * x.val + b by sorry
  let c := f 1
  foo
  /-
   Returns the following, which does not actually work:

Try this: simp_all only [Subtype.forall, exists_and_left] unhygienic with_reducible aesop_destruct_products apply Exists.intro apply And.intro on_goal 2 => exact ⟨val - f { val := val, property := property }, fun a ha => by simpa⟩ exact property

  -/

This is with mathlib commit 8d0c6e6f821392660468fdce7c5463740d7988be and aesop commit 5fefb40a7c9038a7150e7edd92e43b1b94c49e79

[JLimperg]

Minimised:

import Aesop

@[aesop 90%]
def myTacGen : Aesop.TacGen := fun _ => do
  return #[("exact ⟨val - f { val := val, property := property }, fun a ha => by simpa⟩",
            0.9)]

theorem foo2 (f : { x // 0 < x } → { x // 0 < x })
    (val : Nat)
    (property : 0 < val) :
    ∃ w x, ∀ (a : Nat) (b : 0 < a), ↑(f { val := a, property := b }) = w * a + x := by
  constructor
  aesop?
  -- Try this:
  -- exact ⟨val - f { val := val, property := property }, fun a ha => by simpa⟩