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

Proof state:
case pos
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)
hncan : ¬Cancels u w
⊢ unitsSMulWithCancel φ (-u) (unitsSMul φ u w) hcan = w

Tactic:
unfold unitsSMul

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

Proof state:
case pos
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)
hncan : ¬Cancels u w
⊢ unitsSMulWithCancel φ (-u)
      (cons (↑(unitsSMulGroup φ d u w.head).1) u ((↑(unitsSMulGroup φ d u w.head).2 * w.head⁻¹) • w) ⋯ ⋯) ⋯ =
    w

Tactic:
simp [unitsSMulWithCancel, unitsSMulGroup, (d.compl u).equiv_snd_eq_inv_mul]

Result:
case pos
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)
hncan : ¬Cancels u w
⊢ ↑(⋯.equiv w.head).1 • (↑(⋯.equiv w.head).2 * w.head⁻¹) • w = w

Proof state:
case neg.cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
g : G
u' : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u'
h2 : ∀ u'_1 ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u' → u' = u'_1
hcan✝ :
  ¬Cancels (-u)
      (if h : Cancels u (cons g u' w h1 h2) then unitsSMulWithCancel φ u (cons g u' w h1 h2) h
      else
        let g' := unitsSMulGroup φ d u (cons g u' w h1 h2).head;
        cons (↑g'.1) u ((↑g'.2 * (cons g u' w h1 h2).head⁻¹) • cons g u' w h1 h2) ⋯ ⋯)
hcan2 : Cancels u (cons g u' w h1 h2)
hcan : ¬Cancels (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2)
⊢ 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)
      ⋯ ⋯ =
    cons g u' w h1 h2

Tactic:
cases hcan2.2

Result:
case neg.cons.refl
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)
⊢ 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)
      ⋯ ⋯ =
    cons g { val := -↑u, inv := -↑u⁻¹, val_inv := ⋯, inv_val := ⋯ } w h1 h2

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

Tactic:
split_ifs with hcan

Result:
case pos
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)
⊢ unitsSMulWithCancel φ (-u) (unitsSMul φ u w) hcan = w

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

Proof state:
case pos
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)
hncan : ¬Cancels u w
⊢ ↑(⋯.equiv w.head).1 • (↑(⋯.equiv w.head).2 * w.head⁻¹) • w = w

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

Result:
case pos
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)
hncan : ¬Cancels u w
⊢ ↑(⋯.equiv w.head).1 • ((↑(⋯.equiv w.head).1)⁻¹ * w.head * w.head⁻¹) • w = w

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

Tactic:
simp only [unitsSMulGroup, SetLike.coe_sort_coe, unitsSMulWithCancel, id_eq, consRecOn_cons,
  group_smul_head, IsComplement.equiv_mul_left, map_mul, Submonoid.coe_mul, coe_toSubmonoid,
  toSubgroupEquiv_neg_apply, mul_inv_rev]

Result:
case neg.cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
g : G
u' : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u'
h2 : ∀ u'_1 ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u' → u' = u'_1
hcan✝ :
  ¬Cancels (-u)
      (if h : Cancels u (cons g u' w h1 h2) then unitsSMulWithCancel φ u (cons g u' w h1 h2) h
      else
        let g' := unitsSMulGroup φ d u (cons g u' w h1 h2).head;
        cons (↑g'.1) u ((↑g'.2 * (cons g u' w h1 h2).head⁻¹) • cons g u' w h1 h2) ⋯ ⋯)
hcan2 : Cancels u (cons g u' w h1 h2)
hcan : ¬Cancels (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2)
⊢ 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)
      ⋯ ⋯ =
    cons g u' w h1 h2