-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
i j : ι
w : Word M
m : M i
empty :
  Membership.mem (γ := List ((i : ι) × M i))
      (toList (M := M)
        (Pair.tail (M := M) (i := j)
          (↑(consRecOn (M := M) (motive := fun (x : Word M) ↦ { p : Pair M j // rcons (M := M) p = x })
                (Word.empty (M := M))
                (Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = Word.empty (M := M))
                  (Pair.mk (M := M) 1 (Word.empty (M := M)) ⋯) ⋯)
                fun (j_1 : ι) (m : M j_1) (w : Word M) (h1 : ¬w.fstIdx (M := M) = some j_1) (h2 : ¬m = 1)
                  (x : { p : Pair M j // rcons (M := M) p = w }) ↦
                if ij : j = j_1 then
                  Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = Word.cons (M := M) m w h1 h2)
                    (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j_1 = x) ↦ M x) m ⋯) w ⋯) ⋯
                else
                  Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = Word.cons (M := M) m w h1 h2)
                    (Pair.mk (M := M) 1 (Word.cons (M := M) m w h1 h2) ⋯) ⋯) :
            Pair M j)))
      (Sigma.mk (β := fun (i : ι) ↦ M i) i m) ↔
    Membership.mem (γ := List ((i : ι) × M i)) (List.tail (toList (M := M) (Word.empty (M := M))))
        (Sigma.mk (β := fun (i : ι) ↦ M i) i m) ∨
      ¬i = j ∧
        ∃ (h : ¬Eq (α := List ((i : ι) × M i)) (toList (M := M) (Word.empty (M := M))) []),
          List.head (toList (M := M) (Word.empty (M := M))) h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
cons :
  ∀ (k : ι) (g : M k) (tail : Word M) (h1 : tail.fstIdx (M := M) ≠ some k) (h2 : g ≠ 1)
    (ih :
      Membership.mem (γ := List ((i : ι) × M i))
          (toList (M := M)
            (Pair.tail (M := M) (i := j)
              (↑(consRecOn (M := M) (motive := fun (x : Word M) ↦ { p : Pair M j // rcons (M := M) p = x }) tail
                    (Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = Word.empty (M := M))
                      (Pair.mk (M := M) 1 (Word.empty (M := M)) ⋯) ⋯)
                    fun (j_1 : ι) (m : M j_1) (w : Word M) (h1 : ¬w.fstIdx (M := M) = some j_1) (h2 : ¬m = 1)
                      (x : { p : Pair M j // rcons (M := M) p = w }) ↦
                    if ij : j = j_1 then
                      Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = Word.cons (M := M) m w h1 h2)
                        (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j_1 = x) ↦ M x) m ⋯) w ⋯) ⋯
                    else
                      Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = Word.cons (M := M) m w h1 h2)
                        (Pair.mk (M := M) 1 (Word.cons (M := M) m w h1 h2) ⋯) ⋯) :
                Pair M j)))
          (Sigma.mk (β := fun (i : ι) ↦ M i) i m) ↔
        Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ tail.toList (M := M).tail ∨
          ¬i = j ∧
            ∃ (h : ¬tail.toList (M := M) = []), tail.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m),
    Membership.mem (γ := List ((i : ι) × M i))
        (toList (M := M)
          (Pair.tail (M := M) (i := j)
            (↑(consRecOn (M := M) (motive := fun (x : Word M) ↦ { p : Pair M j // rcons (M := M) p = x })
                  (Word.cons (M := M) g tail h1 h2)
                  (Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = Word.empty (M := M))
                    (Pair.mk (M := M) 1 (Word.empty (M := M)) ⋯) ⋯)
                  fun (j_1 : ι) (m : M j_1) (w : Word M) (h1 : ¬w.fstIdx (M := M) = some j_1) (h2 : ¬m = 1)
                    (x : { p : Pair M j // rcons (M := M) p = w }) ↦
                  if ij : j = j_1 then
                    Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = Word.cons (M := M) m w h1 h2)
                      (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j_1 = x) ↦ M x) m ⋯) w ⋯) ⋯
                  else
                    Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = Word.cons (M := M) m w h1 h2)
                      (Pair.mk (M := M) 1 (Word.cons (M := M) m w h1 h2) ⋯) ⋯) :
              Pair M j)))
        (Sigma.mk (β := fun (i : ι) ↦ M i) i m) ↔
      Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ (Word.cons (M := M) g tail h1 h2).toList (M := M).tail ∨
        ¬i = j ∧
          ∃ (h : ¬(Word.cons (M := M) g tail h1 h2).toList (M := M) = []),
            (Word.cons (M := M) g tail h1 h2).toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
⊢ Membership.mem (γ := List ((i : ι) × M i))
      (toList (M := M)
        (Pair.tail (M := M) (i := j)
          (↑(consRecOn (M := M) (motive := fun (x : Word M) ↦ { p : Pair M j // rcons (M := M) p = x }) w
                (Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = Word.empty (M := M))
                  (Pair.mk (M := M) 1 (Word.empty (M := M)) ⋯) ⋯)
                fun (j_1 : ι) (m : M j_1) (w : Word M) (h1 : ¬w.fstIdx (M := M) = some j_1) (h2 : ¬m = 1)
                  (x : { p : Pair M j // rcons (M := M) p = w }) ↦
                if ij : j = j_1 then
                  Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = Word.cons (M := M) m w h1 h2)
                    (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j_1 = x) ↦ M x) m ⋯) w ⋯) ⋯
                else
                  Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = Word.cons (M := M) m w h1 h2)
                    (Pair.mk (M := M) 1 (Word.cons (M := M) m w h1 h2) ⋯) ⋯) :
            Pair M j)))
      (Sigma.mk (β := fun (i : ι) ↦ M i) i m) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ w.toList (M := M).tail ∨
      ¬i = j ∧ ∃ (h : ¬w.toList (M := M) = []), w.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m

Tactic:
induction w using consRecOn with
  | empty => simp
  | cons k g tail h1 h2 ih =>
    simp only [consRecOn_cons]
    split_ifs with h
    · subst k
      by_cases hij : j = i <;> simp_all
    · by_cases hik : i = k
      · subst i; simp_all [@eq_comm _ m g, @eq_comm _ k j, or_comm]
      · simp [hik, Ne.symm hik]

Premises used: Monoid.CoprodI.Word.empty, Monoid.CoprodI.Word.cons, or_comm, Monoid.CoprodI.Word.consRecOn_cons