awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
V : Type u
inst : ReflQuiver.{v₁, u} V
W : Type u₂
inst_1 : ReflQuiver.{v₂, u₂} W
F_obj : V → W
map : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id :
  ∀ (X : V),
    { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.map (𝟙rq X) =
      𝟙rq ({ obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X)
map_1 : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id_1 :
  ∀ (X : V),
    { obj := F_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.map (𝟙rq X) =
      𝟙rq ({ obj := F_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X)
h_obj :
  ∀ (X : V),
    { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X =
      { obj := F_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.map f =
      Eq.recOn (motive :=
        fun (x : W)
          (x_1 : { obj := F_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj Y = x) ↦
        { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X ⟶ x) ⋯
        (Eq.recOn (motive :=
          fun (x : W)
            (x_1 : { obj := F_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X = x) ↦
          x ⟶ { obj := F_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj Y) ⋯
          ({ obj := F_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.map f))
X Y : V
f : X ⟶ Y
⊢ map f = map_1 f

Tactic:
simpa using h_map X Y f
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
V W : Type u
inst : ReflQuiver.{v, u} V
inst_1 : ReflQuiver.{v, u} W
F G : ReflPrefunctor.{v, v, u, u} V W
h_obj : ∀ (X : V), F.obj X = G.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), F.map f = Quiver.homOfEq (G.map f) ⋯ ⋯
obtain :
  ∀ (Fpre : Prefunctor.{v, v, u, u} V W) (Fid : ∀ (X : V), Fpre.map (𝟙rq X) = 𝟙rq (Fpre.obj X))
    (h_obj : ∀ (X : V), { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W }.obj X = G.obj X)
    (h_map :
      ∀ (X Y : V) (f : X ⟶ Y),
        { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W }.map f = Quiver.homOfEq (G.map f) ⋯ ⋯),
    { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W } = G
⊢ F = G

Tactic:
obtain ⟨Fpre, Fid⟩ := F
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
V W : Type u
inst : ReflQuiver.{v, u} V
inst_1 : ReflQuiver.{v, u} W
G : ReflPrefunctor.{v, v, u, u} V W
Fpre : Prefunctor.{v, v, u, u} V W
Fid : ∀ (X : V), Fpre.map (𝟙rq X) = 𝟙rq (Fpre.obj X)
h_obj : ∀ (X : V), { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W }.obj X = G.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W }.map f = Quiver.homOfEq (G.map f) ⋯ ⋯
obtain :
  ∀ (Gpre : Prefunctor.{v, v, u, u} V W) (Gid : ∀ (X : V), Gpre.map (𝟙rq X) = 𝟙rq (Gpre.obj X))
    (h_obj :
      ∀ (X : V),
        { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W }.obj X =
          { toPrefunctor := Gpre, map_id := Gid : ReflPrefunctor.{v, v, u, u} V W }.obj X)
    (h_map :
      ∀ (X Y : V) (f : X ⟶ Y),
        { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W }.map f =
          Quiver.homOfEq ({ toPrefunctor := Gpre, map_id := Gid : ReflPrefunctor.{v, v, u, u} V W }.map f) ⋯ ⋯),
    { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W } = { toPrefunctor := Gpre, map_id := Gid }
⊢ { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W } = G

Tactic:
obtain ⟨Gpre, Gid⟩ := G
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
V W : Type u
inst : ReflQuiver.{v, u} V
inst_1 : ReflQuiver.{v, u} W
Fpre : Prefunctor.{v, v, u, u} V W
Fid : ∀ (X : V), Fpre.map (𝟙rq X) = 𝟙rq (Fpre.obj X)
Gpre : Prefunctor.{v, v, u, u} V W
Gid : ∀ (X : V), Gpre.map (𝟙rq X) = 𝟙rq (Gpre.obj X)
h_obj :
  ∀ (X : V),
    { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W }.obj X =
      { toPrefunctor := Gpre, map_id := Gid : ReflPrefunctor.{v, v, u, u} V W }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W }.map f =
      Quiver.homOfEq ({ toPrefunctor := Gpre, map_id := Gid : ReflPrefunctor.{v, v, u, u} V W }.map f) ⋯ ⋯
⊢ Fpre = Gpre

Tactic:
Prefunctor.ext' (V := V) (W := W) h_obj h_map

Premises used: Prefunctor.ext'
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
V W : Type u
inst : ReflQuiver.{v, u} V
inst_1 : ReflQuiver.{v, u} W
Fpre : Prefunctor.{v, v, u, u} V W
Fid : ∀ (X : V), Fpre.map (𝟙rq X) = 𝟙rq (Fpre.obj X)
Gpre : Prefunctor.{v, v, u, u} V W
Gid : ∀ (X : V), Gpre.map (𝟙rq X) = 𝟙rq (Gpre.obj X)
h_obj :
  ∀ (X : V),
    { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W }.obj X =
      { toPrefunctor := Gpre, map_id := Gid : ReflPrefunctor.{v, v, u, u} V W }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W }.map f =
      Quiver.homOfEq ({ toPrefunctor := Gpre, map_id := Gid : ReflPrefunctor.{v, v, u, u} V W }.map f) ⋯ ⋯
obtain :
  ∀ (Gid : ∀ (X : V), Fpre.map (𝟙rq X) = 𝟙rq (Fpre.obj X))
    (h_obj :
      ∀ (X : V),
        { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W }.obj X =
          { toPrefunctor := Fpre, map_id := Gid : ReflPrefunctor.{v, v, u, u} V W }.obj X)
    (h_map :
      ∀ (X Y : V) (f : X ⟶ Y),
        { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W }.map f =
          Quiver.homOfEq ({ toPrefunctor := Fpre, map_id := Gid : ReflPrefunctor.{v, v, u, u} V W }.map f) ⋯ ⋯),
    { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W } = { toPrefunctor := Fpre, map_id := Gid }
⊢ { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W } = { toPrefunctor := Gpre, map_id := Gid }

Tactic:
obtain rfl : Fpre = Gpre := Prefunctor.ext' (V := V) (W := W) h_obj h_map

Premises used: Prefunctor.ext', rfl
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
V W : Type u
inst : ReflQuiver.{v, u} V
inst_1 : ReflQuiver.{v, u} W
Fpre : Prefunctor.{v, v, u, u} V W
Fid Gid : ∀ (X : V), Fpre.map (𝟙rq X) = 𝟙rq (Fpre.obj X)
h_obj :
  ∀ (X : V),
    { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W }.obj X =
      { toPrefunctor := Fpre, map_id := Gid : ReflPrefunctor.{v, v, u, u} V W }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W }.map f =
      Quiver.homOfEq ({ toPrefunctor := Fpre, map_id := Gid : ReflPrefunctor.{v, v, u, u} V W }.map f) ⋯ ⋯
⊢ { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W } = { toPrefunctor := Fpre, map_id := Gid }

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
U : Type u_1
inst : ReflQuiver.{u_4, u_1} U
V : Type u_2
inst_1 : ReflQuiver.{u_5, u_2} V
W : Type u_3
inst_2 : ReflQuiver.{u_6, u_3} W
F : ReflPrefunctor.{u_4, u_5, u_1, u_2} U V
G : ReflPrefunctor.{u_5, u_6, u_2, u_3} V W
x : U
⊢ (F.toPrefunctor ⋙q G.toPrefunctor).map (𝟙rq x) = 𝟙rq ((F.toPrefunctor ⋙q G.toPrefunctor).obj x)

Tactic:
simp [F.map_id, G.map_id]

Premises used: CategoryTheory.ReflPrefunctor.map_id
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
U : Type u_1
V : Type u_2
inst : ReflQuiver.{u_3, u_1} U
inst_1 : ReflQuiver.{u_4, u_2} V
F : ReflPrefunctor.{u_3, u_4, u_1, u_2} U V
⊢ F.comp (id V) = F

Tactic:
rfl

Premises used: CategoryTheory.ReflPrefunctor.comp, Prefunctor.comp, rfl
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
U : Type u_1
V : Type u_2
inst : ReflQuiver.{u_3, u_1} U
inst_1 : ReflQuiver.{u_4, u_2} V
F : ReflPrefunctor.{u_3, u_4, u_1, u_2} U V
⊢ comp (id U) F = F

Tactic:
rfl

Premises used: CategoryTheory.ReflPrefunctor.comp, Prefunctor.comp, rfl
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
U : Type u_1
V : Type u_2
W : Type u_3
Z : Type u_4
inst : ReflQuiver.{u_5, u_1} U
inst_1 : ReflQuiver.{u_6, u_2} V
inst_2 : ReflQuiver.{u_7, u_3} W
inst_3 : ReflQuiver.{u_8, u_4} Z
F : ReflPrefunctor.{u_5, u_6, u_1, u_2} U V
G : ReflPrefunctor.{u_6, u_7, u_2, u_3} V W
H : ReflPrefunctor.{u_7, u_8, u_3, u_4} W Z
⊢ (F.comp G).comp H = F.comp (G.comp H)

Tactic:
rfl

Premises used: CategoryTheory.ReflPrefunctor.comp, Prefunctor.comp, rfl
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
U : Type u_1
V : Type u_2
inst : ReflQuiver.{u_3, u_1} U
inst_1 : ReflQuiver.{u_4, u_2} V
F : ReflPrefunctor.{u_3, u_4, u_1, u_2} U V
X Y : U
f g : X ⟶ Y
h : f = g
⊢ F.map f = F.map g

Tactic:
congrArg F.map h

Premises used: congrArg, CategoryTheory.ReflPrefunctor.toPrefunctor, Prefunctor.map
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
U : Type u_1
V : Type u_2
inst : ReflQuiver.{u_3, u_1} U
inst_1 : ReflQuiver.{u_4, u_2} V
F G : ReflPrefunctor.{u_3, u_4, u_1, u_2} U V
e : F = G
X : U
refl : F.obj X = F.obj X
⊢ F.obj X = G.obj X

Tactic:
cases e
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
U : Type u_1
V : Type u_2
inst : ReflQuiver.{u_3, u_1} U
inst_1 : ReflQuiver.{u_4, u_2} V
F : ReflPrefunctor.{u_3, u_4, u_1, u_2} U V
X : U
⊢ F.obj X = F.obj X

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
U : Type u_1
V : Type u_2
inst : ReflQuiver.{u_3, u_1} U
inst_1 : ReflQuiver.{u_4, u_2} V
F G : ReflPrefunctor.{u_3, u_4, u_1, u_2} U V
e : F = G
X Y : U
f : X ⟶ Y
subst : Quiver.homOfEq (F.map f) ⋯ ⋯ = F.map f
⊢ Quiver.homOfEq (F.map f) ⋯ ⋯ = G.map f

Tactic:
subst e
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
U : Type u_1
V : Type u_2
inst : ReflQuiver.{u_3, u_1} U
inst_1 : ReflQuiver.{u_4, u_2} V
F : ReflPrefunctor.{u_3, u_4, u_1, u_2} U V
X Y : U
f : X ⟶ Y
⊢ Quiver.homOfEq (F.map f) ⋯ ⋯ = F.map f

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
⊢ (F ⋙ G).toReflPrefunctor = F.toReflPrefunctor ⋙rq G.toReflPrefunctor

Tactic:
rfl

Premises used: CategoryTheory.ReflPrefunctor.comp, Prefunctor.comp, rfl
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
C : Cat
D : Cat
F : Functor.{u_1, u_3, u_2, u_4} (↑C : Type u_2) (↑D : Type u_4)
⊢ F.toReflPrefunctor.toPrefunctor = F.toPrefunctor

Tactic:
rfl

Premises used: CategoryTheory.Functor.toPrefunctor, rfl
-- Module: Mathlib.Combinatorics.Quiver.Schreier
Goal:
V : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : MulAction M V
S : Type u_3
ι : S → M
a b : M
x : SchreierGraph V ι
toVertex : ((a * b) • x).toVertex = (a • b • x).toVertex
⊢ (a * b) • x = a • b • x

Tactic:
ext
-- Module: Mathlib.Combinatorics.Quiver.Schreier
Goal:
V : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : MulAction M V
S : Type u_3
ι : S → M
a b : M
x : SchreierGraph V ι
⊢ ((a * b) • x).toVertex = (a • b • x).toVertex

Tactic:
mul_smul a b x.toVertex

Premises used: Quiver.SchreierGraph.toVertex, SemigroupAction.mul_smul
-- Module: Mathlib.Combinatorics.Quiver.Schreier
Goal:
V : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : MulAction M V
S : Type u_3
ι : S → M
a b : M
x : SchreierGraph V ι
⊢ ((a * b) • x).toVertex = (a • b • x).toVertex

Tactic:
exact mul_smul a b x.toVertex

Premises used: Quiver.SchreierGraph.toVertex, SemigroupAction.mul_smul
-- Module: Mathlib.Combinatorics.Quiver.Schreier
Goal:
V : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : MulAction M V
S : Type u_3
ι : S → M
x : SchreierGraph V ι
toVertex : (HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 x).toVertex = x.toVertex
⊢ HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 x = x

Tactic:
ext
-- Module: Mathlib.Combinatorics.Quiver.Schreier
Goal:
V : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : MulAction M V
S : Type u_3
ι : S → M
x : SchreierGraph V ι
⊢ (HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 x).toVertex = x.toVertex

Tactic:
one_smul M x.toVertex

Premises used: Quiver.SchreierGraph.toVertex, one_smul
-- Module: Mathlib.Combinatorics.Quiver.Schreier
Goal:
V : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : MulAction M V
S : Type u_3
ι : S → M
x : SchreierGraph V ι
⊢ (HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 x).toVertex = x.toVertex

Tactic:
exact one_smul M x.toVertex

Premises used: Quiver.SchreierGraph.toVertex, one_smul
-- Module: Mathlib.Combinatorics.Quiver.Schreier
Goal:
V : Type u_1
M : Type u_2
inst : Group M
inst_1 : MulAction M V
S : Type u_3
ι : S → M
x : SchreierGraph V ι
x_1 : Costar (SingleObj.star S)
fst : SingleObj S
s : fst ⟶ SingleObj.star S
⊢ ι s • (ι s)⁻¹ • x = x

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Schreier
Goal:
V : Type u_1
M : Type u_2
inst : Group M
inst_1 : MulAction M V
S : Type u_3
ι : S → M
x v : SchreierGraph V ι
s : S
hs : ι s • v = x
simp :
  Eq (α := Costar.{u_3, u_1} x)
    (Sigma.mk (β := fun (u : SchreierGraph V ι) ↦ u ⟶ x) ((ι s)⁻¹ • x)
      (Subtype.mk (p := fun (s_1 : S) ↦ ι s_1 • (ι s)⁻¹ • x = x) s ⋯))
    (Sigma.mk (β := fun (u : SchreierGraph V ι) ↦ u ⟶ x) v (Subtype.mk (p := fun (s : S) ↦ ι s • v = x) s hs))
⊢ Eq (α := Costar.{u_3, u_1} x)
    ((fun (x_1 : Costar (SingleObj.star S)) ↦
        (match (motive := Costar (SingleObj.star S) → Costar.{u_3, u_1} x) x_1 with
          | ⟨fst, s⟩ =>
            Sigma.mk (β := fun (u : SchreierGraph V ι) ↦ u ⟶ x) ((ι s)⁻¹ • x)
              (Subtype.mk (p := fun (s_1 : S) ↦ ι s_1 • (ι s)⁻¹ • x = x) s ⋯) :
          Costar.{u_3, u_1} x))
      (Prefunctor.costar (labelling V ι) x
        (Sigma.mk (β := fun (u : SchreierGraph V ι) ↦ u ⟶ x) v (Subtype.mk (p := fun (s : S) ↦ ι s • v = x) s hs))))
    (Sigma.mk (β := fun (u : SchreierGraph V ι) ↦ u ⟶ x) v (Subtype.mk (p := fun (s : S) ↦ ι s • v = x) s hs))

Tactic:
simp only [Prefunctor.costar_apply, labelling_map]

Premises used: Quiver.SchreierGraph.labelling_map, Prefunctor.costar_apply
-- Module: Mathlib.Combinatorics.Quiver.Schreier
Goal:
V : Type u_1
M : Type u_2
inst : Group M
inst_1 : MulAction M V
S : Type u_3
ι : S → M
x v : SchreierGraph V ι
s : S
hs : ι s • v = x
rw : (ι s)⁻¹ • ι s • v = v
rw₁ rw₂ : v = v
⊢ (ι s)⁻¹ • x = v

Tactic:
rw [← hs, inv_smul_smul]

Premises used: inv_smul_smul
-- Module: Mathlib.Combinatorics.Quiver.Schreier
Goal:
V : Type u_1
M : Type u_2
inst : Group M
inst_1 : MulAction M V
S : Type u_3
ι : S → M
x v : SchreierGraph V ι
s : S
hs : ι s • v = x
⊢ (ι s)⁻¹ • x = v

Tactic:
have : (ι s)⁻¹ • x = v := by rw [← hs, inv_smul_smul]
-- Module: Mathlib.Combinatorics.Quiver.Schreier
Goal:
V : Type u_1
M : Type u_2
inst : Group M
inst_1 : MulAction M V
S : Type u_3
ι : S → M
x v : SchreierGraph V ι
s : S
hs : ι s • v = x
this : (ι s)⁻¹ • x = v
subst :
  ∀ (hs : ι s • (ι s)⁻¹ • x = x),
    Eq (α := Costar.{u_3, u_1} x)
      (Sigma.mk (β := fun (u : SchreierGraph V ι) ↦ u ⟶ x) ((ι s)⁻¹ • x)
        (Subtype.mk (p := fun (s_1 : S) ↦ ι s_1 • (ι s)⁻¹ • x = x) s ⋯))
      (Sigma.mk (β := fun (u : SchreierGraph V ι) ↦ u ⟶ x) ((ι s)⁻¹ • x)
        (Subtype.mk (p := fun (s_1 : S) ↦ ι s_1 • (ι s)⁻¹ • x = x) s hs))
⊢ Eq (α := Costar.{u_3, u_1} x)
    (Sigma.mk (β := fun (u : SchreierGraph V ι) ↦ u ⟶ x) ((ι s)⁻¹ • x)
      (Subtype.mk (p := fun (s_1 : S) ↦ ι s_1 • (ι s)⁻¹ • x = x) s ⋯))
    (Sigma.mk (β := fun (u : SchreierGraph V ι) ↦ u ⟶ x) v (Subtype.mk (p := fun (s : S) ↦ ι s • v = x) s hs))

Tactic:
subst this
-- Module: Mathlib.Combinatorics.Quiver.Schreier
Goal:
V : Type u_1
M : Type u_2
inst : Group M
inst_1 : MulAction M V
S : Type u_3
ι : S → M
x : SchreierGraph V ι
s : S
hs : ι s • (ι s)⁻¹ • x = x
⊢ Eq (α := Costar.{u_3, u_1} x)
    (Sigma.mk (β := fun (u : SchreierGraph V ι) ↦ u ⟶ x) ((ι s)⁻¹ • x)
      (Subtype.mk (p := fun (s_1 : S) ↦ ι s_1 • (ι s)⁻¹ • x = x) s ⋯))
    (Sigma.mk (β := fun (u : SchreierGraph V ι) ↦ u ⟶ x) ((ι s)⁻¹ • x)
      (Subtype.mk (p := fun (s_1 : S) ↦ ι s_1 • (ι s)⁻¹ • x = x) s hs))

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Schreier
Goal:
V : Type u_1
M : Type u_2
inst : Group M
inst_1 : MulAction M V
S : Type u_3
ι : S → M
W : Type u_4
inst_2 : MulAction M W
φ : Prefunctor.{u_3, u_3, u_1, u_4} (SchreierGraph V ι) (SchreierGraph W ι)
φm : φ ⋙q labelling W ι = labelling V ι
v : SchreierGraph V ι
s : S
e : v ⟶ ι s • v := Subtype.mk (p := fun (s_1 : S) ↦ ι s_1 • v = ι s • v) s ⋯
⊢ ι (↑(φ.map e) : S) • φ.obj v = φ.obj (ι s • v)

Tactic:
have h := (φ.map e).property
-- Module: Mathlib.Combinatorics.Quiver.Schreier
Goal:
V : Type u_1
M : Type u_2
inst : Group M
inst_1 : MulAction M V
S : Type u_3
ι : S → M
W : Type u_4
inst_2 : MulAction M W
φ : Prefunctor.{u_3, u_3, u_1, u_4} (SchreierGraph V ι) (SchreierGraph W ι)
φm : φ ⋙q labelling W ι = labelling V ι
v : SchreierGraph V ι
s : S
e : v ⟶ ι s • v := Subtype.mk (p := fun (s_1 : S) ↦ ι s_1 • v = ι s • v) s ⋯
h : ι (↑(φ.map e) : S) • φ.obj v = φ.obj (ι s • v)
rw rw₁ :
  Eq (α := Prefunctor.obj (labelling V ι) v ⟶ Prefunctor.obj (labelling V ι) (ι s • v))
    (Prefunctor.map (labelling V ι) e) (Prefunctor.map (labelling V ι) e)
⊢ (φ ⋙q labelling W ι).map e = Prefunctor.map (labelling V ι) e

Tactic:
rw [φm]
-- Module: Mathlib.Combinatorics.Quiver.Schreier
Goal:
V : Type u_1
M : Type u_2
inst : Group M
inst_1 : MulAction M V
S : Type u_3
ι : S → M
W : Type u_4
inst_2 : MulAction M W
φ : Prefunctor.{u_3, u_3, u_1, u_4} (SchreierGraph V ι) (SchreierGraph W ι)
φm : φ ⋙q labelling W ι = labelling V ι
v : SchreierGraph V ι
s : S
e : v ⟶ ι s • v := Subtype.mk (p := fun (s_1 : S) ↦ ι s_1 • v = ι s • v) s ⋯
h : ι (↑(φ.map e) : S) • φ.obj v = φ.obj (ι s • v)
⊢ (φ ⋙q labelling W ι).map e = Prefunctor.map (labelling V ι) e

Tactic:
have : (φ ⋙q labelling W ι).map e = (labelling V ι).map e := by
      rw [φm]
-- Module: Mathlib.Combinatorics.Quiver.Schreier
Goal:
V : Type u_1
M : Type u_2
inst : Group M
inst_1 : MulAction M V
S : Type u_3
ι : S → M
W : Type u_4
inst_2 : MulAction M W
φ : Prefunctor.{u_3, u_3, u_1, u_4} (SchreierGraph V ι) (SchreierGraph W ι)
φm : φ ⋙q labelling W ι = labelling V ι
v : SchreierGraph V ι
s : S
e : v ⟶ ι s • v := Subtype.mk (p := fun (s_1 : S) ↦ ι s_1 • v = ι s • v) s ⋯
h : ι (↑(φ.map e) : S) • φ.obj v = φ.obj (ι s • v)
this : (↑(φ.map e) : S) = (↑e : S)
⊢ (↑(φ.map e) : S) = s

Tactic:
this
-- Module: Mathlib.Combinatorics.Quiver.Schreier
Goal:
V : Type u_1
M : Type u_2
inst : Group M
inst_1 : MulAction M V
S : Type u_3
ι : S → M
W : Type u_4
inst_2 : MulAction M W
φ : Prefunctor.{u_3, u_3, u_1, u_4} (SchreierGraph V ι) (SchreierGraph W ι)
φm : φ ⋙q labelling W ι = labelling V ι
v : SchreierGraph V ι
s : S
e : v ⟶ ι s • v := Subtype.mk (p := fun (s_1 : S) ↦ ι s_1 • v = ι s • v) s ⋯
h : ι (↑(φ.map e) : S) • φ.obj v = φ.obj (ι s • v)
this : (↑(φ.map e) : S) = (↑e : S)
⊢ (↑(φ.map e) : S) = s

Tactic:
exact this
-- Module: Mathlib.Combinatorics.Quiver.Schreier
Goal:
V : Type u_1
M : Type u_2
inst : Group M
inst_1 : MulAction M V
S : Type u_3
ι : S → M
W : Type u_4
inst_2 : MulAction M W
φ : Prefunctor.{u_3, u_3, u_1, u_4} (SchreierGraph V ι) (SchreierGraph W ι)
φm : φ ⋙q labelling W ι = labelling V ι
v : SchreierGraph V ι
s : S
e : v ⟶ ι s • v := Subtype.mk (p := fun (s_1 : S) ↦ ι s_1 • v = ι s • v) s ⋯
h : ι (↑(φ.map e) : S) • φ.obj v = φ.obj (ι s • v)
⊢ (↑(φ.map e) : S) = s

Tactic:
have label_eq : (φ.map e).val = s := by
    -- `φm` says `φ ⋙q labelling = labelling`
    -- So `(φ ⋙q labelling).map e = labelling.map e`
    have : (φ ⋙q labelling W ι).map e = (labelling V ι).map e := by
      rw [φm]
    simp only [Prefunctor.comp_map, labelling_map] at this
    exact this
-- Module: Mathlib.Combinatorics.Quiver.Schreier
Goal:
V : Type u_1
M : Type u_2
inst : Group M
inst_1 : MulAction M V
S : Type u_3
ι : S → M
W : Type u_4
inst_2 : MulAction M W
φ : Prefunctor.{u_3, u_3, u_1, u_4} (SchreierGraph V ι) (SchreierGraph W ι)
φm : φ ⋙q labelling W ι = labelling V ι
v : SchreierGraph V ι
s : S
e : v ⟶ ι s • v := Subtype.mk (p := fun (s_1 : S) ↦ ι s_1 • v = ι s • v) s ⋯
h : ι (↑(φ.map e) : S) • φ.obj v = φ.obj (ι s • v)
label_eq : (↑(φ.map e) : S) = s
⊢ ι s • φ.obj v = φ.obj (ι s • v)

Tactic:
rw [label_eq] at h
-- Module: Mathlib.Combinatorics.Quiver.Schreier
Goal:
V : Type u_1
M : Type u_2
inst : Group M
inst_1 : MulAction M V
S : Type u_3
ι : S → M
W : Type u_4
inst_2 : MulAction M W
φ : Prefunctor.{u_3, u_3, u_1, u_4} (SchreierGraph V ι) (SchreierGraph W ι)
φm : φ ⋙q labelling W ι = labelling V ι
v : SchreierGraph V ι
s : S
e : v ⟶ ι s • v := Subtype.mk (p := fun (s_1 : S) ↦ ι s_1 • v = ι s • v) s ⋯
h : ι (↑(φ.map e) : S) • φ.obj v = φ.obj (ι s • v)
label_eq : (↑(φ.map e) : S) = s
h₁ : ι s • φ.obj v = φ.obj (ι s • v)
⊢ (↑(φ.map e) : S) = s

Tactic:
rw [label_eq] at h
-- Module: Mathlib.Combinatorics.Quiver.Schreier
Goal:
V : Type u_1
M : Type u_2
inst : Group M
inst_1 : MulAction M V
S : Type u_3
ι : S → M
W : Type u_4
inst_2 : MulAction M W
φ : Prefunctor.{u_3, u_3, u_1, u_4} (SchreierGraph V ι) (SchreierGraph W ι)
φm : φ ⋙q labelling W ι = labelling V ι
v : SchreierGraph V ι
s : S
e : v ⟶ ι s • v := Subtype.mk (p := fun (s_1 : S) ↦ ι s_1 • v = ι s • v) s ⋯
h : ι s • φ.obj v = φ.obj (ι s • v)
label_eq : (↑(φ.map e) : S) = s
⊢ φ.obj (ι s • v) = ι s • φ.obj v

Tactic:
h.symm

Premises used: Eq.symm
-- Module: Mathlib.Combinatorics.Quiver.Schreier
Goal:
V : Type u_1
M : Type u_2
inst : Group M
inst_1 : MulAction M V
S : Type u_3
ι : S → M
W : Type u_4
inst_2 : MulAction M W
φ : Prefunctor.{u_3, u_3, u_1, u_4} (SchreierGraph V ι) (SchreierGraph W ι)
φm : φ ⋙q labelling W ι = labelling V ι
v : SchreierGraph V ι
s : S
e : v ⟶ ι s • v := Subtype.mk (p := fun (s_1 : S) ↦ ι s_1 • v = ι s • v) s ⋯
h : ι s • φ.obj v = φ.obj (ι s • v)
label_eq : (↑(φ.map e) : S) = s
⊢ φ.obj (ι s • v) = ι s • φ.obj v

Tactic:
exact h.symm

Premises used: Eq.symm
-- Module: Mathlib.Combinatorics.Quiver.SingleObj
Goal:
α : Type u_1
x y : SingleObj α
⊢ x = y

Tactic:
Unit.ext x y

Premises used: Quiver.SingleObj, Unit.ext
-- Module: Mathlib.Combinatorics.Quiver.SingleObj
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := SingleObj α ⥤q SingleObj α)
    ((toPrefunctor : (a : α → α) → SingleObj α ⥤q SingleObj α) id : SingleObj α ⥤q SingleObj α)
    (𝟭q (SingleObj α) : SingleObj α ⥤q SingleObj α)

Tactic:
rfl

Premises used: Prefunctor.id, rfl
-- Module: Mathlib.Combinatorics.Quiver.SingleObj
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := α → α)
    ((Equiv.symm toPrefunctor : (a : SingleObj α ⥤q SingleObj α) → α → α) (𝟭q (SingleObj α)) : α → α) (id : (a : α) → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Quiver.SingleObj
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
⊢ Eq (α := Prefunctor.{u_1, u_3, 0, 0} (SingleObj α) (SingleObj γ))
    ((toPrefunctor : (a : α → γ) → SingleObj α ⥤q SingleObj γ) (g ∘ f) :
      Prefunctor.{u_1, u_3, 0, 0} (SingleObj α) (SingleObj γ))
    (Prefunctor.comp.{0, 0, 0, u_1, u_2, u_3} (V := SingleObj β)
        ((toPrefunctor : (a : α → β) → SingleObj α ⥤q SingleObj β) f)
        ((toPrefunctor : (a : β → γ) → SingleObj β ⥤q SingleObj γ) g) :
      Prefunctor.{u_1, u_3, 0, 0} (SingleObj α) (SingleObj γ))

Tactic:
rfl

Premises used: Prefunctor.comp, rfl
-- Module: Mathlib.Combinatorics.Quiver.SingleObj
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Prefunctor.{u_1, u_2, 0, 0} (SingleObj α) (SingleObj β)
g : Prefunctor.{u_2, u_3, 0, 0} (SingleObj β) (SingleObj γ)
⊢ Eq (α := α → γ) ((Equiv.symm toPrefunctor : (a : SingleObj α ⥤q SingleObj γ) → α → γ) (f ⋙q g) : α → γ)
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β)
        ((Equiv.symm toPrefunctor : (a : SingleObj β ⥤q SingleObj γ) → β → γ) g)
        ((Equiv.symm toPrefunctor : (a : SingleObj α ⥤q SingleObj β) → α → β) f) :
      α → γ)

Tactic:
simp only [Equiv.symm_apply_eq, toPrefunctor_comp, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, Equiv.symm_apply_eq, Quiver.SingleObj.toPrefunctor_comp
-- Module: Mathlib.Combinatorics.Quiver.SingleObj
Goal:
α : Type u_1
x : SingleObj α
⊢ Eq.{u_1 + 1} (α := Path (star α) (star α)) (listToPath (pathToList Path.nil)) (Path.cast ⋯ ⋯ Path.nil)

Tactic:
rfl