-- Mathlib/Data/Finset/Max.lean
theorem mem_of_max {s : Finset α} : ∀ {a : α}, s.max = a → a ∈ s

Proof state:
case insert
α : Type u_2
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : b ∉ s
ih : ∀ {a : α}, s.max = ↑a → a ∈ s
⊢ ∀ {a : α}, (insert b s).max = ↑a → a ∈ insert b s

Tactic:
intro a h

Result:
case insert
α : Type u_2
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : b ∉ s
ih : ∀ {a : α}, s.max = ↑a → a ∈ s
a : α
h : (insert b s).max = ↑a
⊢ a ∈ insert b s

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ ∀ {a : α}, s.max = ↑a → a ∈ s

Tactic:
induction' s using Finset.induction_on with b s _ ih

Result:
case empty
α : Type u_2
inst✝ : LinearOrder α
⊢ ∀ {a : α}, ∅.max = ↑a → a ∈ ∅

case insert
α : Type u_2
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : b ∉ s
ih : ∀ {a : α}, s.max = ↑a → a ∈ s
⊢ ∀ {a : α}, (insert b s).max = ↑a → a ∈ insert b s

Proof state:
case empty
α : Type u_2
inst✝ : LinearOrder α
a✝ : α
H : ∅.max = ↑a✝
⊢ a✝ ∈ ∅

Tactic:
cases H

Result:
no goals

Proof state:
case insert
α : Type u_2
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : b ∉ s
ih : ∀ {a : α}, s.max = ↑a → a ∈ s
a : α
h : (insert b s).max = ↑a
⊢ a ∈ insert b s

Tactic:
by_cases p : b = a

Result:
case pos
α : Type u_2
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : b ∉ s
ih : ∀ {a : α}, s.max = ↑a → a ∈ s
a : α
h : (insert b s).max = ↑a
p : b = a
⊢ a ∈ insert b s

case neg
α : Type u_2
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : b ∉ s
ih : ∀ {a : α}, s.max = ↑a → a ∈ s
a : α
h : (insert b s).max = ↑a
p : ¬b = a
⊢ a ∈ insert b s

Proof state:
case empty
α : Type u_2
inst✝ : LinearOrder α
⊢ ∀ {a : α}, ∅.max = ↑a → a ∈ ∅

Tactic:
intro _ H

Result:
case empty
α : Type u_2
inst✝ : LinearOrder α
a✝ : α
H : ∅.max = ↑a✝
⊢ a✝ ∈ ∅

Proof state:
case neg.inl.refl
α : Type u_2
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : b ∉ s
ih : ∀ {a : α}, s.max = ↑a → a ∈ s
q : ↑b ⊔ s.max = ↑b
p : ¬b = b
⊢ b ∈ insert b s

Tactic:
cases p rfl

Result:
no goals

Proof state:
case neg
α : Type u_2
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : b ∉ s
ih : ∀ {a : α}, s.max = ↑a → a ∈ s
a : α
h : (insert b s).max = ↑a
p : ¬b = a
⊢ a ∈ insert b s

Tactic:
rcases max_choice (↑b) s.max with q | q <;> rw [max_insert, q] at h

Result:
case neg.inl
α : Type u_2
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : b ∉ s
ih : ∀ {a : α}, s.max = ↑a → a ∈ s
a : α
h : ↑b = ↑a
p : ¬b = a
q : ↑b ⊔ s.max = ↑b
⊢ a ∈ insert b s

case neg.inr
α : Type u_2
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : b ∉ s
ih : ∀ {a : α}, s.max = ↑a → a ∈ s
a : α
h : s.max = ↑a
p : ¬b = a
q : ↑b ⊔ s.max = s.max
⊢ a ∈ insert b s

Proof state:
case pos.refl
α : Type u_2
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : b ∉ s
ih : ∀ {a : α}, s.max = ↑a → a ∈ s
a : α
h : (insert b s).max = ↑b
⊢ b ∈ insert b s

Tactic:
exact mem_insert_self b s

Result:
no goals

Proof state:
case neg.inr
α : Type u_2
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : b ∉ s
ih : ∀ {a : α}, s.max = ↑a → a ∈ s
a : α
h : s.max = ↑a
p : ¬b = a
q : ↑b ⊔ s.max = s.max
⊢ a ∈ insert b s

Tactic:
exact mem_insert_of_mem (ih h)

Result:
no goals

Proof state:
case pos
α : Type u_2
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : b ∉ s
ih : ∀ {a : α}, s.max = ↑a → a ∈ s
a : α
h : (insert b s).max = ↑a
p : b = a
⊢ a ∈ insert b s

Tactic:
induction p

Result:
case pos.refl
α : Type u_2
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : b ∉ s
ih : ∀ {a : α}, s.max = ↑a → a ∈ s
a : α
h : (insert b s).max = ↑b
⊢ b ∈ insert b s

Proof state:
case neg.inl
α : Type u_2
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : b ∉ s
ih : ∀ {a : α}, s.max = ↑a → a ∈ s
a : α
h : ↑b = ↑a
p : ¬b = a
q : ↑b ⊔ s.max = ↑b
⊢ a ∈ insert b s

Tactic:
cases h

Result:
case neg.inl.refl
α : Type u_2
inst✝ : LinearOrder α
b : α
s : Finset α
a✝ : b ∉ s
ih : ∀ {a : α}, s.max = ↑a → a ∈ s
q : ↑b ⊔ s.max = ↑b
p : ¬b = b
⊢ b ∈ insert b s