-- Module: Mathlib.GroupTheory.CoprodI
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))
rw₆ 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)
⊢ (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))

Tactic:
rw [rcons, dif_neg hm, cons, prod, List.map_cons, List.prod_cons, prod]

Premises used: List.map_cons, Monoid.CoprodI.Word.prod, dif_neg, Monoid.CoprodI.Word.rcons, Monoid.CoprodI.Word.cons, List.prod_cons