Bare `⊢ ℝ` unsolved goal when constructing IsPicardLindelof via of_time_independent with NNReal params

Description

Constructing IsPicardLindelof via IsPicardLindelof.of_time_independent with NNReal parameters produces a spurious bare ⊢ ℝ "unsolved goals" error. The metavariable never appears in the context list — it is created and consumed during elaboration of the have hf : IsPicardLindelof ... line, leaving a bare type as the residual goal.

The error is independent of:

• Vector field content (trivial fun _ _ => (0 : ℝ×ℝ) vs real)
• NNReal values (literal (1 : ℝ≥0) vs computed bounds)
• Binding form (set vs let)
• Proof mode (term-mode annotation vs apply + bullets)
• Named pins (all pinned vs none vs some)
• Type annotation (explicit full type vs inferred)
• Icc construction form (term-mode ⟨by norm_num, h⟩, tactic-mode refine, by exact ⟨...⟩, inline)
• Structure construction method (direct 4-field ⟨...⟩ vs of_time_independent)
• Downstream consumer usage (replacing the consumer with admit does NOT clear the error)
• Named pins on the TYPE annotation ((tmin := 0) (tmax := T') in the have hf : IsPicardLindelof ... line)

The error persists across all of the above variations — ~20 builds tested.

Toolchain

• Lean: leanprover/lean4:v4.33.1
• Mathlib: rev 0df444a360ea (via git URL https://github.com/leanprover-community/mathlib4.git)

Minimal repro

import Mathlib.Analysis.ODE.Basic
import Mathlib.Analysis.ODE.ExistUnique
import Mathlib.Analysis.Calculus.Deriv.Basic
import Mathlib.Data.NNReal.Defs

open Set Filter
open scoped NNReal Topology

noncomputable def V (K ω₀ ω_c : ℝ) : ℝ × ℝ → ℝ × ℝ := fun p =>
  (p.2, ω_c * (ω₀ - K * Real.sin p.1 - p.2))

theorem repro_local_solution (K ω₀ ω_c θ₀ ω_init T : ℝ) (hT : 0 < T) :
    ∃ T' : ℝ, 0 < T' ∧ T' ≤ T ∧
      ∃ α : ℝ → ℝ × ℝ, α 0 = (θ₀, ω_init) ∧
        ∀ t ∈ Icc 0 T', HasDerivWithinAt α (V K ω₀ ω_c (α t)) (Icc 0 T') t := by
  set x₀ : ℝ × ℝ := (θ₀, ω_init)
  set a_nn : ℝ≥0 := ⟨2 * max 1 (max |θ₀| |ω_init|), by positivity⟩
  have hL_nonneg : 0 ≤ (2 : ℝ) * ↑a_nn + |ω_c| * (|ω₀| + |K| * 2 * ↑a_nn + 2 * ↑a_nn) := by positivity
  let L_nn : ℝ≥0 := ⟨(2 : ℝ) * ↑a_nn + |ω_c| * (|ω₀| + |K| * 2 * ↑a_nn + 2 * ↑a_nn), hL_nonneg⟩
  set T' : ℝ := min T (↑a_nn / ((L_nn : ℝ) + 1))
  have hTp_pos : 0 < T' := by rw [show T' = min T (↑a_nn / ((L_nn : ℝ) + 1)) from rfl]; apply lt_min; exact hT; positivity
  have hTp_le_T : T' ≤ T := by rw [show T' = min T (↑a_nn / ((L_nn : ℝ) + 1)) from rfl]; exact min_le_left _ _
  have ht₀ : Icc (0 : ℝ) T' := ⟨by norm_num, hTp_le_T⟩
  -- THE CRITICAL LINE — spawns bare `⊢ ℝ`:
  have hf : IsPicardLindelof (fun _ ↦ V K ω₀ ω_c) ht₀ x₀ a_nn 0 L_nn (1 : ℝ≥0) := by
    apply IsPicardLindelof.of_time_independent
    · intro p hp; norm_num [V]
    · exact LipschitzWith.lipschitzOnWith (by
        refine' LipschitzWith.mul_const _ (LipschitzWith.add _ (LipschitzWith.sub _ _))
        <;> simp_all [V] <;> norm_num)
    · nlinarith [min_le_left T _, hTp_pos.le]
  obtain ⟨α, hα₀, hderiv⟩ :=
    IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt₀ (tmin := (0 : ℝ)) (tmax := T') hf
  refine ⟨T', hTp_pos, hTp_le_T, α, hα₀, ?_⟩
  intro t ht
  have ht' : t ∈ Icc 0 T := by constructor <;> linarith [ht.1, ht.2, hTp_le_T]
  exact hderiv t ht'

Error output

error: src/repro.lean:29:32: unsolved goals
K ω₀ ω_c θ₀ ω_init T : ℝ
hT : 0 < T
x₀ : ℝ × ℝ := (θ₀, ω_init)
a_nn : ℝ≥0 := ⟨2 * max 1 (max |θ₀| |ω_init|), ⋯⟩
L_nn : ℝ≥0 := ⟨2 * ↑a_nn + |ω_c| * (|ω₀| + |K| * 2 * ↑a_nn + 2 * ↑a_nn), ⋯⟩
T' : ℝ := min T (↑a_nn / (↑L_nn + 1))
hTp_pos : 0 < T'
hTp_le_T : T' ≤ T
⊢ ℝ

Note: the goal is a BARE TYPE (ℝ) with NO metavariables visible in any hypothesis. The ?m : ℝ is created DURING elaboration of the have hf line and never appears in the context.

Impact

This blocks formalization of local existence results for autonomous ODEs using the Picard-Lindelöf theorem with NNReal parameters. All bounds (Lipschitz constant, norm bound, time interval constraint) can be proven — only the final packaging into IsPicardLindelof fails.

Workaround attempted

Marked the affected theorem with sorry + docstring. No proof-level workaround found after exhausting all construction variations listed above.

Start by compiling the supplied minimal repro with Lean 4.33.1 and the listed mathlib revision, focusing on IsPicardLindelof.of_time_independent and the have hf line. Trace where the hidden ℝ metavariable is introduced during elaboration; done means the repro builds without the bare ⊢ ℝ goal.