awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
x : V
⊢ G.incidenceSet x ⊆ Sym2.diagSetᶜ

Tactic:
(incidenceSet_subset G x).trans G.edgeSet_subset_compl_diagSet

Premises used: HasSubset.Subset.trans, SimpleGraph.edgeSet_subset_compl_diagSet, SimpleGraph.incidenceSet_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
x : V
⊢ G.incidenceSet x ⊆ Sym2.diagSetᶜ

Tactic:
exact (incidenceSet_subset G x).trans G.edgeSet_subset_compl_diagSet

Premises used: HasSubset.Subset.trans, SimpleGraph.edgeSet_subset_compl_diagSet, SimpleGraph.incidenceSet_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
x : V
simp_rw : (G.deleteEdges (G.incidenceSet x)).edgeSet = G.edgeSet \ G.incidenceSet x
simp_rw₁ : (G \ fromEdgeSet (G.incidenceSet x)).edgeSet = G.edgeSet \ G.incidenceSet x
simp_rw₂ : G.edgeSet \ (fromEdgeSet (G.incidenceSet x)).edgeSet = G.edgeSet \ G.incidenceSet x
⊢ (G.deleteIncidenceSet x).edgeSet = G.edgeSet \ G.incidenceSet x

Tactic:
simp_rw [deleteIncidenceSet, deleteEdges, edgeSet_sdiff, edgeSet_fromEdgeSet_incidenceSet]

Premises used: SimpleGraph.deleteEdges, SimpleGraph.edgeSet_fromEdgeSet_incidenceSet, SimpleGraph.deleteIncidenceSet, SimpleGraph.edgeSet_sdiff
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
x x_1 : V
simp_rw : (∃ (w : V), G.Adj x_1 w ∧ x_1 ≠ x ∧ w ≠ x) → x_1 ∈ G.support \ {x}
⊢ x_1 ∈ (G.deleteIncidenceSet x).support → x_1 ∈ G.support \ {x}

Tactic:
simp_rw [mem_support, deleteIncidenceSet_adj]

Premises used: SimpleGraph.mem_support, SimpleGraph.deleteIncidenceSet_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
x x_1 : V
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ (w : V), G.Adj x_1 w → x_1 ≠ x → w ≠ x → x_1 ∈ G.support \ {x}
⊢ (∃ (w : V), G.Adj x_1 w ∧ x_1 ≠ x ∧ w ≠ x) → x_1 ∈ G.support \ {x}

Tactic:
tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
x : V
h : x ∉ s
Adj : ∀ (v₁ v₂ : (↑s : Type u_1)), (induce s (G.deleteIncidenceSet x)).Adj v₁ v₂ ↔ (induce s G).Adj v₁ v₂
⊢ induce s (G.deleteIncidenceSet x) = induce s G

Tactic:
ext v₁ v₂
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
x : V
h : x ∉ s
v₁ v₂ : (↑s : Type u_1)
Adj : G.Adj (↑v₁ : V) (↑v₂ : V) → (↑v₁ : V) ≠ x ∧ (↑v₂ : V) ≠ x
⊢ (induce s (G.deleteIncidenceSet x)).Adj v₁ v₂ ↔ (induce s G).Adj v₁ v₂

Tactic:
simp_rw [comap_adj, Function.Embedding.coe_subtype, deleteIncidenceSet_adj, and_iff_left_iff_imp]

Premises used: SimpleGraph.deleteIncidenceSet_adj, Function.Embedding.coe_subtype, SimpleGraph.comap_adj, and_iff_left_iff_imp
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
x : V
h : x ∉ s
v₁ v₂ : (↑s : Type u_1)
⊢ G.Adj (↑v₁ : V) (↑v₂ : V) → (↑v₁ : V) ≠ x ∧ (↑v₂ : V) ≠ x

Tactic:
fun _ ↦ ⟨v₁.prop.ne_of_notMem h, v₂.prop.ne_of_notMem h⟩

Premises used: Membership.mem.ne_of_notMem, Subtype.prop, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
x : V
h : x ∉ s
v₁ v₂ : (↑s : Type u_1)
⊢ G.Adj (↑v₁ : V) (↑v₂ : V) → (↑v₁ : V) ≠ x ∧ (↑v₂ : V) ≠ x

Tactic:
exact fun _ ↦ ⟨v₁.prop.ne_of_notMem h, v₂.prop.ne_of_notMem h⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
⊢ x ∉ {x}ᶜ

Tactic:
have h_notMem : x ∉ ({x}ᶜ : Set V) := Set.notMem_compl_iff.mpr (Set.mem_singleton x)
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
h_notMem : x ∉ {x}ᶜ
simp_rw :
  Finset.card (α := Sym2 (↑{x}ᶜ : Type u_1)) (Set.toFinset (edgeSet (induce {x}ᶜ (G.deleteIncidenceSet x)))) =
    #(G.deleteIncidenceSet x).edgeSet.toFinset
⊢ Finset.card (α := Sym2 (↑{x}ᶜ : Type u_1)) (edgeFinset (induce {x}ᶜ G)) = #(G.deleteIncidenceSet x).edgeFinset

Tactic:
simp_rw [edgeFinset, Set.toFinset_card,
    ← G.induce_deleteIncidenceSet_of_notMem h_notMem, ← Set.toFinset_card]

Premises used: SimpleGraph.induce_deleteIncidenceSet_of_notMem, Set.toFinset_card, SimpleGraph.edgeFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
h_notMem : x ∉ {x}ᶜ
h : (G.deleteIncidenceSet x).support ⊆ {x}ᶜ
⊢ Finset.card (α := Sym2 (↑{x}ᶜ : Type u_1)) (Set.toFinset (edgeSet (induce {x}ᶜ (G.deleteIncidenceSet x)))) =
    #(G.deleteIncidenceSet x).edgeSet.toFinset

Tactic:
apply card_edgeFinset_induce_of_support_subset

Premises used: SimpleGraph.card_edgeFinset_induce_of_support_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
h_notMem : x ∉ {x}ᶜ
trans : (G.deleteIncidenceSet x).support ⊆ G.support \ {x}
trans₁ : G.support \ {x} ⊆ {x}ᶜ
⊢ (G.deleteIncidenceSet x).support ⊆ {x}ᶜ

Tactic:
trans G.support \ {x}

Premises used: SimpleGraph.support
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
h_notMem : x ∉ {x}ᶜ
⊢ (G.deleteIncidenceSet x).support ⊆ G.support \ {x}

Tactic:
support_deleteIncidenceSet_subset G x

Premises used: SimpleGraph.support_deleteIncidenceSet_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
h_notMem : x ∉ {x}ᶜ
⊢ (G.deleteIncidenceSet x).support ⊆ G.support \ {x}

Tactic:
exact support_deleteIncidenceSet_subset G x

Premises used: SimpleGraph.support_deleteIncidenceSet_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
h_notMem : x ∉ {x}ᶜ
rw : G.support \ {x} ⊆ Set.univ \ {x}
⊢ G.support \ {x} ⊆ {x}ᶜ

Tactic:
rw [Set.compl_eq_univ_diff]

Premises used: Set.compl_eq_univ_diff
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
h_notMem : x ∉ {x}ᶜ
⊢ G.support \ {x} ⊆ Set.univ \ {x}

Tactic:
Set.diff_subset_diff_left (Set.subset_univ G.support)

Premises used: Set.subset_univ, Set.diff_subset_diff_left, SimpleGraph.support
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
h_notMem : x ∉ {x}ᶜ
⊢ G.support \ {x} ⊆ Set.univ \ {x}

Tactic:
exact Set.diff_subset_diff_left (Set.subset_univ G.support)

Premises used: Set.subset_univ, Set.diff_subset_diff_left, SimpleGraph.support
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
a : (↑(G.deleteIncidenceSet x).edgeFinset : Set (Sym2 V)) = (↑(G.edgeFinset \ G.incidenceFinset x) : Set (Sym2 V))
⊢ (G.deleteIncidenceSet x).edgeFinset = G.edgeFinset \ G.incidenceFinset x

Tactic:
apply Finset.coe_injective

Premises used: Finset.coe_injective
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
a : (G.deleteIncidenceSet x).edgeSet = G.edgeSet \ G.incidenceSet x
⊢ (↑(G.deleteIncidenceSet x).edgeFinset : Set (Sym2 V)) = (↑(G.edgeFinset \ G.incidenceFinset x) : Set (Sym2 V))

Tactic:
push_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
⊢ (G.deleteIncidenceSet x).edgeSet = G.edgeSet \ G.incidenceSet x

Tactic:
G.edgeSet_deleteIncidenceSet x

Premises used: SimpleGraph.edgeSet_deleteIncidenceSet
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
⊢ (G.deleteIncidenceSet x).edgeSet = G.edgeSet \ G.incidenceSet x

Tactic:
exact G.edgeSet_deleteIncidenceSet x

Premises used: SimpleGraph.edgeSet_deleteIncidenceSet
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
simp_rw : #(G.deleteIncidenceSet x).edgeFinset = #G.edgeFinset - #(G.incidenceFinset x)
simp_rw₁ : #(G.deleteIncidenceSet x).edgeFinset = #(G.edgeFinset \ G.incidenceFinset x)
⊢ #(G.deleteIncidenceSet x).edgeFinset = #G.edgeFinset - G.degree x

Tactic:
simp_rw [← card_incidenceFinset_eq_degree, ← card_sdiff_of_subset (G.incidenceFinset_subset x),
    edgeFinset_deleteIncidenceSet_eq_sdiff]

Premises used: SimpleGraph.edgeFinset_deleteIncidenceSet_eq_sdiff, Finset.card_sdiff_of_subset, SimpleGraph.incidenceFinset_subset, SimpleGraph.card_incidenceFinset_eq_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
rw : {x_1 ∈ G.edgeFinset | x_1 ∉ G.incidenceFinset x} = {x_1 ∈ G.edgeFinset | x ∉ x_1}
⊢ (G.deleteIncidenceSet x).edgeFinset = {x_1 ∈ G.edgeFinset | x ∉ x_1}

Tactic:
rw [edgeFinset_deleteIncidenceSet_eq_sdiff, sdiff_eq_filter]

Premises used: Finset.sdiff_eq_filter, SimpleGraph.edgeFinset_deleteIncidenceSet_eq_sdiff
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
H : ∀ x_1 ∈ G.edgeFinset, x_1 ∉ G.incidenceFinset x ↔ x ∉ x_1
⊢ {x_1 ∈ G.edgeFinset | x_1 ∉ G.incidenceFinset x} = {x_1 ∈ G.edgeFinset | x ∉ x_1}

Tactic:
apply filter_congr

Premises used: Finset.filter_congr
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
x_1 : Sym2 V
h : x_1 ∈ G.edgeFinset
H : x_1 ∈ G.edgeSet ∨ x ∉ x_1
⊢ x_1 ∉ G.incidenceFinset x ↔ x ∉ x_1

Tactic:
rw [incidenceFinset, Set.mem_toFinset, incidenceSet,
    Set.mem_setOf_eq, not_and, Classical.imp_iff_right_iff]

Premises used: SimpleGraph.incidenceSet, Set.mem_setOf_eq, Classical.imp_iff_right_iff, Set.mem_toFinset, SimpleGraph.incidenceFinset, not_and
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
x_1 : Sym2 V
h : x_1 ∈ G.edgeFinset
H : x_1 ∈ G.edgeSet
⊢ x_1 ∈ G.edgeSet ∨ x ∉ x_1

Tactic:
left
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
x_1 : Sym2 V
h : x_1 ∈ G.edgeFinset
H H₁ H₂ H₃ : ∀ (h : x_1 ∈ G.edgeSet), x_1 ∈ G.edgeSet
⊢ x_1 ∈ G.edgeSet

Tactic:
rwa [mem_edgeFinset] at h

Premises used: SimpleGraph.mem_edgeFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
hx : x ∈ G.support
⊢ Set.toFinset {x} ⊆ G.support.toFinset

Tactic:
rw [← Set.singleton_subset_iff, ← Set.toFinset_subset_toFinset] at hx

Premises used: Set.singleton_subset_iff, Set.toFinset_subset_toFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
hx : Set.toFinset {x} ⊆ G.support.toFinset
simp_rw : #(G.deleteIncidenceSet x).support.toFinset ≤ #(G.support \ {x}).toFinset
⊢ Fintype.card.{u_1} (↑(G.deleteIncidenceSet x).support : Type u_1) ≤ Fintype.card.{u_1} (↑G.support : Type u_1) - 1

Tactic:
simp_rw [← Set.card_singleton x, ← Set.toFinset_card, ← card_sdiff_of_subset hx,
    ← Set.toFinset_diff]

Premises used: Set.toFinset_diff, Finset.card_sdiff_of_subset, Set.toFinset_card, Set.card_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
hx : Set.toFinset {x} ⊆ G.support.toFinset
a : (G.deleteIncidenceSet x).support.toFinset ⊆ (G.support \ {x}).toFinset
⊢ #(G.deleteIncidenceSet x).support.toFinset ≤ #(G.support \ {x}).toFinset

Tactic:
apply card_le_card

Premises used: Finset.card_le_card
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
hx : Set.toFinset {x} ⊆ G.support.toFinset
a : (G.deleteIncidenceSet x).support ⊆ G.support \ {x}
⊢ (G.deleteIncidenceSet x).support.toFinset ⊆ (G.support \ {x}).toFinset

Tactic:
rw [Set.toFinset_subset_toFinset]

Premises used: Set.toFinset_subset_toFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
hx : Set.toFinset {x} ⊆ G.support.toFinset
⊢ (G.deleteIncidenceSet x).support ⊆ G.support \ {x}

Tactic:
G.support_deleteIncidenceSet_subset x

Premises used: SimpleGraph.support_deleteIncidenceSet_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
x : V
hx : Set.toFinset {x} ⊆ G.support.toFinset
⊢ (G.deleteIncidenceSet x).support ⊆ G.support \ {x}

Tactic:
exact G.support_deleteIncidenceSet_subset x

Premises used: SimpleGraph.support_deleteIncidenceSet_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype (↑G.edgeSet : Type u_1)
p : SimpleGraph V → Prop
r : 𝕜
inst_3 : Fintype (Sym2 V)
⊢ G.DeleteFar p r ↔
    ∀ ⦃H : SimpleGraph V⦄ [inst_4 : DecidableRel H.Adj],
      H ≤ G → p H → r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)

Tactic:
⟨fun h H _ hHG hH ↦ ?_, fun h s hs hG ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype (↑G.edgeSet : Type u_1)
p : SimpleGraph V → Prop
r : 𝕜
inst_3 : Fintype (Sym2 V)
refine_1 :
  ∀ (h : G.DeleteFar p r) (H : SimpleGraph V) (x : DecidableRel H.Adj) (hHG : H ≤ G) (hH : p H),
    r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)
refine_2 :
  ∀
    (h :
      ∀ ⦃H : SimpleGraph V⦄ [inst_4 : DecidableRel H.Adj],
        H ≤ G → p H → r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜))
    (s : Finset (Sym2 V)) (hs : s ⊆ G.edgeFinset) (hG : p (G.deleteEdges (↑s : Set (Sym2 V)))), r ≤ (↑(#s) : 𝕜)
⊢ G.DeleteFar p r ↔
    ∀ ⦃H : SimpleGraph V⦄ [inst_4 : DecidableRel H.Adj],
      H ≤ G → p H → r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)

Tactic:
refine ⟨fun h H _ hHG hH ↦ ?_, fun h s hs hG ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype (↑G.edgeSet : Type u_1)
p : SimpleGraph V → Prop
r : 𝕜
inst_3 : Fintype (Sym2 V)
h : G.DeleteFar p r
H : SimpleGraph V
x : DecidableRel H.Adj
hHG : H ≤ G
hH : p H
⊢ p (G.deleteEdges (↑(G.edgeFinset \ H.edgeFinset) : Set (Sym2 V))) → r ≤ (↑(#(G.edgeFinset \ H.edgeFinset)) : 𝕜)

Tactic:
have := h (sdiff_subset (t := H.edgeFinset))
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype (↑G.edgeSet : Type u_1)
p : SimpleGraph V → Prop
r : 𝕜
inst_3 : Fintype (Sym2 V)
h : G.DeleteFar p r
H : SimpleGraph V
x : DecidableRel H.Adj
hHG : H ≤ G
hH : p H
this : p (G.deleteEdges (↑(G.edgeFinset \ H.edgeFinset) : Set (Sym2 V))) → r ≤ (↑(#(G.edgeFinset \ H.edgeFinset)) : 𝕜)
⊢ p H → r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)

Tactic:
simp only [deleteEdges_sdiff_eq_of_le hHG, edgeFinset_mono hHG, card_sdiff_of_subset,
      card_le_card, coe_sdiff, coe_edgeFinset, Nat.cast_sub] at this

Premises used: SimpleGraph.edgeFinset_mono, Nat.cast_sub, SimpleGraph.coe_edgeFinset, Finset.card_le_card, Finset.card_sdiff_of_subset, Finset.coe_sdiff, SimpleGraph.deleteEdges_sdiff_eq_of_le
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype (↑G.edgeSet : Type u_1)
p : SimpleGraph V → Prop
r : 𝕜
inst_3 : Fintype (Sym2 V)
h : G.DeleteFar p r
H : SimpleGraph V
x : DecidableRel H.Adj
hHG : H ≤ G
hH : p H
this : p H → r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)
⊢ r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)

Tactic:
this hH
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype (↑G.edgeSet : Type u_1)
p : SimpleGraph V → Prop
r : 𝕜
inst_3 : Fintype (Sym2 V)
h : G.DeleteFar p r
H : SimpleGraph V
x : DecidableRel H.Adj
hHG : H ≤ G
hH : p H
this : p H → r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)
⊢ r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)

Tactic:
exact this hH
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype (↑G.edgeSet : Type u_1)
p : SimpleGraph V → Prop
r : 𝕜
inst_3 : Fintype (Sym2 V)
h :
  ∀ ⦃H : SimpleGraph V⦄ [inst_4 : DecidableRel H.Adj],
    H ≤ G → p H → r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)
s : Finset (Sym2 V)
hs : s ⊆ G.edgeFinset
hG : p (G.deleteEdges (↑s : Set (Sym2 V)))
⊢ r ≤ (↑(#s) : 𝕜)

Tactic:
simpa [card_sdiff_of_subset hs, edgeFinset_deleteEdges, -Set.toFinset_card, Nat.cast_sub,
      card_le_card hs] using h (G.deleteEdges_le s) hG

Premises used: Nat.cast_sub, Finset.card_le_card, Finset.card_sdiff_of_subset, Set.toFinset_card, SetLike.coe, SimpleGraph.edgeFinset_deleteEdges, SimpleGraph.deleteEdges_le
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype (↑G.edgeSet : Type u_1)
p : SimpleGraph V → Prop
r : 𝕜
inst_3 : Fintype (Sym2 V)
h :
  ∀ ⦃H : SimpleGraph V⦄ [inst_4 : DecidableRel H.Adj],
    H ≤ G → p H → r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)
s : Finset (Sym2 V)
hs : s ⊆ G.edgeFinset
hG : p (G.deleteEdges (↑s : Set (Sym2 V)))
⊢ r ≤ (↑(#s) : 𝕜)

Tactic:
classical
    simpa [card_sdiff_of_subset hs, edgeFinset_deleteEdges, -Set.toFinset_card, Nat.cast_sub,
      card_le_card hs] using h (G.deleteEdges_le s) hG

Premises used: Nat.cast_sub, Finset.card_le_card, Finset.card_sdiff_of_subset, Set.toFinset_card, SetLike.coe, SimpleGraph.edgeFinset_deleteEdges, SimpleGraph.deleteEdges_le
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype (↑G.edgeSet : Type u_1)
p : SimpleGraph V → Prop
r : 𝕜
inst_3 : Fintype (Sym2 V)
refine_1 :
  ∀ (h : G.DeleteFar p r) (H : SimpleGraph V) (x : DecidableRel H.Adj) (hHG : H ≤ G) (hH : p H),
    r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)
refine_2 refine_2₁ :
  ∀
    (h :
      ∀ ⦃H : SimpleGraph V⦄ [inst_4 : DecidableRel H.Adj],
        H ≤ G → p H → r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜))
    (s : Finset (Sym2 V)) (hs : s ⊆ G.edgeFinset) (hG : p (G.deleteEdges (↑s : Set (Sym2 V)))), r ≤ (↑(#s) : 𝕜)
⊢ G.DeleteFar p r ↔
    ∀ ⦃H : SimpleGraph V⦄ [inst_4 : DecidableRel H.Adj],
      H ≤ G → p H → r ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)

Tactic:
classical
  refine ⟨fun h H _ hHG hH ↦ ?_, fun h s hs hG ↦ ?_⟩
  · have := h (sdiff_subset (t := H.edgeFinset))
    simp only [deleteEdges_sdiff_eq_of_le hHG, edgeFinset_mono hHG, card_sdiff_of_subset,
      card_le_card, coe_sdiff, coe_edgeFinset, Nat.cast_sub] at this
    exact this hH
  · classical
    simpa [card_sdiff_of_subset hs, edgeFinset_deleteEdges, -Set.toFinset_card, Nat.cast_sub,
      card_le_card hs] using h (G.deleteEdges_le s) hG

Premises used: Nat.cast_sub, SimpleGraph.coe_edgeFinset, Finset.card_le_card, Finset.card_sdiff_of_subset, Finset.coe_sdiff, Set.toFinset_card, SimpleGraph.edgeFinset_deleteEdges
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype (↑G.edgeSet : Type u_1)
p : SimpleGraph V → Prop
r₁ r₂ : 𝕜
h : G.DeleteFar p r₂
hr : r₁ ≤ r₂
⊢ G.DeleteFar p r₁

Tactic:
fun _ hs hG =>
  hr.trans <| h hs hG

Premises used: SimpleGraph.DeleteFar, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype (↑G.edgeSet : Type u_1)
p : SimpleGraph V → Prop
r : 𝕜
h : G.DeleteFar p r
hp : p ⊥
⊢ p (G.deleteEdges (↑G.edgeFinset : Set (Sym2 V)))

Tactic:
simpa
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
x : α × β
rw : x ∈ {e ∈ s ×ˢ t | r e.1 e.2} ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2
rw₁ : x ∈ s ×ˢ t ∧ r x.1 x.2 ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2
rw₂ : (x.1 ∈ s ∧ x.2 ∈ t) ∧ r x.1 x.2 ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2
rw₃ rw₄ : x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2 ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2
⊢ x ∈ interedges r s t ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2

Tactic:
rw [interedges, mem_filter, Finset.mem_product, and_assoc]

Premises used: Rel.interedges, and_assoc, Finset.mem_filter, Finset.mem_product
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
a : α
b : β
⊢ (a, b) ∈ interedges r s t ↔ a ∈ s ∧ b ∈ t ∧ r a b

Tactic:
mem_interedges_iff

Premises used: Set.Mem, setOf, Rel.mem_interedges_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
t : Finset β
rw : {e ∈ SProd.sprod (α := Finset α) ∅ t | r e.1 e.2} = ∅
rw₁ : Eq (α := Finset (α × β)) ({e ∈ ∅ | r e.1 e.2}) ∅
rw₂ rw₃ : Eq (α := Finset (α × β)) ∅ ∅
⊢ interedges r ∅ t = ∅

Tactic:
rw [interedges, Finset.empty_product, filter_empty]

Premises used: Finset.empty_product, Rel.interedges, Finset.filter_empty
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
x : α × β
simp_rw : x.1 ∈ s₂ ∧ x.2 ∈ t₂ ∧ r x.1 x.2 → x.1 ∈ s₁ ∧ x.2 ∈ t₁ ∧ r x.1 x.2
⊢ x ∈ interedges r s₂ t₂ → x ∈ interedges r s₁ t₁

Tactic:
simp_rw [mem_interedges_iff]

Premises used: Rel.mem_interedges_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
x : α × β
⊢ x.1 ∈ s₂ ∧ x.2 ∈ t₂ ∧ r x.1 x.2 → x.1 ∈ s₁ ∧ x.2 ∈ t₁ ∧ r x.1 x.2

Tactic:
fun h ↦ ⟨hs h.1, ht h.2.1, h.2.2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Density
Goal:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
x : α × β
⊢ x.1 ∈ s₂ ∧ x.2 ∈ t₂ ∧ r x.1 x.2 → x.1 ∈ s₁ ∧ x.2 ∈ t₁ ∧ r x.1 x.2

Tactic:
exact fun h ↦ ⟨hs h.1, ht h.2.1, h.2.2⟩