-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : ¬p.head (M := M) = 1
rw :
  prod (M := M)
      (if h : p.head (M := M) = 1 then p.tail (M := M) else cons (M := M) (p.head (M := M)) (p.tail (M := M)) ⋯ h) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
rw₁ :
  (cons (M := M) (p.head (M := M)) (p.tail (M := M)) ⋯ hm).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
rw₂ :
  (mk (M := M) (Sigma.mk (β := fun (i : ι) ↦ M i) i (p.head (M := M)) :: p.tail (M := M).toList (M := M)) ⋯ ⋯).prod
      (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
rw₃ :
  List.prod
      (List.map (fun (l : (i : ι) × M i) ↦ (of (M := M) : (a : M l.fst) → CoprodI M) (l.snd (β := fun (i : ι) ↦ M i)))
        ((mk (M := M) (Sigma.mk (β := fun (i : ι) ↦ M i) i (p.head (M := M)) :: p.tail (M := M).toList (M := M)) ⋯
              ⋯).toList
          (M := M))) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
rw₄ :
  List.prod
      ((of (M := M) : (a : M ⟨i, p.head⟩.fst) → CoprodI M)
          ((Sigma.mk (β := fun (i : ι) ↦ M i) i (p.head (M := M))).snd (β := fun (i : ι) ↦ M i)) ::
        List.map (fun (l : (i : ι) × M i) ↦ (of (M := M) : (a : M l.fst) → CoprodI M) (l.snd (β := fun (i : ι) ↦ M i)))
          (p.tail (M := M).toList (M := M))) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
rw₅ :
  HMul.hMul (α := CoprodI M) (β := CoprodI M)
      ((of (M := M) : (a : M ⟨i, p.head⟩.fst) → CoprodI M)
          ((Sigma.mk (β := fun (i : ι) ↦ M i) i (p.head (M := M))).snd (β := fun (i : ι) ↦ M i)) :
        CoprodI M)
      (List.prod
          (List.map
            (fun (l : (i : ι) × M i) ↦ (of (M := M) : (a : M l.fst) → CoprodI M) (l.snd (β := fun (i : ι) ↦ M i)))
            (p.tail (M := M).toList (M := M))) :
        CoprodI M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
⊢ (rcons (M := M) p).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
have rw₆ : HMul.hMul (α := CoprodI M) (β := CoprodI M)
    ((of (M := M) : (a : M ⟨i, p.head⟩.fst) → CoprodI M)
        ((Sigma.mk (β := fun (i : ι) ↦ M i) i (p.head (M := M))).snd (β := fun (i : ι) ↦ M i)) :
      CoprodI M)
    (List.prod
        (List.map (fun (l : (i : ι) × M i) ↦ (of (M := M) : (a : M l.fst) → CoprodI M) (l.snd (β := fun (i : ι) ↦ M i)))
          (p.tail (M := M).toList (M := M))) :
      CoprodI M) =
  HMul.hMul (α := CoprodI M) (β := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
    (List.prod
        (List.map (fun (l : (i : ι) × M i) ↦ (of (M := M) : (a : M l.fst) → CoprodI M) (l.snd (β := fun (i : ι) ↦ M i)))
          (p.tail (M := M).toList (M := M))) :
      CoprodI M)
Tactic: rw [rcons, dif_neg hm, cons, prod, List.map_cons, List.prod_cons, prod]