case empty
α✝ : Type ?u.117523
β : Type ?u.117526
γ : Type ?u.117529
inst✝ : DecidableEq α✝
s✝ t u v : Finset α✝
a b : α✝
α : Type u_1
p : (s : Finset α) → Finset.Nonempty s → Prop
h₀ : ∀ (a : α), p {a} (_ : Finset.Nonempty {a})
h₁ :
  ∀ ⦃a : α⦄ (s : Finset α) (h : ¬a ∈ s) (hs : Finset.Nonempty s),
    p s hs → p (cons a s h) (_ : Finset.Nonempty (cons a s h))
s : Finset α
hs✝ : Finset.Nonempty s
hs : Finset.Nonempty ∅
⊢ p ∅ hs

case cons
α✝ : Type ?u.117523
β : Type ?u.117526
γ : Type ?u.117529
inst✝ : DecidableEq α✝
s✝ t✝ u v : Finset α✝
a✝ b : α✝
α : Type u_1
p : (s : Finset α) → Finset.Nonempty s → Prop
h₀ : ∀ (a : α), p {a} (_ : Finset.Nonempty {a})
h₁ :
  ∀ ⦃a : α⦄ (s : Finset α) (h : ¬a ∈ s) (hs : Finset.Nonempty s),
    p s hs → p (cons a s h) (_ : Finset.Nonempty (cons a s h))
s : Finset α
hs✝ : Finset.Nonempty s
a : α
t : Finset α
ha : ¬a ∈ t
h : ∀ (hs : Finset.Nonempty t), p t hs
hs : Finset.Nonempty (cons a t ha)
⊢ p (cons a t ha) hs
α✝ : Type ?u.117523
β : Type ?u.117526
γ : Type ?u.117529
inst✝ : DecidableEq α✝
s✝ t u v : Finset α✝
a b : α✝
α : Type u_1
p : (s : Finset α) → Finset.Nonempty s → Prop
h₀ : ∀ (a : α), p {a} (_ : Finset.Nonempty {a})
h₁ :
  ∀ ⦃a : α⦄ (s : Finset α) (h : ¬a ∈ s) (hs : Finset.Nonempty s),
    p s hs → p (cons a s h) (_ : Finset.Nonempty (cons a s h))
s : Finset α
hs : Finset.Nonempty s
⊢ p s hs
induction' s using Finset.cons_induction with a t ha h
case cons.inl
α✝ : Type ?u.117523
β : Type ?u.117526
γ : Type ?u.117529
inst✝ : DecidableEq α✝
s✝ t u v : Finset α✝
a✝ b : α✝
α : Type u_1
p : (s : Finset α) → Finset.Nonempty s → Prop
h₀ : ∀ (a : α), p {a} (_ : Finset.Nonempty {a})
h₁ :
  ∀ ⦃a : α⦄ (s : Finset α) (h : ¬a ∈ s) (hs : Finset.Nonempty s),
    p s hs → p (cons a s h) (_ : Finset.Nonempty (cons a s h))
s : Finset α
hs✝ : Finset.Nonempty s
a : α
ha : ¬a ∈ ∅
h : ∀ (hs : Finset.Nonempty ∅), p ∅ hs
hs : Finset.Nonempty (cons a ∅ ha)
⊢ p (cons a ∅ ha) hs

case cons.inr
α✝ : Type ?u.117523
β : Type ?u.117526
γ : Type ?u.117529
inst✝ : DecidableEq α✝
s✝ t✝ u v : Finset α✝
a✝ b : α✝
α : Type u_1
p : (s : Finset α) → Finset.Nonempty s → Prop
h₀ : ∀ (a : α), p {a} (_ : Finset.Nonempty {a})
h₁ :
  ∀ ⦃a : α⦄ (s : Finset α) (h : ¬a ∈ s) (hs : Finset.Nonempty s),
    p s hs → p (cons a s h) (_ : Finset.Nonempty (cons a s h))
s : Finset α
hs✝ : Finset.Nonempty s
a : α
t : Finset α
ha : ¬a ∈ t
h : ∀ (hs : Finset.Nonempty t), p t hs
hs : Finset.Nonempty (cons a t ha)
ht : Finset.Nonempty t
⊢ p (cons a t ha) hs
case cons
α✝ : Type ?u.117523
β : Type ?u.117526
γ : Type ?u.117529
inst✝ : DecidableEq α✝
s✝ t✝ u v : Finset α✝
a✝ b : α✝
α : Type u_1
p : (s : Finset α) → Finset.Nonempty s → Prop
h₀ : ∀ (a : α), p {a} (_ : Finset.Nonempty {a})
h₁ :
  ∀ ⦃a : α⦄ (s : Finset α) (h : ¬a ∈ s) (hs : Finset.Nonempty s),
    p s hs → p (cons a s h) (_ : Finset.Nonempty (cons a s h))
s : Finset α
hs✝ : Finset.Nonempty s
a : α
t : Finset α
ha : ¬a ∈ t
h : ∀ (hs : Finset.Nonempty t), p t hs
hs : Finset.Nonempty (cons a t ha)
⊢ p (cons a t ha) hs
obtain rfl | ht := t.eq_empty_or_nonempty
no goals
case empty
α✝ : Type ?u.117523
β : Type ?u.117526
γ : Type ?u.117529
inst✝ : DecidableEq α✝
s✝ t u v : Finset α✝
a b : α✝
α : Type u_1
p : (s : Finset α) → Finset.Nonempty s → Prop
h₀ : ∀ (a : α), p {a} (_ : Finset.Nonempty {a})
h₁ :
  ∀ ⦃a : α⦄ (s : Finset α) (h : ¬a ∈ s) (hs : Finset.Nonempty s),
    p s hs → p (cons a s h) (_ : Finset.Nonempty (cons a s h))
s : Finset α
hs✝ : Finset.Nonempty s
hs : Finset.Nonempty ∅
⊢ p ∅ hs
exact (not_nonempty_empty hs).elim
no goals
case cons.inl
α✝ : Type ?u.117523
β : Type ?u.117526
γ : Type ?u.117529
inst✝ : DecidableEq α✝
s✝ t u v : Finset α✝
a✝ b : α✝
α : Type u_1
p : (s : Finset α) → Finset.Nonempty s → Prop
h₀ : ∀ (a : α), p {a} (_ : Finset.Nonempty {a})
h₁ :
  ∀ ⦃a : α⦄ (s : Finset α) (h : ¬a ∈ s) (hs : Finset.Nonempty s),
    p s hs → p (cons a s h) (_ : Finset.Nonempty (cons a s h))
s : Finset α
hs✝ : Finset.Nonempty s
a : α
ha : ¬a ∈ ∅
h : ∀ (hs : Finset.Nonempty ∅), p ∅ hs
hs : Finset.Nonempty (cons a ∅ ha)
⊢ p (cons a ∅ ha) hs
exact h₀ a
no goals
case cons.inr
α✝ : Type ?u.117523
β : Type ?u.117526
γ : Type ?u.117529
inst✝ : DecidableEq α✝
s✝ t✝ u v : Finset α✝
a✝ b : α✝
α : Type u_1
p : (s : Finset α) → Finset.Nonempty s → Prop
h₀ : ∀ (a : α), p {a} (_ : Finset.Nonempty {a})
h₁ :
  ∀ ⦃a : α⦄ (s : Finset α) (h : ¬a ∈ s) (hs : Finset.Nonempty s),
    p s hs → p (cons a s h) (_ : Finset.Nonempty (cons a s h))
s : Finset α
hs✝ : Finset.Nonempty s
a : α
t : Finset α
ha : ¬a ∈ t
h : ∀ (hs : Finset.Nonempty t), p t hs
hs : Finset.Nonempty (cons a t ha)
ht : Finset.Nonempty t
⊢ p (cons a t ha) hs
exact h₁ t ha ht (h ht)