ι : Type ?u.27087
α : Type ?u.27090
M : Type u_1
N : Type ?u.27096
P : Type ?u.27099
M₀ : Type ?u.27102
G : Type ?u.27105
R : Type ?u.27108
inst✝ : Monoid M
l : List M
⊢ op (prod l) = prod (reverse (map op l))
ι : Type ?u.27087
α : Type ?u.27090
M : Type u_1
N : Type ?u.27096
P : Type ?u.27099
M₀ : Type ?u.27102
G : Type ?u.27105
R : Type ?u.27108
inst✝ : Monoid M
⊢ ∀ (l : List M), op (prod l) = prod (reverse (map op l))
intro l
no goals
ι : Type ?u.27087
α : Type ?u.27090
M : Type u_1
N : Type ?u.27096
P : Type ?u.27099
M₀ : Type ?u.27102
G : Type ?u.27105
R : Type ?u.27108
inst✝ : Monoid M
l : List M
⊢ op (prod l) = prod (reverse (map op l))
induction l with
| nil => rfl
| cons x xs ih =>
rw [List.prod_cons, List.map_cons, List.reverse_cons', List.prod_concat, op_mul, ih]
no goals
case nil
ι : Type ?u.27087
α : Type ?u.27090
M : Type u_1
N : Type ?u.27096
P : Type ?u.27099
M₀ : Type ?u.27102
G : Type ?u.27105
R : Type ?u.27108
inst✝ : Monoid M
⊢ op (prod []) = prod (reverse (map op []))
rfl
no goals
case cons
ι : Type ?u.27087
α : Type ?u.27090
M : Type u_1
N : Type ?u.27096
P : Type ?u.27099
M₀ : Type ?u.27102
G : Type ?u.27105
R : Type ?u.27108
inst✝ : Monoid M
x : M
xs : List M
ih : op (prod xs) = prod (reverse (map op xs))
⊢ op (prod (x :: xs)) = prod (reverse (map op (x :: xs)))
rw [List.prod_cons, List.map_cons, List.reverse_cons', List.prod_concat, op_mul, ih]