Why can't it be automatically inferred

Stream: lean4

[Zichen Wang]

image.png
I've proved the instance what it need, but this definition in pic can't be automatically inferred

[Edward van de Meent]

Instance search can't find the implicit argument x. Using [X.Nonempty] may fix it?

[Edward van de Meent]

Next time, please send a #mwe instead of a screenshot

[Zichen Wang]

Sorry.

section

variable {X : Set α}{x : α} (h : x ∈ X) --[hm : ProperFunction X (Convex.indicator X)]

noncomputable instance ConvexIndicator_is_proper:
    ProperFunction X (Convex.indicator X) where
  uninfinity := by
    intro a _
    dsimp[Convex.indicator]
    simp
    by_cases h1 : a ∈ X
    · rw[if_pos h1];exact EReal.bot_lt_zero
    rw[if_neg h1];exact bot_lt_top
  existence_of_finite_value:= by
    right;
    use x,h
    dsimp[Convex.indicator]
    rw[if_pos h];
    exact EReal.zero_lt_top
-- #check hm

#check (ConvexIndicator_is_proper h)


#check subdifferential X (Convex.indicator X) x

end

But using [X.Nonempty] can't fix it.

And where is the  the implicit argument x

[Edward van de Meent]

it seems this is missing imports?

[Zichen Wang]

Edward van de Meent 发言道：

it seems this is missing imports?

yes, it depends on a lot of our own defs. So I send a screenshot.

[Edward van de Meent]

would you agree that the following is a representation of what you're trying to do?

import Mathlib
set_option autoImplicit false
class Foo (X:Type*)

variable {α : Type*} {X : Set α} {x:α} {h:x ∈ X}

instance bar {x:α} {_:x ∈ X}: Foo X where

-- #check hm

#synth Foo X

[Edward van de Meent]

because if so, adding [Nonempty X] instead of x and h should fix it.

[Zichen Wang]

Thx. We have solved. But I wonder why I can't write like before.Where is problem?

[Yury G. Kudryashov]

How should it find x and h? Instance search can use only instance search for dependencies