α : Type u_1
β : Type ?u.65760
γ : Type ?u.65763
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ False
α : Type u_1
β : Type ?u.65760
γ : Type ?u.65763
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ False
skip
no goals
α : Type u_1
β : Type ?u.65760
γ : Type ?u.65763
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ False
classical
  refine' lt_irrefl (Fintype.card α) _
  calc
    Fintype.card α ≤ Fintype.card s := Fintype.card_le_of_injective f hf
    _ = s.toFinset.card := s.toFinset_card.symm
    _ < Fintype.card α :=
      Finset.card_lt_card <| by rwa [Set.toFinset_ssubset_univ, Set.ssubset_univ_iff]
α : Type u_1
β : Type ?u.65760
γ : Type ?u.65763
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ Fintype.card α < Fintype.card α
α : Type u_1
β : Type ?u.65760
γ : Type ?u.65763
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ False
refine' lt_irrefl (Fintype.card α) _
no goals
α : Type u_1
β : Type ?u.65760
γ : Type ?u.65763
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ Fintype.card α < Fintype.card α
calc
  Fintype.card α ≤ Fintype.card s := Fintype.card_le_of_injective f hf
  _ = s.toFinset.card := s.toFinset_card.symm
  _ < Fintype.card α :=
    Finset.card_lt_card <| by rwa [Set.toFinset_ssubset_univ, Set.ssubset_univ_iff]
no goals
α : Type u_1
β : Type ?u.65760
γ : Type ?u.65763
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ Set.toFinset s ⊂ univ
rwa [Set.toFinset_ssubset_univ, Set.ssubset_univ_iff]