awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G A : Type u
inst : Group G
inst_1 : IsFreeGroup G
inst_2 : MulAction G A
X : Type u
inst_3 : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun (e : IsFreeGroup.Generators G) ↦
    ⟨fun (b : A) ↦
      f (a :=
        Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) ()
          ((IsFreeGroup.of e)⁻¹ • b))
        (b := Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) () b)
        (Subtype.mk (p := fun (e_1 : IsFreeGroup.Generators G) ↦
          HSMul.hSMul (β := A) (IsFreeGroup.of e_1)
              (ActionCategory.back (M := G)
                (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) ()
                  ((IsFreeGroup.of e)⁻¹ • b))) =
            ActionCategory.back (M := G)
              (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) () b))
          e ⋯),
      IsFreeGroup.of e⟩
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), (F' : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun (F : G →* (A → X) ⋊[mulAutArrow] G) ↦
          ∀ (a : IsFreeGroup.Generators G), (F : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of a) = f' a)
        y →
      y = F'
E : ActionCategory G A ⥤ CategoryTheory.SingleObj X
hE :
  ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b),
    E.map
        (Subtype.mk (p :=
          fun
            (f :
              Sigma.fst (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                  (have this := a;
                  this) ⟶
                b.fst (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (CategoryTheory.Functor.map (actionAsFunctor G A) f) :
                (a :
                    (fun (X : Type u) ↦ X)
                      ((actionAsFunctor G A).obj
                        (have this := a;
                          this).fst)) →
                  (fun (X : Type u) ↦ X) ((actionAsFunctor G A).obj b.fst))
              (Sigma.snd (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                (have this := a;
                this)) =
            b.snd (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c))
          (IsFreeGroup.of (↑g : IsFreeGroup.Generators G)) ⋯) =
      f g
e : IsFreeGroup.Generators G
a :
  ∀ (x : A),
    SemidirectProduct.left (G := G) (φ := mulAutArrow)
        ((curry E : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of e)) x =
      (f' e).left x
⊢ (curry E : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of e) = f' e
have a₁ : SemidirectProduct.right (N := A → X) (φ := mulAutArrow)
    ((curry E : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of e)) =
  (f' e).right
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (hypothesis)
Goal:
G A : Type u
inst : Group G
inst_1 : IsFreeGroup G
inst_2 : MulAction G A
X : Type u
inst_3 : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun (e : IsFreeGroup.Generators G) ↦
    ⟨fun (b : A) ↦
      f (a :=
        Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) ()
          ((IsFreeGroup.of e)⁻¹ • b))
        (b := Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) () b)
        (Subtype.mk (p := fun (e_1 : IsFreeGroup.Generators G) ↦
          HSMul.hSMul (β := A) (IsFreeGroup.of e_1)
              (ActionCategory.back (M := G)
                (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) ()
                  ((IsFreeGroup.of e)⁻¹ • b))) =
            ActionCategory.back (M := G)
              (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) () b))
          e ⋯),
      IsFreeGroup.of e⟩
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), (F' : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun (F : G →* (A → X) ⋊[mulAutArrow] G) ↦
          ∀ (a : IsFreeGroup.Generators G), (F : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of a) = f' a)
        y →
      y = F'
E : ActionCategory G A ⥤ CategoryTheory.SingleObj X
hE :
  ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b),
    E.map
        (Subtype.mk (p :=
          fun
            (f :
              Sigma.fst (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                  (have this := a;
                  this) ⟶
                b.fst (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (CategoryTheory.Functor.map (actionAsFunctor G A) f) :
                (a :
                    (fun (X : Type u) ↦ X)
                      ((actionAsFunctor G A).obj
                        (have this := a;
                          this).fst)) →
                  (fun (X : Type u) ↦ X) ((actionAsFunctor G A).obj b.fst))
              (Sigma.snd (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                (have this := a;
                this)) =
            b.snd (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c))
          (IsFreeGroup.of (↑g : IsFreeGroup.Generators G)) ⋯) =
      f g
⊢ E = uncurry F' ⋯
have this : curry E = F'
Tactic: have : curry E = F' := by
        apply uF'
        intro e
        ext
        · convert! hE _ _ _
          rfl
        · rfl
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G A : Type u
inst : Group G
inst_1 : IsFreeGroup G
inst_2 : MulAction G A
X : Type u
inst_3 : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun (e : IsFreeGroup.Generators G) ↦
    ⟨fun (b : A) ↦
      f (a :=
        Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) ()
          ((IsFreeGroup.of e)⁻¹ • b))
        (b := Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) () b)
        (Subtype.mk (p := fun (e_1 : IsFreeGroup.Generators G) ↦
          HSMul.hSMul (β := A) (IsFreeGroup.of e_1)
              (ActionCategory.back (M := G)
                (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) ()
                  ((IsFreeGroup.of e)⁻¹ • b))) =
            ActionCategory.back (M := G)
              (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) () b))
          e ⋯),
      IsFreeGroup.of e⟩
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), (F' : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun (F : G →* (A → X) ⋊[mulAutArrow] G) ↦
          ∀ (a : IsFreeGroup.Generators G), (F : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of a) = f' a)
        y →
      y = F'
E : ActionCategory G A ⥤ CategoryTheory.SingleObj X
hE :
  ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b),
    E.map
        (Subtype.mk (p :=
          fun
            (f :
              Sigma.fst (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                  (have this := a;
                  this) ⟶
                b.fst (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (CategoryTheory.Functor.map (actionAsFunctor G A) f) :
                (a :
                    (fun (X : Type u) ↦ X)
                      ((actionAsFunctor G A).obj
                        (have this := a;
                          this).fst)) →
                  (fun (X : Type u) ↦ X) ((actionAsFunctor G A).obj b.fst))
              (Sigma.snd (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                (have this := a;
                this)) =
            b.snd (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c))
          (IsFreeGroup.of (↑g : IsFreeGroup.Generators G)) ⋯) =
      f g
this : curry E = F'
⊢ E = uncurry F' ⋯
have refine_3 : ∀ (X_1 : ActionCategory G A), E.obj X_1 = (uncurry F' sorry).obj X_1
Tactic: apply Functor.hext
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G A : Type u
inst : Group G
inst_1 : IsFreeGroup G
inst_2 : MulAction G A
X : Type u
inst_3 : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun (e : IsFreeGroup.Generators G) ↦
    ⟨fun (b : A) ↦
      f (a :=
        Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) ()
          ((IsFreeGroup.of e)⁻¹ • b))
        (b := Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) () b)
        (Subtype.mk (p := fun (e_1 : IsFreeGroup.Generators G) ↦
          HSMul.hSMul (β := A) (IsFreeGroup.of e_1)
              (ActionCategory.back (M := G)
                (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) ()
                  ((IsFreeGroup.of e)⁻¹ • b))) =
            ActionCategory.back (M := G)
              (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) () b))
          e ⋯),
      IsFreeGroup.of e⟩
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), (F' : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun (F : G →* (A → X) ⋊[mulAutArrow] G) ↦
          ∀ (a : IsFreeGroup.Generators G), (F : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of a) = f' a)
        y →
      y = F'
E : ActionCategory G A ⥤ CategoryTheory.SingleObj X
hE :
  ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b),
    E.map
        (Subtype.mk (p :=
          fun
            (f :
              Sigma.fst (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                  (have this := a;
                  this) ⟶
                b.fst (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (CategoryTheory.Functor.map (actionAsFunctor G A) f) :
                (a :
                    (fun (X : Type u) ↦ X)
                      ((actionAsFunctor G A).obj
                        (have this := a;
                          this).fst)) →
                  (fun (X : Type u) ↦ X) ((actionAsFunctor G A).obj b.fst))
              (Sigma.snd (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                (have this := a;
                this)) =
            b.snd (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c))
          (IsFreeGroup.of (↑g : IsFreeGroup.Generators G)) ⋯) =
      f g
this : curry E = F'
refine_3 : ∀ (X_1 : ActionCategory G A), E.obj X_1 = (uncurry F' ⋯).obj X_1
⊢ E = uncurry F' ⋯
have refine_3₁ : ∀ (X_1 Y : ActionCategory G A) (f : X_1 ⟶ Y), E.map f ≍ (uncurry F' sorry).map f
Tactic: apply Functor.hext
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G A : Type u
inst : Group G
inst_1 : IsFreeGroup G
inst_2 : MulAction G A
X : Type u
inst_3 : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun (e : IsFreeGroup.Generators G) ↦
    ⟨fun (b : A) ↦
      f (a :=
        Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) ()
          ((IsFreeGroup.of e)⁻¹ • b))
        (b := Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) () b)
        (Subtype.mk (p := fun (e_1 : IsFreeGroup.Generators G) ↦
          HSMul.hSMul (β := A) (IsFreeGroup.of e_1)
              (ActionCategory.back (M := G)
                (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) ()
                  ((IsFreeGroup.of e)⁻¹ • b))) =
            ActionCategory.back (M := G)
              (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) () b))
          e ⋯),
      IsFreeGroup.of e⟩
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), (F' : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun (F : G →* (A → X) ⋊[mulAutArrow] G) ↦
          ∀ (a : IsFreeGroup.Generators G), (F : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of a) = f' a)
        y →
      y = F'
E : ActionCategory G A ⥤ CategoryTheory.SingleObj X
hE :
  ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b),
    E.map
        (Subtype.mk (p :=
          fun
            (f :
              Sigma.fst (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                  (have this := a;
                  this) ⟶
                b.fst (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (CategoryTheory.Functor.map (actionAsFunctor G A) f) :
                (a :
                    (fun (X : Type u) ↦ X)
                      ((actionAsFunctor G A).obj
                        (have this := a;
                          this).fst)) →
                  (fun (X : Type u) ↦ X) ((actionAsFunctor G A).obj b.fst))
              (Sigma.snd (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                (have this := a;
                this)) =
            b.snd (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c))
          (IsFreeGroup.of (↑g : IsFreeGroup.Generators G)) ⋯) =
      f g
this : curry E = F'
⊢ ∀ (X_1 Y : ActionCategory G A) (f : X_1 ⟶ Y), E.map f ≍ (uncurry F' ⋯).map f
have refine_3 : ∀ (t : A) (g : G), E.map (homOfPair t g) ≍ (uncurry F' sorry).map (homOfPair t g)
Tactic: refine ActionCategory.cases ?_
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G A : Type u
inst : Group G
inst_1 : IsFreeGroup G
inst_2 : MulAction G A
X : Type u
inst_3 : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun (e : IsFreeGroup.Generators G) ↦
    ⟨fun (b : A) ↦
      f (a :=
        Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) ()
          ((IsFreeGroup.of e)⁻¹ • b))
        (b := Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) () b)
        (Subtype.mk (p := fun (e_1 : IsFreeGroup.Generators G) ↦
          HSMul.hSMul (β := A) (IsFreeGroup.of e_1)
              (ActionCategory.back (M := G)
                (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) ()
                  ((IsFreeGroup.of e)⁻¹ • b))) =
            ActionCategory.back (M := G)
              (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) () b))
          e ⋯),
      IsFreeGroup.of e⟩
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), (F' : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun (F : G →* (A → X) ⋊[mulAutArrow] G) ↦
          ∀ (a : IsFreeGroup.Generators G), (F : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of a) = f' a)
        y →
      y = F'
E : ActionCategory G A ⥤ CategoryTheory.SingleObj X
hE :
  ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b),
    E.map
        (Subtype.mk (p :=
          fun
            (f :
              Sigma.fst (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                  (have this := a;
                  this) ⟶
                b.fst (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (CategoryTheory.Functor.map (actionAsFunctor G A) f) :
                (a :
                    (fun (X : Type u) ↦ X)
                      ((actionAsFunctor G A).obj
                        (have this := a;
                          this).fst)) →
                  (fun (X : Type u) ↦ X) ((actionAsFunctor G A).obj b.fst))
              (Sigma.snd (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                (have this := a;
                this)) =
            b.snd (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c))
          (IsFreeGroup.of (↑g : IsFreeGroup.Generators G)) ⋯) =
      f g
this : curry E = F'
t : A
g : G
⊢ E.map (homOfPair t g) ≍ (uncurry F' ⋯).map (homOfPair t g)
have refine_3 : E.map (homOfPair t g) ≍ E.map (homOfPair t g)
Tactic: simp only [← this, uncurry_map, curry_apply_left, coe_back, homOfPair.val]
-- 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)
a : G
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) a
⊢ treeHom T a = homOfPath T p
have rw : homOfPath T default = homOfPath T p
Tactic: rw [treeHom, Unique.default_eq]
-- 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)
a : G
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) a
rw : homOfPath T default = homOfPath T p
⊢ treeHom T a = homOfPath T p
have rw₁ : homOfPath T p = homOfPath T p
Tactic: rw [treeHom, Unique.default_eq]
-- 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)
a b : Generators G
e : a ⟶ b
H : e ∈ wideSubquiverSymmetrify T a b
⊢ loopOfHom T (of e) = 𝟙 (root' T)
have rw : Eq (α := root' T ⟶ b)
  (treeHom T
      (have this := a;
      this) ≫
    of e)
  (treeHom T b)
Tactic: rw [loopOfHom, ← Category.assoc, IsIso.comp_inv_eq, Category.id_comp]
-- 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)
a b : Generators G
e : a ⟶ b
H : e ∈ wideSubquiverSymmetrify T a b
⊢ Eq (α := root' T ⟶ b)
    (treeHom T
        (have this := a;
        this) ≫
      of e)
    (treeHom T b)
have inl : ∀ (H : Sum.inl e ∈ T a b),
  Eq (α := root' T ⟶ b)
    (treeHom T
        (have this := a;
        this) ≫
      of e)
    (treeHom T b)
Tactic: rcases H with H | H
Cleared hypotheses: H
-- 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)
a b : Generators G
e : a ⟶ b
H : e ∈ wideSubquiverSymmetrify T a b
inl :
  ∀ (H : Sum.inl e ∈ T a b),
    Eq (α := root' T ⟶ b)
      (treeHom T
          (have this := a;
          this) ≫
        of e)
      (treeHom T b)
⊢ Eq (α := root' T ⟶ b)
    (treeHom T
        (have this := a;
        this) ≫
      of e)
    (treeHom T b)
have inr : ∀ (H : Sum.inr e ∈ T b a),
  Eq (α := root' T ⟶ b)
    (treeHom T
        (have this := a;
        this) ≫
      of e)
    (treeHom T b)
Tactic: rcases H with H | H
Cleared hypotheses: H
-- 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)
a b : Generators G
e : a ⟶ b
H : Sum.inl e ∈ T a b
⊢ Eq (α := root' T ⟶ b)
    (treeHom T
        (have this := a;
        this) ≫
      of e)
    (treeHom T b)
have inl : Eq (α := root' T ⟶ b)
  (treeHom T
      (have this := a;
      this) ≫
    of e)
  (CategoryStruct.comp (Y := a) (homOfPath T default)
    (Sum.recOn (motive := fun (x : a ⟶ b) ↦ a ⟶ b)
      (↑(Subtype.mk (p := fun (f : a ⟶ b) ↦ f ∈ T a b) (Sum.inl e) H) : a ⟶ b) (fun (e : a ⟶ b) ↦ of e)
      fun (e : b ⟶ a) ↦ inv (of e)))
Tactic: rw [treeHom_eq T (Path.cons default ⟨Sum.inl e, H⟩), homOfPath]
-- 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)
a b : Generators G
e : a ⟶ b
H : Sum.inr e ∈ T b a
⊢ Eq (α := root' T ⟶ b)
    (treeHom T
        (have this := a;
        this) ≫
      of e)
    (treeHom T b)
have inr : Eq (α := root' T ⟶ b)
  (CategoryStruct.comp (Y := b) (homOfPath T default)
      (Sum.recOn (motive := fun (x : b ⟶ a) ↦ b ⟶ a)
        (↑(Subtype.mk (p := fun (f : b ⟶ a) ↦ f ∈ T b a) (Sum.inr e) H) : b ⟶ a) (fun (e : b ⟶ a) ↦ of e)
        fun (e : a ⟶ b) ↦ inv (of e)) ≫
    of e)
  (treeHom T b)
Tactic: rw [treeHom_eq T (Path.cons default ⟨Sum.inr e, H⟩), homOfPath]
-- 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_1
inst_3 : Monoid X
f : MonoidHom.{u, u_1} (End (root' T)) X
a : G
⊢ Eq.{u_1 + 1} (α := () ⟶ ()) ((f : (a : End (root' T)) → X) (loopOfHom T (𝟙 a)) : X) (𝟙 () : () ⟶ ())
have dsimp : Eq.{u_1 + 1} (α := () ⟶ ()) ((f : (a : End (root' T)) → X) (treeHom T a ≫ 𝟙 a ≫ inv (treeHom T a)) : X) (𝟙 () : () ⟶ ())
Tactic: dsimp only [loopOfHom]
-- 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_1
inst_3 : Monoid X
f : MonoidHom.{u, u_1} (End (root' T)) X
a : G
⊢ Eq.{u_1 + 1} (α := () ⟶ ()) ((f : (a : End (root' T)) → X) (treeHom T a ≫ 𝟙 a ≫ inv (treeHom T a)) : X)
    (𝟙 () : () ⟶ ())
have rw : Eq.{u_1 + 1} (α := () ⟶ ()) ((f : (a : End (root' T)) → X) (treeHom T a ≫ inv (treeHom T a)) : X) (𝟙 () : () ⟶ ())
Tactic: rw [Category.id_comp, IsIso.hom_inv_id, ← End.one_def, f.map_one, id_as_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_1
inst_3 : Monoid X
f : MonoidHom.{u, u_1} (End (root' T)) X
a : G
rw : Eq.{u_1 + 1} (α := () ⟶ ()) ((f : (a : End (root' T)) → X) (treeHom T a ≫ inv (treeHom T a)) : X) (𝟙 () : () ⟶ ())
⊢ Eq.{u_1 + 1} (α := () ⟶ ()) ((f : (a : End (root' T)) → X) (treeHom T a ≫ 𝟙 a ≫ inv (treeHom T a)) : X)
    (𝟙 () : () ⟶ ())
have rw₁ : Eq.{u_1 + 1} (α := () ⟶ ()) ((f : (a : End (root' T)) → X) (𝟙 (root' T)) : X) (𝟙 () : () ⟶ ())
Tactic: rw [Category.id_comp, IsIso.hom_inv_id, ← End.one_def, f.map_one, id_as_one]