awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
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' := ⋯ }
a : ↥A
⊢ HMul.hMul (β := ↥S) (Subtype.mk (p := fun (x : HNNExtension G A B φ) ↦ x ∈ S) HNNExtension.t t)
      (((MonoidHom.codRestrict HNNExtension.of S of : G →* ↥S) : (a : G) → ↥S) (↑a : G) : ↥S) =
    ((MonoidHom.codRestrict HNNExtension.of S of : G →* ↥S) : (a : G) → ↥S) (↑((φ : (a : ↥A) → ↥B) a) : G) *
      Subtype.mk (p := fun (x : HNNExtension G A B φ) ↦ x ∈ S) HNNExtension.t t
have a₁ : (↑(HMul.hMul (β := ↥S) (Subtype.mk (p := fun (x : HNNExtension G A B φ) ↦ x ∈ S) HNNExtension.t t)
        (((MonoidHom.codRestrict HNNExtension.of S of : G →* ↥S) : (a : G) → ↥S) (↑a : G) : ↥S)) :
    HNNExtension G A B φ) =
  (↑(((MonoidHom.codRestrict HNNExtension.of S of : G →* ↥S) : (a : G) → ↥S) (↑((φ : (a : ↥A) → ↥B) a) : G) *
        Subtype.mk (p := fun (x : HNNExtension G A B φ) ↦ x ∈ S) HNNExtension.t t) :
    HNNExtension G A B φ)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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) ⋯
⊢ (S.subtype.comp f).comp HNNExtension.of = MonoidHom.comp (MonoidHom.id (HNNExtension G A B φ)) HNNExtension.of
have h : ∀ (x : G),
  Eq (α := HNNExtension G A B φ)
    (((S.subtype.comp f).comp HNNExtension.of : (a : G) → HNNExtension G A B φ) x : HNNExtension G A B φ)
    ((MonoidHom.comp (MonoidHom.id (HNNExtension G A B φ)) HNNExtension.of : (a : G) → HNNExtension G A B φ) x :
      HNNExtension G A B φ)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (hypothesis)
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) ⋯
⊢ motive x
have hf : S.subtype.comp f = MonoidHom.id (HNNExtension G A B φ)
Tactic: have hf : S.subtype.comp f = MonoidHom.id _ :=
    hom_ext (by ext; simp [f]) (by simp [f])
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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 x
have change : motive ((MonoidHom.id (HNNExtension G A B φ) : (a : HNNExtension G A B φ) → HNNExtension G A B φ) x)
Tactic: change motive (MonoidHom.id _ x)
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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 ((MonoidHom.id (HNNExtension G A B φ) : (a : HNNExtension G A B φ) → HNNExtension G A B φ) x)
have rw : motive ((S.subtype.comp f : (a : HNNExtension G A B φ) → HNNExtension G A B φ) x)
Tactic: rw [← hf]
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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
⊢ ↥(toSubgroup A B u) ≃* ↥(toSubgroup A B (-u))
have h : ∀ (x : G), toSubgroup A B u = B
Tactic: convert! φ.symm
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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
⊢ ↥(toSubgroup A B u) ≃* ↥(toSubgroup A B (-u))
have h₁ : ∀ (x : G), toSubgroup A B (-u) = A
Tactic: convert! φ.symm
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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
⊢ ↥(toSubgroup A B u) ≃* ↥(toSubgroup A B (-u))
have h₂ : ↥(toSubgroup A B u) = ↥B → toSubgroup A B u = B
Tactic: convert! φ.symm
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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
⊢ ↥(toSubgroup A B u) ≃* ↥(toSubgroup A B (-u))
have h₃ : ↥(toSubgroup A B (-u)) = ↥A → toSubgroup A B (-u) = A
Tactic: convert! φ.symm
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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
⊢ toSubgroup A B u = B
have h : u = 1 → toSubgroup A B u = B
Tactic: cases Int.units_eq_one_or u
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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
⊢ toSubgroup A B u = B
have h₁ : u = -1 → toSubgroup A B u = B
Tactic: cases Int.units_eq_one_or u
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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
⊢ toSubgroup A B (-u) = A
have h : u = 1 → toSubgroup A B (-u) = A
Tactic: cases Int.units_eq_one_or u
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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
⊢ toSubgroup A B (-u) = A
have h₁ : u = -1 → toSubgroup A B (-u) = A
Tactic: cases Int.units_eq_one_or u
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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
⊢ toSubgroup A B u = B
have h : u = 1 → toSubgroup A B u = B
Tactic: cases Int.units_eq_one_or u
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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
⊢ toSubgroup A B u = B
have h₁ : u = -1 → toSubgroup A B u = B
Tactic: cases Int.units_eq_one_or u
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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
⊢ toSubgroup A B (-u) = A
have h : u = 1 → toSubgroup A B (-u) = A
Tactic: cases Int.units_eq_one_or u
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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
⊢ toSubgroup A B (-u) = A
have h₁ : u = -1 → toSubgroup A B (-u) = A
Tactic: cases Int.units_eq_one_or u
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
u : ℤˣ
a : ↥(toSubgroup A B u)
⊢ (↑((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)
have 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)
Tactic: rcases Int.units_eq_one_or u with rfl | rfl
Cleared hypotheses: u, a
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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)
⊢ (↑((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)
have 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)
Tactic: rcases Int.units_eq_one_or u with rfl | rfl
Cleared hypotheses: u, a
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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)
have inr : (toSubgroupEquiv φ (- -1) : (a : ↥(toSubgroup A B (- -1))) → ↥(toSubgroup A B (- - -1)))
    ((φ.symm : (a : ↥B) → ↥(toSubgroup A B (- -1))) a) =
  a
Tactic: simp only [toSubgroup_neg_one, toSubgroupEquiv_neg_one, SetLike.coe_eq_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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
⊢ Nonempty.{u_1 + 1} (TransversalPair G A B)
have 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)
Tactic: choose t ht using fun u ↦ (toSubgroup A B u).exists_isComplement_right 1
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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
⊢ w = w'
have 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'
Tactic: rcases w with ⟨⟨⟩, _⟩
Cleared hypotheses: w, h1, h2
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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
⊢ { head := head, toList := toList, chain := chain, mem_set := mem_set : NormalWord d } = w'
have 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 }
Tactic: cases w'
Cleared hypotheses: w', h1, h2
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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)
have refine : ∀ y ∈ w.toList.head?, (u, w.head).2 ∈ toSubgroup A B (u, w.head).1 → (u, w.head).1 = y.1
Tactic: refine List.isChain_cons.2 ⟨?_, w.chain⟩
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (hypothesis)
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
⊢ g' ∈ d.set u'
have h'₁ : u' = u ∧ g' = w.head ∨ (u', g') ∈ w.toList
Tactic: simp only [List.mem_cons, Prod.mk.injEq] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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
⊢ g' ∈ d.set u'
have 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'
Tactic: rcases h' with ⟨rfl, rfl⟩ | h'
Cleared hypotheses: u, h1, h2, g', h'
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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'
⊢ g' ∈ d.set u'
have inr : ∀ (h' : (u', g') ∈ w.toList), g' ∈ d.set u'
Tactic: rcases h' with ⟨rfl, rfl⟩ | h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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)
⊢ motive w
have 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 }
Tactic: rcases w with ⟨⟨g, l, chain⟩, mem_set⟩
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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
⊢ motive { head := g, toList := l, chain := chain, mem_set := mem_set }
have 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 }
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 _ _ _)
Cleared hypotheses: g, l, chain, mem_set
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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 }
⊢ motive { head := g, toList := l, chain := chain, mem_set := mem_set }
have 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 }
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 _ _ _)
Cleared hypotheses: g, l, chain, mem_set
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
g : G
⊢ (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
have 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) sorry :
        (a : G) → (↑(↑(toSubgroup A B 1) : Set G) : Type u_1) × (↑(d.set 1) : Type u_1))
      g).2
Tactic: rcases Int.units_eq_one_or u with rfl | rfl
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
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
⊢ (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
have 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)) sorry :
        (a : G) → (↑(↑(toSubgroup A B (-1)) : Set G) : Type u_1) × (↑(d.set (-1)) : Type u_1))
      g).2
Tactic: rcases Int.units_eq_one_or u with rfl | rfl
Cleared hypotheses: u