[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type ?u.84
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Trunc (α ≃ Fin (card α))
[PROOFSTEP]
unfold card Finset.card
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type ?u.84
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Trunc (α ≃ Fin (↑Multiset.card univ.val))
[PROOFSTEP]
exact
  Quot.recOnSubsingleton' (motive := fun s : Multiset α =>
    (∀ x : α, x ∈ s) → s.Nodup → Trunc (α ≃ Fin (Multiset.card s))) univ.val
    (fun l (h : ∀ x : α, x ∈ l) (nd : l.Nodup) => Trunc.mk (nd.getEquivOfForallMemList _ h).symm) mem_univ_val univ.2
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type ?u.1546
inst✝ : Fintype α
⊢ Trunc { f // Bijective f }
[PROOFSTEP]
unfold card Finset.card
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type ?u.1546
inst✝ : Fintype α
⊢ Trunc { f // Bijective f }
[PROOFSTEP]
refine
  Quot.recOnSubsingleton' (motive := fun s : Multiset α =>
    (∀ x : α, x ∈ s) → s.Nodup → Trunc { f : Fin (Multiset.card s) → α // Bijective f }) univ.val
    (fun l (h : ∀ x : α, x ∈ l) (nd : l.Nodup) => Trunc.mk (nd.getBijectionOfForallMemList _ h)) mem_univ_val univ.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
inst✝ : Fintype { x // p x }
⊢ card { x // p x } = Finset.card s
[PROOFSTEP]
rw [← subtype_card s H]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
inst✝ : Fintype { x // p x }
⊢ card { x // p x } = card { x // p x }
[PROOFSTEP]
congr
[GOAL]
case h.e_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
inst✝ : Fintype { x // p x }
⊢ inst✝ = Fintype.subtype s H
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
inst✝ : Fintype ↑p
⊢ card ↑p = Finset.card s
[PROOFSTEP]
rw [← card_ofFinset s H]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
inst✝ : Fintype ↑p
⊢ card ↑p = card ↑p
[PROOFSTEP]
congr
[GOAL]
case h.e_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
inst✝ : Fintype ↑p
⊢ inst✝ = ofFinset s H
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ≃ β
⊢ card α = card β
[PROOFSTEP]
rw [← ofEquiv_card f]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ≃ β
⊢ card β = card β
[PROOFSTEP]
congr
[GOAL]
case h.e_2.h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ≃ β
⊢ ofEquiv α f = inst✝
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
h : α = β
⊢ α ≃ β
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
h : card α = card β
⊢ α ≃ β
[PROOFSTEP]
letI := Classical.decEq α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
h : card α = card β
this : DecidableEq α := Classical.decEq α
⊢ α ≃ β
[PROOFSTEP]
letI := Classical.decEq β
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
h : card α = card β
this✝ : DecidableEq α := Classical.decEq α
this : DecidableEq β := Classical.decEq β
⊢ α ≃ β
[PROOFSTEP]
exact (truncEquivOfCardEq h).out
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
s : Finset α
hs : card s = Fintype.card α
⊢ card univ ≤ card s
[PROOFSTEP]
rw [hs, Finset.card_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
s : Finset α
⊢ s = univ → card s = Fintype.card α
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
⊢ card univ = Fintype.card α
[PROOFSTEP]
exact Finset.card_univ
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑sᶜ
⊢ card ↑sᶜ = card α - card ↑s
[PROOFSTEP]
classical rw [← Set.toFinset_card, ← Set.toFinset_card, ← Finset.card_compl, Set.toFinset_compl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑sᶜ
⊢ card ↑sᶜ = card α - card ↑s
[PROOFSTEP]
rw [← Set.toFinset_card, ← Set.toFinset_card, ← Finset.card_compl, Set.toFinset_compl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
⊢ card univ = n
[PROOFSTEP]
rw [Finset.card_univ, Fintype.card_fin]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
n m : ℕ
h : Fin n = Fin m
⊢ _root_.cast h = ↑(castIso (_ : n = m))
[PROOFSTEP]
cases fin_injective h
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
h : Fin n = Fin n
⊢ _root_.cast h = ↑(castIso (_ : n = n))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
s : Finset (Fin n)
⊢ card s ≤ n
[PROOFSTEP]
simpa only [Fintype.card_fin] using s.card_le_univ
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
m n : ℕ
x✝ : Nonempty (Fin m ≃ Fin n)
h : Fin m ≃ Fin n
⊢ m = n
[PROOFSTEP]
simpa using Fintype.card_congr h
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Sort u_4
β : Sort u_5
inst✝ : Finite β
f : α → β
H : Injective f
⊢ Finite α
[PROOFSTEP]
cases nonempty_fintype (PLift β)
[GOAL]
case intro
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Sort u_4
β : Sort u_5
inst✝ : Finite β
f : α → β
H : Injective f
val✝ : Fintype (PLift β)
⊢ Finite α
[PROOFSTEP]
rw [← Equiv.injective_comp Equiv.plift f, ← Equiv.comp_injective _ Equiv.plift.symm] at H 
[GOAL]
case intro
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Sort u_4
β : Sort u_5
inst✝ : Finite β
f : α → β
H : Injective (↑Equiv.plift.symm ∘ f ∘ ↑Equiv.plift)
val✝ : Fintype (PLift β)
⊢ Finite α
[PROOFSTEP]
haveI := Fintype.ofInjective _ H
[GOAL]
case intro
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Sort u_4
β : Sort u_5
inst✝ : Finite β
f : α → β
H : Injective (↑Equiv.plift.symm ∘ f ∘ ↑Equiv.plift)
val✝ : Fintype (PLift β)
this : Fintype (PLift α)
⊢ Finite α
[PROOFSTEP]
exact Finite.of_equiv _ Equiv.plift
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
⊢ ∃ l, List.Nodup l ∧ ∀ (x : α), x ∈ l
[PROOFSTEP]
cases nonempty_fintype α
[GOAL]
case intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
val✝ : Fintype α
⊢ ∃ l, List.Nodup l ∧ ∀ (x : α), x ∈ l
[PROOFSTEP]
obtain ⟨l, e⟩ := Quotient.exists_rep (@univ α _).1
[GOAL]
case intro.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
val✝ : Fintype α
l : List α
e : Quotient.mk (List.isSetoid α) l = univ.val
⊢ ∃ l, List.Nodup l ∧ ∀ (x : α), x ∈ l
[PROOFSTEP]
have := And.intro (@univ α _).2 (@mem_univ_val α _)
[GOAL]
case intro.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
val✝ : Fintype α
l : List α
e : Quotient.mk (List.isSetoid α) l = univ.val
this : Multiset.Nodup univ.val ∧ ∀ (x : α), x ∈ univ.val
⊢ ∃ l, List.Nodup l ∧ ∀ (x : α), x ∈ l
[PROOFSTEP]
exact ⟨_, by rwa [← e] at this ⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
val✝ : Fintype α
l : List α
e : Quotient.mk (List.isSetoid α) l = univ.val
this : Multiset.Nodup univ.val ∧ ∀ (x : α), x ∈ univ.val
⊢ List.Nodup ?m.13327 ∧ ∀ (x : α), x ∈ ?m.13327
[PROOFSTEP]
rwa [← e] at this 
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Fintype α
l : List α
h : Nodup l
⊢ length l ≤ Fintype.card α
[PROOFSTEP]
classical exact List.toFinset_card_of_nodup h ▸ l.toFinset.card_le_univ
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Fintype α
l : List α
h : Nodup l
⊢ length l ≤ Fintype.card α
[PROOFSTEP]
exact List.toFinset_card_of_nodup h ▸ l.toFinset.card_le_univ
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → β
h : Injective f
b : β
w : ¬b ∈ Set.range f
⊢ ¬?m.15183 f h w ∈ map { toFun := f, inj' := h } univ
[PROOFSTEP]
rwa [← mem_coe, coe_map, coe_univ, Set.image_univ]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
inst✝³ : Fintype α✝
inst✝² : Fintype β✝
α : Type u_4
β : Type u_5
f : α → β
inst✝¹ : Fintype α
inst✝ : Fintype ↑(Set.range f)
a : α
⊢ f a ∈ Set.range f
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
inst✝³ : Fintype α✝
inst✝² : Fintype β✝
α : Type u_4
β : Type u_5
f : α → β
inst✝¹ : Fintype α
inst✝ : Fintype ↑(Set.range f)
x✝ : ↑(Set.range f)
val✝ : β
a : α
ha : f a = val✝
⊢ (fun a => { val := f a, property := (_ : f a ∈ Set.range f) }) a = { val := val✝, property := (_ : ∃ y, f y = val✝) }
[PROOFSTEP]
simpa using ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ card α = 1 ↔ ∃ x, ∀ (y : α), y = x
[PROOFSTEP]
rw [← card_unit, card_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ Nonempty (α ≃ Unit) ↔ ∃ x, ∀ (y : α), y = x
[PROOFSTEP]
exact
  ⟨fun ⟨a⟩ => ⟨a.symm (), fun y => a.injective (Subsingleton.elim _ _)⟩, fun ⟨x, hx⟩ =>
    ⟨⟨fun _ => (), fun _ => x, fun _ => (hx _).trans (hx _).symm, fun _ => Subsingleton.elim _ _⟩⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ card α = 0 ↔ IsEmpty α
[PROOFSTEP]
rw [card, Finset.card_eq_zero, univ_eq_empty_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
n : ℕ := card α
hn : n = card α
ha : 1 = card α
_h : card α ≤ 1
a b : α
⊢ a = b
[PROOFSTEP]
let ⟨x, hx⟩ := card_eq_one_iff.1 ha.symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
n : ℕ := card α
hn : n = card α
ha : 1 = card α
_h : card α ≤ 1
a b x : α
hx : ∀ (y : α), y = x
⊢ a = b
[PROOFSTEP]
rw [hx a, hx b]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : card α ≤ 1
⊢ False
[PROOFSTEP]
rw [← ha] at h 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : n + 2 ≤ 1
⊢ False
[PROOFSTEP]
cases h with
| step h => cases h; done
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : n + 2 ≤ 1
⊢ False
[PROOFSTEP]
cases h with
| step h => cases h; done
[GOAL]
case step
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : Nat.le (n + 2) 0
⊢ False
[PROOFSTEP]

| step h => cases h; done
[GOAL]
case step
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : Nat.le (n + 2) 0
⊢ False
[PROOFSTEP]
cases h
[GOAL]

[PROOFSTEP]
done
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ 1 < card α ↔ Nontrivial α
[PROOFSTEP]
classical
rw [← not_iff_not]
push_neg
rw [not_nontrivial_iff_subsingleton, card_le_one_iff_subsingleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ 1 < card α ↔ Nontrivial α
[PROOFSTEP]
rw [← not_iff_not]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ ¬1 < card α ↔ ¬Nontrivial α
[PROOFSTEP]
push_neg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ card α ≤ 1 ↔ ¬Nontrivial α
[PROOFSTEP]
rw [not_nontrivial_iff_subsingleton, card_le_one_iff_subsingleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ 2 < card α ↔ ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c
[PROOFSTEP]
simp_rw [← Finset.card_univ, two_lt_card_iff, mem_univ, true_and_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
f : α → α
hinj : Injective f
⊢ Surjective f
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
⊢ ∃ a, f a = x
[PROOFSTEP]
have := Classical.propDecidable
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
⊢ ∃ a, f a = x
[PROOFSTEP]
cases nonempty_fintype α
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
⊢ ∃ a, f a = x
[PROOFSTEP]
have h₁ : image f univ = univ :=
  eq_of_subset_of_card_le (subset_univ _) ((card_image_of_injective univ hinj).symm ▸ le_rfl)
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
h₁ : image f univ = univ
⊢ ∃ a, f a = x
[PROOFSTEP]
have h₂ : x ∈ image f univ := h₁.symm ▸ mem_univ x
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
h₁ : image f univ = univ
h₂ : x ∈ image f univ
⊢ ∃ a, f a = x
[PROOFSTEP]
obtain ⟨y, h⟩ := mem_image.1 h₂
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
h₁ : image f univ = univ
h₂ : x ∈ image f univ
y : α
h : y ∈ univ ∧ f y = x
⊢ ∃ a, f a = x
[PROOFSTEP]
exact ⟨y, h.2⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
f : α → α
⊢ Injective f ↔ Bijective f
[PROOFSTEP]
simp [Bijective, injective_iff_surjective]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
f : α → α
⊢ Surjective f ↔ Bijective f
[PROOFSTEP]
simp [Bijective, injective_iff_surjective]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
f : α → β
e : α ≃ β
this : Injective (↑e.symm ∘ f) ↔ Surjective (↑e.symm ∘ f)
hinj : Injective f
⊢ Surjective f
[PROOFSTEP]
simpa [Function.comp] using e.surjective.comp (this.1 (e.symm.injective.comp hinj))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
f : α → β
e : α ≃ β
this : Injective (↑e.symm ∘ f) ↔ Surjective (↑e.symm ∘ f)
hsurj : Surjective f
⊢ Injective f
[PROOFSTEP]
simpa [Function.comp] using e.injective.comp (this.2 (e.symm.surjective.comp hsurj))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ Fintype.card ↑s = Fintype.card α ↔ s = Set.univ
[PROOFSTEP]
rw [← Set.toFinset_card, Finset.card_eq_iff_eq_univ, ← Set.toFinset_univ, Set.toFinset_inj]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
e : α ↪ α
⊢ Equiv.toEmbedding (equivOfFintypeSelfEmbedding e) = e
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
e : α ↪ α
x✝ : α
⊢ ↑(Equiv.toEmbedding (equivOfFintypeSelfEmbedding e)) x✝ = ↑e x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
h : Fintype.card α ≤ Fintype.card β
⊢ Nonempty (α ↪ β)
[PROOFSTEP]
classical exact (truncOfCardLE h).nonempty
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
h : Fintype.card α ≤ Fintype.card β
⊢ Nonempty (α ↪ β)
[PROOFSTEP]
exact (truncOfCardLE h).nonempty
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ card s
⊢ ∃ f, Set.range ↑f ⊆ ↑s
[PROOFSTEP]
rw [← Fintype.card_coe] at h 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card { x // x ∈ s }
⊢ ∃ f, Set.range ↑f ⊆ ↑s
[PROOFSTEP]
rcases nonempty_of_card_le h with ⟨f⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card { x // x ∈ s }
f : α ↪ { x // x ∈ s }
⊢ ∃ f, Set.range ↑f ⊆ ↑s
[PROOFSTEP]
exact ⟨f.trans (Embedding.subtype _), by simp [Set.range_subset_iff]⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card { x // x ∈ s }
f : α ↪ { x // x ∈ s }
⊢ Set.range ↑(Embedding.trans f (subtype fun x => x ∈ s)) ⊆ ↑s
[PROOFSTEP]
simp [Set.range_subset_iff]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Fintype α
e : α ↪ α
⊢ map e univ = univ
[PROOFSTEP]
rw [← e.equiv_of_fintype_self_embedding_to_embedding, univ_map_equiv_to_embedding]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : ¬p x
⊢ ¬?m.56237 hx ∈ Set.range Subtype.val
[PROOFSTEP]
rwa [Subtype.range_coe_subtype]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ card { x // p x } = Finset.card (filter p univ)
[PROOFSTEP]
refine' Fintype.card_of_subtype _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ ∀ (x : α), x ∈ filter p univ ↔ p x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ card { x // ¬p x } = card α - card { x // p x }
[PROOFSTEP]
classical rw [Fintype.card_of_subtype (Set.toFinset {x | p x}ᶜ), Set.toFinset_compl, Finset.card_compl,
    Fintype.card_of_subtype] <;>
  · intro
    simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_setOf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ card { x // ¬p x } = card α - card { x // p x }
[PROOFSTEP]
rw [Fintype.card_of_subtype (Set.toFinset {x | p x}ᶜ), Set.toFinset_compl, Finset.card_compl, Fintype.card_of_subtype]
[GOAL]
case H
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ Set.toFinset {x | p x} ↔ p x
[PROOFSTEP]
intro
[GOAL]
case H
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
x✝ : α
⊢ x✝ ∈ Set.toFinset {x | p x} ↔ p x✝
[PROOFSTEP]
simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_setOf]
[GOAL]
case H
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ Set.toFinset {x | p x}ᶜ ↔ ¬p x
[PROOFSTEP]
intro
[GOAL]
case H
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
x✝ : α
⊢ x✝ ∈ Set.toFinset {x | p x}ᶜ ↔ ¬p x✝
[PROOFSTEP]
simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_setOf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : Finite α
p q : α → Prop
inst✝³ : Fintype { x // p x }
inst✝² : Fintype { x // ¬p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // ¬q x }
h : card { x // p x } = card { x // q x }
⊢ card { x // ¬p x } = card { x // ¬q x }
[PROOFSTEP]
cases nonempty_fintype α
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : Finite α
p q : α → Prop
inst✝³ : Fintype { x // p x }
inst✝² : Fintype { x // ¬p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // ¬q x }
h : card { x // p x } = card { x // q x }
val✝ : Fintype α
⊢ card { x // ¬p x } = card { x // ¬q x }
[PROOFSTEP]
simp only [Fintype.card_subtype_compl, h]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ univ = {x}
[PROOFSTEP]
symm
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ {x} = univ
[PROOFSTEP]
apply eq_of_subset_of_card_le (subset_univ { x })
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ card univ ≤ card {x}
[PROOFSTEP]
apply le_of_eq
[GOAL]
case a
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ card univ = card {x}
[PROOFSTEP]
simp [h, Finset.card_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
⊢ WellFounded r
[PROOFSTEP]
classical
cases nonempty_fintype α
have : ∀ x y, r x y → (univ.filter fun z => r z x).card < (univ.filter fun z => r z y).card := fun x y hxy =>
  Finset.card_lt_card <| by
    simp only [Finset.lt_iff_ssubset.symm, lt_iff_le_not_le, Finset.le_iff_subset, Finset.subset_iff, mem_filter,
      true_and_iff, mem_univ, hxy];
    exact ⟨fun z hzx => _root_.trans hzx hxy, not_forall_of_exists_not ⟨x, not_imp.2 ⟨hxy, irrefl x⟩⟩⟩
exact Subrelation.wf (this _ _) (measure _).wf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
⊢ WellFounded r
[PROOFSTEP]
cases nonempty_fintype α
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
val✝ : Fintype α
⊢ WellFounded r
[PROOFSTEP]
have : ∀ x y, r x y → (univ.filter fun z => r z x).card < (univ.filter fun z => r z y).card := fun x y hxy =>
  Finset.card_lt_card <| by
    simp only [Finset.lt_iff_ssubset.symm, lt_iff_le_not_le, Finset.le_iff_subset, Finset.subset_iff, mem_filter,
      true_and_iff, mem_univ, hxy];
    exact ⟨fun z hzx => _root_.trans hzx hxy, not_forall_of_exists_not ⟨x, not_imp.2 ⟨hxy, irrefl x⟩⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
val✝ : Fintype α
x y : α
hxy : r x y
⊢ filter (fun z => r z x) univ ⊂ filter (fun z => r z y) univ
[PROOFSTEP]
simp only [Finset.lt_iff_ssubset.symm, lt_iff_le_not_le, Finset.le_iff_subset, Finset.subset_iff, mem_filter,
  true_and_iff, mem_univ, hxy]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
val✝ : Fintype α
x y : α
hxy : r x y
⊢ (∀ ⦃x_1 : α⦄, r x_1 x → r x_1 y) ∧ ¬∀ ⦃x_1 : α⦄, r x_1 y → r x_1 x
[PROOFSTEP]
exact ⟨fun z hzx => _root_.trans hzx hxy, not_forall_of_exists_not ⟨x, not_imp.2 ⟨hxy, irrefl x⟩⟩⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
val✝ : Fintype α
this : ∀ (x y : α), r x y → card (filter (fun z => r z x) univ) < card (filter (fun z => r z y) univ)
⊢ WellFounded r
[PROOFSTEP]
exact Subrelation.wf (this _ _) (measure _).wf
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Preorder α
s : Finset α
h : Finset.Nonempty s
⊢ ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬x < m
[PROOFSTEP]
obtain ⟨c, hcs : c ∈ s⟩ := h
[GOAL]
case intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Preorder α
s : Finset α
c : α
hcs : c ∈ s
⊢ ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬x < m
[PROOFSTEP]
have : WellFounded (@LT.lt { x // x ∈ s } _) := Finite.wellFounded_of_trans_of_irrefl _
[GOAL]
case intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Preorder α
s : Finset α
c : α
hcs : c ∈ s
this : WellFounded LT.lt
⊢ ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬x < m
[PROOFSTEP]
obtain ⟨⟨m, hms : m ∈ s⟩, -, H⟩ := this.has_min Set.univ ⟨⟨c, hcs⟩, trivial⟩
[GOAL]
case intro.intro.mk.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Preorder α
s : Finset α
c : α
hcs : c ∈ s
this : WellFounded LT.lt
m : α
hms : m ∈ s
H : ∀ (x : { x // x ∈ s }), x ∈ Set.univ → ¬x < { val := m, property := hms }
⊢ ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬x < m
[PROOFSTEP]
exact ⟨m, hms, fun x hx hxm => H ⟨x, hx⟩ trivial hxm⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ False
[PROOFSTEP]
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]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ False
[PROOFSTEP]
refine' lt_irrefl (Fintype.card α) _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ Fintype.card α < Fintype.card α
[PROOFSTEP]
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]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ Set.toFinset s ⊂ univ
[PROOFSTEP]
rwa [Set.toFinset_ssubset_univ, Set.ssubset_univ_iff]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
H : Infinite α
x : α
_hx : ¬x ∈ ∅
y : α
hy : ¬y ∈ {x}
⊢ y ≠ x
[PROOFSTEP]
simpa only [mem_singleton] using hy
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Infinite α
⊢ Nonempty α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ Fintype ℕ → False
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
h : Fintype ℕ
⊢ False
[PROOFSTEP]
exact (Finset.range _).card_le_univ.not_lt ((Nat.lt_succ_self _).trans_eq (card_range _).symm)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ Injective mk
[PROOFSTEP]
intro _ _ h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a₁✝ a₂✝ : List Char
h : { data := a₁✝ } = { data := a₂✝ }
⊢ a₁✝ = a₂✝
[PROOFSTEP]
cases h with
| refl => rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a₁✝ a₂✝ : List Char
h : { data := a₁✝ } = { data := a₂✝ }
⊢ a₁✝ = a₂✝
[PROOFSTEP]
cases h with
| refl => rfl
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
a₁✝ : List Char
⊢ a₁✝ = a₁✝
[PROOFSTEP]

| refl => rfl
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
a₁✝ : List Char
⊢ a₁✝ = a₁✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Mul α
inst✝ : Infinite α
⊢ Injective fun a => { val := (a, a), property := (_ : (a, a).fst * (a, a).snd = (a, a).fst * (a, a).snd) }
[PROOFSTEP]
intro
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Mul α
inst✝ : Infinite α
a₁✝ : α
⊢ ∀ ⦃a₂ : α⦄,
    (fun a => { val := (a, a), property := (_ : (a, a).fst * (a, a).snd = (a, a).fst * (a, a).snd) }) a₁✝ =
        (fun a => { val := (a, a), property := (_ : (a, a).fst * (a, a).snd = (a, a).fst * (a, a).snd) }) a₂ →
      a₁✝ = a₂
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
hmn : m < n
⊢ m = n
[PROOFSTEP]
letI := Classical.decEq α
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
hmn : m < n
this : DecidableEq α := Classical.decEq α
⊢ m = n
[PROOFSTEP]
exfalso
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
hmn : m < n
this : DecidableEq α := Classical.decEq α
⊢ False
[PROOFSTEP]
refine'
  (Classical.choose_spec
      (exists_not_mem_finset
        ((Multiset.range n).pmap (fun m (_hm : m < n) => natEmbeddingAux α m) fun _ => Multiset.mem_range.1).toFinset))
    _
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
hmn : m < n
this : DecidableEq α := Classical.decEq α
⊢ Classical.choose
      (_ :
        ∃ x,
          ¬x ∈
              Multiset.toFinset
                (Multiset.pmap (fun m _hm => Infinite.natEmbeddingAux α m) (Multiset.range n)
                  (_ : ∀ (x : ℕ), x ∈ Multiset.range n → x < n))) ∈
    Multiset.toFinset
      (Multiset.pmap (fun m _hm => Infinite.natEmbeddingAux α m) (Multiset.range n)
        (_ : ∀ (x : ℕ), x ∈ Multiset.range n → x < n))
[PROOFSTEP]
refine' Multiset.mem_toFinset.2 (Multiset.mem_pmap.2 ⟨m, Multiset.mem_range.2 hmn, _⟩)
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
hmn : m < n
this : DecidableEq α := Classical.decEq α
⊢ Infinite.natEmbeddingAux α m =
    Classical.choose
      (_ :
        ∃ x,
          ¬x ∈
              Multiset.toFinset
                (Multiset.pmap (fun m _hm => Infinite.natEmbeddingAux α m) (Multiset.range n)
                  (_ : ∀ (x : ℕ), x ∈ Multiset.range n → x < n)))
[PROOFSTEP]
rw [h, natEmbeddingAux]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Infinite α
⊢ Injective (Infinite.natEmbeddingAux α)
[PROOFSTEP]
rintro m n h
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
⊢ m = n
[PROOFSTEP]
letI := Classical.decEq α
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
this : DecidableEq α := Classical.decEq α
⊢ m = n
[PROOFSTEP]
rcases lt_trichotomy m n with hmn | rfl | hnm
[GOAL]
case inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
this : DecidableEq α := Classical.decEq α
hmn : m < n
⊢ m = n
[PROOFSTEP]
apply natEmbeddingAux_injective_aux α m n h hmn
[GOAL]
case inr.inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Infinite α
m : ℕ
this : DecidableEq α := Classical.decEq α
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α m
⊢ m = m
[PROOFSTEP]
rfl
[GOAL]
case inr.inr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Infinite α
m n : ℕ
h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n
this : DecidableEq α := Classical.decEq α
hnm : n < m
⊢ m = n
[PROOFSTEP]
apply (natEmbeddingAux_injective_aux α n m h.symm hnm).symm
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Infinite α
n : ℕ
⊢ card (map (natEmbedding α) (range n)) = n
[PROOFSTEP]
rw [card_map, card_range]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Infinite α
s : Finset α
n : ℕ
hn : card s ≤ n
⊢ ∃ t, s ⊆ t ∧ card t = n
[PROOFSTEP]
induction' n with n IH generalizing s
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Infinite α
s✝ : Finset α
n : ℕ
hn✝ : card s✝ ≤ n
s : Finset α
hn : card s ≤ zero
⊢ ∃ t, s ⊆ t ∧ card t = zero
[PROOFSTEP]
exact ⟨s, subset_refl _, Nat.eq_zero_of_le_zero hn⟩
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Infinite α
s✝ : Finset α
n✝ : ℕ
hn✝ : card s✝ ≤ n✝
n : ℕ
IH : ∀ (s : Finset α), card s ≤ n → ∃ t, s ⊆ t ∧ card t = n
s : Finset α
hn : card s ≤ succ n
⊢ ∃ t, s ⊆ t ∧ card t = succ n
[PROOFSTEP]
cases' hn.eq_or_lt with hn' hn'
[GOAL]
case succ.inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Infinite α
s✝ : Finset α
n✝ : ℕ
hn✝ : card s✝ ≤ n✝
n : ℕ
IH : ∀ (s : Finset α), card s ≤ n → ∃ t, s ⊆ t ∧ card t = n
s : Finset α
hn : card s ≤ succ n
hn' : card s = succ n
⊢ ∃ t, s ⊆ t ∧ card t = succ n
[PROOFSTEP]
exact ⟨s, subset_refl _, hn'⟩
[GOAL]
case succ.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Infinite α
s✝ : Finset α
n✝ : ℕ
hn✝ : card s✝ ≤ n✝
n : ℕ
IH : ∀ (s : Finset α), card s ≤ n → ∃ t, s ⊆ t ∧ card t = n
s : Finset α
hn : card s ≤ succ n
hn' : card s < succ n
⊢ ∃ t, s ⊆ t ∧ card t = succ n
[PROOFSTEP]
obtain ⟨t, hs, ht⟩ := IH _ (Nat.le_of_lt_succ hn')
[GOAL]
case succ.inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Infinite α
s✝ : Finset α
n✝ : ℕ
hn✝ : card s✝ ≤ n✝
n : ℕ
IH : ∀ (s : Finset α), card s ≤ n → ∃ t, s ⊆ t ∧ card t = n
s : Finset α
hn : card s ≤ succ n
hn' : card s < succ n
t : Finset α
hs : s ⊆ t
ht : card t = n
⊢ ∃ t, s ⊆ t ∧ card t = succ n
[PROOFSTEP]
obtain ⟨x, hx⟩ := exists_not_mem_finset t
[GOAL]
case succ.inr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Infinite α
s✝ : Finset α
n✝ : ℕ
hn✝ : card s✝ ≤ n✝
n : ℕ
IH : ∀ (s : Finset α), card s ≤ n → ∃ t, s ⊆ t ∧ card t = n
s : Finset α
hn : card s ≤ succ n
hn' : card s < succ n
t : Finset α
hs : s ⊆ t
ht : card t = n
x : α
hx : ¬x ∈ t
⊢ ∃ t, s ⊆ t ∧ card t = succ n
[PROOFSTEP]
refine' ⟨Finset.cons x t hx, hs.trans (Finset.subset_cons _), _⟩
[GOAL]
case succ.inr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Infinite α
s✝ : Finset α
n✝ : ℕ
hn✝ : card s✝ ≤ n✝
n : ℕ
IH : ∀ (s : Finset α), card s ≤ n → ∃ t, s ⊆ t ∧ card t = n
s : Finset α
hn : card s ≤ succ n
hn' : card s < succ n
t : Finset α
hs : s ⊆ t
ht : card t = n
x : α
hx : ¬x ∈ t
⊢ card (cons x t hx) = succ n
[PROOFSTEP]
simp [hx, ht]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
w : ∀ (s : Finset ι), card s ≤ n
⊢ Fintype ι
[PROOFSTEP]
apply fintypeOfNotInfinite
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
w : ∀ (s : Finset ι), card s ≤ n
⊢ ¬Infinite ι
[PROOFSTEP]
intro i
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
w : ∀ (s : Finset ι), card s ≤ n
i : Infinite ι
⊢ False
[PROOFSTEP]
obtain ⟨s, c⟩ := Infinite.exists_subset_card_eq ι (n + 1)
[GOAL]
case h.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
w : ∀ (s : Finset ι), card s ≤ n
i : Infinite ι
s : Finset ι
c : card s = n + 1
⊢ False
[PROOFSTEP]
specialize w s
[GOAL]
case h.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
i : Infinite ι
s : Finset ι
c : card s = n + 1
w : card s ≤ n
⊢ False
[PROOFSTEP]
rw [c] at w 
[GOAL]
case h.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
i : Infinite ι
s : Finset ι
c : card s = n + 1
w : n + 1 ≤ n
⊢ False
[PROOFSTEP]
exact Nat.not_succ_le_self n w
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Sort u_4
β : Sort u_5
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
⊢ ∃ x y, x ≠ y ∧ f x = f y
[PROOFSTEP]
simpa only [Injective, not_forall, not_imp, and_comm] using not_injective_infinite_finite f
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
⊢ ∃ y, Infinite ↑(f ⁻¹' {y})
[PROOFSTEP]
classical
by_contra' hf
cases nonempty_fintype β
haveI := fun y => fintypeOfNotInfinite <| hf y
let key : Fintype α :=
  { elems := univ.biUnion fun y : β => (f ⁻¹' { y }).toFinset
    complete := by simp }
exact key.false
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
⊢ ∃ y, Infinite ↑(f ⁻¹' {y})
[PROOFSTEP]
by_contra' hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), ¬Infinite ↑(f ⁻¹' {y})
⊢ False
[PROOFSTEP]
cases nonempty_fintype β
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), ¬Infinite ↑(f ⁻¹' {y})
val✝ : Fintype β
⊢ False
[PROOFSTEP]
haveI := fun y => fintypeOfNotInfinite <| hf y
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), ¬Infinite ↑(f ⁻¹' {y})
val✝ : Fintype β
this : (y : β) → Fintype ↑(f ⁻¹' {y})
⊢ False
[PROOFSTEP]
let key : Fintype α :=
  { elems := univ.biUnion fun y : β => (f ⁻¹' { y }).toFinset
    complete := by simp }
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), ¬Infinite ↑(f ⁻¹' {y})
val✝ : Fintype β
this : (y : β) → Fintype ↑(f ⁻¹' {y})
⊢ ∀ (x : α), x ∈ Finset.biUnion univ fun y => Set.toFinset (f ⁻¹' {y})
[PROOFSTEP]
simp
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), ¬Infinite ↑(f ⁻¹' {y})
val✝ : Fintype β
this : (y : β) → Fintype ↑(f ⁻¹' {y})
key : Fintype α :=
  { elems := Finset.biUnion univ fun y => Set.toFinset (f ⁻¹' {y}),
    complete := (_ : ∀ (a : α), a ∈ Finset.biUnion univ fun y => Set.toFinset (f ⁻¹' {y})) }
⊢ False
[PROOFSTEP]
exact key.false
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : (α : Type u_4) → [inst : Fintype α] → Prop
α : Type u_4
inst✝ : Fintype α
hbase : ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
⊢ P α
[PROOFSTEP]
obtain ⟨n, hn⟩ : ∃ n, Fintype.card α = n := ⟨Fintype.card α, rfl⟩
[GOAL]
case intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : (α : Type u_4) → [inst : Fintype α] → Prop
α : Type u_4
inst✝ : Fintype α
hbase : ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
hn : card α = n
⊢ P α
[PROOFSTEP]
induction' n using Nat.strong_induction_on with n ih generalizing α
[GOAL]
case intro.h
α✝¹ : Type u_1
β : Type u_2
γ : Type u_3
P : (α : Type u_4) → [inst : Fintype α] → Prop
α✝ : Type u_4
inst✝¹ : Fintype α✝
hbase : ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n✝ : ℕ
hn✝ : card α✝ = n✝
n : ℕ
ih : ∀ (m : ℕ), m < n → ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α
α : Type u_4
inst✝ : Fintype α
hn : card α = n
⊢ P α
[PROOFSTEP]
cases' subsingleton_or_nontrivial α with hsing hnontriv
[GOAL]
case intro.h.inl
α✝¹ : Type u_1
β : Type u_2
γ : Type u_3
P : (α : Type u_4) → [inst : Fintype α] → Prop
α✝ : Type u_4
inst✝¹ : Fintype α✝
hbase : ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n✝ : ℕ
hn✝ : card α✝ = n✝
n : ℕ
ih : ∀ (m : ℕ), m < n → ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α
α : Type u_4
inst✝ : Fintype α
hn : card α = n
hsing : Subsingleton α
⊢ P α
[PROOFSTEP]
apply hbase
[GOAL]
case intro.h.inr
α✝¹ : Type u_1
β : Type u_2
γ : Type u_3
P : (α : Type u_4) → [inst : Fintype α] → Prop
α✝ : Type u_4
inst✝¹ : Fintype α✝
hbase : ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n✝ : ℕ
hn✝ : card α✝ = n✝
n : ℕ
ih : ∀ (m : ℕ), m < n → ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α
α : Type u_4
inst✝ : Fintype α
hn : card α = n
hnontriv : Nontrivial α
⊢ P α
[PROOFSTEP]
apply hstep
[GOAL]
case intro.h.inr._ih
α✝¹ : Type u_1
β : Type u_2
γ : Type u_3
P : (α : Type u_4) → [inst : Fintype α] → Prop
α✝ : Type u_4
inst✝¹ : Fintype α✝
hbase : ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n✝ : ℕ
hn✝ : card α✝ = n✝
n : ℕ
ih : ∀ (m : ℕ), m < n → ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α
α : Type u_4
inst✝ : Fintype α
hn : card α = n
hnontriv : Nontrivial α
⊢ ∀ (β : Type u_4) [inst : Fintype β], card β < card α → P β
[PROOFSTEP]
intro β _ hlt
[GOAL]
case intro.h.inr._ih
α✝¹ : Type u_1
β✝ : Type u_2
γ : Type u_3
P : (α : Type u_4) → [inst : Fintype α] → Prop
α✝ : Type u_4
inst✝² : Fintype α✝
hbase : ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n✝ : ℕ
hn✝ : card α✝ = n✝
n : ℕ
ih : ∀ (m : ℕ), m < n → ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α
α : Type u_4
inst✝¹ : Fintype α
hn : card α = n
hnontriv : Nontrivial α
β : Type u_4
inst✝ : Fintype β
hlt : card β < card α
⊢ P β
[PROOFSTEP]
rw [hn] at hlt 
[GOAL]
case intro.h.inr._ih
α✝¹ : Type u_1
β✝ : Type u_2
γ : Type u_3
P : (α : Type u_4) → [inst : Fintype α] → Prop
α✝ : Type u_4
inst✝² : Fintype α✝
hbase : ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n✝ : ℕ
hn✝ : card α✝ = n✝
n : ℕ
ih : ∀ (m : ℕ), m < n → ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α
α : Type u_4
inst✝¹ : Fintype α
hn : card α = n
hnontriv : Nontrivial α
β : Type u_4
inst✝ : Fintype β
hlt : card β < n
⊢ P β
[PROOFSTEP]
exact ih (Fintype.card β) hlt _ rfl
