awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
inst : DecidableEq α
w : α × Bool
g : FreeGroup α
hC_1 : 0 < g.toWord.length
h :
  (getElem (valid := fun (as : List (α × Bool)) (i : ℕ) ↦ i < as.length) g.toWord 0 hC_1).1 = w.1 →
    (getElem (valid := fun (as : List (α × Bool)) (i : ℕ) ↦ i < as.length) g.toWord 0 hC_1).2 = w.2
hC : True
pos :
  getElem? (coll := List (α × Bool)) (idx := ℕ) (valid := fun (as : List (α × Bool)) (i : ℕ) ↦ i < as.length)
      (List.rec (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) [w]
          (fun (head : α × Bool) (tail tail_ih : List (α × Bool)) ↦
            if w.1 = head.1 ∧ w.2 = !head.2 then tail else w :: head :: tail)
          (g.toWord.head ⋯ :: g.toWord.tail) :
        List (α × Bool))
      0 =
    some w
⊢ getElem? (coll := List (α × Bool)) (idx := ℕ) (valid := fun (as : List (α × Bool)) (i : ℕ) ↦ i < as.length)
      (List.rec (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) [w]
          (fun (head : α × Bool) (tail tail_ih : List (α × Bool)) ↦
            if w.1 = head.1 ∧ w.2 = !head.2 then tail else w :: head :: tail)
          g.toWord :
        List (α × Bool))
      0 =
    some w

Tactic:
rw [show g.toWord = g.toWord.head (by grind) :: g.toWord.tail by grind]
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
inst : DecidableEq α
w : α × Bool
g : FreeGroup α
hC_1 : 0 < g.toWord.length
h :
  (getElem (valid := fun (as : List (α × Bool)) (i : ℕ) ↦ i < as.length) g.toWord 0 hC_1).1 = w.1 →
    (getElem (valid := fun (as : List (α × Bool)) (i : ℕ) ↦ i < as.length) g.toWord 0 hC_1).2 = w.2
hC : True
⊢ getElem? (coll := List (α × Bool)) (idx := ℕ) (valid := fun (as : List (α × Bool)) (i : ℕ) ↦ i < as.length)
      (List.rec (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) [w]
          (fun (head : α × Bool) (tail tail_ih : List (α × Bool)) ↦
            if w.1 = head.1 ∧ w.2 = !head.2 then tail else w :: head :: tail)
          (g.toWord.head ⋯ :: g.toWord.tail) :
        List (α × Bool))
      0 =
    some w

Tactic:
grind
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
inst : DecidableEq α
w : α × Bool
g : FreeGroup α
h : g ∉ startsWith (w.1, !w.2)
hC : ¬0 < g.toWord.length
⊢ mk [w] * g ∈ startsWith w

Tactic:
simp_all [startsWith]

Premises used: FreeGroup.startsWith
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
w : α × Bool
g : (↑(startsWith w) : Type u_1)
x : X
⊢ g • x = (↑g : FreeGroup α) • x

Tactic:
rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
x : X
w : α × Bool
h :
  ∀ (i : X),
    Membership.mem (γ := Set X)
        {x_1 : X | ∃ y ∈ MulAction.orbit.{u_1, u_2} (↑(startsWith w) : Type u_1) x, (mk [w])⁻¹ • y = x_1} i ↔
      Membership.mem (γ := Set X)
        ((⋃ (v : α × Bool),
            ⋃ (_ : Membership.mem (γ := Set (α × Bool)) {z : α × Bool | z ≠ (w.1, !w.2)} v),
              MulAction.orbit.{u_1, u_2} (↑(startsWith v) : Type u_1) x) ∪
          {x})
        i
⊢ Eq (α := Set X) {x_1 : X | ∃ y ∈ MulAction.orbit.{u_1, u_2} (↑(startsWith w) : Type u_1) x, (mk [w])⁻¹ • y = x_1}
    ((⋃ (v : α × Bool),
        ⋃ (_ : Membership.mem (γ := Set (α × Bool)) {z : α × Bool | z ≠ (w.1, !w.2)} v),
          MulAction.orbit.{u_1, u_2} (↑(startsWith v) : Type u_1) x) ∪
      {x})

Tactic:
ext i
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
x : X
w : α × Bool
i : X
h :
  Membership.mem (γ := Set X)
      {x_1 : X | ∃ y ∈ MulAction.orbit.{u_1, u_2} (↑(startsWith w) : Type u_1) x, (mk [w])⁻¹ • y = x_1} i →
    Membership.mem (γ := Set X)
      ((⋃ (v : α × Bool),
          ⋃ (_ : Membership.mem (γ := Set (α × Bool)) {z : α × Bool | z ≠ (w.1, !w.2)} v),
            MulAction.orbit.{u_1, u_2} (↑(startsWith v) : Type u_1) x) ∪
        {x})
      i
h₁ :
  Membership.mem (γ := Set X)
      ((⋃ (v : α × Bool),
          ⋃ (_ : Membership.mem (γ := Set (α × Bool)) {z : α × Bool | z ≠ (w.1, !w.2)} v),
            MulAction.orbit.{u_1, u_2} (↑(startsWith v) : Type u_1) x) ∪
        {x})
      i →
    Membership.mem (γ := Set X)
      {x_1 : X | ∃ y ∈ MulAction.orbit.{u_1, u_2} (↑(startsWith w) : Type u_1) x, (mk [w])⁻¹ • y = x_1} i
⊢ Membership.mem (γ := Set X)
      {x_1 : X | ∃ y ∈ MulAction.orbit.{u_1, u_2} (↑(startsWith w) : Type u_1) x, (mk [w])⁻¹ • y = x_1} i ↔
    Membership.mem (γ := Set X)
      ((⋃ (v : α × Bool),
          ⋃ (_ : Membership.mem (γ := Set (α × Bool)) {z : α × Bool | z ≠ (w.1, !w.2)} v),
            MulAction.orbit.{u_1, u_2} (↑(startsWith v) : Type u_1) x) ∪
        {x})
      i

Tactic:
constructor
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
⊢ let l := g.toWord;
  l = g.toWord

Tactic:
set l := g.toWord with hl

Premises used: FreeGroup.toWord
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l : List (α × Bool) := g.toWord
hl : l = g.toWord
⊢ mk g.toWord ∈ startsWith w

Tactic:
simp [g.mk_toWord, hg]

Premises used: FreeGroup.mk_toWord
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l : List (α × Bool) := g.toWord
hl : l = g.toWord
⊢ Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) g hg =
    Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) (mk g.toWord) ⋯

Tactic:
simp [g.mk_toWord]

Premises used: FreeGroup.mk_toWord
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l : List (α × Bool) := g.toWord
hl : l = g.toWord
⊢ Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) g hg =
    Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) (mk g.toWord) ⋯

Tactic:
have h : (⟨g, hg⟩ : startsWith w) = ⟨mk g.toWord, by simp [g.mk_toWord, hg]⟩ := by
      simp [g.mk_toWord]
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l : List (α × Bool) := g.toWord
h :
  Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) g hg =
    Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) (mk g.toWord) ⋯
hl : [] = g.toWord
⊢ Membership.mem (γ := Set X)
    ((⋃ (v : α × Bool),
        ⋃ (_ : Membership.mem (γ := Set (α × Bool)) {z : α × Bool | z ≠ (w.1, !w.2)} v),
          MulAction.orbit.{u_1, u_2} (↑(startsWith v) : Type u_1) x) ∪
      {x})
    (HSMul.hSMul (β := X) (mk [w])⁻¹
      ((fun (m : (↑(startsWith w) : Type u_1)) ↦ m • x)
        (Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) g hg)))

Tactic:
simp [← hl, startsWith] at hg

Premises used: FreeGroup.startsWith
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l : List (α × Bool) := g.toWord
h :
  Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) g hg =
    Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) (mk g.toWord) ⋯
a : α × Bool
hl : [a] = g.toWord
⊢ a = w

Tactic:
simpa [← hl, startsWith] using hg

Premises used: FreeGroup.startsWith
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l : List (α × Bool) := g.toWord
h :
  Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) g hg =
    Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) (mk g.toWord) ⋯
a : α × Bool
hl : [a] = g.toWord
simp_rw :
  Membership.mem (γ := Set X)
    ((⋃ (v : α × Bool),
        ⋃ (_ : Membership.mem (γ := Set (α × Bool)) {z : α × Bool | z ≠ (w.1, !w.2)} v),
          MulAction.orbit.{u_1, u_2} (↑(startsWith v) : Type u_1) x) ∪
      {x})
    x
⊢ Membership.mem (γ := Set X)
    ((⋃ (v : α × Bool),
        ⋃ (_ : Membership.mem (γ := Set (α × Bool)) {z : α × Bool | z ≠ (w.1, !w.2)} v),
          MulAction.orbit.{u_1, u_2} (↑(startsWith v) : Type u_1) x) ∪
      {x})
    (HSMul.hSMul (β := X) (mk [w])⁻¹
      ((fun (m : (↑(startsWith w) : Type u_1)) ↦ m • x)
        (Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) g hg)))

Tactic:
simp_rw [h, ← hl, show a = w by simpa [← hl, startsWith] using hg, startsWith.smul_def,
        inv_smul_smul]

Premises used: inv_smul_smul, FreeGroup.startsWith.smul_def
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l : List (α × Bool) := g.toWord
h :
  Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) g hg =
    Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) (mk g.toWord) ⋯
a : α × Bool
hl : [a] = g.toWord
⊢ Membership.mem (γ := Set X)
    ((⋃ (v : α × Bool),
        ⋃ (_ : Membership.mem (γ := Set (α × Bool)) {z : α × Bool | z ≠ (w.1, !w.2)} v),
          MulAction.orbit.{u_1, u_2} (↑(startsWith v) : Type u_1) x) ∪
      {x})
    x

Tactic:
Or.inr rfl

Premises used: Set.union, Set.Mem, setOf, Or.inr, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l : List (α × Bool) := g.toWord
h :
  Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) g hg =
    Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) (mk g.toWord) ⋯
a : α × Bool
hl : [a] = g.toWord
⊢ Membership.mem (γ := Set X)
    ((⋃ (v : α × Bool),
        ⋃ (_ : Membership.mem (γ := Set (α × Bool)) {z : α × Bool | z ≠ (w.1, !w.2)} v),
          MulAction.orbit.{u_1, u_2} (↑(startsWith v) : Type u_1) x) ∪
      {x})
    x

Tactic:
exact Or.inr rfl

Premises used: Or.inr, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l_1 : List (α × Bool) := g.toWord
h :
  Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) g hg =
    Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) (mk g.toWord) ⋯
a b : α × Bool
l : List (α × Bool)
hl : a :: b :: l = g.toWord
⊢ a = w

Tactic:
simpa [← hl, startsWith] using hg

Premises used: FreeGroup.startsWith
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l_1 : List (α × Bool) := g.toWord
h :
  Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) g hg =
    Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) (mk g.toWord) ⋯
a b : α × Bool
l : List (α × Bool)
hl : a :: b :: l = g.toWord
⊢ a = w

Tactic:
have ha : a = w := by simpa [← hl, startsWith] using hg
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l_1 : List (α × Bool) := g.toWord
h :
  Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) g hg =
    Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) (mk g.toWord) ⋯
a b : α × Bool
l : List (α × Bool)
hl : a :: b :: l = g.toWord
ha : a = w
⊢ (a.1 = b.1 → a.2 = b.2) ∧ IsReduced (b :: l)

Tactic:
have h1 := isReduced_cons_cons.mp (hl ▸ isReduced_toWord)
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l_1 : List (α × Bool) := g.toWord
h :
  Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) g hg =
    Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) (mk g.toWord) ⋯
a b : α × Bool
l : List (α × Bool)
hl : a :: b :: l = g.toWord
ha : a = w
h1 : (a.1 = b.1 → a.2 = b.2) ∧ IsReduced (b :: l)
⊢ Membership.mem (γ := Set (α × Bool)) {z : α × Bool | z ≠ (w.1, !w.2)} b

Tactic:
grind
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l_1 : List (α × Bool) := g.toWord
h :
  Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) g hg =
    Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) (mk g.toWord) ⋯
a b : α × Bool
l : List (α × Bool)
hl : a :: b :: l = g.toWord
ha : a = w
h1 : (a.1 = b.1 → a.2 = b.2) ∧ IsReduced (b :: l)
refine :
  HSMul.hSMul (β := X) (mk [w])⁻¹
      ((fun (m : (↑(startsWith w) : Type u_1)) ↦ m • x)
        (Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) g hg)) ∈
    MulAction.orbit.{u_1, u_2} (↑(startsWith b) : Type u_1) x
⊢ Membership.mem (γ := Set X)
    ((⋃ (v : α × Bool),
        ⋃ (_ : Membership.mem (γ := Set (α × Bool)) {z : α × Bool | z ≠ (w.1, !w.2)} v),
          MulAction.orbit.{u_1, u_2} (↑(startsWith v) : Type u_1) x) ∪
      {x})
    (HSMul.hSMul (β := X) (mk [w])⁻¹
      ((fun (m : (↑(startsWith w) : Type u_1)) ↦ m • x)
        (Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) g hg)))

Tactic:
refine Or.inl (Set.mem_biUnion (x := b) (by grind) ?_)

Premises used: Set.mem_biUnion, Or.inl
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l_1 : List (α × Bool) := g.toWord
h :
  Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) g hg =
    Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) (mk g.toWord) ⋯
a b : α × Bool
l : List (α × Bool)
hl : a :: b :: l = g.toWord
ha : a = w
h1 : (a.1 = b.1 → a.2 = b.2) ∧ IsReduced (b :: l)
simp_rw : mk (b :: l) • x ∈ MulAction.orbit.{u_1, u_2} (↑(startsWith b) : Type u_1) x
⊢ HSMul.hSMul (β := X) (mk [w])⁻¹
      ((fun (m : (↑(startsWith w) : Type u_1)) ↦ m • x)
        (Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) g hg)) ∈
    MulAction.orbit.{u_1, u_2} (↑(startsWith b) : Type u_1) x

Tactic:
simp_rw [h, ← hl, ha, ← List.singleton_append (l := b :: l), ← mul_mk, startsWith.smul_def,
        mul_smul, inv_smul_smul]

Premises used: inv_smul_smul, List.singleton_append, FreeGroup.mul_mk, FreeGroup.startsWith.smul_def, SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l_1 : List (α × Bool) := g.toWord
h :
  Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) g hg =
    Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) (mk g.toWord) ⋯
a b : α × Bool
l : List (α × Bool)
hl : a :: b :: l = g.toWord
ha : a = w
h1 : (a.1 = b.1 → a.2 = b.2) ∧ IsReduced (b :: l)
⊢ mk (b :: l) ∈ startsWith b

Tactic:
simp [startsWith, h1.2.reduce_eq]

Premises used: FreeGroup.IsReduced.reduce_eq, And.right, FreeGroup.startsWith
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l_1 : List (α × Bool) := g.toWord
h :
  Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) g hg =
    Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) (mk g.toWord) ⋯
a b : α × Bool
l : List (α × Bool)
hl : a :: b :: l = g.toWord
ha : a = w
h1 : (a.1 = b.1 → a.2 = b.2) ∧ IsReduced (b :: l)
⊢ mk (b :: l) • x ∈ MulAction.orbit.{u_1, u_2} (↑(startsWith b) : Type u_1) x

Tactic:
exact ⟨⟨mk (b :: l), by simp [startsWith, h1.2.reduce_eq]⟩, rfl⟩
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l : List (α × Bool) := g.toWord
hl : l = g.toWord
h :
  Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) g hg =
    Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) (mk g.toWord) ⋯
⊢ Membership.mem (γ := Set X)
    ((⋃ (v : α × Bool),
        ⋃ (_ : Membership.mem (γ := Set (α × Bool)) {z : α × Bool | z ≠ (w.1, !w.2)} v),
          MulAction.orbit.{u_1, u_2} (↑(startsWith v) : Type u_1) x) ∪
      {x})
    (HSMul.hSMul (β := X) (mk [w])⁻¹
      ((fun (m : (↑(startsWith w) : Type u_1)) ↦ m • x)
        (Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) g hg)))

Tactic:
match l with
    | [] => simp [← hl, startsWith] at hg
    | [a] =>
      simp_rw [h, ← hl, show a = w by simpa [← hl, startsWith] using hg, startsWith.smul_def,
        inv_smul_smul]
      exact Or.inr rfl
    | a :: b :: l =>
      have ha : a = w := by simpa [← hl, startsWith] using hg
      have h1 := isReduced_cons_cons.mp (hl ▸ isReduced_toWord)
      refine Or.inl (Set.mem_biUnion (x := b) (by grind) ?_)
      simp_rw [h, ← hl, ha, ← List.singleton_append (l := b :: l), ← mul_mk, startsWith.smul_def,
        mul_smul, inv_smul_smul]
      exact ⟨⟨mk (b :: l), by simp [startsWith, h1.2.reduce_eq]⟩, rfl⟩
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
x : X
w w' : α × Bool
hw : Membership.mem (γ := Set (α × Bool)) {z : α × Bool | z ≠ (w.1, !w.2)} w'
g : FreeGroup α
hg : g ∈ startsWith w'
⊢ Membership.mem (γ := Set X)
    {x_1 : X | ∃ y ∈ MulAction.orbit.{u_1, u_2} (↑(startsWith w) : Type u_1) x, (mk [w])⁻¹ • y = x_1}
    ((fun (m : (↑(startsWith w') : Type u_1)) ↦ m • x)
      (Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w') g hg))

Tactic:
⟨mk [w] • g • x, ⟨⟨mk [w] * g, startsWith_mk_mul g
        ((startsWith.disjoint_iff_ne.mpr hw).notMem_of_mem_left hg)⟩,
        mul_smul (mk [w]) g x⟩, inv_smul_smul (mk [w]) (g • x)⟩

Premises used: Iff.mpr, HMul.hMul, Set.Mem, setOf, FreeGroup.startsWith_mk_mul, inv_smul_smul, List.cons, Subtype.mk, FreeGroup.startsWith.disjoint_iff_ne, And.intro, FreeGroup.mk, Exists.intro, Disjoint.notMem_of_mem_left, HSMul.hSMul, SemigroupAction.mul_smul, List.nil
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
x : X
w w' : α × Bool
hw : Membership.mem (γ := Set (α × Bool)) {z : α × Bool | z ≠ (w.1, !w.2)} w'
g : FreeGroup α
hg : g ∈ startsWith w'
⊢ Membership.mem (γ := Set X)
    {x_1 : X | ∃ y ∈ MulAction.orbit.{u_1, u_2} (↑(startsWith w) : Type u_1) x, (mk [w])⁻¹ • y = x_1}
    ((fun (m : (↑(startsWith w') : Type u_1)) ↦ m • x)
      (Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w') g hg))

Tactic:
exact ⟨mk [w] • g • x, ⟨⟨mk [w] * g, startsWith_mk_mul g
        ((startsWith.disjoint_iff_ne.mpr hw).notMem_of_mem_left hg)⟩,
        mul_smul (mk [w]) g x⟩, inv_smul_smul (mk [w]) (g • x)⟩
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
w : α × Bool
i : X
⊢ Membership.mem (γ := Set X)
    {x : X | ∃ y ∈ MulAction.orbit.{u_1, u_2} (↑(startsWith w) : Type u_1) i, (mk [w])⁻¹ • y = x} i

Tactic:
⟨mk [w] • i, ⟨⟨mk [w], rfl⟩, rfl⟩, inv_smul_smul (mk [w]) i⟩

Premises used: Set.Mem, setOf, inv_smul_smul, List.cons, Subtype.mk, And.intro, FreeGroup.mk, Exists.intro, HSMul.hSMul, rfl, List.nil
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
w : α × Bool
i : X
⊢ Membership.mem (γ := Set X)
    {x : X | ∃ y ∈ MulAction.orbit.{u_1, u_2} (↑(startsWith w) : Type u_1) i, (mk [w])⁻¹ • y = x} i

Tactic:
exact ⟨mk [w] • i, ⟨⟨mk [w], rfl⟩, rfl⟩, inv_smul_smul (mk [w]) i⟩
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Eq.{u_1 + 1} (α := List (α × Bool)) (reduce []) []

Tactic:
rfl

Premises used: FreeGroup.reduce, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
s : α × Bool
⊢ reduce [s] = [s]

Tactic:
rfl

Premises used: FreeGroup.reduce, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
x : α × Bool
⊢ reduce (x :: L) =
    List.casesOn (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) (reduce L) [x]
      fun (hd : α × Bool) (tl : List (α × Bool)) ↦ if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl

Tactic:
rfl

Premises used: FreeGroup.reduce, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x : α × Bool
⊢ reduce (List.replicate 0 x) = List.replicate 0 x

Tactic:
simp [reduce]

Premises used: FreeGroup.reduce
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x : α × Bool
n : ℕ
ih : reduce (List.replicate n x) = List.replicate n x
succ :
  (List.casesOn (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) (List.replicate n x) [x]
      fun (hd : α × Bool) (tl : List (α × Bool)) ↦ if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl) =
    x :: List.replicate n x
⊢ reduce (List.replicate (n + 1) x) = List.replicate (n + 1) x

Tactic:
rw [List.replicate_succ, reduce.cons, ih]

Premises used: FreeGroup.reduce.cons, List.replicate_succ
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x : α × Bool
ih : reduce (List.replicate 0 x) = List.replicate 0 x
⊢ (List.casesOn (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) (List.replicate 0 x) [x]
      fun (hd : α × Bool) (tl : List (α × Bool)) ↦ if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl) =
    x :: List.replicate 0 x

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x : α × Bool
n : ℕ
ih : reduce (List.replicate (n + 1) x) = List.replicate (n + 1) x
⊢ (List.casesOn (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) (List.replicate (n + 1) x) [x]
      fun (hd : α × Bool) (tl : List (α × Bool)) ↦ if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl) =
    x :: List.replicate (n + 1) x

Tactic:
simp [List.replicate_succ]

Premises used: List.replicate_succ
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x : α × Bool
n : ℕ
ih : reduce (List.replicate n x) = List.replicate n x
succ :
  ∀ (ih : reduce (List.replicate 0 x) = List.replicate 0 x),
    (List.casesOn (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) (List.replicate 0 x) [x]
        fun (hd : α × Bool) (tl : List (α × Bool)) ↦ if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl) =
      x :: List.replicate 0 x
succ₁ :
  ∀ (n : ℕ) (ih : reduce (List.replicate (n + 1) x) = List.replicate (n + 1) x),
    (List.casesOn (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) (List.replicate (n + 1) x) [x]
        fun (hd : α × Bool) (tl : List (α × Bool)) ↦ if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl) =
      x :: List.replicate (n + 1) x
⊢ (List.casesOn (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) (List.replicate n x) [x]
      fun (hd : α × Bool) (tl : List (α × Bool)) ↦ if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl) =
    x :: List.replicate n x

Tactic:
cases n with
    | zero => simp
    | succ n => simp [List.replicate_succ]

Premises used: List.replicate_succ