English
If p(1) holds and p is preserved when left-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(s_i) → p(w) → p(s_i w)) and closure$$
Lean4
/-- If `p : W → Prop` holds for the identity and it is preserved under multiplying on the left
by a simple reflection, then it holds for all elements of `W`. -/
theorem simple_induction_left {p : W → Prop} (w : W) (one : p 1)
(mul_simple_left : ∀ (w : W) (i : B), p w → p (s i * w)) : 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_left with
| one => exact one
| mul_left i mi y my ih =>
rw [Set.mem_range] at mi
exact mi.choose_spec ▸ mul_simple_left _ _ ih
