awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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)
refine_2 : ∀ (a b : Generators G) (g : a ⟶ b), (functorOfMonoidHom T E).map (of g) = f' g
⊢ functorOfMonoidHom T E = F'

Tactic:
apply uF'
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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
refine_2 :
  Eq (α := X) ((E : (a : End (root' T)) → X) (loopOfHom T (of e)) : X)
    (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) :
      X)
⊢ (functorOfMonoidHom T E).map (of e) = f' e

Tactic:
change E (loopOfHom T _) = dite _ _ _

Premises used: IsFreeGroupoid.SpanningTree.loopOfHom, dite, DFunLike.coe
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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)
pos₂ pos₃ : Eq.{u + 1} (α := X) 1 1
⊢ Eq (α := X) ((E : (a : End (root' T)) → X) (loopOfHom T (of e)) : X) (1 : X)

Tactic:
rw [loopOfHom_eq_id T e h, ← End.one_def, E.map_one]

Premises used: IsFreeGroupoid.SpanningTree.loopOfHom_eq_id, MonoidHom.map_one, CategoryTheory.End.one_def
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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
⊢ (E : (a : End (root' T)) → X) (loopOfHom T (of e)) =
    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 : Quiver.Total (Generators G) } h)

Tactic:
hE ⟨⟨a, b, e⟩, h⟩

Premises used: Quiver.Total.mk, Subtype.mk
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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
⊢ (E : (a : End (root' T)) → X) (loopOfHom T (of e)) =
    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 : Quiver.Total (Generators G) } h)

Tactic:
exact hE ⟨⟨a, b, e⟩, h⟩

Premises used: Quiver.Total.mk, Subtype.mk
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsFreeGroupoid G
a b : G
p : a ⟶ b
rw :
  HMul.hMul (α := FreeGroup (WeaklyConnectedComponent (Generators G)))
      (FreeGroup.of (WeaklyConnectedComponent.mk (symgen b)))
      (FreeGroup.of (WeaklyConnectedComponent.mk (symgen a)))⁻¹ =
    1
⊢ Nonempty.{u + 1} (Path (V := Symmetrify (Generators G)) (symgen a) (symgen b))

Tactic:
rw [← @WeaklyConnectedComponent.eq (Generators G), eq_comm, ← FreeGroup.of_injective.eq_iff, ←
    mul_inv_eq_one]

Premises used: mul_inv_eq_one, Function.Injective.eq_iff, Quiver.WeaklyConnectedComponent.eq, eq_comm, FreeGroup.of_injective
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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
change : F.map p = CategoryTheory.Functor.map (Functor.obj (Functor.const G) ()) p
⊢ HMul.hMul (α := FreeGroup (WeaklyConnectedComponent (Generators G)))
      (FreeGroup.of (WeaklyConnectedComponent.mk (symgen b)))
      (FreeGroup.of (WeaklyConnectedComponent.mk (symgen a)))⁻¹ =
    1

Tactic:
change (F.map p) = ((@CategoryTheory.Functor.const G _ _ (SingleObj.category X)).obj ()).map p

Premises used: Unit.unit, CategoryTheory.Functor.map, CategoryTheory.Functor.const, CategoryTheory.Functor.obj
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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
h : F = Functor.obj (Functor.const G) ()
⊢ F.map p = CategoryTheory.Functor.map (Functor.obj (Functor.const G) ()) p

Tactic:
congr
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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
h :
  ∀ (a b : Generators G) (e : a ⟶ b),
    F.map (of e) = CategoryTheory.Functor.map (Functor.obj (Functor.const G) ()) (of e)
⊢ F = Functor.obj (Functor.const G) ()

Tactic:
ext
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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
h :
  f b_1 =
    f
      (have this := a_1;
      this)
⊢ F.map (of e) = CategoryTheory.Functor.map (Functor.obj (Functor.const G) ()) (of e)

Tactic:
rw [Functor.const_obj_map, id_as_one, differenceFunctor_map, @mul_inv_eq_one _ _ (f _)]

Premises used: CategoryTheory.SingleObj.id_as_one, mul_inv_eq_one, CategoryTheory.SingleObj.differenceFunctor_map, CategoryTheory.Functor.const_obj_map
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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
h :
  Eq (α := WeaklyConnectedComponent (Generators G)) (WeaklyConnectedComponent.mk b_1)
    (WeaklyConnectedComponent.mk
      (have this := a_1;
      this))
⊢ f b_1 =
    f
      (have this := a_1;
      this)

Tactic:
apply congr_arg FreeGroup.of

Premises used: FreeGroup.of, congr_arg
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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
h :
  Nonempty.{u + 1}
    (Path b_1
      (have this := a_1;
      this))
⊢ Eq (α := WeaklyConnectedComponent (Generators G)) (WeaklyConnectedComponent.mk b_1)
    (WeaklyConnectedComponent.mk
      (have this := a_1;
      this))

Tactic:
apply (WeaklyConnectedComponent.eq _ _).mpr

Premises used: Iff.mpr, Quiver.WeaklyConnectedComponent.eq
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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
⊢ (have this := a_1;
    this) ⟶
    b_1

Tactic:
assumption
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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
⊢ Nonempty.{u + 1}
    (Path b_1
      (have this := a_1;
      this))

Tactic:
exact ⟨Hom.toPath (Sum.inr (by assumption))⟩
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsConnected G
inst_2 : IsFreeGroupoid G
r : G
⊢ RootedConnected (V := Symmetrify (Generators G)) (symgen r)

Tactic:
⟨fun b => path_nonempty_of_hom (CategoryTheory.nonempty_hom_of_preconnected_groupoid r b)⟩

Premises used: CategoryTheory.nonempty_hom_of_preconnected_groupoid, IsFreeGroupoid.path_nonempty_of_hom, Quiver.RootedConnected.mk
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsConnected G
inst_2 : IsFreeGroupoid G
r : G
⊢ IsFreeGroup.{u} (End r)

Tactic:
SpanningTree.endIsFree <| geodesicSubtree (symgen r)

Premises used: _private.0.IsFreeGroupoid.symgen, IsFreeGroupoid.SpanningTree.endIsFree, Quiver.geodesicSubtree, _private.0.IsFreeGroupoid.SpanningTree.root', Quiver.root
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
Goal:
G : Type u
inst : Group G
inst_1 : IsFreeGroup G
H : Subgroup G
⊢ IsFreeGroup.{u} ↥H

Tactic:
IsFreeGroup.ofMulEquiv (endMulEquivSubgroup H)

Premises used: IsFreeGroup.ofMulEquiv, CategoryTheory.ActionCategory.endMulEquivSubgroup
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
inst : DecidableEq α
w : α × Bool
g : FreeGroup α
h : g ∈ startsWith w
h1 : g = 1
⊢ False

Tactic:
simp [h1, startsWith, FreeGroup.toWord_one] at h

Premises used: FreeGroup.toWord_one, FreeGroup.startsWith
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
inst : DecidableEq α
w w' : α × Bool
simp_all :
  (∀ (x : FreeGroup α),
      getElem? (valid := fun (as : List (α × Bool)) (i : ℕ) ↦ i < as.length) x.toWord 0 = some w → ¬w = w') ↔
    ¬w = w'
⊢ Disjoint (startsWith w) (startsWith 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]

Premises used: iff_false, Set.mem_inter_iff, Option.some.injEq, Set.mem_setOf_eq, ne_eq, Set.disjoint_iff_inter_eq_empty, FreeGroup.startsWith, Set.mem_empty_iff_false, Set.ext_iff, not_and
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
inst : DecidableEq α
w w' : α × Bool
h :
  ∀ (x : FreeGroup α),
    getElem? (valid := fun (as : List (α × Bool)) (i : ℕ) ↦ i < as.length) x.toWord 0 = some w → ¬w = w'
⊢ getElem? (valid := fun (as : List (α × Bool)) (i : ℕ) ↦ i < as.length) (mk [w]).toWord 0 = some w

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
inst : DecidableEq α
w w' : α × Bool
⊢ ¬w = w' →
    ∀ (x : FreeGroup α),
      getElem? (valid := fun (as : List (α × Bool)) (i : ℕ) ↦ i < as.length) x.toWord 0 = some w → ¬w = w'

Tactic:
grind
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
inst : DecidableEq α
w w' : α × Bool
⊢ (∀ (x : FreeGroup α),
      getElem? (valid := fun (as : List (α × Bool)) (i : ℕ) ↦ i < as.length) x.toWord 0 = some w → ¬w = w') ↔
    ¬w = w'

Tactic:
exact Iff.intro (fun h ↦ h (mk [w]) (by simp)) (by grind)

Premises used: Iff.intro
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
inst : DecidableEq α
a b : α × Bool
h : startsWith a = startsWith b
⊢ ∀ (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

Premises used: Set.mem_setOf_eq, FreeGroup.startsWith, Set.ext_iff
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
Goal:
α : Type u_1
inst : DecidableEq α
a b : α × Bool
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
⊢ a = b

Tactic:
simpa using h (mk [a])

Premises used: List.cons, FreeGroup.mk, List.nil
-- Module: Mathlib.GroupTheory.FreeGroup.Orbit
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
neg : ∀ (hC : ¬0 < g.toWord.length), mk [w] * g ∈ startsWith w
⊢ mk [w] * g ∈ startsWith w

Tactic:
by_cases hC : 0 < g.toWord.length

Premises used: FreeGroup.toWord, List.length
-- 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
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
⊢ mk [w] * g ∈ startsWith 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 *

Premises used: FreeGroup.reduce.cons, Option.some.injEq, FreeGroup.toWord_mk, Set.mem_setOf_eq, FreeGroup.reduce_toWord, FreeGroup.reduce_nil, FreeGroup.startsWith, getElem?_pos, List.nil_append, Prod.eq_iff_fst_eq_snd_eq, not_and, Bool.not_eq_not, List.cons_append, FreeGroup.toWord_mul
-- 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
⊢ g.toWord ≠ []

Tactic:
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
⊢ g.toWord = g.toWord.head ⋯ :: g.toWord.tail

Tactic:
grind