case a
F : Type ?u.399951
α : Type u_2
β : Type ?u.399957
γ : Type ?u.399960
ι : Type u_1
κ : Type ?u.399966
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
⊢ p s
F : Type ?u.399951
α : Type u_2
β : Type ?u.399957
γ : Type ?u.399960
ι : Type u_1
κ : Type ?u.399966
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
s : Finset ι
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
⊢ p s
induction' s using Finset.strongInductionOn with s ihs
case a.inl
F : Type ?u.399951
α : Type u_2
β : Type ?u.399957
γ : Type ?u.399960
ι : Type u_1
κ : Type ?u.399966
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : image f s = ∅
⊢ p s

case a.inr
F : Type ?u.399951
α : Type u_2
β : Type ?u.399957
γ : Type ?u.399960
ι : Type u_1
κ : Type ?u.399966
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : Finset.Nonempty (image f s)
⊢ p s
case a
F : Type ?u.399951
α : Type u_2
β : Type ?u.399957
γ : Type ?u.399960
ι : Type u_1
κ : Type ?u.399966
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
⊢ p s
rcases(s.image f).eq_empty_or_nonempty with (hne | hne)
case a.inl
F : Type ?u.399951
α : Type u_2
β : Type ?u.399957
γ : Type ?u.399960
ι : Type u_1
κ : Type ?u.399966
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : s = ∅
⊢ p s
case a.inl
F : Type ?u.399951
α : Type u_2
β : Type ?u.399957
γ : Type ?u.399960
ι : Type u_1
κ : Type ?u.399966
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : image f s = ∅
⊢ p s
simp only [image_eq_empty] at hne
no goals
case a.inl
F : Type ?u.399951
α : Type u_2
β : Type ?u.399957
γ : Type ?u.399960
ι : Type u_1
κ : Type ?u.399966
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : s = ∅
⊢ p s
simp only [hne, h0]
case a.inr
F : Type ?u.399951
α : Type u_2
β : Type ?u.399957
γ : Type ?u.399960
ι : Type u_1
κ : Type ?u.399966
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : Finset.Nonempty (image f s)
H : max' (image f s) hne ∈ image f s
⊢ p s
case a.inr
F : Type ?u.399951
α : Type u_2
β : Type ?u.399957
γ : Type ?u.399960
ι : Type u_1
κ : Type ?u.399966
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : Finset.Nonempty (image f s)
⊢ p s
have H : (s.image f).max' hne ∈ s.image f := max'_mem (s.image f) hne
case a.inr
F : Type ?u.399951
α : Type u_2
β : Type ?u.399957
γ : Type ?u.399960
ι : Type u_1
κ : Type ?u.399966
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : Finset.Nonempty (image f s)
H : ∃ a, a ∈ s ∧ f a = max' (image f s) hne
⊢ p s
case a.inr
F : Type ?u.399951
α : Type u_2
β : Type ?u.399957
γ : Type ?u.399960
ι : Type u_1
κ : Type ?u.399966
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : Finset.Nonempty (image f s)
H : max' (image f s) hne ∈ image f s
⊢ p s
simp only [mem_image, exists_prop] at H
case a.inr.intro.intro
F : Type ?u.399951
α : Type u_2
β : Type ?u.399957
γ : Type ?u.399960
ι : Type u_1
κ : Type ?u.399966
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : Finset.Nonempty (image f s)
a : ι
has : a ∈ s
hfa : f a = max' (image f s) hne
⊢ p s
case a.inr
F : Type ?u.399951
α : Type u_2
β : Type ?u.399957
γ : Type ?u.399960
ι : Type u_1
κ : Type ?u.399966
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : Finset.Nonempty (image f s)
H : ∃ a, a ∈ s ∧ f a = max' (image f s) hne
⊢ p s
rcases H with ⟨a, has, hfa⟩
case a.inr.intro.intro
F : Type ?u.399951
α : Type u_2
β : Type ?u.399957
γ : Type ?u.399960
ι : Type u_1
κ : Type ?u.399966
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : Finset.Nonempty (image f s)
a : ι
has : a ∈ s
hfa : f a = max' (image f s) hne
⊢ p (insert a (erase s a))
case a.inr.intro.intro
F : Type ?u.399951
α : Type u_2
β : Type ?u.399957
γ : Type ?u.399960
ι : Type u_1
κ : Type ?u.399966
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : Finset.Nonempty (image f s)
a : ι
has : a ∈ s
hfa : f a = max' (image f s) hne
⊢ p s
rw [← insert_erase has]
case a.inr.intro.intro
F : Type ?u.399951
α : Type u_2
β : Type ?u.399957
γ : Type ?u.399960
ι : Type u_1
κ : Type ?u.399966
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : Finset.Nonempty (image f s)
a : ι
has : a ∈ s
hfa : f a = max' (image f s) hne
x : ι
hx : x ∈ erase s a
⊢ f x ≤ f a
case a.inr.intro.intro
F : Type ?u.399951
α : Type u_2
β : Type ?u.399957
γ : Type ?u.399960
ι : Type u_1
κ : Type ?u.399966
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : Finset.Nonempty (image f s)
a : ι
has : a ∈ s
hfa : f a = max' (image f s) hne
⊢ p (insert a (erase s a))
refine' step _ _ (not_mem_erase a s) (fun x hx => _) (ihs _ <| erase_ssubset has)
case a.inr.intro.intro
F : Type ?u.399951
α : Type u_2
β : Type ?u.399957
γ : Type ?u.399960
ι : Type u_1
κ : Type ?u.399966
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : Finset.Nonempty (image f s)
a : ι
has : a ∈ s
hfa : f a = max' (image f s) hne
x : ι
hx : x ∈ erase s a
⊢ f x ≤ max' (image f s) hne
case a.inr.intro.intro
F : Type ?u.399951
α : Type u_2
β : Type ?u.399957
γ : Type ?u.399960
ι : Type u_1
κ : Type ?u.399966
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : Finset.Nonempty (image f s)
a : ι
has : a ∈ s
hfa : f a = max' (image f s) hne
x : ι
hx : x ∈ erase s a
⊢ f x ≤ f a
rw [hfa]
no goals
case a.inr.intro.intro
F : Type ?u.399951
α : Type u_2
β : Type ?u.399957
γ : Type ?u.399960
ι : Type u_1
κ : Type ?u.399966
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : DecidableEq ι
f : ι → α
p : Finset ι → Prop
h0 : p ∅
step : ∀ (a : ι) (s : Finset ι), ¬a ∈ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (insert a s)
s : Finset ι
ihs : ∀ (t : Finset ι), t ⊂ s → p t
hne : Finset.Nonempty (image f s)
a : ι
has : a ∈ s
hfa : f a = max' (image f s) hne
x : ι
hx : x ∈ erase s a
⊢ f x ≤ max' (image f s) hne
exact le_max' _ _ (mem_image_of_mem _ <| mem_of_mem_erase hx)