English
A second variant of the induction principle for SkewMonoidAlgebra, mirroring the first with slightly different hypotheses.
Русский
Второй вариант принципа индукции для SkewMonoidAlgebra, повторяющий первый с немного изменёнными условиями.
LaTeX
$$$p f \Longrightarrow p (single a b) + f.erase a$$$
Lean4
@[elab_as_elim]
theorem induction {p : SkewMonoidAlgebra M α → Prop} (f : SkewMonoidAlgebra M α) (h0 : p 0)
(ha : ∀ (a b) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)) : p f :=
suffices ∀ (s) (f : SkewMonoidAlgebra M α), f.support = s → p f from this _ _ rfl
fun s ↦
Finset.cons_induction_on s (fun f hf ↦ by rwa [support_eq_empty.1 hf]) fun a s has ih f hf ↦
by
suffices p (single a (f.coeff a) + f.erase a) by rwa [single_add_erase] at this
classical
apply ha
· rw [support_erase, Finset.mem_erase]
exact fun H ↦ H.1 rfl
· simp only [← mem_support_iff, hf, Finset.mem_cons_self]
· apply ih
rw [support_erase, hf, Finset.erase_cons]
