English
An induction principle consRecOn for NormalWord: to prove a property for any NormalWord, it suffices to prove it for the empty word, and to show that if it holds for w, it holds for cons g w under appropriate side-conditions.
Русский
Принцип индукции consRecOn для NormalWord: чтобы доказать свойство для любого NormalWord, достаточно доказать его для пустого слова, и показать, что если оно верно для w, тогда верно для cons g w при необходимых условиях.
LaTeX
$$$$\text{consRecOn} : \text{motive }(w) \Rightarrow \text{motive}(\text{cons } g w)$$$$
Lean4
/-- Induction principle for `NormalWord`, that corresponds closely to inducting on
the underlying list. -/
@[elab_as_elim]
noncomputable def consRecOn {motive : NormalWord d → Sort _} (w : NormalWord d) (empty : motive empty)
(cons :
∀ (i : ι) (g : G i) (w : NormalWord d) (hmw : w.fstIdx ≠ some i) (_hgn : g ∈ d.set i) (hgr : g ∉ (φ i).range)
(_hw1 : w.head = 1), motive w → motive (cons g w hmw hgr))
(base : ∀ (h : H) (w : NormalWord d), w.head = 1 → motive w → motive (base φ h • w)) : motive w :=
by
rcases w with ⟨w, head, h3⟩
convert base head ⟨w, 1, h3⟩ rfl ?_
· simp [base_smul_def]
·
induction w using Word.consRecOn with
| empty => exact empty
| cons i g w h1 hg1
ih =>
convert
cons i g ⟨w, 1, fun _ _ h => h3 _ _ (List.mem_cons_of_mem _ h)⟩ h1 (h3 _ _ List.mem_cons_self) ?_ rfl (ih ?_)
·
simp only [Word.cons, NormalWord.cons, map_one, mul_one,
(equiv_snd_eq_self_iff_mem (d.compl i) (one_mem _)).2 (h3 _ _ List.mem_cons_self)]
· apply d.injective i
simp only [NormalWord.cons, equiv_fst_eq_mul_inv, MonoidHom.apply_ofInjective_symm, map_one, mul_one,
mul_inv_cancel, (equiv_snd_eq_self_iff_mem (d.compl i) (one_mem _)).2 (h3 _ _ List.mem_cons_self)]
·
rwa [← SetLike.mem_coe, ← coe_equiv_snd_eq_one_iff_mem (d.compl i) (d.one_mem _),
(equiv_snd_eq_self_iff_mem (d.compl i) (one_mem _)).2 (h3 _ _ List.mem_cons_self)]
