awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst_2 : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst_3 : Group X
f :
  (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
            (wideSubquiverSymmetrify T))ᶜ :
      Type u) →
    X
f' : Labelling (Generators G) X :=
  fun (a b : Generators G) (e : a ⟶ b) ↦
    if h : e ∈ wideSubquiverSymmetrify T a b then 1
    else
      f
        (Subtype.mk (p := fun (x : Quiver.Total (Generators G)) ↦
          Membership.mem (γ := Set (Quiver.Total (Generators G)))
            (((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
                  (wideSubquiverSymmetrify T))ᶜ :
              Set (Quiver.Total (Generators G)))
            x)
          { left := a, right := b, hom := e } h)
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X),
    (fun (F : G ⥤ CategoryTheory.SingleObj X) ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (root' T) →* X
hE :
  ∀
    (a :
      (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
              (wideSubquiverSymmetrify T))ᶜ :
        Type u)),
    (E : (a : End (root' T)) → X)
        ((fun
              (e :
                (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
                        (wideSubquiverSymmetrify T))ᶜ :
                  Type u)) ↦
            (loopOfHom T (of (↑e : Quiver.Total (Generators G)).hom) : End (root' T)))
          a) =
      f a
x : End (root' T)
a b : Generators G
e : a ⟶ b
h : e ∈ wideSubquiverSymmetrify T a b
pos : Eq (α := X) ((E : (a : End (root' T)) → X) (𝟙 (root' T)) : X) (1 : X)
⊢ Eq (α := X) ((E : (a : End (root' T)) → X) (loopOfHom T (of e)) : X) (1 : X)
have pos₁ : Eq (α := X) ((E : (a : End (root' T)) → X) 1 : X) (1 : X)
Tactic: rw [loopOfHom_eq_id T e h, ← End.one_def, E.map_one]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst_2 : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst_3 : Group X
f :
  (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
            (wideSubquiverSymmetrify T))ᶜ :
      Type u) →
    X
f' : Labelling (Generators G) X :=
  fun (a b : Generators G) (e : a ⟶ b) ↦
    if h : e ∈ wideSubquiverSymmetrify T a b then 1
    else
      f
        (Subtype.mk (p := fun (x : Quiver.Total (Generators G)) ↦
          Membership.mem (γ := Set (Quiver.Total (Generators G)))
            (((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
                  (wideSubquiverSymmetrify T))ᶜ :
              Set (Quiver.Total (Generators G)))
            x)
          { left := a, right := b, hom := e } h)
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X),
    (fun (F : G ⥤ CategoryTheory.SingleObj X) ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (root' T) →* X
hE :
  ∀
    (a :
      (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
              (wideSubquiverSymmetrify T))ᶜ :
        Type u)),
    (E : (a : End (root' T)) → X)
        ((fun
              (e :
                (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
                        (wideSubquiverSymmetrify T))ᶜ :
                  Type u)) ↦
            (loopOfHom T (of (↑e : Quiver.Total (Generators G)).hom) : End (root' T)))
          a) =
      f a
x : End (root' T)
a b : Generators G
e : a ⟶ b
h : e ∈ wideSubquiverSymmetrify T a b
pos : Eq (α := X) ((E : (a : End (root' T)) → X) (𝟙 (root' T)) : X) (1 : X)
pos₁ : Eq (α := X) ((E : (a : End (root' T)) → X) 1 : X) (1 : X)
⊢ Eq (α := X) ((E : (a : End (root' T)) → X) (loopOfHom T (of e)) : X) (1 : X)
have pos₂ : Eq.{u + 1} (α := X) 1 1
Tactic: rw [loopOfHom_eq_id T e h, ← End.one_def, E.map_one]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsFreeGroupoid G
a b : G
p : a ⟶ b
⊢ Nonempty.{u + 1} (Path (V := Symmetrify (Generators G)) (symgen a) (symgen b))
have rw : HMul.hMul (α := FreeGroup (WeaklyConnectedComponent (Generators G)))
    (FreeGroup.of (WeaklyConnectedComponent.mk (symgen b))) (FreeGroup.of (WeaklyConnectedComponent.mk (symgen a)))⁻¹ =
  1
Tactic: rw [← @WeaklyConnectedComponent.eq (Generators G), eq_comm, ← FreeGroup.of_injective.eq_iff, ←
    mul_inv_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun (g : G) ↦ FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
⊢ HMul.hMul (α := FreeGroup (WeaklyConnectedComponent (Generators G)))
      (FreeGroup.of (WeaklyConnectedComponent.mk (symgen b)))
      (FreeGroup.of (WeaklyConnectedComponent.mk (symgen a)))⁻¹ =
    1
have change : F.map p = CategoryTheory.Functor.map (Functor.obj (Functor.const G) ()) p
Tactic: change (F.map p) = ((@CategoryTheory.Functor.const G _ _ (SingleObj.category X)).obj ()).map p
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun (g : G) ↦ FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
⊢ F.map p = CategoryTheory.Functor.map (Functor.obj (Functor.const G) ()) p
have h : F = Functor.obj (Functor.const G) ()
Tactic: congr
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun (g : G) ↦ FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
⊢ F = Functor.obj (Functor.const G) ()
have h : ∀ (a b : Generators G) (e : a ⟶ b), F.map (of e) = CategoryTheory.Functor.map (Functor.obj (Functor.const G) ()) (of e)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun (g : G) ↦ FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
a_1 b_1 : Generators G
e : a_1 ⟶ b_1
⊢ F.map (of e) = CategoryTheory.Functor.map (Functor.obj (Functor.const G) ()) (of e)
have h : f b_1 =
  f
    (have this := a_1;
    this)
Tactic: rw [Functor.const_obj_map, id_as_one, differenceFunctor_map, @mul_inv_eq_one _ _ (f _)]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun (g : G) ↦ FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
a_1 b_1 : Generators G
e : a_1 ⟶ b_1
⊢ f b_1 =
    f
      (have this := a_1;
      this)
have h : Eq (α := WeaklyConnectedComponent (Generators G)) (WeaklyConnectedComponent.mk b_1)
  (WeaklyConnectedComponent.mk
    (have this := a_1;
    this))
Tactic: apply congr_arg FreeGroup.of
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun (g : G) ↦ FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
a_1 b_1 : Generators G
e : a_1 ⟶ b_1
⊢ Eq (α := WeaklyConnectedComponent (Generators G)) (WeaklyConnectedComponent.mk b_1)
    (WeaklyConnectedComponent.mk
      (have this := a_1;
      this))
have h : Nonempty.{u + 1}
  (Path b_1
    (have this := a_1;
    this))
Tactic: apply (WeaklyConnectedComponent.eq _ _).mpr
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Orbit (goal)
Goal:
α : Type u_1
inst : DecidableEq α
w w' : α × Bool
⊢ Disjoint (startsWith w) (startsWith w') ↔ w ≠ w'
have simp_all : (∀ (x : FreeGroup α),
    getElem? (valid := fun (as : List (α × Bool)) (i : ℕ) ↦ i < as.length) x.toWord 0 = some w → ¬w = w') ↔
  ¬w = w'
Tactic: simp_all only [ne_eq, startsWith, Set.disjoint_iff_inter_eq_empty, Set.ext_iff, Set.mem_inter_iff,
    Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false, not_and, Option.some.injEq]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Orbit (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
a b : α × Bool
h : startsWith a = startsWith b
⊢ a = b
have h₁ : ∀ (x : FreeGroup α),
  getElem? (valid := fun (as : List (α × Bool)) (i : ℕ) ↦ i < as.length) x.toWord 0 = some a ↔
    getElem? (valid := fun (as : List (α × Bool)) (i : ℕ) ↦ i < as.length) x.toWord 0 = some b
Tactic: simp only [startsWith, Set.ext_iff, Set.mem_setOf_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Orbit (goal)
Goal:
α : Type u_1
inst : DecidableEq α
w : α × Bool
g : FreeGroup α
h : g ∉ startsWith (w.1, !w.2)
⊢ mk [w] * g ∈ startsWith w
have pos : ∀ (hC : 0 < g.toWord.length), mk [w] * g ∈ startsWith w
Tactic: by_cases hC : 0 < g.toWord.length
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Orbit (goal)
Goal:
α : Type u_1
inst : DecidableEq α
w : α × Bool
g : FreeGroup α
h : g ∉ startsWith (w.1, !w.2)
pos : ∀ (hC : 0 < g.toWord.length), mk [w] * g ∈ startsWith w
⊢ mk [w] * g ∈ startsWith w
have neg : ∀ (hC : ¬0 < g.toWord.length), mk [w] * g ∈ startsWith w
Tactic: by_cases hC : 0 < g.toWord.length
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Orbit (goal)
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
have pos : ∀
  (h :
    (getElem (valid := fun (as : List (α × Bool)) (i : ℕ) ↦ i < as.length) g.toWord 0 hC).1 = w.1 →
      (getElem (valid := fun (as : List (α × Bool)) (i : ℕ) ↦ i < as.length) g.toWord 0 hC).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 :
        List (α × Bool))
      0 =
    some w
Tactic: simp only [startsWith, Set.mem_setOf_eq, getElem?_pos, Option.some.injEq,
      Prod.eq_iff_fst_eq_snd_eq, not_and, Bool.not_eq_not, toWord_mul, toWord_mk, reduce.cons,
      reduce_nil, List.cons_append, List.nil_append, reduce_toWord, hC] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Orbit (goal)
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 :
        List (α × Bool))
      0 =
    some w
have 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 sorry :: g.toWord.tail) :
      List (α × Bool))
    0 =
  some w
Tactic: rw [show g.toWord = g.toWord.head (by grind) :: g.toWord.tail by grind]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Orbit (goal)
Goal:
α : Type u_1
X : Type u_2
inst : DecidableEq α
inst_1 : MulAction.{u_1, u_2} (FreeGroup α) X
x : X
w : α × Bool
⊢ 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})
have 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
Tactic: ext i
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Orbit (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Orbit (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Orbit (hypothesis)
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
⊢ 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)))
have hl : let l := g.toWord;
l = g.toWord
Tactic: set l := g.toWord with hl
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Orbit (hypothesis)
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
⊢ 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)))
have h : Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) g hg =
  Subtype.mk (p := fun (x : FreeGroup α) ↦ x ∈ startsWith w) (mk g.toWord) sorry
Tactic: have h : (⟨g, hg⟩ : startsWith w) = ⟨mk g.toWord, by simp [g.mk_toWord, hg]⟩ := by
      simp [g.mk_toWord]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Orbit (goal)
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})
    (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)))
have 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
Tactic: simp_rw [h, ← hl, show a = w by simpa [← hl, startsWith] using hg, startsWith.smul_def,
        inv_smul_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Orbit (hypothesis)
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
⊢ 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)))
have ha : a = w
Tactic: have ha : a = w := by simpa [← hl, startsWith] using hg
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Orbit (hypothesis)
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
⊢ 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)))
have h1 : (a.1 = b.1 → a.2 = b.2) ∧ IsReduced (b :: l)
Tactic: have h1 := isReduced_cons_cons.mp (hl ▸ isReduced_toWord)
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Orbit (goal)
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 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)))
have 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
Tactic: refine Or.inl (Set.mem_biUnion (x := b) (by grind) ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Orbit (goal)
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)
⊢ 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
have simp_rw : mk (b :: l) • x ∈ 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]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : α × Bool
n : ℕ
ih : reduce (List.replicate n x) = List.replicate n x
⊢ reduce (List.replicate (n + 1) x) = List.replicate (n + 1) x
have 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
Tactic: rw [List.replicate_succ, reduce.cons, ih]