-- Mathlib/GroupTheory/HNNExtension.lean
theorem prod_unitsSMul (u : ℤˣ) (w : NormalWord d) :
    (unitsSMul φ u w).prod φ = (t^(u : ℤ) * w.prod φ : HNNExtension G A B φ)

Proof state:
case neg.inl
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
hcan : ¬Cancels 1 w
⊢ of ↑(⋯.equiv w.head).1 * (of ↑(⋯.equiv w.head).2 * ((of w.head)⁻¹ * ReducedWord.prod φ w.toReducedWord)) =
    ReducedWord.prod φ w.toReducedWord

Tactic:
erw [(d.compl 1).equiv_snd_eq_inv_mul]

Result:
case neg.inl
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
hcan : ¬Cancels 1 w
⊢ of ↑(⋯.equiv w.head).1 *
      (of ((↑(⋯.equiv w.head).1)⁻¹ * w.head) * ((of w.head)⁻¹ * ReducedWord.prod φ w.toReducedWord)) =
    ReducedWord.prod φ w.toReducedWord

Proof state:
case pos.ofGroup
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
g✝ : G
hcan : Cancels u (ofGroup g✝)
⊢ ReducedWord.prod φ (unitsSMulWithCancel φ u (ofGroup g✝) hcan).toReducedWord =
    t ^ ↑u * ReducedWord.prod φ (ofGroup g✝).toReducedWord

Tactic:
simp [Cancels] at hcan

Result:
no goals

Proof state:
case pos.cons.refl.inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g✝ : G
w✝ : NormalWord d
h1✝ : w✝.head ∈ d.set { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ }
h2✝ :
  ∀ u' ∈ Option.map Prod.fst w✝.toList.head?,
    w✝.head ∈ toSubgroup A B { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } →
      { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } = u'
hcan : Cancels (-1) (cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝)
a✝ :
  cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝ = w✝ →
    ReducedWord.prod φ
        (unitsSMulWithCancel φ (-1) (cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝)
            hcan).toReducedWord =
      t ^ ↑(-1) *
        ReducedWord.prod φ
          (cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝).toReducedWord
⊢ of ↑((toSubgroupEquiv φ (-1)) ⟨g✝, ⋯⟩) * ReducedWord.prod φ w✝.toReducedWord =
    t ^ ↑(-1) * (of g✝ * ((t ^ ↑(-1))⁻¹ * ReducedWord.prod φ w✝.toReducedWord))

Tactic:
simp [equiv_symm_eq_conj, mul_assoc]

Result:
case pos.cons.refl.inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g✝ : G
w✝ : NormalWord d
h1✝ : w✝.head ∈ d.set { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ }
h2✝ :
  ∀ u' ∈ Option.map Prod.fst w✝.toList.head?,
    w✝.head ∈ toSubgroup A B { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } →
      { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } = u'
hcan : Cancels (-1) (cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝)
a✝ :
  cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝ = w✝ →
    ReducedWord.prod φ
        (unitsSMulWithCancel φ (-1) (cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝)
            hcan).toReducedWord =
      t ^ ↑(-1) *
        ReducedWord.prod φ
          (cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝).toReducedWord
⊢ of ↑(φ.symm ⟨g✝, ⋯⟩) * ReducedWord.prod φ w✝.toReducedWord = t⁻¹ * (of g✝ * (t * ReducedWord.prod φ w✝.toReducedWord))

Proof state:
case pos.cons.refl.inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g✝ : G
w✝ : NormalWord d
h1✝ : w✝.head ∈ d.set { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ }
h2✝ :
  ∀ u' ∈ Option.map Prod.fst w✝.toList.head?,
    w✝.head ∈ toSubgroup A B { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } →
      { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } = u'
hcan : Cancels (-1) (cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝)
a✝ :
  cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝ = w✝ →
    ReducedWord.prod φ
        (unitsSMulWithCancel φ (-1) (cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝)
            hcan).toReducedWord =
      t ^ ↑(-1) *
        ReducedWord.prod φ
          (cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝).toReducedWord
⊢ of ↑(φ.symm ⟨g✝, ⋯⟩) * ReducedWord.prod φ w✝.toReducedWord = t⁻¹ * (of g✝ * (t * ReducedWord.prod φ w✝.toReducedWord))

Tactic:
erw [equiv_symm_eq_conj]

Result:
case pos.cons.refl.inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g✝ : G
w✝ : NormalWord d
h1✝ : w✝.head ∈ d.set { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ }
h2✝ :
  ∀ u' ∈ Option.map Prod.fst w✝.toList.head?,
    w✝.head ∈ toSubgroup A B { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } →
      { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } = u'
hcan : Cancels (-1) (cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝)
a✝ :
  cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝ = w✝ →
    ReducedWord.prod φ
        (unitsSMulWithCancel φ (-1) (cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝)
            hcan).toReducedWord =
      t ^ ↑(-1) *
        ReducedWord.prod φ
          (cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝).toReducedWord
⊢ t⁻¹ * of ↑⟨g✝, ⋯⟩ * t * ReducedWord.prod φ w✝.toReducedWord =
    t⁻¹ * (of g✝ * (t * ReducedWord.prod φ w✝.toReducedWord))

Proof state:
case neg.inl
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
hcan : ¬Cancels 1 w
⊢ of ↑((toSubgroupEquiv φ 1) (⋯.equiv w.head).1) *
      (t ^ ↑1 * (of ↑(⋯.equiv w.head).2 * (of w.head)⁻¹ * ReducedWord.prod φ w.toReducedWord)) =
    t ^ ↑1 * ReducedWord.prod φ w.toReducedWord

Tactic:
simp [equiv_eq_conj, mul_assoc, (d.compl _).equiv_snd_eq_inv_mul]

Result:
case neg.inl
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
hcan : ¬Cancels 1 w
⊢ of ↑(⋯.equiv w.head).1 * (of ↑(⋯.equiv w.head).2 * ((of w.head)⁻¹ * ReducedWord.prod φ w.toReducedWord)) =
    ReducedWord.prod φ w.toReducedWord