-- Mathlib/GroupTheory/HNNExtension.lean
theorem prod_smul_empty (w : NormalWord d) :
    (w.prod φ) • empty = w

Proof state:
case cons.h2.h.a
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
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'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
i✝ : ℕ
a✝ : ℤˣ × G
⊢ ((u, (↑⟨1, ⋯⟩)⁻¹ * w.head) :: w.toList)[i✝]? = some a✝ ↔ ((u, w.head) :: w.toList)[i✝]? = some a✝

Tactic:
simp

Result:
no goals

Proof state:
case cons.h2.h.a
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
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'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
i✝ : ℕ
a✝ : ℤˣ × G
⊢ ((u, (↑(⋯.equiv w.head).1)⁻¹ * w.head) :: w.toList)[i✝]? = some a✝ ↔ ((u, w.head) :: w.toList)[i✝]? = some a✝

Tactic:
erw [(d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1]

Result:
case cons.h2.h.a
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
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'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
i✝ : ℕ
a✝ : ℤˣ × G
⊢ ((u, (↑⟨1, ⋯⟩)⁻¹ * w.head) :: w.toList)[i✝]? = some a✝ ↔ ((u, w.head) :: w.toList)[i✝]? = some a✝

Proof state:
case cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
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'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
⊢ ReducedWord.prod φ (cons g u w h1 h2).toReducedWord • empty = cons g u w h1 h2

Tactic:
rw [prod_cons, ← mul_assoc, mul_smul, ih, mul_smul, t_pow_smul_eq_unitsSMul,
  of_smul_eq_smul, unitsSMul]

Result:
case cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
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'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
⊢ (g •
      if h : Cancels u w then unitsSMulWithCancel φ u w h
      else
        let g' := unitsSMulGroup φ d u w.head;
        cons (↑g'.1) u ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯) =
    cons g u w h1 h2

Proof state:
case ofGroup
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g✝ : G
⊢ ReducedWord.prod φ (ofGroup g✝).toReducedWord • empty = ofGroup g✝

Tactic:
simp [ofGroup, ReducedWord.prod, of_smul_eq_smul, group_smul_def]

Result:
no goals

Proof state:
case cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
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'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
⊢ (g •
      let g' := unitsSMulGroup φ d u w.head;
      cons (↑g'.1) u ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯) =
    cons g u w h1 h2

Tactic:
simp only [unitsSMulGroup]

Result:
case cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
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'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
⊢ g • cons (↑((toSubgroupEquiv φ u) (⋯.equiv w.head).1)) u ((↑(⋯.equiv w.head).2 * w.head⁻¹) • w) ⋯ ⋯ = cons g u w h1 h2

Proof state:
case cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
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'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
⊢ (g •
      if h : Cancels u w then unitsSMulWithCancel φ u w h
      else
        let g' := unitsSMulGroup φ d u w.head;
        cons (↑g'.1) u ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯) =
    cons g u w h1 h2

Tactic:
rw [dif_neg (not_cancels_of_cons_hyp u w h2)]

Result:
case cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
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'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
⊢ (g •
      let g' := unitsSMulGroup φ d u w.head;
      cons (↑g'.1) u ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯) =
    cons g u w h1 h2

Proof state:
case cons.h2.h.a
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
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'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
i✝ : ℕ
a✝ : ℤˣ × G
⊢ ((u, ↑(⋯.equiv w.head).2) :: w.toList)[i✝]? = some a✝ ↔ ((u, w.head) :: w.toList)[i✝]? = some a✝

Tactic:
erw [(d.compl _).equiv_snd_eq_inv_mul]

Result:
case cons.h2.h.a
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
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'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
i✝ : ℕ
a✝ : ℤˣ × G
⊢ ((u, (↑(⋯.equiv w.head).1)⁻¹ * w.head) :: w.toList)[i✝]? = some a✝ ↔ ((u, w.head) :: w.toList)[i✝]? = some a✝

Proof state:
case cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
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'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
⊢ g • cons (↑((toSubgroupEquiv φ u) ⟨1, ⋯⟩)) u ((↑(⋯.equiv w.head).2 * w.head⁻¹) • w) ⋯ ⋯ = cons g u w h1 h2

Tactic:
ext <;> simp

Result:
case cons.h2.h.a
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
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'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
i✝ : ℕ
a✝ : ℤˣ × G
⊢ ((u, ↑(⋯.equiv w.head).2) :: w.toList)[i✝]? = some a✝ ↔ ((u, w.head) :: w.toList)[i✝]? = some a✝

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
⊢ ReducedWord.prod φ w.toReducedWord • empty = w

Tactic:
induction w using consRecOn with
| ofGroup => simp [ofGroup, ReducedWord.prod, of_smul_eq_smul, group_smul_def]
| cons g u w h1 h2 ih =>
  rw [prod_cons, ← mul_assoc, mul_smul, ih, mul_smul, t_pow_smul_eq_unitsSMul,
    of_smul_eq_smul, unitsSMul]
  rw [dif_neg (not_cancels_of_cons_hyp u w h2)]
  simp only [unitsSMulGroup]
  simp_rw [SetLike.coe_sort_coe]
  erw [(d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1]
  ext <;> simp
  erw [(d.compl _).equiv_snd_eq_inv_mul]
  simp_rw [SetLike.coe_sort_coe]
  erw [(d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1]
  simp

Result:
no goals