-- Mathlib/GroupTheory/HNNExtension.lean
theorem unitsSMul_cancels_iff (u : ℤˣ) (w : NormalWord d) :
    Cancels (-u) (unitsSMul φ u w) ↔ ¬ Cancels u w

Proof state:
case pos.cons.refl
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
g : G
w : NormalWord d
a✝ : ∀ (h : Cancels u w), ¬Cancels (-u) (unitsSMulWithCancel φ u w ⋯)
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

Tactic:
simpa [Cancels, unitsSMulWithCancel,
  Subgroup.mul_mem_cancel_left] using hc

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
⊢ Cancels (-u) (unitsSMul φ u w) ↔ ¬Cancels u w

Tactic:
by_cases h : Cancels u w

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

case neg
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
⊢ Cancels (-u) (unitsSMul φ u w) ↔ ¬Cancels u w

Proof state:
case pos
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
⊢ ¬Cancels (-u) (unitsSMulWithCancel φ u w ⋯)

Tactic:
induction w using consRecOn with
| ofGroup => simp [Cancels, unitsSMulWithCancel]
| cons g u' w h1 h2 _ =>
  intro hc
  apply not_cancels_of_cons_hyp _ _ h2
  simp only [Cancels, cons_head, cons_toList, List.head?_cons,
    Option.map_some', Option.some.injEq] at h
  cases h.2
  simpa [Cancels, unitsSMulWithCancel,
    Subgroup.mul_mem_cancel_left] using hc

Result:
no goals

Proof state:
case pos.cons
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
a✝ : ∀ (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) ⋯)
⊢ False

Tactic:
apply not_cancels_of_cons_hyp _ _ h2

Result:
case pos.cons
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
a✝ : ∀ (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) ⋯)
⊢ Cancels u' w

Proof state:
case pos.cons
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
a✝ : ∀ (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) ⋯)
⊢ Cancels u' w

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

Result:
case pos.cons
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
a✝ : ∀ (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) ⋯)
h : g ∈ toSubgroup A B u ∧ u' = -u
⊢ Cancels u' w

Proof state:
case neg
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
⊢ Cancels (-u) (cons (↑(unitsSMulGroup φ d u w.head).1) u ((↑(unitsSMulGroup φ d u w.head).2 * w.head⁻¹) • w) ⋯ ⋯) ↔
    ¬Cancels u w

Tactic:
simpa [Cancels] using h

Result:
no goals

Proof state:
case neg
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
⊢ Cancels (-u) (unitsSMul φ u w) ↔ ¬Cancels u w

Tactic:
simp only [unitsSMul, dif_neg h]

Result:
case neg
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
⊢ Cancels (-u) (cons (↑(unitsSMulGroup φ d u w.head).1) u ((↑(unitsSMulGroup φ d u w.head).2 * w.head⁻¹) • w) ⋯ ⋯) ↔
    ¬Cancels u w

Proof state:
case pos
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
⊢ Cancels (-u) (unitsSMul φ u w) ↔ ¬Cancels u w

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

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

Proof state:
case pos.ofGroup
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
g✝ : G
h : Cancels u (ofGroup g✝)
⊢ ¬Cancels (-u) (unitsSMulWithCancel φ u (ofGroup g✝) ⋯)

Tactic:
simp [Cancels, unitsSMulWithCancel]

Result:
no goals

Proof state:
case pos.cons
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
a✝ : ∀ (h : Cancels u w), ¬Cancels (-u) (unitsSMulWithCancel φ u w ⋯)
h : Cancels u (cons g u' w h1 h2)
⊢ ¬Cancels (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) ⋯)

Tactic:
intro hc

Result:
case pos.cons
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
a✝ : ∀ (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) ⋯)
⊢ False

Proof state:
case pos.cons
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
a✝ : ∀ (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) ⋯)
h : g ∈ toSubgroup A B u ∧ u' = -u
⊢ Cancels u' w

Tactic:
cases h.2

Result:
case pos.cons.refl
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
g : G
w : NormalWord d
a✝ : ∀ (h : Cancels u w), ¬Cancels (-u) (unitsSMulWithCancel φ u w ⋯)
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