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

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

State before:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hvA : v ∈ A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
⊢ degRes G v A ≤ maxDegRes G A
Tactic:
have := mem_image_of_mem (fun v => G.degRes v A) hvA
State after:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hvA : v ∈ A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
this : (fun v => degRes G v A) v ∈ image (fun v => degRes G v A) A
⊢ degRes G v A ≤ maxDegRes G A

State before:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hvA : v ∈ A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
this : (fun v => degRes G v A) v ∈ image (fun v => degRes G v A) A
⊢ degRes G v A ≤ maxDegRes G A
Tactic:
have := Finset.le_max_of_eq this ht
State after:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hvA : v ∈ A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
this✝ : (fun v => degRes G v A) v ∈ image (fun v => degRes G v A) A
this : (fun v => degRes G v A) v ≤ t
⊢ degRes G v A ≤ maxDegRes G A

State before:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hvA : v ∈ A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
this✝ : (fun v => degRes G v A) v ∈ image (fun v => degRes G v A) A
this : (fun v => degRes G v A) v ≤ t
⊢ degRes G v A ≤ maxDegRes G A
Tactic:
rwa [maxDegRes, ht]
State after:
no goals