-- 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
i : ι
h_1 : 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
hφw :
  ∀ (j : ι) (g : G j),
    Sigma.mk (β := fun (i : ι) ↦ G i) j g ∈
        (HSMul.hSMul (α := CoprodI G)
              ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h_1) : 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 i)
    ((↑((⋯.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))
              (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)).2 :
        G i) :
      G i)
    (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)
hh1 : ¬h_1 = 1
h :
  Eq (α := (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set (G := G) i) : Type u_2))
    ((⋯.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))
        (HMul.hMul (α := G i) (β := G i) ((φ i : (a : H) → G i) h_1 : G i)
          (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)) :
      (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set (G := G) i) : Type u_2))
    ((⋯.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))
        1 :
      (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set (G := G) i) : Type u_2))
⊢ (↑(HMul.hMul (α := (↑(↑(φ i).range : Set (G i)) : Type u_2)) (β := (↑(↑(φ i).range : Set (G i)) : Type u_2))
            (Subtype.mk (p := fun (x : G i) ↦ x ∈ (↑(φ i).range : Set (G i))) ((φ i : (a : H) → G i) h_1) ⋯ :
              { x : G i // x ∈ (↑(φ i).range : Set (G i)) })
            (((⋯.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))
                  (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)).1 :
              (↑(↑(φ i).range : Set (G i)) : Type u_2))) :
        G i) =
      1 ∧
    Eq.{u_2 + 1} (α := G i)
      (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i) (1 : G i)

Tactic:
simp only [Prod.ext_iff, equiv_one (d.compl i) (one_mem _) (d.one_mem _),
        equiv_mul_left_of_mem (d.compl i) ⟨_, rfl⟩, hhead, Subtype.ext_iff,
        Prod.ext_iff] at h

Premises used: Subgroup.IsComplement.equiv_one, Monoid.PushoutI.NormalWord.Transversal.compl, Subgroup.IsComplement.equiv_mul_left_of_mem, Monoid.PushoutI.NormalWord.Transversal.one_mem, Prod.ext_iff, Subtype.ext_iff, Exists.intro, OneMemClass.one_mem, rfl