English
A variant of the Weyl group induction requiring Nonempty ι; it deduces pred for any WeylGroup element using the same base steps as the standard induction.
Русский
Вариант индукции Weyl-группы, требующий не пустого ι; выводит предикат для любого элемента Weyl-группы по тем же базовым шагам индукции.
LaTeX
$$$\\text{If } ι \\text{ is nonempty, then the same induction as above applies under a single reflection argument.}$$$
Lean4
@[elab_as_elim]
theorem induction' [Nonempty ι] {pred : (g : Aut P) → g ∈ P.weylGroup → Prop}
(mem : ∀ i, pred (Equiv.reflection P i) (P.reflection_mem_weylGroup i))
(mul : ∀ x y hx hy, pred x hx → pred y hy → pred (x * y) (mul_mem hx hy)) {x} (hx : x ∈ P.weylGroup) : pred x hx :=
by
refine weylGroup.induction P mem ?_ mul hx
obtain ⟨i⟩ : Nonempty ι := inferInstance
have : (Equiv.reflection P i) ^ 2 = 1 := by rw [sq, mul_eq_one_iff_inv_eq, Equiv.reflection_inv P i]
simpa [sq, ← this] using mul _ _ _ _ (mem i) (mem i)
