Merge pull request #51 from NUS-Math-Formalization/new_lemmas

add two lemmas (proved) used in Rpoly.lean to CoxetrMatrix.Lemmas

Coxeter/CoxeterMatrix/Lemmas.lean

@@ -16,6 +16,12 @@ variable {G : Type*} {w : G} [hG:CoxeterGroup G]
 -- some lemmas are symmetric, such as muls_twice : w*s*s = w, the symm version is s*s*w = w.
 -- this section only contain lemmas that needed in Hecke.lean, you can also formulate the symms if u want.
 
+lemma ne_one_of_length_smul_lt {s : hG.S} {w:G} (lt: ℓ(s*w) < ℓ(w)) : w ≠ 1 := by
+  have : 0 < HOrderTwoGenGroup.length w := lt_of_le_of_lt (Nat.zero_le _) lt
+  contrapose! this
+  rw [HOrderTwoGenGroup.length]
+  apply (length_zero_iff_one (S := hG.S)).mpr at this
+  rw [this]
 
 lemma leftDescent_NE_of_ne_one (h : w ≠ 1) : Nonempty $ leftDescent w := by
   revert h
@@ -33,17 +39,21 @@ lemma leftDescent_NE_of_ne_one (h : w ≠ 1) : Nonempty $ leftDescent w := by
   rw [← length_eq_iff.mp this, ← length_eq_iff.mp hr]
   simp
 
+lemma ne_one_of_leftDescent_NE (h: Nonempty $ leftDescent w) : w ≠ 1 := by
+  let s:= Classical.choice h
+  have : ℓ(s*w) < ℓ(w) := (Set.mem_setOf.1 (Set.mem_of_mem_inter_left s.2)).2
+  exact ne_one_of_length_smul_lt (s:= ⟨s.1, Set.mem_of_mem_inter_right s.2⟩) this
+
 lemma rightDescent_NE_of_ne_one (h : w ≠ 1) : Nonempty $ rightDescent w := by
   rw [← inv_inv w, rightDescent_inv_eq_leftDescent]
   have : w⁻¹ ≠ 1 := by contrapose! h; exact inv_eq_one.mp h
   exact leftDescent_NE_of_ne_one this
 
-lemma ne_one_of_length_smul_lt {s : hG.S} {w:G} (lt: ℓ(s*w) < ℓ(w)) : w ≠ 1 := by
-  have : 0 < HOrderTwoGenGroup.length w := lt_of_le_of_lt (Nat.zero_le _) lt
+lemma ne_one_of_rightDescent_NE(h: Nonempty $ rightDescent w) : w ≠ 1 := by
+  rw [← inv_inv w, rightDescent_inv_eq_leftDescent] at h
+  have := ne_one_of_leftDescent_NE h
   contrapose! this
-  rw [HOrderTwoGenGroup.length]
-  apply (length_zero_iff_one (S := hG.S)).mpr at this
-  rw [this]
+  exact inv_eq_one.mpr this
 
 lemma length_smul_neq (s:hG.S) (w:G) : ℓ(s*w) ≠ ℓ(w) := by
   obtain ⟨L, hr, hL⟩ := @exists_reduced_word G _ hG.S _ w
@@ -54,7 +64,6 @@ lemma length_smul_neq (s:hG.S) (w:G) : ℓ(s*w) ≠ ℓ(w) := by
   linarith [List.removeNth_length L i,
     @length_le_list_length G _ hG.S _ (L.removeNth i)]
 
-
 lemma length_muls (w : G) (s : hG.S) : OrderTwoGen.length hG.S (w * s) = OrderTwoGen.length hG.S (s * w⁻¹) := by
   nth_rw 1 [← inv_inv (w * s)]
   rw [mul_inv_rev, inv_length_eq_length]
@@ -114,9 +123,17 @@ lemma length_muls_of_length_gt {s : hG.S} {w:G} (gt: ℓ(w) < ℓ(w * s)) : ℓ(
   repeat rw [← HOrderTwoGenGroup.length] at *
   exact length_smul_of_length_gt gt
 
-lemma length_muls_of_mem_leftDescent (s : leftDescent w) : ℓ(s*w) = ℓ(w) - 1 :=sorry
+lemma length_muls_of_mem_leftDescent (s : leftDescent w) : ℓ(s*w) = ℓ(w) - 1 := by
+  have hNE : Nonempty $ leftDescent w := Nonempty.intro s
+  have := ne_one_of_leftDescent_NE hNE
+  have hlt : ℓ(s*w) < ℓ(w) := Set.mem_setOf.1 (Set.mem_of_mem_inter_left s.2).2
+  exact length_smul_of_length_lt (s := ⟨s.1, Set.mem_of_mem_inter_right s.2⟩) hlt
 
-lemma length_muls_of_mem_rightDescent (s : rightDescent w) : ℓ(w*s) = ℓ(w) - 1 :=sorry
+lemma length_muls_of_mem_rightDescent (s : rightDescent w) : ℓ(w*s) = ℓ(w) - 1 := by
+  have hNE : Nonempty $ rightDescent w := Nonempty.intro s
+  have := ne_one_of_rightDescent_NE hNE
+  have hlt : ℓ(w*s) < ℓ(w) := Set.mem_setOf.1 (Set.mem_of_mem_inter_left s.2).2
+  exact length_muls_of_length_lt (s := ⟨s.1, Set.mem_of_mem_inter_right s.2⟩) hlt
 
 lemma muls_twice (w:G) (s:hG.S) : w*s*s = w := by
   rw [mul_assoc]