Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: case refine_2
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
i₁ : ιₚ
g₁ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₁)).subtype (↑ps i₁).symmetries
i₂ : ιₚ
g₂ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₂)).subtype (↑ps i₂).symmetries
x✝ :
  { index := i₁, groupElts := g₁ }.index = { index := i₂, groupElts := g₂ }.index ∧
    Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₁, groupElts := g₁ }.index)).subtype
              (↑ps { index := i₁, groupElts := g₁ }.index).symmetries)) ⁻¹'
        {{ index := i₁, groupElts := g₁ }.groupElts} =
      Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₂, groupElts := g₂ }.index)).subtype
              (↑ps { index := i₂, groupElts := g₂ }.index).symmetries)) ⁻¹'
        {{ index := i₂, groupElts := g₂ }.groupElts}
hi : { index := i₁, groupElts := g₁ }.index = { index := i₂, groupElts := g₂ }.index
hq :
  Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₁, groupElts := g₁ }.index)).subtype
            (↑ps { index := i₁, groupElts := g₁ }.index).symmetries)) ⁻¹'
      {{ index := i₁, groupElts := g₁ }.groupElts} =
    Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₂, groupElts := g₂ }.index)).subtype
            (↑ps { index := i₂, groupElts := g₂ }.index).symmetries)) ⁻¹'
      {{ index := i₂, groupElts := g₂ }.groupElts}
⊢ { index := i₁, groupElts := g₁ } = { index := i₂, groupElts := g₂ }

Tactic:
dsimp only at hi

Goal state after:
case refine_2
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
i₁ : ιₚ
g₁ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₁)).subtype (↑ps i₁).symmetries
i₂ : ιₚ
g₂ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₂)).subtype (↑ps i₂).symmetries
x✝ :
  { index := i₁, groupElts := g₁ }.index = { index := i₂, groupElts := g₂ }.index ∧
    Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₁, groupElts := g₁ }.index)).subtype
              (↑ps { index := i₁, groupElts := g₁ }.index).symmetries)) ⁻¹'
        {{ index := i₁, groupElts := g₁ }.groupElts} =
      Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₂, groupElts := g₂ }.index)).subtype
              (↑ps { index := i₂, groupElts := g₂ }.index).symmetries)) ⁻¹'
        {{ index := i₂, groupElts := g₂ }.groupElts}
hi : i₁ = i₂
hq :
  Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₁, groupElts := g₁ }.index)).subtype
            (↑ps { index := i₁, groupElts := g₁ }.index).symmetries)) ⁻¹'
      {{ index := i₁, groupElts := g₁ }.groupElts} =
    Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₂, groupElts := g₂ }.index)).subtype
            (↑ps { index := i₂, groupElts := g₂ }.index).symmetries)) ⁻¹'
      {{ index := i₂, groupElts := g₂ }.groupElts}
⊢ { index := i₁, groupElts := g₁ } = { index := i₂, groupElts := g₂ }