Theorem: SimpleGraph.exists_max_res_deg_vertex (Turan4/NbhdRes.lean)

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : Finset.Nonempty A
⊢ ∃ v, v ∈ A ∧ maxDegRes G A = degRes G v A
Tactic:
obtain ⟨t, ht⟩ := max_of_nonempty (Nonempty.image hA (fun v => G.degRes v A))
State after:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : Finset.Nonempty A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
⊢ ∃ v, v ∈ A ∧ maxDegRes G A = degRes G v A

State before:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : Finset.Nonempty A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
⊢ ∃ v, v ∈ A ∧ maxDegRes G A = degRes G v A
Tactic:
obtain ⟨a, ha1, ha2⟩:=mem_image.1 (mem_of_max ht)
State after:
case intro.intro.intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : Finset.Nonempty A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
a : α
ha1 : a ∈ A
ha2 : degRes G a A = t
⊢ ∃ v, v ∈ A ∧ maxDegRes G A = degRes G v A

State before:
case intro.intro.intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : Finset.Nonempty A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
a : α
ha1 : a ∈ A
ha2 : degRes G a A = t
⊢ ∃ v, v ∈ A ∧ maxDegRes G A = degRes G v A
Tactic:
refine ⟨a, ha1,?_⟩
State after:
case intro.intro.intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : Finset.Nonempty A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
a : α
ha1 : a ∈ A
ha2 : degRes G a A = t
⊢ maxDegRes G A = degRes G a A

State before:
case intro.intro.intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : Finset.Nonempty A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
a : α
ha1 : a ∈ A
ha2 : degRes G a A = t
⊢ maxDegRes G A = degRes G a A
Tactic:
rw [maxDegRes,ht,ha2]
State after:
case intro.intro.intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : Finset.Nonempty A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
a : α
ha1 : a ∈ A
ha2 : degRes G a A = t
⊢ Option.getD (↑t) 0 = t

State before:
case intro.intro.intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : Finset.Nonempty A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
a : α
ha1 : a ∈ A
ha2 : degRes G a A = t
⊢ Option.getD (↑t) 0 = t
Tactic:
rfl
State after:
no goals