fun_prop fails Nat.cast ∘ Set.ncard : Set ℕ → ℕ measurable

Stream: mathlib4

[Yaël Dillies]

This is very confusing. The identity Nat.cast : ℕ → ℕ is certainly measurable, and fun_prop knows that thanks to docs#measurable_from_nat, but it fails to realise that when composing with a function to ℕ:

import Mathlib.MeasureTheory.MeasurableSpace.NCard

variable {R : Type*} [NatCast R] {mR : MeasurableSpace R}

example : Measurable (Nat.cast : ℕ → R) := by fun_prop -- works
example : Measurable (Nat.cast : ℕ → ℕ) := by fun_prop -- works
example : Measurable (Nat.cast ∘ Set.ncard : Set ℕ → R) := by fun_prop -- works
example : Measurable (Nat.cast ∘ Set.ncard : Set ℕ → ℕ) := by fun_prop -- fails

[Jireh Loreaux]

What does the trace say?

[Yaël Dillies]

... which one?

[Aaron Liu]

import Mathlib.MeasureTheory.MeasurableSpace.NCard

variable {R : Type*} [NatCast R] {mR : MeasurableSpace R}
set_option trace.Meta.Tactic.fun_prop true
example : Measurable (Nat.cast : ℕ → R) := by fun_prop -- works
example : Measurable (Nat.cast : ℕ → ℕ) := by fun_prop -- works
/-
[Meta.Tactic.fun_prop] [✅️] Measurable (Nat.cast ∘ Set.ncard) ▼
  [] candidate theorems for NatCast.natCast #[]
  [] failed applying `Measurable` theorems for `NatCast.natCast`
               trying again after decomposing function as: `(fun a2 => ↑a2) ∘ (fun a => a.ncard)`
  [] [✅️] applying: Measurable.comp' ▼
    [] [✅️] Measurable fun a2 => ↑a2 ▶
    [] [✅️] Measurable fun a => a.ncard ▶
-/
example : Measurable (Nat.cast ∘ Set.ncard : Set ℕ → R) := by fun_prop -- works
/-
[Meta.Tactic.fun_prop] [❌️] Measurable (Nat.cast ∘ Set.ncard) ▼
  [] candidate theorems for NatCast.natCast #[]
  [] failed applying `Measurable` theorems for `NatCast.natCast`
               now trying to prove `Measurable` from another function property
  [] candidate transition theorems: [@Measurable.of_discrete,
       @Measurable.of_discrete,
       @measurable_from_top,
       @Subsingleton.measurable,
       @measurable_of_subsingleton_codomain]
  [] [❌️] applying: Measurable.of_discrete ▶
  [] [❌️] applying: Measurable.of_discrete ▶
  [] [❌️] applying: measurable_from_top ▶
  [] [❌️] applying: Subsingleton.measurable ▶
  [] [❌️] applying: measurable_of_subsingleton_codomain ▶
-/
example : Measurable (Nat.cast ∘ Set.ncard : Set ℕ → ℕ) := by fun_prop -- fails

[Yaël Dillies]

Ah, the fun_prop one. As you see, it simply does not try any lemma for Measurable Nat.cast

[Floris van Doorn]

you mean: it doesn't try to apply Measurable.comp' anymore....