more with simp and defeq

Stream: lean4

[Matthew Ballard]

I am deeply confused. I have the following

example [UniformSpace α] [UniformSpace β] :
    (instTopologicalSpaceProd : TopologicalSpace (α × β)) = UniformSpace.toTopologicalSpace := by
 with_reducible_and_instances rfl — works

but I get the following error when tracing simp

[Meta.Tactic.simp.discharge] @ContinuousLinearMap.strongUniformity_topology_eq, failed to assign instance
      TopologicalSpace (M₁ × M₃)
    sythesized value
      instTopologicalSpaceProd
    is not definitionally equal to
      UniformSpace.toTopologicalSpace

What am I missing here?

[Matthew Ballard]

The error comes from docs#Lean.Meta.Simp.synthesizeArgs.synthesizeInstance in the block

if (← withReducibleAndInstances <| isDefEq x val) then
        return true
      else
        trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to assign instance{indentExpr type}\nsythesized value{indentExpr val}\nis not definitionally equal to{indentExpr x}"
        return false

[Adam Topaz]

Your --works line doesn't work for me.

[Adam Topaz]

Is the error suppressed somehow in your actual code?

[Adam Topaz]

Of course

import Mathlib

example [UniformSpace α] [UniformSpace β] :
    (instTopologicalSpaceProd : TopologicalSpace (α × β)) = UniformSpace.toTopologicalSpace := by
  rfl

works

[Matthew Ballard]

Sorry I should have prefaced that I am working in branch#mrb/reducible_uniform_space_comap

[Matthew Ballard]

The only change is that docs#UniformSpace.comap is reducible there

[Matthew Ballard]

Actually branch#mrb/operator_norm might be better if you want try to replicate the error also.

[Adam Topaz]

I can't reproduce the error in your branch with

set_option trace.Meta.Tactic.simp.discharge true in
example [UniformSpace α] [UniformSpace β] :
    (instTopologicalSpaceProd : TopologicalSpace (α × β)) = UniformSpace.toTopologicalSpace := by
  with_reducible_and_instances rfl

[Adam Topaz]

Oh the error is in a different file!

[Matthew Ballard]

Yes, sorry. To reproduce the error, checkout branch#mrb/operator_norm and in docs#ContinuousLinearMap.prodMapL remove the (_) from the last simp call in the proof

[Adam Topaz]

I'm going straight to strongUniformity_topology_eq

[Matthew Ballard]

It looks like unification is taking using a different instance in simp than just before.

[Matthew Ballard]

Should this be expected? Better version of the question below

[Matthew Ballard]

example :
    (instTopologicalSpaceProd : TopologicalSpace (M₁ × M₃)) = PseudoMetricSpace.toUniformSpace.toTopologicalSpace := by
  with_reducible_and_instances  — fails

This is where it ends up in the simp call

[Matthew Ballard]

Do previous simp steps affect the priority of instances? Is it going to some cache that it didn’t have before?