-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (G i)
w : Word G
h : H
hw :
  ∀ (i : ι) (g : G i),
    Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toList (M := G) →
      (↑((⋯.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
                  (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
                g).2 :
          G i) =
        g
hh1 : ¬h = 1
hnil : ¬w.toList (M := G) = []
hφw :
  ∀ (j : ι) (g : G j),
    Sigma.mk (β := fun (i : ι) ↦ G i) j g ∈
        (HSMul.hSMul (α := CoprodI G)
              ((CoprodI.of (M := G) : (a : G (w.toList.head hnil).fst) → CoprodI G)
                  ((φ ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)) :
                      (a : H) → G (w.toList.head hnil).fst)
                    h) :
                CoprodI G)
              w).toList
          (M := G) →
      (↑((⋯.equiv (S := (↑(φ j).range : Set (G j))) (T := d.set (G := G) j) :
                  (a : G j) → (↑(↑(φ j).range : Set (G j)) : Type u_2) × (↑(d.set j) : Type u_2))
                g).2 :
          G j) =
        g
hhead :
  Eq.{u_2 + 1} (α := G ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)))
    ((↑((equiv (S :=
                  (↑(MonoidHom.range (φ ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)))) :
                    Set (G (w.toList.head hnil).fst)))
                  (T := d.set (G := G) ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i))) ⋯ :
                (a : G (w.toList.head hnil).fst) →
                  (↑(↑(φ (w.toList.head hnil).fst).range : Set (G (w.toList.head hnil).fst)) : Type u_2) ×
                    (↑(d.set (w.toList.head hnil).fst) : Type u_2))
              (Word.Pair.head (M := G)
                  ((Word.equivPair (M := G) ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)) :
                      (a : Word G) → Word.Pair G (w.toList.head hnil).fst)
                    w) :
                G ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)))).2 :
        G ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i))) :
      G ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)))
    (Word.Pair.head (M := G)
        ((Word.equivPair (M := G) ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)) :
            (a : Word G) → Word.Pair G (w.toList.head hnil).fst)
          w) :
      G ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)))
pos :
  Sigma.mk (β := fun (i : ι) ↦ G i) ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i))
        (HMul.hMul (α := G ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i))) (β :=
          G ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)))
          ((φ ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)) : (a : H) → G (w.toList.head hnil).fst) h :
            G ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)))
          (@Eq.rec _ _ (fun (x : ι) (h : (w.toList (M := G).head ⋯).fst (β := fun (i : ι) ↦ G i) = x) ↦ G x)
              ((w.toList (M := G).head ⋯).snd (β := fun (i : ι) ↦ G i))
              ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)) ⋯ :
            G ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)))) ∈
      w.toList (M := G).tail ∨
    some (w.toList (M := G).head hnil) =
        some
          (Sigma.mk (β := fun (i : ι) ↦ G i) ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i))
            (@Eq.rec _ _ (fun (x : ι) (h : (w.toList (M := G).head ⋯).fst (β := fun (i : ι) ↦ G i) = x) ↦ G x)
              ((w.toList (M := G).head ⋯).snd (β := fun (i : ι) ↦ G i))
              ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)) ⋯)) ∨
      ¬w.fstIdx (M := G) = some ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)) ∧
        Eq.{u_2 + 1} (α := G ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)))
          (@Eq.rec _ _ (fun (x : ι) (h : (w.toList (M := G).head ⋯).fst (β := fun (i : ι) ↦ G i) = x) ↦ G x)
              ((w.toList (M := G).head ⋯).snd (β := fun (i : ι) ↦ G i))
              ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)) ⋯ :
            G ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)))
          (1 : G ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)))
⊢ Sigma.mk (β := fun (i : ι) ↦ G i) ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i))
        (HMul.hMul (α := G ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i))) (β :=
          G ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)))
          ((φ ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)) : (a : H) → G (w.toList.head hnil).fst) h :
            G ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)))
          (@Eq.rec _ _ (fun (x : ι) (h : (w.toList (M := G).head ⋯).fst (β := fun (i : ι) ↦ G i) = x) ↦ G x)
              ((w.toList (M := G).head ⋯).snd (β := fun (i : ι) ↦ G i))
              ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)) ⋯ :
            G ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)))) ∈
      w.toList (M := G).tail ∨
    w.toList (M := G).head? =
        some
          (Sigma.mk (β := fun (i : ι) ↦ G i) ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i))
            (@Eq.rec _ _ (fun (x : ι) (h : (w.toList (M := G).head ⋯).fst (β := fun (i : ι) ↦ G i) = x) ↦ G x)
              ((w.toList (M := G).head ⋯).snd (β := fun (i : ι) ↦ G i))
              ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)) ⋯)) ∨
      ¬w.fstIdx (M := G) = some ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)) ∧
        Eq.{u_2 + 1} (α := G ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)))
          (@Eq.rec _ _ (fun (x : ι) (h : (w.toList (M := G).head ⋯).fst (β := fun (i : ι) ↦ G i) = x) ↦ G x)
              ((w.toList (M := G).head ⋯).snd (β := fun (i : ι) ↦ G i))
              ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)) ⋯ :
            G ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)))
          (1 : G ((w.toList (M := G).head hnil).fst (β := fun (i : ι) ↦ G i)))

Tactic:
rw [head?_eq_some_head hnil]

Premises used: List.head?_eq_some_head