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 ιₚ
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:
exact heq_of_eq (Set.singleton_eq_singleton_iff.1
        ((Set.preimage_eq_preimage Quotient.mk''_surjective).1 hq))

Premises used: Set.singleton_eq_singleton_iff, Quotient.mk''_surjective, heq_of_eq, Set.preimage_eq_preimage, Iff.mp
-- 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
a b : G
r :
  (QuotientGroup.leftRel
        (Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X)).subtype
          ((↑ps : ιₚ → Prototile G X) pt.index).symmetries) :
      G → G → Prop)
    a b
⊢ a⁻¹ * b ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X)))
      ((↑ps : ιₚ → Prototile G X) pt.index).symmetries

Tactic:
rw [QuotientGroup.leftRel_eq] at r

Premises used: QuotientGroup.leftRel_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 : 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
rw :
  Membership.mem (γ := Subgroup G) (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X)) (a⁻¹ * b)
⊢ a • (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X) = b • (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X)

Tactic:
rw [eq_comm, ← inv_smul_eq_iff, smul_smul, ← MulAction.mem_stabilizer_iff]

Premises used: inv_smul_eq_iff, smul_smul, eq_comm, MulAction.mem_stabilizer_iff
-- 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
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
⊢ Membership.mem (γ := Subgroup G) (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X)) (a⁻¹ * b)

Tactic:
SetLike.le_def.1 (Subgroup.map_subtype_le _) r

Premises used: SetLike.le_def, Subgroup.map_subtype_le, Iff.mp
-- 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
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
⊢ Membership.mem (γ := Subgroup G) (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X)) (a⁻¹ * b)

Tactic:
exact SetLike.le_def.1 (Subgroup.map_subtype_le _) r

Premises used: SetLike.le_def, Subgroup.map_subtype_le, Iff.mp
-- 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 ιₚ
x : X
pt : PlacedTile ps
⊢ x ∈ (↑pt : Set X) ↔ x ∈ pt

Tactic:
Iff.rfl

Premises used: Iff.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
⊢ (↑{ index := i, groupElts := ⟦g⟧ : PlacedTile ps } : Set X) = g • (↑((↑ps : ιₚ → Prototile G X) i) : Set X)

Tactic:
rfl

Premises used: Quotient.liftOn', rfl, DiscreteTiling.PlacedTile.coeSet
-- 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
⊢ (↑{ index := i,
          groupElts :=
            (↑g :
              G ⧸
                Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
                  ((↑ps : ιₚ → Prototile G X) i).symmetries) } :
      Set X) =
    g • (↑((↑ps : ιₚ → Prototile G X) i) : Set X)

Tactic:
rfl

Premises used: Quotient.liftOn', rfl, DiscreteTiling.PlacedTile.coeSet
-- 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
rcases :
  ∀ (index : ιₚ)
    (groupElts :
      G ⧸
        Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) index) : Set X)))
          ((↑ps : ιₚ → Prototile G X) index).symmetries),
    (↑{ index := index, groupElts := groupElts : PlacedTile ps } : Set X).Nonempty ↔
      (↑((↑ps : ιₚ → Prototile G X) { index := index, groupElts := groupElts : PlacedTile ps }.index) : Set X).Nonempty
⊢ (↑pt : Set X).Nonempty ↔ (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X).Nonempty

Tactic:
rcases pt with ⟨index, groupElts⟩

Premises used: DiscreteTiling.PlacedTile.groupElts, DiscreteTiling.PlacedTile.index
-- 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 ιₚ
index : ιₚ
groupElts :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) index) : Set X)))
      ((↑ps : ιₚ → Prototile G X) index).symmetries
simp :
  Set.Nonempty.{u_2} (α := X)
      (Quotient.liftOn' groupElts (fun (g : G) ↦ g • (↑((↑ps : ιₚ → Prototile G X) index) : Set X)) ⋯) ↔
    (↑((↑ps : ιₚ → Prototile G X) index) : Set X).Nonempty
⊢ (↑{ index := index, groupElts := groupElts : PlacedTile ps } : Set X).Nonempty ↔
    (↑((↑ps : ιₚ → Prototile G X) { index := index, groupElts := groupElts : PlacedTile ps }.index) : Set X).Nonempty

Tactic:
simp only [coeSet]

Premises used: DiscreteTiling.PlacedTile.coeSet
-- 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 ιₚ
index : ιₚ
groupElts :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) index) : Set X)))
      ((↑ps : ιₚ → Prototile G X) index).symmetries
rw :
  (Quotient.out groupElts • (↑((↑ps : ιₚ → Prototile G X) index) : Set X)).Nonempty ↔
    (↑((↑ps : ιₚ → Prototile G X) index) : Set X).Nonempty
⊢ Set.Nonempty.{u_2} (α := X)
      (Quotient.liftOn' groupElts (fun (g : G) ↦ g • (↑((↑ps : ιₚ → Prototile G X) index) : Set X)) ⋯) ↔
    (↑((↑ps : ιₚ → Prototile G X) index) : Set X).Nonempty

Tactic:
rw [← groupElts.out_eq', Quotient.liftOn'_mk'']

Premises used: Quotient.out_eq', Quotient.liftOn'_mk''
-- 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 ιₚ
index : ιₚ
groupElts :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) index) : Set X)))
      ((↑ps : ιₚ → Prototile G X) index).symmetries
⊢ (Quotient.out groupElts • (↑((↑ps : ιₚ → Prototile G X) index) : Set X)).Nonempty ↔
    (↑((↑ps : ιₚ → Prototile G X) index) : Set X).Nonempty

Tactic:
simp
-- 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 ⧸
    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 } : Set X).Nonempty ↔
    (↑((↑ps : ιₚ → Prototile G X) i) : Set X).Nonempty

Tactic:
coe_nonempty_iff

Premises used: DiscreteTiling.PlacedTile.coe_nonempty_iff
-- 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
rcases :
  ∀ (index : ιₚ)
    (groupElts :
      G ⧸
        Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) index) : Set X)))
          ((↑ps : ιₚ → Prototile G X) index).symmetries),
    (↑{ index := index, groupElts := groupElts : PlacedTile ps } : Set X).Finite ↔
      (↑((↑ps : ιₚ → Prototile G X) { index := index, groupElts := groupElts : PlacedTile ps }.index) : Set X).Finite
⊢ (↑pt : Set X).Finite ↔ (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X).Finite

Tactic:
rcases pt with ⟨index, groupElts⟩

Premises used: DiscreteTiling.PlacedTile.groupElts, DiscreteTiling.PlacedTile.index
-- 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 ιₚ
index : ιₚ
groupElts :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) index) : Set X)))
      ((↑ps : ιₚ → Prototile G X) index).symmetries
simp :
  Set.Finite.{u_2} (α := X)
      (Quotient.liftOn' groupElts (fun (g : G) ↦ g • (↑((↑ps : ιₚ → Prototile G X) index) : Set X)) ⋯) ↔
    (↑((↑ps : ιₚ → Prototile G X) index) : Set X).Finite
⊢ (↑{ index := index, groupElts := groupElts : PlacedTile ps } : Set X).Finite ↔
    (↑((↑ps : ιₚ → Prototile G X) { index := index, groupElts := groupElts : PlacedTile ps }.index) : Set X).Finite

Tactic:
simp only [coeSet]

Premises used: DiscreteTiling.PlacedTile.coeSet
-- 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 ιₚ
index : ιₚ
groupElts :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) index) : Set X)))
      ((↑ps : ιₚ → Prototile G X) index).symmetries
rw :
  (Quotient.out groupElts • (↑((↑ps : ιₚ → Prototile G X) index) : Set X)).Finite ↔
    (↑((↑ps : ιₚ → Prototile G X) index) : Set X).Finite
⊢ Set.Finite.{u_2} (α := X)
      (Quotient.liftOn' groupElts (fun (g : G) ↦ g • (↑((↑ps : ιₚ → Prototile G X) index) : Set X)) ⋯) ↔
    (↑((↑ps : ιₚ → Prototile G X) index) : Set X).Finite

Tactic:
rw [← groupElts.out_eq', Quotient.liftOn'_mk'']

Premises used: Quotient.out_eq', Quotient.liftOn'_mk''
-- 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 ιₚ
index : ιₚ
groupElts :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) index) : Set X)))
      ((↑ps : ιₚ → Prototile G X) index).symmetries
⊢ (Quotient.out groupElts • (↑((↑ps : ιₚ → Prototile G X) index) : Set X)).Finite ↔
    (↑((↑ps : ιₚ → Prototile G X) index) : Set X).Finite

Tactic:
simp
-- 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 ⧸
    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 } : Set X).Finite ↔ (↑((↑ps : ιₚ → Prototile G X) i) : Set X).Finite

Tactic:
coe_finite_iff

Premises used: DiscreteTiling.PlacedTile.coe_finite_iff
-- 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 :
  (QuotientGroup.leftRel
        (Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X)).subtype
          ((↑ps : ιₚ → Prototile G X) pt.index).symmetries) :
      G → G → Prop)
    a b
⊢ a⁻¹ * b ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X)))
      ((↑ps : ιₚ → Prototile G X) pt.index).symmetries

Tactic:
rw [QuotientGroup.leftRel_eq] at r

Premises used: QuotientGroup.leftRel_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 ιₚ
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)

Tactic:
PlacedTile.ext rfl ?_

Premises used: DiscreteTiling.PlacedTile.ext, 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 h : G
i : ιₚ
⊢ g • { index := i, groupElts := ⟦h⟧ : PlacedTile ps } =
    { index := i,
      groupElts :=
        (↑(g * h) :
          G ⧸
            Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
              ((↑ps : ιₚ → Prototile G X) i).symmetries) }

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, setOf, 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 h : G
i : ιₚ
⊢ HSMul.hSMul (β := PlacedTile ps) g
      { index := i,
        groupElts :=
          (↑h :
            G ⧸
              Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
                ((↑ps : ιₚ → Prototile G X) i).symmetries) :
        PlacedTile ps } =
    { index := i,
      groupElts :=
        (↑(g * h) :
          G ⧸
            Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
              ((↑ps : ιₚ → Prototile G X) i).symmetries) }

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, setOf, 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
pt : PlacedTile ps
h :
  ∀ (i : ιₚ) (gx : G),
    (HSMul.hSMul (β := PlacedTile ps) g
          { index := i,
            groupElts :=
              (↑gx :
                G ⧸
                  Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
                    ((↑ps : ιₚ → Prototile G X) i).symmetries) :
            PlacedTile ps }).index =
      index.{u_1, u_2, u_3} (X := X) (ps := ps)
        { index := i,
          groupElts :=
            (↑gx :
              G ⧸
                Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
                  ((↑ps : ιₚ → Prototile G X) i).symmetries) }
⊢ (g • pt).index = pt.index

Tactic:
induction pt using PlacedTile.induction_on
-- 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 : ιₚ
gx : G
⊢ (HSMul.hSMul (β := PlacedTile ps) g
        { index := i,
          groupElts :=
            (↑gx :
              G ⧸
                Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
                  ((↑ps : ιₚ → Prototile G X) i).symmetries) :
          PlacedTile ps }).index =
    index.{u_1, u_2, u_3} (X := X) (ps := ps)
      { index := i,
        groupElts :=
          (↑gx :
            G ⧸
              Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
                ((↑ps : ιₚ → Prototile G X) i).symmetries) }

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
pt : PlacedTile ps
h :
  ∀ (i : ιₚ) (gx : G),
    (↑(HSMul.hSMul (β := PlacedTile ps) g
            { index := i,
              groupElts :=
                (↑gx :
                  G ⧸
                    Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
                      ((↑ps : ιₚ → Prototile G X) i).symmetries) :
              PlacedTile ps }) :
        Set X) =
      HSMul.hSMul (β := Set X) g
        (↑{ index := i,
              groupElts :=
                (↑gx :
                  G ⧸
                    Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
                      ((↑ps : ιₚ → Prototile G X) i).symmetries) } :
          Set X)
⊢ (↑(g • pt) : Set X) = g • (↑pt : Set X)

Tactic:
induction pt using PlacedTile.induction_on
-- 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 : ιₚ
gx : G
⊢ (↑(HSMul.hSMul (β := PlacedTile ps) g
          { index := i,
            groupElts :=
              (↑gx :
                G ⧸
                  Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
                    ((↑ps : ιₚ → Prototile G X) i).symmetries) :
            PlacedTile ps }) :
      Set X) =
    HSMul.hSMul (β := Set X) g
      (↑{ index := i,
            groupElts :=
              (↑gx :
                G ⧸
                  Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
                    ((↑ps : ιₚ → Prototile G X) i).symmetries) } :
        Set X)

Tactic:
simp [coeSet, mul_smul]

Premises used: SemigroupAction.mul_smul, DiscreteTiling.PlacedTile.coeSet
-- 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 ιₚ
x y : G
pt : PlacedTile ps
h :
  ∀ (i : ιₚ) (gx : G),
    HSMul.hSMul (β := PlacedTile ps) (x * y)
        { index := i,
          groupElts :=
            (↑gx :
              G ⧸
                Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
                  ((↑ps : ιₚ → Prototile G X) i).symmetries) :
          PlacedTile ps } =
      x •
        HSMul.hSMul (β := PlacedTile ps) y
          { index := i,
            groupElts :=
              (↑gx :
                G ⧸
                  Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
                    ((↑ps : ιₚ → Prototile G X) i).symmetries) :
            PlacedTile ps }
⊢ (x * y) • pt = x • y • pt

Tactic:
induction pt using PlacedTile.induction_on
-- 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 ιₚ
x y : G
i : ιₚ
gx : G
⊢ HSMul.hSMul (β := PlacedTile ps) (x * y)
      { index := i,
        groupElts :=
          (↑gx :
            G ⧸
              Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
                ((↑ps : ιₚ → Prototile G X) i).symmetries) :
        PlacedTile ps } =
    x •
      HSMul.hSMul (β := PlacedTile ps) y
        { index := i,
          groupElts :=
            (↑gx :
              G ⧸
                Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
                  ((↑ps : ιₚ → Prototile G X) i).symmetries) :
          PlacedTile ps }

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- 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
h :
  ∀ (i : ιₚ) (gx : G),
    HSMul.hSMul (α := G) (β := PlacedTile ps) 1
        { index := i,
          groupElts :=
            (↑gx :
              G ⧸
                Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
                  ((↑ps : ιₚ → Prototile G X) i).symmetries) :
          PlacedTile ps } =
      { index := i,
        groupElts :=
          (↑gx :
            G ⧸
              Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
                ((↑ps : ιₚ → Prototile G X) i).symmetries) }
⊢ HSMul.hSMul (α := G) 1 pt = pt

Tactic:
induction pt using PlacedTile.induction_on
-- 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 : ιₚ
gx : G
⊢ HSMul.hSMul (α := G) (β := PlacedTile ps) 1
      { index := i,
        groupElts :=
          (↑gx :
            G ⧸
              Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
                ((↑ps : ιₚ → Prototile G X) i).symmetries) :
        PlacedTile ps } =
    { index := i,
      groupElts :=
        (↑gx :
          G ⧸
            Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
              ((↑ps : ιₚ → Prototile G X) i).symmetries) }

Tactic:
simp
-- 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
x : X
pt : PlacedTile ps
rw : g • x ∈ (↑(g • pt) : Set X) ↔ x ∈ pt
rw₁ : g • x ∈ g • (↑pt : Set X) ↔ x ∈ pt
rw₂ : x ∈ (↑pt : Set X) ↔ x ∈ pt
rw₃ rw₄ : x ∈ pt ↔ x ∈ pt
⊢ g • x ∈ g • pt ↔ x ∈ pt

Tactic:
rw [← mem_coe, coe_smul, Set.smul_mem_smul_set_iff, mem_coe]

Premises used: DiscreteTiling.PlacedTile.mem_coe, DiscreteTiling.PlacedTile.coe_smul, Set.smul_mem_smul_set_iff
-- 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
x : X
pt : PlacedTile ps
simp_rw : x ∈ (↑(g • pt) : Set X) ↔ g⁻¹ • x ∈ (↑pt : Set X)
simp_rw₁ : x ∈ g • (↑pt : Set X) ↔ g⁻¹ • x ∈ (↑pt : Set X)
⊢ x ∈ g • pt ↔ g⁻¹ • x ∈ pt

Tactic:
simp_rw [← mem_coe, coe_smul, Set.mem_smul_set_iff_inv_smul_mem]

Premises used: DiscreteTiling.PlacedTile.mem_coe, DiscreteTiling.PlacedTile.coe_smul, Set.mem_smul_set_iff_inv_smul_mem