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 : ι) → 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_1 : 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_1) : 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
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))
            1).2 :
      G i)
    1
have neg : (↑(Subtype.mk (p := fun (x : G i) ↦ x ∈ (↑(φ i).range : Set (G i))) 1 sorry,
          Subtype.mk (p := fun (x : G i) ↦ x ∈ d.set (G := G) i) 1 sorry).2 :
    G i) =
  1
Tactic: rw [equiv_one (d.compl i) (one_mem _) (d.one_mem _)]
-- 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) →
      (↑((⋯.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
⊢ h = 1
have hhead : 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))
            (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)
Tactic: have hhead : ((d.compl i).equiv (Word.equivPair i w).head).2 =
      (Word.equivPair i w).head := by
    rw [Word.equivPair_head]
    split_ifs with h
    · rcases h with ⟨_, rfl⟩
      exact hw _ _ (List.head_mem _)
    · rw [equiv_one (d.compl i) (one_mem _) (d.one_mem _)]
-- 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
hhead :
  Eq.{u_2 + 1} (α := G i)
    ((↑((⋯.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
                (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
              (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)).2 :
        G i) :
      G i)
    (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)
⊢ h = 1
have by_contra : ∀ (hh1 : ¬h = 1), False
Tactic: by_contra hh1
-- 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
hhead :
  Eq.{u_2 + 1} (α := G i)
    ((↑((⋯.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
                (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
              (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)).2 :
        G i) :
      G i)
    (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)
hh1 : ¬h = 1
⊢ False
have refine_2 : ∀
  (this :
    (↑((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) ((φ i : (a : H) → G i) h : G i)
                (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i))).2 :
        G i) =
      HMul.hMul (α := G i) (β := G i) ((φ i : (a : H) → G i) h : G i)
        (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)),
  False
Tactic: have := hφw i (φ i h * (Word.equivPair i w).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
hhead :
  Eq.{u_2 + 1} (α := G i)
    ((↑((⋯.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
                (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
              (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)).2 :
        G i) :
      G i)
    (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)
hh1 : ¬h = 1
refine_2 :
  ∀
    (this :
      (↑((⋯.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) ((φ i : (a : H) → G i) h : G i)
                  (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i))).2 :
          G i) =
        HMul.hMul (α := G i) (β := G i) ((φ i : (a : H) → G i) h : G i)
          (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)),
    False
⊢ False
have refine_1 : Sigma.mk (β := fun (i : ι) ↦ G i) i
    (HMul.hMul (α := G i) (β := G i) ((φ i : (a : H) → G i) h : G i)
      (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)) ∈
  (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)
Tactic: have := hφw i (φ i h * (Word.equivPair i w).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
hhead :
  Eq.{u_2 + 1} (α := G i)
    ((↑((⋯.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
                (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
              (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)).2 :
        G i) :
      G i)
    (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)
hh1 : ¬h = 1
this :
  (↑((⋯.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) ((φ i : (a : H) → G i) h : G i)
              (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i))).2 :
      G i) =
    HMul.hMul (α := G i) (β := G i) ((φ i : (a : H) → G i) h : G i)
      (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)
⊢ False
have refine_2 : h = 1
Tactic: apply hh1
-- 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) →
      (↑((⋯.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
                  (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
                g).2 :
          G i) =
        g
hφw :
  ∀ (j : ι) (g : G j),
    Sigma.mk (β := fun (i : ι) ↦ G i) j g ∈
        (HSMul.hSMul (α := CoprodI G)
              ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h) : CoprodI G) w).toList
          (M := G) →
      (↑((⋯.equiv (S := (↑(φ j).range : Set (G j))) (T := d.set (G := G) j) :
                  (a : G j) → (↑(↑(φ j).range : Set (G j)) : Type u_2) × (↑(d.set j) : Type u_2))
                g).2 :
          G j) =
        g
hhead :
  Eq.{u_2 + 1} (α := G i)
    ((↑((⋯.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
                (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
              (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)).2 :
        G i) :
      G i)
    (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)
hh1 : ¬h = 1
this :
  (↑((⋯.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) ((φ i : (a : H) → G i) h : G i)
              (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i))).2 :
      G i) =
    HMul.hMul (α := G i) (β := G i) ((φ i : (a : H) → G i) h : G i)
      (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)
⊢ h = 1
have this₁ : Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) =
  HMul.hMul (α := G i) (β := G i) ((φ i : (a : H) → G i) h : G i)
    (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)
Tactic: rw [equiv_mul_left_of_mem (d.compl i) ⟨_, rfl⟩, hhead] at this
Cleared hypotheses: this
-- 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
hhead :
  Eq.{u_2 + 1} (α := G i)
    ((↑((⋯.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
                (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
              (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)).2 :
        G i) :
      G i)
    (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)
hh1 : ¬h = 1
⊢ Sigma.mk (β := fun (i : ι) ↦ G i) i
      (HMul.hMul (α := G i) (β := G i) ((φ i : (a : H) → G i) h : G i)
        (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)) ∈
    (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)
have refine_1 : ¬HMul.hMul (α := G i) (β := G i) ((φ i : (a : H) → G i) h : G i)
        (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i) =
      1 ∧
  (Sigma.mk (β := fun (i : ι) ↦ G i) i
        (HMul.hMul (α := G i) (β := G i) ((φ i : (a : H) → G i) h : G i)
          (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)) ∈
      w.toList (M := G).tail ∨
    w.toList (M := G).head? =
        some
          (Sigma.mk (β := fun (i : ι) ↦ G i) i
            (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w))) ∨
      ¬w.fstIdx (M := G) = some i ∧
        Eq.{u_2 + 1} (α := G i)
          (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i) (1 : G i))
Tactic: simp only [Word.mem_smul_iff, not_true, false_and, ne_eq, Option.mem_def, mul_right_inj,
      exists_eq_right', mul_eq_left, exists_prop, true_and, false_or]
-- 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
hhead :
  Eq.{u_2 + 1} (α := G i)
    ((↑((⋯.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
                (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
              (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)).2 :
        G i) :
      G i)
    (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)
hh1 : ¬h = 1
⊢ ¬HMul.hMul (α := G i) (β := G i) ((φ i : (a : H) → G i) h : G i)
          (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i) =
        1 ∧
    (Sigma.mk (β := fun (i : ι) ↦ G i) i
          (HMul.hMul (α := G i) (β := G i) ((φ i : (a : H) → G i) h : G i)
            (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)) ∈
        w.toList (M := G).tail ∨
      w.toList (M := G).head? =
          some
            (Sigma.mk (β := fun (i : ι) ↦ G i) i
              (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w))) ∨
        ¬w.fstIdx (M := G) = some i ∧
          Eq.{u_2 + 1} (α := G i)
            (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i) (1 : G i))
have refine_1 : ¬HMul.hMul (α := G i) (β := G i) ((φ i : (a : H) → G i) h : G i)
      (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i) =
    1
Tactic: constructor
-- 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_1 : 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_1) : CoprodI G) w).toList
          (M := G) →
      (↑((⋯.equiv (S := (↑(φ j).range : Set (G j))) (T := d.set (G := G) j) :
                  (a : G j) → (↑(↑(φ j).range : Set (G j)) : Type u_2) × (↑(d.set j) : Type u_2))
                g).2 :
          G j) =
        g
hhead :
  Eq.{u_2 + 1} (α := G i)
    ((↑((⋯.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
                (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
              (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)).2 :
        G i) :
      G i)
    (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)
hh1 : ¬h_1 = 1
h :
  HMul.hMul (α := G i) (β := G i) ((φ i : (a : H) → G i) h_1 : G i)
      (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i) =
    1
⊢ False
have h₁ : Eq (α := (↑(↑(φ 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) ((φ i : (a : H) → G i) h_1 : G i)
        (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) w) : G i)) :
    (↑(↑(φ 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))
      1 :
    (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set (G := G) i) : Type u_2))
Tactic: apply_fun (d.compl i).equiv at h
Cleared hypotheses: h