I have defined two structures corresponding to a group and a subgroup :

structure groupe : Type (u+1) :=
  (ens : Type u)
  (mul : ens → ens → ens)
  -- other things

structure sous_groupe (G : groupe) :=
  (sous_ensemble : set G.ens)
  -- other things

I then defined coercions from a group G to the carrier type, and from a subgroup H of G to the underlying group with the carrier type being {a : G.ens // a ∈ H.sous_ens}:

instance groupe_to_ens : has_coe_to_sort groupe (Type u) :=
  ⟨λ G : groupe, G.ens⟩

instance sous_groupe_to_groupe {G: groupe} : has_coe (sous_groupe G) groupe :=
  sorry -- definition of the subtype and the corresponding functions and axioms


Now what I tried to to is :

example (G: groupe) (H : sous_groupe G) (a : G) (b : H): G.ens := G.mul a b

What I expected for it to do is for b to be coerced by H --> x : group --> x.ens (which equals {a : G.ens // a ∈ H.sous_ens}) --> G.ens). But I got this error:

type mismatch at application
  G.mul a b
has type
  @coe_sort.{u+1 u+2} (sous_groupe G) (Type u) (@coe_sort_trans.{u+2 u+1 u+2} (sous_groupe G) groupe (Type u) groupe_to_ens (@coe_base_aux.{u+1 u+2} (sous_groupe G) groupe (@sous_groupe_to_groupe G))) H

I tried to do #reduce [the big expression for the type of b in the error] and it reduced to {a : G.ens // H.sous_ens a} so it seems to have been coerced all the way up to the subtype, but it did not do the final coercion from the subtype to the corresponding type.

I also tried to do this:

variable (a : G)
variable (b : {t // H.sous_ens t})
variable (c : [the big expression that reduces to {t // H.sous_ens t})
example : G.ens := G.mul a b -- This works correctly and b is coerced to G.ens
example : G.ens := G.mul a c -- This fails even though c is definitionally equal to b

Full block of code to reproduce the error

universe u

structure groupe : Type (u+1) :=
  (ens : Type u)
  (mul : ens → ens → ens )
  (neutre : ens)
  (inv : ens → ens )
  (mul_assoc : ∀ a b c : ens, mul (mul a b) c = mul a (mul b c))  
  (neutre_gauche : ∀ x : ens, mul neutre x = x)
  (inv_gauche : ∀ x : ens, mul (inv x) x = neutre)

instance groupe_to_ens : has_coe_to_sort groupe (Type u) :=
  ⟨λ a : groupe, a.ens⟩
instance groupe_has_inv (G: groupe) :
  has_inv (G.ens) := ⟨G.inv⟩
instance groupe_has_mul (G : groupe) :
  has_mul (G.ens) := ⟨G.mul⟩

structure sous_groupe (G: groupe) :=
  (sous_ens : set G.ens)
  (mul_stab : ∀ a b ∈ sous_ens, G.mul a b ∈ sous_ens)
  (inv_stab : ∀ a ∈ sous_ens, a⁻¹ ∈ sous_ens)
  (contient_neutre : G.neutre ∈ sous_ens )

instance sous_groupe_to_groupe {G: groupe}:
  has_coe (sous_groupe G) groupe :=
  ⟨λ SG : sous_groupe G,
  {groupe .
    ens := {a // a ∈ SG.sous_ens},
    mul :=  λ x y, ⟨x.val*y.val, SG.mul_stab x.val x.property y.val y.property⟩,
    inv := λ x, ⟨x.val⁻¹, SG.inv_stab x.val x.property⟩,
    neutre := ⟨G.neutre, SG.contient_neutre⟩,
    mul_assoc := λ x y z, by {rw subtype.mk.inj_eq, unfold subtype.val, exact G.mul_assoc x y z},
    neutre_gauche := λ x, by {cases x, rw subtype.mk.inj_eq, unfold subtype.val, exact G.neutre_gauche _},
    inv_gauche := λ x, by {rw subtype.mk.inj_eq, unfold subtype.val, exact G.inv_gauche x.val},

variable (G: groupe)
variable (H: sous_groupe G)
variable (a : G)
variable (a' : H)
variable (b : {c // H.sous_ens c})
variable (b' : (@coe_sort.{u+1 u+2} (sous_groupe G) (Type u)
    (@coe_sort_trans.{u+2 u+1 u+2} (sous_groupe G) groupe (Type u) groupe_to_ens
      (@coe_base_aux.{u+1 u+2} (sous_groupe G) groupe (@sous_groupe_to_groupe G)))

#reduce (@coe_sort.{u+1 u+2} (sous_groupe G) (Type u)
    (@coe_sort_trans.{u+2 u+1 u+2} (sous_groupe G) groupe (Type u) groupe_to_ens
      (@coe_base_aux.{u+1 u+2} (sous_groupe G) groupe (@sous_groupe_to_groupe G)))
    H) -- infered type, reduces to {a // H.sous_ens a}

set_option pp.all true
#reduce G.mul a a' -- does not work, the infered type for a' is the type of b'
#reduce G.mul a b -- works
#reduce G.mul a b' -- does not work 


Is there anything in the coercion mechanisms that would explain this behaviour ?

  • $\begingroup$ This question would be a bit easier to answer if you posted one block of fully working code. Is it Lean 3 or Lean 4? Examples of problems I've fixed so far: carrier in mul -> ens, sous_groupe {G : groupe} -> sous_groupe (G : groupe), but I still can't reproduce your error. You're asking about a specific error and the best way to do this is to just produce one fully compiling block of code which will let me reproduce the error on my own machine. $\endgroup$ Feb 26 at 13:25
  • $\begingroup$ @KevinBuzzard sorry about that, I have corrected the mistakes you pointed to, and added a link to the file with the full block of code, and it is in Lean 3. $\endgroup$
    – Blumer
    Feb 26 at 13:52
  • 1
    $\begingroup$ Could you please insert a full block of working code. Links are unstable, and links into revision control systems even more so. Future readers will likely not be able to recover the code. Also, you did not even link to a section of code that is self sufficient, as it does not contain the definition of groups, for example. $\endgroup$ Feb 26 at 16:12

1 Answer 1


I don't think you are defining a coercion from H to G; you're defining a coercion from the type of all subgroups of a group to the type of all groups. This doesn't give you a coercion from H (coerced to a type) to G, it just lets you coerce H to a type. If you add

instance foo (G : groupe) (H : sous_groupe G) : has_coe H G := ⟨subtype.val⟩

then everything works.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.