mathlib-initiative/mathlib-tactics huggingface dataset:
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
this✝ : (FreeGroup.of i * FreeGroup.of i') ^ M.M i i' ∈ M.relationsSet
this : (PresentedGroup.mk M.relationsSet) ((FreeGroup.of i * FreeGroup.of i') ^ M.M i i') = 1
⊢ cs.mulEquiv.symm ((PresentedGroup.of i * PresentedGroup.of i') ^ M.M i i') = 1

Tactic:
]

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
this✝ : (FreeGroup.of i * FreeGroup.of i') ^ M.M i i' ∈ M.relationsSet
this : (PresentedGroup.mk M.relationsSet) ((FreeGroup.of i * FreeGroup.of i') ^ M.M i i') = 1
⊢ cs.mulEquiv.symm ((PresentedGroup.of i * PresentedGroup.of i') ^ M.M i i') = 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
f g : CoprodI M →* N
h : ∀ (i : ι), f.comp of = g.comp of
x✝ : (i : ι) × M i
i : ι
x : M i
⊢ f (of x) = g (of x)

Tactic:
]

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
f g : CoprodI M →* N
h : ∀ (i : ι), f.comp of = g.comp of
x✝ : (i : ι) × M i
i : ι
x : M i
⊢ f (of x) = g (of x)
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
f g : CoprodI M →* N
h : ∀ (i : ι), f.comp of = g.comp of
x✝ : (i : ι) × M i
i : ι
x : M i
⊢ (g.comp of) x = (g.comp of) x

Tactic:
]

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
this : cs.simple = ⇑cs.mulEquiv.symm ∘ PresentedGroup.of
⊢ cs.mulEquiv.symm.toMonoidHom.range = ⊤

Tactic:
]

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
this : cs.simple = ⇑cs.mulEquiv.symm ∘ PresentedGroup.of
⊢ cs.mulEquiv.symm.toMonoidHom.range = ⊤
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
this : Set.range cs.simple = Set.range cs.simple ∪ (Set.range cs.simple)⁻¹
⊢ ⊤ = ⊤

Tactic:
]

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

Goal state before:
pp: case mul_left
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x ↦ p w
i : W
mi : ∃ y, cs.simple y = i
y : W
my : y ∈ Submonoid.closure (Set.range cs.simple)
ih : p y
⊢ p (i * y)

Tactic:
]

Goal state after:
case mul_left
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x ↦ p w
i : W
mi : ∃ y, cs.simple y = i
y : W
my : y ∈ Submonoid.closure (Set.range cs.simple)
ih : p y
⊢ p (i * y)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_4
inst✝ : Monoid N
f : (i : ι) → M i →* N
⊢ ⨆ i, Submonoid.closure (range fun b ↦ (f ⟨i, b⟩.fst) ⟨i, b⟩.snd) = ⨆ i, MonoidHom.mrange (f i)

Tactic:
]

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_4
inst✝ : Monoid N
f : (i : ι) → M i →* N
⊢ ⨆ i, Submonoid.closure (range fun b ↦ (f ⟨i, b⟩.fst) ⟨i, b⟩.snd) = ⨆ i, MonoidHom.mrange (f i)
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case mul_right
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_right : ∀ (w : W) (i : B), p w → p (w * cs.simple i)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x ↦ p w
y : W
my : y ∈ Submonoid.closure (Set.range cs.simple)
i : W
mi : ∃ y, cs.simple y = i
ih : p y
⊢ p (y * i)

Tactic:
]

Goal state after:
case mul_right
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_right : ∀ (w : W) (i : B), p w → p (w * cs.simple i)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x ↦ p w
y : W
my : y ∈ Submonoid.closure (Set.range cs.simple)
i : W
mi : ∃ y, cs.simple y = i
ih : p y
⊢ p (y * i)
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
p : W → Prop
w : W
one : p 1
mul_simple_right : ∀ (w : W) (i : B), p w → p (w * cs.simple i)
⊢ p w

Tactic:
by
  let p' : ((w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop) :=
    fun w _ ↦ p w
  have := cs.submonoid_closure_range_simple.symm ▸ Submonoid.mem_top w
  induction this using Submonoid.closure_induction_right with
  | one => exact one
  | mul_right y my i mi ih =>
    rw [Set.mem_range] at mi
    exact mi.choose_spec ▸ mul_simple_right _ _ ih

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

Goal state before:
pp: B : Type u_1
M : CoxeterMatrix B
G : Type u_5
inst✝ : Group G
f : B → G
hf : M.IsLiftable f
i i' : B
⊢ (f (i, i').1 * f (i, i').2) ^ M.M (i, i').1 (i, i').2 = 1

Tactic:
]

Goal state after:
B : Type u_1
M : CoxeterMatrix B
G : Type u_5
inst✝ : Group G
f : B → G
hf : M.IsLiftable f
i i' : B
⊢ (f (i, i').1 * f (i, i').2) ^ M.M (i, i').1 (i, i').2 = 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
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
m : CoprodI G
⊢ MulOpposite.unop ((lift fun i ↦ (MonoidHom.op of).comp (MulEquiv.inv' (G i)).toMonoidHom) m) * m = 1

Tactic:
]

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
N : Type u_3
inst✝¹ : Monoid N
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
m : CoprodI G
⊢ MulOpposite.unop ((lift fun i ↦ (MonoidHom.op of).comp (MulEquiv.inv' (G i)).toMonoidHom) m) * m = 1
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
a : PresentedGroup M.relationsSet
⊢ a = a

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case one
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
N : Type u_3
inst✝¹ : Monoid N
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
⊢ 1 = 1

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)
N : Type u_3
inst✝¹ : Monoid N
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
m : ι
ih : G m
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝² : Group W
inst✝¹ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst✝ : Monoid G
ι : W →* G
i i' : B
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝² : Group W
inst✝¹ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst✝ : Monoid G
f : { f // M.IsLiftable f }
i : B
⊢ ↑(restrictUnit ⋯ i) = ↑f i

Tactic:
restrictUnit

Goal state after:
B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝² : Group W
inst✝¹ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst✝ : Monoid G
f : { f // M.IsLiftable f }
i : B
⊢ ↑{ val := ↑f i, inv := ↑f i, val_inv := ⋯, inv_val := ⋯ } = ↑f i
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝² : Group W
inst✝¹ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst✝ : Monoid G
f : { f // M.IsLiftable f }
i : B
⊢ ↑{ val := ↑f i, inv := ↑f i, val_inv := ⋯, inv_val := ⋯ } = ↑f i

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)
N : Type u_3
inst✝¹ : Monoid N
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
x y : CoprodI G
ihx : MulOpposite.unop ((lift fun i ↦ (MonoidHom.op of).comp (MulEquiv.inv' (G i)).toMonoidHom) x) * x = 1
ihy : MulOpposite.unop ((lift fun i ↦ (MonoidHom.op of).comp (MulEquiv.inv' (G i)).toMonoidHom) y) * y = 1
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝² : Group W
inst✝¹ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst✝ : Monoid G
ι : W →* G
i : B
⊢ ↑{ val := (⇑ι ∘ cs.simple) i, inv := (⇑ι ∘ cs.simple) i, val_inv := ⋯, inv_val := ⋯ } =
    ι (cs.mulEquiv.symm (PresentedGroup.of i))

Tactic:
]

Goal state after:
B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝² : Group W
inst✝¹ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst✝ : Monoid G
ι : W →* G
i : B
⊢ ↑{ val := (⇑ι ∘ cs.simple) i, inv := (⇑ι ∘ cs.simple) i, val_inv := ⋯, inv_val := ⋯ } =
    ι (cs.mulEquiv.symm (PresentedGroup.of i))
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 y : B
hy :
  ‖Trivialization.symmL ℝ (trivializationAt F E x) x ∘SL
        Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ <
    2
A :
  Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x ∘SL
      Trivialization.symmL ℝ (trivializationAt F E x) x =
    ContinuousLinearMap.id ℝ F
this :
  Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y =
    ContinuousLinearMap.id ℝ F ∘SL Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y
⊢ ‖Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖ *
      ‖Trivialization.symmL ℝ (trivializationAt F E x) x ∘SL
          Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ <
    (1 + ‖Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖) * 2

Tactic:
]

Goal state after:
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 y : B
hy :
  ‖Trivialization.symmL ℝ (trivializationAt F E x) x ∘SL
        Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ <
    2
A :
  Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x ∘SL
      Trivialization.symmL ℝ (trivializationAt F E x) x =
    ContinuousLinearMap.id ℝ F
this :
  Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y =
    ContinuousLinearMap.id ℝ F ∘SL Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y
⊢ ‖Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖ *
      ‖Trivialization.symmL ℝ (trivializationAt F E x) x ∘SL
          Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ <
    (1 + ‖Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖) * 2
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs1 cs2 : CoxeterSystem M W
h : cs1.simple = cs2.simple
⊢ ∀ (i : B), cs1.mulEquiv.toMonoidHom (cs1.simple i) = cs2.mulEquiv.toMonoidHom (cs2.simple i)

Tactic:
]

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs1 cs2 : CoxeterSystem M W
h : cs1.simple = cs2.simple
⊢ ∀ (i : B), cs1.mulEquiv.toMonoidHom (cs1.simple i) = cs2.mulEquiv.toMonoidHom (cs2.simple i)
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case h
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : p.head = 1
⊢ p.tail.prod = of p.head * p.tail.prod

Tactic:
hm,

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : p.head = 1
⊢ p.tail.prod = of 1 * p.tail.prod
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : p.head = 1
⊢ p.tail.prod = p.tail.prod

Tactic:
]

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

Goal state before:
pp: case h
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
ω : List B
⊢ cs.simple i * cs.wordProd ω = cs.simple i * cs.wordProd ω

Tactic:
]

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

Goal state before:
pp: case succ
B : Type u_1
m : ℕ
ih : ∀ (i i' : B), alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m
i i' : B
⊢ (alternatingWord i' i (m + 1)).concat i' = (if Even (m + 1) then i' else i) :: alternatingWord i i' (m + 1)

Tactic:
]

Goal state after:
case succ
B : Type u_1
m : ℕ
ih : ∀ (i i' : B), alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m
i i' : B
⊢ (alternatingWord i' i (m + 1)).concat i' = (if Even (m + 1) then i' else i) :: alternatingWord i i' (m + 1)
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case succ
B : Type u_1
m : ℕ
ih : ∀ (i i' : B), alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m
i i' : B
⊢ ((if Even m then i else i') :: alternatingWord i' i m).concat i' =
    (if Even (m + 1) then i' else i) :: alternatingWord i i' (m + 1)

Tactic:
]

Goal state after:
case succ
B : Type u_1
m : ℕ
ih : ∀ (i i' : B), alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m
i i' : B
⊢ ((if Even m then i else i') :: alternatingWord i' i m).concat i' =
    (if Even (m + 1) then i' else i) :: alternatingWord i i' (m + 1)
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case succ
B : Type u_1
m : ℕ
ih : ∀ (i i' : B), alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m
i i' : B
⊢ ((if Even m then i else i') :: alternatingWord i' i m).concat i' =
    (if Even (m + 1) then i' else i) :: (alternatingWord i' i m).concat i'

Tactic:
]

Goal state after:
case succ
B : Type u_1
m : ℕ
ih : ∀ (i i' : B), alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m
i i' : B
⊢ ((if Even m then i else i') :: alternatingWord i' i m).concat i' =
    (if Even (m + 1) then i' else i) :: (alternatingWord i' i m).concat i'
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : ¬p.head = 1
⊢ of ⟨i, p.head⟩.snd * (List.map (fun l ↦ of l.snd) p.tail.toList).prod =
    of p.head * (List.map (fun l ↦ of l.snd) p.tail.toList).prod

Tactic:
]

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

Goal state before:
pp: B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
⊢ (if Even (p + (k + 1)) then i else j) = if Even (p + k) then j else i

Tactic:
]

Goal state after:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
⊢ (if Even (p + (k + 1)) then i else j) = if Even (p + k) then j else i
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case pos
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
h_even : Even (p + k)
⊢ (if Even (p + k + 1) then i else j) = j

Tactic:
]

Goal state after:
case pos
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
h_even : Even (p + k)
⊢ (if Even (p + k + 1) then i else j) = j
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case neg
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
h_even : ¬Even (p + k)
⊢ (if Even (p + k + 1) then i else j) = i

Tactic:
]

Goal state after:
case neg
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
h_even : ¬Even (p + k)
⊢ (if Even (p + k + 1) then i else j) = i
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case neg
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
m' : M i
w' : Word M
h' : w'.fstIdx ≠ some i
hm : m = 1
hm' : ¬m' = 1
h : (cons m' w' ⋯ ⋯).fstIdx ≠ some i
he : w = cons m' w' ⋯ ⋯
⊢ False

Tactic:
]

Goal state after:
case neg
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
m' : M i
w' : Word M
h' : w'.fstIdx ≠ some i
hm : m = 1
hm' : ¬m' = 1
h : (cons m' w' ⋯ ⋯).fstIdx ≠ some i
he : w = cons m' w' ⋯ ⋯
⊢ False
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case pos
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx ≠ some i
m' : M i
w' : Word M
hm : ¬m = 1
h' : (cons m w ⋯ ⋯).fstIdx ≠ some i
hm' : m' = 1
he : cons m w ⋯ ⋯ = w'
⊢ False

Tactic:
]

Goal state after:
case pos
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx ≠ some i
m' : M i
w' : Word M
hm : ¬m = 1
h' : (cons m w ⋯ ⋯).fstIdx ≠ some i
hm' : m' = 1
he : cons m w ⋯ ⋯ = w'
⊢ False
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case pos
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord i j k
⊢ (take k (alternatingWord i j (2 * p))).concat (alternatingWord i j (2 * p))[k] =
    (take k (alternatingWord i j (2 * p))).concat i

Tactic:
]

Goal state after:
case pos
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord i j k
⊢ (take k (alternatingWord i j (2 * p))).concat (alternatingWord i j (2 * p))[k] =
    (take k (alternatingWord i j (2 * p))).concat i
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case cons.refine_1
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
motive : Word M → Sort u_4
empty : motive Word.empty
cons :
  (i : ι) → (m : M i) → (w : Word M) → (h1 : w.fstIdx ≠ some i) → (h2 : m ≠ 1) → motive w → motive (Word.cons m w h1 h2)
m : (i : ι) × M i
w : List ((i : ι) × M i)
ih :
  (h1 : ∀ l ∈ w, l.snd ≠ 1) →
    (h2 : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) w) → motive { toList := w, ne_one := h1, chain_ne := h2 }
h1 : ∀ l ∈ m :: w, l.snd ≠ 1
h2✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (m :: w)
h2 : (∀ y ∈ w.head?, m.fst ≠ y.fst) ∧ List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) w
⊢ { toList := w, ne_one := ⋯, chain_ne := ⋯ }.fstIdx ≠ some m.fst

Tactic:
]

Goal state after:
case cons.refine_1
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
motive : Word M → Sort u_4
empty : motive Word.empty
cons :
  (i : ι) → (m : M i) → (w : Word M) → (h1 : w.fstIdx ≠ some i) → (h2 : m ≠ 1) → motive w → motive (Word.cons m w h1 h2)
m : (i : ι) × M i
w : List ((i : ι) × M i)
ih :
  (h1 : ∀ l ∈ w, l.snd ≠ 1) →
    (h2 : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) w) → motive { toList := w, ne_one := h1, chain_ne := h2 }
h1 : ∀ l ∈ m :: w, l.snd ≠ 1
h2✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (m :: w)
h2 : (∀ y ∈ w.head?, m.fst ≠ y.fst) ∧ List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) w
⊢ { toList := w, ne_one := ⋯, chain_ne := ⋯ }.fstIdx ≠ some m.fst
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case pos
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord i j k
⊢ (if Even (2 * p + k) then i else j) = i

Tactic:
]

Goal state after:
case pos
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord i j k
⊢ (if Even (2 * p + k) then i else j) = i
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case neg
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : ¬Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord j i k
⊢ (alternatingWord j i k).concat (alternatingWord i j (2 * p))[k] = (alternatingWord j i k).concat j

Tactic:
]

Goal state after:
case neg
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : ¬Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord j i k
⊢ (alternatingWord j i k).concat (alternatingWord i j (2 * p))[k] = (alternatingWord j i k).concat j
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case neg
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : ¬Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord j i k
⊢ (if Even (2 * p + k) then i else j) = j

Tactic:
]

Goal state after:
case neg
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : ¬Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord j i k
⊢ (if Even (2 * p + k) then i else j) = j
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ (if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)) =
    i :: if Even k then alternatingWord j i k else alternatingWord i j k

Tactic:
]

Goal state after:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ (if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)) =
    i :: if Even k then alternatingWord j i k else alternatingWord i j k
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
h_even : Odd k
⊢ Even (k + 1)

Tactic:
]

Goal state after:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
h_even : Odd k
⊢ Even (k + 1)
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case succ
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
ih :
  cs.wordProd (alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)
⊢ cs.simple (if Even m then i' else i) *
      ((if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)) =
    (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)

Tactic:
]

Goal state after:
case succ
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
ih :
  cs.wordProd (alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)
⊢ cs.simple (if Even m then i' else i) *
      ((if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)) =
    (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)