awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m_1 : ℕ
hM : M.M i i' ≠ 0
m_2 : ℕ
m : (M.M i i').succ.le m_2
ih : cs.IsReduced (alternatingWord i i' m_2.succ)
⊢ cs.IsReduced ((if Even m_2 then i' else i) :: alternatingWord i i' m_2)

Tactic:
rw [alternatingWord_succ'] at ih

Premises used: CoxeterSystem.alternatingWord_succ'
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m_1 : ℕ
hM : M.M i i' ≠ 0
m_2 : ℕ
m : (M.M i i').succ.le m_2
ih : cs.IsReduced ((if Even m_2 then i' else i) :: alternatingWord i i' m_2)
⊢ cs.IsReduced (drop 1 ((if Even m_2 then i' else i) :: alternatingWord i i' m_2))

Tactic:
apply IsReduced.drop (j := 1) at ih

Premises used: CoxeterSystem.IsReduced.drop, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m_1 : ℕ
hM : M.M i i' ≠ 0
m_2 : ℕ
m : (M.M i i').succ.le m_2
ih : cs.IsReduced (drop 1 ((if Even m_2 then i' else i) :: alternatingWord i i' m_2))
⊢ cs.IsReduced (alternatingWord i i' m_2)

Tactic:
simpa using ih
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
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
hm : m > M.M i i'
refl : ¬cs.IsReduced (alternatingWord i i' (M.M i i').succ)
step :
  ∀ {m : ℕ} (m_1 : (M.M i i').succ.le m) (ih : ¬cs.IsReduced (alternatingWord i i' m)),
    ¬cs.IsReduced (alternatingWord i i' m.succ)
⊢ ¬cs.IsReduced (alternatingWord i i' m)

Tactic:
induction hm with
  | refl => -- Base case; m = M i i' + 1
    suffices h : ℓ (π (alternatingWord i i' (M i i' + 1))) < M i i' + 1 by
      unfold IsReduced
      rw [Nat.succ_eq_add_one, length_alternatingWord]
      lia
    have : M i i' + 1 ≤ M i i' * 2 := by linarith [Nat.one_le_iff_ne_zero.mpr hM]
    rw [cs.prod_alternatingWord_eq_prod_alternatingWord_sub i i' _ this]
    have : M i i' * 2 - (M i i' + 1) = M i i' - 1 := by lia
    rw [this]
    calc
      ℓ (π (alternatingWord i' i (M i i' - 1)))
      _ ≤ (alternatingWord i' i (M i i' - 1)).length := cs.length_wordProd_le _
      _ = M i i' - 1 := length_alternatingWord _ _ _
      _ ≤ M i i' := Nat.sub_le _ _
      _ < M i i' + 1 := Nat.lt_succ_self _
  | step m ih => -- Inductive step
    contrapose ih
    rw [alternatingWord_succ'] at ih
    apply IsReduced.drop (j := 1) at ih
    simpa using ih

Premises used: CoxeterSystem.IsReduced.drop, CoxeterMatrix.M, HSub.hSub, Nat.lt_succ_self, Nat.sub_le, CoxeterSystem.alternatingWord, CoxeterSystem.length_wordProd_le, CoxeterSystem.alternatingWord_succ', OfNat.ofNat, refl, List.length, CoxeterSystem.length_alternatingWord
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ ¬cs.IsLeftDescent 1 i

Tactic:
simp [IsLeftDescent]

Premises used: CoxeterSystem.IsLeftDescent
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ ¬cs.IsRightDescent 1 i

Tactic:
simp [IsRightDescent]

Premises used: CoxeterSystem.IsRightDescent
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
nth_rw : cs.length (cs.simple i * w⁻¹)⁻¹ < cs.length w⁻¹ ↔ cs.length (w * cs.simple i) < cs.length w
⊢ cs.length (cs.simple i * w⁻¹) < cs.length w⁻¹ ↔ cs.length (w * cs.simple i) < cs.length w

Tactic:
nth_rw 1 [← length_inv]

Premises used: CoxeterSystem.length_inv
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
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:
simp
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.IsRightDescent w⁻¹ i ↔ cs.IsLeftDescent w i

Tactic:
simpa using (cs.isLeftDescent_inv_iff (w := w⁻¹)).symm

Premises used: CoxeterSystem.isLeftDescent_inv_iff, Iff.symm
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
hw : w ≠ 1
rcases : ∀ (ω : List B) (h : cs.IsReduced ω) (hw : cs.wordProd ω ≠ 1), ∃ (i : B), cs.IsLeftDescent (cs.wordProd ω) i
⊢ ∃ (i : B), cs.IsLeftDescent w i

Tactic:
rcases cs.exists_isReduced w with ⟨ω, h, rfl⟩

Premises used: CoxeterSystem.exists_isReduced, rfl
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
h : cs.IsReduced []
hw : cs.wordProd [] ≠ 1
⊢ False

Tactic:
simp at hw
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
h : cs.IsReduced ω
hw : cs.wordProd ω ≠ 1
⊢ ω ≠ []

Tactic:
have h₁ : ω ≠ [] := by rintro rfl; simp at hw
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
h : cs.IsReduced ω
hw : cs.wordProd ω ≠ 1
h₁ : ω ≠ []
rcases :
  ∀ (i : B) (ω' : List B) (h : cs.IsReduced (i :: ω')) (hw : cs.wordProd (i :: ω') ≠ 1) (h₁ : i :: ω' ≠ []),
    ∃ (i_1 : B), cs.IsLeftDescent (cs.wordProd (i :: ω')) i_1
⊢ ∃ (i : B), cs.IsLeftDescent (cs.wordProd ω) i

Tactic:
rcases List.exists_cons_of_ne_nil h₁ with ⟨i, ω', rfl⟩

Premises used: List.exists_cons_of_ne_nil, rfl
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
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 :: ω' ≠ []
h₂ : cs.IsLeftDescent (cs.wordProd (i :: ω')) i
⊢ ∃ (i_1 : B), cs.IsLeftDescent (cs.wordProd (i :: ω')) i_1

Tactic:
use i
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
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 :: ω' ≠ []
h₂ : cs.length (cs.wordProd ω') < (i :: ω').length
⊢ cs.IsLeftDescent (cs.wordProd (i :: ω')) i

Tactic:
rw [IsLeftDescent, h, wordProd_cons, simple_mul_simple_cancel_left]

Premises used: CoxeterSystem.IsLeftDescent, CoxeterSystem.wordProd_cons, CoxeterSystem.simple_mul_simple_cancel_left
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
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 ω') ≤ ω'.length

Tactic:
cs.length_wordProd_le ω'

Premises used: CoxeterSystem.length_wordProd_le
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
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 :: ω' ≠ []
⊢ ω'.length < (i :: ω').length

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
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 :: ω' ≠ []
ℓ : ω'.length < (i :: ω').length
⊢ cs.length (cs.wordProd ω') < (i :: ω').length

Tactic:
calc
    ℓ (π ω') ≤ ω'.length := cs.length_wordProd_le ω'
    _ < (i :: ω').length := by simp

Premises used: CoxeterSystem.length_wordProd_le, List.cons, List.length
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
hw : w ≠ 1
simp : ∃ (i : B), cs.IsLeftDescent w⁻¹ i
⊢ ∃ (i : B), cs.IsRightDescent w i

Tactic:
simp only [← isLeftDescent_inv_iff]

Premises used: CoxeterSystem.isLeftDescent_inv_iff
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
hw : w ≠ 1
hw₁ : w⁻¹ ≠ 1
⊢ ∃ (i : B), cs.IsLeftDescent w⁻¹ i

Tactic:
apply exists_leftDescent_of_ne_one

Premises used: CoxeterSystem.exists_leftDescent_of_ne_one
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
hw : w ≠ 1
⊢ w⁻¹ ≠ 1

Tactic:
simpa
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
mp : cs.length (cs.simple i * w) < cs.length w → cs.length (cs.simple i * w) + 1 = cs.length w
mpr : cs.length (cs.simple i * w) + 1 = cs.length w → cs.length (cs.simple i * w) < cs.length w
⊢ cs.length (cs.simple i * w) < cs.length w ↔ cs.length (cs.simple i * w) + 1 = cs.length w

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
h : cs.length (cs.simple i * w) < cs.length w
⊢ ¬cs.length (cs.simple i * w) = cs.length w + 1

Tactic:
lia
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
h : cs.length (cs.simple i * w) < cs.length w
⊢ cs.length (cs.simple i * w) + 1 = cs.length w

Tactic:
exact (cs.length_simple_mul w i).resolve_left (by lia)

Premises used: CoxeterSystem.length_simple_mul, Or.resolve_left
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
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 (cs.simple i * w) < cs.length w

Tactic:
lia
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
mp : ¬cs.length (cs.simple i * w) < cs.length w → cs.length (cs.simple i * w) = cs.length w + 1
mpr : cs.length (cs.simple i * w) = cs.length w + 1 → ¬cs.length (cs.simple i * w) < cs.length w
⊢ ¬cs.length (cs.simple i * w) < cs.length w ↔ cs.length (cs.simple i * w) = cs.length w + 1

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
h : ¬cs.length (cs.simple i * w) < cs.length w
⊢ ¬cs.length (cs.simple i * w) + 1 = cs.length w

Tactic:
lia
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
h : ¬cs.length (cs.simple i * w) < cs.length w
⊢ cs.length (cs.simple i * w) = cs.length w + 1

Tactic:
exact (cs.length_simple_mul w i).resolve_right (by lia)

Premises used: CoxeterSystem.length_simple_mul, Or.resolve_right
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
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) < cs.length w

Tactic:
lia
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
mp : cs.length (w * cs.simple i) < cs.length w → cs.length (w * cs.simple i) + 1 = cs.length w
mpr : cs.length (w * cs.simple i) + 1 = cs.length w → cs.length (w * cs.simple i) < cs.length w
⊢ cs.length (w * cs.simple i) < cs.length w ↔ cs.length (w * cs.simple i) + 1 = cs.length w

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
h : cs.length (w * cs.simple i) < cs.length w
⊢ ¬cs.length (w * cs.simple i) = cs.length w + 1

Tactic:
lia
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
h : cs.length (w * cs.simple i) < cs.length w
⊢ cs.length (w * cs.simple i) + 1 = cs.length w

Tactic:
exact (cs.length_mul_simple w i).resolve_left (by lia)

Premises used: CoxeterSystem.length_mul_simple, Or.resolve_left
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
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.simple i) < cs.length w

Tactic:
lia
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
mp : ¬cs.length (w * cs.simple i) < cs.length w → cs.length (w * cs.simple i) = cs.length w + 1
mpr : cs.length (w * cs.simple i) = cs.length w + 1 → ¬cs.length (w * cs.simple i) < cs.length w
⊢ ¬cs.length (w * cs.simple i) < cs.length w ↔ cs.length (w * cs.simple i) = cs.length w + 1

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
h : ¬cs.length (w * cs.simple i) < cs.length w
⊢ ¬cs.length (w * cs.simple i) + 1 = cs.length w

Tactic:
lia
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
h : ¬cs.length (w * cs.simple i) < cs.length w
⊢ cs.length (w * cs.simple i) = cs.length w + 1

Tactic:
exact (cs.length_mul_simple w i).resolve_right (by lia)

Premises used: CoxeterSystem.length_mul_simple, Or.resolve_right
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
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) < cs.length w

Tactic:
lia
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
rw : cs.length (cs.simple i * w) + 1 = cs.length w ↔ cs.length w = cs.length (cs.simple i * w) + 1
⊢ cs.IsLeftDescent w i ↔ ¬cs.IsLeftDescent (cs.simple i * w) i

Tactic:
rw [isLeftDescent_iff, not_isLeftDescent_iff, simple_mul_simple_cancel_left]

Premises used: CoxeterSystem.not_isLeftDescent_iff, CoxeterSystem.isLeftDescent_iff, CoxeterSystem.simple_mul_simple_cancel_left
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
mp : cs.length (cs.simple i * w) + 1 = cs.length w → cs.length w = cs.length (cs.simple i * w) + 1
mpr : cs.length w = cs.length (cs.simple i * w) + 1 → cs.length (cs.simple i * w) + 1 = cs.length w
mp₁ mp₂ mp₃ : cs.length (cs.simple i * w) + 1 = cs.length w → cs.length w = cs.length (cs.simple i * w) + 1
mpr₁ mpr₂ mpr₃ : cs.length w = cs.length (cs.simple i * w) + 1 → cs.length (cs.simple i * w) + 1 = cs.length w
mp₄ mp₅ mp₆ : cs.length (cs.simple i * w) + 1 = cs.length w → cs.length w = cs.length (cs.simple i * w) + 1
mpr₄ mpr₅ mpr₆ : cs.length w = cs.length (cs.simple i * w) + 1 → cs.length (cs.simple i * w) + 1 = cs.length w
mp₇ mp₈ : cs.length (cs.simple i * w) + 1 = cs.length w → cs.length w = cs.length (cs.simple i * w) + 1
mpr₇ mpr₈ : cs.length w = cs.length (cs.simple i * w) + 1 → cs.length (cs.simple i * w) + 1 = cs.length w
⊢ cs.length (cs.simple i * w) + 1 = cs.length w ↔ cs.length w = cs.length (cs.simple i * w) + 1

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
rw : cs.length (w * cs.simple i) + 1 = cs.length w ↔ cs.length w = cs.length (w * cs.simple i) + 1
⊢ cs.IsRightDescent w i ↔ ¬cs.IsRightDescent (w * cs.simple i) i

Tactic:
rw [isRightDescent_iff, not_isRightDescent_iff, simple_mul_simple_cancel_right]

Premises used: CoxeterSystem.isRightDescent_iff, CoxeterSystem.not_isRightDescent_iff, CoxeterSystem.simple_mul_simple_cancel_right
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
mp : cs.length (w * cs.simple i) + 1 = cs.length w → cs.length w = cs.length (w * cs.simple i) + 1
mpr : cs.length w = cs.length (w * cs.simple i) + 1 → cs.length (w * cs.simple i) + 1 = cs.length w
mp₁ mp₂ mp₃ : cs.length (w * cs.simple i) + 1 = cs.length w → cs.length w = cs.length (w * cs.simple i) + 1
mpr₁ mpr₂ mpr₃ : cs.length w = cs.length (w * cs.simple i) + 1 → cs.length (w * cs.simple i) + 1 = cs.length w
mp₄ mp₅ mp₆ : cs.length (w * cs.simple i) + 1 = cs.length w → cs.length w = cs.length (w * cs.simple i) + 1
mpr₄ mpr₅ mpr₆ : cs.length w = cs.length (w * cs.simple i) + 1 → cs.length (w * cs.simple i) + 1 = cs.length w
mp₇ mp₈ : cs.length (w * cs.simple i) + 1 = cs.length w → cs.length w = cs.length (w * cs.simple i) + 1
mpr₇ mpr₈ : cs.length w = cs.length (w * cs.simple i) + 1 → cs.length (w * cs.simple i) + 1 = cs.length w
⊢ cs.length (w * cs.simple i) + 1 = cs.length w ↔ cs.length w = cs.length (w * cs.simple i) + 1

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Coxeter.Matrix
Goal:
B : Type u_1
M : CoxeterMatrix B
i i' : B
⊢ M.M i i' = M.M i' i

Tactic:
M.isSymm.apply i' i

Premises used: CoxeterMatrix.isSymm, Matrix.IsSymm.apply
-- Module: Mathlib.GroupTheory.Coxeter.Matrix
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
i i' : B'
⊢ (CoxeterMatrix.reindex e M).M i i' = M.M ((e.symm : (a : B') → B) i) ((e.symm : (a : B') → B) i')

Tactic:
rfl

Premises used: Matrix.submatrix, rfl
-- Module: Mathlib.GroupTheory.Coxeter.Matrix
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ Eq (α := Matrix (Fin n) (Fin n) ℕ)
    (Matrix.transpose
      ((Matrix.of : (a : Fin n → Fin n → ℕ) → Matrix (Fin n) (Fin n) ℕ) fun (i j : Fin n) ↦
        if i = j then 1 else if (↑j : ℕ) + 1 = (↑i : ℕ) ∨ (↑i : ℕ) + 1 = (↑j : ℕ) then 3 else 2))
    ((Matrix.of : (a : Fin n → Fin n → ℕ) → Matrix (Fin n) (Fin n) ℕ) fun (i j : Fin n) ↦
      if i = j then 1 else if (↑j : ℕ) + 1 = (↑i : ℕ) ∨ (↑i : ℕ) + 1 = (↑j : ℕ) then 3 else 2)

Tactic:
aesop
-- Module: Mathlib.GroupTheory.Coxeter.Matrix
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ ∀ (i : Fin n),
    Eq (α := ℕ)
      ((Matrix.of : (a : Fin n → Fin n → ℕ) → Matrix (Fin n) (Fin n) ℕ)
          (fun (i j : Fin n) ↦ if i = j then 1 else if (↑j : ℕ) + 1 = (↑i : ℕ) ∨ (↑i : ℕ) + 1 = (↑j : ℕ) then 3 else 2)
          i i :
        ℕ)
      (1 : ℕ)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coxeter.Matrix
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ ∀ (i i' : Fin n),
    i ≠ i' →
      Ne (α := ℕ)
        ((Matrix.of : (a : Fin n → Fin n → ℕ) → Matrix (Fin n) (Fin n) ℕ)
            (fun (i j : Fin n) ↦
              if i = j then 1 else if (↑j : ℕ) + 1 = (↑i : ℕ) ∨ (↑i : ℕ) + 1 = (↑j : ℕ) then 3 else 2)
            i i' :
          ℕ)
        (1 : ℕ)

Tactic:
aesop
-- Module: Mathlib.GroupTheory.Coxeter.Matrix
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ Eq (α := Matrix (Fin n) (Fin n) ℕ)
    (Matrix.transpose
      ((Matrix.of : (a : Fin n → Fin n → ℕ) → Matrix (Fin n) (Fin n) ℕ) fun (i j : Fin n) ↦
        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))
    ((Matrix.of : (a : Fin n → Fin n → ℕ) → Matrix (Fin n) (Fin n) ℕ) fun (i j : Fin n) ↦
      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)

Tactic:
aesop
-- Module: Mathlib.GroupTheory.Coxeter.Matrix
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ ∀ (i : Fin n),
    Eq (α := ℕ)
      ((Matrix.of : (a : Fin n → Fin n → ℕ) → Matrix (Fin n) (Fin n) ℕ)
          (fun (i j : Fin n) ↦
            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:
simp
-- Module: Mathlib.GroupTheory.Coxeter.Matrix
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ ∀ (i i' : Fin n),
    i ≠ i' →
      Ne (α := ℕ)
        ((Matrix.of : (a : Fin n → Fin n → ℕ) → Matrix (Fin n) (Fin n) ℕ)
            (fun (i j : Fin n) ↦
              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:
aesop
-- Module: Mathlib.GroupTheory.Coxeter.Matrix
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ Eq (α := Matrix (Fin n) (Fin n) ℕ)
    (Matrix.transpose
      ((Matrix.of : (a : Fin n → Fin n → ℕ) → Matrix (Fin n) (Fin n) ℕ) fun (i j : Fin n) ↦
        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))
    ((Matrix.of : (a : Fin n → Fin n → ℕ) → Matrix (Fin n) (Fin n) ℕ) fun (i j : Fin n) ↦
      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)

Tactic:
aesop
-- Module: Mathlib.GroupTheory.Coxeter.Matrix
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ ∀ (i : Fin n),
    Eq (α := ℕ)
      ((Matrix.of : (a : Fin n → Fin n → ℕ) → Matrix (Fin n) (Fin n) ℕ)
          (fun (i j : Fin n) ↦
            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:
simp
-- Module: Mathlib.GroupTheory.Coxeter.Matrix
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ ∀ (i i' : Fin n),
    i ≠ i' →
      Ne (α := ℕ)
        ((Matrix.of : (a : Fin n → Fin n → ℕ) → Matrix (Fin n) (Fin n) ℕ)
            (fun (i j : Fin n) ↦
              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:
aesop
-- Module: Mathlib.GroupTheory.Coxeter.Matrix
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n m : ℕ
⊢ Eq (α := Matrix (Fin 2) (Fin 2) ℕ)
    (Matrix.transpose
      ((Matrix.of : (a : Fin 2 → Fin 2 → ℕ) → Matrix (Fin 2) (Fin 2) ℕ) fun (i j : Fin 2) ↦ if i = j then 1 else m + 2))
    ((Matrix.of : (a : Fin 2 → Fin 2 → ℕ) → Matrix (Fin 2) (Fin 2) ℕ) fun (i j : Fin 2) ↦ if i = j then 1 else m + 2)

Tactic:
aesop
-- Module: Mathlib.GroupTheory.Coxeter.Matrix
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n m : ℕ
⊢ ∀ (i : Fin 2),
    Eq (α := ℕ)
      ((Matrix.of : (a : Fin 2 → Fin 2 → ℕ) → Matrix (Fin 2) (Fin 2) ℕ) (fun (i j : Fin 2) ↦ if i = j then 1 else m + 2)
          i i :
        ℕ)
      (1 : ℕ)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coxeter.Matrix
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n m : ℕ
⊢ ∀ (i i' : Fin 2),
    i ≠ i' →
      Ne (α := ℕ)
        ((Matrix.of : (a : Fin 2 → Fin 2 → ℕ) → Matrix (Fin 2) (Fin 2) ℕ)
            (fun (i j : Fin 2) ↦ if i = j then 1 else m + 2) i i' :
          ℕ)
        (1 : ℕ)

Tactic:
simp
-- Module: Mathlib.GroupTheory.DedekindFinite
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Finite M
a b : M
hab : a * b = 1
have : ∀ (c : M) (hbc : Eq.{u_1 + 1} (α := M) ((fun (x : M) ↦ b * x) c) 1), b * a = 1
⊢ b * a = 1

Tactic:
have ⟨c, hbc⟩ := Finite.surjective_of_injective (isLeftRegular_of_mul_eq_one hab) 1