awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
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
⊢ motive (↑x : (con φ).Quotient)
have H₁ : ∀ (g : CoprodI G), motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) g) : (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
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
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)
⊢ motive (↑x : (con φ).Quotient)
have H₂ : ∀ (h : H), motive (↑((inr : (a : H) → CoprodI G ∗ H) h) : (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
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
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)
⊢ motive (↑x : (con φ).Quotient)
have H₃ : ∀ (x y : CoprodI G ∗ H) (ihx : motive (↑x : (con φ).Quotient)) (ihy : motive (↑y : (con φ).Quotient)),
  motive (↑(x * y) : (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
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
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)
⊢ motive x
have H₁ : ∀ (x : CoprodI G ∗ H), motive (↑x : (con φ).Quotient)
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
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
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)
⊢ Nonempty (Transversal (G := G) φ)
have choose : ∀ (t : (i : ι) → Set (G i)) (ht : ∀ (i : ι), IsComplement (↑(φ i).range : Set (G i)) (t i) ∧ 1 ∈ t i),
  Nonempty (Transversal (G := G) φ)
Tactic: choose t ht using fun i => (φ i).range.exists_isComplement_right 1
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
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
⊢ Nonempty (Transversal (G := G) φ)
have val : Transversal (G := G) φ
Tactic: apply Nonempty.intro
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
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)
⊢ w₁ = w₂
have 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₂
Tactic: rcases w₁ with ⟨⟨_, _, _⟩, _, _⟩
Cleared hypotheses: w₁, hhead, hlist
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
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)
⊢ mk (G := G) (Word.mk (M := G) toList ne_one chain_ne) head normalized = w₂
have 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
Tactic: rcases w₂ with ⟨⟨_, _, _⟩, _, _⟩
Cleared hypotheses: w₂, hhead, hlist
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (hypothesis)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Group (G i)
inst_2 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
i_1 : ι
g_1 : G i_1
w : NormalWord (G := G) d
hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i_1
hgr : g_1 ∉ (φ i_1).range
n : (↑(↑(φ i_1).range : Set (G i_1)) : Type u_2) × (↑(d.set (G := G) i_1) : Type u_2) :=
  (⋯.equiv (S := (↑(φ i_1).range : Set (G i_1))) (T := d.set (G := G) i_1) :
      (a : G i_1) → (↑(↑(φ i_1).range : Set (G i_1)) : Type u_2) × (↑(d.set i_1) : Type u_2))
    (HMul.hMul (β := G i_1) g_1 ((φ i_1 : (a : H) → G i_1) (w.head (G := G)) : G i_1))
w' : Word G := Word.cons (M := G) (↑n.2 : G i_1) (w.toWord (G := G)) hmw ⋯
i : ι
g : G i
hg : Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w'.toList (M := G)
⊢ g ∈ d.set (G := G) i
have hg₁ : i = i_1 ∧ g ≍ (↑n.2 : G i_1) ∨ Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toWord (G := G).toList (M := G)
Tactic: simp only [w', Word.cons, mem_cons, Sigma.mk.inj_iff] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Group (G i)
inst_2 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
i_1 : ι
g_1 : G i_1
w : NormalWord (G := G) d
hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i_1
hgr : g_1 ∉ (φ i_1).range
n : (↑(↑(φ i_1).range : Set (G i_1)) : Type u_2) × (↑(d.set (G := G) i_1) : Type u_2) :=
  (⋯.equiv (S := (↑(φ i_1).range : Set (G i_1))) (T := d.set (G := G) i_1) :
      (a : G i_1) → (↑(↑(φ i_1).range : Set (G i_1)) : Type u_2) × (↑(d.set i_1) : Type u_2))
    (HMul.hMul (β := G i_1) g_1 ((φ i_1 : (a : H) → G i_1) (w.head (G := G)) : G i_1))
w' : Word G := Word.cons (M := G) (↑n.2 : G i_1) (w.toWord (G := G)) hmw ⋯
i : ι
g : G i
hg : i = i_1 ∧ g ≍ (↑n.2 : G i_1) ∨ Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toWord (G := G).toList (M := G)
⊢ g ∈ d.set (G := G) i
have inl : ∀ (g : G i) (hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i) (hgr : g ∉ (φ i).range),
  let n : (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set (G := G) i) : Type u_2) :=
    (sorry.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
        (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
      (HMul.hMul (β := G i) g ((φ i : (a : H) → G i) (w.head (G := G)) : G i));
  ∀ {β : Type u_2}, (↑n.2 : G i) ∈ d.set (G := G) i
Tactic: rcases hg with ⟨rfl, hg | hg⟩
Cleared hypotheses: i_1, g_1, hmw, hgr, n, w', g, hg
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Group (G i)
inst_2 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
i_1 : ι
g_1 : G i_1
w : NormalWord (G := G) d
hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i_1
hgr : g_1 ∉ (φ i_1).range
n : (↑(↑(φ i_1).range : Set (G i_1)) : Type u_2) × (↑(d.set (G := G) i_1) : Type u_2) :=
  (⋯.equiv (S := (↑(φ i_1).range : Set (G i_1))) (T := d.set (G := G) i_1) :
      (a : G i_1) → (↑(↑(φ i_1).range : Set (G i_1)) : Type u_2) × (↑(d.set i_1) : Type u_2))
    (HMul.hMul (β := G i_1) g_1 ((φ i_1 : (a : H) → G i_1) (w.head (G := G)) : G i_1))
w' : Word G := Word.cons (M := G) (↑n.2 : G i_1) (w.toWord (G := G)) hmw ⋯
i : ι
g : G i
hg : i = i_1 ∧ g ≍ (↑n.2 : G i_1) ∨ Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toWord (G := G).toList (M := G)
inl :
  ∀ (g : G i) (hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i) (hgr : g ∉ (φ i).range),
    let n : (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set (G := G) i) : Type u_2) :=
      (⋯.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
          (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
        (HMul.hMul (β := G i) g ((φ i : (a : H) → G i) (w.head (G := G)) : G i));
    ∀ {β : Type u_2}, (↑n.2 : G i) ∈ d.set (G := G) i
⊢ g ∈ d.set (G := G) i
have inr : Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toWord (G := G).toList (M := G) → g ∈ d.set (G := G) i
Tactic: rcases hg with ⟨rfl, hg | hg⟩
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (hypothesis)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toList (M := G) → g ∈ d.set (G := G) i
hφw :
  ∀ (j : ι) (g : G j),
    Sigma.mk (β := fun (i : ι) ↦ G i) j g ∈
        (HSMul.hSMul (α := CoprodI G)
              ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h) : CoprodI G) w).toList
          (M := G) →
      g ∈ d.set (G := G) j
⊢ h = 1
have hw₁ : ∀ (i : ι) (g : G i),
  Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toList (M := G) →
    (↑((sorry.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
                (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
              g).2 :
        G i) =
      g
Tactic: simp only [← (d.compl _).equiv_snd_eq_self_iff_mem (one_mem _)] at hw hφw
Cleared hypotheses: hw, hφw
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (hypothesis)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toList (M := G) → g ∈ d.set (G := G) i
hφw :
  ∀ (j : ι) (g : G j),
    Sigma.mk (β := fun (i : ι) ↦ G i) j g ∈
        (HSMul.hSMul (α := CoprodI G)
              ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h) : CoprodI G) w).toList
          (M := G) →
      g ∈ d.set (G := G) j
hw₁ :
  ∀ (i : ι) (g : G i),
    Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toList (M := G) →
      (↑((⋯.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
                  (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
                g).2 :
          G i) =
        g
⊢ h = 1
have 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) →
    (↑((sorry.equiv (S := (↑(φ j).range : Set (G j))) (T := d.set (G := G) j) :
                (a : G j) → (↑(↑(φ j).range : Set (G j)) : Type u_2) × (↑(d.set j) : Type u_2))
              g).2 :
        G j) =
      g
Tactic: simp only [← (d.compl _).equiv_snd_eq_self_iff_mem (one_mem _)] at hw hφw
Cleared hypotheses: hw, hφw
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw :
  ∀ (i : ι) (g : G i),
    Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toList (M := G) →
      (↑((⋯.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
                  (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
                g).2 :
          G i) =
        g
hφw :
  ∀ (j : ι) (g : G j),
    Sigma.mk (β := fun (i : ι) ↦ G i) j g ∈
        (HSMul.hSMul (α := CoprodI G)
              ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h) : CoprodI G) w).toList
          (M := G) →
      (↑((⋯.equiv (S := (↑(φ j).range : Set (G j))) (T := d.set (G := G) j) :
                  (a : G j) → (↑(↑(φ j).range : Set (G j)) : Type u_2) × (↑(d.set j) : Type u_2))
                g).2 :
          G j) =
        g
⊢ Eq.{u_2 + 1} (α := G i)
    ((↑((⋯.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
                (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
              (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)).2 :
        G i) :
      G i)
    (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)
have rw : Eq.{u_2 + 1} (α := G i)
  (↑((sorry.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
            (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
          (if h : ∃ (h : w.toList (M := G) ≠ []), (w.toList (M := G).head h).fst (β := fun (i : ι) ↦ G i) = i then
            Eq.rec (motive := fun (x : ι) (h : (w.toList (M := G).head sorry).fst (β := fun (i : ι) ↦ G i) = x) ↦ G x)
              ((w.toList (M := G).head sorry).snd (β := fun (i : ι) ↦ G i)) sorry
          else 1)).2 :
    G i)
  (if h : ∃ (h : w.toList (M := G) ≠ []), (w.toList (M := G).head h).fst (β := fun (i : ι) ↦ G i) = i then
    Eq.rec (motive := fun (x : ι) (h : (w.toList (M := G).head sorry).fst (β := fun (i : ι) ↦ G i) = x) ↦ G x)
      ((w.toList (M := G).head sorry).snd (β := fun (i : ι) ↦ G i)) sorry
  else 1)
Tactic: rw [Word.equivPair_head]
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw :
  ∀ (i : ι) (g : G i),
    Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toList (M := G) →
      (↑((⋯.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
                  (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
                g).2 :
          G i) =
        g
hφw :
  ∀ (j : ι) (g : G j),
    Sigma.mk (β := fun (i : ι) ↦ G i) j g ∈
        (HSMul.hSMul (α := CoprodI G)
              ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h) : CoprodI G) w).toList
          (M := G) →
      (↑((⋯.equiv (S := (↑(φ j).range : Set (G j))) (T := d.set (G := G) j) :
                  (a : G j) → (↑(↑(φ j).range : Set (G j)) : Type u_2) × (↑(d.set j) : Type u_2))
                g).2 :
          G j) =
        g
⊢ Eq.{u_2 + 1} (α := G i)
    (↑((⋯.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
              (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
            (if h : ∃ (h : w.toList (M := G) ≠ []), (w.toList (M := G).head h).fst (β := fun (i : ι) ↦ G i) = i then
              Eq.rec (motive := fun (x : ι) (h : (w.toList (M := G).head ⋯).fst (β := fun (i : ι) ↦ G i) = x) ↦ G x)
                ((w.toList (M := G).head ⋯).snd (β := fun (i : ι) ↦ G i)) ⋯
            else 1)).2 :
      G i)
    (if h : ∃ (h : w.toList (M := G) ≠ []), (w.toList (M := G).head h).fst (β := fun (i : ι) ↦ G i) = i then
      Eq.rec (motive := fun (x : ι) (h : (w.toList (M := G).head ⋯).fst (β := fun (i : ι) ↦ G i) = x) ↦ G x)
        ((w.toList (M := G).head ⋯).snd (β := fun (i : ι) ↦ G i)) ⋯
    else 1)
have pos : ∀ (h : ∃ (h : w.toList (M := G) ≠ []), (w.toList (M := G).head h).fst (β := fun (i : ι) ↦ G i) = i),
  Eq.{u_2 + 1} (α := G i)
    ((↑((sorry.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
                (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
              (Eq.rec (motive := fun (x : ι) (h : (w.toList (M := G).head sorry).fst (β := fun (i : ι) ↦ G i) = x) ↦ G x)
                  ((w.toList (M := G).head sorry).snd (β := fun (i : ι) ↦ G i)) sorry :
                G i)).2 :
        G i) :
      G i)
    (Eq.rec (motive := fun (x : ι) (h : (w.toList (M := G).head sorry).fst (β := fun (i : ι) ↦ G i) = x) ↦ G x)
        ((w.toList (M := G).head sorry).snd (β := fun (i : ι) ↦ G i)) sorry :
      G i)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw :
  ∀ (i : ι) (g : G i),
    Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toList (M := G) →
      (↑((⋯.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
                  (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
                g).2 :
          G i) =
        g
hφw :
  ∀ (j : ι) (g : G j),
    Sigma.mk (β := fun (i : ι) ↦ G i) j g ∈
        (HSMul.hSMul (α := CoprodI G)
              ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h) : CoprodI G) w).toList
          (M := G) →
      (↑((⋯.equiv (S := (↑(φ j).range : Set (G j))) (T := d.set (G := G) j) :
                  (a : G j) → (↑(↑(φ j).range : Set (G j)) : Type u_2) × (↑(d.set j) : Type u_2))
                g).2 :
          G j) =
        g
pos :
  ∀ (h : ∃ (h : w.toList (M := G) ≠ []), (w.toList (M := G).head h).fst (β := fun (i : ι) ↦ G i) = i),
    Eq.{u_2 + 1} (α := G i)
      ((↑((⋯.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
                  (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
                (Eq.rec (motive := fun (x : ι) (h : (w.toList (M := G).head ⋯).fst (β := fun (i : ι) ↦ G i) = x) ↦ G x)
                    ((w.toList (M := G).head ⋯).snd (β := fun (i : ι) ↦ G i)) ⋯ :
                  G i)).2 :
          G i) :
        G i)
      (Eq.rec (motive := fun (x : ι) (h : (w.toList (M := G).head ⋯).fst (β := fun (i : ι) ↦ G i) = x) ↦ G x)
          ((w.toList (M := G).head ⋯).snd (β := fun (i : ι) ↦ G i)) ⋯ :
        G i)
⊢ Eq.{u_2 + 1} (α := G i)
    (↑((⋯.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
              (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
            (if h : ∃ (h : w.toList (M := G) ≠ []), (w.toList (M := G).head h).fst (β := fun (i : ι) ↦ G i) = i then
              Eq.rec (motive := fun (x : ι) (h : (w.toList (M := G).head ⋯).fst (β := fun (i : ι) ↦ G i) = x) ↦ G x)
                ((w.toList (M := G).head ⋯).snd (β := fun (i : ι) ↦ G i)) ⋯
            else 1)).2 :
      G i)
    (if h : ∃ (h : w.toList (M := G) ≠ []), (w.toList (M := G).head h).fst (β := fun (i : ι) ↦ G i) = i then
      Eq.rec (motive := fun (x : ι) (h : (w.toList (M := G).head ⋯).fst (β := fun (i : ι) ↦ G i) = x) ↦ G x)
        ((w.toList (M := G).head ⋯).snd (β := fun (i : ι) ↦ G i)) ⋯
    else 1)
have neg : ∀ (h : ¬∃ (h : w.toList (M := G) ≠ []), (w.toList (M := G).head h).fst (β := fun (i : ι) ↦ G i) = i),
  Eq.{u_2 + 1} (α := G i)
    (↑((sorry.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
              (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
            1).2 :
      G i)
    1
Tactic: split_ifs with h