mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
ω : List B
ih : cs.rightInvSeq (ω.concat i) = (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i)
⊢ (cs.wordProd (ω.concat i))⁻¹ * cs.simple j * cs.wordProd (ω.concat i) ::
      (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i) =
    (List.map (⇑(MulAut.conj (cs.simple i)))
          ((cs.wordProd ω)⁻¹ * cs.simple j * cs.wordProd ω :: cs.rightInvSeq ω)).concat
      (cs.simple i)

Tactic:
]

Goal state after:
case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
ω : List B
ih : cs.rightInvSeq (ω.concat i) = (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i)
⊢ (cs.wordProd (ω.concat i))⁻¹ * cs.simple j * cs.wordProd (ω.concat i) ::
      (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i) =
    (List.map (⇑(MulAut.conj (cs.simple i)))
          ((cs.wordProd ω)⁻¹ * cs.simple j * cs.wordProd ω :: cs.rightInvSeq ω)).concat
      (cs.simple i)
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
h : cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) < M.M i i' + 1
⊢ ¬cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) = M.M i i' + 1

Tactic:
]

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
h : cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) < M.M i i' + 1
⊢ ¬cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) = M.M i i' + 1
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case refl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
this : M.M i i' + 1 ≤ M.M i i' * 2
⊢ cs.length (cs.wordProd (alternatingWord i' i (M.M i i' * 2 - (M.M i i' + 1)))) < M.M i i' + 1

Tactic:
]

Goal state after:
case refl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
this : M.M i i' + 1 ≤ M.M i i' * 2
⊢ cs.length (cs.wordProd (alternatingWord i' i (M.M i i' * 2 - (M.M i i' + 1)))) < M.M i i' + 1
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih : cs.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse
⊢ cs.simple i :: List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω) = (cs.rightInvSeq (i :: ω).reverse).reverse

Tactic:
reverse_cons,

Goal state after:
case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih : cs.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse
⊢ cs.simple i :: List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω) = (cs.rightInvSeq (ω.reverse ++ [i])).reverse
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih : cs.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse
⊢ cs.simple i :: List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω.reverse).reverse =
    ((List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω.reverse)).concat (cs.simple i)).reverse

Tactic:
]

Goal state after:
case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih : cs.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse
⊢ cs.simple i :: List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω.reverse).reverse =
    ((List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω.reverse)).concat (cs.simple i)).reverse
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case refl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
this✝ : M.M i i' + 1 ≤ M.M i i' * 2
this : M.M i i' * 2 - (M.M i i' + 1) = M.M i i' - 1
⊢ cs.length (cs.wordProd (alternatingWord i' i (M.M i i' - 1))) < M.M i i' + 1

Tactic:
]

Goal state after:
case refl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
this✝ : M.M i i' + 1 ≤ M.M i i' * 2
this : M.M i i' * 2 - (M.M i i' + 1) = M.M i i' - 1
⊢ cs.length (cs.wordProd (alternatingWord i' i (M.M i i' - 1))) < M.M i i' + 1
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case step
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m✝¹ : ℕ
hM : M.M i i' ≠ 0
m✝ : ℕ
m : (M.M i i').succ.le m✝
ih : cs.IsReduced ((if Even m✝ then i' else i) :: alternatingWord i i' m✝)
⊢ cs.IsReduced (alternatingWord i i' m✝)

Tactic:
]

Goal state after:
case step
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m✝¹ : ℕ
hM : M.M i i' ≠ 0
m✝ : ℕ
m : (M.M i i').succ.le m✝
ih : cs.IsReduced ((if Even m✝ then i' else i) :: alternatingWord i i' m✝)
⊢ cs.IsReduced (alternatingWord i i' m✝)
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w⁻¹)⁻¹ < cs.length w⁻¹ ↔ cs.length (w * cs.simple i) < cs.length w

Tactic:
]

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w⁻¹)⁻¹ < cs.length w⁻¹ ↔ cs.length (w * cs.simple i) < cs.length w
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω' : List B
h : cs.IsReduced (i :: ω')
hw : cs.wordProd (i :: ω') ≠ 1
h₁ : i :: ω' ≠ []
⊢ cs.length (cs.wordProd ω') < (i :: ω').length

Tactic:
]

Goal state after:
case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω' : List B
h : cs.IsReduced (i :: ω')
hw : cs.wordProd (i :: ω') ≠ 1
h₁ : i :: ω' ≠ []
⊢ cs.length (cs.wordProd ω') < (i :: ω').length
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
h : j < ω.length
⊢ (cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω) =
    (cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω)

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case cons.succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω)).getD j' 1 =
    cs.wordProd (take (j' + 1) (i :: ω)) * (Option.map cs.simple (i :: ω)[j' + 1]?).getD 1 *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹

Tactic:
]

Goal state after:
case cons.succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω)).getD j' 1 =
    cs.wordProd (take (j' + 1) (i :: ω)) * (Option.map cs.simple (i :: ω)[j' + 1]?).getD 1 *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w) + 1 = cs.length w ↔ cs.length w = cs.length (cs.simple i * w) + 1

Tactic:
]

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w) + 1 = cs.length w ↔ cs.length w = cs.length (cs.simple i * w) + 1
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case cons.succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω)).getD j' ((MulAut.conj (cs.simple i)) 1) =
    cs.wordProd (take (j' + 1) (i :: ω)) *
        (Option.map cs.simple (i :: ω)[j' + 1]?).getD ((MulAut.conj (cs.simple i)) 1) *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹

Tactic:
]

Goal state after:
case cons.succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω)).getD j' ((MulAut.conj (cs.simple i)) 1) =
    cs.wordProd (take (j' + 1) (i :: ω)) *
        (Option.map cs.simple (i :: ω)[j' + 1]?).getD ((MulAut.conj (cs.simple i)) 1) *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (w * cs.simple i) + 1 = cs.length w ↔ cs.length w = cs.length (w * cs.simple i) + 1

Tactic:
]

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (w * cs.simple i) + 1 = cs.length w ↔ cs.length w = cs.length (w * cs.simple i) + 1
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case cons.succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (MulAut.conj (cs.simple i)) ((cs.leftInvSeq ω).getD j' 1) =
    cs.wordProd (take (j' + 1) (i :: ω)) *
        (Option.map cs.simple (i :: ω)[j' + 1]?).getD ((MulAut.conj (cs.simple i)) 1) *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹

Tactic:
]

Goal state after:
case cons.succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (MulAut.conj (cs.simple i)) ((cs.leftInvSeq ω).getD j' 1) =
    cs.wordProd (take (j' + 1) (i :: ω)) *
        (Option.map cs.simple (i :: ω)[j' + 1]?).getD ((MulAut.conj (cs.simple i)) 1) *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case cons.succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (MulAut.conj (cs.simple i))
      (cs.wordProd (take j' ω) * (Option.map cs.simple ω[j']?).getD 1 * (cs.wordProd (take j' ω))⁻¹) =
    cs.wordProd (take (j' + 1) (i :: ω)) *
        (Option.map cs.simple (i :: ω)[j' + 1]?).getD ((MulAut.conj (cs.simple i)) 1) *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹

Tactic:
]

Goal state after:
case cons.succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (MulAut.conj (cs.simple i))
      (cs.wordProd (take j' ω) * (Option.map cs.simple ω[j']?).getD 1 * (cs.wordProd (take j' ω))⁻¹) =
    cs.wordProd (take (j' + 1) (i :: ω)) *
        (Option.map cs.simple (i :: ω)[j' + 1]?).getD ((MulAut.conj (cs.simple i)) 1) *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
ls : Word M
h1 : ls.fstIdx ≠ some i
h2 : m ≠ 1
⊢ cons m ls h1 h2 =
    rcons
      (have __src := { head := 1, tail := ls, fstIdx_ne := ?m.39 };
      { head := m * { head := 1, tail := ls, fstIdx_ne := ?m.39 }.head, tail := __src.tail, fstIdx_ne := ⋯ })

pp: ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
ls : Word M
h1 : ls.fstIdx ≠ some i
h2 : m ≠ 1
⊢ ls.fstIdx ≠ some i

Tactic:
]

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
ls : Word M
h1 : ls.fstIdx ≠ some i
h2 : m ≠ 1
⊢ cons m ls h1 h2 =
    rcons
      (have __src := { head := 1, tail := ls, fstIdx_ne := ?m.39 };
      { head := m * { head := 1, tail := ls, fstIdx_ne := ?m.39 }.head, tail := __src.tail, fstIdx_ne := ⋯ })

ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
ls : Word M
h1 : ls.fstIdx ≠ some i
h2 : m ≠ 1
⊢ ls.fstIdx ≠ some i
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
w : Word M
⊢ w = w

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case cons
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
motive : Word M → Prop
empty : motive Word.empty
smul : ∀ (i : ι) (m : M i) (w : Word M), motive w → motive (of m • w)
i✝ : ι
m✝ : M i✝
w✝ : Word M
h1✝ : w✝.fstIdx ≠ some i✝
h2✝ : m✝ ≠ 1
ih : motive w✝
⊢ motive (of m✝ • w✝)

Tactic:
]

Goal state after:
case cons
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
motive : Word M → Prop
empty : motive Word.empty
smul : ∀ (i : ι) (m : M i) (w : Word M), motive w → motive (of m • w)
i✝ : ι
m✝ : M i✝
w✝ : Word M
h1✝ : w✝.fstIdx ≠ some i✝
h2✝ : m✝ ≠ 1
ih : motive w✝
⊢ motive (of m✝ • w✝)
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
h : j < ω.length
⊢ cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹ =
    cs.wordProd (take j ω) * cs.simple ω[j] * (cs.wordProd (take j ω))⁻¹

Tactic:
]

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
h : j < ω.length
⊢ cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹ =
    cs.wordProd (take j ω) * cs.simple ω[j] * (cs.wordProd (take j ω))⁻¹
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case one
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
w✝ : Word M
⊢ w✝.prod = w✝.prod

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case of
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i✝ : ι
m✝ : M i✝
w✝ : Word M
⊢ of m✝ * w✝.prod = of m✝ * w✝.prod

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case mul
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
x y : CoprodI M
hx : ∀ (w : Word M), (x • w).prod = x * w.prod
hy : ∀ (w : Word M), (y • w).prod = y * w.prod
w : Word M
⊢ x * (y * w.prod) = x * (y * w.prod)

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
hj : j < ω.length
⊢ (cs.wordProd (drop (j + 1) ω))⁻¹ *
      ((Option.map cs.simple (some ω[j])).getD 1 *
        (cs.wordProd (drop (j + 1) ω) *
          ((cs.wordProd (drop (j + 1) ω))⁻¹ *
            ((Option.map cs.simple (some ω[j])).getD 1 * cs.wordProd (drop (j + 1) ω))))) =
    1

Tactic:
]

Goal state after:
case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
hj : j < ω.length
⊢ (cs.wordProd (drop (j + 1) ω))⁻¹ *
      ((Option.map cs.simple (some ω[j])).getD 1 *
        (cs.wordProd (drop (j + 1) ω) *
          ((cs.wordProd (drop (j + 1) ω))⁻¹ *
            ((Option.map cs.simple (some ω[j])).getD 1 * cs.wordProd (drop (j + 1) ω))))) =
    1
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝² : Monoid N
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
m : CoprodI M
⊢ m = m

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case empty
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝² : Monoid N
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
⊢ empty = empty

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case inr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
nhj : ¬j < ω.length
⊢ (cs.wordProd (drop (j + 1) ω))⁻¹ *
      ((Option.map cs.simple none).getD 1 *
        (cs.wordProd (drop (j + 1) ω) *
          ((cs.wordProd (drop (j + 1) ω))⁻¹ * ((Option.map cs.simple none).getD 1 * cs.wordProd (drop (j + 1) ω))))) =
    1

Tactic:
]

Goal state after:
case inr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
nhj : ¬j < ω.length
⊢ (cs.wordProd (drop (j + 1) ω))⁻¹ *
      ((Option.map cs.simple none).getD 1 *
        (cs.wordProd (drop (j + 1) ω) *
          ((cs.wordProd (drop (j + 1) ω))⁻¹ * ((Option.map cs.simple none).getD 1 * cs.wordProd (drop (j + 1) ω))))) =
    1
Module: Mathlib.GroupTheory.Descent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
f : G →* G
hf : ∀ (U : Subgroup G), map f U ≤ U
s : Set G
h : G → ℝ
a b c : ℝ
ha : 0 ≤ a
H₀ : a < b
hs : s.Finite
H₁ : s * ↑f.range = Set.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h (f x)
inst✝ : Northcott h
q : G → G ⧸ map f ⊤ := QuotientGroup.mk
S : Set G := s ∪ {x | h x ≤ 2 * c / (b - a)}
U : Subgroup G := closure S
H : (↑U)ᶜ.Nonempty
⊢ False

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
f : G →* G
hf : ∀ (U : Subgroup G), map f U ≤ U
s : Set G
h : G → ℝ
a b c : ℝ
ha : 0 ≤ a
H₀ : a < b
hs : s.Finite
H₁ : s * ↑f.range = Set.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h (f x)
inst✝ : Northcott h
q : G → G ⧸ map f ⊤ := QuotientGroup.mk
S : Set G := s ∪ {x | h x ≤ 2 * c / (b - a)}
U : Subgroup G := closure S
H : (↑U)ᶜ.Nonempty
⊢ False
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case smul
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝² : Monoid N
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
ih : w.prod • empty = w
⊢ of m • w = of m • w

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j : ι
w : NeWord M i j
⊢ ⟨j, w.last⟩ ∈ w.toList.getLast?

Tactic:
]

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j : ι
w : NeWord M i j
⊢ ⟨j, w.last⟩ ∈ w.toList.getLast?
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
hj : j < ω.length
⊢ cs.wordProd (take j ω) *
      ((Option.map cs.simple (some ω[j])).getD 1 *
        ((cs.wordProd (take j ω))⁻¹ *
          (cs.wordProd (take j ω) * ((Option.map cs.simple (some ω[j])).getD 1 * (cs.wordProd (take j ω))⁻¹)))) =
    1

Tactic:
]

Goal state after:
case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
hj : j < ω.length
⊢ cs.wordProd (take j ω) *
      ((Option.map cs.simple (some ω[j])).getD 1 *
        ((cs.wordProd (take j ω))⁻¹ *
          (cs.wordProd (take j ω) * ((Option.map cs.simple (some ω[j])).getD 1 * (cs.wordProd (take j ω))⁻¹)))) =
    1
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ (singleton x✝ a✝).toList.getLast? = some ⟨i✝, (singleton x✝ a✝).last⟩

Tactic:
]

Goal state after:
case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ (singleton x✝ a✝).toList.getLast? = some ⟨i✝, (singleton x✝ a✝).last⟩
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case inr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
nhj : ¬j < ω.length
⊢ cs.wordProd (take j ω) *
      ((Option.map cs.simple none).getD 1 *
        ((cs.wordProd (take j ω))⁻¹ *
          (cs.wordProd (take j ω) * ((Option.map cs.simple none).getD 1 * (cs.wordProd (take j ω))⁻¹)))) =
    1

Tactic:
]

Goal state after:
case inr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
nhj : ¬j < ω.length
⊢ cs.wordProd (take j ω) *
      ((Option.map cs.simple none).getD 1 *
        ((cs.wordProd (take j ω))⁻¹ *
          (cs.wordProd (take j ω) * ((Option.map cs.simple none).getD 1 * (cs.wordProd (take j ω))⁻¹)))) =
    1