no goals
case empty
α✝ : Type ?u.115585
β : Type ?u.115588
γ : Type ?u.115591
inst✝ : DecidableEq α✝
s t u v : Finset α✝
a b : α✝
α : Type u_1
p : Finset α → Prop
empty : p ∅
cons : ∀ ⦃a : α⦄ {s : Finset α} (h : ¬a ∈ s), p s → p (Finset.cons a s h)
nd : Nodup 0
⊢ p { val := 0, nodup := nd }
exact empty
case cons.intro
α✝ : Type ?u.115585
β : Type ?u.115588
γ : Type ?u.115591
inst✝ : DecidableEq α✝
s✝ t u v : Finset α✝
a✝ b : α✝
α : Type u_1
p : Finset α → Prop
empty : p ∅
cons : ∀ ⦃a : α⦄ {s : Finset α} (h : ¬a ∈ s), p s → p (Finset.cons a s h)
a : α
s : Multiset α
IH : ∀ (nd : Nodup s), p { val := s, nodup := nd }
nd : Nodup (a ::ₘ s)
m : ¬a ∈ s
nd' : Nodup s
⊢ p { val := a ::ₘ s, nodup := nd }
case cons
α✝ : Type ?u.115585
β : Type ?u.115588
γ : Type ?u.115591
inst✝ : DecidableEq α✝
s✝ t u v : Finset α✝
a✝ b : α✝
α : Type u_1
p : Finset α → Prop
empty : p ∅
cons : ∀ ⦃a : α⦄ {s : Finset α} (h : ¬a ∈ s), p s → p (Finset.cons a s h)
a : α
s : Multiset α
IH : ∀ (nd : Nodup s), p { val := s, nodup := nd }
nd : Nodup (a ::ₘ s)
⊢ p { val := a ::ₘ s, nodup := nd }
cases' nodup_cons.1 nd with m nd'
case cons.intro
α✝ : Type ?u.115585
β : Type ?u.115588
γ : Type ?u.115591
inst✝ : DecidableEq α✝
s✝ t u v : Finset α✝
a✝ b : α✝
α : Type u_1
p : Finset α → Prop
empty : p ∅
cons : ∀ ⦃a : α⦄ {s : Finset α} (h : ¬a ∈ s), p s → p (Finset.cons a s h)
a : α
s : Multiset α
IH : ∀ (nd : Nodup s), p { val := s, nodup := nd }
nd : Nodup (a ::ₘ s)
m : ¬a ∈ s
nd' : Nodup s
⊢ p (Finset.cons a { val := s, nodup := ?m.115914 } m)

α✝ : Type ?u.115585
β : Type ?u.115588
γ : Type ?u.115591
inst✝ : DecidableEq α✝
s✝ t u v : Finset α✝
a✝ b : α✝
α : Type u_1
p : Finset α → Prop
empty : p ∅
cons : ∀ ⦃a : α⦄ {s : Finset α} (h : ¬a ∈ s), p s → p (Finset.cons a s h)
a : α
s : Multiset α
IH : ∀ (nd : Nodup s), p { val := s, nodup := nd }
nd : Nodup (a ::ₘ s)
m : ¬a ∈ s
nd' : Nodup s
⊢ Nodup s

α✝ : Type ?u.115585
β : Type ?u.115588
γ : Type ?u.115591
inst✝ : DecidableEq α✝
s✝ t u v : Finset α✝
a✝ b : α✝
α : Type u_1
p : Finset α → Prop
empty : p ∅
cons : ∀ ⦃a : α⦄ {s : Finset α} (h : ¬a ∈ s), p s → p (Finset.cons a s h)
a : α
s : Multiset α
IH : ∀ (nd : Nodup s), p { val := s, nodup := nd }
nd : Nodup (a ::ₘ s)
m : ¬a ∈ s
nd' : Nodup s
⊢ (Finset.cons a { val := s, nodup := ?m.115914 } m).val = { val := a ::ₘ s, nodup := nd }.val
case cons.intro
α✝ : Type ?u.115585
β : Type ?u.115588
γ : Type ?u.115591
inst✝ : DecidableEq α✝
s✝ t u v : Finset α✝
a✝ b : α✝
α : Type u_1
p : Finset α → Prop
empty : p ∅
cons : ∀ ⦃a : α⦄ {s : Finset α} (h : ¬a ∈ s), p s → p (Finset.cons a s h)
a : α
s : Multiset α
IH : ∀ (nd : Nodup s), p { val := s, nodup := nd }
nd : Nodup (a ::ₘ s)
m : ¬a ∈ s
nd' : Nodup s
⊢ p { val := a ::ₘ s, nodup := nd }
rw [← (eq_of_veq _ : Finset.cons a ⟨s, _⟩ m = ⟨a ::ₘ s, nd⟩)]
no goals
case cons.intro
α✝ : Type ?u.115585
β : Type ?u.115588
γ : Type ?u.115591
inst✝ : DecidableEq α✝
s✝ t u v : Finset α✝
a✝ b : α✝
α : Type u_1
p : Finset α → Prop
empty : p ∅
cons : ∀ ⦃a : α⦄ {s : Finset α} (h : ¬a ∈ s), p s → p (Finset.cons a s h)
a : α
s : Multiset α
IH : ∀ (nd : Nodup s), p { val := s, nodup := nd }
nd : Nodup (a ::ₘ s)
m : ¬a ∈ s
nd' : Nodup s
⊢ p (Finset.cons a { val := s, nodup := ?m.115914 } m)
exact cons m (IH nd')
no goals
α✝ : Type ?u.115585
β : Type ?u.115588
γ : Type ?u.115591
inst✝ : DecidableEq α✝
s✝ t u v : Finset α✝
a✝ b : α✝
α : Type u_1
p : Finset α → Prop
empty : p ∅
cons : ∀ ⦃a : α⦄ {s : Finset α} (h : ¬a ∈ s), p s → p (Finset.cons a s h)
a : α
s : Multiset α
IH : ∀ (nd : Nodup s), p { val := s, nodup := nd }
nd : Nodup (a ::ₘ s)
m : ¬a ∈ s
nd' : Nodup s
⊢ (Finset.cons a { val := s, nodup := nd' } m).val = { val := a ::ₘ s, nodup := nd }.val
rw [cons_val]