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)
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
this : h₁⁻¹ * h₂ = 1
⊢ h₁ = h₂

Tactic:
rw [inv_mul_eq_one] at this

Premises used: inv_mul_eq_one
-- 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
this : h₁ = h₂
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)
    (hw₁_2 :
      ∀ (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),
    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)
      (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₁_1 =
    mk (G := G) w₂ h₂ hw₂

Tactic:
subst this
-- 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
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
⊢ 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₁_1 =
    mk (G := G) w₂ h₁ hw₂

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) φ
inst_3 : DecidableEq ι
inst_4 : (i : ι) → DecidableEq (G i)
i_1 : ι
p : Pair (G := G) d i_1
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))
    (p.toPair (G := G).head (M := G))
w : Word G :=
  (Equiv.symm (Word.equivPair (M := G) i_1) : (a : Word.Pair G i_1) → Word G)
    (let __src := p.toPair (G := G);
    Word.Pair.mk (M := G) (↑n.2 : G i_1) (__src.tail (M := G)) ⋯)
i : ι
g : G i
hg :
  Membership.mem (γ := List ((i : ι) × G i))
    (Word.toList (M := G)
      ((Equiv.symm (Word.equivPair (M := G) i_1) : (a : Word.Pair G i_1) → Word G)
        (Word.Pair.mk (M := G) (↑n.2 : G i_1) (p.toPair (G := G).tail (M := G)) ⋯)))
    (Sigma.mk (β := fun (i : ι) ↦ G i) i g)
⊢ Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈
      (Word.Pair.mk (M := G) (↑n.2 : G i_1) (p.toPair (G := G).tail (M := G)) ⋯).tail (M := G).toList (M := G) ∨
    g ≠ 1 ∧
      ∃ (h : i_1 = i),
        g =
          Eq.rec (motive := fun (x : ι) (h : i_1 = x) ↦ G x)
            ((Word.Pair.mk (M := G) (↑n.2 : G i_1) (p.toPair (G := G).tail (M := G)) ⋯).head (M := G)) h

Tactic:
rw [Word.equivPair_symm, Word.mem_rcons_iff] at hg

Premises used: Monoid.CoprodI.Word.equivPair_symm, Monoid.CoprodI.Word.mem_rcons_iff
-- 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) φ
inst_3 : DecidableEq ι
inst_4 : (i : ι) → DecidableEq (G i)
i_1 : ι
p : Pair (G := G) d i_1
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))
    (p.toPair (G := G).head (M := G))
w : Word G :=
  (Equiv.symm (Word.equivPair (M := G) i_1) : (a : Word.Pair G i_1) → Word G)
    (let __src := p.toPair (G := G);
    Word.Pair.mk (M := G) (↑n.2 : G i_1) (__src.tail (M := G)) ⋯)
i : ι
g : G i
hg :
  Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈
      (Word.Pair.mk (M := G) (↑n.2 : G i_1) (p.toPair (G := G).tail (M := G)) ⋯).tail (M := G).toList (M := G) ∨
    g ≠ 1 ∧
      ∃ (h : i_1 = i),
        g =
          Eq.rec (motive := fun (x : ι) (h : i_1 = x) ↦ G x)
            ((Word.Pair.mk (M := G) (↑n.2 : G i_1) (p.toPair (G := G).tail (M := G)) ⋯).head (M := G)) h
inl :
  ∀
    (hg :
      Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈
        (Word.Pair.mk (M := G) (↑n.2 : G i_1) (p.toPair (G := G).tail (M := G)) ⋯).tail (M := G).toList (M := G)),
    g ∈ d.set (G := G) i
inr :
  Ne.{u_2 + 1} (α := G i_1)
      (Eq.rec (motive := fun (x : ι) (h : i_1 = x) ↦ G x)
          ((Word.Pair.mk (M := G) (↑n.2 : G i_1) (p.toPair (G := G).tail (M := G)) ⋯).head (M := G)) ⋯ :
        G i_1)
      (1 : G i_1) →
    Membership.mem (α := G i_1) (d.set (G := G) i_1)
      (Eq.rec (motive := fun (x : ι) (h : i_1 = x) ↦ G x)
          ((Word.Pair.mk (M := G) (↑n.2 : G i_1) (p.toPair (G := G).tail (M := G)) ⋯).head (M := G)) ⋯ :
        G i_1)
⊢ g ∈ d.set (G := G) i

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

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) φ
inst_3 : DecidableEq ι
inst_4 : (i : ι) → DecidableEq (G i)
i_1 : ι
p : Pair (G := G) d i_1
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))
    (p.toPair (G := G).head (M := G))
w : Word G :=
  (Equiv.symm (Word.equivPair (M := G) i_1) : (a : Word.Pair G i_1) → Word G)
    (let __src := p.toPair (G := G);
    Word.Pair.mk (M := G) (↑n.2 : G i_1) (__src.tail (M := G)) ⋯)
i : ι
g : G i
hg :
  Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈
    (Word.Pair.mk (M := G) (↑n.2 : G i_1) (p.toPair (G := G).tail (M := G)) ⋯).tail (M := G).toList (M := G)
⊢ g ∈ d.set (G := G) i

Tactic:
p.normalized _ _ hg

Premises used: Monoid.PushoutI.NormalWord.Pair.normalized
-- 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) φ
inst_3 : DecidableEq ι
inst_4 : (i : ι) → DecidableEq (G i)
i_1 : ι
p : Pair (G := G) d i_1
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))
    (p.toPair (G := G).head (M := G))
w : Word G :=
  (Equiv.symm (Word.equivPair (M := G) i_1) : (a : Word.Pair G i_1) → Word G)
    (let __src := p.toPair (G := G);
    Word.Pair.mk (M := G) (↑n.2 : G i_1) (__src.tail (M := G)) ⋯)
i : ι
g : G i
hg :
  Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈
    (Word.Pair.mk (M := G) (↑n.2 : G i_1) (p.toPair (G := G).tail (M := G)) ⋯).tail (M := G).toList (M := G)
⊢ g ∈ d.set (G := G) i

Tactic:
exact p.normalized _ _ hg

Premises used: Monoid.PushoutI.NormalWord.Pair.normalized
-- 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) φ
inst_3 : DecidableEq ι
inst_4 : (i : ι) → DecidableEq (G i)
i : ι
p : Pair (G := G) d i
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))
    (p.toPair (G := G).head (M := G))
w : Word G :=
  (Equiv.symm (Word.equivPair (M := G) i) : (a : Word.Pair G i) → Word G)
    (let __src := p.toPair (G := G);
    Word.Pair.mk (M := G) (↑n.2 : G i) (__src.tail (M := G)) ⋯)
left :
  Ne.{u_2 + 1} (α := G i)
    (Eq.rec (motive := fun (x : ι) (h : i = x) ↦ G x)
        ((Word.Pair.mk (M := G) (↑n.2 : G i) (p.toPair (G := G).tail (M := G)) ⋯).head (M := G)) ⋯ :
      G i)
    (1 : G i)
⊢ Membership.mem (α := G i) (d.set (G := G) i)
    (Eq.rec (motive := fun (x : ι) (h : i = x) ↦ G x)
        ((Word.Pair.mk (M := G) (↑n.2 : G i) (p.toPair (G := G).tail (M := G)) ⋯).head (M := G)) ⋯ :
      G i)

Tactic:
simp
-- 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 : ι
head₁ : G i
tail₁ : Word G
fstIdx_ne : tail₁.fstIdx (M := G) ≠ some i
normalized :
  ∀ (i_1 : ι) (g : G i_1),
    Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g ∈
        (Word.Pair.mk (M := G) head₁ tail₁ fstIdx_ne).tail (M := G).toList (M := G) →
      g ∈ d.set (G := G) i_1
head₂ : G i
tail₂ : Word G
fstIdx_ne_1 : tail₂.fstIdx (M := G) ≠ some i
normalized_1 :
  ∀ (i_1 : ι) (g : G i_1),
    Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g ∈
        (Word.Pair.mk (M := G) head₂ tail₂ fstIdx_ne_1).tail (M := G).toList (M := G) →
      g ∈ d.set (G := G) i_1
simp :
  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))
              head₁).2 :
        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))
              head₂).2 :
        G i) →
    tail₁ = tail₂ →
      Eq.{u_2 + 1} (α := ↥(φ i).range)
          ((⋯.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))
              head₁).1
          ((⋯.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))
              head₂).1 →
        head₁ = head₂ ∧ tail₁ = tail₂
⊢ rcons (G := G) i (Pair.mk (G := G) (Word.Pair.mk (M := G) head₁ tail₁ fstIdx_ne) normalized) =
      rcons (G := G) i (Pair.mk (G := G) (Word.Pair.mk (M := G) head₂ tail₂ fstIdx_ne_1) normalized_1) →
    Pair.mk (G := G) (Word.Pair.mk (M := G) head₁ tail₁ fstIdx_ne) normalized =
      Pair.mk (G := G) (Word.Pair.mk (M := G) head₂ tail₂ fstIdx_ne_1) normalized_1

Tactic:
simp only [rcons, NormalWord.mk.injEq, EmbeddingLike.apply_eq_iff_eq,
    Word.Pair.mk.injEq, Pair.mk.injEq, and_imp]

Premises used: and_imp, Monoid.PushoutI.NormalWord.Pair.mk.injEq, EmbeddingLike.apply_eq_iff_eq, Monoid.PushoutI.NormalWord.mk.injEq, Monoid.CoprodI.Word.Pair.mk.injEq, Monoid.PushoutI.NormalWord.rcons
-- 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 : ι
head₁ : G i
tail₁ : Word G
fstIdx_ne : tail₁.fstIdx (M := G) ≠ some i
normalized :
  ∀ (i_1 : ι) (g : G i_1),
    Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g ∈
        (Word.Pair.mk (M := G) head₁ tail₁ fstIdx_ne).tail (M := G).toList (M := G) →
      g ∈ d.set (G := G) i_1
head₂ : G i
h₁ :
  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))
            head₁).2 :
      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))
            head₂).2 :
      G i)
fstIdx_ne_1 : tail₁.fstIdx (M := G) ≠ some i
normalized_1 :
  ∀ (i_1 : ι) (g : G i_1),
    Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g ∈
        (Word.Pair.mk (M := G) head₂ tail₁ fstIdx_ne_1).tail (M := G).toList (M := G) →
      g ∈ d.set (G := G) i_1
h₃ :
  Eq.{u_2 + 1} (α := ↥(φ i).range)
    ((⋯.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))
        head₁).1
    ((⋯.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))
        head₂).1
rw :
  HMul.hMul (α := 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))
                head₂).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))
                head₂).2 :
          G i) =
      HMul.hMul (α := 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))
                head₂).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))
                head₂).2 :
          G i) ∧
    tail₁ = tail₁
⊢ head₁ = head₂ ∧ tail₁ = tail₁

Tactic:
rw [← equiv_fst_mul_equiv_snd (d.compl i) head₁,
      ← equiv_fst_mul_equiv_snd (d.compl i) head₂,
    h₁, h₃]

Premises used: Monoid.PushoutI.NormalWord.Transversal.compl, Subgroup.IsComplement.equiv_fst_mul_equiv_snd
-- 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 : ι
head₁ : G i
tail₁ : Word G
fstIdx_ne : tail₁.fstIdx (M := G) ≠ some i
normalized :
  ∀ (i_1 : ι) (g : G i_1),
    Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g ∈
        (Word.Pair.mk (M := G) head₁ tail₁ fstIdx_ne).tail (M := G).toList (M := G) →
      g ∈ d.set (G := G) i_1
head₂ : G i
h₁ :
  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))
            head₁).2 :
      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))
            head₂).2 :
      G i)
fstIdx_ne_1 : tail₁.fstIdx (M := G) ≠ some i
normalized_1 :
  ∀ (i_1 : ι) (g : G i_1),
    Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g ∈
        (Word.Pair.mk (M := G) head₂ tail₁ fstIdx_ne_1).tail (M := G).toList (M := G) →
      g ∈ d.set (G := G) i_1
h₃ :
  Eq.{u_2 + 1} (α := ↥(φ i).range)
    ((⋯.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))
        head₁).1
    ((⋯.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))
        head₂).1
⊢ HMul.hMul (α := 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))
                head₂).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))
                head₂).2 :
          G i) =
      HMul.hMul (α := 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))
                head₂).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))
                head₂).2 :
          G i) ∧
    tail₁ = tail₁

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) φ
inst_3 : DecidableEq ι
inst_4 : (i : ι) → DecidableEq (G i)
i : ι
w : NormalWord (G := G) d
p : Word.Pair G i :=
  (Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i)
    (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)))
j : ι
g : G j
hg :
  Membership.mem (γ := List ((i : ι) × G i))
    (Word.toList (M := G)
        (Word.Pair.tail (M := G) (i := i)
          ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i)
            (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))))) :
      List ((i : ι) × G i))
    (Sigma.mk (β := fun (i : ι) ↦ G i) j g)
⊢ Membership.mem (γ := List ((i : ι) × G i))
    (Word.toList (M := G)
      (Word.Pair.tail (M := G) (i := i)
        (have __src : Word.Pair G i := (Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) (w.toWord (G := G));
        Word.Pair.mk (M := G)
          (HMul.hMul (α := G i) (β := G i) ((φ i : (a : H) → G i) (w.head (G := G)) : G i)
            (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) (w.toWord (G := G))) :
              G i))
          (__src.tail (M := G)) ⋯)))
    (Sigma.mk (β := fun (i : ι) ↦ G i) j g)

Tactic:
rw [Word.of_smul_def, ← Word.equivPair_symm, Equiv.apply_symm_apply] at hg

Premises used: Equiv.apply_symm_apply, Monoid.CoprodI.Word.of_smul_def, Monoid.CoprodI.Word.equivPair_symm
-- 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) φ
inst_3 : DecidableEq ι
inst_4 : (i : ι) → DecidableEq (G i)
i : ι
w : NormalWord (G := G) d
p : Word.Pair G i :=
  (Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i)
    (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)))
j : ι
g : G j
hg :
  Membership.mem (γ := List ((i : ι) × G i))
    (Word.toList (M := G)
        (Word.Pair.tail (M := G) (i := i)
          ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) (w.toWord (G := G)))) :
      List ((i : ι) × G i))
    (Sigma.mk (β := fun (i : ι) ↦ G i) j g)
⊢ g ∈ d.set (G := G) j

Tactic:
w.normalized _ _ (Word.mem_of_mem_equivPair_tail _ hg)

Premises used: Monoid.CoprodI.Word.mem_of_mem_equivPair_tail, Monoid.PushoutI.NormalWord.normalized
-- 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) φ
inst_3 : DecidableEq ι
inst_4 : (i : ι) → DecidableEq (G i)
i : ι
w : NormalWord (G := G) d
p : Word.Pair G i :=
  (Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i)
    (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)))
j : ι
g : G j
hg :
  Membership.mem (γ := List ((i : ι) × G i))
    (Word.toList (M := G)
        (Word.Pair.tail (M := G) (i := i)
          ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) (w.toWord (G := G)))) :
      List ((i : ι) × G i))
    (Sigma.mk (β := fun (i : ι) ↦ G i) j g)
⊢ g ∈ d.set (G := G) j

Tactic:
exact w.normalized _ _ (Word.mem_of_mem_equivPair_tail _ hg)

Premises used: Monoid.CoprodI.Word.mem_of_mem_equivPair_tail, Monoid.PushoutI.NormalWord.normalized