case refine'_1
α : Type u_1
β : Type ?u.162338
s t : Set α
a b x y : α
f : α → β
h : ncard s = 2
⊢ ∃ x y, x ≠ y ∧ s = {x, y}

case refine'_2
α : Type u_1
β : Type ?u.162338
s t : Set α
a b x y : α
f : α → β
⊢ (∃ x y, x ≠ y ∧ s = {x, y}) → ncard s = 2
α : Type u_1
β : Type ?u.162338
s t : Set α
a b x y : α
f : α → β
⊢ ncard s = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}
refine' ⟨fun h ↦ _, _⟩
case refine'_2.intro.intro.intro
α : Type u_1
β : Type ?u.162338
t : Set α
a b x✝ y✝ : α
f : α → β
x y : α
hxy : x ≠ y
⊢ ncard {x, y} = 2
case refine'_2
α : Type u_1
β : Type ?u.162338
s t : Set α
a b x y : α
f : α → β
⊢ (∃ x y, x ≠ y ∧ s = {x, y}) → ncard s = 2
rintro ⟨x, y, hxy, rfl⟩
case refine'_2.intro.intro.intro
α : Type u_1
β : Type ?u.162338
t : Set α
a b x✝ y✝ : α
f : α → β
x y : α
hxy : x ≠ y
⊢ ∃ x_1 y_1, x_1 ≠ y_1 ∧ Finite.toFinset (_ : Set.Finite {x, y}) = {x_1, y_1}
case refine'_2.intro.intro.intro
α : Type u_1
β : Type ?u.162338
t : Set α
a b x✝ y✝ : α
f : α → β
x y : α
hxy : x ≠ y
⊢ ncard {x, y} = 2
rw [ncard_eq_toFinset_card _, Finset.card_eq_two]
no goals
case refine'_2.intro.intro.intro
α : Type u_1
β : Type ?u.162338
t : Set α
a b x✝ y✝ : α
f : α → β
x y : α
hxy : x ≠ y
⊢ ∃ x_1 y_1, x_1 ≠ y_1 ∧ Finite.toFinset (_ : Set.Finite {x, y}) = {x_1, y_1}
exact ⟨x, y, hxy, by ext; simp⟩
case refine'_1.intro.intro.intro.intro
α : Type u_1
β : Type ?u.162338
t✝ : Set α
a b x✝ y : α
f : α → β
x : α
t : Set α
hxt : ¬x ∈ t
ht : ncard t = 1
h : ncard (insert x t) = 2
⊢ ∃ x_1 y, x_1 ≠ y ∧ insert x t = {x_1, y}
case refine'_1
α : Type u_1
β : Type ?u.162338
s t : Set α
a b x y : α
f : α → β
h : ncard s = 2
⊢ ∃ x y, x ≠ y ∧ s = {x, y}
obtain ⟨x, t, hxt, rfl, ht⟩ := eq_insert_of_ncard_eq_succ h
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.162338
t : Set α
a b x✝ y✝ : α
f : α → β
x y : α
hxt : ¬x ∈ {y}
ht : ncard {y} = 1
h : ncard {x, y} = 2
⊢ ∃ x_1 y_1, x_1 ≠ y_1 ∧ {x, y} = {x_1, y_1}
case refine'_1.intro.intro.intro.intro
α : Type u_1
β : Type ?u.162338
t✝ : Set α
a b x✝ y : α
f : α → β
x : α
t : Set α
hxt : ¬x ∈ t
ht : ncard t = 1
h : ncard (insert x t) = 2
⊢ ∃ x_1 y, x_1 ≠ y ∧ insert x t = {x_1, y}
obtain ⟨y, rfl⟩ := ncard_eq_one.mp ht
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.162338
t : Set α
a b x✝ y✝ : α
f : α → β
x y : α
hxt : ¬x = y
ht : ncard {y} = 1
h : ncard {x, y} = 2
⊢ ∃ x_1 y_1, x_1 ≠ y_1 ∧ {x, y} = {x_1, y_1}
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.162338
t : Set α
a b x✝ y✝ : α
f : α → β
x y : α
hxt : ¬x ∈ {y}
ht : ncard {y} = 1
h : ncard {x, y} = 2
⊢ ∃ x_1 y_1, x_1 ≠ y_1 ∧ {x, y} = {x_1, y_1}
rw [mem_singleton_iff] at hxt
no goals
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.162338
t : Set α
a b x✝ y✝ : α
f : α → β
x y : α
hxt : ¬x = y
ht : ncard {y} = 1
h : ncard {x, y} = 2
⊢ ∃ x_1 y_1, x_1 ≠ y_1 ∧ {x, y} = {x_1, y_1}
exact ⟨_, _, hxt, rfl⟩
case a
α : Type u_1
β : Type ?u.162338
t : Set α
a b x✝ y✝ : α
f : α → β
x y : α
hxy : x ≠ y
a✝ : α
⊢ a✝ ∈ Finite.toFinset (_ : Set.Finite {x, y}) ↔ a✝ ∈ {x, y}
α : Type u_1
β : Type ?u.162338
t : Set α
a b x✝ y✝ : α
f : α → β
x y : α
hxy : x ≠ y
⊢ Finite.toFinset (_ : Set.Finite {x, y}) = {x, y}
ext
no goals
case a
α : Type u_1
β : Type ?u.162338
t : Set α
a b x✝ y✝ : α
f : α → β
x y : α
hxy : x ≠ y
a✝ : α
⊢ a✝ ∈ Finite.toFinset (_ : Set.Finite {x, y}) ↔ a✝ ∈ {x, y}
simp