-- Mathlib/GroupTheory/FreeGroup/NielsenSchreier.lean
theorem path_nonempty_of_hom {G} [Groupoid.{u, u} G] [IsFreeGroupoid G] {a b : G} :
    Nonempty (a ⟶ b) → Nonempty (Path (symgen a) (symgen b))

Proof state:
case intro
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
⊢ FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen b)) *
      (FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen a)))⁻¹ =
    1

Tactic:
let X := FreeGroup (WeaklyConnectedComponent <| Generators G)

Result:
case intro
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
⊢ FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen b)) *
      (FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen a)))⁻¹ =
    1

Proof state:
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
⊢ Nonempty (a ⟶ b) → Nonempty (Path (IsFreeGroupoid.symgen a) (IsFreeGroupoid.symgen b))

Tactic:
rintro ⟨p⟩

Result:
case intro
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
⊢ Nonempty (Path (IsFreeGroupoid.symgen a) (IsFreeGroupoid.symgen b))

Proof state:
case intro
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
⊢ Nonempty (Path (IsFreeGroupoid.symgen a) (IsFreeGroupoid.symgen b))

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

Result:
case intro
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
⊢ FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen b)) *
      (FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen a)))⁻¹ =
    1

Proof state:
case intro.h.e_5.h.e_self.h
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
a✝ b✝ : Generators G
e✝ : a✝ ⟶ b✝
⊢ Nonempty
    (Path b✝
      (let_fun this := a✝;
      this))

Tactic:
exact ⟨Hom.toPath (Sum.inr (by assumption))⟩

Result:
no goals

Proof state:
case intro
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
⊢ FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen b)) *
      (FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen a)))⁻¹ =
    1

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

Result:
case intro
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
⊢ F.map p = ((Functor.const G).obj ()).map p

Proof state:
case intro
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
⊢ FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen b)) *
      (FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen a)))⁻¹ =
    1

Tactic:
let F : G ⥤ CategoryTheory.SingleObj.{u} (X : Type u) := SingleObj.differenceFunctor f

Result:
case intro
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
⊢ FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen b)) *
      (FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen a)))⁻¹ =
    1

Proof state:
case intro.h.e_5.h.e_self.h
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
a✝ b✝ : Generators G
e✝ : a✝ ⟶ b✝
⊢ WeaklyConnectedComponent.mk b✝ =
    WeaklyConnectedComponent.mk
      (let_fun this := a✝;
      this)

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

Result:
case intro.h.e_5.h.e_self.h
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
a✝ b✝ : Generators G
e✝ : a✝ ⟶ b✝
⊢ Nonempty
    (Path b✝
      (let_fun this := a✝;
      this))

Proof state:
case intro
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
⊢ FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen b)) *
      (FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen a)))⁻¹ =
    1

Tactic:
let f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)

Result:
case intro
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
⊢ FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen b)) *
      (FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen a)))⁻¹ =
    1

Proof state:
case intro
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
⊢ F.map p = ((Functor.const G).obj ()).map p

Tactic:
congr

Result:
case intro.h.e_5.h.e_self
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
⊢ F = (Functor.const G).obj ()

Proof state:
case intro.h.e_5.h.e_self.h
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
a✝ b✝ : Generators G
e✝ : a✝ ⟶ b✝
⊢ f b✝ =
    f
      (let_fun this := a✝;
      this)

Tactic:
apply congr_arg FreeGroup.of

Result:
case intro.h.e_5.h.e_self.h
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
a✝ b✝ : Generators G
e✝ : a✝ ⟶ b✝
⊢ WeaklyConnectedComponent.mk b✝ =
    WeaklyConnectedComponent.mk
      (let_fun this := a✝;
      this)