-- Mathlib/GroupTheory/PushoutI.lean
theorem eq_one_of_smul_normalized (w : CoprodI.Word G) {i : ι} (h : H)
    (hw : ∀ i g, ⟨i, g⟩ ∈ w.toList → g ∈ d.set i)
    (hφw : ∀ j g, ⟨j, g⟩ ∈ (CoprodI.of (φ i h) • w).toList → g ∈ d.set j) :
    h = 1

Proof state:
case pos
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw✝ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
hep : ∀ (h : ¬w.toList = []), (w.toList.head h).fst ≠ i
hw : w.toList = []
⊢ ⟨i, (φ i) h * 1⟩ ∈ w.toList.tail ∨ w.toList.head? = some ⟨i, 1⟩ ∨ ¬w.fstIdx = some i ∧ 1 = 1

Tactic:
simp [hw, Word.fstIdx]

Result:
no goals

Proof state:
case refine_1
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
⊢ ⟨i, (φ i) h * ((Word.equivPair i) w).head⟩ ∈ (CoprodI.of ((φ i) h) • w).toList

Tactic:
simp only [Word.mem_smul_iff, not_true, false_and, ne_eq, Option.mem_def, mul_right_inj,
  exists_eq_right', mul_right_eq_self, exists_prop, true_and, false_or]

Result:
case refine_1
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
⊢ ¬(φ i) h * ((Word.equivPair i) w).head = 1 ∧
    (⟨i, (φ i) h * ((Word.equivPair i) w).head⟩ ∈ w.toList.tail ∨
      w.toList.head? = some ⟨i, ((Word.equivPair i) w).head⟩ ∨ ¬w.fstIdx = some i ∧ ((Word.equivPair i) w).head = 1)

Proof state:
case refine_1.left
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
⊢ ¬(φ i) h * ((Word.equivPair i) w).head = 1

Tactic:
intro h

Result:
case refine_1.left
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h✝ : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h✝) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h✝ = 1
h : (φ i) h✝ * ((Word.equivPair i) w).head = 1
⊢ False

Proof state:
case refine_1.left
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h✝ : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h✝) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h✝ = 1
h : (φ i) h✝ * ((Word.equivPair i) w).head = 1
⊢ False

Tactic:
apply_fun (d.compl i).equiv at h

Result:
case refine_1.left
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h✝ : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h✝) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h✝ = 1
h : ⋯.equiv ((φ i) h✝ * ((Word.equivPair i) w).head) = ⋯.equiv 1
⊢ False

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
⊢ ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head

Tactic:
rw [Word.equivPair_head]

Result:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
⊢ ↑(⋯.equiv (if h : ∃ (h : w.toList ≠ []), (w.toList.head h).fst = i then ⋯ ▸ (w.toList.head ⋯).snd else 1)).2 =
    if h : ∃ (h : w.toList ≠ []), (w.toList.head h).fst = i then ⋯ ▸ (w.toList.head ⋯).snd else 1

Proof state:
case refine_1.right
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
⊢ ⟨i, (φ i) h * ((Word.equivPair i) w).head⟩ ∈ w.toList.tail ∨
    w.toList.head? = some ⟨i, ((Word.equivPair i) w).head⟩ ∨ ¬w.fstIdx = some i ∧ ((Word.equivPair i) w).head = 1

Tactic:
rw [Word.equivPair_head]

Result:
case refine_1.right
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
⊢ ⟨i, (φ i) h * if h : ∃ (h : w.toList ≠ []), (w.toList.head h).fst = i then ⋯ ▸ (w.toList.head ⋯).snd else 1⟩ ∈
      w.toList.tail ∨
    w.toList.head? =
        some ⟨i, if h : ∃ (h : w.toList ≠ []), (w.toList.head h).fst = i then ⋯ ▸ (w.toList.head ⋯).snd else 1⟩ ∨
      ¬w.fstIdx = some i ∧
        (if h : ∃ (h : w.toList ≠ []), (w.toList.head h).fst = i then ⋯ ▸ (w.toList.head ⋯).snd else 1) = 1