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
u : ℤˣ
g : G
w : NormalWord d
h_1 : ∀ (h : Cancels u w), ¬Cancels (-u) (unitsSMulWithCancel φ u w ⋯)
h1 : w.head ∈ d.set (-u)
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B (-u) → -u = u'
h_2 : Cancels u (cons g (-u) w h1 h2)
hc : Cancels (-u) (unitsSMulWithCancel φ u (cons g (-u) w h1 h2) ⋯)
h : g ∈ toSubgroup A B u ∧ -u = -u
⊢ Cancels (-u) w

Tactic:
simpa [Cancels, unitsSMulWithCancel,
        Subgroup.mul_mem_cancel_left] using hc

Premises used: HNNExtension.NormalWord.Cancels, Subgroup.mul_mem_cancel_left, HNNExtension.NormalWord.unitsSMulWithCancel
-- 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
h : Cancels u w
pos :
  ∀ (g : G) (h : Cancels (A := A) (B := B) (d := d) u (ofGroup g)),
    ¬Cancels (-u) (unitsSMulWithCancel φ u (ofGroup g) ⋯)
pos₁ :
  ∀ (g : G) (u' : ℤˣ) (w : NormalWord d) (h1 : w.head ∈ d.set u')
    (h2 : ∀ u'_1 ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u' → u' = u'_1),
    (∀ (h : Cancels u w), ¬Cancels (-u) (unitsSMulWithCancel φ u w ⋯)) →
      ∀ (h : Cancels u (cons g u' w h1 h2)), ¬Cancels (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) ⋯)
⊢ ¬Cancels (-u) (unitsSMulWithCancel φ u w ⋯)

Tactic:
induction w using consRecOn with
    | ofGroup => simp [Cancels, unitsSMulWithCancel]
    | cons g u' w h1 h2 _ =>
      intro hc
      apply not_cancels_of_cons_hyp _ _ h2
      simp only [Cancels, cons_head, cons_toList, List.head?_cons,
        Option.map_some, Option.some.injEq] at h
      cases h.2
      simpa [Cancels, unitsSMulWithCancel,
        Subgroup.mul_mem_cancel_left] using hc

Premises used: HNNExtension.NormalWord.ofGroup, HNNExtension.NormalWord.Cancels, Option.some.injEq, Subgroup.mul_mem_cancel_left, And.right, List.head?_cons, Option.map_some, HNNExtension.NormalWord.cons, HNNExtension.NormalWord.cons_toList, HNNExtension.NormalWord.unitsSMulWithCancel, HNNExtension.NormalWord.cons_head
-- 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
h : ¬Cancels u w
neg :
  Cancels (-u)
      (cons (↑(unitsSMulGroup φ d u w.head).1 : G) u (((↑(unitsSMulGroup φ d u w.head).2 : G) * w.head⁻¹) • w) ⋯ ⋯) ↔
    ¬Cancels u w
⊢ Cancels (-u) (unitsSMul φ u w) ↔ ¬Cancels u w

Tactic:
simp only [unitsSMul, dif_neg h]

Premises used: dif_neg, HNNExtension.NormalWord.unitsSMul
-- 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
h : ¬Cancels u w
⊢ Cancels (-u)
      (cons (↑(unitsSMulGroup φ d u w.head).1 : G) u (((↑(unitsSMulGroup φ d u w.head).2 : G) * w.head⁻¹) • w) ⋯ ⋯) ↔
    ¬Cancels u w

Tactic:
simpa [Cancels] using h

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 : ℤˣ
w : NormalWord d
pos : ∀ (hcan : Cancels (-u) (unitsSMul φ u w)), unitsSMulWithCancel φ (-u) (unitsSMul φ u w) hcan = w
neg :
  ∀ (hcan : ¬Cancels (-u) (unitsSMul φ u w)),
    (let g' : ↥(toSubgroup A B (- -u)) × (↑(d.set (-u)) : Type u_1) := unitsSMulGroup φ d (-u) (unitsSMul φ u w).head;
      cons (↑g'.1 : G) (-u) (((↑g'.2 : G) * (unitsSMul φ u w).head⁻¹) • unitsSMul φ u w) ⋯ ⋯) =
      w
⊢ (if h : Cancels (-u) (unitsSMul φ u w) then unitsSMulWithCancel φ (-u) (unitsSMul φ u w) h
    else
      let g' : ↥(toSubgroup A B (- -u)) × (↑(d.set (-u)) : Type u_1) := unitsSMulGroup φ d (-u) (unitsSMul φ u w).head;
      cons (↑g'.1 : G) (-u) (((↑g'.2 : G) * (unitsSMul φ u w).head⁻¹) • unitsSMul φ u w) ⋯ ⋯) =
    w

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) (unitsSMul φ u w)
⊢ ¬Cancels u w

Tactic:
have hncan : ¬ Cancels u w := (unitsSMul_cancels_iff _ _ _).1 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) (unitsSMul φ u w)
hncan : ¬Cancels u w
pos :
  unitsSMulWithCancel φ (-u)
      (cons (↑(unitsSMulGroup φ d u w.head).1 : G) u (((↑(unitsSMulGroup φ d u w.head).2 : G) * w.head⁻¹) • w) ⋯ ⋯) ⋯ =
    w
⊢ unitsSMulWithCancel φ (-u)
      (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) ⋯ ⋯)
      hcan =
    w

Tactic:
simp only [dif_neg hncan]

Premises used: dif_neg
-- 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) (unitsSMul φ u w)
hncan : ¬Cancels u w
⊢ unitsSMulWithCancel φ (-u)
      (cons (↑(unitsSMulGroup φ d u w.head).1 : G) u (((↑(unitsSMulGroup φ d u w.head).2 : G) * w.head⁻¹) • w) ⋯ ⋯) ⋯ =
    w

Tactic:
simp [unitsSMulWithCancel, unitsSMulGroup, (d.compl u).equiv_snd_eq_inv_mul,
      -SetLike.coe_sort_coe]

Premises used: SetLike.coe_sort_coe, HNNExtension.NormalWord.TransversalPair.compl, HNNExtension.NormalWord.unitsSMulGroup, HNNExtension.NormalWord.unitsSMulWithCancel, Subgroup.IsComplement.equiv_snd_eq_inv_mul
-- 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) (unitsSMul φ u w)
⊢ Cancels u w

Tactic:
have hcan2 : Cancels u w := not_not.1 (mt (unitsSMul_cancels_iff _ _ _).2 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) (unitsSMul φ u w)
hcan2 : Cancels u w
neg :
  (let g' : ↥(toSubgroup A B (- -u)) × (↑(d.set (-u)) : Type u_1) :=
      unitsSMulGroup φ d (-u)
        (ReducedWord.head (A := A) (B := B)
          (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) ⋯ ⋯)));
    cons (↑g'.1 : G) (-u)
      (HSMul.hSMul (β := NormalWord d)
        ((↑g'.2 : G) *
          (ReducedWord.head (A := A) (B := B)
              (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) ⋯ ⋯)))⁻¹)
        (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) ⋯ ⋯))
      ⋯ ⋯) =
    w
⊢ (let g' : ↥(toSubgroup A B (- -u)) × (↑(d.set (-u)) : Type u_1) := unitsSMulGroup φ d (-u) (unitsSMul φ u w).head;
    cons (↑g'.1 : G) (-u) (((↑g'.2 : G) * (unitsSMul φ u w).head⁻¹) • unitsSMul φ u w) ⋯ ⋯) =
    w

Tactic:
unfold unitsSMul at hcan ⊢

Premises used: HNNExtension.NormalWord.unitsSMul
-- 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_1} (G := G) (A := A) (B := B) (d := d) (-u)
      (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) ⋯ ⋯)
hcan2 : Cancels u w
neg :
  ∀ (hcan_1 : ¬Cancels (-u) (unitsSMulWithCancel φ u w hcan2)),
    cons (↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u w hcan2).head).1 : G) (-u)
        (((↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u w hcan2).head).2 : G) *
            (unitsSMulWithCancel φ u w hcan2).head⁻¹) •
          unitsSMulWithCancel φ u w hcan2)
        ⋯ ⋯ =
      w
⊢ (let g' : ↥(toSubgroup A B (- -u)) × (↑(d.set (-u)) : Type u_1) :=
      unitsSMulGroup φ d (-u)
        (ReducedWord.head (A := A) (B := B)
          (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) ⋯ ⋯)));
    cons (↑g'.1 : G) (-u)
      (HSMul.hSMul (β := NormalWord d)
        ((↑g'.2 : G) *
          (ReducedWord.head (A := A) (B := B)
              (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) ⋯ ⋯)))⁻¹)
        (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) ⋯ ⋯))
      ⋯ ⋯) =
    w

Tactic:
simp only [dif_pos hcan2] at hcan ⊢

Premises used: dif_pos
-- 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_1 :
  ¬Cancels.{u_1} (G := G) (A := A) (B := B) (d := d) (-u)
      (if h : Cancels (A := A) (B := B) (d := d) u (ofGroup g) then unitsSMulWithCancel φ u (ofGroup g) h
      else
        let g' := unitsSMulGroup φ d u (ReducedWord.head (A := A) (B := B) (toReducedWord (d := d) (ofGroup g)));
        cons (↑g'.1 : G) u
          (HSMul.hSMul (β := NormalWord d)
            ((↑g'.2 : G) * (ReducedWord.head (A := A) (B := B) (toReducedWord (d := d) (ofGroup g)))⁻¹) (ofGroup g))
          ⋯ ⋯)
hcan2 : Cancels (A := A) (B := B) (d := d) u (ofGroup g)
hcan : ¬Cancels (-u) (unitsSMulWithCancel φ u (ofGroup g) hcan2)
⊢ cons (↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u (ofGroup g) hcan2).head).1 : G) (-u)
      (((↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u (ofGroup g) hcan2).head).2 : G) *
          (unitsSMulWithCancel φ u (ofGroup g) hcan2).head⁻¹) •
        unitsSMulWithCancel φ u (ofGroup g) hcan2)
      ⋯ ⋯ =
    ofGroup g

Tactic:
simp [Cancels] at hcan2

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' : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u'
h2 : ∀ u'_1 ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u' → u' = u'_1
hcan_1 :
  ¬Cancels.{u_1} (G := G) (A := A) (B := B) (d := d) (-u)
      (if h : Cancels u (cons g u' w h1 h2) then unitsSMulWithCancel φ u (cons g u' w h1 h2) h
      else
        let g' := unitsSMulGroup φ d u (cons g u' w h1 h2).head;
        cons (↑g'.1 : G) u (((↑g'.2 : G) * (cons g u' w h1 h2).head⁻¹) • cons g u' w h1 h2) ⋯ ⋯)
hcan2 : Cancels u (cons g u' w h1 h2)
hcan : ¬Cancels (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2)
neg :
  cons
      (↑((toSubgroupEquiv φ (-u) : (a : ↥(toSubgroup A B (-u))) → ↥(toSubgroup A B (- -u)))
            ((IsComplement.equiv (S := (↑(toSubgroup A B (-u)) : Set G)) (T := d.set (-u)) ⋯ :
                  (a : G) → ↥(toSubgroup A B (-u)) × (↑(d.set (-u)) : Type u_1))
                ((↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
                        (Subtype.mk (p := fun (x : G) ↦ x ∈ toSubgroup A B u) g ⋯)) :
                    G) *
                  w.head)).1) :
        G)
      (-u)
      (((↑((IsComplement.equiv (S := (↑(toSubgroup A B (-u)) : Set G)) (T := d.set (-u)) ⋯ :
                    (a : G) → ↥(toSubgroup A B (-u)) × (↑(d.set (-u)) : Type u_1))
                  ((↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
                          (Subtype.mk (p := fun (x : G) ↦ x ∈ toSubgroup A B u) g ⋯)) :
                      G) *
                    w.head)).2 :
            G) *
          (w.head⁻¹ *
            (↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
                    (Subtype.mk (p := fun (x : G) ↦ x ∈ toSubgroup A B u) g ⋯)) :
                G)⁻¹)) •
        HSMul.hSMul (α := G)
          (↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
                (Subtype.mk (p := fun (x : G) ↦ x ∈ toSubgroup A B u) g ⋯)) :
            G)
          w)
      ⋯ ⋯ =
    cons g u' w h1 h2
⊢ cons (↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2).head).1 : G) (-u)
      (((↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2).head).2 : G) *
          (unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2).head⁻¹) •
        unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2)
      ⋯ ⋯ =
    cons g u' w h1 h2

Tactic:
simp only [unitsSMulGroup, SetLike.coe_sort_coe, unitsSMulWithCancel, id_eq, consRecOn_cons,
        group_smul_head,
        mul_inv_rev]

Premises used: SetLike.coe_sort_coe, HNNExtension.NormalWord.consRecOn_cons, HNNExtension.NormalWord.group_smul_head, mul_inv_rev, HNNExtension.NormalWord.unitsSMulGroup, 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
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_1 :
  ¬Cancels.{u_1} (G := G) (A := A) (B := B) (d := d) (-u)
      (if h : Cancels u (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2) then
        unitsSMulWithCancel φ u (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ } w h1 h2) h
      else
        let g' :=
          unitsSMulGroup φ d u
            (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2).head;
        cons (↑g'.1 : G) u
          (((↑g'.2 : G) *
              (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2).head⁻¹) •
            cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2)
          ⋯ ⋯)
hcan2 : Cancels u (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2)
hcan :
  ¬Cancels (-u)
      (unitsSMulWithCancel φ u
        (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2) hcan2)
⊢ Eq.{u_1 + 1} (α := (↑(↑(toSubgroup A B (-u)) : Set G) : Type u_1))
    ((IsComplement.equiv (S := (↑(toSubgroup A B (-u)) : Set G)) (T := d.set (-u)) ⋯ :
          (a : G) → (↑(↑(toSubgroup A B (-u)) : Set G) : Type u_1) × (↑(d.set (-u)) : Type u_1))
        w.head).1
    1

Tactic:
have : ((d.compl (-u)).equiv w.head).1 = 1 :=
        (d.compl (-u)).equiv_fst_eq_one_of_mem_of_one_mem _ h1
-- 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
x : NormalWord d
rw rw₁ : x = x
⊢ unitsSMul φ (-1) (unitsSMul φ 1 x) = x

Tactic:
rw [unitsSMul_neg]

Premises used: HNNExtension.NormalWord.unitsSMul_neg
-- 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
⊢ unitsSMul φ (- -1) (unitsSMul φ (-1) w) = w

Tactic:
unitsSMul_neg _ _ w

Premises used: HNNExtension.NormalWord.unitsSMul_neg
-- 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
h : Eq (α := ℤˣ) 1 (- -1)
⊢ unitsSMul φ 1 (unitsSMul φ (-1) w) = w

Tactic:
convert! unitsSMul_neg _ _ w

Premises used: HNNExtension.NormalWord.unitsSMul_neg
-- 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
⊢ Eq (α := ℤˣ) 1 (- -1)

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 : ↥A
w : NormalWord d
unfold :
  (if h : Cancels 1 ((↑g : G) • w) then unitsSMulWithCancel φ 1 ((↑g : G) • w) h
    else
      let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 ((↑g : G) • w).head;
      cons (↑g'.1 : G) 1 (((↑g'.2 : G) * ((↑g : G) • w).head⁻¹) • (↑g : G) • w) ⋯ ⋯) =
    HSMul.hSMul (α := G) (β := NormalWord d) (↑((φ : (a : ↥A) → ↥B) g) : G)
      (if h : Cancels 1 w then unitsSMulWithCancel φ 1 w h
      else
        let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 w.head;
        cons (↑g'.1 : G) 1 (((↑g'.2 : G) * w.head⁻¹) • w) ⋯ ⋯)
⊢ unitsSMul φ 1 ((↑g : G) • w) = HSMul.hSMul (α := G) (↑((φ : (a : ↥A) → ↥B) g) : G) (unitsSMul φ 1 w)

Tactic:
unfold unitsSMul

Premises used: HNNExtension.NormalWord.unitsSMul
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
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 : G) • w) ↔ Cancels 1 w

Tactic:
simp [Cancels, Subgroup.mul_mem_cancel_left]

Premises used: HNNExtension.NormalWord.Cancels, Subgroup.mul_mem_cancel_left
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
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 : G) • w) ↔ Cancels 1 w

Tactic:
have : Cancels 1 ((g : G) • w) ↔ Cancels 1 w := by
    simp [Cancels, Subgroup.mul_mem_cancel_left]
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
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 : G) • w) ↔ Cancels 1 w
pos :
  ∀ (hcan : Cancels 1 w),
    (if h : Cancels 1 ((↑g : G) • w) then unitsSMulWithCancel φ 1 ((↑g : G) • w) h
      else
        let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 ((↑g : G) • w).head;
        cons (↑g'.1 : G) 1 (((↑g'.2 : G) * ((↑g : G) • w).head⁻¹) • (↑g : G) • w) ⋯ ⋯) =
      HSMul.hSMul (α := G) (β := NormalWord d) (↑((φ : (a : ↥A) → ↥B) g) : G)
        (if h : Cancels 1 w then unitsSMulWithCancel φ 1 w h
        else
          let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 w.head;
          cons (↑g'.1 : G) 1 (((↑g'.2 : G) * w.head⁻¹) • w) ⋯ ⋯)
neg :
  ∀ (hcan : ¬Cancels 1 w),
    (if h : Cancels 1 ((↑g : G) • w) then unitsSMulWithCancel φ 1 ((↑g : G) • w) h
      else
        let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 ((↑g : G) • w).head;
        cons (↑g'.1 : G) 1 (((↑g'.2 : G) * ((↑g : G) • w).head⁻¹) • (↑g : G) • w) ⋯ ⋯) =
      HSMul.hSMul (α := G) (β := NormalWord d) (↑((φ : (a : ↥A) → ↥B) g) : G)
        (if h : Cancels 1 w then unitsSMulWithCancel φ 1 w h
        else
          let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 w.head;
          cons (↑g'.1 : G) 1 (((↑g'.2 : G) * w.head⁻¹) • w) ⋯ ⋯)
⊢ (if h : Cancels 1 ((↑g : G) • w) then unitsSMulWithCancel φ 1 ((↑g : G) • w) h
    else
      let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 ((↑g : G) • w).head;
      cons (↑g'.1 : G) 1 (((↑g'.2 : G) * ((↑g : G) • w).head⁻¹) • (↑g : G) • w) ⋯ ⋯) =
    HSMul.hSMul (α := G) (β := NormalWord d) (↑((φ : (a : ↥A) → ↥B) g) : G)
      (if h : Cancels 1 w then unitsSMulWithCancel φ 1 w h
      else
        let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 w.head;
        cons (↑g'.1 : G) 1 (((↑g'.2 : G) * w.head⁻¹) • w) ⋯ ⋯)

Tactic:
by_cases hcan : Cancels 1 w

Premises used: HNNExtension.NormalWord.Cancels, OfNat.ofNat
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
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 : G) • w) ↔ Cancels 1 w
hcan : Cancels 1 w
pos :
  consRecOn (motive := fun (x : NormalWord d) ↦ Cancels 1 x → NormalWord d) ((↑g : G) • w)
      (fun (g_1 : G) (a : g_1 ∈ A ∧ Eq (α := Option ℤˣ) none (some (-1))) ↦ (↑g : G) • w)
      (fun (g : G) (x : ℤˣ) (w : NormalWord d) (x_1 : w.head ∈ d.set x)
          (x_2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B x → x = u')
          (x_3 : Cancels 1 w → NormalWord d) (can : Cancels 1 (cons g x w x_1 x_2)) ↦
        HSMul.hSMul (α := G) (↑((φ : (a : ↥A) → ↥B) (Subtype.mk (p := fun (x : G) ↦ x ∈ A) g ⋯)) : G) w)
      ⋯ =
    HSMul.hSMul (α := G) (β := NormalWord d) (↑((φ : (a : ↥A) → ↥B) g) : G)
      (consRecOn (motive := fun (x : NormalWord d) ↦ Cancels 1 x → NormalWord d) w
          (fun (g : G) (a : g ∈ A ∧ Eq (α := Option ℤˣ) none (some (-1))) ↦ w)
          (fun (g : G) (x : ℤˣ) (w : NormalWord d) (x_1 : w.head ∈ d.set x)
              (x_2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B x → x = u')
              (x_3 : Cancels 1 w → NormalWord d) (can : Cancels 1 (cons g x w x_1 x_2)) ↦
            HSMul.hSMul (α := G) (↑((φ : (a : ↥A) → ↥B) (Subtype.mk (p := fun (x : G) ↦ x ∈ A) g ⋯)) : G) w)
          hcan :
        NormalWord d)
⊢ (if h : Cancels 1 ((↑g : G) • w) then unitsSMulWithCancel φ 1 ((↑g : G) • w) h
    else
      let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 ((↑g : G) • w).head;
      cons (↑g'.1 : G) 1 (((↑g'.2 : G) * ((↑g : G) • w).head⁻¹) • (↑g : G) • w) ⋯ ⋯) =
    HSMul.hSMul (α := G) (β := NormalWord d) (↑((φ : (a : ↥A) → ↥B) g) : G)
      (if h : Cancels 1 w then unitsSMulWithCancel φ 1 w h
      else
        let g' : ↥(toSubgroup A B (-1)) × (↑(d.set 1) : Type u_1) := unitsSMulGroup φ d 1 w.head;
        cons (↑g'.1 : G) 1 (((↑g'.2 : G) * w.head⁻¹) • w) ⋯ ⋯)

Tactic:
simp only [unitsSMulWithCancel, toSubgroup_one, id_eq, toSubgroup_neg_one, toSubgroupEquiv_one,
      group_smul_head, mul_inv_rev, dif_pos (this.2 hcan), dif_pos hcan]

Premises used: Iff.mpr, HNNExtension.toSubgroup_neg_one, HNNExtension.toSubgroup_one, dif_pos, HNNExtension.NormalWord.group_smul_head, HNNExtension.toSubgroupEquiv_one, mul_inv_rev, HNNExtension.NormalWord.unitsSMulWithCancel, id_eq