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
motive : HNNExtension G A B φ → Prop
x : HNNExtension G A B φ
of : ∀ (g : G), motive ((HNNExtension.of : (a : G) → HNNExtension G A B φ) g)
t : motive HNNExtension.t
mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)
inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹
S : Subgroup (HNNExtension G A B φ) := { carrier := setOf motive, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
f : HNNExtension G A B φ →* ↥S :=
  lift (MonoidHom.codRestrict HNNExtension.of S of)
    (Subtype.mk (p := fun (x : HNNExtension G A B φ) ↦ x ∈ S) HNNExtension.t t) ⋯
hf : S.subtype.comp f = MonoidHom.id (HNNExtension G A B φ)
⊢ motive ((S.subtype.comp f : (a : HNNExtension G A B φ) → HNNExtension G A B φ) x)

Tactic:
(f x).2

Premises used: Set.Mem, setOf, DFunLike.coe, Subtype.property
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
motive : HNNExtension G A B φ → Prop
x : HNNExtension G A B φ
of : ∀ (g : G), motive ((HNNExtension.of : (a : G) → HNNExtension G A B φ) g)
t : motive HNNExtension.t
mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)
inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹
S : Subgroup (HNNExtension G A B φ) := { carrier := setOf motive, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
f : HNNExtension G A B φ →* ↥S :=
  lift (MonoidHom.codRestrict HNNExtension.of S of)
    (Subtype.mk (p := fun (x : HNNExtension G A B φ) ↦ x ∈ S) HNNExtension.t t) ⋯
hf : S.subtype.comp f = MonoidHom.id (HNNExtension G A B φ)
⊢ motive ((S.subtype.comp f : (a : HNNExtension G A B φ) → HNNExtension G A B φ) x)

Tactic:
exact (f x).2

Premises used: DFunLike.coe, Subtype.property
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
⊢ toSubgroup A B 1 = A

Tactic:
rfl

Premises used: HNNExtension.toSubgroup, rfl, ite
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
⊢ toSubgroup A B (-1) = B

Tactic:
rfl

Premises used: HNNExtension.toSubgroup, rfl, ite
-- 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
u : ℤˣ
hu : ¬u = 1
h : ∀ (x : G), toSubgroup A B u = B
h₁ : ∀ (x : G), toSubgroup A B (-u) = A
h₂ : ↥(toSubgroup A B u) = ↥B → toSubgroup A B u = B
h₃ : ↥(toSubgroup A B (-u)) = ↥A → toSubgroup A B (-u) = A
⊢ ↥(toSubgroup A B u) ≃* ↥(toSubgroup A B (-u))

Tactic:
convert! φ.symm

Premises used: MulEquiv.symm
-- 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
u : ℤˣ
hu : ¬u = 1
x : G
h : u = 1 → toSubgroup A B u = B
h₁ : u = -1 → toSubgroup A B u = B
⊢ toSubgroup A B u = B

Tactic:
cases Int.units_eq_one_or u

Premises used: Int.units_eq_one_or
-- 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
u : ℤˣ
hu : ¬u = 1
x : G
h : u = 1 → toSubgroup A B (-u) = A
h₁ : u = -1 → toSubgroup A B (-u) = A
⊢ toSubgroup A B (-u) = A

Tactic:
cases Int.units_eq_one_or u

Premises used: Int.units_eq_one_or
-- 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
u : ℤˣ
hu : ¬u = 1
e_1 : ↥(toSubgroup A B u) = ↥B
h : u = 1 → toSubgroup A B u = B
h₁ : u = -1 → toSubgroup A B u = B
⊢ toSubgroup A B u = B

Tactic:
cases Int.units_eq_one_or u

Premises used: Int.units_eq_one_or
-- 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
u : ℤˣ
hu : ¬u = 1
e_2 : ↥(toSubgroup A B (-u)) = ↥A
h : u = 1 → toSubgroup A B (-u) = A
h₁ : u = -1 → toSubgroup A B (-u) = A
⊢ toSubgroup A B (-u) = A

Tactic:
cases Int.units_eq_one_or u

Premises used: Int.units_eq_one_or
-- 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
u : ℤˣ
hu : ¬u = 1
x : G
h : u = 1
⊢ toSubgroup A B u = B

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
u : ℤˣ
hu : ¬u = 1
x : G
h : u = -1
⊢ toSubgroup A B u = B

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
u : ℤˣ
hu : ¬u = 1
x : G
h : u = 1
⊢ toSubgroup A B (-u) = A

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
u : ℤˣ
hu : ¬u = 1
x : G
h : u = -1
⊢ toSubgroup A B (-u) = A

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
u : ℤˣ
hu : ¬u = 1
e_1 : ↥(toSubgroup A B u) = ↥B
h : u = 1
⊢ toSubgroup A B u = B

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
u : ℤˣ
hu : ¬u = 1
e_1 : ↥(toSubgroup A B u) = ↥B
h : u = -1
⊢ toSubgroup A B u = B

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
u : ℤˣ
hu : ¬u = 1
e_2 : ↥(toSubgroup A B (-u)) = ↥A
h : u = 1
⊢ toSubgroup A B (-u) = A

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
u : ℤˣ
hu : ¬u = 1
e_2 : ↥(toSubgroup A B (-u)) = ↥A
h : u = -1
⊢ toSubgroup A B (-u) = A

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
⊢ toSubgroupEquiv φ 1 = φ

Tactic:
rfl

Premises used: HNNExtension.toSubgroupEquiv, dite, rfl
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
⊢ toSubgroupEquiv φ (-1) = φ.symm

Tactic:
rfl

Premises used: Eq.mpr, Set.Mem, HNNExtension.toSubgroupEquiv, HNNExtension.toSubgroup, MulEquiv.symm, rfl, ite
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
u : ℤˣ
a : ↥(toSubgroup A B u)
inl :
  ∀ (a : ↥(toSubgroup A B 1)),
    (↑((toSubgroupEquiv φ (-1) : (a : ↥(toSubgroup A B (-1))) → ↥(toSubgroup A B (- -1)))
            ((toSubgroupEquiv φ 1 : (a : ↥(toSubgroup A B 1)) → ↥(toSubgroup A B (-1))) a)) :
        G) =
      (↑a : G)
inr :
  ∀ (a : ↥(toSubgroup A B (-1))),
    (↑((toSubgroupEquiv φ (- -1) : (a : ↥(toSubgroup A B (- -1))) → ↥(toSubgroup A B (- - -1)))
            ((toSubgroupEquiv φ (-1) : (a : ↥(toSubgroup A B (-1))) → ↥(toSubgroup A B (- -1))) a)) :
        G) =
      (↑a : G)
⊢ (↑((toSubgroupEquiv φ (-u) : (a : ↥(toSubgroup A B (-u))) → ↥(toSubgroup A B (- -u)))
          ((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u))) a)) :
      G) =
    (↑a : G)

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
a : ↥(toSubgroup A B 1)
⊢ (↑((toSubgroupEquiv φ (-1) : (a : ↥(toSubgroup A B (-1))) → ↥(toSubgroup A B (- -1)))
          ((toSubgroupEquiv φ 1 : (a : ↥(toSubgroup A B 1)) → ↥(toSubgroup A B (-1))) a)) :
      G) =
    (↑a : G)

Tactic:
simp [toSubgroup]

Premises used: HNNExtension.toSubgroup
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥(toSubgroup A B (-1))
inr :
  (toSubgroupEquiv φ (- -1) : (a : ↥(toSubgroup A B (- -1))) → ↥(toSubgroup A B (- - -1)))
      ((φ.symm : (a : ↥B) → ↥(toSubgroup A B (- -1))) a) =
    a
⊢ (↑((toSubgroupEquiv φ (- -1) : (a : ↥(toSubgroup A B (- -1))) → ↥(toSubgroup A B (- - -1)))
          ((toSubgroupEquiv φ (-1) : (a : ↥(toSubgroup A B (-1))) → ↥(toSubgroup A B (- -1))) a)) :
      G) =
    (↑a : G)

Tactic:
simp only [toSubgroup_neg_one, toSubgroupEquiv_neg_one, SetLike.coe_eq_coe]

Premises used: HNNExtension.toSubgroup_neg_one, HNNExtension.toSubgroupEquiv_neg_one, SetLike.coe_eq_coe
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥(toSubgroup A B (-1))
⊢ (toSubgroupEquiv φ (- -1) : (a : ↥(toSubgroup A B (- -1))) → ↥(toSubgroup A B (- - -1)))
      ((φ.symm : (a : ↥B) → ↥(toSubgroup A B (- -1))) a) =
    a

Tactic:
φ.apply_symm_apply a

Premises used: Set.Mem, Int.neg, MulEquiv.apply_symm_apply
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥(toSubgroup A B (-1))
⊢ (toSubgroupEquiv φ (- -1) : (a : ↥(toSubgroup A B (- -1))) → ↥(toSubgroup A B (- - -1)))
      ((φ.symm : (a : ↥B) → ↥(toSubgroup A B (- -1))) a) =
    a

Tactic:
exact φ.apply_symm_apply a

Premises used: MulEquiv.apply_symm_apply
-- 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
choose :
  ∀ (t : (u : ℤˣ) → Set G) (ht : ∀ (u : ℤˣ), IsComplement (↑(toSubgroup A B u) : Set G) (t u) ∧ 1 ∈ t u),
    Nonempty.{u_1 + 1} (TransversalPair G A B)
⊢ Nonempty.{u_1 + 1} (TransversalPair G A B)

Tactic:
choose t ht using fun u ↦ (toSubgroup A B u).exists_isComplement_right 1

Premises used: HNNExtension.t, HNNExtension.toSubgroup, OfNat.ofNat, Subgroup.exists_isComplement_right
-- 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
t : (u : ℤˣ) → Set G
ht : ∀ (u : ℤˣ), IsComplement (↑(toSubgroup A B u) : Set G) (t u) ∧ 1 ∈ t u
⊢ Nonempty.{u_1 + 1} (TransversalPair G A B)

Tactic:
⟨⟨t, fun i ↦ (ht i).1⟩⟩

Premises used: HNNExtension.NormalWord.TransversalPair.mk, Nonempty.intro, And.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
t : (u : ℤˣ) → Set G
ht : ∀ (u : ℤˣ), IsComplement (↑(toSubgroup A B u) : Set G) (t u) ∧ 1 ∈ t u
⊢ Nonempty.{u_1 + 1} (TransversalPair G A B)

Tactic:
exact ⟨⟨t, fun i ↦ (ht i).1⟩⟩
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
d : TransversalPair G A B
w w' : NormalWord d
h1 : w.head = w'.head
h2 : w.toList = w'.toList
rcases :
  ∀ (head : G) (toList : List (ℤˣ × G))
    (chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) toList)
    (mem_set :
      ∀ (u : ℤˣ) (g : G),
        (u, g) ∈ { head := head, toList := toList, chain := chain : ReducedWord G A B }.toList → g ∈ d.set u)
    (h1 : { head := head, toList := toList, chain := chain, mem_set := mem_set : NormalWord d }.head = w'.head)
    (h2 : { head := head, toList := toList, chain := chain, mem_set := mem_set : NormalWord d }.toList = w'.toList),
    { head := head, toList := toList, chain := chain, mem_set := mem_set : NormalWord d } = w'
⊢ w = w'

Tactic:
rcases w with ⟨⟨⟩, _⟩
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
d : TransversalPair G A B
w' : NormalWord d
head : G
toList : List (ℤˣ × G)
chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) toList
mem_set :
  ∀ (u : ℤˣ) (g : G),
    (u, g) ∈ { head := head, toList := toList, chain := chain : ReducedWord G A B }.toList → g ∈ d.set u
h1 : { head := head, toList := toList, chain := chain, mem_set := mem_set : NormalWord d }.head = w'.head
h2 : { head := head, toList := toList, chain := chain, mem_set := mem_set : NormalWord d }.toList = w'.toList
mk :
  ∀ (toReducedWord : ReducedWord G A B) (mem_set_1 : ∀ (u : ℤˣ) (g : G), (u, g) ∈ toReducedWord.toList → g ∈ d.set u)
    (h1 :
      { head := head, toList := toList, chain := chain, mem_set := mem_set : NormalWord d }.head =
        { toReducedWord := toReducedWord, mem_set := mem_set_1 : NormalWord d }.head)
    (h2 :
      { head := head, toList := toList, chain := chain, mem_set := mem_set : NormalWord d }.toList =
        { toReducedWord := toReducedWord, mem_set := mem_set_1 : NormalWord d }.toList),
    { head := head, toList := toList, chain := chain, mem_set := mem_set : NormalWord d } =
      { toReducedWord := toReducedWord, mem_set := mem_set_1 }
⊢ { head := head, toList := toList, chain := chain, mem_set := mem_set : NormalWord d } = w'

Tactic:
cases w'
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
d : TransversalPair G A B
head : G
toList : List (ℤˣ × G)
chain : List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) toList
mem_set :
  ∀ (u : ℤˣ) (g : G),
    (u, g) ∈ { head := head, toList := toList, chain := chain : ReducedWord G A B }.toList → g ∈ d.set u
toReducedWord : ReducedWord G A B
mem_set_1 : ∀ (u : ℤˣ) (g : G), (u, g) ∈ toReducedWord.toList → g ∈ d.set u
h1 :
  { head := head, toList := toList, chain := chain, mem_set := mem_set : NormalWord d }.head =
    { toReducedWord := toReducedWord, mem_set := mem_set_1 : NormalWord d }.head
h2 :
  { head := head, toList := toList, chain := chain, mem_set := mem_set : NormalWord d }.toList =
    { toReducedWord := toReducedWord, mem_set := mem_set_1 : NormalWord d }.toList
⊢ { head := head, toList := toList, chain := chain, mem_set := mem_set : NormalWord d } =
    { toReducedWord := toReducedWord, mem_set := mem_set_1 }

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 : ℤˣ) (g : G), Membership.mem (γ := List (ℤˣ × G)) [] (u, g) → g ∈ 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
g : G
⊢ ∀ (u : ℤˣ) (g : G), Membership.mem (γ := List (ℤˣ × G)) [] (u, g) → g ∈ 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
⊢ ∀ (x y : G) (b : NormalWord d), (x * y) • b = x • y • b

Tactic:
simp +instances [instHSMul, mul_assoc]

Premises used: instHSMul, mul_assoc
-- 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
⊢ ∀ (b : NormalWord d), HSMul.hSMul (α := G) 1 b = b

Tactic:
simp +instances [instHSMul]

Premises used: instHSMul
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
d : TransversalPair G A B
g : G
w : NormalWord d
⊢ g • w = { head := g * w.head, toList := w.toList, chain := ⋯, mem_set := ⋯ }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
d : TransversalPair G A B
g : G
w : NormalWord d
⊢ (g • w).head = g * w.head

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
d : TransversalPair G A B
g : G
w : NormalWord d
⊢ (g • w).toList = w.toList

Tactic:
rfl

Premises used: 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
⊢ ∀ {m₁ m₂ : G}, (∀ (a : NormalWord d), m₁ • a = m₂ • a) → m₁ = m₂

Tactic:
simp [group_smul_def]

Premises used: HNNExtension.NormalWord.group_smul_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
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'
⊢ List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) ((u, w.head) :: w.toList)

Tactic:
List.isChain_cons.2 ⟨?_, w.chain⟩

Premises used: Iff.mpr, HNNExtension.NormalWord.ReducedWord.chain, HNNExtension.NormalWord.toReducedWord, List.isChain_cons, And.intro
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst_1 : Group H
M : Type u_3
inst_2 : Monoid M
d : TransversalPair G A B
g : 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'
refine : ∀ y ∈ w.toList.head?, (u, w.head).2 ∈ toSubgroup A B (u, w.head).1 → (u, w.head).1 = y.1
⊢ List.IsChain (fun (a b : ℤˣ × G) ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) ((u, w.head) :: w.toList)

Tactic:
refine List.isChain_cons.2 ⟨?_, w.chain⟩

Premises used: Iff.mpr, HNNExtension.NormalWord.ReducedWord.chain, HNNExtension.NormalWord.toReducedWord, List.isChain_cons, And.intro
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst_1 : Group H
M : Type u_3
inst_2 : Monoid M
d : TransversalPair G A B
g : 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'
u' : ℤˣ
g' : G
hu' : (u', g') ∈ w.toList.head?
hw1 : (u, w.head).2 ∈ toSubgroup A B (u, w.head).1
⊢ (u', g').1 ∈ Option.map Prod.fst w.toList.head?

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
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'
u' : ℤˣ
g' : G
hu' : (u', g') ∈ w.toList.head?
hw1 : (u, w.head).2 ∈ toSubgroup A B (u, w.head).1
⊢ (u, w.head).1 = (u', g').1

Tactic:
exact h2 _ (by simp_all) hw1
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst_1 : Group H
M : Type u_3
inst_2 : Monoid M
d : TransversalPair G A B
g : 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'
u' : ℤˣ
g' : G
h' : (u', g') ∈ (u, w.head) :: w.toList
⊢ u' = u ∧ g' = w.head ∨ (u', g') ∈ w.toList

Tactic:
simp only [List.mem_cons, Prod.mk.injEq] at h'

Premises used: Prod.mk.injEq, List.mem_cons
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst_1 : Group H
M : Type u_3
inst_2 : Monoid M
d : TransversalPair G A B
g : 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'
u' : ℤˣ
g' : G
h' : u' = u ∧ g' = w.head ∨ (u', g') ∈ w.toList
inl :
  ∀ (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),
    w.head ∈ d.set u'
inr : ∀ (h' : (u', g') ∈ w.toList), g' ∈ d.set u'
⊢ g' ∈ d.set u'

Tactic:
rcases h' with ⟨rfl, rfl⟩ | h'

Premises used: 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
g : G
w : NormalWord d
u' : ℤˣ
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
⊢ w.head ∈ d.set u'

Tactic:
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
g : G
w : NormalWord d
u' : ℤˣ
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
⊢ w.head ∈ d.set u'

Tactic:
exact 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
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'
u' : ℤˣ
g' : G
h' : (u', g') ∈ w.toList
⊢ g' ∈ d.set u'

Tactic:
w.mem_set _ _ h'

Premises used: HNNExtension.NormalWord.mem_set
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst_1 : Group H
M : Type u_3
inst_2 : Monoid M
d : TransversalPair G A B
g : 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'
u' : ℤˣ
g' : G
h' : (u', g') ∈ w.toList
⊢ g' ∈ d.set u'

Tactic:
exact w.mem_set _ _ h'

Premises used: HNNExtension.NormalWord.mem_set
-- 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
w : NormalWord d
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)
rcases :
  (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) →
          motive { head := g, toList := l, chain := chain, mem_set := mem_set }
⊢ motive w

Tactic:
rcases w with ⟨⟨g, l, chain⟩, mem_set⟩

Premises used: HNNExtension.NormalWord.mem_set
-- 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
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 }

Tactic:
exact ofGroup _