awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ReflQuiver (goal)
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
X X' : V
hX : X = X'
⊢ Eq.{u_2 + 1} (α := X' ⟶ X') (Quiver.homOfEq (𝟙rq X) hX hX) (𝟙rq X')
have subst : Eq.{u_2 + 1} (α := X ⟶ X) (Quiver.homOfEq (𝟙rq X) sorry sorry) (𝟙rq X)
Tactic: subst hX
Cleared hypotheses: X', hX
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ReflQuiver (goal)
Goal:
V : Type u
inst : ReflQuiver.{v₁, u} V
W : Type u₂
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 =
      Eq.recOn (motive := fun (x : W) (x_1 : G.obj Y = x) ↦ F.obj X ⟶ x) ⋯
        (Eq.recOn (motive := fun (x : W) (x_1 : G.obj X = x) ↦ x ⟶ G.obj Y) ⋯ (G.map f))
⊢ F = G
have obtain : ∀ (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))
  (h_obj :
    ∀ (X : V), { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X = G.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 : G.obj Y = x) ↦
          { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X ⟶ x) sorry
          (Eq.recOn (motive := fun (x : W) (x_1 : G.obj X = x) ↦ x ⟶ G.obj Y) sorry (G.map f))),
  { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W } = G
Tactic: obtain ⟨⟨F_obj⟩⟩ := F
Cleared hypotheses: F, h_obj, h_map
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ReflQuiver (goal)
Goal:
V : Type u
inst : ReflQuiver.{v₁, u} V
W : Type u₂
inst_1 : ReflQuiver.{v₂, u₂} W
G : ReflPrefunctor.{v₁, v₂, u, u₂} V 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)
h_obj : ∀ (X : V), { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X = G.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 : G.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 : G.obj X = x) ↦ x ⟶ G.obj Y) ⋯ (G.map f))
⊢ { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W } = G
have obtain : ∀ (G_obj : V → W) (map_1 : {X Y : V} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y))
  (map_id_1 :
    ∀ (X : V),
      { obj := G_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.map (𝟙rq X) =
        𝟙rq ({ obj := G_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 := G_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 := G_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) sorry
          (Eq.recOn (motive :=
            fun (x : W)
              (x_1 :
                { obj := G_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X = x) ↦
            x ⟶ { obj := G_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj Y) sorry
            ({ obj := G_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.map f))),
  { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W } =
    { obj := G_obj, map := @map_1, map_id := map_id_1 }
Tactic: obtain ⟨⟨G_obj⟩⟩ := G
Cleared hypotheses: G, h_obj, h_map
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ReflQuiver (goal)
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))
⊢ { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W } =
    { obj := F_obj, map := @map_1, map_id := map_id_1 }
have e_toPrefunctor : @map = @map_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ReflQuiver (goal)
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))
⊢ @map = @map_1
have e_toPrefunctor : ∀ (X Y : V) (f : X ⟶ Y), map f = map_1 f
Tactic: funext X Y f
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ReflQuiver (goal)
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) ⋯ ⋯
⊢ F = G
have 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) sorry sorry),
  { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W } = G
Tactic: obtain ⟨Fpre, Fid⟩ := F
Cleared hypotheses: F, h_obj, h_map
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ReflQuiver (goal)
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) ⋯ ⋯
⊢ { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W } = G
have 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) sorry sorry),
  { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W } = { toPrefunctor := Gpre, map_id := Gid }
Tactic: obtain ⟨Gpre, Gid⟩ := G
Cleared hypotheses: G, h_obj, h_map
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ReflQuiver (goal)
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) ⋯ ⋯
⊢ { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W } = { toPrefunctor := Gpre, map_id := Gid }
have 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) sorry sorry),
  { toPrefunctor := Fpre, map_id := Fid : ReflPrefunctor.{v, v, u, u} V W } = { toPrefunctor := Fpre, map_id := Gid }
Tactic: obtain rfl : Fpre = Gpre := Prefunctor.ext' (V := V) (W := W) h_obj h_map
Cleared hypotheses: Gpre, Gid, h_obj, h_map
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ReflQuiver (goal)
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
⊢ F.obj X = G.obj X
have refl : F.obj X = F.obj X
Tactic: cases e
Cleared hypotheses: G, e
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ReflQuiver (goal)
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
⊢ Quiver.homOfEq (F.map f) ⋯ ⋯ = G.map f
have subst : Quiver.homOfEq (F.map f) sorry sorry = F.map f
Tactic: subst e
Cleared hypotheses: G, e
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Schreier (goal)
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 = a • b • x
have toVertex : ((a * b) • x).toVertex = (a • b • x).toVertex
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Schreier (goal)
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 = x
have toVertex : (HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 x).toVertex = x.toVertex
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Schreier (goal)
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
⊢ 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))
have 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 sorry))
  (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]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Schreier (goal)
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
have rw : (ι s)⁻¹ • ι s • v = v
Tactic: rw [← hs, inv_smul_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Schreier (goal)
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
⊢ (ι s)⁻¹ • x = v
have rw₁ : v = v
Tactic: rw [← hs, inv_smul_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Schreier (hypothesis)
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
⊢ 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))
have this : (ι s)⁻¹ • x = v
Tactic: have : (ι s)⁻¹ • x = v := by rw [← hs, inv_smul_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Schreier (goal)
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
⊢ 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))
have 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 sorry))
    (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: subst this
Cleared hypotheses: v, hs, this
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Schreier (hypothesis)
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 ⋯
⊢ φ.obj (ι s • v) = ι s • φ.obj v
have h : ι (↑(φ.map e) : S) • φ.obj v = φ.obj (ι s • v)
Tactic: have h := (φ.map e).property
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Schreier (goal)
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
have rw : Eq (α := Prefunctor.obj (labelling V ι) v ⟶ Prefunctor.obj (labelling V ι) (ι s • v)) (Prefunctor.map (labelling V ι) e)
  (Prefunctor.map (labelling V ι) e)
Tactic: rw [φm]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Schreier (hypothesis)
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
have this : (φ ⋙q labelling W ι).map e = Prefunctor.map (labelling V ι) e
Tactic: have : (φ ⋙q labelling W ι).map e = (labelling V ι).map e := by
      rw [φm]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Schreier (hypothesis)
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)
⊢ φ.obj (ι s • v) = ι s • φ.obj v
have label_eq : (↑(φ.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
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Schreier (hypothesis)
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
⊢ φ.obj (ι s • v) = ι s • φ.obj v
have h₁ : ι s • φ.obj v = φ.obj (ι s • v)
Tactic: rw [label_eq] at h
Cleared hypotheses: h, label_eq
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.SingleObj (goal)
Goal:
α : Type u_1
x b c : SingleObj α
a : Path (star α) b
a_1 : b ⟶ c
ih : listToPath (pathToList a) = Path.cast ⋯ ⋯ a
⊢ listToPath (pathToList (a.cons a_1)) = Path.cast ⋯ ⋯ (a.cons a_1)
have cons : (listToPath (pathToList a)).cons a_1 = a.cons a_1
Tactic: dsimp [pathToList] at *
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.SingleObj (goal)
Goal:
α : Type u_1
x b c : SingleObj α
a : Path (star α) b
a_1 : b ⟶ c
ih : listToPath (pathToList a) = a
⊢ (listToPath (pathToList a)).cons a_1 = a.cons a_1
have cons : a.cons a_1 = a.cons a_1
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.SingleObj (goal)
Goal:
α : Type u_1
x : SingleObj α
p : Path (star α) x
⊢ listToPath (pathToList p) = Path.cast ⋯ ⋯ p
have nil : Eq.{u_1 + 1} (α := Path (star α) (star α)) (listToPath (pathToList Path.nil)) (Path.cast sorry sorry Path.nil)
Tactic: induction p with
  | nil => rfl
  | cons _ _ ih => dsimp [pathToList] at *; rw [ih]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.SingleObj (goal)
Goal:
α : Type u_1
x : SingleObj α
p : Path (star α) x
nil : Eq.{u_1 + 1} (α := Path (star α) (star α)) (listToPath (pathToList Path.nil)) (Path.cast ⋯ ⋯ Path.nil)
⊢ listToPath (pathToList p) = Path.cast ⋯ ⋯ p
have cons : ∀ {b c : SingleObj α} (a : Path (star α) b) (a_1 : b ⟶ c) (ih : listToPath (pathToList a) = Path.cast sorry sorry a),
  listToPath (pathToList (a.cons a_1)) = Path.cast sorry sorry (a.cons a_1)
Tactic: induction p with
  | nil => rfl
  | cons _ _ ih => dsimp [pathToList] at *; rw [ih]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.SingleObj (goal)
Goal:
α : Type u_1
a : α
l : List α
ih : pathToList (listToPath l) = l
⊢ a :: pathToList (listToPath l) = a :: l
have cons : a :: l = a :: l
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.SingleObj (goal)
Goal:
α : Type u_1
l : List α
⊢ pathToList (listToPath l) = l
have nil : Eq.{u_1 + 1} (α := List α) (pathToList (listToPath [])) []
Tactic: induction l with
  | nil => rfl
  | cons a l ih => change a :: pathToList (listToPath l) = a :: l; rw [ih]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.SingleObj (goal)
Goal:
α : Type u_1
l : List α
nil : Eq.{u_1 + 1} (α := List α) (pathToList (listToPath [])) []
⊢ pathToList (listToPath l) = l
have cons : ∀ (a : α) (l : List α) (ih : pathToList (listToPath l) = l), pathToList (listToPath (a :: l)) = a :: l
Tactic: induction l with
  | nil => rfl
  | cons a l ih => change a :: pathToList (listToPath l) = a :: l; rw [ih]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Symmetric (goal)
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
h : HasInvolutiveReverse.{v, u_2} V
a b : V
f g : a ⟶ b
⊢ reverse f = reverse g ↔ f = g
have mp : reverse f = reverse g → f = g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Symmetric (goal)
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
h : HasInvolutiveReverse.{v, u_2} V
a b : V
f g : a ⟶ b
mp : reverse f = reverse g → f = g
⊢ reverse f = reverse g ↔ f = g
have mpr : f = g → reverse f = reverse g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Symmetric (goal)
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
h : HasInvolutiveReverse.{v, u_2} V
a b : V
f : a ⟶ b
g : b ⟶ a
⊢ f = reverse g ↔ reverse f = g
have rw : reverse f = reverse (reverse g) ↔ reverse f = g
Tactic: rw [← reverse_inj, reverse_reverse]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Symmetric (goal)
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
h : HasInvolutiveReverse.{v, u_2} V
a b : V
f : a ⟶ b
g : b ⟶ a
rw : reverse f = reverse (reverse g) ↔ reverse f = g
⊢ f = reverse g ↔ reverse f = g
have rw₁ : reverse f = g ↔ reverse f = g
Tactic: rw [← reverse_inj, reverse_reverse]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Symmetric (goal)
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
inst_1 : HasReverse.{v, u_2} V
a b c : V
p : Path.{v, u_2} a b
q : Path.{v, u_2} b c
⊢ (p.comp q).reverse = q.reverse.comp p.reverse
have nil : (p.comp nil).reverse = comp (reverse nil) p.reverse
Tactic: induction q with
  | nil => simp
  | cons _ _ h => simp [h]
Cleared hypotheses: q