mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
G H : Graph α β
h : x ∈ V(G)
h' : x ∈ V(H)
⊢ ¬Disjoint G H

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ H G : Graph α β
E : Set β
hE : ∀ (e : β), e ∈ E ↔ ∃ x y, G.IsLink e x y
⊢ ∀ ⦃e : β⦄, e ∈ E → Std.Symm (G.IsLink e)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ (G.restrict F₁).restrict F₂ = G.restrict (F₁ ∩ F₂)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
E : Set β
hE : ∀ (e : β), e ∈ E ↔ ∃ x y, G.IsLink e x y
⊢ E = E(G)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e : β
G✝ H : Graph α β
F✝ F₀ : Set β
X : Set α
G : Graph α β
F : Set β
⊢ E(G.restrict (E(G) \ F)) = E(G) \ F

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ y✝ : α
e✝ : β
G✝ H : Graph α β
F✝ F₀ : Set β
X : Set α
G : Graph α β
F : Set β
e : β
x y : α
⊢ (G.restrict (E(G) \ F)).IsLink e x y ↔ G.IsLink e x y ∧ e ∉ F

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F : Set β
⊢ G.deleteEdges F ≤ G

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e✝ : β
G✝ H✝ G H : Graph α β
e : β
⊢ e ∈ {e | e ∈ E(G) ∩ E(H) ∧ ∀ (x y : α), G.IsLink e x y ↔ H.IsLink e x y} ↔ ∃ x y, G.IsLink e x y ∧ H.IsLink e x y

Tactic:
simp only [edgeSet_eq_setOfPred_exists_isLink, mem_inter_iff, mem_ofPred_eq]

Goal state after:
α : Type u_1
β : Type u_2
x y : α
e✝ : β
G✝ H✝ G H : Graph α β
e : β
⊢ (((∃ 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
Module: Mathlib.Combinatorics.Graph.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝¹ y✝ : α
e✝ : β
G✝ H✝ G H : Graph α β
e : β
x✝ : ((∃ 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
⊢ H.IsLink e x y

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝¹ y✝ : α
e✝ : β
G✝ H✝ G H : Graph α β
e : β
x✝ : ∃ x y, G.IsLink e x y ∧ H.IsLink e x y
x y : α
hfG : G.IsLink e x y
hfH : H.IsLink e x y
z w : α
⊢ G.IsLink e z w ↔ H.IsLink e z w

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e✝ : β
G✝ H✝ G H : Graph α β
e : β
⊢ e ∈ {e | e ∈ E(G) ∩ E(H) ∧ ∀ (x y : α), G.IsLink e x y ↔ H.IsLink e x y} ↔ ∃ x y, G.IsLink e x y ∧ H.IsLink e x y

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e : β
G✝ H✝ G H : Graph α β
⊢ ∀ ⦃e : β⦄ ⦃x y : α⦄,
    { vertexSet := V(G) ∩ V(H), IsLink := fun e x y ↦ G.IsLink e x y ∧ H.IsLink e x y,
            edgeSet := {e | e ∈ E(G) ∩ E(H) ∧ ∀ (x y : α), G.IsLink e x y ↔ H.IsLink e x y}, isLink_symm := ⋯,
            eq_or_eq_of_isLink_of_isLink := ⋯, edge_mem_iff_exists_isLink := ⋯, left_mem_of_isLink := ⋯ }.IsLink
        e x y →
      G.IsLink e x y

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e : β
G✝ H✝ G H : Graph α β
⊢ ∀ ⦃e : β⦄ ⦃x y : α⦄,
    { vertexSet := V(G) ∩ V(H), IsLink := fun e x y ↦ G.IsLink e x y ∧ H.IsLink e x y,
            edgeSet := {e | e ∈ E(G) ∩ E(H) ∧ ∀ (x y : α), G.IsLink e x y ↔ H.IsLink e x y}, isLink_symm := ⋯,
            eq_or_eq_of_isLink_of_isLink := ⋯, edge_mem_iff_exists_isLink := ⋯, left_mem_of_isLink := ⋯ }.IsLink
        e x y →
      H.IsLink e x y

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ y✝ : α
e✝ : β
G H✝ H G₁ G₂ : Graph α β
h₁ : H ≤ G₁
h₂ : H ≤ G₂
e : β
x y : α
h : H.IsLink e x y
⊢ { vertexSet := V(G₁) ∩ V(G₂), IsLink := fun e x y ↦ G₁.IsLink e x y ∧ G₂.IsLink e x y,
        edgeSet := {e | e ∈ E(G₁) ∩ E(G₂) ∧ ∀ (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y}, isLink_symm := ⋯,
        eq_or_eq_of_isLink_of_isLink := ⋯, edge_mem_iff_exists_isLink := ⋯, left_mem_of_isLink := ⋯ }.IsLink
    e x y

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
⊢ (G ⊓ H).Inc e x ↔ ∃ y, G.IsLink e x y ∧ H.IsLink e x y

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
⊢ (G ⊓ H).IsLoopAt e x ↔ G.IsLoopAt e x ∧ H.IsLoopAt e x

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
⊢ (G ⊓ H).IsNonloopAt e x ↔ ∃ y, y ≠ x ∧ G.IsLink e x y ∧ H.IsLink e x y

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
⊢ Disjoint G H ↔ Disjoint V(G) V(H)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F : Set β
⊢ E(G.restrict F) = E(G.deleteEdges (E(G) \ F))

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
⊢ G.deleteEdges ∅ = G

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
h : G.Compatible H
⊢ E(G ⊓ H) = E(G) ∩ E(H)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
E : Set β
hE : ∀ (e : β), e ∈ E ↔ ∃ x y, G.IsLink e x y
⊢ { vertexSet := V(G), IsLink := G.IsLink, edgeSet := E, isLink_symm := ⋯, eq_or_eq_of_isLink_of_isLink := ⋯,
      edge_mem_iff_exists_isLink := hE, left_mem_of_isLink := ⋯ } =
    G

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
hA : ∃ A, #S ≤ #A ∧ ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
⊢ ∃ H x Z, ↑(Fintype.card ↥H) ≤ (2 / ε - 1) * ↑(#S) ∧ ↑(#Z) ≤ 2 / ε - 1 ∧ ↑S ⊆ ↑H * ↑Z

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
⊢ H.deleteEdges F ≤ G.deleteEdges F

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : 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:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
F : Set β
⊢ (G.deleteEdges F).IsLoopAt e x ↔ G.IsLoopAt e x ∧ e ∉ F

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hA₀ : A.Nonempty
hA₁ : ↑(#(A * A)) ≤ (2 - ε) * ↑(#A)
⊢ #A ≤ #A

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ (G.deleteEdges F₁).deleteEdges F₂ = G.deleteEdges (F₁ ∪ F₂)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e : β
G✝ H : Graph α β
F F₀ : Set β
X✝ : Set α
G : Graph α β
X : Set α
⊢ ∀ ⦃e : β⦄,
    e ∈ {e | ∃ x y, (fun e x y ↦ G.IsLink e x y ∧ x ∈ X ∧ y ∈ X) e x y} →
      Std.Symm fun x y ↦ G.IsLink e x y ∧ x ∈ X ∧ y ∈ X

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
⊢ G.induce V(G) ≤ G

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
⊢ G.induce V(G) = G

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y
⊢ G₁ = G₂

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
X : Set α
⊢ V(G.deleteVerts X) = V(G) \ X

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : 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:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
X : Set α
⊢ (G.deleteVerts X).IsLink e x y ↔ G.IsLink e x y ∧ x ∉ X ∧ y ∉ X

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : 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:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
⊢ G.deleteVerts ∅ = G

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x : α), G₁.Inc e x ↔ G₂.Inc e x
x✝² : β
x✝¹ x✝ : α
⊢ G₁.IsLink x✝² x✝¹ x✝ ↔ G₂.IsLink x✝² x✝¹ x✝

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u v w : α
e✝ f : β
G✝ H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
e : β
he : e ∈ edgeSet
⊢ Std.Symm (IsLink e)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
⊢ ∀ ⦃e : β⦄ ⦃x y v w : α⦄, IsLink e x y → IsLink e v w → x = v ∨ x = w

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
⊢ ∀ (e : β), e ∈ edgeSet ↔ ∃ x y, IsLink e x y

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
⊢ ∀ ⦃e : β⦄ ⦃x y : α⦄, IsLink e x y → x ∈ vertexSet

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
V : Set α
E : Set β
IsLink : β → α → α → Prop
hV : V(G) = V
hE : E(G) = E
h_isLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
⊢ G.copy hV hE h_isLink = G

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hGH : G.Compatible H
heH : e ∈ E(H)
h : G.Inc e x
⊢ H.Inc e x

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hGH : G.Compatible H
heH : e ∈ E(H)
h : G.IsNonloopAt e x
⊢ H.IsNonloopAt e x

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
x y z u v w : α
e f : β✝
G H : Graph α β✝
vertexSet : Set α
β : Type u_3
⊢ ∀ ⦃e : β⦄, e ∈ ∅ → Std.Symm fun x x_1 ↦ False

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
x y z u v w : α
e f : β✝
G H : Graph α β✝
vertexSet : Set α
β : Type u_3
⊢ ∀ ⦃e : β⦄ ⦃x : α⦄ ⦃y : α⦄ ⦃v w : α⦄, False → False → x = v ∨ x = w

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
x y z u v w : α
e f : β✝
G H : Graph α β✝
vertexSet : Set α
β : Type u_3
⊢ ∀ (e : β), e ∈ ∅ ↔ ∃ x y, False

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
h : G = noEdge V(G) β
⊢ E(G) = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
⊢ E(G) = ∅ ↔ G = noEdge V(G) β

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u✝ v✝ w : α
e f : β
G H : Graph α β
vertexSet : Set α
edgeSet✝ : Set β
u v : α
edgeSet : Set β
⊢ ∀ ⦃e : β⦄, e ∈ edgeSet → Std.Symm fun x y ↦ e ∈ edgeSet ∧ (x = u ∧ y = v ∨ x = v ∧ y = u)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u✝ v✝ w : α
e f : β
G H : Graph α β
vertexSet : Set α
edgeSet✝ : Set β
u v : α
edgeSet : Set β
⊢ ∀ ⦃e : β⦄ ⦃x y v_1 w : α⦄,
    e ∈ edgeSet ∧ (x = u ∧ y = v ∨ x = v ∧ y = u) → e ∈ edgeSet ∧ (v_1 = u ∧ w = v ∨ v_1 = v ∧ w = u) → x = v_1 ∨ x = w

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u✝ v✝ w : α
e f : β
G H : Graph α β
vertexSet : Set α
edgeSet✝ : Set β
u v : α
edgeSet : Set β
⊢ ∀ (e : β), e ∈ edgeSet ↔ ∃ x y, e ∈ edgeSet ∧ (x = u ∧ y = v ∨ x = v ∧ y = u)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x u v : α
e : β
edgeSet : Set β
⊢ (banana u v edgeSet).Inc e x ↔ e ∈ edgeSet ∧ (x = u ∨ x = v)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : α
edgeSet : Set β
⊢ ∀ (e : β) (x : α), (banana u v edgeSet).Inc e x ↔ (banana v u edgeSet).Inc e x

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x u v : α
e : β
edgeSet : Set β
⊢ (banana u v edgeSet).IsNonloopAt e x ↔ e ∈ edgeSet ∧ (x = u ∨ x = v) ∧ u ≠ v

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x u v : α
e : β
edgeSet : Set β
⊢ (banana u v edgeSet).IsLoopAt e x ↔ e ∈ edgeSet ∧ x = u ∧ u = v

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x y u v : α
edgeSet : Set β
⊢ (banana u v edgeSet).Adj x y ↔ edgeSet.Nonempty ∧ s(x, y) = s(u, v)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : α
⊢ banana u v ∅ = noEdge {u, v} β

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
v : α
edgeSet : Set β
⊢ V(bouquet v edgeSet) = {v}

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : 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:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
v : α
edgeSet : Set β
⊢ (bouquet v edgeSet).Inc e x ↔ e ∈ edgeSet ∧ x = v

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x y v : α
edgeSet : Set β
⊢ (bouquet v edgeSet).Adj x y ↔ edgeSet.Nonempty ∧ x = v ∧ y = v

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
v : α
edgeSet : Set β
⊢ (bouquet v edgeSet).IsLoopAt e x ↔ e ∈ edgeSet ∧ x = v

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x v : α
e : β
edgeSet : Set β
⊢ ¬(bouquet v edgeSet).IsNonloopAt e x

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : 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:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
⊢ G = bouquet v E(G)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
v : α
G : Graph α β
h : V(G) = {v}
⊢ v ∈ V(G)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
v : α
G : Graph α β
h : V(G) = {v}
⊢ V(G).Subsingleton

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
v : α
⊢ bouquet v ∅ = noEdge {v} β

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G✝ H : Graph α β
f✝ g : α → α'
u v : α
e : β
x y : α'
f : α → α'
G : Graph α β
⊢ ∀ ⦃e : β⦄ ⦃x y v w : α'⦄, Relation.Map (G.IsLink e) f f x y → Relation.Map (G.IsLink e) f f v w → x = v ∨ x = w

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G✝ H : Graph α β
f✝ g : α → α'
u v : α
e✝ : β
x y : α'
f : α → α'
G : Graph α β
e : β
⊢ e ∈ E(G) ↔ ∃ x y, Relation.Map (G.IsLink e) f f x y

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G✝ H : Graph α β
f✝ g : α → α'
u v : α
e : β
x y : α'
f : α → α'
G : Graph α β
⊢ ∀ ⦃e : β⦄ ⦃x y : α'⦄, Relation.Map (G.IsLink e) f f x y → x ∈ f '' V(G)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
e : β
x : α'
f : α → α'
⊢ (map f G).Inc e x ↔ ∃ v, G.Inc e v ∧ x = f v

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
v : α
e : β
f : α → α'
h : G.Inc e v
⊢ (map f G).Inc e (f v)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
x y : α'
f : α → α'
⊢ (map f G).Adj x y ↔ Relation.Map G.Adj f f x y

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
u v : α
f : α → α'
h : G.Adj u v
⊢ (map f G).Adj (f u) (f v)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: α : Type u_1
β : Type u_4
G : Graph α β
⊢ map id G = G

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G : Graph α β
f : α → α'
f' : α' → α''
⊢ map f' (map f G) = map (f' ∘ f) G

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G : Graph α β
f : α → α'
f' : α' → α''
⊢ map f' (map f G) = map (f' ∘ f) G

Tactic:
by
  ext a b c <;> simp [map_apply]

Goal state after:
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_4
G H : Graph α β
f : α → α'
h : G ≤ H
v : α'
⊢ v ∈ V(map f G) → v ∈ V(map f H)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_4
G H : Graph α β
f : α → α'
hsle : G ≤s H
⊢ V(map f G) = V(map f H)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
f g : α → α'
h : EqOn f g V(G)
⊢ V(map f G) = V(map g G)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
f g : α → α'
h : EqOn f g V(G)
⊢ map f G = map g G

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
inst✝ : G.Loopless
hE : E(G).Nonempty
⊢ V(G).Nontrivial

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
hG : G.Loopless
hle : H ≤ G
⊢ H.Loopless

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
inst✝ : G.Simple
hle : H ≤ G
e : β
x : α
⊢ ¬H.IsLoopAt e x

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
u v : α
e f : β
X Y : Set α
inst✝ : G.Simple
V : Set α
⊢ ∀ (e : β) (x : α), ¬(noEdge V β).IsLoopAt e x

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
u v : α
e f : β
X Y : Set α
inst✝ : G.Simple
V : Set α
⊢ ∀ ⦃e f : β⦄ ⦃x y : α⦄, (noEdge V β).IsLink e x y → (noEdge V β).IsLink f x y → e = f

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: α : Type u_1
β : Type u_2
G✝ H : Graph α β
u✝ v✝ : α
e f : β
X Y : Set α
G : Graph α β
u v : ↑V(G)
⊢ u ≠ v ∧ G.Adj ↑u ↑v → v ≠ u ∧ G.Adj ↑v ↑u

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
inst✝ : G.Loopless
u v : ↑V(G)
⊢ G.toSimpleGraph.Adj u v ↔ G.Adj ↑u ↑v

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
h : G ≤s H
⊢ G.toSimpleGraph ≤ ⋯ ▸ H.toSimpleGraph

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: α : Type u_1
β : Type u_2
G✝ H : Graph α β
u✝ v✝ : α
e✝ f : β
X Y : Set α
G : SimpleGraph α
e : Sym2 α
he : e ∈ G.edgeSet
u v : α
⊢ e = s(u, v) ∧ e ∈ G.edgeSet → e = s(v, u) ∧ e ∈ G.edgeSet

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: α : Type u_1
β : Type u_2
G✝ H : Graph α β
u✝ v✝ : α
e✝ f : β
X Y : Set α
G : SimpleGraph α
e : Sym2 α
u v x y : α
he : e = s(u, v) ∧ e ∈ G.edgeSet
hf : e = s(x, y) ∧ e ∈ G.edgeSet
⊢ u = x ∨ u = y

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e✝ f : β
X Y : Set α
G : SimpleGraph α
e : Sym2 α
⊢ e ∈ G.edgeSet ↔ ∃ x y, e = s(x, y) ∧ e ∈ G.edgeSet

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
u v : α
⊢ (ofSimpleGraph G).Adj u v ↔ G.Adj u v

Tactic:
by

Goal state after: