[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
s t : Finset α
⊢ s = univ ↔ ∀ (x : α), x ∈ s
[PROOFSTEP]
simp [ext_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
s t : Finset α
⊢ ↑univ = Set.univ
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
s t : Finset α
x✝ : α
⊢ x✝ ∈ ↑univ ↔ x✝ ∈ Set.univ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
s t : Finset α
⊢ ↑s = Set.univ ↔ s = univ
[PROOFSTEP]
rw [← coe_univ, coe_inj]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
s t : Finset α
inst✝ : Subsingleton α
⊢ Finset.Nonempty s → s = univ
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
s t : Finset α
inst✝ : Subsingleton α
x : α
hx : x ∈ s
⊢ s = univ
[PROOFSTEP]
refine' eq_univ_of_forall fun y => by rwa [Subsingleton.elim y x]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
s t : Finset α
inst✝ : Subsingleton α
x : α
hx : x ∈ s
y : α
⊢ y ∈ s
[PROOFSTEP]
rwa [Subsingleton.elim y x]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
s t : Finset α
⊢ Finset.Nonempty univ ↔ Nonempty α
[PROOFSTEP]
rw [← coe_nonempty, coe_univ, Set.nonempty_iff_univ_nonempty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
s t : Finset α
⊢ univ = ∅ ↔ IsEmpty α
[PROOFSTEP]
rw [← not_nonempty_iff, ← univ_nonempty_iff, not_nonempty_iff_eq_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
s t : Finset α
⊢ Codisjoint s t ↔ ∀ ⦃a : α⦄, ¬a ∈ s → a ∈ t
[PROOFSTEP]
classical simp [codisjoint_iff, eq_univ_iff_forall, or_iff_not_imp_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
s t : Finset α
⊢ Codisjoint s t ↔ ∀ ⦃a : α⦄, ¬a ∈ s → a ∈ t
[PROOFSTEP]
simp [codisjoint_iff, eq_univ_iff_forall, or_iff_not_imp_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
a : α
⊢ a ∈ sᶜ ↔ ¬a ∈ s
[PROOFSTEP]
simp [compl_eq_univ_sdiff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
a : α
⊢ ¬a ∈ sᶜ ↔ a ∈ s
[PROOFSTEP]
rw [mem_compl, not_not]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
a : α
⊢ (erase s a)ᶜ = insert a sᶜ
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ (erase s a)ᶜ ↔ a✝ ∈ insert a sᶜ
[PROOFSTEP]
simp only [or_iff_not_imp_left, mem_insert, not_and, mem_compl, mem_erase]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
a : α
⊢ (insert a s)ᶜ = erase sᶜ a
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ (insert a s)ᶜ ↔ a✝ ∈ erase sᶜ a
[PROOFSTEP]
simp only [not_or, mem_insert, iff_self_iff, mem_compl, mem_erase]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
a x : α
⊢ insert x {x}ᶜ = univ
[PROOFSTEP]
rw [← compl_erase, erase_singleton, compl_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Fintype α
s t : Finset α
inst✝² : DecidableEq α
a : α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
⊢ ∀ (a : α), a ∈ (filter p univ)ᶜ ↔ a ∈ filter (fun x => ¬p x) univ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
s✝ t : Finset α
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ sᶜ ≠ univ ↔ Finset.Nonempty s
[PROOFSTEP]
simp [eq_univ_iff_forall, Finset.Nonempty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
a✝ a : α
⊢ {a}ᶜ = erase univ a
[PROOFSTEP]
rw [compl_eq_univ_sdiff, sdiff_singleton_eq_erase]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
s✝ t : Finset α
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ Set.InjOn (fun a => insert a s) ↑sᶜ
[PROOFSTEP]
rw [coe_compl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
s✝ t : Finset α
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ Set.InjOn (fun a => insert a s) (↑s)ᶜ
[PROOFSTEP]
exact s.insert_inj_on
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
s✝ t : Finset α
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ a ∈ univ ∩ s ↔ a ∈ s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
s✝ t : Finset α
inst✝ : DecidableEq α
s : Finset α
⊢ s ∩ univ = s
[PROOFSTEP]
rw [inter_comm, univ_inter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
s t : Finset α
inst✝ : (i : α) → Decidable (i ∈ univ)
δ : α → Sort u_4
f g : (i : α) → δ i
⊢ piecewise univ f g = f
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
s t : Finset α
inst✝ : (i : α) → Decidable (i ∈ univ)
δ : α → Sort u_4
f g : (i : α) → δ i
i : α
⊢ piecewise univ f g i = f i
[PROOFSTEP]
simp [piecewise]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Fintype α
s✝ t : Finset α
inst✝² : DecidableEq α
s : Finset α
inst✝¹ : (i : α) → Decidable (i ∈ s)
inst✝ : (i : α) → Decidable (i ∈ sᶜ)
δ : α → Sort u_4
f g : (i : α) → δ i
⊢ piecewise sᶜ f g = piecewise s g f
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Fintype α
s✝ t : Finset α
inst✝² : DecidableEq α
s : Finset α
inst✝¹ : (i : α) → Decidable (i ∈ s)
inst✝ : (i : α) → Decidable (i ∈ sᶜ)
δ : α → Sort u_4
f g : (i : α) → δ i
i : α
⊢ piecewise sᶜ f g i = piecewise s g f i
[PROOFSTEP]
simp [piecewise]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
s t : Finset α
δ : α → Sort u_4
inst✝ : DecidableEq α
a : α
f g : (a : α) → δ a
⊢ piecewise (erase univ a) f g = update f a (g a)
[PROOFSTEP]
rw [← compl_singleton, piecewise_compl, piecewise_singleton]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
inst✝² : Fintype α✝
s t : Finset α✝
α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : Fintype β
e : α ≃ β
b : β
⊢ ↑(Equiv.toEmbedding e) (↑e.symm b) = b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Fintype α
s t : Finset α
f : α → β
inst✝² : Fintype β
inst✝¹ : DecidablePred fun y => ∃ x, f x = y
inst✝ : DecidableEq β
⊢ filter (fun y => ∃ x, f x = y) univ = image f univ
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Fintype α
s t : Finset α
f : α → β
inst✝² : Fintype β
inst✝¹ : DecidablePred fun y => ∃ x, f x = y
inst✝ : DecidableEq β
a✝ : β
⊢ a✝ ∈ filter (fun y => ∃ x, f x = y) univ ↔ a✝ ∈ image f univ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Fintype α
s t : Finset α
f : α → β
inst✝² : Fintype β
inst✝¹ : DecidablePred fun y => y ∈ Set.range f
inst✝ : DecidableEq β
⊢ filter (fun y => y ∈ Set.range f) univ = image f univ
[PROOFSTEP]
letI : DecidablePred (fun y => ∃ x, f x = y) := by simpa using ‹_›
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Fintype α
s t : Finset α
f : α → β
inst✝² : Fintype β
inst✝¹ : DecidablePred fun y => y ∈ Set.range f
inst✝ : DecidableEq β
⊢ DecidablePred fun y => ∃ x, f x = y
[PROOFSTEP]
simpa using ‹_›
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Fintype α
s t : Finset α
f : α → β
inst✝² : Fintype β
inst✝¹ : DecidablePred fun y => y ∈ Set.range f
inst✝ : DecidableEq β
this : DecidablePred fun y => ∃ x, f x = y := inst✝¹
⊢ filter (fun y => y ∈ Set.range f) univ = image f univ
[PROOFSTEP]
exact univ_filter_exists f
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
s t : Finset α
p : α → Prop
inst✝ : DecidablePred p
⊢ ↑(filter p univ) = {x | p x}
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type ?u.30074
β : α → Type u_4
inst✝¹ : (a : α) → DecidableEq (β a)
inst✝ : Fintype α
f g : (a : α) → β a
⊢ (∀ (a : α), a ∈ elems → f a = g a) ↔ f = g
[PROOFSTEP]
simp [Function.funext_iff, Fintype.complete]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype α
⊢ (∀ (a : α), a ∈ univ → p a) ↔ ∀ (a : α), p a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype α
⊢ (∃ a, a ∈ univ ∧ p a) ↔ ∃ a, p a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Fintype α
x : α → β
⊢ Decidable (Injective x)
[PROOFSTEP]
unfold Injective
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Fintype α
x : α → β
⊢ Decidable (∀ ⦃a₁ a₂ : α⦄, x a₁ = x a₂ → a₁ = a₂)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
x : α → β
⊢ Decidable (Surjective x)
[PROOFSTEP]
unfold Surjective
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
x : α → β
⊢ Decidable (∀ (b : β), ∃ a, x a = b)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
x : α → β
⊢ Decidable (Bijective x)
[PROOFSTEP]
unfold Bijective
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
x : α → β
⊢ Decidable (Injective x ∧ Surjective x)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : α → β
g : β → α
⊢ Decidable (∀ (x : α), g (f x) = x)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → β
g : β → α
⊢ Decidable (∀ (x : β), f (g x) = x)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Multiset α
H : ∀ (x : α), x ∈ s
⊢ ∀ (x : α), x ∈ Multiset.toFinset s
[PROOFSTEP]
simpa using H
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l : List α
H : ∀ (x : α), x ∈ l
⊢ ∀ (x : α), x ∈ List.toFinset l
[PROOFSTEP]
simpa using H
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
x✝¹ x✝ : Fintype α
s₁ : Finset α
h₁ : ∀ (x : α), x ∈ s₁
s₂ : Finset α
h₂ : ∀ (x : α), x ∈ s₂
⊢ { elems := s₁, complete := h₁ } = { elems := s₂, complete := h₂ }
[PROOFSTEP]
congr
[GOAL]
case e_elems
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
x✝¹ x✝ : Fintype α
s₁ : Finset α
h₁ : ∀ (x : α), x ∈ s₁
s₂ : Finset α
h₂ : ∀ (x : α), x ∈ s₂
⊢ s₁ = s₂
[PROOFSTEP]
simp [Finset.ext_iff, h₁, h₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
b : ↑(Set.range f)
⊢ ∀ (a : α), f a = ↑b ↔ a ∈ univ ∧ (fun a => f a = ↑b) a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α → β
hf : Injective f
inst✝ : Nonempty α
⊢ Set.restrict (Set.range f) (invFun f) = invOfMemRange hf
[PROOFSTEP]
ext ⟨b, h⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α → β
hf : Injective f
inst✝ : Nonempty α
b : β
h : b ∈ Set.range f
⊢ Set.restrict (Set.range f) (invFun f) { val := b, property := h } = invOfMemRange hf { val := b, property := h }
[PROOFSTEP]
apply hf
[GOAL]
case h.mk.a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α → β
hf : Injective f
inst✝ : Nonempty α
b : β
h : b ∈ Set.range f
⊢ f (Set.restrict (Set.range f) (invFun f) { val := b, property := h }) =
    f (invOfMemRange hf { val := b, property := h })
[PROOFSTEP]
simp [hf.left_inv_of_invOfMemRange, @invFun_eq _ _ _ f b (Set.mem_range.mp h)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
a : α
⊢ invOfMemRange hf { val := f a, property := (_ : f a ∈ Set.range f) } = a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α ↪ β
b : ↑(Set.range ↑f)
inst✝ : Nonempty α
⊢ Set.restrict (Set.range ↑f) (invFun ↑f) = invOfMemRange f
[PROOFSTEP]
ext ⟨b, h⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α ↪ β
b✝ : ↑(Set.range ↑f)
inst✝ : Nonempty α
b : β
h : b ∈ Set.range ↑f
⊢ Set.restrict (Set.range ↑f) (invFun ↑f) { val := b, property := h } = invOfMemRange f { val := b, property := h }
[PROOFSTEP]
apply f.injective
[GOAL]
case h.mk.a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α ↪ β
b✝ : ↑(Set.range ↑f)
inst✝ : Nonempty α
b : β
h : b ∈ Set.range ↑f
⊢ ↑f (Set.restrict (Set.range ↑f) (invFun ↑f) { val := b, property := h }) =
    ↑f (invOfMemRange f { val := b, property := h })
[PROOFSTEP]
simp [f.left_inv_of_invOfMemRange, @invFun_eq _ _ _ f b (Set.mem_range.mp h)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α ↪ β
b : ↑(Set.range ↑f)
a : α
⊢ invOfMemRange f { val := ↑f a, property := (_ : ↑f a ∈ Set.range ↑f) } = a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t✝ s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : s = t
⊢ toFinset s = toFinset t
[PROOFSTEP]
subst h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t s : Set α
inst✝¹ inst✝ : Fintype ↑s
⊢ toFinset s = toFinset s
[PROOFSTEP]
congr
[GOAL]
case h.e_3.h
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t s : Set α
inst✝¹ inst✝ : Fintype ↑s
⊢ inst✝¹ = inst✝
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t s : Set α
inst✝ : Fintype ↑s
a : α
⊢ a ∈ toFinset s ↔ a ∈ s
[PROOFSTEP]
simp [toFinset]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
x : α
⊢ x ∈ toFinset p ↔ x ∈ s
[PROOFSTEP]
rw [@mem_toFinset _ _ (id _), H]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t s : Set α
inst✝ : Fintype ↑s
⊢ Finset.Nonempty (toFinset s) ↔ Set.Nonempty s
[PROOFSTEP]
rw [← Finset.coe_nonempty, coe_toFinset]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t✝ s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : toFinset s = toFinset t
⊢ s = t
[PROOFSTEP]
rw [← s.coe_toFinset, h, t.coe_toFinset]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t✝ s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : s = t
⊢ toFinset s = toFinset t
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ toFinset s ⊆ toFinset t ↔ s ⊆ t
[PROOFSTEP]
simp [Finset.subset_iff, Set.subset_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t✝ : Set α
inst✝ : Fintype ↑s
t : Finset α
⊢ toFinset s ⊂ t ↔ s ⊂ ↑t
[PROOFSTEP]
rw [← Finset.coe_ssubset, coe_toFinset]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t : Set α
s : Finset α
inst✝ : Fintype ↑t
⊢ s ⊆ toFinset t ↔ ↑s ⊆ t
[PROOFSTEP]
rw [← Finset.coe_subset, coe_toFinset]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t : Set α
s : Finset α
inst✝ : Fintype ↑t
⊢ s ⊂ toFinset t ↔ ↑s ⊂ t
[PROOFSTEP]
rw [← Finset.coe_ssubset, coe_toFinset]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ toFinset s ⊂ toFinset t ↔ s ⊂ t
[PROOFSTEP]
simp only [Finset.ssubset_def, toFinset_subset_toFinset, ssubset_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t✝ : Set α
inst✝ : Fintype ↑s
t : Finset α
⊢ toFinset s ⊆ t ↔ s ⊆ ↑t
[PROOFSTEP]
rw [← Finset.coe_subset, coe_toFinset]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ Disjoint (toFinset s) (toFinset t) ↔ Disjoint s t
[PROOFSTEP]
simp only [← disjoint_coe, coe_toFinset]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∩ t)
⊢ toFinset (s ∩ t) = toFinset s ∩ toFinset t
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∩ t)
a✝ : α
⊢ a✝ ∈ toFinset (s ∩ t) ↔ a✝ ∈ toFinset s ∩ toFinset t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∪ t)
⊢ toFinset (s ∪ t) = toFinset s ∪ toFinset t
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∪ t)
a✝ : α
⊢ a✝ ∈ toFinset (s ∪ t) ↔ a✝ ∈ toFinset s ∪ toFinset t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s \ t)
⊢ toFinset (s \ t) = toFinset s \ toFinset t
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s \ t)
a✝ : α
⊢ a✝ ∈ toFinset (s \ t) ↔ a✝ ∈ toFinset s \ toFinset t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∆ t)
⊢ toFinset (s ∆ t) = toFinset s ∆ toFinset t
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∆ t)
a✝ : α
⊢ a✝ ∈ toFinset (s ∆ t) ↔ a✝ ∈ toFinset s ∆ toFinset t
[PROOFSTEP]
simp [mem_symmDiff, Finset.mem_symmDiff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
inst✝⁴ : DecidableEq α
inst✝³ : Fintype ↑s
inst✝² : Fintype ↑t
inst✝¹ : Fintype α
inst✝ : Fintype ↑sᶜ
⊢ toFinset sᶜ = (toFinset s)ᶜ
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
inst✝⁴ : DecidableEq α
inst✝³ : Fintype ↑s
inst✝² : Fintype ↑t
inst✝¹ : Fintype α
inst✝ : Fintype ↑sᶜ
a✝ : α
⊢ a✝ ∈ toFinset sᶜ ↔ a✝ ∈ (toFinset s)ᶜ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
inst✝ : Fintype ↑∅
⊢ toFinset ∅ = ∅
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
inst✝ : Fintype ↑∅
a✝ : α
⊢ a✝ ∈ toFinset ∅ ↔ a✝ ∈ ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
inst✝¹ : Fintype α
inst✝ : Fintype ↑univ
⊢ toFinset univ = Finset.univ
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
inst✝¹ : Fintype α
inst✝ : Fintype ↑univ
a✝ : α
⊢ a✝ ∈ toFinset univ ↔ a✝ ∈ Finset.univ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
inst✝ : Fintype ↑s
⊢ toFinset s = ∅ ↔ s = ∅
[PROOFSTEP]
rw [← toFinset_empty, toFinset_inj]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
inst✝¹ : Fintype α
inst✝ : Fintype ↑s
⊢ toFinset s = Finset.univ ↔ s = univ
[PROOFSTEP]
rw [← coe_inj, coe_toFinset, coe_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype ↑{x | p x}
⊢ toFinset {x | p x} = filter p Finset.univ
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype ↑{x | p x}
a✝ : α
⊢ a✝ ∈ toFinset {x | p x} ↔ a✝ ∈ filter p Finset.univ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t : Set α
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ toFinset s ⊂ Finset.univ ↔ s ⊂ univ
[PROOFSTEP]
rw [← coe_ssubset, coe_toFinset, coe_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t : Set α
inst✝² : DecidableEq β
f : α → β
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑(f '' s)
⊢ ↑(toFinset (f '' s)) = ↑(Finset.image f (toFinset s))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
inst✝² : DecidableEq α
inst✝¹ : Fintype β
f : β → α
inst✝ : Fintype ↑(range f)
⊢ toFinset (range f) = Finset.image f Finset.univ
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
inst✝² : DecidableEq α
inst✝¹ : Fintype β
f : β → α
inst✝ : Fintype ↑(range f)
a✝ : α
⊢ a✝ ∈ toFinset (range f) ↔ a✝ ∈ Finset.image f Finset.univ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
a : α
inst✝ : Fintype ↑{a}
⊢ toFinset {a} = {a}
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
a : α
inst✝ : Fintype ↑{a}
a✝ : α
⊢ a✝ ∈ toFinset {a} ↔ a✝ ∈ {a}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t : Set α
inst✝² : DecidableEq α
a : α
s : Set α
inst✝¹ : Fintype ↑(insert a s)
inst✝ : Fintype ↑s
⊢ toFinset (insert a s) = insert a (toFinset s)
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t : Set α
inst✝² : DecidableEq α
a : α
s : Set α
inst✝¹ : Fintype ↑(insert a s)
inst✝ : Fintype ↑s
a✝ : α
⊢ a✝ ∈ toFinset (insert a s) ↔ a✝ ∈ insert a (toFinset s)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t : Set α
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x => x ∈ s
⊢ filter (fun x => x ∈ s) Finset.univ = toFinset s
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t : Set α
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x => x ∈ s
a✝ : α
⊢ a✝ ∈ filter (fun x => x ∈ s) Finset.univ ↔ a✝ ∈ toFinset s
[PROOFSTEP]
simp only [Finset.mem_univ, decide_eq_true_eq, forall_true_left, mem_filter, true_and, mem_toFinset]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
i : Fin (n + 1)
⊢ image (succAbove i) univ = {i}ᶜ
[PROOFSTEP]
ext m
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
i m : Fin (n + 1)
⊢ m ∈ image (succAbove i) univ ↔ m ∈ {i}ᶜ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
⊢ image succ univ = {0}ᶜ
[PROOFSTEP]
rw [← Fin.succAbove_zero, Fin.image_succAbove_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
⊢ image castSucc univ = {last n}ᶜ
[PROOFSTEP]
rw [← Fin.succAbove_last, Fin.image_succAbove_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
⊢ ¬0 ∈ map { toFun := succ, inj' := (_ : Injective succ) } univ
[PROOFSTEP]
simp [map_eq_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
⊢ univ =
    cons 0 (map { toFun := succ, inj' := (_ : Injective succ) } univ)
      (_ : ¬0 ∈ map { toFun := succ, inj' := (_ : Injective succ) } univ)
[PROOFSTEP]
simp [map_eq_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
⊢ ¬last n ∈ map castSuccEmb.toEmbedding univ
[PROOFSTEP]
simp [map_eq_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
⊢ univ =
    cons (last n) (map castSuccEmb.toEmbedding univ)
      (_ :
        ¬last n ∈ map { toFun := castSucc, inj' := (_ : ∀ (x x_1 : Fin n), castSucc x = castSucc x_1 → x = x_1) } univ)
[PROOFSTEP]
simp [map_eq_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
p : Fin (n + 1)
⊢ ¬p ∈ map (succAboveEmb p).toEmbedding univ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
p : Fin (n + 1)
⊢ univ =
    cons p (map (succAboveEmb p).toEmbedding univ)
      (_ :
        ¬p ∈
            map { toFun := succAbove p, inj' := (_ : ∀ (x x_1 : Fin n), succAbove p x = succAbove p x_1 → x = x_1) }
              univ)
[PROOFSTEP]
simp [map_eq_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
y : α
⊢ ∀ (x : α), x ∈ {y} ↔ x = y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
y : α
⊢ ∀ (x : α), x ∈ {y} ↔ y = x
[PROOFSTEP]
simp [eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ Multiset.Nodup {true, false}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : Bool
⊢ x ∈ { val := {true, false}, nodup := (_ : Multiset.Nodup {true, false}) }
[PROOFSTEP]
cases x
[GOAL]
case false
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ false ∈ { val := {true, false}, nodup := (_ : Multiset.Nodup {true, false}) }
[PROOFSTEP]
simp
[GOAL]
case true
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ true ∈ { val := {true, false}, nodup := (_ : Multiset.Nodup {true, false}) }
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type ?u.106979
β : Type ?u.106978
inst✝² : DecidableEq α
inst✝¹ : Fintype (α × β)
inst✝ : Nonempty β
a : α
⊢ a ∈ image Prod.fst univ
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type ?u.109138
β : Type ?u.109137
inst✝² : DecidableEq β
inst✝¹ : Fintype (α × β)
inst✝ : Nonempty α
b : β
⊢ b ∈ image Prod.snd univ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α → β
⊢ ↑(image f univ) = Set.range f
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α → β
x : β
⊢ x ∈ ↑(image f univ) ↔ x ∈ Set.range f
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
inst✝ : Decidable p
x✝ : PLift p
h : p
⊢ { down := h } ∈ if h : p then {{ down := h }} else ∅
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ Multiset.Nodup {True, False}
[PROOFSTEP]
simp [true_ne_false]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ True ∈ { val := {True, False}, nodup := (_ : Multiset.Nodup (True ::ₘ {False})) }
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ False ∈ { val := {True, False}, nodup := (_ : Multiset.Nodup (True ::ₘ {False})) }
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ univ.val = {True, False}.val
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ univ.val = True ::ₘ {False}
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype α
⊢ ∀ (x : α), x ∈ filter p univ ↔ p x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
⊢ Set α → Finset α
[PROOFSTEP]
classical exact fun s => s.toFinset
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
⊢ Set α → Finset α
[PROOFSTEP]
exact fun s => s.toFinset
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
s : Finset α
⊢ Set.toFinset ↑s = s
[PROOFSTEP]
convert Finset.toFinset_coe s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
s : Set α
⊢ ↑(Set.toFinset s) = s
[PROOFSTEP]
classical exact s.coe_toFinset
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
s : Set α
⊢ ↑(Set.toFinset s) = s
[PROOFSTEP]
exact s.coe_toFinset
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ ↑finsetEquivSet.symm s = Set.toFinset s
[PROOFSTEP]
simp [finsetEquivSet]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ Set.toFinset s = Set.toFinset s
[PROOFSTEP]
congr
[GOAL]
case h.e_3.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ (Subtype.fintype fun x => x ∈ s) = inst✝
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Prop
β : α → Prop
inst✝¹ : Decidable α
inst✝ : (a : α) → Decidable (β a)
h : ∃ a, β a
x✝ : (a : α) ×' β a
fst✝ : α
snd✝ : β fst✝
⊢ { fst := fst✝, snd := snd✝ } ∈ {{ fst := (_ : α), snd := (_ : β (_ : α)) }}
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
inst✝¹ : Decidable p
α : p → Type u_4
inst✝ : (hp : p) → Fintype (α hp)
hp : ¬p
h : (hp : p) → α hp
x : p
⊢ h x = False.elim (_ : False)
[PROOFSTEP]
contradiction
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α → β
b : β
⊢ b ∈ image f univ ↔ b ∈ Set.range f
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
hp : ∃! a, p a
⊢ ∃! a, a ∈ univ ∧ p a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
hp : ∃! a, p a
⊢ ∃! a, p a
[PROOFSTEP]
exact hp
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Fintype α✝
p✝ : α✝ → Prop
inst✝² : DecidablePred p✝
α : Type u_4
p : α → Prop
inst✝¹ : Fintype { a // p a }
inst✝ : DecidableEq α
x y : { a // p a }
hy : (fun a => ↑a = ↑x) y
⊢ y = x
[PROOFSTEP]
simpa [Subtype.ext_iff] using hy
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Fintype α✝
p✝ : α✝ → Prop
inst✝² : DecidablePred p✝
α : Type u_4
p : α → Prop
inst✝¹ : Fintype { a // p a }
inst✝ : DecidableEq α
x : { a // p a }
h : optParam (∃! a, ↑a = ↑x) (_ : ∃ x_1, (fun a => ↑a = ↑x) x_1 ∧ ∀ (y : { a // p a }), (fun a => ↑a = ↑x) y → y = x_1)
⊢ choose (fun y => ↑y = ↑x) h = x
[PROOFSTEP]
rw [Subtype.ext_iff, Fintype.choose_spec (fun y : { a : α // p a } => (y : α) = x) _]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α → β
f_bij : Bijective f
b : β
⊢ ∃! a, (fun a => f a = b) a
[PROOFSTEP]
rcases f_bij.right b with ⟨a', fa_eq_b⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α → β
f_bij : Bijective f
b : β
a' : α
fa_eq_b : f a' = b
⊢ ∃! a, (fun a => f a = b) a
[PROOFSTEP]
rw [← fa_eq_b]
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α → β
f_bij : Bijective f
b : β
a' : α
fa_eq_b : f a' = b
⊢ ∃! a, (fun a => f a = f a') a
[PROOFSTEP]
exact ⟨a', ⟨rfl, fun a h => f_bij.left h⟩⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type ?u.140463
s : Multiset α
l : List α
h : ∃ x, x ∈ Quotient.mk (List.isSetoid α) l
x✝ : ∃ x, x ∈ Quotient.mk (List.isSetoid α) []
⊢ False
[PROOFSTEP]
tauto
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type ?u.141508
inst✝¹ : Nonempty α
inst✝ : Fintype α
⊢ ∃ x, x ∈ univ.val
[PROOFSTEP]
simp
[GOAL]
a✝ : ℕ
n : ℕ := a✝
i : Fin n
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (↑i) a✝
[PROOFSTEP]
exact i.2
[GOAL]
α : Type u_4
inst✝ : DecidableEq α
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
a✝² : ℕ
a✝¹ : (y : ℕ) → (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y a✝² → α
n : ℕ := a✝²
a✝ : ∀ (x : α), x ∈ image (fun i => a✝¹ ↑i (_ : ↑i < n)) univ → P x
i : Fin n
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (↑i) a✝²
[PROOFSTEP]
exact i.2
[GOAL]
a✝ : ℕ
n : ℕ := a✝
i : Fin n
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (↑i) a✝
[PROOFSTEP]
exact i.2
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
[PROOFSTEP]
classical
have : Nonempty α := by
  rcases h ∅ (by simp) with ⟨y, _⟩
  exact ⟨y⟩
choose! F hF using h
have h' : ∀ s : Finset α, ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y := fun s => ⟨F s, hF s⟩
set f := seqOfForallFinsetExistsAux P r h' with hf
have A : ∀ n : ℕ, P (f n) := by
  intro n
  induction' n using Nat.strong_induction_on with n IH
  have IH' : ∀ x : Fin n, P (f x) := fun n => IH n.1 n.2
  rw [hf, seqOfForallFinsetExistsAux]
  exact
    (Classical.choose_spec (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n)))) (by simp [IH'])).1
refine' ⟨f, A, fun m n hmn => _⟩
conv_rhs => rw [hf]
rw [seqOfForallFinsetExistsAux]
apply (Classical.choose_spec (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n)))) (by simp [A])).2
exact Finset.mem_image.2 ⟨⟨m, hmn⟩, Finset.mem_univ _, rfl⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
[PROOFSTEP]
have : Nonempty α := by
  rcases h ∅ (by simp) with ⟨y, _⟩
  exact ⟨y⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
⊢ Nonempty α
[PROOFSTEP]
rcases h ∅ (by simp) with ⟨y, _⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
⊢ ∀ (x : α), x ∈ ∅ → P x
[PROOFSTEP]
simp
[GOAL]
case intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
y : α
h✝ : P y ∧ ∀ (x : α), x ∈ ∅ → r x y
⊢ Nonempty α
[PROOFSTEP]
exact ⟨y⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
this : Nonempty α
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
[PROOFSTEP]
choose! F hF using h
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
[PROOFSTEP]
have h' : ∀ s : Finset α, ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y := fun s => ⟨F s, hF s⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
[PROOFSTEP]
set f := seqOfForallFinsetExistsAux P r h' with hf
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
[PROOFSTEP]
have A : ∀ n : ℕ, P (f n) := by
  intro n
  induction' n using Nat.strong_induction_on with n IH
  have IH' : ∀ x : Fin n, P (f x) := fun n => IH n.1 n.2
  rw [hf, seqOfForallFinsetExistsAux]
  exact
    (Classical.choose_spec (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n)))) (by simp [IH'])).1
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
⊢ ∀ (n : ℕ), P (f n)
[PROOFSTEP]
intro n
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
⊢ P (f n)
[PROOFSTEP]
induction' n using Nat.strong_induction_on with n IH
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ (m : ℕ), m < n → P (f m)
⊢ P (f n)
[PROOFSTEP]
have IH' : ∀ x : Fin n, P (f x) := fun n => IH n.1 n.2
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ (m : ℕ), m < n → P (f m)
IH' : ∀ (x : Fin n), P (f ↑x)
⊢ P (f n)
[PROOFSTEP]
rw [hf, seqOfForallFinsetExistsAux]
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ (m : ℕ), m < n → P (f m)
IH' : ∀ (x : Fin n), P (f ↑x)
⊢ P
    (Classical.choose
      (_ :
        ∃ y,
          (∀ (x : α), x ∈ image (fun i => seqOfForallFinsetExistsAux P r h' ↑i) univ → P x) →
            P y ∧ ∀ (x : α), x ∈ image (fun i => seqOfForallFinsetExistsAux P r h' ↑i) univ → r x y))
[PROOFSTEP]
exact
  (Classical.choose_spec (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n)))) (by simp [IH'])).1
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ (m : ℕ), m < n → P (f m)
IH' : ∀ (x : Fin n), P (f ↑x)
⊢ ∀ (x : α), x ∈ image (fun i => f ↑i) univ → P x
[PROOFSTEP]
simp [IH']
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
[PROOFSTEP]
refine' ⟨f, A, fun m n hmn => _⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ r (f m) (f n)
[PROOFSTEP]
conv_rhs => rw [hf]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
| f n
[PROOFSTEP]
rw [hf]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
| f n
[PROOFSTEP]
rw [hf]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
| f n
[PROOFSTEP]
rw [hf]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ r (f m) (seqOfForallFinsetExistsAux P r h' n)
[PROOFSTEP]
rw [seqOfForallFinsetExistsAux]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ r (f m)
    (Classical.choose
      (_ :
        ∃ y,
          (∀ (x : α), x ∈ image (fun i => seqOfForallFinsetExistsAux P r h' ↑i) univ → P x) →
            P y ∧ ∀ (x : α), x ∈ image (fun i => seqOfForallFinsetExistsAux P r h' ↑i) univ → r x y))
[PROOFSTEP]
apply (Classical.choose_spec (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n)))) (by simp [A])).2
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ ∀ (x : α), x ∈ image (fun i => f ↑i) univ → P x
[PROOFSTEP]
simp [A]
[GOAL]
case a
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ f m ∈ image (fun i => f ↑i) univ
[PROOFSTEP]
exact Finset.mem_image.2 ⟨⟨m, hmn⟩, Finset.mem_univ _, rfl⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m ≠ n → r (f m) (f n)
[PROOFSTEP]
rcases exists_seq_of_forall_finset_exists P r h with ⟨f, hf, hf'⟩
[GOAL]
case intro.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α
hf : ∀ (n : ℕ), P (f n)
hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m ≠ n → r (f m) (f n)
[PROOFSTEP]
refine' ⟨f, hf, fun m n hmn => _⟩
[GOAL]
case intro.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α
hf : ∀ (n : ℕ), P (f n)
hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)
m n : ℕ
hmn : m ≠ n
⊢ r (f m) (f n)
[PROOFSTEP]
rcases lt_trichotomy m n with (h | rfl | h)
[GOAL]
case intro.intro.inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h✝ : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α
hf : ∀ (n : ℕ), P (f n)
hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)
m n : ℕ
hmn : m ≠ n
h : m < n
⊢ r (f m) (f n)
[PROOFSTEP]
exact hf' m n h
[GOAL]
case intro.intro.inr.inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α
hf : ∀ (n : ℕ), P (f n)
hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)
m : ℕ
hmn : m ≠ m
⊢ r (f m) (f m)
[PROOFSTEP]
exact (hmn rfl).elim
[GOAL]
case intro.intro.inr.inr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h✝ : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α
hf : ∀ (n : ℕ), P (f n)
hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)
m n : ℕ
hmn : m ≠ n
h : n < m
⊢ r (f m) (f n)
[PROOFSTEP]
apply symm
[GOAL]
case intro.intro.inr.inr.a
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h✝ : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α
hf : ∀ (n : ℕ), P (f n)
hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)
m n : ℕ
hmn : m ≠ n
h : n < m
⊢ r (f n) (f m)
[PROOFSTEP]
exact hf' n m h


[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