theorem DVRContext.fin2_lt_iff (i j : Fin 2) : ↑i < ↑j ↔ i = 0 ∧ j = 1

Strict inequality of Fin 2 values: $i < j$ iff $(i, j) = (0, 1)$.

theorem DVRContext.fin2_gt_iff (i j : Fin 2) : ↑i > ↑j ↔ i = 1 ∧ j = 0

Strict inequality of Fin 2 values, swapped: $i > j$ iff $(i, j) = (1, 0)$.

theorem DVRContext.iwahoriGLn_eq_iwahoriGL2 (C : DVRContext) [C.DVRClosureGL2] : C.IwahoriGLn 2 = C.IwahoriGL2

Identification of the general $\mathrm{GL}_n$ definition of the Iwahori subgroup at $n = 2$ with the concrete $\mathrm{GL}_2$ definition.

theorem DVRContext.upperUnipGLn_eq_upperUnipGL2 (C : DVRContext) [C.DVRClosureGL2] : C.UpperUnipGLn 2 = C.UpperUnipGL2

Identification of the general upper unipotent subgroup at $n = 2$ with the concrete $\mathrm{GL}_2$ version.

theorem DVRContext.lowerUnipGLn_eq_lowerUnipGL2 (C : DVRContext) [C.DVRClosureGL2] : C.LowerUnipGLn 2 = C.LowerUnipGL2

Identification of the general lower unipotent subgroup at $n = 2$ with the concrete $\mathrm{GL}_2$ version.

theorem DVRContext.diagGLn_eq_diagGL2 (C : DVRContext) [C.DVRClosureGL2] : C.DiagGLn 2 = C.DiagGL2

Identification of the general diagonal subgroup at $n = 2$ with the concrete $\mathrm{GL}_2$ version.

theorem DVRContext.iwahoriDecompositionGLn_base_case (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

Base case ($n = 2$) of the Iwahori decomposition for $\mathrm{GL}_n$: every Iwahori element factors uniquely as $u' \cdot m \cdot u$, obtained from the concrete $\mathrm{GL}_2$ result.