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 : NormalWord (G := G) d
empty :
  HSMul.hSMul (α := PushoutI (G := G) φ) (β := NormalWord (G := G) d)
      (prod (G := G) (d := d) (NormalWord.empty (G := G))) (NormalWord.empty (G := G)) =
    NormalWord.empty (G := G)
cons :
  ∀ (i : ι) (g : G i) (w : NormalWord (G := G) d) (hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i),
    g ∈ d.set (G := G) i →
      ∀ (hgr : g ∉ (φ i).range),
        w.head (G := G) = 1 →
          ∀ (ih : HSMul.hSMul (β := NormalWord (G := G) d) (w.prod (G := G)) (NormalWord.empty (G := G)) = w),
            HSMul.hSMul (β := NormalWord (G := G) d) ((NormalWord.cons (G := G) g w hmw hgr).prod (G := G))
                (NormalWord.empty (G := G)) =
              NormalWord.cons (G := G) g w hmw hgr
base :
  ∀ (h : H) (w : NormalWord (G := G) d),
    w.head (G := G) = 1 →
      ∀ (ih : HSMul.hSMul (β := NormalWord (G := G) d) (w.prod (G := G)) (NormalWord.empty (G := G)) = w),
        HSMul.hSMul (β := NormalWord (G := G) d)
            ((HSMul.hSMul (α := PushoutI (G := G) φ)
                  ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w).prod
              (G := G))
            (NormalWord.empty (G := G)) =
          HSMul.hSMul (α := PushoutI (G := G) φ)
            ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w
⊢ HSMul.hSMul (β := NormalWord (G := G) d) (w.prod (G := G)) (NormalWord.empty (G := G)) = w

Tactic:
induction w using consRecOn with
  | empty => simp
  | cons i g w _ _ _ _ ih =>
    rw [prod_cons, mul_smul, ih, cons_eq_smul]
  | base h w _ ih =>
    rw [prod_smul, mul_smul, ih]

Premises used: Monoid.PushoutI.NormalWord.empty, Monoid.PushoutI.NormalWord.prod_cons, Monoid.PushoutI.base, Monoid.PushoutI.NormalWord.cons_eq_smul, Monoid.PushoutI.NormalWord.prod_smul, Monoid.PushoutI.NormalWord.cons, SemigroupAction.mul_smul
-- 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)
g : PushoutI (G := G) φ
⊢ (fun (w : NormalWord (G := G) d) ↦ w.prod (G := G))
      ((fun (g : PushoutI (G := G) φ) ↦ HSMul.hSMul (β := NormalWord (G := G) d) g (empty (G := G))) g) =
    g

Tactic:
simp only [prod_smul, prod_empty, mul_one]

Premises used: Monoid.PushoutI.NormalWord.prod_empty, Monoid.PushoutI.NormalWord.prod_smul, mul_one
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
H : Type u_3
inst : Group H
ι : Type u_5
G : ι → Type u_6
inst_1 : (i : ι) → Group (G i)
φ : (i : ι) → MonoidHom.{u_3, u_6} H (G i)
d : Transversal (G := G) φ
this_1 : DecidableEq ι := Classical.decEq ι
this : (i : ι) → DecidableEq (G i) := fun (i : ι) ↦ Classical.decEq (G i)
⊢ Injective (α := NormalWord (G := G) d) (prod (G := G))

Tactic:
equiv.symm.injective

Premises used: Monoid.PushoutI.NormalWord.equiv, Monoid.PushoutI.NormalWord.prod, Quotient.map₂, Equiv.injective, Equiv.symm
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
H : Type u_3
inst : Group H
ι : Type u_5
G : ι → Type u_6
inst_1 : (i : ι) → Group (G i)
φ : (i : ι) → MonoidHom.{u_3, u_6} H (G i)
d : Transversal (G := G) φ
this_1 : DecidableEq ι := Classical.decEq ι
this : (i : ι) → DecidableEq (G i) := fun (i : ι) ↦ Classical.decEq (G i)
⊢ Injective (α := NormalWord (G := G) d) (prod (G := G))

Tactic:
exact equiv.symm.injective

Premises used: Monoid.PushoutI.NormalWord.equiv, Equiv.injective, Equiv.symm
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
H : Type u_3
inst : Group H
ι : Type u_5
G : ι → Type u_6
inst_1 : (i : ι) → Group (G i)
φ : (i : ι) → MonoidHom.{u_3, u_6} H (G i)
d : Transversal (G := G) φ
this_1 : DecidableEq ι := Classical.decEq ι
this : (i : ι) → DecidableEq (G i) := fun (i : ι) ↦ Classical.decEq (G i)
⊢ Injective (α := NormalWord (G := G) d) (prod (G := G))

Tactic:
classical exact equiv.symm.injective

Premises used: Monoid.PushoutI.NormalWord.equiv, Equiv.injective, Equiv.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)
m₁ m₂ : PushoutI (G := G) φ
h : ∀ (a : NormalWord (G := G) d), m₁ • a = m₂ • a
⊢ m₁ = m₂

Tactic:
simpa using congr_arg prod (h empty)

Premises used: Monoid.PushoutI.NormalWord.prod, Monoid.PushoutI.NormalWord.empty, congr_arg
-- 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 : ι
⊢ ∀ {m₁ m₂ : G i}, (∀ (a : NormalWord (G := G) d), m₁ • a = m₂ • a) → m₁ = m₂

Tactic:
simp [summand_smul_def']

Premises used: Monoid.PushoutI.NormalWord.summand_smul_def'
-- 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)
⊢ ∀ {m₁ m₂ : H}, (∀ (a : NormalWord (G := G) d), m₁ • a = m₂ • a) → m₁ = m₂

Tactic:
simp [base_smul_def']

Premises used: Monoid.PushoutI.NormalWord.base_smul_def'
-- 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)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i : ι
rcases :
  ∀ (d : Transversal (G := G) φ),
    Injective (α := G i) (β := PushoutI (G := G) φ) (⇑(of (G := G) i) : (a : G i) → PushoutI φ)
⊢ Injective (α := G i) (β := PushoutI (G := G) φ) (⇑(of (G := G) i) : (a : G i) → PushoutI φ)

Tactic:
rcases transversal_nonempty φ hφ with ⟨d⟩

Premises used: Monoid.PushoutI.NormalWord.transversal_nonempty
-- 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)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i : ι
d : Transversal (G := G) φ
x : DecidableEq ι := Classical.decEq ι
x_1 : (i : ι) → DecidableEq (G i) := fun (i : ι) ↦ Classical.decEq (G i)
⊢ Injective (α := G i) (β := PushoutI (G := G) φ) (⇑(of (G := G) i) : (a : G i) → PushoutI φ)

Tactic:
Function.Injective.of_comp
    (f := ((· • ·) : PushoutI φ → NormalWord d → NormalWord d)) ?_

Premises used: Function.Injective.of_comp
-- 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)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i : ι
d : Transversal (G := G) φ
x : DecidableEq ι := Classical.decEq ι
x_1 : (i : ι) → DecidableEq (G i) := fun (i : ι) ↦ Classical.decEq (G i)
refine :
  Injective (α := G i) (β := NormalWord (G := G) d → NormalWord (G := G) d)
    ((fun (x1 : PushoutI (G := G) φ) (x2 : NormalWord (G := G) d) ↦ x1 • x2) ∘
      (⇑(of (G := G) i) : (a : G i) → PushoutI φ))
⊢ Injective (α := G i) (β := PushoutI (G := G) φ) (⇑(of (G := G) i) : (a : G i) → PushoutI φ)

Tactic:
refine Function.Injective.of_comp
    (f := ((· • ·) : PushoutI φ → NormalWord d → NormalWord d)) ?_

Premises used: Function.Injective.of_comp
-- 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)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i : ι
d : Transversal (G := G) φ
x : DecidableEq ι := Classical.decEq ι
x_1 : (i : ι) → DecidableEq (G i) := fun (i : ι) ↦ Classical.decEq (G i)
a₁ : G i
_ :
  ∀ ⦃a₂ : G i⦄,
    Eq (α := NormalWord (G := G) d → NormalWord (G := G) d)
        (((fun (x1 : PushoutI (G := G) φ) (x2 : NormalWord (G := G) d) ↦ x1 • x2) ∘
            (⇑(of (G := G) i) : (a : G i) → PushoutI φ))
          a₁)
        (((fun (x1 : PushoutI (G := G) φ) (x2 : NormalWord (G := G) d) ↦ x1 • x2) ∘
            (⇑(of (G := G) i) : (a : G i) → PushoutI φ))
          a₂) →
      a₁ = a₂
⊢ ∀ ⦃a₂ : G i⦄,
    Eq (α := NormalWord (G := G) d → NormalWord (G := G) d)
        (((fun (x1 : PushoutI (G := G) φ) (x2 : NormalWord (G := G) d) ↦ x1 • x2) ∘
            (⇑(of (G := G) i) : (a : G i) → PushoutI φ))
          a₁)
        (((fun (x1 : PushoutI (G := G) φ) (x2 : NormalWord (G := G) d) ↦ x1 • x2) ∘
            (⇑(of (G := G) i) : (a : G i) → PushoutI φ))
          a₂) →
      a₁ = a₂

Tactic:
_
-- 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)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i : ι
d : Transversal (G := G) φ
x : DecidableEq ι := Classical.decEq ι
x_1 : (i : ι) → DecidableEq (G i) := fun (i : ι) ↦ Classical.decEq (G i)
a₁ a₂ : G i
h :
  Eq (α := NormalWord (G := G) d → NormalWord (G := G) d)
    (((fun (x1 : PushoutI (G := G) φ) (x2 : NormalWord (G := G) d) ↦ x1 • x2) ∘
        (⇑(of (G := G) i) : (a : G i) → PushoutI φ))
      a₁)
    (((fun (x1 : PushoutI (G := G) φ) (x2 : NormalWord (G := G) d) ↦ x1 • x2) ∘
        (⇑(of (G := G) i) : (a : G i) → PushoutI φ))
      a₂)
w : NormalWord (G := G) d
⊢ a₁ • w = a₂ • w

Tactic:
simp_all [funext_iff, of_smul_eq_smul]

Premises used: funext_iff, Monoid.PushoutI.NormalWord.of_smul_eq_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)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i : ι
d : Transversal (G := G) φ
x : DecidableEq ι := Classical.decEq ι
x_1 : (i : ι) → DecidableEq (G i) := fun (i : ι) ↦ Classical.decEq (G i)
a₁ a₂ : G i
h :
  Eq (α := NormalWord (G := G) d → NormalWord (G := G) d)
    (((fun (x1 : PushoutI (G := G) φ) (x2 : NormalWord (G := G) d) ↦ x1 • x2) ∘
        (⇑(of (G := G) i) : (a : G i) → PushoutI φ))
      a₁)
    (((fun (x1 : PushoutI (G := G) φ) (x2 : NormalWord (G := G) d) ↦ x1 • x2) ∘
        (⇑(of (G := G) i) : (a : G i) → PushoutI φ))
      a₂)
⊢ a₁ = a₂

Tactic:
exact eq_of_smul_eq_smul (fun w : NormalWord d =>
    by simp_all [funext_iff, of_smul_eq_smul])

Premises used: FaithfulSMul.eq_of_smul_eq_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)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
rcases :
  ∀ (d : Transversal (G := G) φ),
    Injective (α := H) (β := PushoutI (G := G) φ) (⇑(base (G := G) φ) : (a : H) → PushoutI φ)
⊢ Injective (α := H) (β := PushoutI (G := G) φ) (⇑(base (G := G) φ) : (a : H) → PushoutI φ)

Tactic:
rcases transversal_nonempty φ hφ with ⟨d⟩

Premises used: Monoid.PushoutI.NormalWord.transversal_nonempty
-- 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)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
d : Transversal (G := G) φ
x : DecidableEq ι := Classical.decEq ι
x_1 : (i : ι) → DecidableEq (G i) := fun (i : ι) ↦ Classical.decEq (G i)
⊢ Injective (α := H) (β := PushoutI (G := G) φ) (⇑(base (G := G) φ) : (a : H) → PushoutI φ)

Tactic:
Function.Injective.of_comp
    (f := ((· • ·) : PushoutI φ → NormalWord d → NormalWord d)) ?_

Premises used: Function.Injective.of_comp
-- 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)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
d : Transversal (G := G) φ
x : DecidableEq ι := Classical.decEq ι
x_1 : (i : ι) → DecidableEq (G i) := fun (i : ι) ↦ Classical.decEq (G i)
refine :
  Injective (α := H) (β := NormalWord (G := G) d → NormalWord (G := G) d)
    ((fun (x1 : PushoutI (G := G) φ) (x2 : NormalWord (G := G) d) ↦ x1 • x2) ∘
      (⇑(base (G := G) φ) : (a : H) → PushoutI φ))
⊢ Injective (α := H) (β := PushoutI (G := G) φ) (⇑(base (G := G) φ) : (a : H) → PushoutI φ)

Tactic:
refine Function.Injective.of_comp
    (f := ((· • ·) : PushoutI φ → NormalWord d → NormalWord d)) ?_

Premises used: Function.Injective.of_comp
-- 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)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
d : Transversal (G := G) φ
x : DecidableEq ι := Classical.decEq ι
x_1 : (i : ι) → DecidableEq (G i) := fun (i : ι) ↦ Classical.decEq (G i)
a₁ : H
_ :
  ∀ ⦃a₂ : H⦄,
    Eq (α := NormalWord (G := G) d → NormalWord (G := G) d)
        (((fun (x1 : PushoutI (G := G) φ) (x2 : NormalWord (G := G) d) ↦ x1 • x2) ∘
            (⇑(base (G := G) φ) : (a : H) → PushoutI φ))
          a₁)
        (((fun (x1 : PushoutI (G := G) φ) (x2 : NormalWord (G := G) d) ↦ x1 • x2) ∘
            (⇑(base (G := G) φ) : (a : H) → PushoutI φ))
          a₂) →
      a₁ = a₂
⊢ ∀ ⦃a₂ : H⦄,
    Eq (α := NormalWord (G := G) d → NormalWord (G := G) d)
        (((fun (x1 : PushoutI (G := G) φ) (x2 : NormalWord (G := G) d) ↦ x1 • x2) ∘
            (⇑(base (G := G) φ) : (a : H) → PushoutI φ))
          a₁)
        (((fun (x1 : PushoutI (G := G) φ) (x2 : NormalWord (G := G) d) ↦ x1 • x2) ∘
            (⇑(base (G := G) φ) : (a : H) → PushoutI φ))
          a₂) →
      a₁ = a₂

Tactic:
_
-- 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)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
d : Transversal (G := G) φ
x : DecidableEq ι := Classical.decEq ι
x_1 : (i : ι) → DecidableEq (G i) := fun (i : ι) ↦ Classical.decEq (G i)
a₁ a₂ : H
h :
  Eq (α := NormalWord (G := G) d → NormalWord (G := G) d)
    (((fun (x1 : PushoutI (G := G) φ) (x2 : NormalWord (G := G) d) ↦ x1 • x2) ∘
        (⇑(base (G := G) φ) : (a : H) → PushoutI φ))
      a₁)
    (((fun (x1 : PushoutI (G := G) φ) (x2 : NormalWord (G := G) d) ↦ x1 • x2) ∘
        (⇑(base (G := G) φ) : (a : H) → PushoutI φ))
      a₂)
w : NormalWord (G := G) d
⊢ a₁ • w = a₂ • w

Tactic:
simp_all [funext_iff, base_smul_eq_smul]

Premises used: Monoid.PushoutI.NormalWord.base_smul_eq_smul, funext_iff
-- 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)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
d : Transversal (G := G) φ
x : DecidableEq ι := Classical.decEq ι
x_1 : (i : ι) → DecidableEq (G i) := fun (i : ι) ↦ Classical.decEq (G i)
a₁ a₂ : H
h :
  Eq (α := NormalWord (G := G) d → NormalWord (G := G) d)
    (((fun (x1 : PushoutI (G := G) φ) (x2 : NormalWord (G := G) d) ↦ x1 • x2) ∘
        (⇑(base (G := G) φ) : (a : H) → PushoutI φ))
      a₁)
    (((fun (x1 : PushoutI (G := G) φ) (x2 : NormalWord (G := G) d) ↦ x1 • x2) ∘
        (⇑(base (G := G) φ) : (a : H) → PushoutI φ))
      a₂)
⊢ a₁ = a₂

Tactic:
exact eq_of_smul_eq_smul (fun w : NormalWord d =>
    by simp_all [funext_iff, base_smul_eq_smul])

Premises used: FaithfulSMul.eq_of_smul_eq_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) φ
hw : Reduced (G := G) φ (Word.empty (M := G))
⊢ Eq (α := PushoutI (G := G) φ) (NormalWord.prod (G := G) (d := d) (empty (G := G)))
    ((ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (Word.prod (M := G) (Word.empty (M := G))))

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) φ
hw : Reduced (G := G) φ (Word.empty (M := G))
⊢ ∃ (w' : NormalWord (G := G) d),
    w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (Word.prod (M := G) (Word.empty (M := G))) ∧
      List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
        List.map (α := (i : ι) × G i) (Sigma.fst (β := fun (i : ι) ↦ G i)) (Word.toList (M := G) (Word.empty (M := G)))

Tactic:
exact ⟨empty, by simp, rfl⟩
-- 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 : Word G
hIdx : w.fstIdx (M := G) ≠ some i
hg1 : g ≠ 1
ih :
  ∀ (hw : Reduced (G := G) φ w),
    ∃ (w' : NormalWord (G := G) d),
      w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) ∧
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
          List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
hw : Reduced (G := G) φ (Word.cons (M := G) g w hIdx hg1)
cons :
  ∀ (w' : NormalWord (G := G) d)
    (hw'prod : w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)))
    (hw'map :
      List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))),
    ∃ (w' : NormalWord (G := G) d),
      w'.prod (G := G) =
          (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) ((Word.cons (M := G) g w hIdx hg1).prod (M := G)) ∧
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
          List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) ((Word.cons (M := G) g w hIdx hg1).toList (M := G))
⊢ ∃ (w' : NormalWord (G := G) d),
    w'.prod (G := G) =
        (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) ((Word.cons (M := G) g w hIdx hg1).prod (M := G)) ∧
      List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) ((Word.cons (M := G) g w hIdx hg1).toList (M := G))

Tactic:
rcases ih (fun _ hg => hw _ (List.mem_cons_of_mem _ hg)) with
      ⟨w', hw'prod, hw'map⟩

Premises used: List.mem_cons_of_mem, Sigma.mk
-- 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 : Word G
hIdx : w.fstIdx (M := G) ≠ some i
hg1 : g ≠ 1
ih :
  ∀ (hw : Reduced (G := G) φ w),
    ∃ (w' : NormalWord (G := G) d),
      w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) ∧
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
          List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
hw : Reduced (G := G) φ (Word.cons (M := G) g w hIdx hg1)
w' : NormalWord (G := G) d
hw'prod : w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G))
hw'map :
  List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
    List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
⊢ ∃ (w' : NormalWord (G := G) d),
    w'.prod (G := G) =
        (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) ((Word.cons (M := G) g w hIdx hg1).prod (M := G)) ∧
      List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) ((Word.cons (M := G) g w hIdx hg1).toList (M := G))

Tactic:
⟨cons g w' ?_ ?_, ?_⟩

Premises used: Exists.intro, 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) φ
i : ι
g : G i
w : Word G
hIdx : w.fstIdx (M := G) ≠ some i
hg1 : g ≠ 1
ih :
  ∀ (hw : Reduced (G := G) φ w),
    ∃ (w' : NormalWord (G := G) d),
      w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) ∧
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
          List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
hw : Reduced (G := G) φ (Word.cons (M := G) g w hIdx hg1)
w' : NormalWord (G := G) d
hw'prod : w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G))
hw'map :
  List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
    List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
cons : w'.toWord (G := G).fstIdx (M := G) ≠ some i
cons₁ : g ∉ (φ i).range
cons₂ :
  (NormalWord.cons (G := G) g w' ⋯ ⋯).prod (G := G) =
      (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) ((Word.cons (M := G) g w hIdx hg1).prod (M := G)) ∧
    List.map (Sigma.fst (β := fun (i : ι) ↦ G i))
        ((NormalWord.cons (G := G) g w' ⋯ ⋯).toWord (G := G).toList (M := G)) =
      List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) ((Word.cons (M := G) g w hIdx hg1).toList (M := G))
⊢ ∃ (w' : NormalWord (G := G) d),
    w'.prod (G := G) =
        (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) ((Word.cons (M := G) g w hIdx hg1).prod (M := G)) ∧
      List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) ((Word.cons (M := G) g w hIdx hg1).toList (M := G))

Tactic:
refine ⟨cons g w' ?_ ?_, ?_⟩
-- 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 : Word G
hIdx : w.fstIdx (M := G) ≠ some i
hg1 : g ≠ 1
ih :
  ∀ (hw : Reduced (G := G) φ w),
    ∃ (w' : NormalWord (G := G) d),
      w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) ∧
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
          List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
hw : Reduced (G := G) φ (Word.cons (M := G) g w hIdx hg1)
w' : NormalWord (G := G) d
hw'prod : w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G))
hw'map :
  List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
    List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
cons : Option.map (Sigma.fst (β := fun (i : ι) ↦ G i)) w'.toWord (G := G).toList (M := G).head? ≠ some i
cons₁ : (List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G))).head? ≠ some i
cons₂ : (List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))).head? ≠ some i
cons₃ cons₄ cons₅ cons₆ : Option.map (Sigma.fst (β := fun (i : ι) ↦ G i)) w.toList (M := G).head? ≠ some i
⊢ w'.toWord (G := G).fstIdx (M := G) ≠ some i

Tactic:
rwa [Word.fstIdx, ← List.head?_map, hw'map, List.head?_map]

Premises used: List.head?_map, Monoid.CoprodI.Word.fstIdx