case empty
F : Type ?u.314698
α : Type u_1
β : Type ?u.314704
γ : Type ?u.314707
ι : Type ?u.314710
κ : Type ?u.314713
inst✝ : LinearOrder α
⊢ ∀ {a : α}, Finset.max ∅ = ↑a → a ∈ ∅

case insert
F : Type ?u.314698
α : Type u_1
β : Type ?u.314704
γ : Type ?u.314707
ι : Type ?u.314710
κ : Type ?u.314713
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
⊢ ∀ {a : α}, Finset.max (insert b s) = ↑a → a ∈ insert b s
F : Type ?u.314698
α : Type u_1
β : Type ?u.314704
γ : Type ?u.314707
ι : Type ?u.314710
κ : Type ?u.314713
inst✝ : LinearOrder α
s : Finset α
⊢ ∀ {a : α}, Finset.max s = ↑a → a ∈ s
induction' s using Finset.induction_on with b s _ ih
case empty
F : Type ?u.314698
α : Type u_1
β : Type ?u.314704
γ : Type ?u.314707
ι : Type ?u.314710
κ : Type ?u.314713
inst✝ : LinearOrder α
a✝ : α
H : Finset.max ∅ = ↑a✝
⊢ a✝ ∈ ∅
case empty
F : Type ?u.314698
α : Type u_1
β : Type ?u.314704
γ : Type ?u.314707
ι : Type ?u.314710
κ : Type ?u.314713
inst✝ : LinearOrder α
⊢ ∀ {a : α}, Finset.max ∅ = ↑a → a ∈ ∅
intro _ H
no goals
case empty
F : Type ?u.314698
α : Type u_1
β : Type ?u.314704
γ : Type ?u.314707
ι : Type ?u.314710
κ : Type ?u.314713
inst✝ : LinearOrder α
a✝ : α
H : Finset.max ∅ = ↑a✝
⊢ a✝ ∈ ∅
cases H
case insert
F : Type ?u.314698
α : Type u_1
β : Type ?u.314704
γ : Type ?u.314707
ι : Type ?u.314710
κ : Type ?u.314713
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
a : α
h : Finset.max (insert b s) = ↑a
⊢ a ∈ insert b s
case insert
F : Type ?u.314698
α : Type u_1
β : Type ?u.314704
γ : Type ?u.314707
ι : Type ?u.314710
κ : Type ?u.314713
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
⊢ ∀ {a : α}, Finset.max (insert b s) = ↑a → a ∈ insert b s
intro a h
case pos
F : Type ?u.314698
α : Type u_1
β : Type ?u.314704
γ : Type ?u.314707
ι : Type ?u.314710
κ : Type ?u.314713
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
a : α
h : Finset.max (insert b s) = ↑a
p : b = a
⊢ a ∈ insert b s

case neg
F : Type ?u.314698
α : Type u_1
β : Type ?u.314704
γ : Type ?u.314707
ι : Type ?u.314710
κ : Type ?u.314713
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
a : α
h : Finset.max (insert b s) = ↑a
p : ¬b = a
⊢ a ∈ insert b s
case insert
F : Type ?u.314698
α : Type u_1
β : Type ?u.314704
γ : Type ?u.314707
ι : Type ?u.314710
κ : Type ?u.314713
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
a : α
h : Finset.max (insert b s) = ↑a
⊢ a ∈ insert b s
by_cases p : b = a
case pos.refl
F : Type ?u.314698
α : Type u_1
β : Type ?u.314704
γ : Type ?u.314707
ι : Type ?u.314710
κ : Type ?u.314713
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
a : α
h : Finset.max (insert b s) = ↑b
⊢ b ∈ insert b s
case pos
F : Type ?u.314698
α : Type u_1
β : Type ?u.314704
γ : Type ?u.314707
ι : Type ?u.314710
κ : Type ?u.314713
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
a : α
h : Finset.max (insert b s) = ↑a
p : b = a
⊢ a ∈ insert b s
induction p
no goals
case pos.refl
F : Type ?u.314698
α : Type u_1
β : Type ?u.314704
γ : Type ?u.314707
ι : Type ?u.314710
κ : Type ?u.314713
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
a : α
h : Finset.max (insert b s) = ↑b
⊢ b ∈ insert b s
exact mem_insert_self b s
case neg.inl
F : Type ?u.314698
α : Type u_1
β : Type ?u.314704
γ : Type ?u.314707
ι : Type ?u.314710
κ : Type ?u.314713
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
a : α
h : ↑b = ↑a
p : ¬b = a
q : max (↑b) (Finset.max s) = ↑b
⊢ a ∈ insert b s

case neg.inr
F : Type ?u.314698
α : Type u_1
β : Type ?u.314704
γ : Type ?u.314707
ι : Type ?u.314710
κ : Type ?u.314713
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
a : α
h : Finset.max s = ↑a
p : ¬b = a
q : max (↑b) (Finset.max s) = Finset.max s
⊢ a ∈ insert b s
case neg
F : Type ?u.314698
α : Type u_1
β : Type ?u.314704
γ : Type ?u.314707
ι : Type ?u.314710
κ : Type ?u.314713
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
a : α
h : Finset.max (insert b s) = ↑a
p : ¬b = a
⊢ a ∈ insert b s
cases' max_choice (↑b) s.max with q q <;> rw [max_insert, q] at h
case neg.inl.refl
F : Type ?u.314698
α : Type u_1
β : Type ?u.314704
γ : Type ?u.314707
ι : Type ?u.314710
κ : Type ?u.314713
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
q : max (↑b) (Finset.max s) = ↑b
p : ¬b = b
⊢ b ∈ insert b s
case neg.inl
F : Type ?u.314698
α : Type u_1
β : Type ?u.314704
γ : Type ?u.314707
ι : Type ?u.314710
κ : Type ?u.314713
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
a : α
h : ↑b = ↑a
p : ¬b = a
q : max (↑b) (Finset.max s) = ↑b
⊢ a ∈ insert b s
cases h
no goals
case neg.inl.refl
F : Type ?u.314698
α : Type u_1
β : Type ?u.314704
γ : Type ?u.314707
ι : Type ?u.314710
κ : Type ?u.314713
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
q : max (↑b) (Finset.max s) = ↑b
p : ¬b = b
⊢ b ∈ insert b s
cases p rfl
no goals
case neg.inr
F : Type ?u.314698
α : Type u_1
β : Type ?u.314704
γ : Type ?u.314707
ι : Type ?u.314710
κ : Type ?u.314713
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : ¬b ∈ s
ih : ∀ {a : α}, Finset.max s = ↑a → a ∈ s
a : α
h : Finset.max s = ↑a
p : ¬b = a
q : max (↑b) (Finset.max s) = Finset.max s
⊢ a ∈ insert b s
exact mem_insert_of_mem (ih h)