awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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 φ)
        (↑((φ.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)
have 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 sorry) : 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)
Tactic: erw [equiv_symm_eq_conj, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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)
⊢ (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)
have 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 sorry) : 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)
Tactic: erw [equiv_symm_eq_conj, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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)
⊢ (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)
have pos₂ : t⁻¹ *
    HMul.hMul (α := HNNExtension G A B φ)
      ((of : (a : G) → HNNExtension G A B φ) (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ B) g sorry) : 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)
Tactic: erw [equiv_symm_eq_conj, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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
⊢ 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
have neg : (of : (a : G) → HNNExtension G A B φ)
      (↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
            ((sorry.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 φ)
              (↑((sorry.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
Tactic: simp only [unitsSMulGroup, SetLike.coe_sort_coe, prod_cons, prod_group_smul, map_mul, map_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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
⊢ (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
have neg : ∀ (hcan : ¬Cancels 1 w),
  (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) sorry :
                    (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) sorry :
                          (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: rcases Int.units_eq_one_or u with (rfl | rfl)
Cleared hypotheses: u, hcan
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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 φ)
        (↑((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
have neg : (of : (a : G) → HNNExtension G A B φ)
      (↑((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) sorry : (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) sorry : (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: 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]
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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) *
      ((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
have neg : (of : (a : G) → HNNExtension G A B φ)
      (↑((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) sorry : (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) sorry :
                        (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: erw [(d.compl 1).equiv_snd_eq_inv_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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 φ)
        (↑((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
have 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)) sorry : (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)) sorry : (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: simp only [toSubgroup_neg_one, toSubgroupEquiv_neg_one, Units.val_neg, Units.val_one,
        Int.reduceNeg, zpow_neg, zpow_one, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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 φ)
        (↑((φ.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
have 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)) sorry : (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)) sorry :
                          (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: erw [equiv_symm_eq_conj, (d.compl (-1)).equiv_snd_eq_inv_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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⁻¹ • w).toReducedWord = x⁻¹ * ReducedWord.prod φ w.toReducedWord
have inv : ReducedWord.prod φ (x • x⁻¹ • w).toReducedWord = x * (x⁻¹ * ReducedWord.prod φ w.toReducedWord)
Tactic: rw [← mul_right_inj x, ← ih]
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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
⊢ ReducedWord.prod φ (g • w).toReducedWord = g * ReducedWord.prod φ w.toReducedWord
have of : ∀ (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: 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
Cleared hypotheses: g, w
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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)
⊢ ReducedWord.prod φ (g • w).toReducedWord = g * ReducedWord.prod φ w.toReducedWord
have t : ∀ (w : NormalWord d),
  ReducedWord.prod φ (HSMul.hSMul (α := HNNExtension G A B φ) t w).toReducedWord =
    t * 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
Cleared hypotheses: g, w
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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
⊢ ReducedWord.prod φ (g • w).toReducedWord = g * ReducedWord.prod φ w.toReducedWord
have 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
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
Cleared hypotheses: g, w