English
If a set s has cardinality n + 1, then there exist an element a and a subset t such that a ∉ t, s = t ∪ {a}, and t has cardinality n.
Русский
Если множество s имеет кардиналитет n + 1, то существует элемент a и подмножество t such that a ∉ t, s = t ∪ {a}, и t имеет кардиналитет n.
LaTeX
$$$s.ncard = n+1 \Rightarrow \exists a \exists t\ (a \notin t \land s = t \cup \{a\} \land t.ncard = n)$$$
Lean4
theorem eq_insert_of_ncard_eq_succ {n : ℕ} (h : s.ncard = n + 1) : ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n := by
classical
have hsf := finite_of_ncard_pos (n.zero_lt_succ.trans_eq h.symm)
rw [ncard_eq_toFinset_card _ hsf, Finset.card_eq_succ] at h
obtain ⟨a, t, hat, hts, rfl⟩ := h
simp only [Finset.ext_iff, Finset.mem_insert, Finite.mem_toFinset] at hts
refine ⟨a, t, hat, ?_, ?_⟩
· simp [Set.ext_iff, hts]
· simp
