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
d : TransversalPair G A B
w : NormalWord d
hcan : ¬Cancels 1 w
⊢ (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

Tactic:
simp [mul_assoc]

Premises used: 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
w : NormalWord d
hcan : ¬Cancels (-1) w
neg :
  (of : (a : G) → HNNExtension G A B φ)
        (↑((φ.symm : (a : ↥B) → ↥(toSubgroup A B (- -1)))
              ((IsComplement.equiv (S := (↑B : Set G)) (T := d.set (-1)) ⋯ : (a : G) → ↥B × (↑(d.set (-1)) : Type u_1))
                  w.head).1) :
          G) *
      (t⁻¹ *
        ((of : (a : G) → HNNExtension G A B φ)
            (↑((IsComplement.equiv (S := (↑B : Set G)) (T := d.set (-1)) ⋯ : (a : G) → ↥B × (↑(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))) =
    t⁻¹ * 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, toSubgroupEquiv_neg_one, Units.val_neg, Units.val_one,
        Int.reduceNeg, zpow_neg, zpow_one, mul_assoc]

Premises used: HNNExtension.toSubgroup_neg_one, HNNExtension.toSubgroupEquiv_neg_one, Int.reduceNeg, mul_assoc, zpow_one, Units.val_neg, 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
w : NormalWord d
hcan : ¬Cancels (-1) w
neg :
  HMul.hMul (α := HNNExtension G A B φ) t⁻¹
          ((of : (a : G) → HNNExtension G A B φ)
            (↑((IsComplement.equiv (S := (↑B : Set G)) (T := d.set (-1)) ⋯ : (a : G) → ↥B × (↑(d.set (-1)) : Type u_1))
                    w.head).1 :
              G)) *
        t *
      (t⁻¹ *
        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))) =
    t⁻¹ * ReducedWord.prod φ w.toReducedWord
⊢ (of : (a : G) → HNNExtension G A B φ)
        (↑((φ.symm : (a : ↥B) → ↥(toSubgroup A B (- -1)))
              ((IsComplement.equiv (S := (↑B : Set G)) (T := d.set (-1)) ⋯ : (a : G) → ↥B × (↑(d.set (-1)) : Type u_1))
                  w.head).1) :
          G) *
      (t⁻¹ *
        ((of : (a : G) → HNNExtension G A B φ)
            (↑((IsComplement.equiv (S := (↑B : Set G)) (T := d.set (-1)) ⋯ : (a : G) → ↥B × (↑(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))) =
    t⁻¹ * ReducedWord.prod φ w.toReducedWord

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

Premises used: HNNExtension.NormalWord.TransversalPair.compl, HNNExtension.equiv_symm_eq_conj, OfNat.ofNat, Subgroup.IsComplement.equiv_snd_eq_inv_mul, Neg.neg
-- 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
⊢ HMul.hMul (α := HNNExtension G A B φ) t⁻¹
          ((of : (a : G) → HNNExtension G A B φ)
            (↑((IsComplement.equiv (S := (↑B : Set G)) (T := d.set (-1)) ⋯ : (a : G) → ↥B × (↑(d.set (-1)) : Type u_1))
                    w.head).1 :
              G)) *
        t *
      (t⁻¹ *
        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))) =
    t⁻¹ * ReducedWord.prod φ w.toReducedWord

Tactic:
simp [mul_assoc]

Premises used: 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
⊢ ReducedWord.prod φ (toReducedWord (d := d) empty) = 1

Tactic:
simp [ReducedWord.prod]

Premises used: 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
⊢ ReducedWord.prod φ
      (HSMul.hSMul (α := HNNExtension G A B φ) ((of : (a : G) → HNNExtension G A B φ) g : HNNExtension G A B φ)
          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 [of_smul_eq_smul]

Premises used: HNNExtension.NormalWord.of_smul_eq_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
⊢ ReducedWord.prod φ (HSMul.hSMul (α := HNNExtension G A B φ) t w).toReducedWord =
    t * ReducedWord.prod φ w.toReducedWord

Tactic:
simp [t_smul_eq_unitsSMul, prod_unitsSMul]

Premises used: HNNExtension.NormalWord.t_smul_eq_unitsSMul, HNNExtension.NormalWord.prod_unitsSMul
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
x y : HNNExtension G A B φ
h : ∀ (w : NormalWord d), ReducedWord.prod φ (x • w).toReducedWord = x * ReducedWord.prod φ w.toReducedWord
h_1 : ∀ (w : NormalWord d), ReducedWord.prod φ (y • w).toReducedWord = y * ReducedWord.prod φ w.toReducedWord
w : NormalWord d
⊢ ReducedWord.prod φ ((x * y) • w).toReducedWord = x * y * ReducedWord.prod φ w.toReducedWord

Tactic:
simp_all [mul_smul, mul_assoc]

Premises used: mul_assoc, SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
x : HNNExtension G A B φ
ih : ∀ (w : NormalWord d), ReducedWord.prod φ (x • w).toReducedWord = x * ReducedWord.prod φ w.toReducedWord
w : NormalWord d
inv : ReducedWord.prod φ (x • x⁻¹ • w).toReducedWord = x * (x⁻¹ * ReducedWord.prod φ w.toReducedWord)
⊢ ReducedWord.prod φ (x⁻¹ • w).toReducedWord = x⁻¹ * ReducedWord.prod φ w.toReducedWord

Tactic:
rw [← mul_right_inj x, ← ih]

Premises used: mul_right_inj
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
x : HNNExtension G A B φ
ih : ∀ (w : NormalWord d), ReducedWord.prod φ (x • w).toReducedWord = x * ReducedWord.prod φ w.toReducedWord
w : NormalWord d
⊢ ReducedWord.prod φ (x • x⁻¹ • w).toReducedWord = x * (x⁻¹ * ReducedWord.prod φ w.toReducedWord)

Tactic:
simp
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : HNNExtension G A B φ
w : NormalWord d
of :
  ∀ (g : G) (w : NormalWord d),
    ReducedWord.prod φ
        (HSMul.hSMul (α := HNNExtension G A B φ)
            ((HNNExtension.of : (a : G) → HNNExtension G A B φ) g : HNNExtension G A B φ) w).toReducedWord =
      HMul.hMul (α := HNNExtension G A B φ)
        ((HNNExtension.of : (a : G) → HNNExtension G A B φ) g : HNNExtension G A B φ)
        (ReducedWord.prod φ w.toReducedWord)
t :
  ∀ (w : NormalWord d),
    ReducedWord.prod φ (HSMul.hSMul (α := HNNExtension G A B φ) HNNExtension.t w).toReducedWord =
      HNNExtension.t * ReducedWord.prod φ w.toReducedWord
mul :
  ∀ (x y : HNNExtension G A B φ),
    (∀ (w : NormalWord d), ReducedWord.prod φ (x • w).toReducedWord = x * ReducedWord.prod φ w.toReducedWord) →
      (∀ (w : NormalWord d), ReducedWord.prod φ (y • w).toReducedWord = y * ReducedWord.prod φ w.toReducedWord) →
        ∀ (w : NormalWord d),
          ReducedWord.prod φ ((x * y) • w).toReducedWord = x * y * ReducedWord.prod φ w.toReducedWord
inv :
  ∀ (x : HNNExtension G A B φ)
    (ih : ∀ (w : NormalWord d), ReducedWord.prod φ (x • w).toReducedWord = x * ReducedWord.prod φ w.toReducedWord)
    (w : NormalWord d), ReducedWord.prod φ (x⁻¹ • w).toReducedWord = x⁻¹ * ReducedWord.prod φ w.toReducedWord
⊢ ReducedWord.prod φ (g • w).toReducedWord = g * ReducedWord.prod φ w.toReducedWord

Tactic:
induction g using induction_on generalizing w with
  | of => simp [of_smul_eq_smul]
  | t => simp [t_smul_eq_unitsSMul, prod_unitsSMul]
  | mul => simp_all [mul_smul, mul_assoc]
  | inv x ih =>
    rw [← mul_right_inj x, ← ih]
    simp

Premises used: HNNExtension.NormalWord.t_smul_eq_unitsSMul, mul_assoc, HNNExtension.NormalWord.prod_unitsSMul, HNNExtension.of, HNNExtension.t, Multiplicative.inv, HNNExtension.NormalWord.of_smul_eq_smul, SemigroupAction.mul_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
⊢ HSMul.hSMul (β := NormalWord d) (ReducedWord.prod φ (toReducedWord (d := d) (ofGroup g))) empty = ofGroup g

Tactic:
simp [ofGroup, ReducedWord.prod, of_smul_eq_smul, group_smul_def]

Premises used: HNNExtension.NormalWord.ofGroup, HNNExtension.NormalWord.group_smul_def, HNNExtension.NormalWord.ReducedWord.prod, HNNExtension.NormalWord.of_smul_eq_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'
ih : HSMul.hSMul (β := NormalWord d) (ReducedWord.prod φ w.toReducedWord) empty = w
cons :
  HSMul.hSMul (β := NormalWord d) g
      (if h : Cancels u w then unitsSMulWithCancel φ u w h
      else
        let g' := unitsSMulGroup φ d u w.head;
        NormalWord.cons (↑g'.1 : G) u (((↑g'.2 : G) * w.head⁻¹) • w) ⋯ ⋯) =
    NormalWord.cons g u w h1 h2
⊢ HSMul.hSMul (β := NormalWord d) (ReducedWord.prod φ (NormalWord.cons g u w h1 h2).toReducedWord) empty =
    NormalWord.cons g u w h1 h2

Tactic:
rw [prod_cons, ← mul_assoc, mul_smul, ih, mul_smul, t_pow_smul_eq_unitsSMul,
      of_smul_eq_smul, unitsSMul]

Premises used: HNNExtension.NormalWord.prod_cons, mul_assoc, HNNExtension.NormalWord.unitsSMul, HNNExtension.NormalWord.of_smul_eq_smul, HNNExtension.NormalWord.t_pow_smul_eq_unitsSMul, SemigroupAction.mul_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'
ih : HSMul.hSMul (β := NormalWord d) (ReducedWord.prod φ w.toReducedWord) empty = w
cons :
  HSMul.hSMul (β := NormalWord d) g
      (let g' := unitsSMulGroup φ d u w.head;
      NormalWord.cons (↑g'.1 : G) u (((↑g'.2 : G) * w.head⁻¹) • w) ⋯ ⋯) =
    NormalWord.cons g u w h1 h2
⊢ HSMul.hSMul (β := NormalWord d) g
      (if h : Cancels u w then unitsSMulWithCancel φ u w h
      else
        let g' := unitsSMulGroup φ d u w.head;
        NormalWord.cons (↑g'.1 : G) u (((↑g'.2 : G) * w.head⁻¹) • w) ⋯ ⋯) =
    NormalWord.cons g u w h1 h2

Tactic:
rw [dif_neg (not_cancels_of_cons_hyp u w h2)]

Premises used: dif_neg, HNNExtension.NormalWord.not_cancels_of_cons_hyp
-- 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'
ih : HSMul.hSMul (β := NormalWord d) (ReducedWord.prod φ w.toReducedWord) empty = w
cons :
  NormalWord.cons
      (g *
        (↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
              (Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(toSubgroup A B u) : Set G)) 1 ⋯)) :
          G))
      u w ⋯ ⋯ =
    NormalWord.cons g u w h1 h2
⊢ HSMul.hSMul (β := NormalWord d) g
      (let g' := unitsSMulGroup φ d u w.head;
      NormalWord.cons (↑g'.1 : G) u (((↑g'.2 : G) * w.head⁻¹) • w) ⋯ ⋯) =
    NormalWord.cons g u w h1 h2

Tactic:
simp only [unitsSMulGroup, (d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1,
      (d.compl _).equiv_snd_eq_inv_mul, inv_one, one_mul, mul_inv_cancel, one_smul, smul_cons]

Premises used: inv_one, Subgroup.IsComplement.equiv_fst_eq_one_of_mem_of_one_mem, one_smul, HNNExtension.NormalWord.smul_cons, mul_inv_cancel, HNNExtension.NormalWord.TransversalPair.compl, OneMemClass.one_mem, HNNExtension.NormalWord.unitsSMulGroup, Subgroup.IsComplement.equiv_snd_eq_inv_mul, one_mul
-- 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'
ih : HSMul.hSMul (β := NormalWord d) (ReducedWord.prod φ w.toReducedWord) empty = w
cons :
  (NormalWord.cons
        (g *
          (↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
                (Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(toSubgroup A B u) : Set G)) 1 ⋯)) :
            G))
        u w ⋯ ⋯).head =
    (NormalWord.cons g u w h1 h2).head
cons₁ :
  ∀ (i : ℕ) (a : ℤˣ × G),
    getElem? (valid := fun (as : List (ℤˣ × G)) (i : ℕ) ↦ i < as.length)
          (NormalWord.cons
              (g *
                (↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
                      (Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(toSubgroup A B u) : Set G)) 1 ⋯)) :
                  G))
              u w ⋯ ⋯).toList
          i =
        some a ↔
      getElem? (valid := fun (as : List (ℤˣ × G)) (i : ℕ) ↦ i < as.length) (NormalWord.cons g u w h1 h2).toList i =
        some a
⊢ NormalWord.cons
      (g *
        (↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
              (Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(toSubgroup A B u) : Set G)) 1 ⋯)) :
          G))
      u w ⋯ ⋯ =
    NormalWord.cons g u w h1 h2

Tactic:
ext
-- 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'
ih : HSMul.hSMul (β := NormalWord d) (ReducedWord.prod φ w.toReducedWord) empty = w
⊢ (cons
        (g *
          (↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
                (Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(toSubgroup A B u) : Set G)) 1 ⋯)) :
            G))
        u w ⋯ ⋯).head =
    (cons g u w h1 h2).head

Tactic:
simp
-- 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'
ih : HSMul.hSMul (β := NormalWord d) (ReducedWord.prod φ w.toReducedWord) empty = w
i : ℕ
a : ℤˣ × G
⊢ getElem? (valid := fun (as : List (ℤˣ × G)) (i : ℕ) ↦ i < as.length)
        (cons
            (g *
              (↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
                    (Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(toSubgroup A B u) : Set G)) 1 ⋯)) :
                G))
            u w ⋯ ⋯).toList
        i =
      some a ↔
    getElem? (valid := fun (as : List (ℤˣ × G)) (i : ℕ) ↦ i < as.length) (cons g u w h1 h2).toList i = some a

Tactic:
simp
-- 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
ofGroup :
  ∀ (g : G),
    HSMul.hSMul (β := NormalWord d) (ReducedWord.prod φ (toReducedWord (d := d) (NormalWord.ofGroup g))) empty =
      NormalWord.ofGroup g
cons :
  ∀ (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')
    (ih : HSMul.hSMul (β := NormalWord d) (ReducedWord.prod φ w.toReducedWord) empty = w),
    HSMul.hSMul (β := NormalWord d) (ReducedWord.prod φ (NormalWord.cons g u w h1 h2).toReducedWord) empty =
      NormalWord.cons g u w h1 h2
⊢ HSMul.hSMul (β := NormalWord d) (ReducedWord.prod φ w.toReducedWord) empty = w

Tactic:
induction w using consRecOn with
  | ofGroup => simp [ofGroup, ReducedWord.prod, of_smul_eq_smul, group_smul_def]
  | cons g u w h1 h2 ih =>
    rw [prod_cons, ← mul_assoc, mul_smul, ih, mul_smul, t_pow_smul_eq_unitsSMul,
      of_smul_eq_smul, unitsSMul]
    rw [dif_neg (not_cancels_of_cons_hyp u w h2)]
    -- Before https://github.com/leanprover/lean4/pull/2644, this was just
    -- simp [unitsSMulGroup, (d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1,
    --   -SetLike.coe_sort_coe]
    -- ext <;> simp [-SetLike.coe_sort_coe]
    simp only [unitsSMulGroup, (d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1,
      (d.compl _).equiv_snd_eq_inv_mul, inv_one, one_mul, mul_inv_cancel, one_smul, smul_cons]
    ext <;> simp

Premises used: HNNExtension.NormalWord.ofGroup, inv_one, HNNExtension.NormalWord.prod_cons, mul_assoc, HNNExtension.NormalWord.group_smul_def, one_smul, HNNExtension.NormalWord.unitsSMul, HNNExtension.NormalWord.ReducedWord.prod, HNNExtension.NormalWord.smul_cons, mul_inv_cancel, HNNExtension.NormalWord.cons, HNNExtension.NormalWord.TransversalPair.compl, HNNExtension.NormalWord.of_smul_eq_smul, HNNExtension.NormalWord.unitsSMulGroup, Subgroup.IsComplement.equiv_snd_eq_inv_mul, HNNExtension.NormalWord.t_pow_smul_eq_unitsSMul, SemigroupAction.mul_smul, one_mul
-- 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
g : HNNExtension G A B φ
⊢ (fun (w : NormalWord d) ↦ ReducedWord.prod φ w.toReducedWord)
      ((fun (g : HNNExtension G A B φ) ↦ HSMul.hSMul (β := NormalWord d) g empty) g) =
    g

Tactic:
simp [prod_smul]

Premises used: HNNExtension.NormalWord.prod_smul
-- 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
w : NormalWord d
⊢ (fun (g : HNNExtension G A B φ) ↦ HSMul.hSMul (β := NormalWord d) g empty)
      ((fun (w : NormalWord d) ↦ ReducedWord.prod φ w.toReducedWord) w) =
    w

Tactic:
simp
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
⊢ Injective (β := HNNExtension G A B φ) fun (w : NormalWord d) ↦ ReducedWord.prod φ w.toReducedWord

Tactic:
(equiv φ d).symm.injective

Premises used: Quotient.map₂, HNNExtension.NormalWord.ReducedWord.prod, Equiv.injective, Equiv.symm, HNNExtension.NormalWord.equiv
-- 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
m₁ m₂ : HNNExtension G A B φ
h : ∀ (a : NormalWord d), m₁ • a = m₂ • a
⊢ m₁ = m₂

Tactic:
simpa using congr_arg (fun w => w.prod φ) (h empty)

Premises used: HNNExtension.NormalWord.empty, congr_arg
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
rcases :
  ∀ (d : TransversalPair G A B),
    Injective.{u_1 + 1, u_1 + 1} (α := G) (β := HNNExtension G A B φ) (⇑of : (a : G) → HNNExtension G A B φ)
⊢ Injective.{u_1 + 1, u_1 + 1} (α := G) (β := HNNExtension G A B φ) (⇑of : (a : G) → HNNExtension G A B φ)

Tactic:
rcases TransversalPair.nonempty G A B with ⟨d⟩

Premises used: HNNExtension.NormalWord.TransversalPair.nonempty
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
⊢ Injective.{u_1 + 1, u_1 + 1} (α := G) (β := HNNExtension G A B φ) (⇑of : (a : G) → HNNExtension G A B φ)

Tactic:
Function.Injective.of_comp
    (f := ((· • ·) : HNNExtension G A B φ → NormalWord d → NormalWord d)) ?_

Premises used: Function.Injective.of_comp
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
refine :
  Injective.{u_1 + 1, u_1 + 1} (α := G) (β := NormalWord d → NormalWord d)
    ((fun (x1 : HNNExtension G A B φ) (x2 : NormalWord d) ↦ x1 • x2) ∘ (⇑of : (a : G) → HNNExtension G A B φ))
⊢ Injective.{u_1 + 1, u_1 + 1} (α := G) (β := HNNExtension G A B φ) (⇑of : (a : G) → HNNExtension G A B φ)

Tactic:
refine Function.Injective.of_comp
    (f := ((· • ·) : HNNExtension G A B φ → NormalWord d → NormalWord d)) ?_

Premises used: Function.Injective.of_comp
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
a₁ : G
_ :
  ∀ ⦃a₂ : G⦄,
    Eq (α := NormalWord d → NormalWord d)
        (((fun (x1 : HNNExtension G A B φ) (x2 : NormalWord d) ↦ x1 • x2) ∘ (⇑of : (a : G) → HNNExtension G A B φ)) a₁)
        (((fun (x1 : HNNExtension G A B φ) (x2 : NormalWord d) ↦ x1 • x2) ∘ (⇑of : (a : G) → HNNExtension G A B φ))
          a₂) →
      a₁ = a₂
⊢ ∀ ⦃a₂ : G⦄,
    Eq (α := NormalWord d → NormalWord d)
        (((fun (x1 : HNNExtension G A B φ) (x2 : NormalWord d) ↦ x1 • x2) ∘ (⇑of : (a : G) → HNNExtension G A B φ)) a₁)
        (((fun (x1 : HNNExtension G A B φ) (x2 : NormalWord d) ↦ x1 • x2) ∘ (⇑of : (a : G) → HNNExtension G A B φ))
          a₂) →
      a₁ = a₂

Tactic:
_