-- Mathlib/GroupTheory/FreeGroup/NielsenSchreier.lean
theorem loopOfHom_eq_id {a b : Generators G} (e) (H : e ∈ wideSubquiverSymmetrify T a b) :
    loopOfHom T (of e) = 𝟙 (root' T)

Proof state:
case inr
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : T b a (Sum.inr e)
⊢ treeHom T
        (let_fun this := a;
        this) ≫
      of e =
    treeHom T b

Tactic:
rw [treeHom_eq T (Path.cons default ⟨Sum.inr e, H⟩), homOfPath]

Result:
case inr
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : T b a (Sum.inr e)
⊢ (homOfPath T default ≫ Sum.recOn (↑⟨Sum.inr e, H⟩) (fun e => of e) fun e => inv (of e)) ≫ of e = treeHom T b

Proof state:
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : e ∈ wideSubquiverSymmetrify T a b
⊢ loopOfHom T (of e) = 𝟙 (IsFreeGroupoid.SpanningTree.root' T)

Tactic:
rw [loopOfHom, ← Category.assoc, IsIso.comp_inv_eq, Category.id_comp]

Result:
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : e ∈ wideSubquiverSymmetrify T a b
⊢ treeHom T
        (let_fun this := a;
        this) ≫
      of e =
    treeHom T b

Proof state:
case inr
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : T b a (Sum.inr e)
⊢ (homOfPath T default ≫ Sum.recOn (↑⟨Sum.inr e, H⟩) (fun e => of e) fun e => inv (of e)) ≫ of e = treeHom T b

Tactic:
simp only [IsIso.inv_hom_id, Category.comp_id, Category.assoc, treeHom]

Result:
no goals

Proof state:
case inl
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : T a b (Sum.inl e)
⊢ treeHom T
        (let_fun this := a;
        this) ≫
      of e =
    homOfPath T default ≫ Sum.recOn (↑⟨Sum.inl e, H⟩) (fun e => of e) fun e => inv (of e)

Tactic:
rfl

Result:
no goals

Proof state:
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : e ∈ wideSubquiverSymmetrify T a b
⊢ treeHom T
        (let_fun this := a;
        this) ≫
      of e =
    treeHom T b

Tactic:
rcases H with H | H

Result:
case inl
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : T a b (Sum.inl e)
⊢ treeHom T
        (let_fun this := a;
        this) ≫
      of e =
    treeHom T b

case inr
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : T b a (Sum.inr e)
⊢ treeHom T
        (let_fun this := a;
        this) ≫
      of e =
    treeHom T b

Proof state:
case inl
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : T a b (Sum.inl e)
⊢ treeHom T
        (let_fun this := a;
        this) ≫
      of e =
    treeHom T b

Tactic:
rw [treeHom_eq T (Path.cons default ⟨Sum.inl e, H⟩), homOfPath]

Result:
case inl
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : T a b (Sum.inl e)
⊢ treeHom T
        (let_fun this := a;
        this) ≫
      of e =
    homOfPath T default ≫ Sum.recOn (↑⟨Sum.inl e, H⟩) (fun e => of e) fun e => inv (of e)