-- Module: Mathlib.Combinatorics.Tiling.Tile
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
ps : Protoset G X ιₚ
g : G
pt : PlacedTile ps
a b : G
r :
  a⁻¹ * b ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X)))
      ((↑ps : ιₚ → Prototile G X) pt.index).symmetries
refine :
  HEq.{u_1 + 1} (α :=
    G ⧸
      Subgroup.map
        (Subgroup.subtype
          (MulAction.stabilizer G
            (↑((↑ps : ιₚ → Prototile G X)
                  (index.{u_1, u_2, u_3} (G := G) (X := X) (ps := ps)
                    ((fun (h : G) ↦
                        ({ index := pt.index,
                            groupElts :=
                              (↑(g * h) :
                                G ⧸
                                  Subgroup.map
                                    (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X)).subtype
                                    ((↑ps : ιₚ → Prototile G X) pt.index).symmetries) } :
                          PlacedTile ps))
                      a))) :
              Set X)))
        ((↑ps : ιₚ → Prototile G X)
            (index.{u_1, u_2, u_3} (G := G) (X := X) (ps := ps)
              ((fun (h : G) ↦
                  ({ index := pt.index,
                      groupElts :=
                        (↑(g * h) :
                          G ⧸
                            Subgroup.map
                              (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X)).subtype
                              ((↑ps : ιₚ → Prototile G X) pt.index).symmetries) } :
                    PlacedTile ps))
                a))).symmetries)
    (groupElts
      ((fun (h : G) ↦
          ({ index := pt.index,
              groupElts :=
                (↑(g * h) :
                  G ⧸
                    Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X)).subtype
                      ((↑ps : ιₚ → Prototile G X) pt.index).symmetries) } :
            PlacedTile ps))
        a))
    (β :=
    G ⧸
      Subgroup.map
        (Subgroup.subtype
          (MulAction.stabilizer G
            (↑((↑ps : ιₚ → Prototile G X)
                  (index.{u_1, u_2, u_3} (G := G) (X := X) (ps := ps)
                    ((fun (h : G) ↦
                        ({ index := pt.index,
                            groupElts :=
                              (↑(g * h) :
                                G ⧸
                                  Subgroup.map
                                    (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X)).subtype
                                    ((↑ps : ιₚ → Prototile G X) pt.index).symmetries) } :
                          PlacedTile ps))
                      b))) :
              Set X)))
        ((↑ps : ιₚ → Prototile G X)
            (index.{u_1, u_2, u_3} (G := G) (X := X) (ps := ps)
              ((fun (h : G) ↦
                  ({ index := pt.index,
                      groupElts :=
                        (↑(g * h) :
                          G ⧸
                            Subgroup.map
                              (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X)).subtype
                              ((↑ps : ιₚ → Prototile G X) pt.index).symmetries) } :
                    PlacedTile ps))
                b))).symmetries)
    (groupElts
      ((fun (h : G) ↦
          ({ index := pt.index,
              groupElts :=
                (↑(g * h) :
                  G ⧸
                    Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X)).subtype
                      ((↑ps : ιₚ → Prototile G X) pt.index).symmetries) } :
            PlacedTile ps))
        b))
⊢ Eq (α := PlacedTile ps)
    ((fun (h : G) ↦
        ({ index := pt.index,
            groupElts :=
              (↑(g * h) :
                G ⧸
                  Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X)).subtype
                    ((↑ps : ιₚ → Prototile G X) pt.index).symmetries) } :
          PlacedTile ps))
      a)
    ((fun (h : G) ↦
        ({ index := pt.index,
            groupElts :=
              (↑(g * h) :
                G ⧸
                  Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X)).subtype
                    ((↑ps : ιₚ → Prototile G X) pt.index).symmetries) } :
          PlacedTile ps))
      b)

Tactic:
refine PlacedTile.ext rfl ?_

Premises used: DiscreteTiling.PlacedTile.ext, rfl