no goals
ι : Type ?u.54458
α : Type ?u.54461
M : Type u_1
N : Type ?u.54467
P : Type ?u.54470
M₀ : Type ?u.54473
G : Type ?u.54476
R : Type ?u.54479
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
i : ℕ
p : i < length []
⊢ prod (take (i + 1) []) = prod (take i []) * nthLe [] i p
cases p
ι : Type ?u.54458
α : Type ?u.54461
M : Type u_1
N : Type ?u.54467
P : Type ?u.54470
M₀ : Type ?u.54473
G : Type ?u.54476
R : Type ?u.54479
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a h : M
t : List M
n : ℕ
p : n + 1 < length (h :: t)
⊢ prod (h :: take (n + 1) t) = prod (h :: take n t) * nthLe (h :: t) (n + 1) p
ι : Type ?u.54458
α : Type ?u.54461
M : Type u_1
N : Type ?u.54467
P : Type ?u.54470
M₀ : Type ?u.54473
G : Type ?u.54476
R : Type ?u.54479
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a h : M
t : List M
n : ℕ
p : n + 1 < length (h :: t)
⊢ prod (take (n + 1 + 1) (h :: t)) = prod (take (n + 1) (h :: t)) * nthLe (h :: t) (n + 1) p
dsimp
ι : Type ?u.54458
α : Type ?u.54461
M : Type u_1
N : Type ?u.54467
P : Type ?u.54470
M₀ : Type ?u.54473
G : Type ?u.54476
R : Type ?u.54479
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a h : M
t : List M
n : ℕ
p : n + 1 < length (h :: t)
⊢ h * (prod (take n t) * nthLe t n (_ : n < length t)) =
    h * (prod (take n t) * nthLe t (n + 1 - 1) (_ : n + 1 - 1 < length t))
ι : Type ?u.54458
α : Type ?u.54461
M : Type u_1
N : Type ?u.54467
P : Type ?u.54470
M₀ : Type ?u.54473
G : Type ?u.54476
R : Type ?u.54479
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a h : M
t : List M
n : ℕ
p : n + 1 < length (h :: t)
⊢ prod (h :: take (n + 1) t) = prod (h :: take n t) * nthLe (h :: t) (n + 1) p
rw [prod_cons, prod_cons, prod_take_succ t n (Nat.lt_of_succ_lt_succ p), mul_assoc,
  nthLe_cons, dif_neg (Nat.add_one_ne_zero _)]
no goals
ι : Type ?u.54458
α : Type ?u.54461
M : Type u_1
N : Type ?u.54467
P : Type ?u.54470
M₀ : Type ?u.54473
G : Type ?u.54476
R : Type ?u.54479
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a h : M
t : List M
n : ℕ
p : n + 1 < length (h :: t)
⊢ h * (prod (take n t) * nthLe t n (_ : n < length t)) =
    h * (prod (take n t) * nthLe t (n + 1 - 1) (_ : n + 1 - 1 < length t))
simp