awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
h_sc : IsStronglyConnected.{u_2, u_3} V
i₀ j₀ : V
e₀ : i₀ ⟶ j₀
i j : V
p₁ : Path.{u_3, u_2} i i₀
p₂ : Path.{u_3, u_2} j₀ j
p : Path.{u_3, u_2} i j := p₁.comp (e₀.toPath.comp p₂)
⊢ 0 < p.length

Tactic:
simpa [p, Path.length_comp, Nat.add_comm, Nat.add_left_comm, Nat.add_assoc] using
      Nat.succ_pos (p₁.length + p₂.length)

Premises used: Nat.add_left_comm, HAdd.hAdd, Quiver.Path.length, Nat.succ_pos, Nat.add_assoc, Quiver.Path.length_comp, Nat.add_comm
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
h_sc : IsStronglyConnected.{u_2, u_3} V
i₀ j₀ : V
e₀ : i₀ ⟶ j₀
i j : V
p₁ : Path.{u_3, u_2} i i₀
p₂ : Path.{u_3, u_2} j₀ j
p : Path.{u_3, u_2} i j := p₁.comp (e₀.toPath.comp p₂)
⊢ 0 < p.length

Tactic:
have hp_pos : 0 < p.length := by
    simpa [p, Path.length_comp, Nat.add_comm, Nat.add_left_comm, Nat.add_assoc] using
      Nat.succ_pos (p₁.length + p₂.length)
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
h_sc : IsStronglyConnected.{u_2, u_3} V
i₀ j₀ : V
e₀ : i₀ ⟶ j₀
i j : V
p₁ : Path.{u_3, u_2} i i₀
p₂ : Path.{u_3, u_2} j₀ j
p : Path.{u_3, u_2} i j := p₁.comp (e₀.toPath.comp p₂)
hp_pos : 0 < p.length
⊢ ∃ (p : Path.{u_3, u_2} i j), 0 < p.length

Tactic:
⟨p, hp_pos⟩

Premises used: Exists.intro
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
h_sc : IsStronglyConnected.{u_2, u_3} V
i₀ j₀ : V
e₀ : i₀ ⟶ j₀
i j : V
p₁ : Path.{u_3, u_2} i i₀
p₂ : Path.{u_3, u_2} j₀ j
p : Path.{u_3, u_2} i j := p₁.comp (e₀.toPath.comp p₂)
hp_pos : 0 < p.length
⊢ ∃ (p : Path.{u_3, u_2} i j), 0 < p.length

Tactic:
exact ⟨p, hp_pos⟩
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
u v : U
e : u ⟶ v
⊢ φ.star u (Star.mk e) = Star.mk (φ.map e)

Tactic:
rfl

Premises used: Prefunctor.star, rfl
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
u v : U
e : u ⟶ v
⊢ φ.costar v (Costar.mk e) = Costar.mk (φ.map e)

Tactic:
rfl

Premises used: Prefunctor.costar, rfl
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_3
inst_1 : Quiver.{v, u_3} V
φ : Prefunctor.{u, v, u_1, u_3} U V
W : Type u_2
inst_2 : Quiver.{w, u_2} W
ψ : Prefunctor.{v, w, u_3, u_2} V W
u : U
⊢ (φ ⋙q ψ).star u = ψ.star (φ.obj u) ∘ φ.star u

Tactic:
rfl

Premises used: Prefunctor.star, rfl
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_3
inst_1 : Quiver.{v, u_3} V
φ : Prefunctor.{u, v, u_1, u_3} U V
W : Type u_2
inst_2 : Quiver.{w, u_2} W
ψ : Prefunctor.{v, w, u_3, u_2} V W
u : U
⊢ (φ ⋙q ψ).costar u = ψ.costar (φ.obj u) ∘ φ.costar u

Tactic:
rfl

Premises used: Prefunctor.costar, rfl
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
hφ : φ.IsCovering
u v : U
f g : u ⟶ v
he : Eq.{v + 1} (α := φ.obj u ⟶ φ.obj v) ((fun (f : u ⟶ v) ↦ φ.map f) f) ((fun (f : u ⟶ v) ↦ φ.map f) g)
⊢ φ.star u (Star.mk f) = φ.star u (Star.mk g)

Tactic:
simpa using he
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
hφ : φ.IsCovering
u v : U
f g : u ⟶ v
he : Eq.{v + 1} (α := φ.obj u ⟶ φ.obj v) ((fun (f : u ⟶ v) ↦ φ.map f) f) ((fun (f : u ⟶ v) ↦ φ.map f) g)
⊢ φ.star u (Star.mk f) = φ.star u (Star.mk g)

Tactic:
have : φ.star u (Quiver.Star.mk f) = φ.star u (Quiver.Star.mk g) := by simpa using he
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
hφ : φ.IsCovering
u v : U
f g : u ⟶ v
he : Eq.{v + 1} (α := φ.obj u ⟶ φ.obj v) ((fun (f : u ⟶ v) ↦ φ.map f) f) ((fun (f : u ⟶ v) ↦ φ.map f) g)
this : φ.star u (Star.mk f) = φ.star u (Star.mk g)
⊢ f = g

Tactic:
simpa using (hφ.star_bijective u).left this

Premises used: Prefunctor.IsCovering.star_bijective, And.left
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
W : Type u_3
inst_2 : Quiver.{w, u_3} W
ψ : Prefunctor.{v, w, u_2, u_3} V W
hφ : φ.IsCovering
hψ : ψ.IsCovering
⊢ (φ ⋙q ψ).IsCovering

Tactic:
⟨fun _ => (hψ.star_bijective _).comp (hφ.star_bijective _),
   fun _ => (hψ.costar_bijective _).comp (hφ.costar_bijective _)⟩

Premises used: Prefunctor.IsCovering.star_bijective, Prefunctor.IsCovering.costar_bijective, Prefunctor.IsCovering.mk, Function.Bijective.comp, Prefunctor.obj
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_3
inst : Quiver.{u, u_3} U
V : Type u_1
inst_1 : Quiver.{v, u_1} V
φ : Prefunctor.{u, v, u_3, u_1} U V
W : Type u_2
inst_2 : Quiver.{w, u_2} W
ψ : Prefunctor.{v, w, u_1, u_2} V W
hψ : ψ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
⊢ φ.IsCovering

Tactic:
⟨fun _ => (Bijective.of_comp_iff' (hψ.star_bijective _) _).mp (hφψ.star_bijective _),
   fun _ => (Bijective.of_comp_iff' (hψ.costar_bijective _) _).mp (hφψ.costar_bijective _)⟩

Premises used: Prefunctor.costar, Prefunctor.IsCovering.star_bijective, Prefunctor.IsCovering.costar_bijective, Function.Bijective.of_comp_iff', Iff.mp, Prefunctor.IsCovering.mk, Prefunctor.star, Prefunctor.obj
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
W : Type u_3
inst_2 : Quiver.{w, u_3} W
ψ : Prefunctor.{v, w, u_2, u_3} V W
hφ : φ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
φsur : Surjective φ.obj
⊢ ψ.IsCovering

Tactic:
⟨fun v => ?_, fun v => ?_⟩

Premises used: Prefunctor.IsCovering.mk
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
W : Type u_3
inst_2 : Quiver.{w, u_3} W
ψ : Prefunctor.{v, w, u_2, u_3} V W
hφ : φ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
φsur : Surjective φ.obj
refine_1 : ∀ (v : V), Bijective (ψ.star v)
refine_2 : ∀ (v : V), Bijective (ψ.costar v)
⊢ ψ.IsCovering

Tactic:
refine ⟨fun v => ?_, fun v => ?_⟩
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
W : Type u_3
inst_2 : Quiver.{w, u_3} W
ψ : Prefunctor.{v, w, u_2, u_3} V W
hφ : φ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
φsur : Surjective φ.obj
v : V
refine_1 : ∀ (u : U), Bijective (α := Star.{v, u_2} (φ.obj u)) (ψ.star (φ.obj u))
⊢ Bijective (ψ.star v)

Tactic:
obtain ⟨u, rfl⟩ := φsur v

Premises used: rfl
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
W : Type u_3
inst_2 : Quiver.{w, u_3} W
ψ : Prefunctor.{v, w, u_2, u_3} V W
hφ : φ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
φsur : Surjective φ.obj
v : V
refine_2 : ∀ (u : U), Bijective (α := Costar.{v, u_2} (φ.obj u)) (ψ.costar (φ.obj u))
⊢ Bijective (ψ.costar v)

Tactic:
obtain ⟨u, rfl⟩ := φsur v

Premises used: rfl
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
W : Type u_3
inst_2 : Quiver.{w, u_3} W
ψ : Prefunctor.{v, w, u_2, u_3} V W
hφ : φ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
φsur : Surjective φ.obj
u : U
⊢ Bijective (α := Star.{v, u_2} (φ.obj u)) (ψ.star (φ.obj u))

Tactic:
(Bijective.of_comp_iff _ (hφ.star_bijective u)).mp (hφψ.star_bijective u)

Premises used: Prefunctor.IsCovering.star_bijective, Function.Bijective.of_comp_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
W : Type u_3
inst_2 : Quiver.{w, u_3} W
ψ : Prefunctor.{v, w, u_2, u_3} V W
hφ : φ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
φsur : Surjective φ.obj
u : U
⊢ Bijective (α := Costar.{v, u_2} (φ.obj u)) (ψ.costar (φ.obj u))

Tactic:
(Bijective.of_comp_iff _ (hφ.costar_bijective u)).mp (hφψ.costar_bijective u)

Premises used: Function.Bijective.of_comp_iff, Prefunctor.IsCovering.costar_bijective, Iff.mp
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
W : Type u_3
inst_2 : Quiver.{w, u_3} W
ψ : Prefunctor.{v, w, u_2, u_3} V W
hφ : φ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
φsur : Surjective φ.obj
u : U
⊢ Bijective (α := Star.{v, u_2} (φ.obj u)) (ψ.star (φ.obj u))

Tactic:
exacts [(Bijective.of_comp_iff _ (hφ.star_bijective u)).mp (hφψ.star_bijective u),
    (Bijective.of_comp_iff _ (hφ.costar_bijective u)).mp (hφψ.costar_bijective u)]
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
u : U
rw :
  (⇑(Quiver.symmetrifyStar (φ.obj u)) : (a : Star (Symmetrify.of.obj (φ.obj u))) → Star (φ.obj u) ⊕ Costar (φ.obj u)) ∘
      φ.symmetrify.star u =
    Sum.map (φ.star u) (φ.costar u) ∘
      (⇑(Quiver.symmetrifyStar u) : (a : Star (Symmetrify.of.obj u)) → Star u ⊕ Costar u)
⊢ φ.symmetrify.star u =
    (⇑(Equiv.symm (Quiver.symmetrifyStar (φ.obj u))) :
        (a : Star (φ.obj u) ⊕ Costar (φ.obj u)) → Star (Symmetrify.of.obj (φ.obj u))) ∘
      Sum.map (φ.star u) (φ.costar u) ∘
        (⇑(Quiver.symmetrifyStar u) : (a : Star (Symmetrify.of.obj u)) → Star u ⊕ Costar u)

Tactic:
rw [Equiv.eq_symm_comp (e := Quiver.symmetrifyStar (φ.obj u))]

Premises used: Quiver.symmetrifyStar, Equiv.eq_symm_comp, Prefunctor.obj
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
u : U
h :
  ∀ (v : Symmetrify U) (f : u ⟶ v),
    ((⇑(Quiver.symmetrifyStar (φ.obj u)) :
            (a : Star (Symmetrify.of.obj (φ.obj u))) → Star (φ.obj u) ⊕ Costar (φ.obj u)) ∘
          φ.symmetrify.star u)
        (Sigma.mk (β := fun (v : Symmetrify U) ↦ u ⟶ v) v (Sum.inl f)) =
      Function.comp (α := Star.{u, u_1} (obj.{u, u, u_1, u_1} Symmetrify.of u)) (Sum.map (φ.star u) (φ.costar u))
        (⇑(Quiver.symmetrifyStar u) : (a : Star (Symmetrify.of.obj u)) → Star u ⊕ Costar u)
        (Sigma.mk (β := fun (v : Symmetrify U) ↦ u ⟶ v) v (Sum.inl f))
h₁ :
  ∀ (v : Symmetrify U) (g : v ⟶ u),
    ((⇑(Quiver.symmetrifyStar (φ.obj u)) :
            (a : Star (Symmetrify.of.obj (φ.obj u))) → Star (φ.obj u) ⊕ Costar (φ.obj u)) ∘
          φ.symmetrify.star u)
        (Sigma.mk (β := fun (v : Symmetrify U) ↦ u ⟶ v) v (Sum.inr g)) =
      Function.comp (α := Star.{u, u_1} (obj.{u, u, u_1, u_1} Symmetrify.of u)) (Sum.map (φ.star u) (φ.costar u))
        (⇑(Quiver.symmetrifyStar u) : (a : Star (Symmetrify.of.obj u)) → Star u ⊕ Costar u)
        (Sigma.mk (β := fun (v : Symmetrify U) ↦ u ⟶ v) v (Sum.inr g))
⊢ (⇑(Quiver.symmetrifyStar (φ.obj u)) : (a : Star (Symmetrify.of.obj (φ.obj u))) → Star (φ.obj u) ⊕ Costar (φ.obj u)) ∘
      φ.symmetrify.star u =
    Sum.map (φ.star u) (φ.costar u) ∘
      (⇑(Quiver.symmetrifyStar u) : (a : Star (Symmetrify.of.obj u)) → Star u ⊕ Costar u)

Tactic:
ext ⟨v, f | g⟩
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
u : U
v : Symmetrify U
f : u ⟶ v
⊢ Sum.map
      (Sigma.mk (β := fun (i : Symmetrify V) ↦ obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u) ⟶ i)
        ((φ.symmetrify.star u (Sigma.mk (β := fun (v : Symmetrify U) ↦ u ⟶ v) v (Sum.inl f))).fst (β :=
          fun (i : Symmetrify V) ↦
          (obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u) ⟶ i) ⊕ (i ⟶ obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u)))))
      (Sigma.mk (β := fun (i : Symmetrify V) ↦ i ⟶ obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u))
        ((φ.symmetrify.star u (Sigma.mk (β := fun (v : Symmetrify U) ↦ u ⟶ v) v (Sum.inl f))).fst (β :=
          fun (i : Symmetrify V) ↦
          (obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u) ⟶ i) ⊕ (i ⟶ obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u)))))
      ((φ.symmetrify.star u (Sigma.mk (β := fun (v : Symmetrify U) ↦ u ⟶ v) v (Sum.inl f))).snd (β :=
        fun (i : Symmetrify V) ↦
        (obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u) ⟶ i) ⊕ (i ⟶ obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u)))) =
    Sum.map (φ.star u) (φ.costar u)
      (Sum.map
        (Sigma.mk (β := fun (i : Symmetrify U) ↦ obj.{u, u, u_1, u_1} Symmetrify.of u ⟶ i)
          (Sigma.fst (β := fun (i : Symmetrify U) ↦
            (obj.{u, u, u_1, u_1} Symmetrify.of u ⟶ i) ⊕ (i ⟶ obj.{u, u, u_1, u_1} Symmetrify.of u))
            (Sigma.mk (β := fun (v : Symmetrify U) ↦ u ⟶ v) v (Sum.inl f))))
        (Sigma.mk (β := fun (i : Symmetrify U) ↦ i ⟶ obj.{u, u, u_1, u_1} Symmetrify.of u)
          (Sigma.fst (β := fun (i : Symmetrify U) ↦
            (obj.{u, u, u_1, u_1} Symmetrify.of u ⟶ i) ⊕ (i ⟶ obj.{u, u, u_1, u_1} Symmetrify.of u))
            (Sigma.mk (β := fun (v : Symmetrify U) ↦ u ⟶ v) v (Sum.inl f))))
        (Sigma.snd (β := fun (i : Symmetrify U) ↦
          (obj.{u, u, u_1, u_1} Symmetrify.of u ⟶ i) ⊕ (i ⟶ obj.{u, u, u_1, u_1} Symmetrify.of u))
          (Sigma.mk (β := fun (v : Symmetrify U) ↦ u ⟶ v) v (Sum.inl f))))

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
u : U
v : Symmetrify U
g : v ⟶ u
⊢ Sum.map
      (Sigma.mk (β := fun (i : Symmetrify V) ↦ obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u) ⟶ i)
        ((φ.symmetrify.star u (Sigma.mk (β := fun (v : Symmetrify U) ↦ u ⟶ v) v (Sum.inr g))).fst (β :=
          fun (i : Symmetrify V) ↦
          (obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u) ⟶ i) ⊕ (i ⟶ obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u)))))
      (Sigma.mk (β := fun (i : Symmetrify V) ↦ i ⟶ obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u))
        ((φ.symmetrify.star u (Sigma.mk (β := fun (v : Symmetrify U) ↦ u ⟶ v) v (Sum.inr g))).fst (β :=
          fun (i : Symmetrify V) ↦
          (obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u) ⟶ i) ⊕ (i ⟶ obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u)))))
      ((φ.symmetrify.star u (Sigma.mk (β := fun (v : Symmetrify U) ↦ u ⟶ v) v (Sum.inr g))).snd (β :=
        fun (i : Symmetrify V) ↦
        (obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u) ⟶ i) ⊕ (i ⟶ obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u)))) =
    Sum.map (φ.star u) (φ.costar u)
      (Sum.map
        (Sigma.mk (β := fun (i : Symmetrify U) ↦ obj.{u, u, u_1, u_1} Symmetrify.of u ⟶ i)
          (Sigma.fst (β := fun (i : Symmetrify U) ↦
            (obj.{u, u, u_1, u_1} Symmetrify.of u ⟶ i) ⊕ (i ⟶ obj.{u, u, u_1, u_1} Symmetrify.of u))
            (Sigma.mk (β := fun (v : Symmetrify U) ↦ u ⟶ v) v (Sum.inr g))))
        (Sigma.mk (β := fun (i : Symmetrify U) ↦ i ⟶ obj.{u, u, u_1, u_1} Symmetrify.of u)
          (Sigma.fst (β := fun (i : Symmetrify U) ↦
            (obj.{u, u, u_1, u_1} Symmetrify.of u ⟶ i) ⊕ (i ⟶ obj.{u, u, u_1, u_1} Symmetrify.of u))
            (Sigma.mk (β := fun (v : Symmetrify U) ↦ u ⟶ v) v (Sum.inr g))))
        (Sigma.snd (β := fun (i : Symmetrify U) ↦
          (obj.{u, u, u_1, u_1} Symmetrify.of u ⟶ i) ⊕ (i ⟶ obj.{u, u, u_1, u_1} Symmetrify.of u))
          (Sigma.mk (β := fun (v : Symmetrify U) ↦ u ⟶ v) v (Sum.inr g))))

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
u : U
rw :
  (⇑(symmetrifyCostar (φ.obj u)) : (a : Costar (Symmetrify.of.obj (φ.obj u))) → Costar (φ.obj u) ⊕ Star (φ.obj u)) ∘
      φ.symmetrify.costar u =
    Sum.map (φ.costar u) (φ.star u) ∘ (⇑(symmetrifyCostar u) : (a : Costar (Symmetrify.of.obj u)) → Costar u ⊕ Star u)
⊢ φ.symmetrify.costar u =
    (⇑(Equiv.symm (symmetrifyCostar (φ.obj u))) :
        (a : Costar (φ.obj u) ⊕ Star (φ.obj u)) → Costar (Symmetrify.of.obj (φ.obj u))) ∘
      Sum.map (φ.costar u) (φ.star u) ∘ (⇑(symmetrifyCostar u) : (a : Costar (Symmetrify.of.obj u)) → Costar u ⊕ Star u)

Tactic:
rw [Equiv.eq_symm_comp (e := Quiver.symmetrifyCostar (φ.obj u))]

Premises used: Equiv.eq_symm_comp, Quiver.symmetrifyCostar, Prefunctor.obj
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
u : U
h :
  ∀ (v : Symmetrify U) (f : v ⟶ u),
    ((⇑(symmetrifyCostar (φ.obj u)) : (a : Costar (Symmetrify.of.obj (φ.obj u))) → Costar (φ.obj u) ⊕ Star (φ.obj u)) ∘
          φ.symmetrify.costar u)
        (Sigma.mk (β := fun (u_1 : Symmetrify U) ↦ u_1 ⟶ u) v (Sum.inl f)) =
      Function.comp (α := Costar.{u, u_1} (obj.{u, u, u_1, u_1} Symmetrify.of u)) (Sum.map (φ.costar u) (φ.star u))
        (⇑(symmetrifyCostar u) : (a : Costar (Symmetrify.of.obj u)) → Costar u ⊕ Star u)
        (Sigma.mk (β := fun (u_1 : Symmetrify U) ↦ u_1 ⟶ u) v (Sum.inl f))
h₁ :
  ∀ (v : Symmetrify U) (g : u ⟶ v),
    ((⇑(symmetrifyCostar (φ.obj u)) : (a : Costar (Symmetrify.of.obj (φ.obj u))) → Costar (φ.obj u) ⊕ Star (φ.obj u)) ∘
          φ.symmetrify.costar u)
        (Sigma.mk (β := fun (u_1 : Symmetrify U) ↦ u_1 ⟶ u) v (Sum.inr g)) =
      Function.comp (α := Costar.{u, u_1} (obj.{u, u, u_1, u_1} Symmetrify.of u)) (Sum.map (φ.costar u) (φ.star u))
        (⇑(symmetrifyCostar u) : (a : Costar (Symmetrify.of.obj u)) → Costar u ⊕ Star u)
        (Sigma.mk (β := fun (u_1 : Symmetrify U) ↦ u_1 ⟶ u) v (Sum.inr g))
⊢ (⇑(symmetrifyCostar (φ.obj u)) : (a : Costar (Symmetrify.of.obj (φ.obj u))) → Costar (φ.obj u) ⊕ Star (φ.obj u)) ∘
      φ.symmetrify.costar u =
    Sum.map (φ.costar u) (φ.star u) ∘ (⇑(symmetrifyCostar u) : (a : Costar (Symmetrify.of.obj u)) → Costar u ⊕ Star u)

Tactic:
ext ⟨v, f | g⟩
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
u : U
v : Symmetrify U
f : v ⟶ u
⊢ Sum.map
      (Sigma.mk (β := fun (i : Symmetrify V) ↦ i ⟶ obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u))
        ((φ.symmetrify.costar u (Sigma.mk (β := fun (u_1 : Symmetrify U) ↦ u_1 ⟶ u) v (Sum.inl f))).fst (β :=
          fun (i : Symmetrify V) ↦
          (i ⟶ obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u)) ⊕ (obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u) ⟶ i))))
      (Sigma.mk (β := fun (i : Symmetrify V) ↦ obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u) ⟶ i)
        ((φ.symmetrify.costar u (Sigma.mk (β := fun (u_1 : Symmetrify U) ↦ u_1 ⟶ u) v (Sum.inl f))).fst (β :=
          fun (i : Symmetrify V) ↦
          (i ⟶ obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u)) ⊕ (obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u) ⟶ i))))
      ((φ.symmetrify.costar u (Sigma.mk (β := fun (u_1 : Symmetrify U) ↦ u_1 ⟶ u) v (Sum.inl f))).snd (β :=
        fun (i : Symmetrify V) ↦
        (i ⟶ obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u)) ⊕ (obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u) ⟶ i))) =
    Sum.map (φ.costar u) (φ.star u)
      (Sum.map
        (Sigma.mk (β := fun (i : Symmetrify U) ↦ i ⟶ obj.{u, u, u_1, u_1} Symmetrify.of u)
          (Sigma.fst (β := fun (i : Symmetrify U) ↦
            (i ⟶ obj.{u, u, u_1, u_1} Symmetrify.of u) ⊕ (obj.{u, u, u_1, u_1} Symmetrify.of u ⟶ i))
            (Sigma.mk (β := fun (u_1 : Symmetrify U) ↦ u_1 ⟶ u) v (Sum.inl f))))
        (Sigma.mk (β := fun (i : Symmetrify U) ↦ obj.{u, u, u_1, u_1} Symmetrify.of u ⟶ i)
          (Sigma.fst (β := fun (i : Symmetrify U) ↦
            (i ⟶ obj.{u, u, u_1, u_1} Symmetrify.of u) ⊕ (obj.{u, u, u_1, u_1} Symmetrify.of u ⟶ i))
            (Sigma.mk (β := fun (u_1 : Symmetrify U) ↦ u_1 ⟶ u) v (Sum.inl f))))
        (Sigma.snd (β := fun (i : Symmetrify U) ↦
          (i ⟶ obj.{u, u, u_1, u_1} Symmetrify.of u) ⊕ (obj.{u, u, u_1, u_1} Symmetrify.of u ⟶ i))
          (Sigma.mk (β := fun (u_1 : Symmetrify U) ↦ u_1 ⟶ u) v (Sum.inl f))))

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
u : U
v : Symmetrify U
g : u ⟶ v
⊢ Sum.map
      (Sigma.mk (β := fun (i : Symmetrify V) ↦ i ⟶ obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u))
        ((φ.symmetrify.costar u (Sigma.mk (β := fun (u_1 : Symmetrify U) ↦ u_1 ⟶ u) v (Sum.inr g))).fst (β :=
          fun (i : Symmetrify V) ↦
          (i ⟶ obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u)) ⊕ (obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u) ⟶ i))))
      (Sigma.mk (β := fun (i : Symmetrify V) ↦ obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u) ⟶ i)
        ((φ.symmetrify.costar u (Sigma.mk (β := fun (u_1 : Symmetrify U) ↦ u_1 ⟶ u) v (Sum.inr g))).fst (β :=
          fun (i : Symmetrify V) ↦
          (i ⟶ obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u)) ⊕ (obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u) ⟶ i))))
      ((φ.symmetrify.costar u (Sigma.mk (β := fun (u_1 : Symmetrify U) ↦ u_1 ⟶ u) v (Sum.inr g))).snd (β :=
        fun (i : Symmetrify V) ↦
        (i ⟶ obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u)) ⊕ (obj.{v, v, u_2, u_2} Symmetrify.of (φ.obj u) ⟶ i))) =
    Sum.map (φ.costar u) (φ.star u)
      (Sum.map
        (Sigma.mk (β := fun (i : Symmetrify U) ↦ i ⟶ obj.{u, u, u_1, u_1} Symmetrify.of u)
          (Sigma.fst (β := fun (i : Symmetrify U) ↦
            (i ⟶ obj.{u, u, u_1, u_1} Symmetrify.of u) ⊕ (obj.{u, u, u_1, u_1} Symmetrify.of u ⟶ i))
            (Sigma.mk (β := fun (u_1 : Symmetrify U) ↦ u_1 ⟶ u) v (Sum.inr g))))
        (Sigma.mk (β := fun (i : Symmetrify U) ↦ obj.{u, u, u_1, u_1} Symmetrify.of u ⟶ i)
          (Sigma.fst (β := fun (i : Symmetrify U) ↦
            (i ⟶ obj.{u, u, u_1, u_1} Symmetrify.of u) ⊕ (obj.{u, u, u_1, u_1} Symmetrify.of u ⟶ i))
            (Sigma.mk (β := fun (u_1 : Symmetrify U) ↦ u_1 ⟶ u) v (Sum.inr g))))
        (Sigma.snd (β := fun (i : Symmetrify U) ↦
          (i ⟶ obj.{u, u, u_1, u_1} Symmetrify.of u) ⊕ (obj.{u, u, u_1, u_1} Symmetrify.of u ⟶ i))
          (Sigma.mk (β := fun (u_1 : Symmetrify U) ↦ u_1 ⟶ u) v (Sum.inr g))))

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
hφ : φ.IsCovering
⊢ φ.symmetrify.IsCovering

Tactic:
⟨fun u => ?_, fun u => ?_⟩

Premises used: Prefunctor.IsCovering.mk
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
hφ : φ.IsCovering
refine_1 : ∀ (u : Symmetrify U), Bijective (φ.symmetrify.star u)
refine_2 : ∀ (u : Symmetrify U), Bijective (φ.symmetrify.costar u)
⊢ φ.symmetrify.IsCovering

Tactic:
refine ⟨fun u => ?_, fun u => ?_⟩
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
hφ : φ.IsCovering
u : Symmetrify U
⊢ Bijective (φ.symmetrify.star u)

Tactic:
simp [φ.symmetrifyStar, φ.symmetrifyCostar, hφ.star_bijective u, hφ.costar_bijective u]

Premises used: Prefunctor.IsCovering.star_bijective, Prefunctor.IsCovering.costar_bijective, Prefunctor.symmetrifyStar, Prefunctor.symmetrifyCostar
-- Module: Mathlib.Combinatorics.Quiver.Covering
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
hφ : φ.IsCovering
u : Symmetrify U
⊢ Bijective (φ.symmetrify.costar u)

Tactic:
simp [φ.symmetrifyStar, φ.symmetrifyCostar, hφ.star_bijective u, hφ.costar_bijective u]

Premises used: Prefunctor.IsCovering.star_bijective, Prefunctor.IsCovering.costar_bijective, Prefunctor.symmetrifyStar, Prefunctor.symmetrifyCostar