-- 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:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
w : NormalWord d
⊢ (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:
have : Cancels 1 ((g : G) • w) ↔ Cancels 1 w := by
  simp [Cancels, Subgroup.mul_mem_cancel_left]

Result:
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) ⋯ ⋯

Proof state:
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

Tactic:
simp [Cancels] at hcan

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
g : ↥A
w : NormalWord d
this : Cancels 1 (↑g • w) ↔ Cancels 1 w
hcan : ¬Cancels 1 w
⊢ cons (↑(φ (⋯.equiv (↑g * w.head)).1)) 1 ((↑(⋯.equiv (↑g * w.head)).2 * w.head⁻¹) • w) ⋯ ⋯ =
    cons (↑(φ g) * ↑(φ (⋯.equiv w.head).1)) 1 ((↑(⋯.equiv w.head).2 * w.head⁻¹) • w) ⋯ ⋯

Tactic:
congr 1

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

case neg.e_w
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
⊢ (↑(⋯.equiv (↑g * w.head)).2 * w.head⁻¹) • w = (↑(⋯.equiv w.head).2 * w.head⁻¹) • w

Proof state:
case neg.e_w
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).2 * w.head⁻¹) • w = (↑(⋯.equiv w.head).2 * w.head⁻¹) • w

Tactic:
rfl

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
g : ↥A
w : NormalWord d
this : Cancels 1 (↑g • w) ↔ Cancels 1 w
hcan : ¬Cancels 1 w
⊢ (let g' := unitsSMulGroup φ d 1 (↑g • w).head;
    cons (↑g'.1) 1 ((↑g'.2 * (↑g • w).head⁻¹) • ↑g • w) ⋯ ⋯) =
    ↑(φ g) •
      let g' := unitsSMulGroup φ d 1 w.head;
      cons (↑g'.1) 1 ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯

Tactic:
simp [← mul_smul, mul_assoc, unitsSMulGroup]

Result:
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
⊢ cons (↑(φ (⋯.equiv (↑g * w.head)).1)) 1 ((↑(⋯.equiv (↑g * w.head)).2 * w.head⁻¹) • w) ⋯ ⋯ =
    cons (↑(φ g) * ↑(φ (⋯.equiv w.head).1)) 1 ((↑(⋯.equiv w.head).2 * w.head⁻¹) • 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
⊢ unitsSMul φ 1 (↑g • w) = ↑(φ g) • unitsSMul φ 1 w

Tactic:
unfold unitsSMul

Result:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
w : NormalWord d
⊢ (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
⊢ ↑(φ (⋯.equiv (↑g * w.head)).1) = ↑(φ g) * ↑(φ (⋯.equiv w.head).1)

Tactic:
conv_lhs => erw [IsComplement.equiv_mul_left]

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

Proof state:
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) ⋯ ⋯

Tactic:
rw [dif_neg (mt this.1 hcan), dif_neg hcan]

Result:
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
⊢ (let g' := unitsSMulGroup φ d 1 (↑g • w).head;
    cons (↑g'.1) 1 ((↑g'.2 * (↑g • w).head⁻¹) • ↑g • w) ⋯ ⋯) =
    ↑(φ g) •
      let g' := unitsSMulGroup φ d 1 w.head;
      cons (↑g'.1) 1 ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯

Proof state:
case neg.e_w
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
⊢ (↑(⋯.equiv (↑g * w.head)).2 * w.head⁻¹) • w = (↑(⋯.equiv w.head).2 * w.head⁻¹) • w

Tactic:
conv_lhs => erw [IsComplement.equiv_mul_left]

Result:
case neg.e_w
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).2 * w.head⁻¹) • w = (↑(⋯.equiv w.head).2 * w.head⁻¹) • w