English
For distinct x and y, encard({x, y}) = 2.
Русский
Для различных x and y, encard({x, y}) = 2.
LaTeX
$$$(x \\neq y) \\Rightarrow encard({x,y}) = 2$$$
Lean4
theorem encard_eq_four {α : Type u_1} {s : Set α} :
encard s = 4 ↔ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = { x, y, z, w } :=
by
refine ⟨fun h ↦ ?_, fun ⟨x, y, z, w, hxy, hxz, hxw, hyz, hyw, hzw, hs⟩ ↦ ?_⟩
· obtain ⟨x, hx⟩ := nonempty_of_encard_ne_zero (s := s) (by rw [h]; simp)
rw [← insert_eq_of_mem hx, ← insert_diff_singleton, encard_insert_of_notMem (fun h ↦ h.2 rfl),
(by exact rfl : (4 : ℕ∞) = 3 + 1), WithTop.add_right_inj WithTop.one_ne_top, encard_eq_three] at h
obtain ⟨y, z, w, hyz, hyw, hzw, hs⟩ := h
refine ⟨x, y, z, w, ?_, ?_, ?_, hyz, hyw, hzw, ?_⟩
· rintro rfl; exact (hs.symm.subset (Or.inl rfl)).2 rfl
· rintro rfl; exact (hs.symm.subset (Or.inr (Or.inl rfl))).2 rfl
· rintro rfl; exact (hs.symm.subset (Or.inr (Or.inr rfl))).2 rfl
rw [← hs, insert_diff_singleton, insert_eq_of_mem hx]
rw [hs, encard_insert_of_notMem, encard_insert_of_notMem, encard_insert_of_notMem, encard_singleton] <;> aesop
