no goals
α : Type u
inst✝ : Group α
x✝¹ : prod [] = 1
x✝ : ℕ
⊢ prod (rotate [] x✝) = 1
simp
α : Type u
inst✝ : Group α
a : α
l : List α
hl : prod (a :: l) = 1
n : ℕ
this : n % length (a :: l) ≤ length (a :: l)
⊢ prod (rotate (a :: l) n) = 1
α : Type u
inst✝ : Group α
a : α
l : List α
hl : prod (a :: l) = 1
n : ℕ
⊢ prod (rotate (a :: l) n) = 1
have : n % List.length (a :: l) ≤ List.length (a :: l) := le_of_lt (Nat.mod_lt _ (by simp))
α : Type u
inst✝ : Group α
a : α
l : List α
n : ℕ
hl : prod (take (n % length (a :: l)) (a :: l) ++ drop (n % length (a :: l)) (a :: l)) = 1
this : n % length (a :: l) ≤ length (a :: l)
⊢ prod (rotate (a :: l) n) = 1
α : Type u
inst✝ : Group α
a : α
l : List α
hl : prod (a :: l) = 1
n : ℕ
this : n % length (a :: l) ≤ length (a :: l)
⊢ prod (rotate (a :: l) n) = 1
rw [← List.take_append_drop (n % List.length (a :: l)) (a :: l)] at hl
no goals
α : Type u
inst✝ : Group α
a : α
l : List α
n : ℕ
hl : prod (take (n % length (a :: l)) (a :: l) ++ drop (n % length (a :: l)) (a :: l)) = 1
this : n % length (a :: l) ≤ length (a :: l)
⊢ prod (rotate (a :: l) n) = 1
rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq, ←
  one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_self, mul_one]
no goals
α : Type u
inst✝ : Group α
a : α
l : List α
hl : prod (a :: l) = 1
n : ℕ
⊢ length (a :: l) > 0
simp