awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ιₚ
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 := i₁, groupElts := g₂ }
have refine_2 : { index := i₁, groupElts := g₁ : PlacedTile ps }.index = { index := i₁, groupElts := g₂ : PlacedTile ps }.index
Tactic: ext
-- 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 ιₚ
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
⊢ { index := i₁, groupElts := g₁ : PlacedTile ps } = { index := i₁, groupElts := g₂ }
have refine_2₁ : { index := i₁, groupElts := g₁ : PlacedTile ps }.groupElts ≍ { index := i₁, groupElts := g₂ : PlacedTile ps }.groupElts
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Tiling.Tile (hypothesis)
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
⊢ Eq.{u_2 + 1} (α := Set X) ((fun (g : G) ↦ g • (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X)) a)
    ((fun (g : G) ↦ g • (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X)) b)
have 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
Tactic: rw [QuotientGroup.leftRel_eq] at r
Cleared hypotheses: r
-- 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 ιₚ
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
⊢ a • (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X) = b • (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X)
have rw : Membership.mem (γ := Subgroup G) (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X)) (a⁻¹ * b)
Tactic: rw [eq_comm, ← inv_smul_eq_iff, smul_smul, ← MulAction.mem_stabilizer_iff]
-- 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 ιₚ
pt : PlacedTile ps
⊢ (↑pt : Set X).Nonempty ↔ (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X).Nonempty
have 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
Tactic: rcases pt with ⟨index, groupElts⟩
Cleared hypotheses: pt
-- 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 ιₚ
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
have simp : Set.Nonempty.{u_2} (α := X)
    (Quotient.liftOn' groupElts (fun (g : G) ↦ g • (↑((↑ps : ιₚ → Prototile G X) index) : Set X)) sorry) ↔
  (↑((↑ps : ιₚ → Prototile G X) index) : Set X).Nonempty
Tactic: simp only [coeSet]
-- 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 ιₚ
index : ιₚ
groupElts :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) index) : Set X)))
      ((↑ps : ιₚ → Prototile G X) index).symmetries
⊢ 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
have rw : (Quotient.out groupElts • (↑((↑ps : ιₚ → Prototile G X) index) : Set X)).Nonempty ↔
  (↑((↑ps : ιₚ → Prototile G X) index) : Set X).Nonempty
Tactic: rw [← groupElts.out_eq', Quotient.liftOn'_mk'']
-- 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 ιₚ
pt : PlacedTile ps
⊢ (↑pt : Set X).Finite ↔ (↑((↑ps : ιₚ → Prototile G X) pt.index) : Set X).Finite
have 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
Tactic: rcases pt with ⟨index, groupElts⟩
Cleared hypotheses: pt
-- 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 ιₚ
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
have simp : Set.Finite.{u_2} (α := X)
    (Quotient.liftOn' groupElts (fun (g : G) ↦ g • (↑((↑ps : ιₚ → Prototile G X) index) : Set X)) sorry) ↔
  (↑((↑ps : ιₚ → Prototile G X) index) : Set X).Finite
Tactic: simp only [coeSet]
-- 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 ιₚ
index : ιₚ
groupElts :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) index) : Set X)))
      ((↑ps : ιₚ → Prototile G X) index).symmetries
⊢ 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
have rw : (Quotient.out groupElts • (↑((↑ps : ιₚ → Prototile G X) index) : Set X)).Finite ↔
  (↑((↑ps : ιₚ → Prototile G X) index) : Set X).Finite
Tactic: rw [← groupElts.out_eq', Quotient.liftOn'_mk'']
-- Lean 4 proof step from Mathlib.Combinatorics.Tiling.Tile (hypothesis)
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
⊢ 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 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
Tactic: rw [QuotientGroup.leftRel_eq] at r
Cleared hypotheses: r
-- 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
⊢ (g • pt).index = pt.index
have 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) }
Tactic: induction pt using PlacedTile.induction_on
Cleared hypotheses: pt
-- 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
⊢ (↑(g • pt) : Set X) = g • (↑pt : Set X)
have 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)
Tactic: induction pt using PlacedTile.induction_on
Cleared hypotheses: pt
-- 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 ιₚ
x y : G
pt : PlacedTile ps
⊢ (x * y) • pt = x • y • pt
have 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 }
Tactic: induction pt using PlacedTile.induction_on
Cleared hypotheses: pt
-- 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 ιₚ
pt : PlacedTile ps
⊢ HSMul.hSMul (α := G) 1 pt = pt
have 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) }
Tactic: induction pt using PlacedTile.induction_on
Cleared hypotheses: pt
-- 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
x : X
pt : PlacedTile ps
⊢ g • x ∈ g • pt ↔ x ∈ pt
have rw : g • x ∈ (↑(g • pt) : Set X) ↔ x ∈ pt
Tactic: rw [← mem_coe, coe_smul, Set.smul_mem_smul_set_iff, mem_coe]
-- 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
x : X
pt : PlacedTile ps
rw : g • x ∈ (↑(g • pt) : Set X) ↔ x ∈ pt
⊢ g • x ∈ g • pt ↔ x ∈ pt
have rw₁ : g • x ∈ g • (↑pt : Set X) ↔ x ∈ pt
Tactic: rw [← mem_coe, coe_smul, Set.smul_mem_smul_set_iff, mem_coe]
-- 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
x : X
pt : PlacedTile ps
rw : g • x ∈ (↑(g • pt) : Set X) ↔ x ∈ pt
rw₁ : g • x ∈ g • (↑pt : Set X) ↔ x ∈ pt
⊢ g • x ∈ g • pt ↔ x ∈ pt
have rw₂ : x ∈ (↑pt : Set X) ↔ x ∈ pt
Tactic: rw [← mem_coe, coe_smul, Set.smul_mem_smul_set_iff, mem_coe]
-- 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
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
⊢ g • x ∈ g • pt ↔ x ∈ pt
have rw₃ : x ∈ pt ↔ x ∈ pt
Tactic: rw [← mem_coe, coe_smul, Set.smul_mem_smul_set_iff, mem_coe]
-- 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
x : X
pt : PlacedTile ps
⊢ x ∈ g • pt ↔ g⁻¹ • x ∈ pt
have simp_rw : x ∈ (↑(g • pt) : Set X) ↔ g⁻¹ • x ∈ (↑pt : Set X)
Tactic: simp_rw [← mem_coe, coe_smul, Set.mem_smul_set_iff_inv_smul_mem]
-- 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
x : X
pt : PlacedTile ps
simp_rw : x ∈ (↑(g • pt) : Set X) ↔ g⁻¹ • x ∈ (↑pt : Set X)
⊢ x ∈ g • pt ↔ g⁻¹ • x ∈ pt
have simp_rw₁ : x ∈ g • (↑pt : Set X) ↔ g⁻¹ • x ∈ (↑pt : Set X)
Tactic: simp_rw [← mem_coe, coe_smul, Set.mem_smul_set_iff_inv_smul_mem]
-- 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
x : X
pt : PlacedTile ps
⊢ x ∈ g⁻¹ • pt ↔ g • x ∈ pt
have simp_rw : x ∈ (↑(g⁻¹ • pt) : Set X) ↔ g • x ∈ (↑pt : Set X)
Tactic: simp_rw [← mem_coe, coe_smul, Set.mem_inv_smul_set_iff]
-- 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
x : X
pt : PlacedTile ps
simp_rw : x ∈ (↑(g⁻¹ • pt) : Set X) ↔ g • x ∈ (↑pt : Set X)
⊢ x ∈ g⁻¹ • pt ↔ g • x ∈ pt
have simp_rw₁ : x ∈ g⁻¹ • (↑pt : Set X) ↔ g • x ∈ (↑pt : Set X)
Tactic: simp_rw [← mem_coe, coe_smul, Set.mem_inv_smul_set_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Young.SemistandardTableau (goal)
Goal:
μ : YoungDiagram
T T' : SemistandardYoungTableau μ
h : T.entry = T'.entry
⊢ T = T'
have mk : ∀ (entry : ℕ → ℕ → ℕ) (row_weak' : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry i j1 ≤ entry i j2)
  (col_strict' : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry i1 j < entry i2 j)
  (zeros' : ∀ {i j : ℕ}, (i, j) ∉ μ → entry i j = 0)
  (h :
    { entry := entry, row_weak' := @row_weak', col_strict' := @col_strict', zeros' := @zeros' :
          SemistandardYoungTableau μ }.entry =
      T'.entry),
  { entry := entry, row_weak' := @row_weak', col_strict' := @col_strict', zeros' := @zeros' :
      SemistandardYoungTableau μ } =
    T'
Tactic: cases T
Cleared hypotheses: T, h
-- Lean 4 proof step from Mathlib.Combinatorics.Young.SemistandardTableau (goal)
Goal:
μ : YoungDiagram
T' : SemistandardYoungTableau μ
entry : ℕ → ℕ → ℕ
row_weak' : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry i j1 ≤ entry i j2
col_strict' : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry i1 j < entry i2 j
zeros' : ∀ {i j : ℕ}, (i, j) ∉ μ → entry i j = 0
h :
  { entry := entry, row_weak' := @row_weak', col_strict' := @col_strict', zeros' := @zeros' :
        SemistandardYoungTableau μ }.entry =
    T'.entry
⊢ { entry := entry, row_weak' := @row_weak', col_strict' := @col_strict', zeros' := @zeros' :
      SemistandardYoungTableau μ } =
    T'
have mk : ∀ (entry_1 : ℕ → ℕ → ℕ) (row_weak'_1 : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry_1 i j1 ≤ entry_1 i j2)
  (col_strict'_1 : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry_1 i1 j < entry_1 i2 j)
  (zeros'_1 : ∀ {i j : ℕ}, (i, j) ∉ μ → entry_1 i j = 0)
  (h :
    { entry := entry, row_weak' := @row_weak', col_strict' := @col_strict', zeros' := @zeros' :
          SemistandardYoungTableau μ }.entry =
      { entry := entry_1, row_weak' := @row_weak'_1, col_strict' := @col_strict'_1, zeros' := @zeros'_1 :
          SemistandardYoungTableau μ }.entry),
  { entry := entry, row_weak' := @row_weak', col_strict' := @col_strict', zeros' := @zeros' :
      SemistandardYoungTableau μ } =
    { entry := entry_1, row_weak' := @row_weak'_1, col_strict' := @col_strict'_1, zeros' := @zeros'_1 }
Tactic: cases T'
Cleared hypotheses: T', h
-- Lean 4 proof step from Mathlib.Combinatorics.Young.SemistandardTableau (goal)
Goal:
μ : YoungDiagram
T T' : SemistandardYoungTableau μ
h : ∀ (i j : ℕ), Eq (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j : ℕ) ((T' : (a : ℕ) → ℕ → ℕ) i j : ℕ)
x : ℕ
⊢ Eq (α := ℕ → ℕ) ((T : (a : ℕ) → ℕ → ℕ) x : ℕ → ℕ) ((T' : (a : ℕ) → ℕ → ℕ) x : ℕ → ℕ)
have h₁ : ∀ (x_1 : ℕ), Eq (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) x x_1 : ℕ) ((T' : (a : ℕ) → ℕ → ℕ) x x_1 : ℕ)
Tactic: funext
-- Lean 4 proof step from Mathlib.Combinatorics.Young.SemistandardTableau (goal)
Goal:
μ : YoungDiagram
T : SemistandardYoungTableau μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
⊢ LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j1 : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j2 : ℕ)
have inl : ∀ (h : j1 = j2), LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j1 : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j2 : ℕ)
Tactic: rcases eq_or_lt_of_le hj with h | h
-- Lean 4 proof step from Mathlib.Combinatorics.Young.SemistandardTableau (goal)
Goal:
μ : YoungDiagram
T : SemistandardYoungTableau μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
inl : ∀ (h : j1 = j2), LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j1 : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j2 : ℕ)
⊢ LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j1 : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j2 : ℕ)
have inr : ∀ (h : j1 < j2), LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j1 : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j2 : ℕ)
Tactic: rcases eq_or_lt_of_le hj with h | h
-- Lean 4 proof step from Mathlib.Combinatorics.Young.SemistandardTableau (goal)
Goal:
μ : YoungDiagram
T : SemistandardYoungTableau μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 = j2
⊢ LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j1 : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j2 : ℕ)
have inl : LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j2 : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j2 : ℕ)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Combinatorics.Young.SemistandardTableau (goal)
Goal:
μ : YoungDiagram
T : SemistandardYoungTableau μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
⊢ LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i1 j : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i2 j : ℕ)
have inl : ∀ (h : i1 = i2), LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i1 j : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i2 j : ℕ)
Tactic: rcases eq_or_lt_of_le hi with h | h