awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
hn : ¬G.Adj s t
e : Sym2 V
x y : V
h : ¬x = t
h_1 : y = t
rw :
  G.Adj s x ↔
    G.Adj x y ∧ ¬(G.Adj x y ∧ (t = x ∨ t = y)) ∨
      Membership.mem (γ := Set (Sym2 V)) ((fun (x : V) ↦ s(x, t)) '' G.neighborSet s) s(x, y)
⊢ G.Adj x s ↔
    G.Adj x y ∧ ¬(G.Adj x y ∧ (t = x ∨ t = y)) ∨
      Membership.mem (γ := Set (Sym2 V)) ((fun (x : V) ↦ s(x, t)) '' G.neighborSet s) s(x, y)

Tactic:
rw [adj_comm]

Premises used: SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
hn : ¬G.Adj s t
e : Sym2 V
x y : V
h : ¬x = t
h_1 : y = t
⊢ G.Adj s x ↔
    G.Adj x y ∧ ¬(G.Adj x y ∧ (t = x ∨ t = y)) ∨
      Membership.mem (γ := Set (Sym2 V)) ((fun (x : V) ↦ s(x, t)) '' G.neighborSet s) s(x, y)

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
hn : ¬G.Adj s t
e : Sym2 V
x y : V
h : ¬x = t
h_1 : ¬y = t
⊢ G.Adj x y ↔
    G.Adj x y ∧ ¬(G.Adj x y ∧ (t = x ∨ t = y)) ∨
      Membership.mem (γ := Set (Sym2 V)) ((fun (x : V) ↦ s(x, t)) '' G.neighborSet s) s(x, y)

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
ha : G.Adj s t
h :
  ∀ (e : Sym2 V),
    e ∈ (G.replaceVertex s t).edgeSet ↔
      e ∈ (G.edgeSet \ G.incidenceSet t ∪ (fun (x : V) ↦ s(x, t)) '' G.neighborSet s) \ {s(t, t)}
⊢ (G.replaceVertex s t).edgeSet =
    (G.edgeSet \ G.incidenceSet t ∪ (fun (x : V) ↦ s(x, t)) '' G.neighborSet s) \ {s(t, t)}

Tactic:
ext e
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
ha : G.Adj s t
e : Sym2 V
⊢ e ∈ (G.replaceVertex s t).edgeSet ↔
    e ∈ (G.edgeSet \ G.incidenceSet t ∪ (fun (x : V) ↦ s(x, t)) '' G.neighborSet s) \ {s(t, t)}

Tactic:
e.inductionOn ?_

Premises used: Sym2.inductionOn
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
ha : G.Adj s t
e : Sym2 V
h :
  ∀ (x y : V),
    s(x, y) ∈ (G.replaceVertex s t).edgeSet ↔
      s(x, y) ∈ (G.edgeSet \ G.incidenceSet t ∪ (fun (x : V) ↦ s(x, t)) '' G.neighborSet s) \ {s(t, t)}
⊢ e ∈ (G.replaceVertex s t).edgeSet ↔
    e ∈ (G.edgeSet \ G.incidenceSet t ∪ (fun (x : V) ↦ s(x, t)) '' G.neighborSet s) \ {s(t, t)}

Tactic:
refine e.inductionOn ?_
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
ha : G.Adj s t
e : Sym2 V
h :
  ∀ (x y : V),
    (if x = t then if y = t then False else G.Adj s y else if y = t then G.Adj x s else G.Adj x y) ↔
      (G.Adj x y ∧ ¬(G.Adj x y ∧ (t = x ∨ t = y)) ∨
          Membership.mem (γ := Set (Sym2 V)) ((fun (x : V) ↦ s(x, t)) '' G.neighborSet s) s(x, y)) ∧
        s(x, y) ∉ {s(t, t)}
⊢ ∀ (x y : V),
    s(x, y) ∈ (G.replaceVertex s t).edgeSet ↔
      s(x, y) ∈ (G.edgeSet \ G.incidenceSet t ∪ (fun (x : V) ↦ s(x, t)) '' G.neighborSet s) \ {s(t, t)}

Tactic:
simp only [replaceVertex, mem_edgeSet, Set.mem_union, Set.mem_diff, mk'_mem_incidenceSet_iff]

Premises used: Set.mem_union, SimpleGraph.replaceVertex, Set.mem_diff, SimpleGraph.mk'_mem_incidenceSet_iff, SimpleGraph.mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
ha : G.Adj s t
e : Sym2 V
x y : V
h : x = t
h_1 : y = t
⊢ False ↔
    (G.Adj x y ∧ ¬(G.Adj x y ∧ (t = x ∨ t = y)) ∨
        Membership.mem (γ := Set (Sym2 V)) ((fun (x : V) ↦ s(x, t)) '' G.neighborSet s) s(x, y)) ∧
      s(x, y) ∉ {s(t, t)}

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
ha : G.Adj s t
e : Sym2 V
x y : V
h : x = t
h_1 : ¬y = t
⊢ G.Adj s y ↔
    (G.Adj x y ∧ ¬(G.Adj x y ∧ (t = x ∨ t = y)) ∨
        Membership.mem (γ := Set (Sym2 V)) ((fun (x : V) ↦ s(x, t)) '' G.neighborSet s) s(x, y)) ∧
      s(x, y) ∉ {s(t, t)}

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
ha : G.Adj s t
e : Sym2 V
x y : V
h : ¬x = t
h_1 : y = t
rw :
  G.Adj s x ↔
    (G.Adj x y ∧ ¬(G.Adj x y ∧ (t = x ∨ t = y)) ∨
        Membership.mem (γ := Set (Sym2 V)) ((fun (x : V) ↦ s(x, t)) '' G.neighborSet s) s(x, y)) ∧
      s(x, y) ∉ {s(t, t)}
⊢ G.Adj x s ↔
    (G.Adj x y ∧ ¬(G.Adj x y ∧ (t = x ∨ t = y)) ∨
        Membership.mem (γ := Set (Sym2 V)) ((fun (x : V) ↦ s(x, t)) '' G.neighborSet s) s(x, y)) ∧
      s(x, y) ∉ {s(t, t)}

Tactic:
rw [adj_comm]

Premises used: SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
ha : G.Adj s t
e : Sym2 V
x y : V
h : ¬x = t
h_1 : y = t
⊢ G.Adj s x ↔
    (G.Adj x y ∧ ¬(G.Adj x y ∧ (t = x ∨ t = y)) ∨
        Membership.mem (γ := Set (Sym2 V)) ((fun (x : V) ↦ s(x, t)) '' G.neighborSet s) s(x, y)) ∧
      s(x, y) ∉ {s(t, t)}

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
ha : G.Adj s t
e : Sym2 V
x y : V
h : ¬x = t
h_1 : ¬y = t
⊢ G.Adj x y ↔
    (G.Adj x y ∧ ¬(G.Adj x y ∧ (t = x ∨ t = y)) ∨
        Membership.mem (γ := Set (Sym2 V)) ((fun (x : V) ↦ s(x, t)) '' G.neighborSet s) s(x, y)) ∧
      s(x, y) ∉ {s(t, t)}

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
hn : ¬G.Adj s t
a :
  (↑(G.replaceVertex s t).edgeFinset : Set (Sym2 V)) =
    (↑(G.edgeFinset \ G.incidenceFinset t ∪ image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)) : Set (Sym2 V))
⊢ (G.replaceVertex s t).edgeFinset =
    G.edgeFinset \ G.incidenceFinset t ∪ image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)

Tactic:
apply Finset.coe_injective

Premises used: Finset.coe_injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
hn : ¬G.Adj s t
a : (G.replaceVertex s t).edgeSet = G.edgeSet \ G.incidenceSet t ∪ (fun (x : V) ↦ s(x, t)) '' G.neighborSet s
⊢ (↑(G.replaceVertex s t).edgeFinset : Set (Sym2 V)) =
    (↑(G.edgeFinset \ G.incidenceFinset t ∪ image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)) : Set (Sym2 V))

Tactic:
push_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
hn : ¬G.Adj s t
⊢ (G.replaceVertex s t).edgeSet = G.edgeSet \ G.incidenceSet t ∪ (fun (x : V) ↦ s(x, t)) '' G.neighborSet s

Tactic:
G.edgeSet_replaceVertex_of_not_adj hn

Premises used: SimpleGraph.edgeSet_replaceVertex_of_not_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
hn : ¬G.Adj s t
⊢ (G.replaceVertex s t).edgeSet = G.edgeSet \ G.incidenceSet t ∪ (fun (x : V) ↦ s(x, t)) '' G.neighborSet s

Tactic:
exact G.edgeSet_replaceVertex_of_not_adj hn

Premises used: SimpleGraph.edgeSet_replaceVertex_of_not_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
ha : G.Adj s t
a :
  (↑(G.replaceVertex s t).edgeFinset : Set (Sym2 V)) =
    (↑((G.edgeFinset \ G.incidenceFinset t ∪ image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)) \ {s(t, t)}) :
      Set (Sym2 V))
⊢ (G.replaceVertex s t).edgeFinset =
    (G.edgeFinset \ G.incidenceFinset t ∪ image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)) \ {s(t, t)}

Tactic:
apply Finset.coe_injective

Premises used: Finset.coe_injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
ha : G.Adj s t
a :
  (G.replaceVertex s t).edgeSet =
    (G.edgeSet \ G.incidenceSet t ∪ (fun (x : V) ↦ s(x, t)) '' G.neighborSet s) \ {s(t, t)}
⊢ (↑(G.replaceVertex s t).edgeFinset : Set (Sym2 V)) =
    (↑((G.edgeFinset \ G.incidenceFinset t ∪ image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)) \ {s(t, t)}) :
      Set (Sym2 V))

Tactic:
push_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
ha : G.Adj s t
⊢ (G.replaceVertex s t).edgeSet =
    (G.edgeSet \ G.incidenceSet t ∪ (fun (x : V) ↦ s(x, t)) '' G.neighborSet s) \ {s(t, t)}

Tactic:
G.edgeSet_replaceVertex_of_adj ha

Premises used: SimpleGraph.edgeSet_replaceVertex_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
ha : G.Adj s t
⊢ (G.replaceVertex s t).edgeSet =
    (G.edgeSet \ G.incidenceSet t ∪ (fun (x : V) ↦ s(x, t)) '' G.neighborSet s) \ {s(t, t)}

Tactic:
exact G.edgeSet_replaceVertex_of_adj ha

Premises used: SimpleGraph.edgeSet_replaceVertex_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
rw :
  ∀ a ∈ G.edgeFinset \ G.incidenceFinset t,
    ∀ (b : Sym2 V), Membership.mem (γ := Finset (Sym2 V)) (image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)) b → a ≠ b
⊢ Disjoint (G.edgeFinset \ G.incidenceFinset t) (image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s))

Tactic:
rw [disjoint_iff_ne]

Premises used: Finset.disjoint_iff_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
e : Sym2 V
he : e ∈ G.edgeFinset \ G.incidenceFinset t
⊢ e ∈ G.edgeFinset ∧ e ∉ G.incidenceSet t

Tactic:
rw [mem_sdiff, mem_incidenceFinset] at he

Premises used: SimpleGraph.mem_incidenceFinset, Finset.mem_sdiff
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
e : Sym2 V
he : e ∈ G.edgeFinset ∧ e ∉ G.incidenceSet t
⊢ e ∈ G.edgeFinset

Tactic:
obtain ⟨_, h⟩ := he
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
e : Sym2 V
he : e ∈ G.edgeFinset ∧ e ∉ G.incidenceSet t
left : e ∈ G.edgeFinset
⊢ e ∉ G.incidenceSet t

Tactic:
obtain ⟨_, h⟩ := he
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
e : Sym2 V
left : e ∈ G.edgeFinset
h : e ∉ G.incidenceSet t
contrapose : ∀ (h : t ∈ e), e ∈ G.incidenceSet t
⊢ t ∉ e

Tactic:
contrapose h
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
e : Sym2 V
left : e ∈ G.edgeFinset
h : t ∈ e
⊢ e ∈ G.incidenceSet t

Tactic:
simp_all [incidenceSet]

Premises used: SimpleGraph.incidenceSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
e : Sym2 V
he : e ∈ G.edgeFinset \ G.incidenceFinset t
⊢ t ∉ e

Tactic:
have : t ∉ e := by
    rw [mem_sdiff, mem_incidenceFinset] at he
    obtain ⟨_, h⟩ := he
    contrapose h
    simp_all [incidenceSet]
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
e : Sym2 V
he : e ∈ G.edgeFinset \ G.incidenceFinset t
this : t ∉ e
⊢ ∀ (b : Sym2 V), Membership.mem (γ := Finset (Sym2 V)) (image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)) b → e ≠ b

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
hn : ¬G.Adj s t
⊢ G.incidenceFinset t ⊆ G.edgeFinset

Tactic:
simp [incidenceFinset, incidenceSet_subset]

Premises used: SimpleGraph.incidenceFinset, SimpleGraph.incidenceSet_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
hn : ¬G.Adj s t
⊢ G.incidenceFinset t ⊆ G.edgeFinset

Tactic:
have inc : G.incidenceFinset t ⊆ G.edgeFinset := by simp [incidenceFinset, incidenceSet_subset]
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
hn : ¬G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
rw :
  #G.edgeFinset + card (α := Sym2 V) (image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)) - G.degree t =
    #G.edgeFinset + G.degree s - G.degree t
⊢ #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t

Tactic:
rw [G.edgeFinset_replaceVertex_of_not_adj hn,
    card_union_of_disjoint G.disjoint_sdiff_neighborFinset_image, card_sdiff_of_subset inc,
    ← Nat.sub_add_comm <| card_le_card inc, card_incidenceFinset_eq_degree]

Premises used: Finset.card_le_card, Finset.card_sdiff_of_subset, Nat.sub_add_comm, SimpleGraph.edgeFinset_replaceVertex_of_not_adj, SimpleGraph.card_incidenceFinset_eq_degree, SimpleGraph.disjoint_sdiff_neighborFinset_image, Finset.card_union_of_disjoint
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
hn : ¬G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
e_a : card (α := Sym2 V) (image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)) = G.degree s
⊢ #G.edgeFinset + card (α := Sym2 V) (image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)) - G.degree t =
    #G.edgeFinset + G.degree s - G.degree t

Tactic:
congr 2
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
hn : ¬G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
e_a : Function.Injective (β := Sym2 V) fun (x : V) ↦ s(x, t)
⊢ card (α := Sym2 V) (image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)) = G.degree s

Tactic:
rw [card_image_of_injective, card_neighborFinset_eq_degree]

Premises used: Finset.card_image_of_injective, SimpleGraph.card_neighborFinset_eq_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
hn : ¬G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ ∀ ⦃a₁ a₂ : V⦄, Eq.{u_1 + 1} (α := Sym2 V) ((fun (x : V) ↦ s(x, t)) a₁) ((fun (x : V) ↦ s(x, t)) a₂) → a₁ = a₂

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
ha : G.Adj s t
⊢ G.incidenceFinset t ⊆ G.edgeFinset

Tactic:
simp [incidenceFinset, incidenceSet_subset]

Premises used: SimpleGraph.incidenceFinset, SimpleGraph.incidenceSet_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
ha : G.Adj s t
⊢ G.incidenceFinset t ⊆ G.edgeFinset

Tactic:
have inc : G.incidenceFinset t ⊆ G.edgeFinset := by simp [incidenceFinset, incidenceSet_subset]
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ {s(t, t)} ⊆ G.edgeFinset \ G.incidenceFinset t ∪ image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)

Tactic:
simp [ha]
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
rw :
  #G.edgeFinset + card (α := Sym2 V) (image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)) - G.degree t -
      card (α := Sym2 V) {s(t, t)} =
    #G.edgeFinset + G.degree s - G.degree t - 1
⊢ #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t - 1

Tactic:
rw [G.edgeFinset_replaceVertex_of_adj ha, card_sdiff_of_subset (by simp [ha]),
    card_union_of_disjoint G.disjoint_sdiff_neighborFinset_image, card_sdiff_of_subset inc,
    ← Nat.sub_add_comm <| card_le_card inc, card_incidenceFinset_eq_degree]

Premises used: Finset.card_le_card, Finset.card_sdiff_of_subset, Nat.sub_add_comm, SimpleGraph.edgeFinset_replaceVertex_of_adj, SimpleGraph.card_incidenceFinset_eq_degree, SimpleGraph.disjoint_sdiff_neighborFinset_image, Finset.card_union_of_disjoint
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
e_a :
  #G.edgeFinset + card (α := Sym2 V) (image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)) = #G.edgeFinset + G.degree s
⊢ #G.edgeFinset + card (α := Sym2 V) (image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)) - G.degree t -
      card (α := Sym2 V) {s(t, t)} =
    #G.edgeFinset + G.degree s - G.degree t - 1

Tactic:
congr 2
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
e_a : Function.Injective (β := Sym2 V) fun (x : V) ↦ s(x, t)
⊢ #G.edgeFinset + card (α := Sym2 V) (image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)) = #G.edgeFinset + G.degree s

Tactic:
rw [card_image_of_injective, card_neighborFinset_eq_degree]

Premises used: Finset.card_image_of_injective, SimpleGraph.card_neighborFinset_eq_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ ∀ ⦃a₁ a₂ : V⦄, Eq.{u_1 + 1} (α := Sym2 V) ((fun (x : V) ↦ s(x, t)) a₁) ((fun (x : V) ↦ s(x, t)) a₂) → a₁ = a₂

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
s t v w : V
rw : Adj (fromEdgeSet {s(s, t)}) v w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
rw₁ : Membership.mem (γ := Set (Sym2 V)) {s(s, t)} s(v, w) ∧ v ≠ w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
rw₂ : s(v, w) = s(s, t) ∧ v ≠ w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
rw₃ rw₄ : (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
⊢ (edge s t).Adj v w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w

Tactic:
rw [edge, fromEdgeSet_adj, Set.mem_singleton_iff, Sym2.eq_iff]

Premises used: SimpleGraph.edge, SimpleGraph.fromEdgeSet_adj, Set.mem_singleton_iff, Sym2.eq_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
s t v w : V
simp : ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
⊢ (edge s t).Adj v w ↔ s(s, t) = s(v, w) ∧ v ≠ w

Tactic:
simp only [edge_adj, ne_eq, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk,
    and_congr_left_iff]

Premises used: Sym2.eq, Prod.swap_prod_mk, ne_eq, Sym2.rel_iff', SimpleGraph.edge_adj, Prod.mk.injEq, and_congr_left_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
s t : V
rw : fromEdgeSet {s(s, t)} = edge t s
rw₁ : Eq (α := SimpleGraph V) (fromEdgeSet {s(s, t)}) (fromEdgeSet {s(t, s)})
rw₂ rw₃ : Eq (α := SimpleGraph V) (fromEdgeSet {s(t, s)}) (fromEdgeSet {s(t, s)})
⊢ edge s t = edge t s

Tactic:
rw [edge, edge, Sym2.eq_swap]

Premises used: SimpleGraph.edge, Sym2.eq_swap
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
⊢ edge s t ≤ G ↔ {s(s, t)} \ Sym2.diagSet ⊆ G.edgeSet

Tactic:
simp [edge]

Premises used: SimpleGraph.edge
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
x x_1 : V
rw : Decidable ((x = s ∧ x_1 = t ∨ x = t ∧ x_1 = s) ∧ x ≠ x_1)
⊢ Decidable ((edge s t).Adj x x_1)

Tactic:
rw [edge_adj]

Premises used: SimpleGraph.edge_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
x x_1 : V
⊢ Decidable ((x = s ∧ x_1 = t ∨ x = t ∧ x_1 = s) ∧ x ≠ x_1)

Tactic:
infer_instance
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
s : V
Adj : ∀ (x x_1 : V), (edge s s).Adj x x_1 ↔ SimpleGraph.Adj ⊥ x x_1
⊢ edge s s = ⊥

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
s x x_1 : V
Adj : (x = s ∧ x_1 = s ∨ x = s ∧ x_1 = s) ∧ x ≠ x_1 ↔ SimpleGraph.Adj ⊥ x x_1
⊢ (edge s s).Adj x x_1 ↔ SimpleGraph.Adj ⊥ x x_1

Tactic:
rw [edge_adj]

Premises used: SimpleGraph.edge_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
s x x_1 : V
⊢ (x = s ∧ x_1 = s ∨ x = s ∧ x_1 = s) ∧ x ≠ x_1 ↔ Adj ⊥ x x_1

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s : V
⊢ G ⊔ edge s s = G

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
hne : s ≠ t
hn : ¬G.Adj s t
⊢ G < G ⊔ edge s t

Tactic:
left_lt_sup.2 fun h ↦ hn <| h <| (edge_adj ..).mpr ⟨Or.inl ⟨rfl, rfl⟩, hne⟩

Premises used: Iff.mpr, left_lt_sup, SimpleGraph.edge_adj, And.intro, Or.inl, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
inl : ∀ (h : v = w), edge v w ≤ G ↔ v = w ∨ G.Adj v w
inr : ∀ (h : v ≠ w), edge v w ≤ G ↔ v = w ∨ G.Adj v w
⊢ edge v w ≤ G ↔ v = w ∨ G.Adj v w

Tactic:
obtain h | h := eq_or_ne v w

Premises used: eq_or_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : v = w
⊢ edge v w ≤ G ↔ v = w ∨ G.Adj v w

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h_1 : v ≠ w
h : edge v w ≤ G
⊢ (edge v w).Adj v w

Tactic:
simp_all [edge_adj]

Premises used: SimpleGraph.edge_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : v ≠ w
inr : ∀ (hadj : v = w ∨ G.Adj v w) (v' w' : V) (hvw' : (edge v w).Adj v' w'), G.Adj v' w'
⊢ edge v w ≤ G ↔ v = w ∨ G.Adj v w

Tactic:
refine ⟨fun h ↦ .inr <| h (by simp_all [edge_adj]), fun hadj v' w' hvw' ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : v ≠ w
hadj : v = w ∨ G.Adj v w
v' w' : V
hvw' : (edge v w).Adj v' w'
⊢ G.Adj v' w'

Tactic:
aesop (add simp [edge_adj, adj_symm])

Premises used: SimpleGraph.edge_adj, SimpleGraph.adj_symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
v w : V
⊢ (edge v w).edgeSet = {s(v, w)} \ Sym2.diagSet

Tactic:
simp [edge]

Premises used: SimpleGraph.edge
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
v w : V
⊢ (edge v w).edgeSet ⊆ {s(v, w)}

Tactic:
simp [edge]

Premises used: SimpleGraph.edge
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
s t : V
h : s ≠ t
⊢ (edge s t).edgeSet = {s(s, t)}

Tactic:
simpa [edge]

Premises used: SimpleGraph.edge
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
h : G.Adj s t
rwa : edge s t ≤ G
rwa₁ : (edge s t).edgeSet ⊆ G.edgeSet
rwa₂ : {s(s, t)} ⊆ G.edgeSet
rwa₃ : s(s, t) ∈ G.edgeSet
rwa₄ rwa₅ rwa₆ rwa₇ : G.Adj s t
⊢ G ⊔ edge s t = G

Tactic:
rwa [sup_eq_left, ← edgeSet_subset_edgeSet, edgeSet_edge_of_ne h.ne, Set.singleton_subset_iff,
    mem_edgeSet]

Premises used: Set.singleton_subset_iff, SimpleGraph.edgeSet_edge_of_ne, SimpleGraph.Adj.ne, SimpleGraph.edgeSet_subset_edgeSet, sup_eq_left, SimpleGraph.mem_edgeSet