mathlib-initiative/mathlib-tactics huggingface dataset:
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)
i : ι
m m' : M i
w : Word M
⊢ (m * m') • w = m • m' • w

Tactic:
by

Goal state after:
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)
i : ι
w : Word M
⊢ 1 • w = w

Tactic:
by

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

Goal state before:
pp: B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
this : ¬Even (2 * k + 1)
⊢ ↑(M.M i i') * 2 - (2 * k + 1) = 2 * (↑(M.M i i') - k - 1) + 1

Tactic:
by

Goal state after:
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
w : Word M
⊢ (equivPair i) (of m • w) = { head := m * ((equivPair i) w).head, tail := ((equivPair i) w).tail, fstIdx_ne := ⋯ }

Tactic:
by

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

Goal state before:
pp: B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
this✝ : ¬Even (2 * k + 1)
this : ¬Even (↑(M.M i i') * 2 - (2 * k + 1))
⊢ ↑(M.M i i') * 2 - (2 * k + 1) = -1 + (-k + ↑(M.M i i')) * 2

Tactic:
by

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

Goal state before:
pp: B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
this✝ : ¬Even (2 * k + 1)
this : ¬Even (↑(M.M i i') * 2 - (2 * k + 1))
⊢ 2 * k + 1 = 1 + k * 2

Tactic:
by

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

Goal state before:
pp: B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
this✝ : ¬Even (2 * k + 1)
this : ¬Even (↑(M.M i i') * 2 - (2 * k + 1))
⊢ 2 ≠ 0

Tactic:
by

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ (Matrix.of fun i j ↦ if i = j then 1 else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2).IsSymm

Tactic:
by

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ ∀ (i : Fin n), Matrix.of (fun i j ↦ if i = j then 1 else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2) i i = 1

Tactic:
by

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ ∀ (i i' : Fin n),
    i ≠ i' → Matrix.of (fun i j ↦ if i = j then 1 else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2) i i' ≠ 1

Tactic:
by

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ (Matrix.of fun i j ↦
      if i = j then 1
      else
        if ↑i = n - 1 ∧ ↑j = n - 2 ∨ ↑j = n - 1 ∧ ↑i = n - 2 then 4
        else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2).IsSymm

Tactic:
by

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ ∀ (i : Fin n),
    Matrix.of
        (fun i j ↦
          if i = j then 1
          else
            if ↑i = n - 1 ∧ ↑j = n - 2 ∨ ↑j = n - 1 ∧ ↑i = n - 2 then 4 else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2)
        i i =
      1

Tactic:
by

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ ∀ (i i' : Fin n),
    i ≠ i' →
      Matrix.of
          (fun i j ↦
            if i = j then 1
            else
              if ↑i = n - 1 ∧ ↑j = n - 2 ∨ ↑j = n - 1 ∧ ↑i = n - 2 then 4
              else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2)
          i i' ≠
        1

Tactic:
by

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ (Matrix.of fun i j ↦
      if i = j then 1
      else
        if ↑i = n - 1 ∧ ↑j = n - 3 ∨ ↑j = n - 1 ∧ ↑i = n - 3 then 3
        else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2).IsSymm

Tactic:
by

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ ∀ (i : Fin n),
    Matrix.of
        (fun i j ↦
          if i = j then 1
          else
            if ↑i = n - 1 ∧ ↑j = n - 3 ∨ ↑j = n - 1 ∧ ↑i = n - 3 then 3 else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2)
        i i =
      1

Tactic:
by

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ ∀ (i i' : Fin n),
    i ≠ i' →
      Matrix.of
          (fun i j ↦
            if i = j then 1
            else
              if ↑i = n - 1 ∧ ↑j = n - 3 ∨ ↑j = n - 1 ∧ ↑i = n - 3 then 3
              else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2)
          i i' ≠
        1

Tactic:
by

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n m : ℕ
⊢ (Matrix.of fun i j ↦ if i = j then 1 else m + 2).IsSymm

Tactic:
by

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n m : ℕ
⊢ ∀ (i : Fin 2), Matrix.of (fun i j ↦ if i = j then 1 else m + 2) i i = 1

Tactic:
by

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n m : ℕ
⊢ ∀ (i i' : Fin 2), i ≠ i' → Matrix.of (fun i j ↦ if i = j then 1 else m + 2) i i' ≠ 1

Tactic:
by

Goal state after:
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
⊢ ∃ n ω, n = ω.length ∧ cs.wordProd ω = w

Tactic:
by

Goal state after:
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
⊢ ∃ ω, cs.IsReduced ω ∧ w = cs.wordProd ω

Tactic:
by

Goal state after:
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
ω : List B
⊢ cs.length (cs.wordProd ω) ≤ ω.length

Tactic:
by

Goal state after:
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
⊢ cs.length w = 0 ↔ w = 1

Tactic:
by

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

Goal state before:
pp: B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hm : m ≤ M.M i i' * 2
⊢ cs.wordProd (alternatingWord i i' m) = cs.wordProd (alternatingWord i' i (M.M i i' * 2 - m))

Tactic:
by

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

Goal state before:
pp: B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
⊢ 0 < 2

Tactic:
by

Goal state after:
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
⊢ cs.length w⁻¹ = cs.length w

Tactic:
by

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

Goal state before:
pp: B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
⊢ cs.wordProd (braidWord M i i') = cs.wordProd (braidWord M i' i)

Tactic:
by

Goal state after:
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₂ : W
⊢ cs.length (w₁ * w₂) ≤ cs.length w₁ + cs.length w₂

Tactic:
by

Goal state after:
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₂ : W
⊢ cs.length w₂ ≤ cs.length (w₁ * w₂) + cs.length w₁

Tactic:
by

Goal state after:
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₂ : W
⊢ cs.length w₁ ≤ cs.length (w₁ * w₂) + cs.length w₂

Tactic:
by

Goal state after:
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
i : B
⊢ cs.IsReflection (cs.simple i)

Tactic:
by

Goal state after:
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
t : W
ht : cs.IsReflection t
⊢ t ^ 2 = 1

Tactic:
by

Goal state after:
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
t : W
ht : cs.IsReflection t
⊢ t * t = 1

Tactic:
by

Goal state after:
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
t : W
ht : cs.IsReflection t
⊢ t⁻¹ = t

Tactic:
by

Goal state after:
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
t : W
ht : cs.IsReflection t
⊢ cs.IsReflection t⁻¹

Tactic:
by

Goal state after:
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
t : W
ht : cs.IsReflection t
this : cs.lengthParity t = Multiplicative.ofAdd 1
⊢ Odd (cs.length t)

Tactic:
by

Goal state after:
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
t : W
ht : cs.IsReflection t
⊢ Odd (cs.length t)

Tactic:
by

Goal state after:
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₂ : W
⊢ cs.length w₁ - cs.length w₂ ≤ cs.length (w₁ * w₂)

Tactic:
by

Goal state after:
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
t : W
ht : cs.IsReflection t
w : W
this : cs.lengthParity (w * t) ≠ cs.lengthParity w
⊢ cs.length (w * t) ≠ cs.length w

Tactic:
by

Goal state after:
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₂ : W
⊢ cs.length w₂ - cs.length w₁ ≤ cs.length (w₁ * w₂)

Tactic:
by

Goal state after:
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
t : W
ht : cs.IsReflection t
w : W
⊢ cs.length (w * t) ≠ cs.length w

Tactic:
by

Goal state after:
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
⊢ 1 + 1 = 0

Tactic:
by

Goal state after:
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
⊢ M.IsLiftable fun x ↦ Multiplicative.ofAdd 1

Tactic:
by

Goal state after:
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
t : W
ht : cs.IsReflection t
w : W
this : cs.lengthParity (t * w) ≠ cs.lengthParity w
⊢ cs.length (t * w) ≠ cs.length w

Tactic:
by

Goal state after:
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
t : W
ht : cs.IsReflection t
w : W
⊢ cs.length (t * w) ≠ cs.length w

Tactic:
by

Goal state after:
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
⊢ cs.lengthParity w = Multiplicative.ofAdd ↑(cs.length w)

Tactic:
by

Goal state after:
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
t : W
ht : cs.IsReflection t
w : W
⊢ cs.IsReflection (w * t * w⁻¹)

Tactic:
by

Goal state after:
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₂ : W
⊢ cs.length (w₁ * w₂) % 2 = (cs.length w₁ + cs.length w₂) % 2

Tactic:
by

Goal state after:
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 : B
length_lt_one : cs.length (cs.simple i) < 1
⊢ cs.lengthParity (cs.simple i) = Multiplicative.ofAdd 0

Tactic:
by

Goal state after:
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
w t : W
⊢ cs.IsReflection (w * t * w⁻¹) ↔ cs.IsReflection t

Tactic:
by

Goal state after:
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 : B
⊢ cs.length (cs.simple i) = 1

Tactic:
by

Goal state after:
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)
w : Word M
hnil : ¬w.toList = []
m₂ m₁ : M (w.toList.head hnil).fst
hw : ⟨(w.toList.head hnil).fst, m₁⟩ ∉ w.toList.tail
hm1 : ¬m₁ = 1
hm' : (∀ (x : M (w.toList.head hnil).fst), ¬w.toList.head? = some ⟨(w.toList.head hnil).fst, x⟩) ∧ m₁ = m₂
⊢ w.toList.head? = some ⟨(w.toList.head hnil).fst, (w.toList.head hnil).snd⟩

Tactic:
by

Goal state after:
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
⊢ cs.length w = 1 ↔ ∃ i, w = cs.simple i

Tactic:
by

Goal state after:
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
w t : W
⊢ cs.IsRightInversion w⁻¹ t ↔ cs.IsLeftInversion w t

Tactic:
by

Goal state after:
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
w t : W
⊢ cs.IsLeftInversion w⁻¹ t ↔ cs.IsRightInversion w t

Tactic:
by

Goal state after:
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) ≠ cs.length w

Tactic:
by

Goal state after:
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

Tactic:
by

Goal state after:
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < r' ^ 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
⊢ ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ

Tactic:
by

Goal state after:
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
t : W
ht : cs.IsReflection t
w : W
⊢ cs.IsRightInversion (w * t) t ↔ ¬cs.IsRightInversion w t

Tactic:
by

Goal state after:
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) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w

Tactic:
by

Goal state after:
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
this : cs.length (w⁻¹ * cs.simple i) = cs.length w⁻¹ + 1 ∨ cs.length (w⁻¹ * cs.simple i) + 1 = cs.length w⁻¹
⊢ w⁻¹ * cs.simple i = (cs.simple i * w)⁻¹

Tactic:
by

Goal state after:
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
t : W
ht : cs.IsReflection t
w : W
⊢ cs.IsLeftInversion (t * w) t ↔ ¬cs.IsLeftInversion w t

Tactic:
by

Goal state after:
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
w : W
i : B
⊢ cs.IsRightInversion w (cs.simple i) ↔ cs.IsRightDescent w i

Tactic:
by

Goal state after:
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
w : W
i : B
⊢ cs.IsLeftInversion w (cs.simple i) ↔ cs.IsLeftDescent w i

Tactic:
by

Goal state after:
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
i : B
⊢ cs.rightInvSeq [i] = [cs.simple i]

Tactic:
by

Goal state after:
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 + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w

Tactic:
by

Goal state after:
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
ω : List B
⊢ cs.IsReduced ω.reverse ↔ cs.IsReduced ω

Tactic:
by

Goal state after:
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
ω : List B
hω : cs.IsReduced ω
j : ℕ
h₁ : cs.length (cs.wordProd (take j ω)) ≤ (take j ω).length
h₂ : cs.length (cs.wordProd (drop j ω)) ≤ (drop j ω).length
⊢ (take j ω).length + (drop j ω).length = ω.length

Tactic:
by

Goal state after:
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
ω : List B
hω : cs.IsReduced ω
j : ℕ
h₁ : cs.length (cs.wordProd (take j ω)) ≤ (take j ω).length
h₂ : cs.length (cs.wordProd (drop j ω)) ≤ (drop j ω).length
⊢ cs.length (cs.wordProd ω) = cs.length (cs.wordProd (take j ω) * cs.wordProd (drop j ω))

Tactic:
by

Goal state after:
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
ω : List B
hω : cs.IsReduced ω
j : ℕ
⊢ cs.IsReduced (take j ω) ∧ cs.IsReduced (drop j ω)

Tactic:
by

Goal state after:
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.IsReduced (alternatingWord i i' (M.M i i').succ)

Tactic:
by

Goal state after:
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:
simp only [concat_eq_append, wordProd_append, wordProd_cons, wordProd_nil, mul_one, mul_inv_rev,
      inv_simple, map_cons, MulAut.conj_apply, cons_append, cons.injEq, and_true]

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.simple i * (cs.wordProd ω)⁻¹ * cs.simple j * (cs.wordProd ω * cs.simple i) =
    cs.simple i * ((cs.wordProd ω)⁻¹ * cs.simple j * cs.wordProd ω) * 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
⊢ M.M i i' + 1 ≤ M.M i i' * 2

Tactic:
by

Goal state after:
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
i : B
⊢ cs.rightInvSeq (ω.concat i) = (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i)

Tactic:
by

Goal state after:
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
this : M.M i i' + 1 ≤ M.M i i' * 2
⊢ M.M i i' * 2 - (M.M i i' + 1) = M.M i i' - 1

Tactic:
by

Goal state after:
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
⊢ cs.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse

Tactic:
by

Goal state after:
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
i : B
⊢ cs.leftInvSeq (ω.concat i) = (cs.leftInvSeq ω).concat (cs.wordProd ω * cs.simple i * (cs.wordProd ω)⁻¹)

Tactic:
by

Goal state after:
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
⊢ cs.rightInvSeq ω.reverse = (cs.leftInvSeq ω).reverse

Tactic:
by

Goal state after:
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
⊢ cs.leftInvSeq ω.reverse = (cs.rightInvSeq ω).reverse

Tactic:
by

Goal state after:
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
⊢ (cs.rightInvSeq ω).length = ω.length

Tactic:
by

Goal state after:
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
⊢ (cs.leftInvSeq ω).length = ω.length

Tactic:
by

Goal state after: