-- Lean 4 proof step from Mathlib.Combinatorics.Tiling.Tile (goal)
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
⊢ 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)
have 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))
Tactic: refine PlacedTile.ext rfl ?_