-- Mathlib/Data/Set/Card.lean
theorem encard_eq_three {α : Type u_1} {s : Set α} :
    encard s = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Proof state:
α : Type u_1
s : Set α
x : α
h : (s \ {x}).encard + 1 = 3
hx : x ∈ s
⊢ 3 = 2 + 1

Tactic:
exact rfl

Result:
no goals

Proof state:
α : Type u_1
s : Set α
h : s.encard = 3
⊢ s.encard ≠ 0

Tactic:
rw [h]

Result:
α : Type u_1
s : Set α
h : s.encard = 3
⊢ 3 ≠ 0

Proof state:
case refine_1.intro.intro.intro.intro.refine_1
α : Type u_1
s : Set α
x : α
hx : x ∈ s
z : α
hne : x ≠ z
hs : s \ {x} = {x, z}
⊢ False

Tactic:
exact (hs.symm.subset (Or.inl rfl)).2 rfl

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro.refine_2
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ x ≠ z

Tactic:
rintro rfl

Result:
case refine_1.intro.intro.intro.intro.refine_2
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y : α
hne : y ≠ x
hs : s \ {x} = {y, x}
⊢ False

Proof state:
case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ s.encard = 3

Tactic:
rw [hs, encard_insert_of_not_mem, encard_insert_of_not_mem, encard_singleton] <;> aesop

Result:
no goals

Proof state:
case refine_1.intro
α : Type u_1
s : Set α
h : s.encard = 3
x : α
hx : x ∈ s
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
rw [← insert_eq_of_mem hx, ← insert_diff_singleton,
  encard_insert_of_not_mem (fun h ↦ h.2 rfl), (by exact rfl : (3 : ℕ∞) = 2 + 1),
  WithTop.add_right_inj WithTop.one_ne_top, encard_eq_two] at h

Result:
case refine_1.intro
α : Type u_1
s : Set α
x : α
h : ∃ x_1 y, x_1 ≠ y ∧ s \ {x} = {x_1, y}
hx : x ∈ s
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Proof state:
case refine_1.intro.intro.intro.intro
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
refine ⟨x, y, z, ?_, ?_, hne, ?_⟩

Result:
case refine_1.intro.intro.intro.intro.refine_1
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ x ≠ y

case refine_1.intro.intro.intro.intro.refine_2
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ x ≠ z

case refine_1.intro.intro.intro.intro.refine_3
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ s = {x, y, z}

Proof state:
case refine_1.intro.intro.intro.intro.refine_2
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y : α
hne : y ≠ x
hs : s \ {x} = {y, x}
⊢ False

Tactic:
exact (hs.symm.subset (Or.inr rfl)).2 rfl

Result:
no goals

Proof state:
case refine_1
α : Type u_1
s : Set α
h : s.encard = 3
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
obtain ⟨x, hx⟩ := nonempty_of_encard_ne_zero (s := s) (by rw [h]; simp)

Result:
case refine_1.intro
α : Type u_1
s : Set α
h : s.encard = 3
x : α
hx : x ∈ s
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Proof state:
case refine_1.intro
α : Type u_1
s : Set α
x : α
h : ∃ x_1 y, x_1 ≠ y ∧ s \ {x} = {x_1, y}
hx : x ∈ s
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
obtain ⟨y, z, hne, hs⟩ := h

Result:
case refine_1.intro.intro.intro.intro
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Proof state:
case refine_1.intro.intro.intro.intro.refine_1
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ x ≠ y

Tactic:
rintro rfl

Result:
case refine_1.intro.intro.intro.intro.refine_1
α : Type u_1
s : Set α
x : α
hx : x ∈ s
z : α
hne : x ≠ z
hs : s \ {x} = {x, z}
⊢ False

Proof state:
α : Type u_1
s : Set α
h : s.encard = 3
⊢ 3 ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro.refine_3
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ s = {x, y, z}

Tactic:
rw [← hs, insert_diff_singleton, insert_eq_of_mem hx]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
⊢ s.encard = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨x, y, z, hxy, hyz, hxz, hs⟩ ↦ ?_⟩

Result:
case refine_1
α : Type u_1
s : Set α
h : s.encard = 3
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ s.encard = 3