α✝ : Type ?u.60858
β : Type ?u.60861
γ : Type ?u.60864
α : Type u_1
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ {x} = univ
α✝ : Type ?u.60858
β : Type ?u.60861
γ : Type ?u.60864
α : Type u_1
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ univ = {x}
symm
α✝ : Type ?u.60858
β : Type ?u.60861
γ : Type ?u.60864
α : Type u_1
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ card univ ≤ card {x}
α✝ : Type ?u.60858
β : Type ?u.60861
γ : Type ?u.60864
α : Type u_1
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ {x} = univ
apply eq_of_subset_of_card_le (subset_univ {x})
case a
α✝ : Type ?u.60858
β : Type ?u.60861
γ : Type ?u.60864
α : Type u_1
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ card univ = card {x}
α✝ : Type ?u.60858
β : Type ?u.60861
γ : Type ?u.60864
α : Type u_1
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ card univ ≤ card {x}
apply le_of_eq
no goals
case a
α✝ : Type ?u.60858
β : Type ?u.60861
γ : Type ?u.60864
α : Type u_1
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ card univ = card {x}
simp [h, Finset.card_univ]