case intro
α✝ : Type ?u.13579
β : Type ?u.13582
γ : Type ?u.13585
α : Type u_1
inst✝ : Finite α
val✝ : Fintype α
⊢ ∃ l, List.Nodup l ∧ ∀ (x : α), x ∈ l
α✝ : Type ?u.13579
β : Type ?u.13582
γ : Type ?u.13585
α : Type u_1
inst✝ : Finite α
⊢ ∃ l, List.Nodup l ∧ ∀ (x : α), x ∈ l
cases nonempty_fintype α
case intro.intro
α✝ : Type ?u.13579
β : Type ?u.13582
γ : Type ?u.13585
α : Type u_1
inst✝ : Finite α
val✝ : Fintype α
l : List α
e : Quotient.mk (List.isSetoid α) l = univ.val
⊢ ∃ l, List.Nodup l ∧ ∀ (x : α), x ∈ l
case intro
α✝ : Type ?u.13579
β : Type ?u.13582
γ : Type ?u.13585
α : Type u_1
inst✝ : Finite α
val✝ : Fintype α
⊢ ∃ l, List.Nodup l ∧ ∀ (x : α), x ∈ l
obtain ⟨l, e⟩ := Quotient.exists_rep (@univ α _).1
case intro.intro
α✝ : Type ?u.13579
β : Type ?u.13582
γ : Type ?u.13585
α : Type u_1
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
case intro.intro
α✝ : Type ?u.13579
β : Type ?u.13582
γ : Type ?u.13585
α : Type u_1
inst✝ : Finite α
val✝ : Fintype α
l : List α
e : Quotient.mk (List.isSetoid α) l = univ.val
⊢ ∃ l, List.Nodup l ∧ ∀ (x : α), x ∈ l
have := And.intro (@univ α _).2 (@mem_univ_val α _)
no goals
case intro.intro
α✝ : Type ?u.13579
β : Type ?u.13582
γ : Type ?u.13585
α : Type u_1
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
exact ⟨_, by rwa [← e] at this⟩
no goals
α✝ : Type ?u.13579
β : Type ?u.13582
γ : Type ?u.13585
α : Type u_1
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.13770 ∧ ∀ (x : α), x ∈ ?m.13770
rwa [← e] at this