blob: 1287c8efbaddbb880ad8453776e20b4d991450e0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
import Mathlib.Tactic
namespace Finset.Nonempty
theorem induction
{α : Type} {motive : Finset α → Prop} [DecidableEq α]
(single : ∀ (a : α), motive {a})
(insert : ∀ (a : α) (s : Finset α), a ∉ s → motive s → motive (insert a s))
: ∀ s, Finset.Nonempty s → motive s := by
intro S
induction' S using Finset.induction
· simp
· expose_names
intro _
by_cases h : (Finset.Nonempty s)
· apply insert
· assumption
· apply h_1; assumption
· simp at h
rw [h]
apply single
end Finset.Nonempty
|
