theorem AffineReflectionGroup.group_maps_chamber_surj {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (C D : W.arrangement.Chamber) (w : E ≃ᵃⁱ[ℝ] E) (hw : w ∈ W.group) (h_maps : ∀ x ∈ C.set, w x ∈ D.set) (y : E) : y ∈ C.set ↔ w y ∈ D.set

If $w \in W$ maps every point of chamber $C$ into chamber $D$, then $w$ in fact gives a bijection $C \leftrightarrow D$: the implication promotes to an iff. This relies on maximality of chambers as connected components of the complement of the hyperplane arrangement.

theorem AffineReflectionGroup.gallery_connectivity_axiom {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (C D : W.arrangement.Chamber) : ∃ (reflections : List (E ≃ᵃⁱ[ℝ] E)), (∀ s ∈ reflections, s * s = 1 ∧ ∃ η ∈ W.arrangement.hyperplanes, ∀ y ∈ η.carrier, s y = y) ∧ ∀ (y : E), y ∈ D.set ↔ reflections.prod y ∈ C.set

Gallery connectivity: any two chambers $C, D$ are connected by a gallery, i.e. a list of reflections through walls such that the composition sends $D$ to $C$. Proved by induction on the number of separating hyperplanes.

theorem AffineReflectionGroup.list_prod_mem_group {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (G : Subgroup (E ≃ᵃⁱ[ℝ] E)) (l : List (E ≃ᵃⁱ[ℝ] E)) (hl : ∀ s ∈ l, s ∈ G) : l.prod ∈ G

A product of elements of a subgroup $G$ is in $G$.

theorem AffineReflectionGroup.involution_fixing_hyperplane_mem_group {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (s : E ≃ᵃⁱ[ℝ] E) (η : AffineHyperplane E) (hη : η ∈ W.arrangement.hyperplanes) (hs_inv : s * s = 1) (hs_fix : ∀ y ∈ η.carrier, s y = y) : s ∈ W.group

Any involution $s$ that fixes a hyperplane $\eta$ from the arrangement is the reflection in $\eta$ and hence is in $W$.

theorem AffineReflectionGroup.group_transitive_on_alcoves_aux {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (C D : W.Alcove) : ∃ w ∈ W.group, ∀ (y : E), y ∈ D.set ↔ w y ∈ C.set

Transitivity of $W$ on alcoves: for any two alcoves $C, D$ there exists $w \in W$ mapping $D$ bijectively onto $C$. Built by composing a gallery of wall reflections from gallery connectivity.