no goals
ι : Type ?u.61763
α : Type ?u.61766
M : Type u_1
N : Type ?u.61772
P : Type ?u.61775
M₀ : Type ?u.61778
G : Type ?u.61781
R : Type ?u.61784
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a✝ x : M
xs : List M
a : M
⊢ prod (set (x :: xs) 0 a) =
    (prod (take 0 (x :: xs)) * if 0 < length (x :: xs) then a else 1) * prod (drop (0 + 1) (x :: xs))
simp [set]
no goals
ι : Type ?u.61763
α : Type ?u.61766
M : Type u_1
N : Type ?u.61772
P : Type ?u.61775
M₀ : Type ?u.61778
G : Type ?u.61781
R : Type ?u.61784
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a✝ x : M
xs : List M
i : ℕ
a : M
⊢ prod (set (x :: xs) (i + 1) a) =
    (prod (take (i + 1) (x :: xs)) * if i + 1 < length (x :: xs) then a else 1) * prod (drop (i + 1 + 1) (x :: xs))
simp [set, prod_set xs i a, mul_assoc, Nat.succ_eq_add_one]
no goals
ι : Type ?u.61763
α : Type ?u.61766
M : Type u_1
N : Type ?u.61772
P : Type ?u.61775
M₀ : Type ?u.61778
G : Type ?u.61781
R : Type ?u.61784
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
x✝¹ : ℕ
x✝ : M
⊢ prod (set [] x✝¹ x✝) = (prod (take x✝¹ []) * if x✝¹ < length [] then x✝ else 1) * prod (drop (x✝¹ + 1) [])
simp [set, (Nat.zero_le _).not_lt, Nat.zero_le]