English
Let P be a property on Π₀ i, β i. If P(0) holds and for all i, b, f with f i = 0 and b ≠ 0, P f implies P (f + single i b), then P holds for all f.
Русский
Пусть P — свойство на Π₀ i, β i. Если P(0) верно и для всех i, b и f с f i = 0 и b ≠ 0 верно, что P f ⇒ P (f + single i b), тогда P верно для всех f.
LaTeX
$$$ P(0) \\land \\forall i\\forall b\\forall f\\ (f(i) = 0 \\land b \\neq 0 \\land P(f) \\rightarrow P(f + single i b)) \\Rightarrow \\forall f\\, P(f) $$$
Lean4
protected theorem induction {p : (Π₀ i, β i) → Prop} (f : Π₀ i, β i) (h0 : p 0)
(ha : ∀ (i b) (f : Π₀ i, β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)) : p f :=
by
obtain ⟨f, s⟩ := f
induction s using Trunc.induction_on with
| _ s
obtain ⟨s, H⟩ := s
induction s using Multiset.induction_on generalizing f with
| empty =>
have : f = 0 := funext fun i => (H i).resolve_left (Multiset.notMem_zero _)
subst this
exact h0
| cons i s ih => ?_
have H2 : p (erase i ⟨f, Trunc.mk ⟨i ::ₘ s, H⟩⟩) :=
by
dsimp only [erase, Trunc.map, Trunc.bind, Trunc.liftOn, Trunc.lift_mk, Function.comp, Subtype.coe_mk]
have H2 : ∀ j, j ∈ s ∨ ite (j = i) 0 (f j) = 0 := by
intro j
rcases H j with H2 | H2
· rcases Multiset.mem_cons.1 H2 with H3 | H3
· right; exact if_pos H3
· left; exact H3
right
split_ifs <;> [rfl; exact H2]
have H3 :
∀ aux,
(⟨fun j : ι => ite (j = i) 0 (f j), Trunc.mk ⟨i ::ₘ s, aux⟩⟩ : Π₀ i, β i) =
⟨fun j : ι => ite (j = i) 0 (f j), Trunc.mk ⟨s, H2⟩⟩ :=
fun _ ↦ ext fun _ => rfl
rw [H3]
apply ih
have H3 : single i _ + _ = (⟨f, Trunc.mk ⟨i ::ₘ s, H⟩⟩ : Π₀ i, β i) := single_add_erase _ _
rw [← H3]
change p (single i (f i) + _)
rcases Classical.em (f i = 0) with h | h
· rw [h, single_zero, zero_add]
exact H2
refine ha _ _ _ ?_ h H2
rw [erase_same]
