awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.length = G.dist v w
hl : 1 < G.dist v w
hnp : ¬p.Nil
this_1 : p.tail.tail.length < p.tail.length
this : p.tail.length < p.length
⊢ G.Adj v (p.getVert 1) ∧ G.Adj (p.getVert 1) (p.getVert 2) ∧ ¬G.Adj v (p.getVert 2) ∧ v ≠ p.getVert 2
have pos : ∀ (hv : v = p.getVert 2),
  G.Adj v (p.getVert 1) ∧ G.Adj (p.getVert 1) (p.getVert 2) ∧ ¬G.Adj v (p.getVert 2) ∧ v ≠ p.getVert 2
Tactic: by_cases hv : v = p.getVert 2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.length = G.dist v w
hl : 1 < G.dist v w
hnp : ¬p.Nil
this_1 : p.tail.tail.length < p.tail.length
this : p.tail.length < p.length
pos :
  ∀ (hv : v = p.getVert 2),
    G.Adj v (p.getVert 1) ∧ G.Adj (p.getVert 1) (p.getVert 2) ∧ ¬G.Adj v (p.getVert 2) ∧ v ≠ p.getVert 2
⊢ G.Adj v (p.getVert 1) ∧ G.Adj (p.getVert 1) (p.getVert 2) ∧ ¬G.Adj v (p.getVert 2) ∧ v ≠ p.getVert 2
have neg : ∀ (hv : ¬v = p.getVert 2),
  G.Adj v (p.getVert 1) ∧ G.Adj (p.getVert 1) (p.getVert 2) ∧ ¬G.Adj v (p.getVert 2) ∧ v ≠ p.getVert 2
Tactic: by_cases hv : v = p.getVert 2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.length = G.dist v w
hl : 1 < G.dist v w
hnp : ¬p.Nil
this_1 : p.tail.tail.length < p.tail.length
this : p.tail.length < p.length
hv : v = p.getVert 2
⊢ G.Adj v (p.getVert 1) ∧ G.Adj (p.getVert 1) (p.getVert 2) ∧ ¬G.Adj v (p.getVert 2) ∧ v ≠ p.getVert 2
have this₁ : G.dist v w ≤ p.tail.tail.length
Tactic: have : G.dist v w ≤ p.tail.tail.length := by
      simpa [hv, p.getVert_tail] using dist_le p.tail.tail
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.length = G.dist v w
hl : 1 < G.dist v w
hnp : ¬p.Nil
this_1 : p.tail.tail.length < p.tail.length
this : p.tail.length < p.length
hv : ¬v = p.getVert 2
⊢ G.Adj v (p.getVert 1) ∧ G.Adj (p.getVert 1) (p.getVert 2) ∧ ¬G.Adj v (p.getVert 2) ∧ v ≠ p.getVert 2
have pos : ∀ (hadj : G.Adj v (p.getVert 2)),
  G.Adj v (p.getVert 1) ∧ G.Adj (p.getVert 1) (p.getVert 2) ∧ ¬G.Adj v (p.getVert 2) ∧ v ≠ p.getVert 2
Tactic: by_cases hadj : G.Adj v (p.getVert 2)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.length = G.dist v w
hl : 1 < G.dist v w
hnp : ¬p.Nil
this_1 : p.tail.tail.length < p.tail.length
this : p.tail.length < p.length
hv : ¬v = p.getVert 2
pos :
  ∀ (hadj : G.Adj v (p.getVert 2)),
    G.Adj v (p.getVert 1) ∧ G.Adj (p.getVert 1) (p.getVert 2) ∧ ¬G.Adj v (p.getVert 2) ∧ v ≠ p.getVert 2
⊢ G.Adj v (p.getVert 1) ∧ G.Adj (p.getVert 1) (p.getVert 2) ∧ ¬G.Adj v (p.getVert 2) ∧ v ≠ p.getVert 2
have neg : ∀ (hadj : ¬G.Adj v (p.getVert 2)),
  G.Adj v (p.getVert 1) ∧ G.Adj (p.getVert 1) (p.getVert 2) ∧ ¬G.Adj v (p.getVert 2) ∧ v ≠ p.getVert 2
Tactic: by_cases hadj : G.Adj v (p.getVert 2)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.length = G.dist v w
hl : 1 < G.dist v w
hnp : ¬p.Nil
this_1 : p.tail.tail.length < p.tail.length
this : p.tail.length < p.length
hv : ¬v = p.getVert 2
hadj : G.Adj v (p.getVert 2)
⊢ G.Adj v (p.getVert 1) ∧ G.Adj (p.getVert 1) (p.getVert 2) ∧ ¬G.Adj v (p.getVert 2) ∧ v ≠ p.getVert 2
have this₁ : G.dist v w ≤ p.tail.tail.length + 1
Tactic: have : G.dist v w ≤ p.tail.tail.length + 1 :=
      dist_le <| p.tail.tail.cons <| p.getVert_tail ▸ hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
c : V
⊢ G.ball c 2 = insert c (G.neighborSet c)
have h : ∀ (v : V), v ∈ G.ball c 2 ↔ v ∈ insert c (G.neighborSet c)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
v w : V
⊢ (if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w) →
    if w = t then if v = t then False else G.Adj s v else if v = t then G.Adj w s else G.Adj w v
have pos : v = t → w = t → False → False
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
v w : V
pos : v = t → w = t → False → False
⊢ (if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w) →
    if w = t then if v = t then False else G.Adj s v else if v = t then G.Adj w s else G.Adj w v
have neg : v = t → ¬w = t → G.Adj s w → G.Adj w s
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
v w : V
pos : v = t → w = t → False → False
neg : v = t → ¬w = t → G.Adj s w → G.Adj w s
⊢ (if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w) →
    if w = t then if v = t then False else G.Adj s v else if v = t then G.Adj w s else G.Adj w v
have pos₁ : ¬v = t → w = t → G.Adj v s → G.Adj s v
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
v w : V
pos : v = t → w = t → False → False
neg : v = t → ¬w = t → G.Adj s w → G.Adj w s
pos₁ : ¬v = t → w = t → G.Adj v s → G.Adj s v
⊢ (if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w) →
    if w = t then if v = t then False else G.Adj s v else if v = t then G.Adj w s else G.Adj w v
have neg₁ : ¬v = t → ¬w = t → G.Adj v w → G.Adj w v
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s : V
inst : DecidableEq V
⊢ G.replaceVertex s s = G
have Adj : ∀ (x x_1 : V), (G.replaceVertex s s).Adj x x_1 ↔ G.Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
hn : ¬G.Adj s t
⊢ (G.replaceVertex s t).edgeSet = G.edgeSet \ G.incidenceSet t ∪ (fun (x : V) ↦ s(x, t)) '' G.neighborSet s
have 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
Tactic: ext e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
hn : ¬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
have 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
Tactic: refine e.inductionOn ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
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),
    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
have 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)
Tactic: simp only [replaceVertex, mem_edgeSet, Set.mem_union, Set.mem_diff, mk'_mem_incidenceSet_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
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
⊢ (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)
have pos : x = t →
  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))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
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
pos :
  x = t →
    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))
⊢ (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)
have neg : x = t →
  ¬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))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
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
pos :
  x = t →
    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))
neg :
  x = t →
    ¬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))
⊢ (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)
have pos₁ : ¬x = t →
  y = 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))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
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
pos :
  x = t →
    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))
neg :
  x = t →
    ¬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))
pos₁ :
  ¬x = t →
    y = 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))
⊢ (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)
have neg₁ : ¬x = t →
  ¬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: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
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 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)
have 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)
Tactic: rw [adj_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
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)}
have 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)}
Tactic: ext e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
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)}
have 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)}
Tactic: refine e.inductionOn ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
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),
    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)}
have 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)}
Tactic: simp only [replaceVertex, mem_edgeSet, Set.mem_union, Set.mem_diff, mk'_mem_incidenceSet_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
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 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)}
have 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)}
Tactic: rw [adj_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
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).edgeFinset =
    G.edgeFinset \ G.incidenceFinset t ∪ image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)
have 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))
Tactic: apply Finset.coe_injective
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
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).edgeFinset : Set (Sym2 V)) =
    (↑(G.edgeFinset \ G.incidenceFinset t ∪ image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)) : Set (Sym2 V))
have a : (G.replaceVertex s t).edgeSet = G.edgeSet \ G.incidenceSet t ∪ (fun (x : V) ↦ s(x, t)) '' G.neighborSet s
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
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).edgeFinset =
    (G.edgeFinset \ G.incidenceFinset t ∪ image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)) \ {s(t, t)}
have 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))
Tactic: apply Finset.coe_injective
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
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).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))
have a : (G.replaceVertex s t).edgeSet = (G.edgeSet \ G.incidenceSet t ∪ (fun (x : V) ↦ s(x, t)) '' G.neighborSet s) \ {s(t, t)}
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
⊢ Disjoint (G.edgeFinset \ G.incidenceFinset t) (image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s))
have 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
Tactic: rw [disjoint_iff_ne]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (hypothesis)
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
have he₁ : e ∈ G.edgeFinset ∧ e ∉ G.incidenceSet t
Tactic: rw [mem_sdiff, mem_incidenceFinset] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (hypothesis)
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
⊢ t ∉ e
have left : e ∈ G.edgeFinset
Tactic: obtain ⟨_, h⟩ := he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (hypothesis)
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
⊢ t ∉ e
have h : e ∉ G.incidenceSet t
Tactic: obtain ⟨_, h⟩ := he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
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
⊢ t ∉ e
have contrapose : ∀ (h : t ∈ e), e ∈ G.incidenceSet t
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (hypothesis)
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
⊢ ∀ (b : Sym2 V), Membership.mem (γ := Finset (Sym2 V)) (image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)) b → e ≠ b
have this : t ∉ e
Tactic: have : t ∉ e := by
    rw [mem_sdiff, mem_incidenceFinset] at he
    obtain ⟨_, h⟩ := he
    contrapose h
    simp_all [incidenceSet]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (hypothesis)
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).edgeFinset = #G.edgeFinset + G.degree s - G.degree t
have inc : G.incidenceFinset t ⊆ G.edgeFinset
Tactic: have inc : G.incidenceFinset t ⊆ G.edgeFinset := by simp [incidenceFinset, incidenceSet_subset]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
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
⊢ #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t
have 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
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
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
⊢ #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
have e_a : card (α := Sym2 V) (image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)) = G.degree s
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
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
⊢ card (α := Sym2 V) (image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)) = G.degree s
have e_a : Function.Injective (β := Sym2 V) fun (x : V) ↦ s(x, t)
Tactic: rw [card_image_of_injective, card_neighborFinset_eq_degree]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (hypothesis)
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).edgeFinset = #G.edgeFinset + G.degree s - G.degree t - 1
have inc : G.incidenceFinset t ⊆ G.edgeFinset
Tactic: have inc : G.incidenceFinset t ⊆ G.edgeFinset := by simp [incidenceFinset, incidenceSet_subset]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
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
⊢ #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t - 1
have 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
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
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
⊢ #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
have e_a : #G.edgeFinset + card (α := Sym2 V) (image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)) = #G.edgeFinset + G.degree s
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
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
⊢ #G.edgeFinset + card (α := Sym2 V) (image (fun (x : V) ↦ s(x, t)) (G.neighborFinset s)) = #G.edgeFinset + G.degree s
have e_a : Function.Injective (β := Sym2 V) fun (x : V) ↦ s(x, t)
Tactic: rw [card_image_of_injective, card_neighborFinset_eq_degree]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
Goal:
V : Type u_1
s t v w : V
⊢ (edge s t).Adj v w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
have rw : Adj (fromEdgeSet {s(s, t)}) v w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
Tactic: rw [edge, fromEdgeSet_adj, Set.mem_singleton_iff, Sym2.eq_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Operations (goal)
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
⊢ (edge s t).Adj v w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
have rw₁ : Membership.mem (γ := Set (Sym2 V)) {s(s, t)} s(v, w) ∧ v ≠ w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
Tactic: rw [edge, fromEdgeSet_adj, Set.mem_singleton_iff, Sym2.eq_iff]