No "FunLike (ℕ → ℕ) ℕ ℕ" ?

Stream: mathlib4

[Michael Stoll]

When trying to prove a goal of the kind as in the last examples below (but more involved), I got en error message telling me that FunLike (ℕ → ℕ) ℕ ℕ cannot be synthesized. This looks strange to me: what can be more like a function than a function itself?

import Mathlib

/--
error: failed to synthesize instance of type class
  FunLike (α → β) α β

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-/
#guard_msgs in
example (α β : Type*) : FunLike (α → β) α β := inferInstance

example (α β : Type*) : FunLike (α → β) α β :=
  { coe := fun ⦃a₁⦄ => a₁,
    coe_injective' := Function.Involutive.injective (congrFun rfl)}

/--
error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  ?f (⨅ i, ?g i)
in the target expression
  1 + ⨅ i, f i = ⨅ i, 1 + i

f : Fin 3 → ℕ
⊢ 1 + ⨅ i, f i = ⨅ i, 1 + i
-/
#guard_msgs in
example (f : Fin 3 → ℕ) : 1 + ⨅ i, f i = ⨅ i, 1 + i := by
  rw [map_iInf]

/--
error: failed to synthesize instance of type class
  FunLike (ℕ → ℕ) ℕ ℕ

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
---
error: unsolved goals
f : Fin 3 → ℕ
⊢ 1 + ⨅ i, f i = ⨅ i, 1 + i
-/
#guard_msgs in
example (f : Fin 3 → ℕ) : 1 + ⨅ i, f i = ⨅ i, 1 + i := by
  rw [map_iInf (β := ℕ) (fun n : ℕ ↦ 1 + n) f]

(There is then the additional complication that the lemma I'm trying to rewrite with wants an docs#sInfHomClass, which essentially seems to be only available for docs#OrderIso s.
<rant>Why is it so hard to work with indexed suprema/infima with finite index type and target type, say, the naturals, integers, or reals?</rant>)

Is this a bug?

[Yury G. Kudryashov]

We use FunLike for bundled morphisms that use DFunLike.coe to be interpreted as a function.

[Yury G. Kudryashov]

If you want to work with finite suprema/infima, you may have better luck with Finset.sup etc.

[Michael Stoll]

The problem with docs#Finset.sup is that it needs a bottom element, and docs#Finset.sup' necessitates carrying around nonemptiness conditions. Also, in my context, it is very natural to consider "tuples" x : ι → K, and switching from iSup x to Finset.sup' .univ (nonemptyness proof) x is a bit clumsy...

[Bhavik Mehta]

Even if we had that FunLike, ℕ → ℕ wouldn't be an sInfHomClass, so I'm not sure it would help in your case. I also don't think finiteness is at fault here - if your f was indexed by the naturals, you'd be in basically the same situation!

[Michael Stoll]

Yes; I've realized that docs#map_iInf is not the way to go, even though you'd expect it to do what I want from its name.

[Bhavik Mehta]

import Mathlib

lemma ciInf_add' {ι α : Type*} [Nonempty ι] [ConditionallyCompleteLattice α]
    [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftMono α] {a : α} {f : ι → α}
    (hf : BddBelow (Set.range f)) :
    (⨅ i, f i) + a = ⨅ i, f i + a := by
  apply le_antisymm
  · simp [add_le_add_left, le_ciInf, ciInf_le hf]
  · rw [← tsub_le_iff_right]
    refine le_ciInf fun x ↦ ?_
    rw [tsub_le_iff_right]
    apply ciInf_le
    obtain ⟨K, hK⟩ := hf
    exact ⟨K + a, by simp_all [lowerBounds, add_le_add_left]⟩

lemma ciInf_add'' {ι α : Type*} [Nonempty ι] [ConditionallyCompleteLattice α] [OrderBot α]
    [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftMono α] {a : α} {f : ι → α} :
    (⨅ i, f i) + a = ⨅ i, f i + a :=
  ciInf_add' (by simp)

lemma add_ciInf' {ι α : Type*} [Nonempty ι] [ConditionallyCompleteLattice α]
    [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftMono α] {a : α} {f : ι → α}
    (hf : BddBelow (Set.range f)) :
    a + ⨅ i, f i = ⨅ i, a + f i := by
  simp_rw [add_comm a, ciInf_add' hf]

lemma add_ciInf'' {ι α : Type*} [Nonempty ι] [ConditionallyCompleteLattice α] [OrderBot α]
    [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftMono α] {a : α} {f : ι → α} :
    a + ⨅ i, f i = ⨅ i, a + f i := by
  simp_rw [add_comm a, ciInf_add'']

example (f : Fin 3 → ℕ) : 1 + ⨅ i, f i = ⨅ i, 1 + f i := by
  rw [add_ciInf'']

example (f : Fin 3 → ℤ) : 1 + ⨅ i, f i = ⨅ i, 1 + f i := by
  rw [add_ciInf]
  exact Finite.bddBelow_range _

We already have the lemma to do this in ints (and AddGroup in general) but it looks like we were missing it for nat-like things

[Eric Wieser]

I think you can avoid OrderedSub there?

[Eric Wieser]

I remember having a discussion about how you can construct a temporary - operator from the + operator alone and suitable order conditions / choice

[Michael Stoll]

This is going off on a tangent now (I over-simplified my actual use case, which looks more like

(↑(Ideal.absNorm v.maximalIdeal.asIdeal ^ ⨅ i, multiplicity v.maximalIdeal.asIdeal (Ideal.span {x ↑i})))⁻¹ = ...

which I would like to transform into

⨆ i, (↑(Ideal.absNorm v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal (Ideal.span {x ↑i})))⁻¹ = ...

By now, I have written some API that allows me to do this relatively painlessly (see #Is there code for X? > Monotone function maps iSup to iSup ), so please feel free to hijack this tread :smile: