ι : Type ?u.120614
α : Type ?u.120617
M : Type ?u.120620
N : Type ?u.120623
P : Type ?u.120626
M₀ : Type ?u.120629
G : Type u_1
R : Type ?u.120635
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
⊢ (prod (take n L) * if n < length L then a else 1) * prod (drop (n + 1) L) =
    prod L * if hn : n < length L then (nthLe L n hn)⁻¹ * a else 1
ι : Type ?u.120614
α : Type ?u.120617
M : Type ?u.120620
N : Type ?u.120623
P : Type ?u.120626
M₀ : Type ?u.120629
G : Type u_1
R : Type ?u.120635
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
⊢ prod (set L n a) = prod L * if hn : n < length L then (nthLe L n hn)⁻¹ * a else 1
refine (prod_set L n a).trans ?_
case inl
ι : Type ?u.120614
α : Type ?u.120617
M : Type ?u.120620
N : Type ?u.120623
P : Type ?u.120626
M₀ : Type ?u.120629
G : Type u_1
R : Type ?u.120635
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
hn : n < length L
⊢ prod (take n L) * a * prod (drop (n + 1) L) = prod L * ((nthLe L n hn)⁻¹ * a)

case inr
ι : Type ?u.120614
α : Type ?u.120617
M : Type ?u.120620
N : Type ?u.120623
P : Type ?u.120626
M₀ : Type ?u.120629
G : Type u_1
R : Type ?u.120635
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
hn : ¬n < length L
⊢ prod (take n L) * 1 * prod (drop (n + 1) L) = prod L * 1
ι : Type ?u.120614
α : Type ?u.120617
M : Type ?u.120620
N : Type ?u.120623
P : Type ?u.120626
M₀ : Type ?u.120629
G : Type u_1
R : Type ?u.120635
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
⊢ (prod (take n L) * if n < length L then a else 1) * prod (drop (n + 1) L) =
    prod L * if hn : n < length L then (nthLe L n hn)⁻¹ * a else 1
split_ifs with hn
no goals
case inl
ι : Type ?u.120614
α : Type ?u.120617
M : Type ?u.120620
N : Type ?u.120623
P : Type ?u.120626
M₀ : Type ?u.120629
G : Type u_1
R : Type ?u.120635
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
hn : n < length L
⊢ prod (take n L) * a * prod (drop (n + 1) L) = prod L * ((nthLe L n hn)⁻¹ * a)
rw [mul_comm _ a, mul_assoc a, prod_drop_succ L n hn, mul_comm _ (drop n L).prod, ←
  mul_assoc (take n L).prod, prod_take_mul_prod_drop, mul_comm a, mul_assoc]
no goals
case inr
ι : Type ?u.120614
α : Type ?u.120617
M : Type ?u.120620
N : Type ?u.120623
P : Type ?u.120626
M₀ : Type ?u.120629
G : Type u_1
R : Type ?u.120635
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
hn : ¬n < length L
⊢ prod (take n L) * 1 * prod (drop (n + 1) L) = prod L * 1
simp only [take_all_of_le (le_of_not_lt hn), prod_nil, mul_one,
  drop_eq_nil_of_le ((le_of_not_lt hn).trans n.le_succ)]