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 : ι) → Monoid (G i)
inst_2 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
x : { f : ((i : ι) → MonoidHom.{u_2, u_4} (G i) K) × (H →* K) // ∀ (i : ι), (f.1 i).comp (φ i) = f.2 }
fst : (i : ι) → MonoidHom.{u_2, u_4} (G i) K
snd : H →* K
property : ∀ (i : ι), ((fst, snd).1 i).comp (φ i) = (fst, snd).2
⊢ Eq (α := { f : ((i : ι) → MonoidHom.{u_2, u_4} (G i) K) × (H →* K) // ∀ (i : ι), (f.1 i).comp (φ i) = f.2 })
    ((fun (f : PushoutI (G := G) φ →* K) ↦
        (Subtype.mk (p := fun (f : ((i : ι) → MonoidHom.{u_2, u_4} (G i) K) × (H →* K)) ↦
            ∀ (i : ι), (f.1 i).comp (φ i) = f.2) (fun (i : ι) ↦ f.comp (of (G := G) i), f.comp (base (G := G) φ)) ⋯ :
          { f : ((i : ι) → MonoidHom.{u_2, u_4} (G i) K) × (H →* K) // ∀ (i : ι), (f.1 i).comp (φ i) = f.2 }))
      ((fun (f : { f : ((i : ι) → MonoidHom.{u_2, u_4} (G i) K) × (H →* K) // ∀ (i : ι), (f.1 i).comp (φ i) = f.2 }) ↦
          lift (G := G) (↑f : ((i : ι) → G i →* K) × (H →* K)).1 (↑f : ((i : ι) → G i →* K) × (H →* K)).2 ⋯)
        (Subtype.mk (p := fun (f : ((i : ι) → MonoidHom.{u_2, u_4} (G i) K) × (H →* K)) ↦
          ∀ (i : ι), (f.1 i).comp (φ i) = f.2) (fst, snd) property)))
    (Subtype.mk (p := fun (f : ((i : ι) → MonoidHom.{u_2, u_4} (G i) K) × (H →* K)) ↦
      ∀ (i : ι), (f.1 i).comp (φ i) = f.2) (fst, snd) property)

Tactic:
simp [DFunLike.ext_iff, funext_iff]

Premises used: funext_iff, DFunLike.ext_iff
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Monoid (G i)
inst_1 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
i : ι
g : G i
⊢ Eq (α := PushoutI (G := G) φ)
    ((ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) ((CoprodI.of (M := G) : (a : G i) → CoprodI G) g) :
      PushoutI (G := G) φ)
    ((of (G := G) i : (a : G i) → PushoutI φ) g : PushoutI (G := G) φ)

Tactic:
simp [ofCoprodI]

Premises used: Monoid.PushoutI.ofCoprodI
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Monoid (G i)
inst_1 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
motive : (con (G := G) φ).Quotient → Prop
of :
  ∀ (i : ι) (g : G i),
    motive (((con (G := G) φ).mk'.comp (MonoidHom.comp inl (CoprodI.of (M := G))) : (a : G i) → (con φ).Quotient) g)
base : ∀ (h : H), motive (((con (G := G) φ).mk'.comp inr : (a : H) → (con φ).Quotient) h)
mul : ∀ (x y : (con (G := G) φ).Quotient), motive x → motive y → motive (x * y)
i : ι
g : G i
⊢ motive
    (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) ((CoprodI.of (M := G) : (a : G i) → CoprodI G) g)) : (con φ).Quotient)

Tactic:
of i g

Premises used: Con.toQuotient
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Monoid (G i)
inst_1 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
motive : (con (G := G) φ).Quotient → Prop
of :
  ∀ (i : ι) (g : G i),
    motive (((con (G := G) φ).mk'.comp (MonoidHom.comp inl (CoprodI.of (M := G))) : (a : G i) → (con φ).Quotient) g)
base : ∀ (h : H), motive (((con (G := G) φ).mk'.comp inr : (a : H) → (con φ).Quotient) h)
mul : ∀ (x y : (con (G := G) φ).Quotient), motive x → motive y → motive (x * y)
i : ι
g : G i
⊢ motive
    (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) ((CoprodI.of (M := G) : (a : G i) → CoprodI G) g)) : (con φ).Quotient)

Tactic:
exact of i g
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Monoid (G i)
inst_1 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
motive : (con (G := G) φ).Quotient → Prop
of :
  ∀ (i : ι) (g : G i),
    motive (((con (G := G) φ).mk'.comp (MonoidHom.comp inl (CoprodI.of (M := G))) : (a : G i) → (con φ).Quotient) g)
base : ∀ (h : H), motive (((con (G := G) φ).mk'.comp inr : (a : H) → (con φ).Quotient) h)
mul : ∀ (x y : (con (G := G) φ).Quotient), motive x → motive y → motive (x * y)
x y : CoprodI G
ihx : motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) x) : (con φ).Quotient)
ihy : motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) y) : (con φ).Quotient)
H₁ :
  motive
    (↑(HMul.hMul (α := CoprodI G ∗ H) (β := CoprodI G ∗ H) ((inl : (a : CoprodI G) → CoprodI G ∗ H) x : CoprodI G ∗ H)
          ((inl : (a : CoprodI G) → CoprodI G ∗ H) y : CoprodI G ∗ H)) :
      (con φ).Quotient)
⊢ motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) (x * y)) : (con φ).Quotient)

Tactic:
rw [map_mul]

Premises used: map_mul
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Monoid (G i)
inst_1 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
motive : (con (G := G) φ).Quotient → Prop
of :
  ∀ (i : ι) (g : G i),
    motive (((con (G := G) φ).mk'.comp (MonoidHom.comp inl (CoprodI.of (M := G))) : (a : G i) → (con φ).Quotient) g)
base : ∀ (h : H), motive (((con (G := G) φ).mk'.comp inr : (a : H) → (con φ).Quotient) h)
mul : ∀ (x y : (con (G := G) φ).Quotient), motive x → motive y → motive (x * y)
x y : CoprodI G
ihx : motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) x) : (con φ).Quotient)
ihy : motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) y) : (con φ).Quotient)
⊢ motive
    (↑(HMul.hMul (α := CoprodI G ∗ H) (β := CoprodI G ∗ H) ((inl : (a : CoprodI G) → CoprodI G ∗ H) x : CoprodI G ∗ H)
          ((inl : (a : CoprodI G) → CoprodI G ∗ H) y : CoprodI G ∗ H)) :
      (con φ).Quotient)

Tactic:
mul _ _ ihx ihy

Premises used: Quotient.map₂, Con.toQuotient
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Monoid (G i)
inst_1 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
motive : (con (G := G) φ).Quotient → Prop
of :
  ∀ (i : ι) (g : G i),
    motive (((con (G := G) φ).mk'.comp (MonoidHom.comp inl (CoprodI.of (M := G))) : (a : G i) → (con φ).Quotient) g)
base : ∀ (h : H), motive (((con (G := G) φ).mk'.comp inr : (a : H) → (con φ).Quotient) h)
mul : ∀ (x y : (con (G := G) φ).Quotient), motive x → motive y → motive (x * y)
x y : CoprodI G
ihx : motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) x) : (con φ).Quotient)
ihy : motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) y) : (con φ).Quotient)
⊢ motive
    (↑(HMul.hMul (α := CoprodI G ∗ H) (β := CoprodI G ∗ H) ((inl : (a : CoprodI G) → CoprodI G ∗ H) x : CoprodI G ∗ H)
          ((inl : (a : CoprodI G) → CoprodI G ∗ H) y : CoprodI G ∗ H)) :
      (con φ).Quotient)

Tactic:
exact mul _ _ ihx ihy
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Monoid (G i)
inst_1 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
motive : (con (G := G) φ).Quotient → Prop
of :
  ∀ (i : ι) (g : G i),
    motive (((con (G := G) φ).mk'.comp (MonoidHom.comp inl (CoprodI.of (M := G))) : (a : G i) → (con φ).Quotient) g)
base : ∀ (h : H), motive (((con (G := G) φ).mk'.comp inr : (a : H) → (con φ).Quotient) h)
mul : ∀ (x y : (con (G := G) φ).Quotient), motive x → motive y → motive (x * y)
⊢ motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) 1) : (con φ).Quotient)

Tactic:
simpa using base 1

Premises used: OfNat.ofNat
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Monoid (G i)
inst_1 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
motive : (con (G := G) φ).Quotient → Prop
of :
  ∀ (i : ι) (g : G i),
    motive (((con (G := G) φ).mk'.comp (MonoidHom.comp inl (CoprodI.of (M := G))) : (a : G i) → (con φ).Quotient) g)
base : ∀ (h : H), motive (((con (G := G) φ).mk'.comp inr : (a : H) → (con φ).Quotient) h)
mul : ∀ (x y : (con (G := G) φ).Quotient), motive x → motive y → motive (x * y)
g : CoprodI G
H₁ :
  ∀ (i : ι) (g : G i),
    motive
      (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) ((CoprodI.of (M := G) : (a : G i) → CoprodI G) g)) : (con φ).Quotient)
H₂ :
  ∀ (x y : CoprodI G) (ihx : motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) x) : (con φ).Quotient))
    (ihy : motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) y) : (con φ).Quotient)),
    motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) (x * y)) : (con φ).Quotient)
H₃ : motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) 1) : (con φ).Quotient)
⊢ motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) g) : (con φ).Quotient)

Tactic:
induction g using CoprodI.induction_on with
      | of i g => exact of i g
      | mul x y ihx ihy =>
        rw [map_mul]
        exact mul _ _ ihx ihy
      | one => simpa using base 1

Premises used: map_mul, Subgroup.one, OfNat.ofNat
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Monoid (G i)
inst_1 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
motive : (con (G := G) φ).Quotient → Prop
of :
  ∀ (i : ι) (g : G i),
    motive (((con (G := G) φ).mk'.comp (MonoidHom.comp inl (CoprodI.of (M := G))) : (a : G i) → (con φ).Quotient) g)
base : ∀ (h : H), motive (((con (G := G) φ).mk'.comp inr : (a : H) → (con φ).Quotient) h)
mul : ∀ (x y : (con (G := G) φ).Quotient), motive x → motive y → motive (x * y)
h : H
⊢ motive (↑((inr : (a : H) → CoprodI G ∗ H) h) : (con φ).Quotient)

Tactic:
base h

Premises used: Con.toQuotient
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Monoid (G i)
inst_1 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
motive : (con (G := G) φ).Quotient → Prop
of :
  ∀ (i : ι) (g : G i),
    motive (((con (G := G) φ).mk'.comp (MonoidHom.comp inl (CoprodI.of (M := G))) : (a : G i) → (con φ).Quotient) g)
base : ∀ (h : H), motive (((con (G := G) φ).mk'.comp inr : (a : H) → (con φ).Quotient) h)
mul : ∀ (x y : (con (G := G) φ).Quotient), motive x → motive y → motive (x * y)
h : H
⊢ motive (↑((inr : (a : H) → CoprodI G ∗ H) h) : (con φ).Quotient)

Tactic:
exact base h
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Monoid (G i)
inst_1 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
motive : (con (G := G) φ).Quotient → Prop
of :
  ∀ (i : ι) (g : G i),
    motive (((con (G := G) φ).mk'.comp (MonoidHom.comp inl (CoprodI.of (M := G))) : (a : G i) → (con φ).Quotient) g)
base : ∀ (h : H), motive (((con (G := G) φ).mk'.comp inr : (a : H) → (con φ).Quotient) h)
mul : ∀ (x y : (con (G := G) φ).Quotient), motive x → motive y → motive (x * y)
x y : CoprodI G ∗ H
ihx : motive (↑x : (con φ).Quotient)
ihy : motive (↑y : (con φ).Quotient)
⊢ motive (↑(x * y) : (con φ).Quotient)

Tactic:
mul _ _ ihx ihy

Premises used: Quotient.map₂, Con.toQuotient
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Monoid (G i)
inst_1 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
motive : (con (G := G) φ).Quotient → Prop
of :
  ∀ (i : ι) (g : G i),
    motive (((con (G := G) φ).mk'.comp (MonoidHom.comp inl (CoprodI.of (M := G))) : (a : G i) → (con φ).Quotient) g)
base : ∀ (h : H), motive (((con (G := G) φ).mk'.comp inr : (a : H) → (con φ).Quotient) h)
mul : ∀ (x y : (con (G := G) φ).Quotient), motive x → motive y → motive (x * y)
x y : CoprodI G ∗ H
ihx : motive (↑x : (con φ).Quotient)
ihy : motive (↑y : (con φ).Quotient)
⊢ motive (↑(x * y) : (con φ).Quotient)

Tactic:
exact mul _ _ ihx ihy
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Monoid (G i)
inst_1 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
motive : (con (G := G) φ).Quotient → Prop
of :
  ∀ (i : ι) (g : G i),
    motive (((con (G := G) φ).mk'.comp (MonoidHom.comp inl (CoprodI.of (M := G))) : (a : G i) → (con φ).Quotient) g)
base : ∀ (h : H), motive (((con (G := G) φ).mk'.comp inr : (a : H) → (con φ).Quotient) h)
mul : ∀ (x y : (con (G := G) φ).Quotient), motive x → motive y → motive (x * y)
x : CoprodI G ∗ H
H₁ : ∀ (g : CoprodI G), motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) g) : (con φ).Quotient)
H₂ : ∀ (h : H), motive (↑((inr : (a : H) → CoprodI G ∗ H) h) : (con φ).Quotient)
H₃ :
  ∀ (x y : CoprodI G ∗ H) (ihx : motive (↑x : (con φ).Quotient)) (ihy : motive (↑y : (con φ).Quotient)),
    motive (↑(x * y) : (con φ).Quotient)
⊢ motive (↑x : (con φ).Quotient)

Tactic:
induction x using Coprod.induction_on with
    | inl g =>
      induction g using CoprodI.induction_on with
      | of i g => exact of i g
      | mul x y ihx ihy =>
        rw [map_mul]
        exact mul _ _ ihx ihy
      | one => simpa using base 1
    | inr h => exact base h
    | mul x y ihx ihy => exact mul _ _ ihx ihy

Premises used: map_mul, Subgroup.one, Monoid.Coprod.inl, Monoid.Coprod.inr, OfNat.ofNat
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Monoid (G i)
inst_1 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
motive : (con (G := G) φ).Quotient → Prop
x : (con (G := G) φ).Quotient
of :
  ∀ (i : ι) (g : G i),
    motive (((con (G := G) φ).mk'.comp (MonoidHom.comp inl (CoprodI.of (M := G))) : (a : G i) → (con φ).Quotient) g)
base : ∀ (h : H), motive (((con (G := G) φ).mk'.comp inr : (a : H) → (con φ).Quotient) h)
mul : ∀ (x y : (con (G := G) φ).Quotient), motive x → motive y → motive (x * y)
H₁ : ∀ (x : CoprodI G ∗ H), motive (↑x : (con φ).Quotient)
⊢ motive x

Tactic:
induction x using Con.induction_on with
  | H x =>
    induction x using Coprod.induction_on with
    | inl g =>
      induction g using CoprodI.induction_on with
      | of i g => exact of i g
      | mul x y ihx ihy =>
        rw [map_mul]
        exact mul _ _ ihx ihy
      | one => simpa using base 1
    | inr h => exact base h
    | mul x y ihx ihy => exact mul _ _ ihx ihy

Premises used: map_mul, Subgroup.one, Monoid.Coprod.inl, Monoid.Coprod.inr, OfNat.ofNat
-- 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)
choose :
  ∀ (t : (i : ι) → Set (G i)) (ht : ∀ (i : ι), IsComplement (↑(φ i).range : Set (G i)) (t i) ∧ 1 ∈ t i),
    Nonempty (Transversal (G := G) φ)
⊢ Nonempty (Transversal (G := G) φ)

Tactic:
choose t ht using fun i => (φ i).range.exists_isComplement_right 1

Premises used: MonoidHom.range, OfNat.ofNat, Subgroup.exists_isComplement_right
-- 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)
t : (i : ι) → Set (G i)
ht : ∀ (i : ι), IsComplement (↑(φ i).range : Set (G i)) (t i) ∧ 1 ∈ t i
val : Transversal (G := G) φ
⊢ Nonempty (Transversal (G := G) φ)

Tactic:
apply Nonempty.intro

Premises used: Nonempty.intro
-- 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)
t : (i : ι) → Set (G i)
ht : ∀ (i : ι), IsComplement (↑(φ i).range : Set (G i)) (t i) ∧ 1 ∈ t i
⊢ Transversal (G := G) φ

Tactic:
exact
    { injective := hφ
      set := t
      one_mem := fun i => (ht i).2
      compl := fun i => (ht i).1 }
-- 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 : ι
g : G i
⊢ Membership.mem (γ := List ((i : ι) × G i)) (Word.toList (M := G) (Word.empty (M := G)))
      (Sigma.mk (β := fun (i : ι) ↦ G i) i g) →
    g ∈ d.set (G := G) i

Tactic:
simp [CoprodI.Word.empty]

Premises used: Monoid.CoprodI.Word.empty
-- 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 : ι
h : __src.toWord (G := G).fstIdx (M := G) = some i
⊢ False

Tactic:
cases 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) φ
w₁ w₂ : NormalWord (G := G) d
hhead : w₁.head (G := G) = w₂.head (G := G)
hlist : w₁.toWord (G := G).toList (M := G) = w₂.toWord (G := G).toList (M := G)
rcases :
  ∀ (head : H) (toList : List ((i : ι) × G i)) (ne_one : ∀ l ∈ toList, l.snd (β := fun (i : ι) ↦ G i) ≠ 1)
    (chain_ne :
      List.IsChain (fun (l l' : (i : ι) × G i) ↦ l.fst (β := fun (i : ι) ↦ G i) ≠ l'.fst (β := fun (i : ι) ↦ G i))
        toList)
    (normalized :
      ∀ (i : ι) (g : G i),
        Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ Word.toList (M := G) (Word.mk (M := G) toList ne_one chain_ne) →
          g ∈ d.set (G := G) i)
    (hhead : (mk (G := G) (Word.mk (M := G) toList ne_one chain_ne) head normalized).head (G := G) = w₂.head (G := G))
    (hlist :
      (mk (G := G) (Word.mk (M := G) toList ne_one chain_ne) head normalized).toWord (G := G).toList (M := G) =
        w₂.toWord (G := G).toList (M := G)),
    mk (G := G) (Word.mk (M := G) toList ne_one chain_ne) head normalized = w₂
⊢ w₁ = w₂

Tactic:
rcases w₁ with ⟨⟨_, _, _⟩, _, _⟩
-- 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) φ
w₂ : NormalWord (G := G) d
head : H
toList : List ((i : ι) × G i)
ne_one : ∀ l ∈ toList, l.snd (β := fun (i : ι) ↦ G i) ≠ 1
chain_ne :
  List.IsChain (fun (l l' : (i : ι) × G i) ↦ l.fst (β := fun (i : ι) ↦ G i) ≠ l'.fst (β := fun (i : ι) ↦ G i)) toList
normalized :
  ∀ (i : ι) (g : G i),
    Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ Word.toList (M := G) (Word.mk (M := G) toList ne_one chain_ne) →
      g ∈ d.set (G := G) i
hhead : (mk (G := G) (Word.mk (M := G) toList ne_one chain_ne) head normalized).head (G := G) = w₂.head (G := G)
hlist :
  (mk (G := G) (Word.mk (M := G) toList ne_one chain_ne) head normalized).toWord (G := G).toList (M := G) =
    w₂.toWord (G := G).toList (M := G)
rcases :
  ∀ (head_1 : H) (toList_1 : List ((i : ι) × G i)) (ne_one_1 : ∀ l ∈ toList_1, l.snd (β := fun (i : ι) ↦ G i) ≠ 1)
    (chain_ne_1 :
      List.IsChain (fun (l l' : (i : ι) × G i) ↦ l.fst (β := fun (i : ι) ↦ G i) ≠ l'.fst (β := fun (i : ι) ↦ G i))
        toList_1)
    (normalized_1 :
      ∀ (i : ι) (g : G i),
        Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ Word.toList (M := G) (Word.mk (M := G) toList_1 ne_one_1 chain_ne_1) →
          g ∈ d.set (G := G) i)
    (hhead :
      (mk (G := G) (Word.mk (M := G) toList ne_one chain_ne) head normalized).head (G := G) =
        (mk (G := G) (Word.mk (M := G) toList_1 ne_one_1 chain_ne_1) head_1 normalized_1).head (G := G))
    (hlist :
      (mk (G := G) (Word.mk (M := G) toList ne_one chain_ne) head normalized).toWord (G := G).toList (M := G) =
        (mk (G := G) (Word.mk (M := G) toList_1 ne_one_1 chain_ne_1) head_1 normalized_1).toWord (G := G).toList (M :=
          G)),
    mk (G := G) (Word.mk (M := G) toList ne_one chain_ne) head normalized =
      mk (G := G) (Word.mk (M := G) toList_1 ne_one_1 chain_ne_1) head_1 normalized_1
⊢ mk (G := G) (Word.mk (M := G) toList ne_one chain_ne) head normalized = w₂

Tactic:
rcases w₂ with ⟨⟨_, _, _⟩, _, _⟩
-- 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) φ
head : H
toList : List ((i : ι) × G i)
ne_one : ∀ l ∈ toList, l.snd (β := fun (i : ι) ↦ G i) ≠ 1
chain_ne :
  List.IsChain (fun (l l' : (i : ι) × G i) ↦ l.fst (β := fun (i : ι) ↦ G i) ≠ l'.fst (β := fun (i : ι) ↦ G i)) toList
normalized :
  ∀ (i : ι) (g : G i),
    Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ Word.toList (M := G) (Word.mk (M := G) toList ne_one chain_ne) →
      g ∈ d.set (G := G) i
head_1 : H
toList_1 : List ((i : ι) × G i)
ne_one_1 : ∀ l ∈ toList_1, l.snd (β := fun (i : ι) ↦ G i) ≠ 1
chain_ne_1 :
  List.IsChain (fun (l l' : (i : ι) × G i) ↦ l.fst (β := fun (i : ι) ↦ G i) ≠ l'.fst (β := fun (i : ι) ↦ G i)) toList_1
normalized_1 :
  ∀ (i : ι) (g : G i),
    Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ Word.toList (M := G) (Word.mk (M := G) toList_1 ne_one_1 chain_ne_1) →
      g ∈ d.set (G := G) i
hhead :
  (mk (G := G) (Word.mk (M := G) toList ne_one chain_ne) head normalized).head (G := G) =
    (mk (G := G) (Word.mk (M := G) toList_1 ne_one_1 chain_ne_1) head_1 normalized_1).head (G := G)
hlist :
  (mk (G := G) (Word.mk (M := G) toList ne_one chain_ne) head normalized).toWord (G := G).toList (M := G) =
    (mk (G := G) (Word.mk (M := G) toList_1 ne_one_1 chain_ne_1) head_1 normalized_1).toWord (G := G).toList (M := G)
⊢ mk (G := G) (Word.mk (M := G) toList ne_one chain_ne) head normalized =
    mk (G := G) (Word.mk (M := G) toList_1 ne_one_1 chain_ne_1) head_1 normalized_1

Tactic:
simp_all
-- 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) φ
⊢ ∀ (x y : H) (b : NormalWord (G := G) d), (x * y) • b = x • y • b

Tactic:
simp +instances [instHSMul, mul_assoc]

Premises used: instHSMul, mul_assoc
-- 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) φ
⊢ ∀ (b : NormalWord (G := G) d), HSMul.hSMul (α := H) 1 b = b

Tactic:
simp +instances [instHSMul]

Premises used: instHSMul
-- 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) φ
h : H
w : NormalWord (G := G) d
⊢ h • w = mk (G := G) (w.toWord (G := G)) (h * w.head (G := G)) ⋯

Tactic:
rfl

Premises used: 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) φ
h : H
w : NormalWord (G := G) d
⊢ (h • w).prod (G := G) =
    HMul.hMul (α := PushoutI (G := G) φ) ((base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ)
      (w.prod (G := G))

Tactic:
simp only [base_smul_def', prod, map_mul, mul_assoc]

Premises used: Monoid.PushoutI.NormalWord.prod, Monoid.PushoutI.NormalWord.base_smul_def', mul_assoc, 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) φ
⊢ Eq (α := PushoutI (G := G) φ) (prod (G := G) (d := d) (empty (G := G))) 1

Tactic:
simp [prod, empty]

Premises used: Monoid.PushoutI.NormalWord.prod, Monoid.PushoutI.NormalWord.empty
-- 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 : ι
g : G i
w : NormalWord (G := G) d
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))
⊢ Membership.mem (α := G i) (φ i).range ((φ i : (a : H) → G i) (w.head (G := G)) : G i)

Tactic:
simp