theorem DVRContext.iwahoriDecompositionGLn_base_case_exists (C : DVRContext) [C.DVRClosureGL2] (b : GL (Fin 2) C.k) : b ∈ C.IwahoriGLn 2 → ∃ (triple : GL (Fin 2) C.k × GL (Fin 2) C.k × GL (Fin 2) C.k), match triple with | (u', m, u) => u' ∈ C.LowerUnipGLn 2 ∩ C.IwahoriGLn 2 ∧ m ∈ C.DiagGLn 2 ∩ C.IwahoriGLn 2 ∧ u ∈ C.UpperUnipGLn 2 ∩ C.IwahoriGLn 2 ∧ b = u' * m * u

Existence half of the base case: each $b$ in the Iwahori subgroup of $\mathrm{GL}_2(k)$ admits some Iwahori factorisation $b = u' \cdot m \cdot u$.

theorem DVRContext.IwahoriDecompositionGLn_existence (C : DVRContext) [C.DVRClosureGL2] (n : ℕ) (hn : n ≥ 2) (b : GL (Fin n) C.k) : b ∈ C.IwahoriGLn n → ∃ (triple : GL (Fin n) C.k × GL (Fin n) C.k × GL (Fin n) C.k), match triple with | (u', m, u) => u' ∈ C.LowerUnipGLn n ∩ C.IwahoriGLn n ∧ m ∈ C.DiagGLn n ∩ C.IwahoriGLn n ∧ u ∈ C.UpperUnipGLn n ∩ C.IwahoriGLn n ∧ b = u' * m * u

Existence of the Iwahori decomposition for $\mathrm{GL}_n(k)$ for all $n \ge 2$: proved by induction on $n$ starting from the $n = 2$ base case and using the inductive clearing step.