theorem CellCover.B_mem_bruhatCell_one {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) {b : G} (hb : b ∈ bp.B) : b ∈ bp.bruhatCell 1

Any $b \in B$ lies in the identity Bruhat cell $C(1) = B \cdot T \cdot B$.

theorem CellCover.bruhatCell_mul_B_right {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) {w : M.Group} {g b : G} (hg : g ∈ bp.bruhatCell w) (hb : b ∈ bp.B) : g * b ∈ bp.bruhatCell w

Right $B$-absorption: $C(w) \cdot B \subseteq C(w)$.

theorem CellCover.bruhatCell_mul_N_simple {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) {w : M.Group} {g : G} (hg : g ∈ bp.bruhatCell w) {n : ↥bp.N} {s : B_idx} (hn : bp.π n = M.toCoxeterSystem.simple s) : ∃ (u : M.Group), g * ↑n ∈ bp.bruhatCell u

Multiplying $g \in C(w)$ by a lift $n \in N$ of a simple reflection $s$ lands in some Bruhat cell.

theorem CellCover.bruhatCell_mul_N {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) {w : M.Group} {g : G} (hg : g ∈ bp.bruhatCell w) (n : ↥bp.N) : ∃ (u : M.Group), g * ↑n ∈ bp.bruhatCell u

Generalization to arbitrary $n \in N$: multiplying $g \in C(w)$ by any element of $N$ lands in some Bruhat cell, by induction on a simple-reflection word for $\pi(n)$.

theorem CellCover.cell_cover_from_bnpair {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (g : G) : ∃ (w : M.Group), g ∈ bp.bruhatCell w

Bruhat cell cover: $G = \bigcup_{w \in W} BwB$. Every element of $G$ lies in some Bruhat cell, proven by induction on a generating word in $B \cup N$.