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

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
C A : Finset α
hC : C ⊆ A
⊢ ∑ v in C, degRes G v A ≤ maxDegRes G A * card C
Tactic:
rw [card_eq_sum_ones, mul_sum, mul_one]
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
C A : Finset α
hC : C ⊆ A
⊢ ∑ v in C, degRes G v A ≤ ∑ x in C, maxDegRes G A

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
C A : Finset α
hC : C ⊆ A
⊢ ∑ v in C, degRes G v A ≤ ∑ x in C, maxDegRes G A
Tactic:
apply sum_le_sum _
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
C A : Finset α
hC : C ⊆ A
⊢ ∀ (i : α), i ∈ C → degRes G i A ≤ maxDegRes G A

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
C A : Finset α
hC : C ⊆ A
⊢ ∀ (i : α), i ∈ C → degRes G i A ≤ maxDegRes G A
Tactic:
intro i hi
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
C A : Finset α
hC : C ⊆ A
i : α
hi : i ∈ C
⊢ degRes G i A ≤ maxDegRes G A

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
C A : Finset α
hC : C ⊆ A
i : α
hi : i ∈ C
⊢ degRes G i A ≤ maxDegRes G A
Tactic:
exact G.degRes_le_maxDegRes (hC hi)
State after:
no goals