α : Type ?u.553591
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
n : ℕ
⊢ ∀ (x : Vector G 1), Vector.head x = 1 → x = 1 ::ᵥ Vector.nil
α : Type ?u.553591
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
n : ℕ
⊢ vectorsProdEqOne G 1 = {1 ::ᵥ Vector.nil}
simp_rw [Set.eq_singleton_iff_unique_mem, mem_iff, Vector.toList_singleton, List.prod_singleton,
  Vector.head_cons, true_and]
no goals
α : Type ?u.553591
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
n : ℕ
⊢ ∀ (x : Vector G 1), Vector.head x = 1 → x = 1 ::ᵥ Vector.nil
exact fun v hv => v.cons_head_tail.symm.trans (congr_arg₂ Vector.cons hv v.tail.eq_nil)