awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst_1 : Group H
M : Type u_3
inst_2 : Monoid M
d : TransversalPair G A B
a : ↥A
x : NormalWord d
⊢ Eq (α := NormalWord d)
    ((HMul.hMul (α := Equiv.Perm (NormalWord d)) (β := Equiv.Perm (NormalWord d)) (unitsSMulEquiv φ)
            ((MulAction.toPermHom G (NormalWord d) : (a : G) → Equiv.Perm (NormalWord d)) (↑a : G) :
              Equiv.Perm (NormalWord d)) :
          (a : NormalWord d) → NormalWord d)
        x :
      NormalWord d)
    ((HMul.hMul (α := Equiv.Perm (NormalWord d)) (β := Equiv.Perm (NormalWord d))
            ((MulAction.toPermHom G (NormalWord d) : (a : G) → Equiv.Perm (NormalWord d))
                (↑((φ : (a : ↥A) → ↥B) a) : G) :
              Equiv.Perm (NormalWord d))
            (unitsSMulEquiv φ) :
          (a : NormalWord d) → NormalWord d)
        x :
      NormalWord d)

Tactic:
simp [unitsSMul_one_group_smul]

Premises used: HNNExtension.NormalWord.unitsSMul_one_group_smul
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
w : NormalWord d
⊢ ReducedWord.prod φ (g • w).toReducedWord =
    HMul.hMul (α := HNNExtension G A B φ) ((of : (a : G) → HNNExtension G A B φ) g : HNNExtension G A B φ)
      (ReducedWord.prod φ w.toReducedWord)

Tactic:
simp [ReducedWord.prod, mul_assoc]

Premises used: mul_assoc, HNNExtension.NormalWord.ReducedWord.prod
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
w : NormalWord d
⊢ HSMul.hSMul (α := HNNExtension G A B φ) ((of : (a : G) → HNNExtension G A B φ) g : HNNExtension G A B φ) w = g • w

Tactic:
simp +instances [instHSMul, SMul.smul, MulAction.toEndHom]

Premises used: instHSMul, MulAction.toEndHom, SMul.smul
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
⊢ HSMul.hSMul (α := HNNExtension G A B φ) t w = unitsSMul φ 1 w

Tactic:
simp +instances [instHSMul, SMul.smul, MulAction.toEndHom]

Premises used: instHSMul, MulAction.toEndHom, SMul.smul
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
inl : HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑1 : ℤ) • w = unitsSMul φ 1 w
inr : HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑(-1) : ℤ) • w = unitsSMul φ (-1) w
⊢ HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) • w = unitsSMul φ u w

Tactic:
rcases Int.units_eq_one_or u with (rfl | rfl)

Premises used: Int.units_eq_one_or, rfl
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
⊢ HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑1 : ℤ) • w = unitsSMul φ 1 w

Tactic:
simp +instances [instHSMul, SMul.smul, MulAction.toEndHom, Equiv.Perm.inv_def]

Premises used: instHSMul, MulAction.toEndHom, Equiv.Perm.inv_def, SMul.smul
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
⊢ HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑(-1) : ℤ) • w = unitsSMul φ (-1) w

Tactic:
simp +instances [instHSMul, SMul.smul, MulAction.toEndHom, Equiv.Perm.inv_def]

Premises used: instHSMul, MulAction.toEndHom, Equiv.Perm.inv_def, SMul.smul
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
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'
⊢ ReducedWord.prod φ (cons g u w h1 h2).toReducedWord =
    HMul.hMul (α := HNNExtension G A B φ) ((of : (a : G) → HNNExtension G A B φ) g : HNNExtension G A B φ)
      (HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ w.toReducedWord)

Tactic:
simp [ReducedWord.prod, cons, mul_assoc]

Premises used: mul_assoc, HNNExtension.NormalWord.ReducedWord.prod, HNNExtension.NormalWord.cons
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
pos :
  ∀ (hcan : Cancels u w),
    ReducedWord.prod φ (unitsSMulWithCancel φ u w hcan).toReducedWord =
      HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ w.toReducedWord
neg :
  ∀ (hcan : ¬Cancels u w),
    ReducedWord.prod φ
        (toReducedWord (d := d)
          (let g' := unitsSMulGroup φ d u w.head;
          cons (↑g'.1 : G) u (((↑g'.2 : G) * w.head⁻¹) • w) ⋯ ⋯)) =
      HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ w.toReducedWord
⊢ ReducedWord.prod φ
      (toReducedWord (d := d)
        (if h : Cancels u w then unitsSMulWithCancel φ u w h
        else
          let g' := unitsSMulGroup φ d u w.head;
          cons (↑g'.1 : G) u (((↑g'.2 : G) * w.head⁻¹) • w) ⋯ ⋯)) =
    HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ w.toReducedWord

Tactic:
split_ifs with hcan
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
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 w
pos :
  ∀ (g : G) (hcan : Cancels (A := A) (B := B) (d := d) u (ofGroup g)),
    ReducedWord.prod φ (unitsSMulWithCancel φ u (ofGroup g) hcan).toReducedWord =
      HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ (toReducedWord (d := d) (ofGroup g))
pos₁ :
  ∀ (g : G) (u_1 : ℤˣ) (w : NormalWord d) (h1 : w.head ∈ d.set u_1)
    (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u_1 → u_1 = u')
    (hcan : Cancels u (cons g u_1 w h1 h2)),
    (∀ (h : cons g u_1 w h1 h2 = w),
        ReducedWord.prod φ (unitsSMulWithCancel φ u (cons g u_1 w h1 h2) hcan).toReducedWord =
          HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ (cons g u_1 w h1 h2).toReducedWord) →
      ReducedWord.prod φ (unitsSMulWithCancel φ u (cons g u_1 w h1 h2) hcan).toReducedWord =
        HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ (cons g u_1 w h1 h2).toReducedWord
⊢ ReducedWord.prod φ (unitsSMulWithCancel φ u w hcan).toReducedWord =
    HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ w.toReducedWord

Tactic:
cases w using consRecOn
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
g : G
hcan : Cancels (A := A) (B := B) (d := d) u (ofGroup g)
⊢ ReducedWord.prod φ (unitsSMulWithCancel φ u (ofGroup g) hcan).toReducedWord =
    HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ (toReducedWord (d := d) (ofGroup g))

Tactic:
simp [Cancels] at hcan

Premises used: HNNExtension.NormalWord.Cancels
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
g : G
u_1 : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u_1
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u_1 → u_1 = u'
hcan : Cancels u (cons g u_1 w h1 h2)
h :
  ∀ (h : cons g u_1 w h1 h2 = w),
    ReducedWord.prod φ (unitsSMulWithCancel φ u (cons g u_1 w h1 h2) hcan).toReducedWord =
      HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ (cons g u_1 w h1 h2).toReducedWord
pos :
  ∀ (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 (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2)),
    (∀ (h : cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2 = w),
        ReducedWord.prod φ
            (unitsSMulWithCancel φ u
                (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2)
                hcan).toReducedWord =
          HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) *
            ReducedWord.prod φ
              (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1
                  h2).toReducedWord) →
      ReducedWord.prod φ
          (unitsSMulWithCancel φ u
              (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2)
              hcan).toReducedWord =
        HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) *
          ReducedWord.prod φ
            (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2).toReducedWord
⊢ ReducedWord.prod φ (unitsSMulWithCancel φ u (cons g u_1 w h1 h2) hcan).toReducedWord =
    HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ (cons g u_1 w h1 h2).toReducedWord

Tactic:
cases hcan.2

Premises used: And.right
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
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 (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2)
h :
  ∀ (h : cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2 = w),
    ReducedWord.prod φ
        (unitsSMulWithCancel φ u
            (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2)
            hcan).toReducedWord =
      HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) *
        ReducedWord.prod φ
          (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2).toReducedWord
pos :
  (of : (a : G) → HNNExtension G A B φ)
        (↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
              (Subtype.mk (p := fun (x : G) ↦ x ∈ toSubgroup A B u) g ⋯)) :
          G) *
      ReducedWord.prod φ w.toReducedWord =
    HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) *
      HMul.hMul (α := HNNExtension G A B φ) ((of : (a : G) → HNNExtension G A B φ) g : HNNExtension G A B φ)
        ((HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ))⁻¹ * ReducedWord.prod φ w.toReducedWord)
⊢ ReducedWord.prod φ
      (unitsSMulWithCancel φ u
          (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2)
          hcan).toReducedWord =
    HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) *
      ReducedWord.prod φ
        (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2).toReducedWord

Tactic:
simp only [unitsSMulWithCancel, id_eq, consRecOn_cons, prod_group_smul, prod_cons, zpow_neg]

Premises used: HNNExtension.NormalWord.prod_group_smul, HNNExtension.NormalWord.prod_cons, HNNExtension.NormalWord.consRecOn_cons, zpow_neg, HNNExtension.NormalWord.unitsSMulWithCancel, id_eq
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
w : NormalWord d
h1 : w.head ∈ d.set { val := -(↑1 : ℤ), inv := -(↑1⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ }
h2 :
  ∀ u' ∈ Option.map Prod.fst w.toList.head?,
    w.head ∈ toSubgroup A B { val := -(↑1 : ℤ), inv := -(↑1⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } →
      { val := -(↑1 : ℤ), inv := -(↑1⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ } = u'
hcan : Cancels 1 (cons g { val := -(↑1 : ℤ), inv := -(↑1⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2)
h :
  ∀ (h : cons g { val := -(↑1 : ℤ), inv := -(↑1⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2 = w),
    ReducedWord.prod φ
        (unitsSMulWithCancel φ 1
            (cons g { val := -(↑1 : ℤ), inv := -(↑1⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2)
            hcan).toReducedWord =
      HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑1 : ℤ) *
        ReducedWord.prod φ
          (cons g { val := -(↑1 : ℤ), inv := -(↑1⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2).toReducedWord
⊢ (of : (a : G) → HNNExtension G A B φ)
        (↑((toSubgroupEquiv φ 1 : (a : ↥(toSubgroup A B 1)) → ↥(toSubgroup A B (-1)))
              (Subtype.mk (p := fun (x : G) ↦ x ∈ toSubgroup A B 1) g ⋯)) :
          G) *
      ReducedWord.prod φ w.toReducedWord =
    HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑1 : ℤ) *
      HMul.hMul (α := HNNExtension G A B φ) ((of : (a : G) → HNNExtension G A B φ) g : HNNExtension G A B φ)
        ((HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑1 : ℤ))⁻¹ * ReducedWord.prod φ w.toReducedWord)

Tactic:
simp [equiv_eq_conj, mul_assoc]

Premises used: HNNExtension.equiv_eq_conj, mul_assoc
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
w : NormalWord d
h1 : w.head ∈ d.set { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ }
h2 :
  ∀ u' ∈ Option.map Prod.fst w.toList.head?,
    w.head ∈ toSubgroup A B { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } →
      { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ } = u'
hcan : Cancels (-1) (cons g { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2)
h :
  ∀ (h : cons g { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2 = w),
    ReducedWord.prod φ
        (unitsSMulWithCancel φ (-1)
            (cons g { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2)
            hcan).toReducedWord =
      HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑(-1) : ℤ) *
        ReducedWord.prod φ
          (cons g { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2).toReducedWord
pos :
  (of : (a : G) → HNNExtension G A B φ)
        (↑((φ.symm : (a : ↥B) → ↥(toSubgroup A B (- -1))) (Subtype.mk (p := fun (x : G) ↦ x ∈ B) g ⋯)) : G) *
      ReducedWord.prod φ w.toReducedWord =
    t⁻¹ *
      HMul.hMul (α := HNNExtension G A B φ) ((of : (a : G) → HNNExtension G A B φ) g : HNNExtension G A B φ)
        (t * ReducedWord.prod φ w.toReducedWord)
⊢ (of : (a : G) → HNNExtension G A B φ)
        (↑((toSubgroupEquiv φ (-1) : (a : ↥(toSubgroup A B (-1))) → ↥(toSubgroup A B (- -1)))
              (Subtype.mk (p := fun (x : G) ↦ x ∈ toSubgroup A B (-1)) g ⋯)) :
          G) *
      ReducedWord.prod φ w.toReducedWord =
    HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑(-1) : ℤ) *
      HMul.hMul (α := HNNExtension G A B φ) ((of : (a : G) → HNNExtension G A B φ) g : HNNExtension G A B φ)
        ((HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑(-1) : ℤ))⁻¹ * ReducedWord.prod φ w.toReducedWord)

Tactic:
simp only [toSubgroup_neg_one, toSubgroupEquiv_neg_one, Units.val_neg, Units.val_one,
          Int.reduceNeg, zpow_neg, zpow_one, inv_inv]

Premises used: HNNExtension.toSubgroup_neg_one, HNNExtension.toSubgroupEquiv_neg_one, Int.reduceNeg, zpow_one, Units.val_neg, inv_inv, zpow_neg, Units.val_one
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
w : NormalWord d
h1 : w.head ∈ d.set { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ }
h2 :
  ∀ u' ∈ Option.map Prod.fst w.toList.head?,
    w.head ∈ toSubgroup A B { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } →
      { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ } = u'
hcan : Cancels (-1) (cons g { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2)
h :
  ∀ (h : cons g { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2 = w),
    ReducedWord.prod φ
        (unitsSMulWithCancel φ (-1)
            (cons g { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2)
            hcan).toReducedWord =
      HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑(-1) : ℤ) *
        ReducedWord.prod φ
          (cons g { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2).toReducedWord
pos :
  HMul.hMul (α := HNNExtension G A B φ) (β := HNNExtension G A B φ) t⁻¹
          ((of : (a : G) → HNNExtension G A B φ) (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ B) g ⋯) : G) :
            HNNExtension G A B φ) *
        t *
      ReducedWord.prod φ w.toReducedWord =
    t⁻¹ *
      HMul.hMul (α := HNNExtension G A B φ) ((of : (a : G) → HNNExtension G A B φ) g : HNNExtension G A B φ)
        (t * ReducedWord.prod φ w.toReducedWord)
pos₁ :
  HMul.hMul (α := HNNExtension G A B φ) (β := HNNExtension G A B φ) t⁻¹
        ((of : (a : G) → HNNExtension G A B φ) (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ B) g ⋯) : G) :
          HNNExtension G A B φ) *
      (t * ReducedWord.prod φ w.toReducedWord) =
    t⁻¹ *
      HMul.hMul (α := HNNExtension G A B φ) ((of : (a : G) → HNNExtension G A B φ) g : HNNExtension G A B φ)
        (t * ReducedWord.prod φ w.toReducedWord)
pos₂ pos₃ :
  t⁻¹ *
      HMul.hMul (α := HNNExtension G A B φ)
        ((of : (a : G) → HNNExtension G A B φ) (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ B) g ⋯) : G) :
          HNNExtension G A B φ)
        (t * ReducedWord.prod φ w.toReducedWord) =
    t⁻¹ *
      HMul.hMul (α := HNNExtension G A B φ) ((of : (a : G) → HNNExtension G A B φ) g : HNNExtension G A B φ)
        (t * ReducedWord.prod φ w.toReducedWord)
⊢ (of : (a : G) → HNNExtension G A B φ)
        (↑((φ.symm : (a : ↥B) → ↥(toSubgroup A B (- -1))) (Subtype.mk (p := fun (x : G) ↦ x ∈ B) g ⋯)) : G) *
      ReducedWord.prod φ w.toReducedWord =
    t⁻¹ *
      HMul.hMul (α := HNNExtension G A B φ) ((of : (a : G) → HNNExtension G A B φ) g : HNNExtension G A B φ)
        (t * ReducedWord.prod φ w.toReducedWord)

Tactic:
erw [equiv_symm_eq_conj, mul_assoc, mul_assoc]

Premises used: mul_assoc, HNNExtension.equiv_symm_eq_conj
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
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 w
neg :
  (of : (a : G) → HNNExtension G A B φ)
        (↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
              ((⋯.equiv (S := (↑(toSubgroup A B u) : Set G)) (T := d.set u) :
                    (a : G) → ↥(toSubgroup A B u) × (↑(d.set u) : Type u_1))
                  w.head).1) :
          G) *
      (HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) *
        (HMul.hMul (α := HNNExtension G A B φ) (β := HNNExtension G A B φ)
            ((of : (a : G) → HNNExtension G A B φ)
                (↑((⋯.equiv (S := (↑(toSubgroup A B u) : Set G)) (T := d.set u) :
                          (a : G) → ↥(toSubgroup A B u) × (↑(d.set u) : Type u_1))
                        w.head).2 :
                  G) :
              HNNExtension G A B φ)
            (((of : (a : G) → HNNExtension G A B φ) w.head)⁻¹ : HNNExtension G A B φ) *
          ReducedWord.prod φ w.toReducedWord)) =
    HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ w.toReducedWord
⊢ ReducedWord.prod φ
      (toReducedWord (d := d)
        (let g' := unitsSMulGroup φ d u w.head;
        cons (↑g'.1 : G) u (((↑g'.2 : G) * w.head⁻¹) • w) ⋯ ⋯)) =
    HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ w.toReducedWord

Tactic:
simp only [unitsSMulGroup, SetLike.coe_sort_coe, prod_cons, prod_group_smul, map_mul, map_inv]

Premises used: HNNExtension.NormalWord.prod_group_smul, SetLike.coe_sort_coe, map_inv, HNNExtension.NormalWord.prod_cons, map_mul, HNNExtension.NormalWord.unitsSMulGroup
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
hcan : ¬Cancels 1 w
neg :
  (of : (a : G) → HNNExtension G A B φ)
        (↑((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ : (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                w.head).1 :
          G) *
      ((of : (a : G) → HNNExtension G A B φ)
          (↑((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ : (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                  w.head).2 :
            G) *
        HMul.hMul (α := HNNExtension G A B φ) (((of : (a : G) → HNNExtension G A B φ) w.head)⁻¹ : HNNExtension G A B φ)
          (ReducedWord.prod φ w.toReducedWord)) =
    ReducedWord.prod φ w.toReducedWord
⊢ (of : (a : G) → HNNExtension G A B φ)
        (↑((toSubgroupEquiv φ 1 : (a : ↥(toSubgroup A B 1)) → ↥(toSubgroup A B (-1)))
              ((IsComplement.equiv (S := (↑(toSubgroup A B 1) : Set G)) (T := d.set 1) ⋯ :
                    (a : G) → ↥(toSubgroup A B 1) × (↑(d.set 1) : Type u_1))
                  w.head).1) :
          G) *
      (HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑1 : ℤ) *
        (HMul.hMul (α := HNNExtension G A B φ) (β := HNNExtension G A B φ)
            ((of : (a : G) → HNNExtension G A B φ)
                (↑((IsComplement.equiv (S := (↑(toSubgroup A B 1) : Set G)) (T := d.set 1) ⋯ :
                          (a : G) → ↥(toSubgroup A B 1) × (↑(d.set 1) : Type u_1))
                        w.head).2 :
                  G) :
              HNNExtension G A B φ)
            (((of : (a : G) → HNNExtension G A B φ) w.head)⁻¹ : HNNExtension G A B φ) *
          ReducedWord.prod φ w.toReducedWord)) =
    HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑1 : ℤ) * ReducedWord.prod φ w.toReducedWord

Tactic:
simp only [toSubgroup_neg_one, toSubgroup_one, toSubgroupEquiv_one, equiv_eq_conj, mul_assoc,
        Units.val_one, zpow_one, inv_mul_cancel_left, mul_right_inj]

Premises used: HNNExtension.toSubgroup_neg_one, inv_mul_cancel_left, HNNExtension.equiv_eq_conj, mul_assoc, HNNExtension.toSubgroup_one, zpow_one, mul_right_inj, Units.val_one, HNNExtension.toSubgroupEquiv_one
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
hcan : ¬Cancels 1 w
neg :
  (of : (a : G) → HNNExtension G A B φ)
        (↑((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ : (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                w.head).1 :
          G) *
      HMul.hMul (α := HNNExtension G A B φ)
        ((of : (a : G) → HNNExtension G A B φ)
            ((↑((IsComplement.equiv (S := (↑(toSubgroup A B 1) : Set G)) (T := d.set 1) ⋯ :
                          (a : G) → (↑(↑(toSubgroup A B 1) : Set G) : Type u_1) × (↑(d.set 1) : Type u_1))
                        w.head).1 :
                  G)⁻¹ *
              w.head) :
          HNNExtension G A B φ)
        (HMul.hMul (α := HNNExtension G A B φ) (((of : (a : G) → HNNExtension G A B φ) w.head)⁻¹ : HNNExtension G A B φ)
          (ReducedWord.prod φ w.toReducedWord)) =
    ReducedWord.prod φ w.toReducedWord
⊢ (of : (a : G) → HNNExtension G A B φ)
        (↑((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ : (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                w.head).1 :
          G) *
      ((of : (a : G) → HNNExtension G A B φ)
          (↑((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ : (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                  w.head).2 :
            G) *
        HMul.hMul (α := HNNExtension G A B φ) (((of : (a : G) → HNNExtension G A B φ) w.head)⁻¹ : HNNExtension G A B φ)
          (ReducedWord.prod φ w.toReducedWord)) =
    ReducedWord.prod φ w.toReducedWord

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

Premises used: HNNExtension.NormalWord.TransversalPair.compl, OfNat.ofNat, Subgroup.IsComplement.equiv_snd_eq_inv_mul