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
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)
⊢ 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)
      ⋯ ⋯
have neg₁ : ((↑(((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) sorry :
                  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) sorry :
                  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
-- 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
g : ↥A
w : NormalWord d
this : Cancels 1 ((↑g : G) • w) ↔ Cancels 1 w
hcan : ¬Cancels 1 w
| (↑((φ : (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)
have erw : (↑((φ : (a : ↥A) → ↥B)
      (g *
            ((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))
                w.head).1,
          ((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))
              w.head).2).1) :
  G)
Tactic: erw [IsComplement.equiv_mul_left]
-- 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
g : ↥A
w : NormalWord d
this : Cancels 1 ((↑g : G) • w) ↔ Cancels 1 w
hcan : ¬Cancels 1 w
⊢ (↑((φ : (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)
have neg : (↑((φ : (a : ↥A) → ↥B)
        (g *
              ((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))
                  w.head).1,
            ((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))
                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) sorry :
                  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]
-- 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
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 := (↑(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)
have neg : (↑((φ : (a : ↥A) → ↥B)
        (g *
          ((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) sorry :
                (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) sorry :
                  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]
-- 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
g : ↥A
w : NormalWord d
this : Cancels 1 ((↑g : G) • w) ↔ Cancels 1 w
hcan : ¬Cancels 1 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
have erw : ((↑(g *
              ((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))
                  w.head).1,
            ((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))
                w.head).2).2 :
      G) *
    w.head⁻¹) •
  w
Tactic: erw [IsComplement.equiv_mul_left]
-- 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
g : ↥A
w : NormalWord d
this : Cancels 1 ((↑g : G) • w) ↔ Cancels 1 w
hcan : ¬Cancels 1 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
have neg : ((↑(g *
                ((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))
                    w.head).1,
              ((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))
                  w.head).2).2 :
        G) *
      w.head⁻¹) •
    w =
  ((↑(((IsComplement.equiv (S := (↑A : Set G)) (T := d.set 1) sorry :
                  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]
-- 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
a : ↥A
⊢ 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 φ)
have 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)
Tactic: ext : 1
-- 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 : ℤˣ
w : NormalWord d
⊢ HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) • w = unitsSMul φ u w
have inl : HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑1 : ℤ) • w = unitsSMul φ 1 w
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 : ℤˣ
w : NormalWord d
inl : HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑1 : ℤ) • w = unitsSMul φ 1 w
⊢ HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) • w = unitsSMul φ u w
have inr : HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑(-1) : ℤ) • w = unitsSMul φ (-1) w
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 : ℤˣ
w : NormalWord d
⊢ ReducedWord.prod φ
      (toReducedWord (d := d)
        (if h : Cancels u w then unitsSMulWithCancel φ u w h
        else
          let g' := unitsSMulGroup φ d u w.head;
          cons (↑g'.1 : G) u (((↑g'.2 : G) * w.head⁻¹) • w) ⋯ ⋯)) =
    HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ w.toReducedWord
have pos : ∀ (hcan : Cancels u w),
  ReducedWord.prod φ (unitsSMulWithCancel φ u w hcan).toReducedWord =
    HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ w.toReducedWord
Tactic: split_ifs with hcan
-- 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 : ℤˣ
w : NormalWord d
pos :
  ∀ (hcan : Cancels u w),
    ReducedWord.prod φ (unitsSMulWithCancel φ u w hcan).toReducedWord =
      HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ w.toReducedWord
⊢ ReducedWord.prod φ
      (toReducedWord (d := d)
        (if h : Cancels u w then unitsSMulWithCancel φ u w h
        else
          let g' := unitsSMulGroup φ d u w.head;
          cons (↑g'.1 : G) u (((↑g'.2 : G) * w.head⁻¹) • w) ⋯ ⋯)) =
    HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ w.toReducedWord
have neg : ∀ (hcan : ¬Cancels u w),
  ReducedWord.prod φ
      (toReducedWord (d := d)
        (let g' := unitsSMulGroup φ d u w.head;
        cons (↑g'.1 : G) u (((↑g'.2 : G) * w.head⁻¹) • w) sorry sorry)) =
    HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ w.toReducedWord
Tactic: split_ifs with hcan
-- 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 : ℤˣ
w : NormalWord d
hcan : Cancels u w
⊢ ReducedWord.prod φ (unitsSMulWithCancel φ u w hcan).toReducedWord =
    HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ w.toReducedWord
have pos : ∀ (g : G) (hcan : Cancels (A := A) (B := B) (d := d) u (ofGroup g)),
  ReducedWord.prod φ (unitsSMulWithCancel φ u (ofGroup g) hcan).toReducedWord =
    HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ (toReducedWord (d := d) (ofGroup g))
Tactic: cases w using consRecOn
Cleared hypotheses: w, hcan
-- 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 : ℤˣ
w : NormalWord d
hcan : Cancels u w
pos :
  ∀ (g : G) (hcan : Cancels (A := A) (B := B) (d := d) u (ofGroup g)),
    ReducedWord.prod φ (unitsSMulWithCancel φ u (ofGroup g) hcan).toReducedWord =
      HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ (toReducedWord (d := d) (ofGroup g))
⊢ ReducedWord.prod φ (unitsSMulWithCancel φ u w hcan).toReducedWord =
    HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ w.toReducedWord
have pos₁ : ∀ (g : G) (u_1 : ℤˣ) (w : NormalWord d) (h1 : w.head ∈ d.set u_1)
  (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u_1 → u_1 = u')
  (hcan : Cancels u (cons g u_1 w h1 h2)),
  (∀ (h : cons g u_1 w h1 h2 = w),
      ReducedWord.prod φ (unitsSMulWithCancel φ u (cons g u_1 w h1 h2) hcan).toReducedWord =
        HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ (cons g u_1 w h1 h2).toReducedWord) →
    ReducedWord.prod φ (unitsSMulWithCancel φ u (cons g u_1 w h1 h2) hcan).toReducedWord =
      HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ (cons g u_1 w h1 h2).toReducedWord
Tactic: cases w using consRecOn
Cleared hypotheses: w, hcan
-- 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
u_1 : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u_1
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u_1 → u_1 = u'
hcan : Cancels u (cons g u_1 w h1 h2)
h :
  ∀ (h : cons g u_1 w h1 h2 = w),
    ReducedWord.prod φ (unitsSMulWithCancel φ u (cons g u_1 w h1 h2) hcan).toReducedWord =
      HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ (cons g u_1 w h1 h2).toReducedWord
⊢ ReducedWord.prod φ (unitsSMulWithCancel φ u (cons g u_1 w h1 h2) hcan).toReducedWord =
    HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) * ReducedWord.prod φ (cons g u_1 w h1 h2).toReducedWord
have pos : ∀ (h1 : w.head ∈ d.set { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := sorry, inv_val := sorry : ℤˣ })
  (h2 :
    ∀ u' ∈ Option.map Prod.fst w.toList.head?,
      w.head ∈ toSubgroup A B { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := sorry, inv_val := sorry : ℤˣ } →
        { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := sorry, inv_val := sorry : ℤˣ } = u')
  (hcan : Cancels u (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := sorry, inv_val := sorry : ℤˣ } w h1 h2)),
  (∀ (h : cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := sorry, inv_val := sorry : ℤˣ } w h1 h2 = w),
      ReducedWord.prod φ
          (unitsSMulWithCancel φ u
              (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := sorry, inv_val := sorry : ℤˣ } w h1 h2)
              hcan).toReducedWord =
        HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) *
          ReducedWord.prod φ
            (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := sorry, inv_val := sorry : ℤˣ } w h1 h2).toReducedWord) →
    ReducedWord.prod φ
        (unitsSMulWithCancel φ u
            (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := sorry, inv_val := sorry : ℤˣ } w h1 h2)
            hcan).toReducedWord =
      HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) *
        ReducedWord.prod φ
          (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := sorry, inv_val := sorry : ℤˣ } w h1 h2).toReducedWord
Tactic: cases hcan.2
Cleared hypotheses: u_1, h1, h2, hcan, h
-- 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
w : NormalWord d
h1 : w.head ∈ d.set { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ }
h2 :
  ∀ u' ∈ Option.map Prod.fst w.toList.head?,
    w.head ∈ toSubgroup A B { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } →
      { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } = u'
hcan : Cancels u (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2)
h :
  ∀ (h : cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2 = w),
    ReducedWord.prod φ
        (unitsSMulWithCancel φ u
            (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2)
            hcan).toReducedWord =
      HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) *
        ReducedWord.prod φ
          (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2).toReducedWord
⊢ ReducedWord.prod φ
      (unitsSMulWithCancel φ u
          (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2)
          hcan).toReducedWord =
    HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) *
      ReducedWord.prod φ
        (cons g { val := -(↑u : ℤ), inv := -(↑u⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2).toReducedWord
have pos : (of : (a : G) → HNNExtension G A B φ)
      (↑((toSubgroupEquiv φ u : (a : ↥(toSubgroup A B u)) → ↥(toSubgroup A B (-u)))
            (Subtype.mk (p := fun (x : G) ↦ x ∈ toSubgroup A B u) g sorry)) :
        G) *
    ReducedWord.prod φ w.toReducedWord =
  HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ) *
    HMul.hMul (α := HNNExtension G A B φ) ((of : (a : G) → HNNExtension G A B φ) g : HNNExtension G A B φ)
      ((HPow.hPow (α := HNNExtension G A B φ) t (↑u : ℤ))⁻¹ * ReducedWord.prod φ w.toReducedWord)
Tactic: simp only [unitsSMulWithCancel, id_eq, consRecOn_cons, prod_group_smul, prod_cons, zpow_neg]
-- 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
g : G
w : NormalWord d
h1 : w.head ∈ d.set { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ }
h2 :
  ∀ u' ∈ Option.map Prod.fst w.toList.head?,
    w.head ∈ toSubgroup A B { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } →
      { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ } = u'
hcan : Cancels (-1) (cons g { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2)
h :
  ∀ (h : cons g { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2 = w),
    ReducedWord.prod φ
        (unitsSMulWithCancel φ (-1)
            (cons g { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2)
            hcan).toReducedWord =
      HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑(-1) : ℤ) *
        ReducedWord.prod φ
          (cons g { val := -(↑(-1) : ℤ), inv := -(↑(-1)⁻¹ : ℤ), val_inv := ⋯, inv_val := ⋯ : ℤˣ } w h1 h2).toReducedWord
⊢ (of : (a : G) → HNNExtension G A B φ)
        (↑((toSubgroupEquiv φ (-1) : (a : ↥(toSubgroup A B (-1))) → ↥(toSubgroup A B (- -1)))
              (Subtype.mk (p := fun (x : G) ↦ x ∈ toSubgroup A B (-1)) g ⋯)) :
          G) *
      ReducedWord.prod φ w.toReducedWord =
    HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑(-1) : ℤ) *
      HMul.hMul (α := HNNExtension G A B φ) ((of : (a : G) → HNNExtension G A B φ) g : HNNExtension G A B φ)
        ((HPow.hPow (α := HNNExtension G A B φ) (β := ℤ) t (↑(-1) : ℤ))⁻¹ * ReducedWord.prod φ w.toReducedWord)
have pos : (of : (a : G) → HNNExtension G A B φ)
      (↑((φ.symm : (a : ↥B) → ↥(toSubgroup A B (- -1))) (Subtype.mk (p := fun (x : G) ↦ x ∈ B) g sorry)) : G) *
    ReducedWord.prod φ w.toReducedWord =
  t⁻¹ *
    HMul.hMul (α := HNNExtension G A B φ) ((of : (a : G) → HNNExtension G A B φ) g : HNNExtension G A B φ)
      (t * ReducedWord.prod φ w.toReducedWord)
Tactic: simp only [toSubgroup_neg_one, toSubgroupEquiv_neg_one, Units.val_neg, Units.val_one,
          Int.reduceNeg, zpow_neg, zpow_one, inv_inv]