no goals
ι : Type ?u.51930
α : Type ?u.51933
M : Type u_1
N : Type ?u.51939
P : Type ?u.51942
M₀ : Type ?u.51945
G : Type ?u.51948
R : Type ?u.51951
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
i : ℕ
⊢ prod (take i []) * prod (drop i []) = prod []
simp [Nat.zero_le]
no goals
ι : Type ?u.51930
α : Type ?u.51933
M : Type u_1
N : Type ?u.51939
P : Type ?u.51942
M₀ : Type ?u.51945
G : Type ?u.51948
R : Type ?u.51951
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
L : List M
⊢ prod (take 0 L) * prod (drop 0 L) = prod L
simp
ι : Type ?u.51930
α : Type ?u.51933
M : Type u_1
N : Type ?u.51939
P : Type ?u.51942
M₀ : Type ?u.51945
G : Type ?u.51948
R : Type ?u.51951
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a h : M
t : List M
n : ℕ
⊢ prod (h :: take n t) * prod (drop n t) = prod (h :: t)
ι : Type ?u.51930
α : Type ?u.51933
M : Type u_1
N : Type ?u.51939
P : Type ?u.51942
M₀ : Type ?u.51945
G : Type ?u.51948
R : Type ?u.51951
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a h : M
t : List M
n : ℕ
⊢ prod (take (n + 1) (h :: t)) * prod (drop (n + 1) (h :: t)) = prod (h :: t)
dsimp
no goals
ι : Type ?u.51930
α : Type ?u.51933
M : Type u_1
N : Type ?u.51939
P : Type ?u.51942
M₀ : Type ?u.51945
G : Type ?u.51948
R : Type ?u.51951
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a h : M
t : List M
n : ℕ
⊢ prod (h :: take n t) * prod (drop n t) = prod (h :: t)
rw [prod_cons, prod_cons, mul_assoc, prod_take_mul_prod_drop t]