awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
h₁ :
  (↑(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) ⋯ :
            { 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
h₂ :
  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)
⊢ h = 1

Tactic:
rw [h₂, coe_mul, ((d.compl i).coe_equiv_fst_eq_one_iff_mem (one_mem _)).mpr (d.one_mem _),
        mul_one, Subtype.coe_mk, map_eq_one_iff (φ i) (d.injective i)] at h₁

Premises used: Subtype.coe_mk, Iff.mpr, Monoid.PushoutI.NormalWord.Transversal.compl, Monoid.PushoutI.NormalWord.Transversal.one_mem, map_eq_one_iff, Subgroup.coe_mul, Subgroup.IsComplement.coe_equiv_fst_eq_one_iff_mem, OneMemClass.one_mem, mul_one, Monoid.PushoutI.NormalWord.Transversal.injective
-- 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
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
h₁ :
  (↑(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) ⋯ :
            { 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
h₂ :
  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)
h₃ : h = 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:
rw [h₂, coe_mul, ((d.compl i).coe_equiv_fst_eq_one_iff_mem (one_mem _)).mpr (d.one_mem _),
        mul_one, Subtype.coe_mk, map_eq_one_iff (φ i) (d.injective i)] at h₁

Premises used: Subtype.coe_mk, Iff.mpr, Monoid.PushoutI.NormalWord.Transversal.compl, Monoid.PushoutI.NormalWord.Transversal.one_mem, map_eq_one_iff, Subgroup.coe_mul, Subgroup.IsComplement.coe_equiv_fst_eq_one_iff_mem, OneMemClass.one_mem, mul_one, Monoid.PushoutI.NormalWord.Transversal.injective
-- 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
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
h₁ : h = 1
h₂ :
  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)
⊢ False

Tactic:
contradiction
-- 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
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
hep : ¬∃ (h : ¬w.toList (M := G) = []), (w.toList (M := G).head h).fst (β := fun (i : ι) ↦ G i) = i
⊢ ∀ (h : ¬w.toList (M := G) = []), (w.toList (M := G).head h).fst (β := fun (i : ι) ↦ G i) ≠ i

Tactic:
push Not at hep

Premises used: Not
-- 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
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
hep : ∀ (h : ¬w.toList (M := G) = []), (w.toList (M := G).head h).fst (β := fun (i : ι) ↦ G i) ≠ i
pos :
  ∀ (hw : w.toList (M := G) = []),
    Sigma.mk (β := fun (i : ι) ↦ G i) i (HMul.hMul (α := G i) (β := G i) ((φ i : (a : H) → G i) h : G i) (1 : G i)) ∈
        w.toList (M := G).tail ∨
      w.toList (M := G).head? = some (Sigma.mk (β := fun (i : ι) ↦ G i) i 1) ∨
        ¬w.fstIdx (M := G) = some i ∧ Eq.{u_2 + 1} (α := G i) 1 1
neg :
  ∀ (hw : ¬w.toList (M := G) = []),
    Sigma.mk (β := fun (i : ι) ↦ G i) i (HMul.hMul (α := G i) (β := G i) ((φ i : (a : H) → G i) h : G i) (1 : G i)) ∈
        w.toList (M := G).tail ∨
      w.toList (M := G).head? = some (Sigma.mk (β := fun (i : ι) ↦ G i) i 1) ∨
        ¬w.fstIdx (M := G) = some i ∧ Eq.{u_2 + 1} (α := G i) 1 1
⊢ Sigma.mk (β := fun (i : ι) ↦ G i) i (HMul.hMul (α := G i) (β := G i) ((φ i : (a : H) → G i) h : G i) (1 : G i)) ∈
      w.toList (M := G).tail ∨
    w.toList (M := G).head? = some (Sigma.mk (β := fun (i : ι) ↦ G i) i 1) ∨
      ¬w.fstIdx (M := G) = some i ∧ Eq.{u_2 + 1} (α := G i) 1 1

Tactic:
by_cases hw : w.toList = []

Premises used: Monoid.CoprodI.Word.toList
-- 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_1 :
  ∀ (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
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
hep : ∀ (h : ¬w.toList (M := G) = []), (w.toList (M := G).head h).fst (β := fun (i : ι) ↦ G i) ≠ i
hw : w.toList (M := G) = []
⊢ Sigma.mk (β := fun (i : ι) ↦ G i) i (HMul.hMul (α := G i) (β := G i) ((φ i : (a : H) → G i) h : G i) (1 : G i)) ∈
      w.toList (M := G).tail ∨
    w.toList (M := G).head? = some (Sigma.mk (β := fun (i : ι) ↦ G i) i 1) ∨
      ¬w.fstIdx (M := G) = some i ∧ Eq.{u_2 + 1} (α := G i) 1 1

Tactic:
simp [hw, Word.fstIdx]

Premises used: Monoid.CoprodI.Word.fstIdx
-- 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_1 :
  ∀ (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
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
hep : ∀ (h : ¬w.toList (M := G) = []), (w.toList (M := G).head h).fst (β := fun (i : ι) ↦ G i) ≠ i
hw : ¬w.toList (M := G) = []
⊢ Sigma.mk (β := fun (i : ι) ↦ G i) i (HMul.hMul (α := G i) (β := G i) ((φ i : (a : H) → G i) h : G i) (1 : G i)) ∈
      w.toList (M := G).tail ∨
    w.toList (M := G).head? = some (Sigma.mk (β := fun (i : ι) ↦ G i) i 1) ∨
      ¬w.fstIdx (M := G) = some i ∧ Eq.{u_2 + 1} (α := G i) 1 1

Tactic:
simp [head?_eq_some_head hw, Word.fstIdx, hep hw]

Premises used: List.head?_eq_some_head, Monoid.CoprodI.Word.fstIdx
-- 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₁ w₂ : NormalWord (G := G) d
i : ι
h :
  HSMul.hSMul (α := CoprodI G)
      ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) (w₁.head (G := G))) : CoprodI G)
      (w₁.toWord (G := G)) =
    HSMul.hSMul (α := CoprodI G)
      ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) (w₂.head (G := G))) : CoprodI G)
      (w₂.toWord (G := G))
rcases :
  ∀ (w₁ : Word G) (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 :
      HSMul.hSMul (α := CoprodI G)
          ((CoprodI.of (M := G) : (a : G i) → CoprodI G)
              ((φ i : (a : H) → G i) ((mk (G := G) w₁ h₁ hw₁).head (G := G))) :
            CoprodI G)
          ((mk (G := G) w₁ h₁ hw₁).toWord (G := G)) =
        HSMul.hSMul (α := CoprodI G)
          ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) (w₂.head (G := G))) : CoprodI G)
          (w₂.toWord (G := G))),
    mk (G := G) w₁ h₁ hw₁ = w₂
⊢ w₁ = w₂

Tactic:
rcases w₁ with ⟨w₁, h₁, hw₁⟩
-- 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₂ : NormalWord (G := G) d
i : ι
w₁ : Word G
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 :
  HSMul.hSMul (α := CoprodI G)
      ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) ((mk (G := G) w₁ h₁ hw₁).head (G := G))) :
        CoprodI G)
      ((mk (G := G) w₁ h₁ hw₁).toWord (G := G)) =
    HSMul.hSMul (α := CoprodI G)
      ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) (w₂.head (G := G))) : CoprodI G)
      (w₂.toWord (G := G))
rcases :
  ∀ (w₂ : Word G) (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 :
      HSMul.hSMul (α := CoprodI G)
          ((CoprodI.of (M := G) : (a : G i) → CoprodI G)
              ((φ i : (a : H) → G i) ((mk (G := G) w₁ h₁ hw₁).head (G := G))) :
            CoprodI G)
          ((mk (G := G) w₁ h₁ hw₁).toWord (G := G)) =
        HSMul.hSMul (α := CoprodI G)
          ((CoprodI.of (M := G) : (a : G i) → CoprodI G)
              ((φ i : (a : H) → G i) ((mk (G := G) w₂ h₂ hw₂).head (G := G))) :
            CoprodI G)
          ((mk (G := G) w₂ h₂ hw₂).toWord (G := G))),
    mk (G := G) w₁ h₁ hw₁ = mk (G := G) w₂ h₂ hw₂
⊢ mk (G := G) w₁ h₁ hw₁ = w₂

Tactic:
rcases w₂ with ⟨w₂, h₂, hw₂⟩
-- 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)
i : ι
w₁ : Word G
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
w₂ : Word G
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 :
  HSMul.hSMul (α := CoprodI G) ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h₁) : CoprodI G)
      w₁ =
    HSMul.hSMul (α := CoprodI G) ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h₂) : CoprodI G)
      w₂
⊢ w₁ =
    HMul.hMul (α := CoprodI G) (β := CoprodI G)
        (((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h₁))⁻¹ : CoprodI G)
        ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h₂) : CoprodI G) •
      w₂

Tactic:
rw [smul_eq_iff_eq_inv_smul, ← mul_smul] at h

Premises used: smul_eq_iff_eq_inv_smul, SemigroupAction.mul_smul
-- 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)
i : ι
w₁ : Word G
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
w₂ : Word G
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₁ =
    HMul.hMul (α := CoprodI G) (β := CoprodI G)
        (((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h₁))⁻¹ : CoprodI G)
        ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h₂) : CoprodI G) •
      w₂
subst :
  ∀
    (hw₁ :
      ∀ (i_1 : ι) (g : G i_1),
        Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g ∈
            (HMul.hMul (α := CoprodI G) (β := CoprodI G)
                    (((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h₁))⁻¹ : 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) i_1),
    mk (G := G)
        (HMul.hMul (α := CoprodI G) (β := CoprodI G)
            (((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h₁))⁻¹ : CoprodI G)
            ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h₂) : CoprodI G) •
          w₂)
        h₁ hw₁ =
      mk (G := G) w₂ h₂ hw₂
⊢ mk (G := G) w₁ h₁ hw₁ = mk (G := G) w₂ h₂ hw₂

Tactic:
subst 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)
i : ι
h₁ : H
w₂ : Word G
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
hw₁ :
  ∀ (i_1 : ι) (g : G i_1),
    Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g ∈
        (HMul.hMul (α := CoprodI G) (β := CoprodI G)
                (((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h₁))⁻¹ : 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) i_1
⊢ ∀ (i_1 : ι) (g : G i_1),
    Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g ∈
        (HSMul.hSMul (α := CoprodI G)
              ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) (h₁⁻¹ * h₂)) : CoprodI G) w₂).toList
          (M := G) →
      g ∈ d.set (G := G) i_1

Tactic:
simp only [← map_inv, ← map_mul] at hw₁

Premises used: map_inv, map_mul
-- 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)
i : ι
h₁ : H
w₂ : Word G
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
hw₁_1 :
  ∀ (i_1 : ι) (g : G i_1),
    Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g ∈
        (HMul.hMul (α := CoprodI G) (β := CoprodI G)
                (((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h₁))⁻¹ : 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) i_1
hw₁ :
  ∀ (i_1 : ι) (g : G i_1),
    Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g ∈
        (HSMul.hSMul (α := CoprodI G)
              ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) (h₁⁻¹ * h₂)) : CoprodI G) w₂).toList
          (M := G) →
      g ∈ d.set (G := G) i_1
⊢ h₁⁻¹ * h₂ = 1

Tactic:
have : h₁⁻¹ * h₂ = 1 := eq_one_of_smul_normalized w₂ (h₁⁻¹ * h₂) hw₂ hw₁