# Context

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


# Problem

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
term
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

section
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},
}⟩

section
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)))
H))

#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
end

end


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

• 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. Commented Feb 26, 2023 at 13:25
• @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. Commented Feb 26, 2023 at 13:52
• 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. Commented Feb 26, 2023 at 16:12

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