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

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

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

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
i : α
a✝ : i ∈ C
⊢ degRes G i B ≤ degRes G i A
Tactic:
rw [degRes, degRes]
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
i : α
a✝ : i ∈ C
⊢ card (nbhdRes G i B) ≤ card (nbhdRes G i A)

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
i : α
a✝ : i ∈ C
⊢ card (nbhdRes G i B) ≤ card (nbhdRes G i A)
Tactic:
apply card_le_of_subset _
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
i : α
a✝ : i ∈ C
⊢ nbhdRes G i B ⊆ nbhdRes G i A

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
i : α
a✝ : i ∈ C
⊢ nbhdRes G i B ⊆ nbhdRes G i A
Tactic:
intro x hx
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
i : α
a✝ : i ∈ C
x : α
hx : x ∈ nbhdRes G i B
⊢ x ∈ nbhdRes G i A

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
i : α
a✝ : i ∈ C
x : α
hx : x ∈ nbhdRes G i B
⊢ x ∈ nbhdRes G i A
Tactic:
rw [mem_res_nbhd_iff] at *
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
i : α
a✝ : i ∈ C
x : α
hx : x ∈ B ∧ x ∈ neighborFinset G i
⊢ x ∈ A ∧ x ∈ neighborFinset G i

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
i : α
a✝ : i ∈ C
x : α
hx : x ∈ B ∧ x ∈ neighborFinset G i
⊢ x ∈ A ∧ x ∈ neighborFinset G i
Tactic:
exact ⟨hB hx.1, hx.2⟩
State after:
no goals