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
g : ↥A
g_1 : G
this :
  Cancels 1 (HSMul.hSMul (β := NormalWord d) (↑g : G) (ofGroup g_1)) ↔
    Cancels (A := A) (B := B) (d := d) 1 (ofGroup g_1)
hcan : Cancels (A := A) (B := B) (d := d) 1 (ofGroup g_1)
⊢ consRecOn (motive := fun (x : NormalWord d) ↦ Cancels 1 x → NormalWord d)
      (HSMul.hSMul (β := NormalWord d) (↑g : G) (ofGroup g_1))
      (fun (g_2 : G) (a : g_2 ∈ A ∧ Eq (α := Option ℤˣ) none (some (-1))) ↦
        HSMul.hSMul (β := NormalWord d) (↑g : G) (ofGroup g_1))
      (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) (ofGroup g_1)
          (fun (g : G) (a : g ∈ A ∧ Eq (α := Option ℤˣ) none (some (-1))) ↦ ofGroup g_1)
          (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)

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
g : ↥A
g_1 : 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'
this : Cancels 1 ((↑g : G) • cons g_1 u w h1 h2) ↔ Cancels 1 (cons g_1 u w h1 h2)
hcan : Cancels 1 (cons g_1 u w h1 h2)
h :
  ∀ (h : cons g_1 u w h1 h2 = w),
    consRecOn (motive := fun (x : NormalWord d) ↦ Cancels 1 x → NormalWord d) ((↑g : G) • cons g_1 u w h1 h2)
        (fun (g_2 : G) (a : g_2 ∈ A ∧ Eq (α := Option ℤˣ) none (some (-1))) ↦ (↑g : G) • cons g_1 u w h1 h2)
        (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) (cons g_1 u w h1 h2)
            (fun (g : G) (a : g ∈ A ∧ Eq (α := Option ℤˣ) none (some (-1))) ↦ cons g_1 u w h1 h2)
            (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)
pos :
  HSMul.hSMul (α := G) (↑((φ : (a : ↥A) → ↥B) (Subtype.mk (p := fun (x : G) ↦ x ∈ A) ((↑g : G) * g_1) ⋯)) : G) w =
    HSMul.hSMul (α := G) (↑((φ : (a : ↥A) → ↥B) (g * Subtype.mk (p := fun (x : G) ↦ x ∈ A) g_1 ⋯)) : G) w
⊢ HSMul.hSMul (α := G) (↑((φ : (a : ↥A) → ↥B) (Subtype.mk (p := fun (x : G) ↦ x ∈ A) ((↑g : G) * g_1) ⋯)) : G) w =
    HSMul.hSMul (α := G) (↑((φ : (a : ↥A) → ↥B) g) : G)
      (HSMul.hSMul (α := G) (↑((φ : (a : ↥A) → ↥B) (Subtype.mk (p := fun (x : G) ↦ x ∈ A) g_1 ⋯)) : G) w)

Tactic:
rw [← mul_smul, ← Subgroup.coe_mul, ← map_mul φ]

Premises used: Subgroup.coe_mul, map_mul, 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 : ↥A
g_1 : 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'
this : Cancels 1 ((↑g : G) • cons g_1 u w h1 h2) ↔ Cancels 1 (cons g_1 u w h1 h2)
hcan : Cancels 1 (cons g_1 u w h1 h2)
h :
  ∀ (h : cons g_1 u w h1 h2 = w),
    consRecOn (motive := fun (x : NormalWord d) ↦ Cancels 1 x → NormalWord d) ((↑g : G) • cons g_1 u w h1 h2)
        (fun (g_2 : G) (a : g_2 ∈ A ∧ Eq (α := Option ℤˣ) none (some (-1))) ↦ (↑g : G) • cons g_1 u w h1 h2)
        (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) (cons g_1 u w h1 h2)
            (fun (g : G) (a : g ∈ A ∧ Eq (α := Option ℤˣ) none (some (-1))) ↦ cons g_1 u w h1 h2)
            (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)
⊢ HSMul.hSMul (α := G) (↑((φ : (a : ↥A) → ↥B) (Subtype.mk (p := fun (x : G) ↦ x ∈ A) ((↑g : G) * g_1) ⋯)) : G) w =
    HSMul.hSMul (α := G) (↑((φ : (a : ↥A) → ↥B) (g * Subtype.mk (p := fun (x : G) ↦ x ∈ A) g_1 ⋯)) : G) w

Tactic:
rfl
-- 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
neg :
  (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)
      (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:
rw [dif_neg (mt this.1 hcan), dif_neg hcan]

Premises used: mt, dif_neg, Iff.mp
-- 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
neg :
  cons
      (↑((φ : (a : ↥A) → ↥B)
            (((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                    G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                  (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                ((↑g : G) * w.head)).1) :
        G)
      1
      (((↑(((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                      G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                    (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                  ((↑g : G) * w.head)).2 :
            G) *
          w.head⁻¹) •
        w)
      ⋯ ⋯ =
    cons
      (HMul.hMul (α := G) (↑((φ : (a : ↥A) → ↥B) g) : G)
        (↑((φ : (a : ↥A) → ↥B)
              (((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                      G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                    (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                  w.head).1) :
          G))
      1
      (((↑(((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                      G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                    (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                  w.head).2 :
            G) *
          w.head⁻¹) •
        w)
      ⋯ ⋯
⊢ (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)
      (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 +instances only [toSubgroup_neg_one, unitsSMulGroup, toSubgroup_one, toSubgroupEquiv_one,
      SetLike.coe_sort_coe, group_smul_head, mul_inv_rev, ← mul_smul, mul_assoc, inv_mul_cancel,
      mul_one, smul_cons]

Premises used: HNNExtension.toSubgroup_neg_one, SetLike.coe_sort_coe, inv_mul_cancel, mul_assoc, HNNExtension.toSubgroup_one, HNNExtension.NormalWord.group_smul_head, HNNExtension.NormalWord.smul_cons, HNNExtension.toSubgroupEquiv_one, mul_inv_rev, mul_one, HNNExtension.NormalWord.unitsSMulGroup, 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 : ↥A
w : NormalWord d
this : Cancels 1 ((↑g : G) • w) ↔ Cancels 1 w
hcan : ¬Cancels 1 w
neg :
  (↑((φ : (a : ↥A) → ↥B)
          (((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                  G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                (a : G) → ↥A × (↑(d.set 1) : Type u_1))
              ((↑g : G) * w.head)).1) :
      G) =
    HMul.hMul (α := G) (↑((φ : (a : ↥A) → ↥B) g) : G)
      (↑((φ : (a : ↥A) → ↥B)
            (((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                    G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                  (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                w.head).1) :
        G)
neg₁ :
  ((↑(((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                    G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                  (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                ((↑g : G) * w.head)).2 :
          G) *
        w.head⁻¹) •
      w =
    ((↑(((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                    G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                  (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                w.head).2 :
          G) *
        w.head⁻¹) •
      w
⊢ cons
      (↑((φ : (a : ↥A) → ↥B)
            (((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                    G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                  (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                ((↑g : G) * w.head)).1) :
        G)
      1
      (((↑(((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                      G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                    (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                  ((↑g : G) * w.head)).2 :
            G) *
          w.head⁻¹) •
        w)
      ⋯ ⋯ =
    cons
      (HMul.hMul (α := G) (↑((φ : (a : ↥A) → ↥B) g) : G)
        (↑((φ : (a : ↥A) → ↥B)
              (((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                      G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                    (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                  w.head).1) :
          G))
      1
      (((↑(((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                      G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                    (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                  w.head).2 :
            G) *
          w.head⁻¹) •
        w)
      ⋯ ⋯

Tactic:
congr 1
-- 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
erw :
  (↑((φ : (a : ↥A) → ↥B)
        (g *
              ((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,
            ((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).2).1) :
    G)
| (↑((φ : (a : ↥A) → ↥B)
        (((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
              (a : G) → ↥A × (↑(d.set 1) : Type u_1))
            ((↑g : G) * w.head)).1) :
    G)

Tactic:
erw [IsComplement.equiv_mul_left]

Premises used: Subgroup.IsComplement.equiv_mul_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
hcan : ¬Cancels 1 w
neg :
  (↑((φ : (a : ↥A) → ↥B)
          (g *
                ((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,
              ((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).2).1) :
      G) =
    HMul.hMul (α := G) (↑((φ : (a : ↥A) → ↥B) g) : G)
      (↑((φ : (a : ↥A) → ↥B)
            (((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                    G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                  (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                w.head).1) :
        G)
⊢ (↑((φ : (a : ↥A) → ↥B)
          (((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                  G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                (a : G) → ↥A × (↑(d.set 1) : Type u_1))
              ((↑g : G) * w.head)).1) :
      G) =
    HMul.hMul (α := G) (↑((φ : (a : ↥A) → ↥B) g) : G)
      (↑((φ : (a : ↥A) → ↥B)
            (((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                    G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                  (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                w.head).1) :
        G)

Tactic:
conv_lhs => erw [IsComplement.equiv_mul_left]

Premises used: Subgroup.IsComplement.equiv_mul_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
hcan : ¬Cancels 1 w
neg :
  (↑((φ : (a : ↥A) → ↥B)
          (g *
            ((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                  (a : G) → (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1))
                w.head).1)) :
      G) =
    HMul.hMul (α := G) (↑((φ : (a : ↥A) → ↥B) g) : G)
      (↑((φ : (a : ↥A) → ↥B)
            (((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                    G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                  (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                w.head).1) :
        G)
⊢ (↑((φ : (a : ↥A) → ↥B)
          (g *
                ((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,
              ((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).2).1) :
      G) =
    HMul.hMul (α := G) (↑((φ : (a : ↥A) → ↥B) g) : G)
      (↑((φ : (a : ↥A) → ↥B)
            (((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                    G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                  (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                w.head).1) :
        G)

Tactic:
simp_rw [toSubgroup_one]

Premises used: HNNExtension.toSubgroup_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 : ↥A
w : NormalWord d
this : Cancels 1 ((↑g : G) • w) ↔ Cancels 1 w
hcan : ¬Cancels 1 w
⊢ (↑((φ : (a : ↥A) → ↥B)
          (g *
            ((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                  (a : G) → (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1))
                w.head).1)) :
      G) =
    HMul.hMul (α := G) (↑((φ : (a : ↥A) → ↥B) g) : G)
      (↑((φ : (a : ↥A) → ↥B)
            (((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                    G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                  (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                w.head).1) :
        G)

Tactic:
simp only [SetLike.coe_sort_coe, map_mul, Subgroup.coe_mul]

Premises used: SetLike.coe_sort_coe, Subgroup.coe_mul, map_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 : ↥A
w : NormalWord d
this : Cancels 1 ((↑g : G) • w) ↔ Cancels 1 w
hcan : ¬Cancels 1 w
erw :
  ((↑(g *
                ((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,
              ((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).2).2 :
        G) *
      w.head⁻¹) •
    w
| ((↑(((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                  G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                (a : G) → ↥A × (↑(d.set 1) : Type u_1))
              ((↑g : G) * w.head)).2 :
        G) *
      w.head⁻¹) •
    w

Tactic:
erw [IsComplement.equiv_mul_left]

Premises used: Subgroup.IsComplement.equiv_mul_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
hcan : ¬Cancels 1 w
neg :
  ((↑(g *
                  ((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,
                ((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).2).2 :
          G) *
        w.head⁻¹) •
      w =
    ((↑(((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                    G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                  (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                w.head).2 :
          G) *
        w.head⁻¹) •
      w
⊢ ((↑(((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                    G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                  (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                ((↑g : G) * w.head)).2 :
          G) *
        w.head⁻¹) •
      w =
    ((↑(((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                    G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                  (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                w.head).2 :
          G) *
        w.head⁻¹) •
      w

Tactic:
conv_lhs => erw [IsComplement.equiv_mul_left]

Premises used: Subgroup.IsComplement.equiv_mul_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
hcan : ¬Cancels 1 w
⊢ ((↑(g *
                  ((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,
                ((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).2).2 :
          G) *
        w.head⁻¹) •
      w =
    ((↑(((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) ⋯ :
                    G ≃ (↑(↑A : Set G) : Type u_1) × (↑(d.set 1) : Type u_1)) :
                  (a : G) → ↥A × (↑(d.set 1) : Type u_1))
                w.head).2 :
          G) *
        w.head⁻¹) •
      w

Tactic:
rfl
-- 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
H₁ :
  ∀ (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)
⊢ 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)) =
    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 φ)

Tactic:
ext : 1