-- Mathlib/GroupTheory/HNNExtension.lean
theorem unitsSMul_one_group_smul (g : A) (w : NormalWord d) :
    unitsSMul φ 1 ((g : G) • w) = (φ g : G) • (unitsSMul φ 1 w)

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

Tactic:
simp [unitsSMulWithCancel, dif_pos (this.2 hcan), dif_pos hcan]

Result:
case pos
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
w : NormalWord d
this : Cancels 1 (↑g • w) ↔ Cancels 1 w
hcan : Cancels 1 w
⊢ consRecOn (motive := fun x => Cancels 1 x → NormalWord d) (↑g • w) (fun g_1 a => ↑g • w)
      (fun g x w x_1 x_2 x_3 can => ↑(φ ⟨g, ⋯⟩) • w) ⋯ =
    ↑(φ g) •
      consRecOn (motive := fun x => Cancels 1 x → NormalWord d) w (fun g a => w)
        (fun g x w x_1 x_2 x_3 can => ↑(φ ⟨g, ⋯⟩) • w) hcan

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

Tactic:
by_cases hcan : Cancels 1 w

Result:
case pos
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
w : NormalWord d
this : Cancels 1 (↑g • w) ↔ Cancels 1 w
hcan : Cancels 1 w
⊢ (if h : Cancels 1 (↑g • w) then unitsSMulWithCancel φ 1 (↑g • w) h
    else
      let g' := unitsSMulGroup φ d 1 (↑g • w).head;
      cons (↑g'.1) 1 ((↑g'.2 * (↑g • w).head⁻¹) • ↑g • w) ⋯ ⋯) =
    ↑(φ g) •
      if h : Cancels 1 w then unitsSMulWithCancel φ 1 w h
      else
        let g' := unitsSMulGroup φ d 1 w.head;
        cons (↑g'.1) 1 ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯

case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
w : NormalWord d
this : Cancels 1 (↑g • w) ↔ Cancels 1 w
hcan : ¬Cancels 1 w
⊢ (if h : Cancels 1 (↑g • w) then unitsSMulWithCancel φ 1 (↑g • w) h
    else
      let g' := unitsSMulGroup φ d 1 (↑g • w).head;
      cons (↑g'.1) 1 ((↑g'.2 * (↑g • w).head⁻¹) • ↑g • w) ⋯ ⋯) =
    ↑(φ g) •
      if h : Cancels 1 w then unitsSMulWithCancel φ 1 w h
      else
        let g' := unitsSMulGroup φ d 1 w.head;
        cons (↑g'.1) 1 ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯

Proof state:
case neg.e_g
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
w : NormalWord d
this : Cancels 1 (↑g • w) ↔ Cancels 1 w
hcan : ¬Cancels 1 w
⊢ ↑(φ (g * (⋯.equiv w.head).1, (⋯.equiv w.head).2).1) = ↑(φ g) * ↑(φ (⋯.equiv w.head).1)

Tactic:
simp_rw [toSubgroup_one]

Result:
case neg.e_g
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
w : NormalWord d
this : Cancels 1 (↑g • w) ↔ Cancels 1 w
hcan : ¬Cancels 1 w
⊢ ↑(φ (g * (⋯.equiv w.head).1)) = ↑(φ g) * ↑(φ (⋯.equiv w.head).1)

Proof state:
case pos.cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
g✝ : G
u✝ : ℤˣ
w✝ : NormalWord d
h1✝ : w✝.head ∈ d.set u✝
h2✝ : ∀ u' ∈ Option.map Prod.fst w✝.toList.head?, w✝.head ∈ toSubgroup A B u✝ → u✝ = u'
this : Cancels 1 (↑g • cons g✝ u✝ w✝ h1✝ h2✝) ↔ Cancels 1 (cons g✝ u✝ w✝ h1✝ h2✝)
hcan : Cancels 1 (cons g✝ u✝ w✝ h1✝ h2✝)
a✝ :
  cons g✝ u✝ w✝ h1✝ h2✝ = w✝ →
    consRecOn (motive := fun x => Cancels 1 x → NormalWord d) (↑g • cons g✝ u✝ w✝ h1✝ h2✝)
        (fun g_1 a => ↑g • cons g✝ u✝ w✝ h1✝ h2✝) (fun g x w x_1 x_2 x_3 can => ↑(φ ⟨g, ⋯⟩) • w) ⋯ =
      ↑(φ g) •
        consRecOn (motive := fun x => Cancels 1 x → NormalWord d) (cons g✝ u✝ w✝ h1✝ h2✝)
          (fun g a => cons g✝ u✝ w✝ h1✝ h2✝) (fun g x w x_1 x_2 x_3 can => ↑(φ ⟨g, ⋯⟩) • w) hcan
⊢ ↑(φ ⟨↑g * g✝, ⋯⟩) • w✝ = ↑(φ (g * ⟨g✝, ⋯⟩)) • w✝

Tactic:
rfl

Result:
no goals