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

case mpr
α : Type u_1
β : Type ?u.60671
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ (∃ x y, x ≠ y ∧ s = {x, y}) → card s = 2
α : Type u_1
β : Type ?u.60671
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ card s = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}
constructor
case mp
α : Type u_1
β : Type ?u.60671
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ (∃ a t, ¬a ∈ t ∧ insert a t = s ∧ card t = 1) → ∃ x y, x ≠ y ∧ s = {x, y}
case mp
α : Type u_1
β : Type ?u.60671
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ card s = 2 → ∃ x y, x ≠ y ∧ s = {x, y}
rw [card_eq_succ]
case mp
α : Type u_1
β : Type ?u.60671
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ (∃ a t, ¬a ∈ t ∧ insert a t = s ∧ ∃ a, t = {a}) → ∃ x y, x ≠ y ∧ s = {x, y}
case mp
α : Type u_1
β : Type ?u.60671
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ (∃ a t, ¬a ∈ t ∧ insert a t = s ∧ card t = 1) → ∃ x y, x ≠ y ∧ s = {x, y}
simp_rw [card_eq_one]
case mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.60671
t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
a b : α
hab : ¬a ∈ {b}
⊢ ∃ x y, x ≠ y ∧ {a, b} = {x, y}
case mp
α : Type u_1
β : Type ?u.60671
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ (∃ a t, ¬a ∈ t ∧ insert a t = s ∧ ∃ a, t = {a}) → ∃ x y, x ≠ y ∧ s = {x, y}
rintro ⟨a, _, hab, rfl, b, rfl⟩
no goals
case mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.60671
t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
a b : α
hab : ¬a ∈ {b}
⊢ ∃ x y, x ≠ y ∧ {a, b} = {x, y}
exact ⟨a, b, not_mem_singleton.1 hab, rfl⟩
case mpr.intro.intro.intro
α : Type u_1
β : Type ?u.60671
t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
x y : α
h : x ≠ y
⊢ card {x, y} = 2
case mpr
α : Type u_1
β : Type ?u.60671
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ (∃ x y, x ≠ y ∧ s = {x, y}) → card s = 2
rintro ⟨x, y, h, rfl⟩
no goals
case mpr.intro.intro.intro
α : Type u_1
β : Type ?u.60671
t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
x y : α
h : x ≠ y
⊢ card {x, y} = 2
exact card_doubleton h