-- 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
⊢ 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

Tactic:
cases w using consRecOn

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

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
⊢ 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

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)) = ↑(φ g) * ↑(φ (⋯.equiv w.head).1)

Tactic:
simp only [SetLike.coe_sort_coe, map_mul, Subgroup.coe_mul]

Result:
no goals

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
⊢ 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

Tactic:
simp only [smul_cons, consRecOn_cons, mul_smul]

Result:
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✝

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
⊢ Cancels 1 (↑g • w) ↔ Cancels 1 w

Tactic:
simp [Cancels, Subgroup.mul_mem_cancel_left]

Result:
no goals

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:
rw [← mul_smul, ← Subgroup.coe_mul, ← map_mul φ]

Result:
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✝