case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, ¬a ∈ s → Set.Finite s → C s → C (insert a s)
s : Finset α
⊢ C ↑s
α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
s : Set α
h : Set.Finite s
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, ¬a ∈ s → Set.Finite s → C s → C (insert a s)
⊢ C s
lift s to Finset α using h
case intro.h₁
α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, ¬a ∈ s → Set.Finite s → C s → C (insert a s)
⊢ C ↑∅

case intro.h₂
α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, ¬a ∈ s → Set.Finite s → C s → C (insert a s)
a : α
s : Finset α
ha : ¬a ∈ s
hs : C ↑s
⊢ C ↑(Finset.cons a s ha)
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, ¬a ∈ s → Set.Finite s → C s → C (insert a s)
s : Finset α
⊢ C ↑s
induction' s using Finset.cons_induction_on with a s ha hs
no goals
case intro.h₁
α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, ¬a ∈ s → Set.Finite s → C s → C (insert a s)
⊢ C ↑∅
rwa [Finset.coe_empty]
case intro.h₂
α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, ¬a ∈ s → Set.Finite s → C s → C (insert a s)
a : α
s : Finset α
ha : ¬a ∈ s
hs : C ↑s
⊢ C (insert a ↑s)
case intro.h₂
α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, ¬a ∈ s → Set.Finite s → C s → C (insert a s)
a : α
s : Finset α
ha : ¬a ∈ s
hs : C ↑s
⊢ C ↑(Finset.cons a s ha)
rw [Finset.coe_cons]
no goals
case intro.h₂
α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, ¬a ∈ s → Set.Finite s → C s → C (insert a s)
a : α
s : Finset α
ha : ¬a ∈ s
hs : C ↑s
⊢ C (insert a ↑s)
exact @H1 a s ha (Set.toFinite _) hs