## Stream: new members

### Topic: Add declaration to environment

#### NicolΓ² Cavalleri (Jul 30 2020 at 15:35):

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') :=

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 (Jul 30 2020 at 15:54):

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 (Jul 30 2020 at 16:19):

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 (Jul 30 2020 at 17:35):

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

#### Kevin Buzzard (Jul 30 2020 at 17:38):

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

Last updated: Dec 20 2023 at 11:08 UTC