-- Mathlib/GroupTheory/PushoutI.lean
theorem ext_smul {w₁ w₂ : NormalWord d} (i : ι)
    (h : CoprodI.of (φ i w₁.head) • w₁.toWord =
         CoprodI.of (φ i w₂.head) • w₂.toWord) :
    w₁ = w₂

Proof state:
case mk.mk
ι : 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)
i : ι
h₁ : H
w₂ : Word G
h₂ : H
hw₂ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₂.toList → g ∈ d.set i
hw₁ :
  ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ (((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂).toList → g ∈ d.set i_1
⊢ { toWord := ((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂, head := h₁, normalized := hw₁ } =
    { toWord := w₂, head := h₂, normalized := hw₂ }

Tactic:
simp only [← map_inv, ← map_mul] at hw₁

Result:
case mk.mk
ι : 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)
i : ι
h₁ : H
w₂ : Word G
h₂ : H
hw₂ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₂.toList → g ∈ d.set i
hw₁✝ :
  ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ (((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂).toList → g ∈ d.set i_1
hw₁ : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ (CoprodI.of ((φ i) (h₁⁻¹ * h₂)) • w₂).toList → g ∈ d.set i_1
⊢ { toWord := ((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂, head := h₁, normalized := hw₁✝ } =
    { toWord := w₂, head := h₂, normalized := hw₂ }

Proof state:
case mk.mk
ι : 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)
i : ι
w₁ : Word G
h₁ : H
hw₁ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₁.toList → g ∈ d.set i
w₂ : Word G
h₂ : H
hw₂ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₂.toList → g ∈ d.set i
h : w₁ = ((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂
⊢ { toWord := w₁, head := h₁, normalized := hw₁ } = { toWord := w₂, head := h₂, normalized := hw₂ }

Tactic:
subst h

Result:
case mk.mk
ι : 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)
i : ι
h₁ : H
w₂ : Word G
h₂ : H
hw₂ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₂.toList → g ∈ d.set i
hw₁ :
  ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ (((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂).toList → g ∈ d.set i_1
⊢ { toWord := ((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂, head := h₁, normalized := hw₁ } =
    { toWord := w₂, head := h₂, normalized := hw₂ }

Proof state:
case mk
ι : 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₂ : NormalWord d
i : ι
w₁ : Word G
h₁ : H
hw₁ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₁.toList → g ∈ d.set i
h :
  CoprodI.of ((φ i) { toWord := w₁, head := h₁, normalized := hw₁ }.head) •
      { toWord := w₁, head := h₁, normalized := hw₁ }.toWord =
    CoprodI.of ((φ i) w₂.head) • w₂.toWord
⊢ { toWord := w₁, head := h₁, normalized := hw₁ } = w₂

Tactic:
rcases w₂ with ⟨w₂, h₂, hw₂⟩

Result:
case mk.mk
ι : 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)
i : ι
w₁ : Word G
h₁ : H
hw₁ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₁.toList → g ∈ d.set i
w₂ : Word G
h₂ : H
hw₂ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₂.toList → g ∈ d.set i
h :
  CoprodI.of ((φ i) { toWord := w₁, head := h₁, normalized := hw₁ }.head) •
      { toWord := w₁, head := h₁, normalized := hw₁ }.toWord =
    CoprodI.of ((φ i) { toWord := w₂, head := h₂, normalized := hw₂ }.head) •
      { toWord := w₂, head := h₂, normalized := hw₂ }.toWord
⊢ { toWord := w₁, head := h₁, normalized := hw₁ } = { toWord := w₂, head := h₂, normalized := hw₂ }

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₁ w₂ : NormalWord d
i : ι
h : CoprodI.of ((φ i) w₁.head) • w₁.toWord = CoprodI.of ((φ i) w₂.head) • w₂.toWord
⊢ w₁ = w₂

Tactic:
rcases w₁ with ⟨w₁, h₁, hw₁⟩

Result:
case mk
ι : 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₂ : NormalWord d
i : ι
w₁ : Word G
h₁ : H
hw₁ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₁.toList → g ∈ d.set i
h :
  CoprodI.of ((φ i) { toWord := w₁, head := h₁, normalized := hw₁ }.head) •
      { toWord := w₁, head := h₁, normalized := hw₁ }.toWord =
    CoprodI.of ((φ i) w₂.head) • w₂.toWord
⊢ { toWord := w₁, head := h₁, normalized := hw₁ } = w₂