-- Mathlib/GroupTheory/HNNExtension.lean
theorem unitsSMul_neg (u : ℤˣ) (w : NormalWord d) :
    unitsSMul φ (-u) (unitsSMul φ u w) = w

Proof state:
case neg.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)
      (if h : Cancels u (ofGroup g✝) then unitsSMulWithCancel φ u (ofGroup g✝) h
      else
        let g' := unitsSMulGroup φ d u (ofGroup g✝).head;
        cons (↑g'.1) u ((↑g'.2 * (ofGroup g✝).head⁻¹) • ofGroup g✝) ⋯ ⋯)
hcan2 : Cancels u (ofGroup g✝)
hcan : ¬Cancels (-u) (unitsSMulWithCancel φ u (ofGroup g✝) hcan2)
⊢ cons (↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u (ofGroup g✝) hcan2).head).1) (-u)
      ((↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u (ofGroup g✝) hcan2).head).2 *
          (unitsSMulWithCancel φ u (ofGroup g✝) hcan2).head⁻¹) •
        unitsSMulWithCancel φ u (ofGroup g✝) hcan2)
      ⋯ ⋯ =
    ofGroup g✝

Tactic:
simp [Cancels] at hcan2

Result:
no goals

Proof state:
case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan : ¬Cancels (-u) (unitsSMul φ u w)
⊢ (let g' := unitsSMulGroup φ d (-u) (unitsSMul φ u w).head;
    cons (↑g'.1) (-u) ((↑g'.2 * (unitsSMul φ u w).head⁻¹) • unitsSMul φ u w) ⋯ ⋯) =
    w

Tactic:
have hcan2 : Cancels u w := not_not.1 (mt (unitsSMul_cancels_iff _ _ _).2 hcan)

Result:
case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan : ¬Cancels (-u) (unitsSMul φ u w)
hcan2 : Cancels u w
⊢ (let g' := unitsSMulGroup φ d (-u) (unitsSMul φ u w).head;
    cons (↑g'.1) (-u) ((↑g'.2 * (unitsSMul φ u w).head⁻¹) • unitsSMul φ u w) ⋯ ⋯) =
    w

Proof state:
case neg.cons.refl.h2
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
g : G
w : NormalWord d
h1 : w.head ∈ d.set { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ }
h2 :
  ∀ u' ∈ Option.map Prod.fst w.toList.head?,
    w.head ∈ toSubgroup A B { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } →
      { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } = u'
hcan✝ :
  ¬Cancels (-u)
      (if h : Cancels u (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2) then
        unitsSMulWithCancel φ u (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2) h
      else
        let g' := unitsSMulGroup φ d u (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2).head;
        cons (↑g'.1) u
          ((↑g'.2 * (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2).head⁻¹) •
            cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2)
          ⋯ ⋯)
hcan2 : Cancels u (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2)
hcan :
  ¬Cancels (-u)
      (unitsSMulWithCancel φ u (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2) hcan2)
this : (⋯.equiv w.head).1 = 1
⊢ (-u,
        ↑(⋯.equiv (↑((toSubgroupEquiv φ u) ⟨g, ⋯⟩) * w.head)).2 * (w.head⁻¹ * (↑((toSubgroupEquiv φ u) ⟨g, ⋯⟩))⁻¹) *
          (↑((toSubgroupEquiv φ u) ⟨g, ⋯⟩) * w.head)) ::
      w.toList =
    ({ val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ }, w.head) :: w.toList

Tactic:
conv_lhs => erw [IsComplement.equiv_mul_left]

Result:
case neg.cons.refl.h2
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
g : G
w : NormalWord d
h1 : w.head ∈ d.set { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ }
h2 :
  ∀ u' ∈ Option.map Prod.fst w.toList.head?,
    w.head ∈ toSubgroup A B { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } →
      { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } = u'
hcan✝ :
  ¬Cancels (-u)
      (if h : Cancels u (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2) then
        unitsSMulWithCancel φ u (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2) h
      else
        let g' := unitsSMulGroup φ d u (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2).head;
        cons (↑g'.1) u
          ((↑g'.2 * (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2).head⁻¹) •
            cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2)
          ⋯ ⋯)
hcan2 : Cancels u (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2)
hcan :
  ¬Cancels (-u)
      (unitsSMulWithCancel φ u (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2) hcan2)
this : (⋯.equiv w.head).1 = 1
⊢ (-u,
        ↑((toSubgroupEquiv φ u) ⟨g, ⋯⟩ * (⋯.equiv w.head).1, (⋯.equiv w.head).2).2 *
            (w.head⁻¹ * (↑((toSubgroupEquiv φ u) ⟨g, ⋯⟩))⁻¹) *
          (↑((toSubgroupEquiv φ u) ⟨g, ⋯⟩) * w.head)) ::
      w.toList =
    ({ val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ }, w.head) :: w.toList

Proof state:
case neg.cons.refl.h1
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
g : G
w : NormalWord d
h1 : w.head ∈ d.set { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ }
h2 :
  ∀ u' ∈ Option.map Prod.fst w.toList.head?,
    w.head ∈ toSubgroup A B { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } →
      { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } = u'
hcan✝ :
  ¬Cancels (-u)
      (if h : Cancels u (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2) then
        unitsSMulWithCancel φ u (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2) h
      else
        let g' := unitsSMulGroup φ d u (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2).head;
        cons (↑g'.1) u
          ((↑g'.2 * (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2).head⁻¹) •
            cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2)
          ⋯ ⋯)
hcan2 : Cancels u (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2)
hcan :
  ¬Cancels (-u)
      (unitsSMulWithCancel φ u (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2) hcan2)
this : (⋯.equiv w.head).1 = 1
⊢ (cons (↑((toSubgroupEquiv φ (-u)) (⋯.equiv (↑((toSubgroupEquiv φ u) ⟨g, ⋯⟩) * w.head)).1)) (-u)
        ((↑(⋯.equiv (↑((toSubgroupEquiv φ u) ⟨g, ⋯⟩) * w.head)).2 * (w.head⁻¹ * (↑((toSubgroupEquiv φ u) ⟨g, ⋯⟩))⁻¹)) •
          ↑((toSubgroupEquiv φ u) ⟨g, ⋯⟩) • w)
        ⋯ ⋯).head =
    (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2).head

Tactic:
dsimp

Result:
case neg.cons.refl.h1
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
g : G
w : NormalWord d
h1 : w.head ∈ d.set { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ }
h2 :
  ∀ u' ∈ Option.map Prod.fst w.toList.head?,
    w.head ∈ toSubgroup A B { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } →
      { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } = u'
hcan✝ :
  ¬Cancels (-u)
      (if h : Cancels u (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2) then
        unitsSMulWithCancel φ u (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2) h
      else
        let g' := unitsSMulGroup φ d u (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2).head;
        cons (↑g'.1) u
          ((↑g'.2 * (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2).head⁻¹) •
            cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2)
          ⋯ ⋯)
hcan2 : Cancels u (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2)
hcan :
  ¬Cancels (-u)
      (unitsSMulWithCancel φ u (cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2) hcan2)
this : (⋯.equiv w.head).1 = 1
⊢ ↑((toSubgroupEquiv φ (-u)) (⋯.equiv (↑((toSubgroupEquiv φ u) ⟨g, ⋯⟩) * w.head)).1) = g