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
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)
rw [loopOfHom, ← Category.assoc, IsIso.comp_inv_eq, Category.id_comp]
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
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
cases' H with H H
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 (↑{ val := Sum.inl e, property := H }) (fun e => of e) fun e => inv (of e)
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
rw [treeHom_eq T (Path.cons default ⟨Sum.inl e, H⟩), homOfPath]
no goals
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 (↑{ val := Sum.inl e, property := H }) (fun e => of e) fun e => inv (of e)
rfl
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 (↑{ val := Sum.inr e, property := H }) (fun e => of e) fun e => inv (of e)) ≫ 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
rw [treeHom_eq T (Path.cons default ⟨Sum.inr e, H⟩), homOfPath]
no goals
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 (↑{ val := Sum.inr e, property := H }) (fun e => of e) fun e => inv (of e)) ≫ of e =
    treeHom T b
simp only [IsIso.inv_hom_id, Category.comp_id, Category.assoc, treeHom]