Add declaration to environment

Stream: new members

[Nicolò Cavalleri]

While working with what to me looks a fairly reasonable definition, I ran into a"failed to add declaration to environment" error. Where did I go wrong?

import geometry.manifold.times_cont_mdiff
import topology.continuous_map

/-!
# Smooth bundled map

In this file we define the type `smooth_map` of smooth bundled maps.

-/

variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
{E : Type*} [normed_group E] [normed_space 𝕜 E]
{E' : Type*} [normed_group E'] [normed_space 𝕜 E']
{H : Type*} [topological_space H]
{H' : Type*} [topological_space H']
{I : model_with_corners 𝕜 E H} {I' : model_with_corners 𝕜 E' H'}
{M : Type*} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M]
{M' : Type*} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M']
{E'' : Type*} [normed_group E''] [normed_space 𝕜 E'']
{H'' : Type*} [topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type*} [topological_space M''] [charted_space H'' M''] [smooth_manifold_with_corners I'' M'']

variables (I) (I') (M) (M')

@[protect_proj]
structure smooth_map :=
(to_fun             : M → M')
(smooth_to_fun      : smooth I I' to_fun)

notation `C∞(` I `, ` M `; ` I' `, ` M' `)` := smooth_map I I' M M'

namespace smooth_map

variables {I} {I'} {M} {M'}

instance : has_coe_to_fun C∞(I, M; I', M') := ⟨_, smooth_map.to_fun⟩
instance : has_coe C∞(I, M; I', M') C(M, M') :=
⟨λ f, ⟨f.to_fun, f.smooth_to_fun.continuous⟩⟩

variables {f g : C∞(I, M; I', M')}

lemma coe_inj ⦃f g : C∞(I, M; I', M')⦄ (h : (f : M → M') = g) : f = g :=
by cases f; cases g; cases h; refl

/-
kernel failed to type check declaration 'ext' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  ∀ {𝕜 : Type u_1} [_inst_1 : nondiscrete_normed_field 𝕜] {E : Type u_2} [_inst_2 : normed_group E]
  [_inst_3 : normed_space 𝕜 E] {E' : Type u_3} [_inst_4 : normed_group E'] [_inst_5 : normed_space 𝕜 E']
  [_inst_6 : topological_space H] {H' : Type u_5} [_inst_7 : topological_space H'] {I : model_with_corners 𝕜 E H}
  {I' : model_with_corners 𝕜 E' H'} {M : Type u_6} [_inst_8 : topological_space M] [_inst_9 : charted_space H M]
  [_inst_10 : smooth_manifold_with_corners I M] {M' : Type u_7} [_inst_11 : topological_space M']
  [_inst_12 : charted_space H' M'] [_inst_13 : smooth_manifold_with_corners I' M'] {f g : C∞(I, M; I', M')}
  {H_1 : Type u_4}, (∀ (x : M), ⇑f x = ⇑g x) → f = g
elaborated value:
  λ {𝕜 : Type u_1} [_inst_1 : nondiscrete_normed_field 𝕜] {E : Type u_2} [_inst_2 : normed_group E]
  [_inst_3 : normed_space 𝕜 E] {E' : Type u_3} [_inst_4 : normed_group E'] [_inst_5 : normed_space 𝕜 E']
  [_inst_6 : topological_space H] {H' : Type u_5} [_inst_7 : topological_space H'] {I : model_with_corners 𝕜 E H}
  {I' : model_with_corners 𝕜 E' H'} {M : Type u_6} [_inst_8 : topological_space M] [_inst_9 : charted_space H M]
  [_inst_10 : smooth_manifold_with_corners I M] {M' : Type u_7} [_inst_11 : topological_space M']
  [_inst_12 : charted_space H' M'] [_inst_13 : smooth_manifold_with_corners I' M'] {f g : C∞(I, M; I', M')}
  {H_1 : Type u_4} (H_1 : ∀ (x : M), ⇑f x = ⇑g x), sorry
nested exception message:
failed to add declaration to environment, it contains local constants
-/

@[ext] theorem ext (H : ∀ x, f x = g x) : f = g := sorry

[Sebastien Gouezel]

You have a space H and an assumption H, and Lean is confused. Use another letter for your assumption, and things should hopefully be better.

[Nicolò Cavalleri]

Ops haha I did not notice that, I copied the file from topology, changed smooth with continuous and did not even look at the name of the hypothesis

[Sebastien Gouezel]

The error message is not extremely helpful, indeed :-)

[Kevin Buzzard]

Yes it's impressively bad on this occasion, something perhaps to remember. Actually I'm not sure I ever remember seeing this message and it being caused by a buggy tactic or a bug in the built-in elaborator