[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
