α β : Type u
⊢ (∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}) ↔ ∃ x y, x ≠ y ∧ {x, y} = univ
α β : Type u
⊢ (#α) = 2 ↔ ∃ x y, x ≠ y ∧ {x, y} = univ
simp only [← @Nat.cast_two Cardinal, mk_eq_nat_iff_finset, Finset.card_eq_two]
case mp
α β : Type u
⊢ (∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}) → ∃ x y, x ≠ y ∧ {x, y} = univ

case mpr
α β : Type u
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) → ∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}
α β : Type u
⊢ (∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}) ↔ ∃ x y, x ≠ y ∧ {x, y} = univ
constructor
case mp.intro.intro.intro.intro.intro
α β : Type u
x y : α
hne : x ≠ y
ht : ↑{x, y} = univ
⊢ ∃ x y, x ≠ y ∧ {x, y} = univ
case mp
α β : Type u
⊢ (∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}) → ∃ x y, x ≠ y ∧ {x, y} = univ
rintro ⟨t, ht, x, y, hne, rfl⟩
no goals
case mp.intro.intro.intro.intro.intro
α β : Type u
x y : α
hne : x ≠ y
ht : ↑{x, y} = univ
⊢ ∃ x y, x ≠ y ∧ {x, y} = univ
exact ⟨x, y, hne, by simpa using ht⟩
no goals
α β : Type u
x y : α
hne : x ≠ y
ht : ↑{x, y} = univ
⊢ {x, y} = univ
simpa using ht
case mpr.intro.intro.intro
α β : Type u
x y : α
hne : x ≠ y
h : {x, y} = univ
⊢ ∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}
case mpr
α β : Type u
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) → ∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}
rintro ⟨x, y, hne, h⟩
no goals
case mpr.intro.intro.intro
α β : Type u
x y : α
hne : x ≠ y
h : {x, y} = univ
⊢ ∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}
exact ⟨{x, y}, by simpa using h, x, y, hne, rfl⟩
no goals
α β : Type u
x y : α
hne : x ≠ y
h : {x, y} = univ
⊢ ↑{x, y} = univ
simpa using h