awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x u v : α
e : β
edgeSet : Set β
simp : e ∈ edgeSet → (x = u ∧ x = v ∨ x = v ∧ x = u ↔ x = u ∧ u = v)
⊢ (banana u v edgeSet).IsLoopAt e x ↔ e ∈ edgeSet ∧ x = u ∧ u = v

Tactic:
simp only [← isLink_self_iff, banana_isLink, and_congr_right_iff]

Premises used: Graph.banana_isLink, and_congr_right_iff, Graph.isLink_self_iff
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x u v : α
e : β
edgeSet : Set β
⊢ e ∈ edgeSet → (x = u ∧ x = v ∨ x = v ∧ x = u ↔ x = u ∧ u = v)

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y u v : α
edgeSet : Set β
simp : x = u ∧ y = v ∨ x = v ∧ y = u → ((∃ (x : β), x ∈ edgeSet) ↔ edgeSet.Nonempty)
⊢ (banana u v edgeSet).Adj x y ↔ edgeSet.Nonempty ∧ s(x, y) = s(u, v)

Tactic:
simp only [Adj, banana_isLink, exists_and_right, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq,
    Prod.swap_prod_mk, and_congr_left_iff]

Premises used: Sym2.eq, Graph.banana_isLink, Graph.Adj, Prod.swap_prod_mk, exists_and_right, Sym2.rel_iff', Prod.mk.injEq, and_congr_left_iff
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y u v : α
edgeSet : Set β
⊢ x = u ∧ y = v ∨ x = v ∧ y = u → ((∃ (x : β), x ∈ edgeSet) ↔ edgeSet.Nonempty)

Tactic:
fun _ ↦ Iff.rfl

Premises used: Iff.rfl, Set.Nonempty
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y u v : α
edgeSet : Set β
⊢ x = u ∧ y = v ∨ x = v ∧ y = u → ((∃ (x : β), x ∈ edgeSet) ↔ edgeSet.Nonempty)

Tactic:
exact fun _ ↦ Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
u v : α
hV : ∀ (x : α), x ∈ vertexSet.{u_1, u_2} (β := β) (banana u v ∅) ↔ Membership.mem (γ := Set α) V(noEdge {u, v} β) x
h : ∀ (e : β) (x y : α), IsLink (banana u v ∅) e x y ↔ IsLink (noEdge {u, v} β) e x y
⊢ banana u v ∅ = noEdge {u, v} β

Tactic:
ext
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
u v x : α
⊢ x ∈ vertexSet.{u_1, u_2} (β := β) (banana u v ∅) ↔ Membership.mem (γ := Set α) V(noEdge {u, v} β) x

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
u v : α
e : β
x y : α
⊢ IsLink (banana u v ∅) e x y ↔ IsLink (noEdge {u, v} β) e x y

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
v : α
edgeSet : Set β
⊢ V(bouquet v edgeSet) = {v}

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
v : α
edgeSet : Set β
⊢ (bouquet v edgeSet).IsLink e x y ↔ e ∈ edgeSet ∧ x = v ∧ y = v

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
v : α
edgeSet : Set β
⊢ (bouquet v edgeSet).Inc e x ↔ e ∈ edgeSet ∧ x = v

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y v : α
edgeSet : Set β
⊢ (bouquet v edgeSet).Adj x y ↔ edgeSet.Nonempty ∧ x = v ∧ y = v

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
v : α
edgeSet : Set β
⊢ (bouquet v edgeSet).IsLoopAt e x ↔ e ∈ edgeSet ∧ x = v

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x v : α
e : β
edgeSet : Set β
⊢ ¬(bouquet v edgeSet).IsNonloopAt e x

Tactic:
simp +contextual [IsNonloopAt, eq_comm]

Premises used: eq_comm, Graph.IsNonloopAt
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
⊢ V(G) = {v}

Tactic:
have hrw := hss.eq_singleton_of_mem hv
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
hrw : V(G) = {v}
⊢ V(G) = V(bouquet v E(G))

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
hrw : V(G) = {v}
refine_1 : ∀ (e : β) (x : α) (h : G.Inc e x), (bouquet v E(G)).Inc e x
refine_2 : ∀ (e : β) (x : α) (h : (bouquet v E(G)).Inc e x), G.Inc e x
⊢ G = bouquet v E(G)

Tactic:
refine Graph.ext_inc (by simpa) fun e x ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Graph.ext_inc, Iff.intro
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
hrw : V(G) = {v}
e : β
x : α
h : G.Inc e x
⊢ (bouquet v E(G)).Inc e x

Tactic:
simp [← mem_singleton_iff, ← hrw, h.edge_mem, h.vertex_mem]

Premises used: Set.mem_singleton_iff, Graph.Inc.vertex_mem, Graph.Inc.edge_mem
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
hrw : V(G) = {v}
e : β
x : α
h : (bouquet v E(G)).Inc e x
⊢ e ∈ E(G) ∧ x = v

Tactic:
simp only [bouquet_inc] at h

Premises used: Graph.bouquet_inc
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
hrw : V(G) = {v}
e : β
x : α
h : e ∈ E(G) ∧ x = v
refine_2 : ∀ (z w : α) (hzw : G.IsLink e z w), G.Inc e x
⊢ G.Inc e x

Tactic:
obtain ⟨z, w, hzw⟩ := exists_isLink_of_mem_edgeSet h.1

Premises used: Graph.exists_isLink_of_mem_edgeSet, And.left
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
hrw : V(G) = {v}
e : β
x : α
h : e ∈ E(G) ∧ x = v
z w : α
hzw : G.IsLink e z w
refine_2 : G.Inc e z
⊢ G.Inc e x

Tactic:
rw [h.2, ← show z = v from (show z ∈ {v} from hrw ▸ hzw.left_mem)]

Premises used: And.right
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
hrw : V(G) = {v}
e : β
x : α
h : e ∈ E(G) ∧ x = v
z w : α
hzw : G.IsLink e z w
⊢ G.Inc e z

Tactic:
hzw.inc_left

Premises used: Graph.IsLink.inc_left
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
hrw : V(G) = {v}
e : β
x : α
h : e ∈ E(G) ∧ x = v
z w : α
hzw : G.IsLink e z w
⊢ G.Inc e z

Tactic:
exact hzw.inc_left

Premises used: Graph.IsLink.inc_left
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
v : α
G : Graph α β
h : V(G) = {v}
⊢ v ∈ V(G)

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
v : α
G : Graph α β
h : V(G) = {v}
⊢ V(G).Subsingleton

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
hne : V(G).Nonempty
hss : V(G).Subsingleton
⊢ ∃ (x : α) (F : Set β), G = bouquet x F

Tactic:
⟨_, _, eq_bouquet_of_subsingleton hne.some_mem hss⟩

Premises used: Set.Nonempty.some_mem, Exists.intro, Graph.eq_bouquet_of_subsingleton
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
v : α
⊢ bouquet v ∅ = noEdge {v} β

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
x y : α
e_1 : β
G_1 H : Graph α β
F F₀ : Set β
X : Set α
G : Graph α β
E₀ : Set β
e : β
h : e ∈ E(G) ∩ E₀
⊢ ∃ (x : α) (y : α), e ∈ E₀ ∧ G.IsLink e x y

Tactic:
simp [G.exists_isLink_of_mem_edgeSet h.1, h.2]

Premises used: Graph.exists_isLink_of_mem_edgeSet, And.right, And.left
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
E₀ : Set β
⊢ ∀ ⦃e : β⦄ ⦃x y : α⦄, (G.restrict E₀).IsLink e x y → G.IsLink e x y

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
E₀ : Set β
h : G.restrict E₀ = G
⊢ E(G) ⊆ E₀

Tactic:
simpa using h.ge.edgeSet_mono

Premises used: Eq.ge, Graph.IsSubgraph.edgeSet_mono
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
E₀ : Set β
h : E(G) ⊆ E₀
⊢ V(G.restrict E₀) = V(G)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
E₀ : Set β
h : E(G) ⊆ E₀
⊢ E(G.restrict E₀) = E(G)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
⊢ G.restrict E(G) ≤ G

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
⊢ G ≤ G

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
⊢ E(G.restrict E(G)) = E(G)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F : Set β
⊢ G.restrict (E(G) ∩ F) ≤ G

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F : Set β
⊢ G.restrict F ≤ G

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F : Set β
⊢ V(G.restrict (E(G) ∩ F)) = V(G.restrict F)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F : Set β
⊢ E(G.restrict (E(G) ∩ F)) = E(G.restrict F)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F : Set β
rw : G.restrict (E(G) ∩ F) = G.restrict F
rw₁ rw₂ : G.restrict F = G.restrict F
⊢ G.restrict (F ∩ E(G)) = G.restrict F

Tactic:
rw [inter_comm, restrict_edgeSet_inter]

Premises used: Graph.restrict_edgeSet_inter, Set.inter_comm
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
⊢ G.restrict F ≤ G

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
refine_1 : V(H.restrict F) ⊆ V(G.restrict F)
refine_2 : E(H.restrict F) ⊆ E(G.restrict F)
⊢ H.restrict F ≤ G.restrict F

Tactic:
refine (Compatible.of_le_le (G := G) (restrict_le.trans h) (by simp)).le_iff.mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, Graph.restrict_le, Graph.Compatible.le_iff, And.intro, LE.le.trans, Graph.Compatible.of_le_le
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
⊢ V(H.restrict F) ⊆ V(G.restrict F)

Tactic:
simpa using h.vertexSet_mono

Premises used: Graph.IsSubgraph.vertexSet_mono
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
⊢ E(H.restrict F) ⊆ E(G.restrict F)

Tactic:
simp [inter_subset_left.trans h.edgeSet_mono]

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, Graph.IsSubgraph.edgeSet_mono
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
F : Set β
⊢ (G.restrict F).Inc e x ↔ G.Inc e x ∧ e ∈ F

Tactic:
simp [Inc, and_comm]

Premises used: Graph.Inc, and_comm
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
F : Set β
⊢ (G.restrict F).IsLoopAt e x ↔ G.IsLoopAt e x ∧ e ∈ F

Tactic:
simp [← isLink_self_iff, and_comm]

Premises used: and_comm, Graph.isLink_self_iff
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ G.restrict F₁ ≤ G

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ G.restrict (F₁ ∩ F₂) ≤ G

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ V((G.restrict F₁).restrict F₂) = V(G.restrict (F₁ ∩ F₂))

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
refine : E((G.restrict F₁).restrict F₂) = E(G.restrict (F₁ ∩ F₂))
⊢ (G.restrict F₁).restrict F₂ = G.restrict (F₁ ∩ F₂)

Tactic:
refine (Compatible.of_le_le (G := G) (restrict_le.trans (by simp)) (by simp)).ext (by simp) ?_

Premises used: Graph.restrict_le, Graph.Compatible.ext, LE.le.trans, Graph.Compatible.of_le_le
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
rw : E(G) ∩ F₁ ∩ F₂ = E(G) ∩ F₁ ∩ F₂
rw₁ rw₂ : F₂ ∩ (E(G) ∩ F₁) = F₂ ∩ (E(G) ∩ F₁)
⊢ E(G) ∩ F₁ ∩ F₂ = E(G) ∩ (F₁ ∩ F₂)

Tactic:
rw [← inter_assoc, inter_comm _ F₂]

Premises used: Set.inter_comm, Set.inter_assoc
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G_1 H : Graph α β
F_1 F₀ : Set β
X : Set α
G : Graph α β
F : Set β
⊢ E(G.restrict (E(G) \ F)) = E(G) \ F

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
x_1 y_1 : α
e_1 : β
G_1 H : Graph α β
F_1 F₀ : Set β
X : Set α
G : Graph α β
F : Set β
e : β
x y : α
simp : G.IsLink e x y → e ∉ F → e ∈ E(G)
⊢ (G.restrict (E(G) \ F)).IsLink e x y ↔ (fun (e : β) (x y : α) ↦ G.IsLink e x y ∧ e ∉ F) e x y

Tactic:
simp only [restrict_isLink, mem_diff, and_comm, and_congr_left_iff, and_iff_left_iff_imp]

Premises used: Graph.restrict_isLink, and_comm, Set.mem_diff, and_congr_left_iff, and_iff_left_iff_imp
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
x_1 y_1 : α
e_1 : β
G_1 H : Graph α β
F_1 F₀ : Set β
X : Set α
G : Graph α β
F : Set β
e : β
x y : α
⊢ G.IsLink e x y → e ∉ F → e ∈ E(G)

Tactic:
fun h _ ↦ h.edge_mem

Premises used: Graph.IsLink.edge_mem
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
x_1 y_1 : α
e_1 : β
G_1 H : Graph α β
F_1 F₀ : Set β
X : Set α
G : Graph α β
F : Set β
e : β
x y : α
⊢ G.IsLink e x y → e ∉ F → e ∈ E(G)

Tactic:
exact fun h _ ↦ h.edge_mem
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F : Set β
⊢ G.restrict (E(G) \ F) = G.deleteEdges F

Tactic:
copy_eq .. |>.symm

Premises used: Graph.deleteEdges, Graph.copy_eq, Eq.symm
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F : Set β
⊢ G.deleteEdges F ≤ G

Tactic:
simp [← restrict_edgeSet_diff_eq_deleteEdges]

Premises used: Graph.restrict_edgeSet_diff_eq_deleteEdges
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F : Set β
⊢ E(G.restrict F) = E(G.deleteEdges (E(G) \ F))

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
⊢ G.deleteEdges ∅ = G

Tactic:
simp [← restrict_edgeSet_diff_eq_deleteEdges]

Premises used: Graph.restrict_edgeSet_diff_eq_deleteEdges
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
simp_rw : H.restrict (E(H) \ F) ≤ G.restrict (E(G) \ F)
⊢ H.deleteEdges F ≤ G.deleteEdges F

Tactic:
simp_rw [← restrict_edgeSet_diff_eq_deleteEdges]

Premises used: Graph.restrict_edgeSet_diff_eq_deleteEdges
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
⊢ H.restrict (E(H) \ F) ≤ G.restrict (E(G) \ F)

Tactic:
(restrict_mono_left h (E(H) \ F)).trans (G.restrict_mono_right ?_)

Premises used: Graph.restrict_mono_right, SDiff.sdiff, Graph.edgeSet, LE.le.trans, Graph.restrict_mono_left
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
refine : E(H) \ F ⊆ E(G) \ F
⊢ H.restrict (E(H) \ F) ≤ G.restrict (E(G) \ F)

Tactic:
refine (restrict_mono_left h (E(H) \ F)).trans (G.restrict_mono_right ?_)

Premises used: Graph.restrict_mono_right, SDiff.sdiff, Graph.edgeSet, LE.le.trans, Graph.restrict_mono_left
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
⊢ E(H) \ F ⊆ E(G) \ F

Tactic:
diff_subset_diff_left h.edgeSet_mono

Premises used: Set.diff_subset_diff_left, Graph.IsSubgraph.edgeSet_mono
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
⊢ E(H) \ F ⊆ E(G) \ F

Tactic:
exact diff_subset_diff_left h.edgeSet_mono

Premises used: Set.diff_subset_diff_left, Graph.IsSubgraph.edgeSet_mono
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
F : Set β
⊢ (G.deleteEdges F).Inc e x ↔ G.Inc e x ∧ e ∉ F

Tactic:
simp [Inc, and_comm]

Premises used: Graph.Inc, and_comm
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
F : Set β
simp : G.IsLoopAt e x → e ∉ F → e ∈ E(G)
⊢ (G.deleteEdges F).IsLoopAt e x ↔ G.IsLoopAt e x ∧ e ∉ F

Tactic:
simp only [← restrict_edgeSet_diff_eq_deleteEdges, restrict_isLoopAt, mem_diff,
    and_congr_right_iff, and_iff_right_iff_imp]

Premises used: Graph.restrict_isLoopAt, and_congr_right_iff, Graph.restrict_edgeSet_diff_eq_deleteEdges, Set.mem_diff, and_iff_right_iff_imp
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
F : Set β
⊢ G.IsLoopAt e x → e ∉ F → e ∈ E(G)

Tactic:
fun h _ ↦ h.edge_mem

Premises used: Graph.IsLoopAt.edge_mem
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
F : Set β
⊢ G.IsLoopAt e x → e ∉ F → e ∈ E(G)

Tactic:
exact fun h _ ↦ h.edge_mem
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
simp : G.restrict (F₁ᶜ ∩ (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ))) = G.restrict (F₁ᶜ ∩ F₂ᶜ)
⊢ (G.deleteEdges F₁).deleteEdges F₂ = G.deleteEdges (F₁ ∪ F₂)

Tactic:
simp only [← restrict_edgeSet_diff_eq_deleteEdges, diff_eq_compl_inter, restrict_inter_edgeSet,
    edgeSet_restrict, restrict_restrict, compl_union]

Premises used: Set.compl_union, Set.diff_eq_compl_inter, Graph.restrict_inter_edgeSet, Graph.restrict_edgeSet_diff_eq_deleteEdges, Graph.edgeSet_restrict, Graph.restrict_restrict
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
rw : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ) ∩ F₁ᶜ) = G.restrict (F₁ᶜ ∩ F₂ᶜ)
rw₁ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ) ∩ F₁ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₂ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ ∩ F₁ᶜ)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₃ : G.restrict (F₂ᶜ ∩ (E(G) ∩ (F₁ᶜ ∩ F₁ᶜ))) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₄ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₅ : G.restrict (E(G) ∩ F₁ᶜ ∩ F₂ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₆ : G.restrict (E(G) ∩ (F₁ᶜ ∩ F₂ᶜ)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₇ : G.restrict (F₁ᶜ ∩ F₂ᶜ ∩ E(G)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₈ : G.restrict (F₁ᶜ ∩ F₂ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₉ rw₁₀ : G.restrict (F₂ᶜ ∩ F₁ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
⊢ G.restrict (F₁ᶜ ∩ (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ))) = G.restrict (F₁ᶜ ∩ F₂ᶜ)

Tactic:
rw [← inter_comm, inter_comm F₁ᶜ, inter_assoc, inter_assoc, inter_self, inter_comm,
    inter_assoc, inter_comm, restrict_inter_edgeSet, inter_comm]

Premises used: Compl.compl, Set.inter_self, Graph.restrict_inter_edgeSet, Set.inter_comm, Set.inter_assoc
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
x_1 y : α
e : β
G_1 H : Graph α β
F F₀ : Set β
X_1 : Set α
G : Graph α β
X : Set α
x_2 : β
h :
  Membership.mem (γ := Set β)
    {e : β | ∃ (x : α) (y : α), (fun (e : β) (x y : α) ↦ G.IsLink e x y ∧ x ∈ X ∧ y ∈ X) e x y} x_2
x : α
⊢ ∀ ⦃y : α⦄,
    (fun (x y : α) ↦ G.IsLink x_2 x y ∧ x ∈ X ∧ y ∈ X) x y → (fun (x y : α) ↦ G.IsLink x_2 x y ∧ x ∈ X ∧ y ∈ X) y x

Tactic:
simp +contextual [G.isLink_comm (x := x)]

Premises used: Graph.isLink_comm
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
X : Set α
hX : X ⊆ V(G)
⊢ G.induce X ≤ G

Tactic:
⟨hX, fun _ _ _ h ↦ h.1⟩

Premises used: Graph.IsSubgraph.mk, And.left
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
X : Set α
⊢ G.induce X ≤ G ↔ X ⊆ V(G)

Tactic:
⟨(·.vertexSet_mono), induce_le⟩

Premises used: Graph.induce_le, Iff.intro, Graph.IsSubgraph.vertexSet_mono
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
X : Set α
⊢ E(G.induce X) = {e : β | ∃ (x : α) (y : α), G.IsLink e x y ∧ x ∈ X ∧ y ∈ X}

Tactic:
rfl

Premises used: setOf, rfl
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
⊢ G.induce V(G) ≤ G

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
refine : ∀ (e : β) (h : e ∈ E(G)), e ∈ E(G.induce V(G))
⊢ G.induce V(G) = G

Tactic:
refine (Compatible.of_le_le (G := G) (by simp) (by simp)).ext rfl <| Set.ext fun e ↦
    ⟨fun ⟨_, _, h⟩ ↦ h.1.edge_mem, fun h ↦ ?_⟩

Premises used: Graph.Compatible.ext, Graph.Compatible.of_le_le, rfl
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
e : β
h : e ∈ E(G)
obtain : ∀ (x y : α) (h : G.IsLink e x y), e ∈ E(G.induce V(G))
⊢ e ∈ E(G.induce V(G))

Tactic:
obtain ⟨x, y, h⟩ := exists_isLink_of_mem_edgeSet h

Premises used: Graph.exists_isLink_of_mem_edgeSet
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
e : β
h_1 : e ∈ E(G)
x y : α
h : G.IsLink e x y
⊢ e ∈ E(G.induce V(G))

Tactic:
⟨x, y, h, h.left_mem, h.right_mem⟩

Premises used: Set.Mem, Graph.IsLink.right_mem, setOf, Graph.IsLink.left_mem, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
e : β
h_1 : e ∈ E(G)
x y : α
h : G.IsLink e x y
⊢ e ∈ E(G.induce V(G))

Tactic:
exact ⟨x, y, h, h.left_mem, h.right_mem⟩
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
X : Set α
⊢ V(G.induce (V(G) \ X)) = V(G) \ X

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
X : Set α
simp : G.IsLink e x y → ((x ∈ V(G) ∧ x ∉ X) ∧ y ∈ V(G) ∧ y ∉ X ↔ x ∉ X ∧ y ∉ X)
⊢ (G.deleteVerts X).IsLink e x y ↔ G.IsLink e x y ∧ x ∉ X ∧ y ∉ X

Tactic:
simp only [deleteVerts, induce_isLink, mem_diff, and_congr_right_iff]

Premises used: Graph.deleteVerts, and_congr_right_iff, Graph.induce_isLink, Set.mem_diff
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
X : Set α
h : G.IsLink e x y
⊢ (x ∈ V(G) ∧ x ∉ X) ∧ y ∈ V(G) ∧ y ∉ X ↔ x ∉ X ∧ y ∉ X

Tactic:
simp [h.left_mem, h.right_mem]

Premises used: Graph.IsLink.right_mem, Graph.IsLink.left_mem
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
X : Set α
⊢ G.IsLink e x y → ((x ∈ V(G) ∧ x ∉ X) ∧ y ∈ V(G) ∧ y ∉ X ↔ x ∉ X ∧ y ∉ X)

Tactic:
exact fun h ↦ by simp [h.left_mem, h.right_mem]
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
X : Set α
⊢ E(G.deleteVerts X) = {e : β | ∃ (x : α) (y : α), G.IsLink e x y ∧ x ∉ X ∧ y ∉ X}

Tactic:
simp [edgeSet_eq_setOf_exists_isLink]

Premises used: Graph.edgeSet_eq_setOf_exists_isLink
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
⊢ G.deleteVerts ∅ = G

Tactic:
simp [deleteVerts]

Premises used: Graph.deleteVerts
-- Module: Mathlib.Combinatorics.Graph.Delete
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
X : Set α
⊢ G.deleteVerts X ≤ G

Tactic:
G.induce_le diff_subset

Premises used: Graph.induce_le, Set.diff_subset, Graph.deleteVerts
-- Module: Mathlib.Combinatorics.Graph.Lattice
Goal:
α : Type u_1
β : Type u_2
x y : α
e_1 : β
G_1 H_1 G H : Graph α β
e : β
simp :
  (((∃ (x : α) (y : α), G.IsLink e x y) ∧ ∃ (x : α) (y : α), H.IsLink e x y) ∧
      ∀ (x y : α), G.IsLink e x y ↔ H.IsLink e x y) ↔
    ∃ (x : α) (y : α), G.IsLink e x y ∧ H.IsLink e x y
⊢ Membership.mem (γ := Set β) {e : β | e ∈ E(G) ∩ E(H) ∧ ∀ (x y : α), G.IsLink e x y ↔ H.IsLink e x y} e ↔
    ∃ (x : α) (y : α), G.IsLink e x y ∧ H.IsLink e x y

Tactic:
simp only [edgeSet_eq_setOf_exists_isLink, mem_inter_iff, mem_setOf_eq]

Premises used: Set.mem_inter_iff, Set.mem_setOf_eq, Graph.edgeSet_eq_setOf_exists_isLink
-- Module: Mathlib.Combinatorics.Graph.Lattice
Goal:
α : Type u_1
β : Type u_2
x_1 y_1 : α
e_1 : β
G_1 H_1 G H : Graph α β
e : β
h_1 :
  ((∃ (x : α) (y : α), G.IsLink e x y) ∧ ∃ (x : α) (y : α), H.IsLink e x y) ∧
    ∀ (x y : α), G.IsLink e x y ↔ H.IsLink e x y
x y : α
hexy : G.IsLink e x y
z w : α
hezw : H.IsLink e z w
h : ∀ (x y : α), G.IsLink e x y ↔ H.IsLink e x y
rwa rwa₁ rwa₂ rwa₃ : G.IsLink e x y
⊢ H.IsLink e x y

Tactic:
rwa [← h]