English
If p(1) holds and p is preserved when right-multiplying by a simple reflection, then p holds for every w ∈ W.
Русский
Если p(1) верно и сохраняется при правом умножении на простое отражение, то p верно для каждого w ∈ W.
LaTeX
$$p(w) if p(1) and (∀ i, p(w) → p(s_i) → p(w s_i)) and closure$$
Lean4
/-- If `p : W → Prop` holds for the identity and it is preserved under multiplying on the right
by a simple reflection, then it holds for all elements of `W`. -/
theorem simple_induction_right {p : W → Prop} (w : W) (one : p 1)
(mul_simple_right : ∀ (w : W) (i : B), p w → p (w * s i)) : p w :=
by
let p' : ((w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop) := fun w _ ↦ p w
have := cs.submonoid_closure_range_simple.symm ▸ Submonoid.mem_top w
induction this using Submonoid.closure_induction_right with
| one => exact one
| mul_right y my i mi ih =>
rw [Set.mem_range] at mi
exact mi.choose_spec ▸ mul_simple_right _ _ ih
