Error : cannot find synthesization order for instance

Stream: new members

[LizBonn]

I am trying to prove that "If a finite group $G$ has a normal Sylow-p subgroup $P$, then for a subgroup $H$ of $G$, $P \cap H$ is the only Sylow-p subgroup of $H$". When I use an instance to show that $P$ is a normal subgroup, something goes wrong. However, if I just write this as a hypothesis, everything seems OK. What on earth happens here?

Thanks in advance.

Minimal work examples:

import Mathlib
-- When using an instance, something goes wrong.
variable {G : Type} [Group G] [Fintype G] {p : ℕ} [Fact p.Prime] (P : Sylow p G) [Subgroup.Normal P.toSubgroup] (H : Subgroup G)

def Pₕ : Sylow p H :=
  let P' := (P.toSubgroup).subgroupOf H
{
  P' with

  isPGroup' := sorry
  is_maximal' := sorry
}

noncomputable instance : Unique (Sylow p H) := Sylow.unique_of_normal (Pₕ P H) {
  conj_mem := fun n memₙ g =>
  Subgroup.mem_subgroupOf.mpr (Subgroup.Normal.conj_mem inferInstance n.val (Subgroup.mem_subgroupOf.mp memₙ) g.val)
}

import Mathlib
-- If I use a hypothesis, the error disappears.
variable {G : Type} [Group G] [Fintype G] {p : ℕ} [Fact p.Prime] (P : Sylow p G) (_ : Subgroup.Normal P.toSubgroup) (H : Subgroup G)

def Pₕ : Sylow p H :=
  let P' := (P.toSubgroup).subgroupOf H
{
  P' with

  isPGroup' := sorry
  is_maximal' := sorry
}

noncomputable instance : Unique (Sylow p H) := Sylow.unique_of_normal (Pₕ P H) {
  conj_mem := fun n memₙ g =>
  Subgroup.mem_subgroupOf.mpr (Subgroup.Normal.conj_mem inferInstance n.val (Subgroup.mem_subgroupOf.mp memₙ) g.val)
}

Error:

cannot find synthesization order for instance @instUniqueSylowSubtypeMemSubgroup with type
  {G : Type} →
    [inst : Group G] →
      [inst_1 : Fintype G] →
        {p : ℕ} →
          [inst_2 : Fact (Nat.Prime p)] →
            (P : Sylow p G) → [inst_3 : (↑P).Normal] → (H : Subgroup G) → Unique (Sylow p ↥H)
all remaining arguments have metavariables:
  @Subgroup.Normal G inst✝³ ↑?P

[Kevin Buzzard]

instance means "You are handing this theorem over to the typeclass inference system" (the square bracket system) so it must be in a form that the typeclass inference system can use. It looks like Lean thinks your instance is not in this form, and my guess is that the problem is that if typeclass inference is summoned to prove Unique (Sylow p H) then there is no way that it can reasonably guess what P is without risking the possibility that it goes off on a wild goose chase.