α β : Type u
x : α
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) ↔ ∃! y, y ≠ x
α β : Type u
x : α
⊢ (#α) = 2 ↔ ∃! y, y ≠ x
rw [mk_eq_two_iff]
case mp
α β : Type u
x : α
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) → ∃! y, y ≠ x

case mpr
α β : Type u
x : α
⊢ (∃! y, y ≠ x) → ∃ x y, x ≠ y ∧ {x, y} = univ
α β : Type u
x : α
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) ↔ ∃! y, y ≠ x
constructor
case mp.intro.intro.intro
α β : Type u
x a b : α
hne : a ≠ b
h : {a, b} = univ
⊢ ∃! y, y ≠ x
case mp
α β : Type u
x : α
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) → ∃! y, y ≠ x
rintro ⟨a, b, hne, h⟩
case mp.intro.intro.intro
α β : Type u
x a b : α
hne : a ≠ b
h : ∀ (x : α), x = a ∨ x = b
⊢ ∃! y, y ≠ x
case mp.intro.intro.intro
α β : Type u
x a b : α
hne : a ≠ b
h : {a, b} = univ
⊢ ∃! y, y ≠ x
simp only [eq_univ_iff_forall, mem_insert_iff, mem_singleton_iff] at h
case mp.intro.intro.intro.inl
α β : Type u
x b : α
hne : x ≠ b
h : ∀ (x_1 : α), x_1 = x ∨ x_1 = b
⊢ ∃! y, y ≠ x

case mp.intro.intro.intro.inr
α β : Type u
x a : α
hne : a ≠ x
h : ∀ (x_1 : α), x_1 = a ∨ x_1 = x
⊢ ∃! y, y ≠ x
case mp.intro.intro.intro
α β : Type u
x a b : α
hne : a ≠ b
h : ∀ (x : α), x = a ∨ x = b
⊢ ∃! y, y ≠ x
rcases h x with (rfl | rfl)
no goals
case mp.intro.intro.intro.inl
α β : Type u
x b : α
hne : x ≠ b
h : ∀ (x_1 : α), x_1 = x ∨ x_1 = b
⊢ ∃! y, y ≠ x

case mp.intro.intro.intro.inr
α β : Type u
x a : α
hne : a ≠ x
h : ∀ (x_1 : α), x_1 = a ∨ x_1 = x
⊢ ∃! y, y ≠ x
exacts [⟨b, hne.symm, fun z => (h z).resolve_left⟩, ⟨a, hne, fun z => (h z).resolve_right⟩]
case mpr.intro.intro
α β : Type u
x y : α
hne : y ≠ x
hy : ∀ (y_1 : α), (fun y => y ≠ x) y_1 → y_1 = y
⊢ ∃ x y, x ≠ y ∧ {x, y} = univ
case mpr
α β : Type u
x : α
⊢ (∃! y, y ≠ x) → ∃ x y, x ≠ y ∧ {x, y} = univ
rintro ⟨y, hne, hy⟩
no goals
case mpr.intro.intro
α β : Type u
x y : α
hne : y ≠ x
hy : ∀ (y_1 : α), (fun y => y ≠ x) y_1 → y_1 = y
⊢ ∃ x y, x ≠ y ∧ {x, y} = univ
exact ⟨x, y, hne.symm, eq_univ_of_forall fun z => or_iff_not_imp_left.2 (hy z)⟩