case a
F : Type ?u.398044
α : Type u_1
β : Type ?u.398050
γ : Type ?u.398053
ι : Type ?u.398056
κ : Type ?u.398059
inst✝¹ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ (x : α), x ∈ s → x < a) → p s → p (insert a s)
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → p t
⊢ p s
F : Type ?u.398044
α : Type u_1
β : Type ?u.398050
γ : Type ?u.398053
ι : Type ?u.398056
κ : Type ?u.398059
inst✝¹ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
inst✝ : DecidableEq α
p : Finset α → Prop
s : Finset α
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ (x : α), x ∈ s → x < a) → p s → p (insert a s)
⊢ p s
induction' s using Finset.strongInductionOn with s ihs
case a.inl
F : Type ?u.398044
α : Type u_1
β : Type ?u.398050
γ : Type ?u.398053
ι : Type ?u.398056
κ : Type ?u.398059
inst✝¹ : LinearOrder α
s : Finset α
H : Finset.Nonempty s
x : α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ (x : α), x ∈ s → x < a) → p s → p (insert a s)
ihs : ∀ (t : Finset α), t ⊂ ∅ → p t
⊢ p ∅

case a.inr
F : Type ?u.398044
α : Type u_1
β : Type ?u.398050
γ : Type ?u.398053
ι : Type ?u.398056
κ : Type ?u.398059
inst✝¹ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ (x : α), x ∈ s → x < a) → p s → p (insert a s)
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → p t
hne : Finset.Nonempty s
⊢ p s
case a
F : Type ?u.398044
α : Type u_1
β : Type ?u.398050
γ : Type ?u.398053
ι : Type ?u.398056
κ : Type ?u.398059
inst✝¹ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ (x : α), x ∈ s → x < a) → p s → p (insert a s)
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → p t
⊢ p s
rcases s.eq_empty_or_nonempty with (rfl | hne)
no goals
case a.inl
F : Type ?u.398044
α : Type u_1
β : Type ?u.398050
γ : Type ?u.398053
ι : Type ?u.398056
κ : Type ?u.398059
inst✝¹ : LinearOrder α
s : Finset α
H : Finset.Nonempty s
x : α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ (x : α), x ∈ s → x < a) → p s → p (insert a s)
ihs : ∀ (t : Finset α), t ⊂ ∅ → p t
⊢ p ∅
exact h0
case a.inr
F : Type ?u.398044
α : Type u_1
β : Type ?u.398050
γ : Type ?u.398053
ι : Type ?u.398056
κ : Type ?u.398059
inst✝¹ : LinearOrder α
s✝ : Finset α
H✝ : Finset.Nonempty s✝
x : α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ (x : α), x ∈ s → x < a) → p s → p (insert a s)
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → p t
hne : Finset.Nonempty s
H : max' s hne ∈ s
⊢ p s
case a.inr
F : Type ?u.398044
α : Type u_1
β : Type ?u.398050
γ : Type ?u.398053
ι : Type ?u.398056
κ : Type ?u.398059
inst✝¹ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x : α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ (x : α), x ∈ s → x < a) → p s → p (insert a s)
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → p t
hne : Finset.Nonempty s
⊢ p s
have H : s.max' hne ∈ s := max'_mem s hne
case a.inr
F : Type ?u.398044
α : Type u_1
β : Type ?u.398050
γ : Type ?u.398053
ι : Type ?u.398056
κ : Type ?u.398059
inst✝¹ : LinearOrder α
s✝ : Finset α
H✝ : Finset.Nonempty s✝
x : α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ (x : α), x ∈ s → x < a) → p s → p (insert a s)
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → p t
hne : Finset.Nonempty s
H : max' s hne ∈ s
⊢ p (insert (max' s hne) (erase s (max' s hne)))
case a.inr
F : Type ?u.398044
α : Type u_1
β : Type ?u.398050
γ : Type ?u.398053
ι : Type ?u.398056
κ : Type ?u.398059
inst✝¹ : LinearOrder α
s✝ : Finset α
H✝ : Finset.Nonempty s✝
x : α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ (x : α), x ∈ s → x < a) → p s → p (insert a s)
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → p t
hne : Finset.Nonempty s
H : max' s hne ∈ s
⊢ p s
rw [← insert_erase H]
no goals
case a.inr
F : Type ?u.398044
α : Type u_1
β : Type ?u.398050
γ : Type ?u.398053
ι : Type ?u.398056
κ : Type ?u.398059
inst✝¹ : LinearOrder α
s✝ : Finset α
H✝ : Finset.Nonempty s✝
x : α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ (x : α), x ∈ s → x < a) → p s → p (insert a s)
s : Finset α
ihs : ∀ (t : Finset α), t ⊂ s → p t
hne : Finset.Nonempty s
H : max' s hne ∈ s
⊢ p (insert (max' s hne) (erase s (max' s hne)))
exact step _ _ (fun x => s.lt_max'_of_mem_erase_max' hne) (ihs _ <| erase_ssubset H)