awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ιₚ
pt₁ pt₂ : PlacedTile ps
refine_1 : ∀ (h : pt₁ = pt₂), pt₁.index = pt₂.index ∧ ∃ (g : G), ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₂.groupElts
refine_2 :
  (pt₁.index = pt₂.index ∧ ∃ (g : G), ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₂.groupElts) →
    ∀ (h : pt₁.index = pt₂.index) (g : G) (hg₁ : ⟦g⟧ = pt₁.groupElts) (hg₂ : ⟦g⟧ = pt₂.groupElts), pt₁ = pt₂
⊢ pt₁ = pt₂ ↔ pt₁.index = pt₂.index ∧ ∃ (g : G), ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₂.groupElts

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨h, g, hg₁, hg₂⟩ ↦ ?_⟩
-- 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 ιₚ
pt₁ pt₂ : PlacedTile ps
h : pt₁ = pt₂
refine_1 : pt₁.index = pt₁.index ∧ ∃ (g : G), ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₁.groupElts
⊢ pt₁.index = pt₂.index ∧ ∃ (g : G), ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₂.groupElts

Tactic:
subst h
-- 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 ιₚ
pt₁ : PlacedTile ps
refine_1 : ∃ (g : G), ⟦g⟧ = pt₁.groupElts
⊢ pt₁.index = pt₁.index ∧ ∃ (g : G), ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₁.groupElts

Tactic:
simp only [and_self, true_and]

Premises used: and_self, true_and
-- 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 ιₚ
pt₁ : PlacedTile ps
⊢ ∃ (g : G), ⟦g⟧ = pt₁.groupElts

Tactic:
⟨pt₁.groupElts.out, ?_⟩

Premises used: DiscreteTiling.PlacedTile.groupElts, Quotient.out, Exists.intro
-- 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 ιₚ
pt₁ : PlacedTile ps
refine_1 : ⟦Quotient.out pt₁.groupElts⟧ = pt₁.groupElts
⊢ ∃ (g : G), ⟦g⟧ = pt₁.groupElts

Tactic:
refine ⟨pt₁.groupElts.out, ?_⟩
-- 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 ιₚ
pt₁ : PlacedTile ps
refine_1 refine_1₁ : pt₁.groupElts = pt₁.groupElts
⊢ ⟦Quotient.out pt₁.groupElts⟧ = pt₁.groupElts

Tactic:
rw [Quotient.out_eq]

Premises used: Quotient.out_eq
-- 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 ιₚ
pt₁ pt₂ : PlacedTile ps
h_1 : pt₁.index = pt₂.index ∧ ∃ (g : G), ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₂.groupElts
h : pt₁.index = pt₂.index
g : G
hg₁ : ⟦g⟧ = pt₁.groupElts
hg₂ : ⟦g⟧ = pt₂.groupElts
refine_2 :
  ∀ (i₁ : ιₚ)
    (g₁ :
      G ⧸
        Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₁) : Set X)))
          ((↑ps : ιₚ → Prototile G X) i₁).symmetries),
    ({ index := i₁, groupElts := g₁ : PlacedTile ps }.index = pt₂.index ∧
        ∃ (g : G), ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = pt₂.groupElts) →
      ∀ (h : { index := i₁, groupElts := g₁ : PlacedTile ps }.index = pt₂.index)
        (hg₁ : ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts), { index := i₁, groupElts := g₁ : PlacedTile ps } = pt₂
⊢ pt₁ = pt₂

Tactic:
rcases pt₁ with ⟨i₁, g₁⟩
-- 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 ιₚ
pt₂ : PlacedTile ps
g : G
hg₂ : ⟦g⟧ = pt₂.groupElts
i₁ : ιₚ
g₁ :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₁) : Set X)))
      ((↑ps : ιₚ → Prototile G X) i₁).symmetries
h_1 :
  { index := i₁, groupElts := g₁ : PlacedTile ps }.index = pt₂.index ∧
    ∃ (g : G), ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = pt₂.groupElts
h : { index := i₁, groupElts := g₁ : PlacedTile ps }.index = pt₂.index
hg₁ : ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts
refine_2 :
  ∀ (i₂ : ιₚ)
    (g₂ :
      G ⧸
        Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₂) : Set X)))
          ((↑ps : ιₚ → Prototile G X) i₂).symmetries)
    (hg₂ : ⟦g⟧ = { index := i₂, groupElts := g₂ }.groupElts),
    ({ index := i₁, groupElts := g₁ : PlacedTile ps }.index = { index := i₂, groupElts := g₂ : PlacedTile ps }.index ∧
        ∃ (g : G),
          ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = { index := i₂, groupElts := g₂ }.groupElts) →
      ∀
        (h :
          { index := i₁, groupElts := g₁ : PlacedTile ps }.index =
            { index := i₂, groupElts := g₂ : PlacedTile ps }.index),
        { index := i₁, groupElts := g₁ : PlacedTile ps } = { index := i₂, groupElts := g₂ }
⊢ { index := i₁, groupElts := g₁ : PlacedTile ps } = pt₂

Tactic:
rcases pt₂ with ⟨i₂, g₂⟩
-- 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
i₁ : ιₚ
g₁ :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₁) : Set X)))
      ((↑ps : ιₚ → Prototile G X) i₁).symmetries
hg₁ : ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts
i₂ : ιₚ
g₂ :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₂) : Set X)))
      ((↑ps : ιₚ → Prototile G X) i₂).symmetries
hg₂ : ⟦g⟧ = { index := i₂, groupElts := g₂ }.groupElts
h_1 :
  { index := i₁, groupElts := g₁ : PlacedTile ps }.index = { index := i₂, groupElts := g₂ : PlacedTile ps }.index ∧
    ∃ (g : G), ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = { index := i₂, groupElts := g₂ }.groupElts
h : i₁ = i₂
refine_2 :
  ∀
    (g₂ :
      G ⧸
        Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₁) : Set X)))
          ((↑ps : ιₚ → Prototile G X) i₁).symmetries)
    (hg₂ : ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts),
    ({ index := i₁, groupElts := g₁ : PlacedTile ps }.index = { index := i₁, groupElts := g₂ : PlacedTile ps }.index ∧
        ∃ (g : G),
          ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts) →
      { index := i₁, groupElts := g₁ : PlacedTile ps } = { index := i₁, groupElts := g₂ }
⊢ { index := i₁, groupElts := g₁ : PlacedTile ps } = { index := i₂, groupElts := g₂ }

Tactic:
subst h
-- 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
i₁ : ιₚ
g₁ :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₁) : Set X)))
      ((↑ps : ιₚ → Prototile G X) i₁).symmetries
hg₁ : ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts
g₂ :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₁) : Set X)))
      ((↑ps : ιₚ → Prototile G X) i₁).symmetries
hg₂ : ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
h :
  { index := i₁, groupElts := g₁ : PlacedTile ps }.index = { index := i₁, groupElts := g₂ : PlacedTile ps }.index ∧
    ∃ (g : G), ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
refine_2 :
  { index := i₁, groupElts := g₁ : PlacedTile ps }.index = { index := i₁, groupElts := g₂ : PlacedTile ps }.index
refine_2₁ :
  { index := i₁, groupElts := g₁ : PlacedTile ps }.groupElts ≍
    { index := i₁, groupElts := g₂ : PlacedTile ps }.groupElts
⊢ { index := i₁, groupElts := g₁ : PlacedTile ps } = { index := i₁, groupElts := g₂ }

Tactic:
ext
-- 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
i₁ : ιₚ
g₁ :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₁) : Set X)))
      ((↑ps : ιₚ → Prototile G X) i₁).symmetries
hg₁ : ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts
g₂ :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₁) : Set X)))
      ((↑ps : ιₚ → Prototile G X) i₁).symmetries
hg₂ : ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
h :
  { index := i₁, groupElts := g₁ : PlacedTile ps }.index = { index := i₁, groupElts := g₂ : PlacedTile ps }.index ∧
    ∃ (g : G), ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
⊢ { index := i₁, groupElts := g₁ : PlacedTile ps }.index = { index := i₁, groupElts := g₂ : PlacedTile ps }.index

Tactic:
rfl
-- 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
i₁ : ιₚ
g₁ :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₁) : Set X)))
      ((↑ps : ιₚ → Prototile G X) i₁).symmetries
hg₁ : ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts
g₂ :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₁) : Set X)))
      ((↑ps : ιₚ → Prototile G X) i₁).symmetries
hg₂ : ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
h :
  { index := i₁, groupElts := g₁ : PlacedTile ps }.index = { index := i₁, groupElts := g₂ : PlacedTile ps }.index ∧
    ∃ (g : G), ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
⊢ { index := i₁, groupElts := g₁ : PlacedTile ps }.groupElts ≍
    { index := i₁, groupElts := g₂ : PlacedTile ps }.groupElts

Tactic:
heq_of_eq (hg₁.symm.trans hg₂)

Premises used: Set.Mem, setOf, heq_of_eq, Eq.symm, Eq.trans
-- 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
i₁ : ιₚ
g₁ :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₁) : Set X)))
      ((↑ps : ιₚ → Prototile G X) i₁).symmetries
hg₁ : ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts
g₂ :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₁) : Set X)))
      ((↑ps : ιₚ → Prototile G X) i₁).symmetries
hg₂ : ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
h :
  { index := i₁, groupElts := g₁ : PlacedTile ps }.index = { index := i₁, groupElts := g₂ : PlacedTile ps }.index ∧
    ∃ (g : G), ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
⊢ { index := i₁, groupElts := g₁ : PlacedTile ps }.groupElts ≍
    { index := i₁, groupElts := g₂ : PlacedTile ps }.groupElts

Tactic:
exact heq_of_eq (hg₁.symm.trans hg₂)

Premises used: heq_of_eq, Eq.symm, Eq.trans
-- 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 ιₚ
pt₁ pt₂ : PlacedTile ps
⊢ pt₁ = pt₂ ↔
    pt₁.index = pt₂.index ∧
      Quotient.mk
            (QuotientGroup.leftRel
              (Subgroup.map
                (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₁.index) : Set X)))
                ((↑ps : ιₚ → Prototile G X) pt₁.index).symmetries)) ⁻¹'
          {pt₁.groupElts} =
        Quotient.mk
            (QuotientGroup.leftRel
              (Subgroup.map
                (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₂.index) : Set X)))
                ((↑ps : ιₚ → Prototile G X) pt₂.index).symmetries)) ⁻¹'
          {pt₂.groupElts}

Tactic:
⟨fun h ↦ ?_, fun ⟨hi, hq⟩ ↦ ?_⟩

Premises used: _private.0.DiscreteTiling.PlacedTile.ext_iff_of_preimage.match_1, Iff.intro, Eq
-- 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 ιₚ
pt₁ pt₂ : PlacedTile ps
refine_1 :
  ∀ (h : pt₁ = pt₂),
    pt₁.index = pt₂.index ∧
      Quotient.mk
            (QuotientGroup.leftRel
              (Subgroup.map
                (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₁.index) : Set X)))
                ((↑ps : ιₚ → Prototile G X) pt₁.index).symmetries)) ⁻¹'
          {pt₁.groupElts} =
        Quotient.mk
            (QuotientGroup.leftRel
              (Subgroup.map
                (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₂.index) : Set X)))
                ((↑ps : ιₚ → Prototile G X) pt₂.index).symmetries)) ⁻¹'
          {pt₂.groupElts}
refine_2 :
  pt₁.index = pt₂.index ∧
      Quotient.mk
            (QuotientGroup.leftRel
              (Subgroup.map
                (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₁.index) : Set X)))
                ((↑ps : ιₚ → Prototile G X) pt₁.index).symmetries)) ⁻¹'
          {pt₁.groupElts} =
        Quotient.mk
            (QuotientGroup.leftRel
              (Subgroup.map
                (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₂.index) : Set X)))
                ((↑ps : ιₚ → Prototile G X) pt₂.index).symmetries)) ⁻¹'
          {pt₂.groupElts} →
    ∀ (hi : pt₁.index = pt₂.index)
      (hq :
        Quotient.mk
              (QuotientGroup.leftRel
                (Subgroup.map
                  (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₁.index) : Set X)))
                  ((↑ps : ιₚ → Prototile G X) pt₁.index).symmetries)) ⁻¹'
            {pt₁.groupElts} =
          Quotient.mk
              (QuotientGroup.leftRel
                (Subgroup.map
                  (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₂.index) : Set X)))
                  ((↑ps : ιₚ → Prototile G X) pt₂.index).symmetries)) ⁻¹'
            {pt₂.groupElts}),
      pt₁ = pt₂
⊢ pt₁ = pt₂ ↔
    pt₁.index = pt₂.index ∧
      Quotient.mk
            (QuotientGroup.leftRel
              (Subgroup.map
                (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₁.index) : Set X)))
                ((↑ps : ιₚ → Prototile G X) pt₁.index).symmetries)) ⁻¹'
          {pt₁.groupElts} =
        Quotient.mk
            (QuotientGroup.leftRel
              (Subgroup.map
                (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₂.index) : Set X)))
                ((↑ps : ιₚ → Prototile G X) pt₂.index).symmetries)) ⁻¹'
          {pt₂.groupElts}

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨hi, hq⟩ ↦ ?_⟩
-- 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 ιₚ
pt₁ pt₂ : PlacedTile ps
h : pt₁ = pt₂
refine_1 :
  pt₁.index = pt₁.index ∧
    Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₁.index) : Set X)))
              ((↑ps : ιₚ → Prototile G X) pt₁.index).symmetries)) ⁻¹'
        {pt₁.groupElts} =
      Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₁.index) : Set X)))
              ((↑ps : ιₚ → Prototile G X) pt₁.index).symmetries)) ⁻¹'
        {pt₁.groupElts}
⊢ pt₁.index = pt₂.index ∧
    Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₁.index) : Set X)))
              ((↑ps : ιₚ → Prototile G X) pt₁.index).symmetries)) ⁻¹'
        {pt₁.groupElts} =
      Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₂.index) : Set X)))
              ((↑ps : ιₚ → Prototile G X) pt₂.index).symmetries)) ⁻¹'
        {pt₂.groupElts}

Tactic:
subst h
-- 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 ιₚ
pt₁ : PlacedTile ps
⊢ pt₁.index = pt₁.index ∧
    Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₁.index) : Set X)))
              ((↑ps : ιₚ → Prototile G X) pt₁.index).symmetries)) ⁻¹'
        {pt₁.groupElts} =
      Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₁.index) : Set X)))
              ((↑ps : ιₚ → Prototile G X) pt₁.index).symmetries)) ⁻¹'
        {pt₁.groupElts}

Tactic:
simp only [and_self]

Premises used: and_self
-- 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 ιₚ
i₁ : ιₚ
g₁ g₂ :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₁) : Set X)))
      ((↑ps : ιₚ → Prototile G X) i₁).symmetries
h :
  { index := i₁, groupElts := g₁ : PlacedTile ps }.index = { index := i₁, groupElts := g₂ : PlacedTile ps }.index ∧
    Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map
              (Subgroup.subtype
                (MulAction.stabilizer G
                  (↑((↑ps : ιₚ → Prototile G X) { index := i₁, groupElts := g₁ : PlacedTile ps }.index) : Set X)))
              ((↑ps : ιₚ → Prototile G X) { index := i₁, groupElts := g₁ : PlacedTile ps }.index).symmetries)) ⁻¹'
        {{ index := i₁, groupElts := g₁ : PlacedTile ps }.groupElts} =
      Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map
              (Subgroup.subtype
                (MulAction.stabilizer G
                  (↑((↑ps : ιₚ → Prototile G X) { index := i₁, groupElts := g₂ : PlacedTile ps }.index) : Set X)))
              ((↑ps : ιₚ → Prototile G X) { index := i₁, groupElts := g₂ : PlacedTile ps }.index).symmetries)) ⁻¹'
        {{ index := i₁, groupElts := g₂ : PlacedTile ps }.groupElts}
hq :
  Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map
            (Subgroup.subtype
              (MulAction.stabilizer G
                (↑((↑ps : ιₚ → Prototile G X) { index := i₁, groupElts := g₁ : PlacedTile ps }.index) : Set X)))
            ((↑ps : ιₚ → Prototile G X) { index := i₁, groupElts := g₁ : PlacedTile ps }.index).symmetries)) ⁻¹'
      {{ index := i₁, groupElts := g₁ : PlacedTile ps }.groupElts} =
    Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map
            (Subgroup.subtype
              (MulAction.stabilizer G
                (↑((↑ps : ιₚ → Prototile G X) { index := i₁, groupElts := g₂ : PlacedTile ps }.index) : Set X)))
            ((↑ps : ιₚ → Prototile G X) { index := i₁, groupElts := g₂ : PlacedTile ps }.index).symmetries)) ⁻¹'
      {{ index := i₁, groupElts := g₂ : PlacedTile ps }.groupElts}
refine_2 :
  { index := i₁, groupElts := g₁ : PlacedTile ps }.index = { index := i₁, groupElts := g₂ : PlacedTile ps }.index
refine_2₁ :
  { index := i₁, groupElts := g₁ : PlacedTile ps }.groupElts ≍
    { index := i₁, groupElts := g₂ : PlacedTile ps }.groupElts
⊢ { index := i₁, groupElts := g₁ : PlacedTile ps } = { index := i₁, groupElts := g₂ }

Tactic:
ext
-- 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 ιₚ
i₁ : ιₚ
g₁ g₂ :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₁) : Set X)))
      ((↑ps : ιₚ → Prototile G X) i₁).symmetries
h :
  { index := i₁, groupElts := g₁ : PlacedTile ps }.index = { index := i₁, groupElts := g₂ : PlacedTile ps }.index ∧
    Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map
              (Subgroup.subtype
                (MulAction.stabilizer G
                  (↑((↑ps : ιₚ → Prototile G X) { index := i₁, groupElts := g₁ : PlacedTile ps }.index) : Set X)))
              ((↑ps : ιₚ → Prototile G X) { index := i₁, groupElts := g₁ : PlacedTile ps }.index).symmetries)) ⁻¹'
        {{ index := i₁, groupElts := g₁ : PlacedTile ps }.groupElts} =
      Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map
              (Subgroup.subtype
                (MulAction.stabilizer G
                  (↑((↑ps : ιₚ → Prototile G X) { index := i₁, groupElts := g₂ : PlacedTile ps }.index) : Set X)))
              ((↑ps : ιₚ → Prototile G X) { index := i₁, groupElts := g₂ : PlacedTile ps }.index).symmetries)) ⁻¹'
        {{ index := i₁, groupElts := g₂ : PlacedTile ps }.groupElts}
hq :
  Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map
            (Subgroup.subtype
              (MulAction.stabilizer G
                (↑((↑ps : ιₚ → Prototile G X) { index := i₁, groupElts := g₁ : PlacedTile ps }.index) : Set X)))
            ((↑ps : ιₚ → Prototile G X) { index := i₁, groupElts := g₁ : PlacedTile ps }.index).symmetries)) ⁻¹'
      {{ index := i₁, groupElts := g₁ : PlacedTile ps }.groupElts} =
    Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map
            (Subgroup.subtype
              (MulAction.stabilizer G
                (↑((↑ps : ιₚ → Prototile G X) { index := i₁, groupElts := g₂ : PlacedTile ps }.index) : Set X)))
            ((↑ps : ιₚ → Prototile G X) { index := i₁, groupElts := g₂ : PlacedTile ps }.index).symmetries)) ⁻¹'
      {{ index := i₁, groupElts := g₂ : PlacedTile ps }.groupElts}
⊢ { index := i₁, groupElts := g₁ : PlacedTile ps }.index = { index := i₁, groupElts := g₂ : PlacedTile ps }.index

Tactic:
rfl
-- 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 ιₚ
i₁ : ιₚ
g₁ g₂ :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₁) : Set X)))
      ((↑ps : ιₚ → Prototile G X) i₁).symmetries
h :
  { index := i₁, groupElts := g₁ : PlacedTile ps }.index = { index := i₁, groupElts := g₂ : PlacedTile ps }.index ∧
    Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map
              (Subgroup.subtype
                (MulAction.stabilizer G
                  (↑((↑ps : ιₚ → Prototile G X) { index := i₁, groupElts := g₁ : PlacedTile ps }.index) : Set X)))
              ((↑ps : ιₚ → Prototile G X) { index := i₁, groupElts := g₁ : PlacedTile ps }.index).symmetries)) ⁻¹'
        {{ index := i₁, groupElts := g₁ : PlacedTile ps }.groupElts} =
      Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map
              (Subgroup.subtype
                (MulAction.stabilizer G
                  (↑((↑ps : ιₚ → Prototile G X) { index := i₁, groupElts := g₂ : PlacedTile ps }.index) : Set X)))
              ((↑ps : ιₚ → Prototile G X) { index := i₁, groupElts := g₂ : PlacedTile ps }.index).symmetries)) ⁻¹'
        {{ index := i₁, groupElts := g₂ : PlacedTile ps }.groupElts}
hq :
  Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map
            (Subgroup.subtype
              (MulAction.stabilizer G
                (↑((↑ps : ιₚ → Prototile G X) { index := i₁, groupElts := g₁ : PlacedTile ps }.index) : Set X)))
            ((↑ps : ιₚ → Prototile G X) { index := i₁, groupElts := g₁ : PlacedTile ps }.index).symmetries)) ⁻¹'
      {{ index := i₁, groupElts := g₁ : PlacedTile ps }.groupElts} =
    Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map
            (Subgroup.subtype
              (MulAction.stabilizer G
                (↑((↑ps : ιₚ → Prototile G X) { index := i₁, groupElts := g₂ : PlacedTile ps }.index) : Set X)))
            ((↑ps : ιₚ → Prototile G X) { index := i₁, groupElts := g₂ : PlacedTile ps }.index).symmetries)) ⁻¹'
      {{ index := i₁, groupElts := g₂ : PlacedTile ps }.groupElts}
⊢ { index := i₁, groupElts := g₁ : PlacedTile ps }.groupElts ≍
    { index := i₁, groupElts := g₂ : PlacedTile ps }.groupElts

Tactic:
heq_of_eq (Set.singleton_eq_singleton_iff.1
        ((Set.preimage_eq_preimage Quotient.mk''_surjective).1 hq))

Premises used: Set.Mem, setOf, Set.singleton_eq_singleton_iff, Quotient.mk''_surjective, heq_of_eq, Set.preimage_eq_preimage, Iff.mp