awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Group (G i)
inst_2 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
i_1 : ι
g_1 : G i_1
w : NormalWord (G := G) d
hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i_1
hgr : g_1 ∉ (φ i_1).range
n : (↑(↑(φ i_1).range : Set (G i_1)) : Type u_2) × (↑(d.set (G := G) i_1) : Type u_2) :=
  (⋯.equiv (S := (↑(φ i_1).range : Set (G i_1))) (T := d.set (G := G) i_1) :
      (a : G i_1) → (↑(↑(φ i_1).range : Set (G i_1)) : Type u_2) × (↑(d.set i_1) : Type u_2))
    (HMul.hMul (β := G i_1) g_1 ((φ i_1 : (a : H) → G i_1) (w.head (G := G)) : G i_1))
w' : Word G := Word.cons (M := G) (↑n.2 : G i_1) (w.toWord (G := G)) hmw ⋯
i : ι
g : G i
hg : Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w'.toList (M := G)
⊢ i = i_1 ∧ g ≍ (↑n.2 : G i_1) ∨ Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toWord (G := G).toList (M := G)

Tactic:
simp only [w', Word.cons, mem_cons, Sigma.mk.inj_iff] at hg

Premises used: Sigma.mk.inj_iff, Monoid.CoprodI.Word.cons, List.mem_cons
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Group (G i)
inst_2 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
i_1 : ι
g_1 : G i_1
w : NormalWord (G := G) d
hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i_1
hgr : g_1 ∉ (φ i_1).range
n : (↑(↑(φ i_1).range : Set (G i_1)) : Type u_2) × (↑(d.set (G := G) i_1) : Type u_2) :=
  (⋯.equiv (S := (↑(φ i_1).range : Set (G i_1))) (T := d.set (G := G) i_1) :
      (a : G i_1) → (↑(↑(φ i_1).range : Set (G i_1)) : Type u_2) × (↑(d.set i_1) : Type u_2))
    (HMul.hMul (β := G i_1) g_1 ((φ i_1 : (a : H) → G i_1) (w.head (G := G)) : G i_1))
w' : Word G := Word.cons (M := G) (↑n.2 : G i_1) (w.toWord (G := G)) hmw ⋯
i : ι
g : G i
hg : i = i_1 ∧ g ≍ (↑n.2 : G i_1) ∨ Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toWord (G := G).toList (M := G)
inl :
  ∀ (g : G i) (hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i) (hgr : g ∉ (φ i).range),
    let n : (↑(↑(φ 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 : (a : H) → G i) (w.head (G := G)) : G i));
    ∀ {β : Type u_2}, (↑n.2 : G i) ∈ d.set (G := G) i
inr : Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toWord (G := G).toList (M := G) → g ∈ d.set (G := G) i
⊢ g ∈ d.set (G := G) i

Tactic:
rcases hg with ⟨rfl, hg | hg⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Group (G i)
inst_2 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
w : NormalWord (G := G) d
i : ι
g : G i
hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i
hgr : g ∉ (φ i).range
n : (↑(↑(φ 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 : (a : H) → G i) (w.head (G := G)) : G i))
w' : Word G := Word.cons (M := G) (↑n.2 : G i) (w.toWord (G := G)) hmw ⋯
β : Type u_2
⊢ (↑n.2 : G i) ∈ d.set (G := G) i

Tactic:
simp
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Group (G i)
inst_2 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
i_1 : ι
g_1 : G i_1
w : NormalWord (G := G) d
hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i_1
hgr : g_1 ∉ (φ i_1).range
n : (↑(↑(φ i_1).range : Set (G i_1)) : Type u_2) × (↑(d.set (G := G) i_1) : Type u_2) :=
  (⋯.equiv (S := (↑(φ i_1).range : Set (G i_1))) (T := d.set (G := G) i_1) :
      (a : G i_1) → (↑(↑(φ i_1).range : Set (G i_1)) : Type u_2) × (↑(d.set i_1) : Type u_2))
    (HMul.hMul (β := G i_1) g_1 ((φ i_1 : (a : H) → G i_1) (w.head (G := G)) : G i_1))
w' : Word G := Word.cons (M := G) (↑n.2 : G i_1) (w.toWord (G := G)) hmw ⋯
i : ι
g : G i
h : Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toWord (G := G).toList (M := G)
⊢ Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toWord (G := G).toList (M := G)

Tactic:
assumption
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Group (G i)
inst_2 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
i_1 : ι
g_1 : G i_1
w : NormalWord (G := G) d
hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i_1
hgr : g_1 ∉ (φ i_1).range
n : (↑(↑(φ i_1).range : Set (G i_1)) : Type u_2) × (↑(d.set (G := G) i_1) : Type u_2) :=
  (⋯.equiv (S := (↑(φ i_1).range : Set (G i_1))) (T := d.set (G := G) i_1) :
      (a : G i_1) → (↑(↑(φ i_1).range : Set (G i_1)) : Type u_2) × (↑(d.set i_1) : Type u_2))
    (HMul.hMul (β := G i_1) g_1 ((φ i_1 : (a : H) → G i_1) (w.head (G := G)) : G i_1))
w' : Word G := Word.cons (M := G) (↑n.2 : G i_1) (w.toWord (G := G)) hmw ⋯
i : ι
g : G i
h : Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toWord (G := G).toList (M := G)
⊢ g ∈ d.set (G := G) i

Tactic:
exact w.normalized _ _ (by assumption)

Premises used: Monoid.PushoutI.NormalWord.normalized
-- 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) φ
i : ι
g : G i
w : NormalWord (G := G) d
hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i
hgr : g ∉ (φ i).range
⊢ (cons (G := G) g w hmw hgr).prod (G := G) =
    HMul.hMul (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) g : PushoutI (G := G) φ)
      (w.prod (G := G))

Tactic:
simp [prod, cons, ← of_apply_eq_base φ i, equiv_fst_eq_mul_inv, mul_assoc]

Premises used: Monoid.PushoutI.NormalWord.prod, mul_assoc, Monoid.PushoutI.of_apply_eq_base, Subgroup.IsComplement.equiv_fst_eq_mul_inv, Monoid.PushoutI.NormalWord.cons
-- 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 : H
hw : ∀ (i : ι) (g : G i), Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toList (M := G) → g ∈ d.set (G := G) i
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) : CoprodI G) w).toList
          (M := G) →
      g ∈ d.set (G := G) j
⊢ ∀ (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

Tactic:
simp only [← (d.compl _).equiv_snd_eq_self_iff_mem (one_mem _)] at hw hφw

Premises used: Subgroup.IsComplement.equiv_snd_eq_self_iff_mem, Monoid.PushoutI.NormalWord.Transversal.compl, OneMemClass.one_mem
-- 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 : H
hw : ∀ (i : ι) (g : G i), Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toList (M := G) → g ∈ d.set (G := G) i
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) : CoprodI G) w).toList
          (M := G) →
      g ∈ d.set (G := G) j
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
⊢ ∀ (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) : 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

Tactic:
simp only [← (d.compl _).equiv_snd_eq_self_iff_mem (one_mem _)] at hw hφw

Premises used: Subgroup.IsComplement.equiv_snd_eq_self_iff_mem, Monoid.PushoutI.NormalWord.Transversal.compl, OneMemClass.one_mem
-- 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 : 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) : 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
rw :
  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))
            (if h : ∃ (h : w.toList (M := G) ≠ []), (w.toList (M := G).head h).fst (β := fun (i : ι) ↦ G i) = i then
              Eq.rec (motive := 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)) ⋯
            else 1)).2 :
      G i)
    (if h : ∃ (h : w.toList (M := G) ≠ []), (w.toList (M := G).head h).fst (β := fun (i : ι) ↦ G i) = i then
      Eq.rec (motive := 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)) ⋯
    else 1)
⊢ 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)

Tactic:
rw [Word.equivPair_head]

Premises used: Monoid.CoprodI.Word.equivPair_head
-- 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 : 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) : 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
pos :
  ∀ (h : ∃ (h : w.toList (M := G) ≠ []), (w.toList (M := G).head h).fst (β := fun (i : ι) ↦ G i) = i),
    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))
                (Eq.rec (motive := 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)) ⋯ :
                  G i)).2 :
          G i) :
        G i)
      (Eq.rec (motive := 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)) ⋯ :
        G i)
neg :
  ∀ (h : ¬∃ (h : w.toList (M := G) ≠ []), (w.toList (M := G).head h).fst (β := fun (i : ι) ↦ G i) = i),
    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))
              1).2 :
        G i)
      1
⊢ 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))
            (if h : ∃ (h : w.toList (M := G) ≠ []), (w.toList (M := G).head h).fst (β := fun (i : ι) ↦ G i) = i then
              Eq.rec (motive := 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)) ⋯
            else 1)).2 :
      G i)
    (if h : ∃ (h : w.toList (M := G) ≠ []), (w.toList (M := G).head h).fst (β := fun (i : ι) ↦ G i) = i then
      Eq.rec (motive := 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)) ⋯
    else 1)

Tactic:
split_ifs with h
-- 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
w_1 : 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 w_1).fst) → CoprodI G)
                  ((φ ((w.toList (M := G).head w_1).fst (β := fun (i : ι) ↦ G i)) : (a : H) → G (w.toList.head w_1).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
⊢ Eq.{u_2 + 1} (α := G ((w.toList (M := G).head w_1).fst (β := fun (i : ι) ↦ G i)))
    ((↑((equiv (S :=
                  (↑(MonoidHom.range (φ ((w.toList (M := G).head w_1).fst (β := fun (i : ι) ↦ G i)))) :
                    Set (G (w.toList.head w_1).fst)))
                  (T := d.set (G := G) ((w.toList (M := G).head w_1).fst (β := fun (i : ι) ↦ G i))) ⋯ :
                (a : G (w.toList.head w_1).fst) →
                  (↑(↑(φ (w.toList.head w_1).fst).range : Set (G (w.toList.head w_1).fst)) : Type u_2) ×
                    (↑(d.set (w.toList.head w_1).fst) : Type u_2))
              (@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 w_1).fst (β := fun (i : ι) ↦ G i)) ⋯ :
                G ((w.toList (M := G).head w_1).fst (β := fun (i : ι) ↦ G i)))).2 :
        G ((w.toList (M := G).head w_1).fst (β := fun (i : ι) ↦ G i))) :
      G ((w.toList (M := G).head w_1).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 w_1).fst (β := fun (i : ι) ↦ G i)) ⋯ :
      G ((w.toList (M := G).head w_1).fst (β := fun (i : ι) ↦ G i)))

Tactic:
hw _ _ (List.head_mem _)

Premises used: List.head_mem
-- 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
w_1 : 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 w_1).fst) → CoprodI G)
                  ((φ ((w.toList (M := G).head w_1).fst (β := fun (i : ι) ↦ G i)) : (a : H) → G (w.toList.head w_1).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
⊢ Eq.{u_2 + 1} (α := G ((w.toList (M := G).head w_1).fst (β := fun (i : ι) ↦ G i)))
    ((↑((equiv (S :=
                  (↑(MonoidHom.range (φ ((w.toList (M := G).head w_1).fst (β := fun (i : ι) ↦ G i)))) :
                    Set (G (w.toList.head w_1).fst)))
                  (T := d.set (G := G) ((w.toList (M := G).head w_1).fst (β := fun (i : ι) ↦ G i))) ⋯ :
                (a : G (w.toList.head w_1).fst) →
                  (↑(↑(φ (w.toList.head w_1).fst).range : Set (G (w.toList.head w_1).fst)) : Type u_2) ×
                    (↑(d.set (w.toList.head w_1).fst) : Type u_2))
              (@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 w_1).fst (β := fun (i : ι) ↦ G i)) ⋯ :
                G ((w.toList (M := G).head w_1).fst (β := fun (i : ι) ↦ G i)))).2 :
        G ((w.toList (M := G).head w_1).fst (β := fun (i : ι) ↦ G i))) :
      G ((w.toList (M := G).head w_1).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 w_1).fst (β := fun (i : ι) ↦ G i)) ⋯ :
      G ((w.toList (M := G).head w_1).fst (β := fun (i : ι) ↦ G i)))

Tactic:
exact hw _ _ (List.head_mem _)

Premises used: List.head_mem
-- 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
h : ¬∃ (h : w.toList (M := G) ≠ []), (w.toList (M := G).head h).fst (β := fun (i : ι) ↦ G i) = i
neg neg₁ :
  (↑(Subtype.mk (p := fun (x : G i) ↦ x ∈ (↑(φ i).range : Set (G i))) 1 ⋯,
            Subtype.mk (p := fun (x : G i) ↦ x ∈ d.set (G := G) i) 1 ⋯).2 :
      G i) =
    1
⊢ 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))
            1).2 :
      G i)
    1

Tactic:
rw [equiv_one (d.compl i) (one_mem _) (d.one_mem _)]

Premises used: Subgroup.IsComplement.equiv_one, Monoid.PushoutI.NormalWord.Transversal.compl, Monoid.PushoutI.NormalWord.Transversal.one_mem, OneMemClass.one_mem
-- 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 : 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) : 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
⊢ 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)

Tactic:
have hhead : ((d.compl i).equiv (Word.equivPair i w).head).2 =
      (Word.equivPair i w).head := by
    rw [Word.equivPair_head]
    split_ifs with h
    · rcases h with ⟨_, rfl⟩
      exact hw _ _ (List.head_mem _)
    · rw [equiv_one (d.compl i) (one_mem _) (d.one_mem _)]