chore(GroupTheory/Coxeter/Length): deprecate redundant theorems (leanprover-community#37155)

We deprecate `exists_reduced_word` and `exists_reduced_word'` in favor of a common `exists_isReduced`, which we accomplish by moving the definition `IsReduced` earlier in the file.

Author: vihdzp

Mathlib/GroupTheory/Coxeter/Length.lean

@@ -65,7 +65,7 @@ local prefix:100 "π " => cs.wordProd
 
 /-! ### Length -/
 
-private theorem exists_word_with_prod (w : W) : ∃ n ω, ω.length = n ∧ π ω = w := by
+private theorem exists_word_with_prod (w : W) : ∃ n ω, n = ω.length ∧ π ω = w := by
   rcases cs.wordProd_surjective w with ⟨ω, rfl⟩
   use ω.length, ω
 
@@ -76,10 +76,19 @@ must be multiplied to form `w`. -/
 
 local prefix:100 "ℓ " => cs.length
 
-theorem exists_reduced_word (w : W) : ∃ ω, ω.length = ℓ w ∧ w = π ω := by
+/-- The proposition that `ω` is reduced; that is, it has minimal length among all words that
+represent the same element of `W`. -/
+def IsReduced (ω : List B) : Prop := ℓ (π ω) = ω.length
+
+theorem IsReduced.eq {ω : List B} (hω : cs.IsReduced ω) : ℓ (π ω) = ω.length := hω
+
+theorem exists_isReduced (w : W) : ∃ ω : List B, cs.IsReduced ω ∧ w = π ω := by
   classical
-  have := Nat.find_spec (cs.exists_word_with_prod w)
-  tauto
+  obtain ⟨ω, hω, rfl⟩ := Nat.find_spec (cs.exists_word_with_prod w)
+  exact ⟨ω, hω, rfl⟩
+
+@[deprecated (since := "2026-03-25")] alias exists_reduced_word := exists_isReduced
+@[deprecated (since := "2026-03-25")] alias exists_reduced_word' := exists_isReduced
 
 open scoped Classical in
 theorem length_wordProd_le (ω : List B) : ℓ (π ω) ≤ ω.length :=
@@ -91,27 +100,27 @@ theorem length_wordProd_le (ω : List B) : ℓ (π ω) ≤ ω.length :=
 theorem length_eq_zero_iff {w : W} : ℓ w = 0 ↔ w = 1 := by
   constructor
   · intro h
-    rcases cs.exists_reduced_word w with ⟨ω, hω, rfl⟩
-    have : ω = [] := eq_nil_of_length_eq_zero (hω.trans h)
+    rcases cs.exists_isReduced w with ⟨ω, hω, rfl⟩
+    have : ω = [] := eq_nil_of_length_eq_zero (hω.symm.trans h)
     rw [this, wordProd_nil]
   · rintro rfl
     exact cs.length_one
 
 @[simp]
 theorem length_inv (w : W) : ℓ (w⁻¹) = ℓ w := by
   apply Nat.le_antisymm
-  · rcases cs.exists_reduced_word w with ⟨ω, hω, rfl⟩
-    have := cs.length_wordProd_le (List.reverse ω)
-    rwa [wordProd_reverse, length_reverse, hω] at this
-  · rcases cs.exists_reduced_word w⁻¹ with ⟨ω, hω, h'ω⟩
-    have := cs.length_wordProd_le (List.reverse ω)
-    rwa [wordProd_reverse, length_reverse, ← h'ω, hω, inv_inv] at this
+  · rcases cs.exists_isReduced w with ⟨ω, hω, rfl⟩
+    have := cs.length_wordProd_le ω.reverse
+    rwa [wordProd_reverse, length_reverse, ← hω] at this
+  · rcases cs.exists_isReduced w⁻¹ with ⟨ω, hω, h'ω⟩
+    have := cs.length_wordProd_le ω.reverse
+    rwa [wordProd_reverse, length_reverse, ← h'ω, ← hω, inv_inv, ← h'ω] at this
 
 theorem length_mul_le (w₁ w₂ : W) : ℓ (w₁ * w₂) ≤ ℓ w₁ + ℓ w₂ := by
-  rcases cs.exists_reduced_word w₁ with ⟨ω₁, hω₁, rfl⟩
-  rcases cs.exists_reduced_word w₂ with ⟨ω₂, hω₂, rfl⟩
+  rcases cs.exists_isReduced w₁ with ⟨ω₁, hω₁, rfl⟩
+  rcases cs.exists_isReduced w₂ with ⟨ω₂, hω₂, rfl⟩
   have := cs.length_wordProd_le (ω₁ ++ ω₂)
-  simpa [hω₁, hω₂, wordProd_append] using this
+  simpa [hω₁.eq, hω₂.eq, wordProd_append] using this
 
 theorem length_le_length_mul_add_left (w₁ w₂ : W) : ℓ w₂ ≤ ℓ (w₁ * w₂) + ℓ w₁ := by
   simpa [add_comm] using cs.length_mul_le w₁⁻¹ (w₁ * w₂)
@@ -147,8 +156,8 @@ theorem lengthParity_comp_simple :
 
 theorem lengthParity_eq_ofAdd_length (w : W) :
     cs.lengthParity w = Multiplicative.ofAdd (↑(ℓ w)) := by
-  rcases cs.exists_reduced_word w with ⟨ω, hω, rfl⟩
-  rw [← hω, wordProd, map_list_prod, List.map_map, lengthParity_comp_simple, map_const',
+  rcases cs.exists_isReduced w with ⟨ω, hω, rfl⟩
+  rw [hω, wordProd, map_list_prod, List.map_map, lengthParity_comp_simple, map_const',
     prod_replicate, ← ofAdd_nsmul, nsmul_one]
 
 theorem length_mul_mod_two (w₁ w₂ : W) : ℓ (w₁ * w₂) % 2 = (ℓ w₁ + ℓ w₂) % 2 := by
@@ -169,8 +178,8 @@ theorem length_simple (i : B) : ℓ (s i) = 1 := by
 theorem length_eq_one_iff {w : W} : ℓ w = 1 ↔ ∃ i : B, w = s i := by
   constructor
   · intro h
-    rcases cs.exists_reduced_word w with ⟨ω, hω, rfl⟩
-    rcases List.length_eq_one_iff.mp (hω.trans h) with ⟨i, rfl⟩
+    rcases cs.exists_isReduced w with ⟨ω, hω, rfl⟩
+    rcases List.length_eq_one_iff.mp (hω.symm.trans h) with ⟨i, rfl⟩
     exact ⟨i, cs.wordProd_singleton i⟩
   · rintro ⟨i, rfl⟩
     exact cs.length_simple i
@@ -198,10 +207,6 @@ theorem length_simple_mul (w : W) (i : B) : ℓ (s i * w) = ℓ w + 1 ∨ ℓ (s
 
 /-! ### Reduced words -/
 
-/-- The proposition that `ω` is reduced; that is, it has minimal length among all words that
-represent the same element of `W`. -/
-def IsReduced (ω : List B) : Prop := ℓ (π ω) = ω.length
-
 @[simp]
 theorem isReduced_reverse_iff (ω : List B) : cs.IsReduced (ω.reverse) ↔ cs.IsReduced ω := by
   simp [IsReduced]
@@ -210,10 +215,6 @@ theorem IsReduced.reverse {cs : CoxeterSystem M W} {ω : List B}
     (hω : cs.IsReduced ω) : cs.IsReduced (ω.reverse) :=
   (cs.isReduced_reverse_iff ω).mpr hω
 
-theorem exists_reduced_word' (w : W) : ∃ ω : List B, cs.IsReduced ω ∧ w = π ω := by
-  rcases cs.exists_reduced_word w with ⟨ω, hω, rfl⟩
-  use ω
-  tauto
 
 private theorem isReduced_take_and_drop {ω : List B} (hω : cs.IsReduced ω) (j : ℕ) :
     cs.IsReduced (ω.take j) ∧ cs.IsReduced (ω.drop j) := by
@@ -283,11 +284,11 @@ theorem isRightDescent_inv_iff {w : W} {i : B} :
   simpa using (cs.isLeftDescent_inv_iff (w := w⁻¹)).symm
 
 theorem exists_leftDescent_of_ne_one {w : W} (hw : w ≠ 1) : ∃ i : B, cs.IsLeftDescent w i := by
-  rcases cs.exists_reduced_word w with ⟨ω, h, rfl⟩
+  rcases cs.exists_isReduced w with ⟨ω, h, rfl⟩
   have h₁ : ω ≠ [] := by rintro rfl; simp at hw
   rcases List.exists_cons_of_ne_nil h₁ with ⟨i, ω', rfl⟩
   use i
-  rw [IsLeftDescent, ← h, wordProd_cons, simple_mul_simple_cancel_left]
+  rw [IsLeftDescent, h, wordProd_cons, simple_mul_simple_cancel_left]
   calc
     ℓ (π ω') ≤ ω'.length := cs.length_wordProd_le ω'
     _ < (i :: ω').length := by simp