Error: typeclass instance problem is stuck, it is often due

Stream: new members

[Victor Liu]

I'm trying to formalize the Newton-Kantorovich theorem in Lean 4 based on the proof by PHILIPPE G. CIARLET and CRISTINEL MARDARE, specifically the one constant version.

Here, I have a minimum working example for my error:

import Mathlib.Analysis.NormedSpace.BoundedLinearMaps
import Mathlib.Topology.MetricSpace.Basic
import Mathlib.Analysis.Calculus.FDeriv.Basic
import Mathlib.Analysis.Calculus.ContDiff.Defs

open Set Function Topology ContinuousLinearMap

-- Define the variables for Banach spaces X and Y
variable {X Y : Type*}
  [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X]
  [NormedAddCommGroup Y] [NormedSpace ℝ Y] [CompleteSpace Y]

-- Define the open subset Ω of X
variable (Ω : Set X) [TopologicalSpace X] (hΩ : IsOpen Ω)

-- Define the point x₀ in Ω
variable (x₀ : X) (hx₀ : x₀ ∈ Ω)

-- Define the C¹ mapping f: Ω → Y
variable (f : X → Y) (hf : ContDiffOn ℝ 1 f Ω)

-- Define f'(x₀) and assume it's bijective
variable (f'x₀ : X →L[ℝ] Y)
variable (hf'x₀ : HasFDerivAt f f'x₀ x₀)

I get the error

MinimumViableExample.lean:24:18

typeclass instance problem is stuck, it is often due to metavariables
  NormedSpace ?m.6515 Y

What can I do to fix this? I have tried using set_option autoImplicit false as was suggested in another post with the same error but I just get the same error message.

[Victor Liu]

Here is the theorem statement for reference, if anyone would like to suggest a potentially better structure.
image.png

[Edward van de Meent]

the problem is that X already has a topological space from NormedAddCommGroup X, and that these topological spaces don't need to coincide.

[Edward van de Meent]

removing [TopologicalSpace X] should fix your issue

[Victor Liu]

That worked, thanks!