case mp
α : Type u_1
β : Type ?u.62214
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ card s = 3 → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

case mpr
α : Type u_1
β : Type ?u.62214
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ (∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}) → card s = 3
α : Type u_1
β : Type ?u.62214
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ card s = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
constructor
case mp
α : Type u_1
β : Type ?u.62214
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ (∃ a t, ¬a ∈ t ∧ insert a t = s ∧ card t = 2) → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
case mp
α : Type u_1
β : Type ?u.62214
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ card s = 3 → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
rw [card_eq_succ]
case mp
α : Type u_1
β : Type ?u.62214
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ (∃ a t, ¬a ∈ t ∧ insert a t = s ∧ ∃ x y, x ≠ y ∧ t = {x, y}) → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
case mp
α : Type u_1
β : Type ?u.62214
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ (∃ a t, ¬a ∈ t ∧ insert a t = s ∧ card t = 2) → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
simp_rw [card_eq_two]
case mp.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.62214
t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
a b c : α
bc : b ≠ c
abc : ¬a ∈ {b, c}
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ {a, b, c} = {x, y, z}
case mp
α : Type u_1
β : Type ?u.62214
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ (∃ a t, ¬a ∈ t ∧ insert a t = s ∧ ∃ x y, x ≠ y ∧ t = {x, y}) → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
rintro ⟨a, _, abc, rfl, b, c, bc, rfl⟩
case mp.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.62214
t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
a b c : α
bc : b ≠ c
abc : ¬a = b ∧ ¬a = c
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ {a, b, c} = {x, y, z}
case mp.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.62214
t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
a b c : α
bc : b ≠ c
abc : ¬a ∈ {b, c}
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ {a, b, c} = {x, y, z}
rw [mem_insert, mem_singleton, not_or] at abc
no goals
case mp.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.62214
t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
a b c : α
bc : b ≠ c
abc : ¬a = b ∧ ¬a = c
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ {a, b, c} = {x, y, z}
exact ⟨a, b, c, abc.1, abc.2, bc, rfl⟩
case mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.62214
t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
x y z : α
xy : x ≠ y
xz : x ≠ z
yz : y ≠ z
⊢ card {x, y, z} = 3
case mpr
α : Type u_1
β : Type ?u.62214
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ (∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}) → card s = 3
rintro ⟨x, y, z, xy, xz, yz, rfl⟩
no goals
case mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.62214
t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
x y z : α
xy : x ≠ y
xz : x ≠ z
yz : y ≠ z
⊢ card {x, y, z} = 3
simp only [xy, xz, yz, mem_insert, card_insert_of_not_mem, not_false_iff, mem_singleton,
  or_self_iff, card_singleton]