awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst_1 : Group H
M : Type u_3
inst_2 : Monoid M
d : TransversalPair G A B
motive : NormalWord d → Sort u_4
ofGroup : (g : G) → motive (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') →
            motive w → motive (NormalWord.cons g u w h1 h2)
a : ℤˣ × G
l : List (ℤˣ × G)
ih :
  (g : G) →
    (chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) l) →
      (mem_set :
          ∀ (u : ℤˣ) (g_1 : G),
            (u, g_1) ∈ { head := g, toList := l, chain := chain : ReducedWord G A B }.toList → g_1 ∈ d.set u) →
        motive { head := g, toList := l, chain := chain, mem_set := mem_set }
g : G
chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)
mem_set :
  ∀ (u : ℤˣ) (g_1 : G),
    (u, g_1) ∈ { head := g, toList := a :: l, chain := chain : ReducedWord G A B }.toList → g_1 ∈ d.set u
⊢ ∀
    u' ∈
      Option.map Prod.fst
        (toReducedWord (d := d) { head := a.2, toList := l, chain := ⋯, mem_set := ⋯ : NormalWord d }).toList.head?,
    (toReducedWord (d := d) { head := a.2, toList := l, chain := ⋯, mem_set := ⋯ : NormalWord d }).head ∈
        toSubgroup A B a.1 →
      a.1 = u'

Tactic:
simpa using (List.isChain_cons.1 chain).1

Premises used: And.left, List.isChain_cons, Iff.mp
-- 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
motive : NormalWord d → Sort u_4
ofGroup : (g : G) → motive (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') →
            motive w → motive (NormalWord.cons g u w h1 h2)
a : ℤˣ × G
l : List (ℤˣ × G)
ih :
  (g : G) →
    (chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) l) →
      (mem_set :
          ∀ (u : ℤˣ) (g_1 : G),
            (u, g_1) ∈ { head := g, toList := l, chain := chain : ReducedWord G A B }.toList → g_1 ∈ d.set u) →
        motive { head := g, toList := l, chain := chain, mem_set := mem_set }
g : G
chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)
mem_set :
  ∀ (u : ℤˣ) (g_1 : G),
    (u, g_1) ∈ { head := g, toList := a :: l, chain := chain : ReducedWord G A B }.toList → g_1 ∈ d.set u
⊢ motive { head := g, toList := a :: l, chain := chain, mem_set := mem_set }

Tactic:
exact cons g a.1
      { head := a.2
        toList := l
        mem_set := fun _ _ h => mem_set _ _ (List.mem_cons_of_mem _ h),
        chain := (List.isChain_cons.1 chain).2 }
      (mem_set a.1 a.2 List.mem_cons_self)
      (by simpa using (List.isChain_cons.1 chain).1)
      (ih _ _ _)

Premises used: HNNExtension.NormalWord.mk, List.mem_cons_of_mem, Prod.fst, And.right, List.isChain_cons, Iff.mp, List.mem_cons_self, HNNExtension.NormalWord.ReducedWord.mk, Prod.snd
-- 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
motive : NormalWord d → Sort u_4
ofGroup : (g : G) → motive (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') →
            motive w → motive (NormalWord.cons g u w h1 h2)
g : G
l : List (ℤˣ × G)
chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) l
mem_set :
  ∀ (u : ℤˣ) (g_1 : G), (u, g_1) ∈ { head := g, toList := l, chain := chain : ReducedWord G A B }.toList → g_1 ∈ d.set u
nil :
  (g : G) →
    (chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) []) →
      (mem_set :
          ∀ (u : ℤˣ) (g_1 : G),
            (u, g_1) ∈ { head := g, toList := [], chain := chain : ReducedWord G A B }.toList → g_1 ∈ d.set u) →
        motive { head := g, toList := [], chain := chain, mem_set := mem_set }
cons₁ :
  (a : ℤˣ × G) →
    (l : List (ℤˣ × G)) →
      (ih :
          (g : G) →
            (chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) l) →
              (mem_set :
                  ∀ (u : ℤˣ) (g_1 : G),
                    (u, g_1) ∈ { head := g, toList := l, chain := chain : ReducedWord G A B }.toList → g_1 ∈ d.set u) →
                motive { head := g, toList := l, chain := chain, mem_set := mem_set }) →
        (g : G) →
          (chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)) →
            (mem_set :
                ∀ (u : ℤˣ) (g_1 : G),
                  (u, g_1) ∈ { head := g, toList := a :: l, chain := chain : ReducedWord G A B }.toList →
                    g_1 ∈ d.set u) →
              motive { head := g, toList := a :: l, chain := chain, mem_set := mem_set }
⊢ motive { head := g, toList := l, chain := chain, mem_set := mem_set }

Tactic:
induction l generalizing g with
  | nil => exact ofGroup _
  | cons a l ih =>
    exact cons g a.1
      { head := a.2
        toList := l
        mem_set := fun _ _ h => mem_set _ _ (List.mem_cons_of_mem _ h),
        chain := (List.isChain_cons.1 chain).2 }
      (mem_set a.1 a.2 List.mem_cons_self)
      (by simpa using (List.isChain_cons.1 chain).1)
      (ih _ _ _)
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
d : TransversalPair G A B
motive : NormalWord d → Sort u_4
g : G
ofGroup : (g : G) → motive (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') →
            motive w → motive (NormalWord.cons g u w h1 h2)
⊢ consRecOn (motive := fun (x : NormalWord d) ↦ motive x) (NormalWord.ofGroup g) ofGroup cons = ofGroup g

Tactic:
rfl

Premises used: HNNExtension.NormalWord.consRecOn, rfl
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
d : TransversalPair G A B
motive : NormalWord d → Sort u_4
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'
ofGroup : (g : G) → motive (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') →
            motive w → motive (NormalWord.cons g u w h1 h2)
⊢ consRecOn (motive := fun (x : NormalWord d) ↦ motive x) (NormalWord.cons g u w h1 h2) ofGroup cons =
    cons g u w h1 h2 (consRecOn (motive := fun (x : NormalWord d) ↦ motive x) w ofGroup cons)

Tactic:
rfl

Premises used: HNNExtension.NormalWord.consRecOn, rfl
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
d : TransversalPair G A B
g₁ 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'
⊢ g₁ • cons g₂ u w h1 h2 = cons (g₁ * g₂) u w h1 h2

Tactic:
rfl

Premises used: HNNExtension.NormalWord.cons, rfl
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
d : TransversalPair G A B
g₁ g₂ : G
⊢ HSMul.hSMul (β := NormalWord d) g₁ (ofGroup g₂) = ofGroup (g₁ * g₂)

Tactic:
rfl

Premises used: HNNExtension.NormalWord.ofGroup, rfl
-- 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
inl :
  Eq (α := (↑(d.set 1) : Type u_1)) (unitsSMulGroup φ d 1 g).2
    ((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))
        g).2
inr :
  Eq (α := (↑(d.set (-1)) : Type u_1)) (unitsSMulGroup φ d (-1) g).2
    ((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))
        g).2
⊢ (unitsSMulGroup φ d u g).2 =
    ((⋯.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))
        g).2

Tactic:
rcases Int.units_eq_one_or u with rfl | rfl

Premises used: Int.units_eq_one_or, rfl
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
⊢ Eq (α := (↑(d.set 1) : Type u_1)) (unitsSMulGroup φ d 1 g).2
    ((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))
        g).2

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 : G
⊢ Eq (α := (↑(d.set (-1)) : Type u_1)) (unitsSMulGroup φ d (-1) g).2
    ((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))
        g).2

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
u : ℤˣ
w : NormalWord d
simp : (g : G) → g ∈ toSubgroup A B u ∧ none = some (-u) → NormalWord d
⊢ (g : G) → Cancels (A := A) (B := B) (d := d) u (ofGroup g) → NormalWord d

Tactic:
simp [Cancels, ofGroup]

Premises used: HNNExtension.NormalWord.ofGroup, HNNExtension.NormalWord.Cancels
-- 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
u : ℤˣ
w : NormalWord d
tauto tauto₁ tauto₂ : (g : G) → g ∈ toSubgroup A B u ∧ none = some (-u) → NormalWord d
⊢ (g : G) → g ∈ toSubgroup A B u ∧ none = some (-u) → NormalWord d

Tactic:
tauto
-- 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
u : ℤˣ
w : NormalWord d
this : (p : Prop) → Decidable p := Classical.dec
h : ¬Cancels u w
g' : ↥(toSubgroup A B (-u)) × (↑(d.set u) : Type u_1) := unitsSMulGroup φ d u w.head
⊢ (((↑g'.2 : G) * w.head⁻¹) • w).head ∈ d.set u

Tactic:
simp
-- 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
u : ℤˣ
w : NormalWord d
this : (p : Prop) → Decidable p := Classical.dec
h : ¬Cancels u w
g' : ↥(toSubgroup A B (-u)) × (↑(d.set u) : Type u_1) := unitsSMulGroup φ d u w.head
simp :
  ∀ (u' : ℤˣ) (x : G) (h : w.toList.head? = some (u', x)),
    (↑((⋯.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).2 :
          G) ∈
        toSubgroup A B u →
      u = u'
⊢ ∀ u' ∈ Option.map Prod.fst (((↑g'.2 : G) * w.head⁻¹) • w).toList.head?,
    (((↑g'.2 : G) * w.head⁻¹) • w).head ∈ toSubgroup A B u → u = u'

Tactic:
simp only [g', group_smul_toList, Option.mem_def, Option.map_eq_some_iff, Prod.exists,
          exists_and_right, exists_eq_right, group_smul_head, inv_mul_cancel_right,
          forall_exists_index, unitsSMulGroup]

Premises used: HNNExtension.NormalWord.group_smul_toList, forall_exists_index, exists_eq_right, exists_and_right, HNNExtension.NormalWord.group_smul_head, HNNExtension.NormalWord.unitsSMulGroup, Prod.exists, inv_mul_cancel_right, Option.map_eq_some_iff, Option.mem_def
-- 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
u : ℤˣ
w : NormalWord d
this : (p : Prop) → Decidable p := Classical.dec
h : ¬Cancels u w
g' : ↥(toSubgroup A B (-u)) × (↑(d.set u) : Type u_1) := unitsSMulGroup φ d u w.head
⊢ w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)

Tactic:
simp only [Cancels, Option.map_eq_some_iff, Prod.exists, exists_and_right, exists_eq_right,
          not_and, not_exists] at h

Premises used: HNNExtension.NormalWord.Cancels, not_exists, exists_eq_right, exists_and_right, Prod.exists, not_and, Option.map_eq_some_iff
-- 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
u : ℤˣ
w : NormalWord d
this : (p : Prop) → Decidable p := Classical.dec
g' : ↥(toSubgroup A B (-u)) × (↑(d.set u) : Type u_1) := unitsSMulGroup φ d u w.head
h : w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
u' : ℤˣ
x : G
hx : w.toList.head? = some (u', x)
hmem :
  (↑((⋯.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).2 :
      G) ∈
    toSubgroup A B u
⊢ RightCosetEquivalence (↑(toSubgroup A B u) : Set G) w.head
    (↑((⋯.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).2 :
      G)

Tactic:
have := (d.compl u).rightCosetEquivalence_equiv_snd w.head
-- 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
u : ℤˣ
w : NormalWord d
this_1 : (p : Prop) → Decidable p := Classical.dec
g' : ↥(toSubgroup A B (-u)) × (↑(d.set u) : Type u_1) := unitsSMulGroup φ d u w.head
h : w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
u' : ℤˣ
x : G
hx : w.toList.head? = some (u', x)
hmem :
  (↑((⋯.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).2 :
      G) ∈
    toSubgroup A B u
this :
  RightCosetEquivalence (↑(toSubgroup A B u) : Set G) w.head
    (↑((⋯.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).2 :
      G)
⊢ w.head⁻¹ ∈ toSubgroup A B u

Tactic:
rw [RightCosetEquivalence, rightCoset_eq_iff, mul_mem_cancel_left hmem] at this

Premises used: rightCoset_eq_iff, RightCosetEquivalence, mul_mem_cancel_left
-- 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
u : ℤˣ
w : NormalWord d
this_1 : (p : Prop) → Decidable p := Classical.dec
g' : ↥(toSubgroup A B (-u)) × (↑(d.set u) : Type u_1) := unitsSMulGroup φ d u w.head
h : w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
u' : ℤˣ
x : G
hx : w.toList.head? = some (u', x)
hmem :
  (↑((⋯.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).2 :
      G) ∈
    toSubgroup A B u
this : w.head⁻¹ ∈ toSubgroup A B u
⊢ w.head ∈ toSubgroup A B u

Tactic:
simp_all
-- 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
u : ℤˣ
w : NormalWord d
this : (p : Prop) → Decidable p := Classical.dec
g' : ↥(toSubgroup A B (-u)) × (↑(d.set u) : Type u_1) := unitsSMulGroup φ d u w.head
h : w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
u' : ℤˣ
x : G
hx : w.toList.head? = some (u', x)
hmem :
  (↑((⋯.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).2 :
      G) ∈
    toSubgroup A B u
⊢ w.head ∈ toSubgroup A B u

Tactic:
have : w.head ∈ toSubgroup A B u := by
          have := (d.compl u).rightCosetEquivalence_equiv_snd w.head
          rw [RightCosetEquivalence, rightCoset_eq_iff, mul_mem_cancel_left hmem] at this
          simp_all
-- 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
u : ℤˣ
w : NormalWord d
this_1 : (p : Prop) → Decidable p := Classical.dec
g' : ↥(toSubgroup A B (-u)) × (↑(d.set u) : Type u_1) := unitsSMulGroup φ d u w.head
h : w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
u' : ℤˣ
x : G
hx : w.toList.head? = some (u', x)
hmem :
  (↑((⋯.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).2 :
      G) ∈
    toSubgroup A B u
this : w.head ∈ toSubgroup A B u
⊢ ¬w.toList.head? = some (-u, x)

Tactic:
have := h this x
-- 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
u : ℤˣ
w : NormalWord d
this_1 : (p : Prop) → Decidable p := Classical.dec
g' : ↥(toSubgroup A B (-u)) × (↑(d.set u) : Type u_1) := unitsSMulGroup φ d u w.head
h : w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
u' : ℤˣ
x : G
hx : w.toList.head? = some (u', x)
hmem :
  (↑((⋯.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).2 :
      G) ∈
    toSubgroup A B u
this_2 : w.head ∈ toSubgroup A B u
this : ¬w.toList.head? = some (-u, x)
⊢ u = u'

Tactic:
simp_all [Int.units_ne_iff_eq_neg]

Premises used: Int.units_ne_iff_eq_neg
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
simp : w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
⊢ ¬Cancels u w

Tactic:
simp only [Cancels, Option.map_eq_some_iff, Prod.exists,
    exists_and_right, exists_eq_right, not_and, not_exists]

Premises used: HNNExtension.NormalWord.Cancels, not_exists, exists_eq_right, exists_and_right, Prod.exists, not_and, Option.map_eq_some_iff
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
hw : w.head ∈ toSubgroup A B u
x : G
hx : w.toList.head? = some (-u, x)
⊢ ∀ u' ∈ Option.map Prod.fst (some (-u, x)), w.head ∈ toSubgroup A B u → u = u'

Tactic:
rw [hx] at h2
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
hw : w.head ∈ toSubgroup A B u
x : G
hx : w.toList.head? = some (-u, x)
h2₁ : ∀ u' ∈ Option.map Prod.fst (some (-u, x)), w.head ∈ toSubgroup A B u → u = u'
⊢ w.toList.head? = some (-u, x)

Tactic:
rw [hx] at h2
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hw : w.head ∈ toSubgroup A B u
x : G
h2 : ∀ u' ∈ Option.map Prod.fst (some (-u, x)), w.head ∈ toSubgroup A B u → u = u'
hx : w.toList.head? = some (-u, x)
⊢ False

Tactic:
simpa using h2 (-u) rfl hw

Premises used: Neg.neg, rfl
-- 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 : ∀ (h : Cancels u w), Cancels (-u) (unitsSMul φ u w) ↔ ¬Cancels u w
neg : ∀ (h : ¬Cancels u w), Cancels (-u) (unitsSMul φ u w) ↔ ¬Cancels u w
⊢ Cancels (-u) (unitsSMul φ u w) ↔ ¬Cancels u w

Tactic:
by_cases h : Cancels u w

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
h : Cancels u w
pos : ¬Cancels (-u) (unitsSMulWithCancel φ u w ⋯)
⊢ Cancels (-u) (unitsSMul φ u w) ↔ ¬Cancels u w

Tactic:
simp only [unitsSMul, h, dite_true, not_true_eq_false, iff_false]

Premises used: iff_false, not_true_eq_false, HNNExtension.NormalWord.unitsSMul, dite_true
-- 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
h : Cancels (A := A) (B := B) (d := d) u (ofGroup g)
⊢ ¬Cancels (-u) (unitsSMulWithCancel φ u (ofGroup g) ⋯)

Tactic:
simp [Cancels, unitsSMulWithCancel]

Premises used: HNNExtension.NormalWord.Cancels, 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 : ℤˣ
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_1 : ∀ (h : Cancels u w), ¬Cancels (-u) (unitsSMulWithCancel φ u w ⋯)
h : Cancels u (cons g u' w h1 h2)
hc : Cancels (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) ⋯)
pos : Cancels u' w
⊢ False

Tactic:
apply not_cancels_of_cons_hyp _ _ h2

Premises used: 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
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
h_1 : ∀ (h : Cancels u w), ¬Cancels (-u) (unitsSMulWithCancel φ u w ⋯)
h : Cancels u (cons g u' w h1 h2)
hc : Cancels (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) ⋯)
⊢ g ∈ toSubgroup A B u ∧ u' = -u

Tactic:
simp only [Cancels, cons_head, cons_toList, List.head?_cons,
        Option.map_some, Option.some.injEq] at h

Premises used: HNNExtension.NormalWord.Cancels, Option.some.injEq, List.head?_cons, Option.map_some, HNNExtension.NormalWord.cons_toList, 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 : ℤˣ
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_1 : ∀ (h : Cancels u w), ¬Cancels (-u) (unitsSMulWithCancel φ u w ⋯)
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
pos :
  ∀ (h1 : w.head ∈ d.set (-u)) (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B (-u) → -u = u')
    (h : 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
⊢ Cancels u' w

Tactic:
cases h.2

Premises used: And.right