awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
u v : V
h : u ≠ v
⊢ dist ⊤ u v = 1

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
u v : V
inst : DecidableEq V
pos : ∀ (h : u = v), dist ⊤ u v = if u = v then 0 else 1
neg : ∀ (h : ¬u = v), dist ⊤ u v = if u = v then 0 else 1
⊢ dist ⊤ u v = if u = v then 0 else 1

Tactic:
by_cases h : u = v
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
u v : V
inst : DecidableEq V
h : u = v
⊢ dist ⊤ u v = if u = v then 0 else 1

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
u v : V
inst : DecidableEq V
h : ¬u = v
⊢ dist ⊤ u v = if u = v then 0 else 1

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
h₁ : p₁.length = G.dist u v
h₂ : p₂.IsSubwalk p₁
⊢ p₂.length = G.dist u' v'

Tactic:
(dist_le _).eq_of_not_lt' fun hh ↦ ?_

Premises used: LE.le.eq_of_not_lt', SimpleGraph.dist_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
h₁ : p₁.length = G.dist u v
h₂ : p₂.IsSubwalk p₁
refine : ∀ (hh : G.dist u' v' < p₂.length), False
⊢ p₂.length = G.dist u' v'

Tactic:
refine (dist_le _).eq_of_not_lt' fun hh ↦ ?_

Premises used: LE.le.eq_of_not_lt', SimpleGraph.dist_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
h₁ : p₁.length = G.dist u v
h₂ : p₂.IsSubwalk p₁
hh : G.dist u' v' < p₂.length
obtain : ∀ (ru : G.Walk u u') (rv : G.Walk v' v) (h : p₁ = (ru.append p₂).append rv), False
⊢ False

Tactic:
obtain ⟨ru, rv, h⟩ := h₂
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
h₁ : p₁.length = G.dist u v
hh : G.dist u' v' < p₂.length
ru : G.Walk u u'
rv : G.Walk v' v
h : p₁ = (ru.append p₂).append rv
obtain : ∀ (s : G.Walk u' v'), s.IsPath ∧ s.length = G.dist u' v' → False
⊢ False

Tactic:
obtain ⟨s, _⟩ := p₂.reachable.exists_path_of_dist

Premises used: SimpleGraph.Walk.reachable, SimpleGraph.Reachable.exists_path_of_dist
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
h₁ : p₁.length = G.dist u v
hh : G.dist u' v' < p₂.length
ru : G.Walk u u'
rv : G.Walk v' v
h : p₁ = (ru.append p₂).append rv
s : G.Walk u' v'
h_1 : s.IsPath ∧ s.length = G.dist u' v'
r : G.Walk u v := (ru.append s).append rv
⊢ p₁.length = ru.length + p₂.length + rv.length

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
h₁ : p₁.length = G.dist u v
hh : G.dist u' v' < p₂.length
ru : G.Walk u u'
rv : G.Walk v' v
h : p₁ = (ru.append p₂).append rv
s : G.Walk u' v'
h_1 : s.IsPath ∧ s.length = G.dist u' v'
r : G.Walk u v := (ru.append s).append rv
⊢ p₁.length = ru.length + p₂.length + rv.length

Tactic:
have : p₁.length = ru.length + p₂.length + rv.length := by simp [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
h₁ : p₁.length = G.dist u v
hh : G.dist u' v' < p₂.length
ru : G.Walk u u'
rv : G.Walk v' v
h : p₁ = (ru.append p₂).append rv
s : G.Walk u' v'
h_1 : s.IsPath ∧ s.length = G.dist u' v'
r : G.Walk u v := (ru.append s).append rv
this : p₁.length = ru.length + p₂.length + rv.length
⊢ r.length = ru.length + s.length + rv.length

Tactic:
simp [r]
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
h₁ : p₁.length = G.dist u v
hh : G.dist u' v' < p₂.length
ru : G.Walk u u'
rv : G.Walk v' v
h : p₁ = (ru.append p₂).append rv
s : G.Walk u' v'
h_1 : s.IsPath ∧ s.length = G.dist u' v'
r : G.Walk u v := (ru.append s).append rv
this : p₁.length = ru.length + p₂.length + rv.length
⊢ r.length = ru.length + s.length + rv.length

Tactic:
have : r.length = ru.length + s.length + rv.length := by simp [r]
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
h₁ : p₁.length = G.dist u v
hh : G.dist u' v' < p₂.length
ru : G.Walk u u'
rv : G.Walk v' v
h : p₁ = (ru.append p₂).append rv
s : G.Walk u' v'
h_1 : s.IsPath ∧ s.length = G.dist u' v'
r : G.Walk u v := (ru.append s).append rv
this_1 : p₁.length = ru.length + p₂.length + rv.length
this : r.length = ru.length + s.length + rv.length
⊢ G.dist u v ≤ r.length

Tactic:
have := dist_le r
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
h₁ : p₁.length = G.dist u v
hh : G.dist u' v' < p₂.length
ru : G.Walk u u'
rv : G.Walk v' v
h : p₁ = (ru.append p₂).append rv
s : G.Walk u' v'
h_1 : s.IsPath ∧ s.length = G.dist u' v'
r : G.Walk u v := (ru.append s).append rv
this_1 : p₁.length = ru.length + p₂.length + rv.length
this_2 : r.length = ru.length + s.length + rv.length
this : G.dist u v ≤ r.length
⊢ False

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
obtain : ∀ (w : G.Walk u v) (hw : w.length = G.dist u v), G'.dist u v ≤ G.dist u v
⊢ G'.dist u v ≤ G.dist u v

Tactic:
obtain ⟨_, hw⟩ := hr.exists_walk_length_eq_dist

Premises used: SimpleGraph.Reachable.exists_walk_length_eq_dist
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w : G.Walk u v
hw : w.length = G.dist u v
rw : G'.dist u v ≤ (Walk.map (Hom.ofLE h) w).length
⊢ G'.dist u v ≤ G.dist u v

Tactic:
rw [← hw, ← Walk.length_map (.ofLE h)]

Premises used: SimpleGraph.Walk.length_map, SimpleGraph.Hom.ofLE
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w : G.Walk u v
hw : w.length = G.dist u v
⊢ G'.dist u v ≤ (Walk.map (Hom.ofLE h) w).length

Tactic:
apply dist_le

Premises used: SimpleGraph.dist_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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
h : G.Adj v (p.getVert 1) ∧ G.Adj (p.getVert 1) (p.getVert 2) ∧ ¬G.Adj v (p.getVert 2) ∧ v ≠ p.getVert 2
⊢ ∃ (x : V) (a : V) (b : V), G.Adj x a ∧ G.Adj a b ∧ ¬G.Adj x b ∧ x ≠ b

Tactic:
use v, p.getVert 1, p.getVert 2

Premises used: OfNat.ofNat, SimpleGraph.Walk.getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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
⊢ ¬p.Nil

Tactic:
grind [Nil.length_eq_zero]

Premises used: SimpleGraph.Walk.Nil.length_eq_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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
⊢ ¬p.Nil

Tactic:
have hnp : ¬p.Nil := by grind [Nil.length_eq_zero]
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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
simp : ∀ (hp : p.tail.length + 1 = G.dist v w), 0 < p.tail.length
⊢ ¬p.tail.Nil

Tactic:
simp only [not_nil_iff_lt_length, ← p.length_tail_add_one hnp] at hp ⊢

Premises used: SimpleGraph.Walk.length_tail_add_one, SimpleGraph.Walk.not_nil_iff_lt_length
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
p : G.Walk v w
hl : 1 < G.dist v w
hnp : ¬p.Nil
hp : p.tail.length + 1 = G.dist v w
⊢ 0 < p.tail.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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
rw : p.tail.tail.length < p.tail.tail.length + 1
⊢ p.tail.tail.length < p.tail.length

Tactic:
rw [← p.tail.length_tail_add_one (by
      simp only [not_nil_iff_lt_length, ← p.length_tail_add_one hnp] at hp ⊢
      lia)]

Premises used: SimpleGraph.Walk.length_tail_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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
⊢ p.tail.tail.length < p.tail.tail.length + 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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
⊢ p.tail.tail.length < p.tail.length

Tactic:
have : p.tail.tail.length < p.tail.length := by
    rw [← p.tail.length_tail_add_one (by
      simp only [not_nil_iff_lt_length, ← p.length_tail_add_one hnp] at hp ⊢
      lia)]
    lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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 : p.tail.tail.length < p.tail.length
rw : p.tail.length < p.tail.length + 1
⊢ p.tail.length < p.length

Tactic:
rw [← p.length_tail_add_one hnp]

Premises used: SimpleGraph.Walk.length_tail_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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 : p.tail.tail.length < p.tail.length
⊢ p.tail.length < p.tail.length + 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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 : p.tail.tail.length < p.tail.length
⊢ p.tail.length < p.length

Tactic:
have : p.tail.length < p.length := by rw [← p.length_tail_add_one hnp]; lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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
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
⊢ 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

Premises used: OfNat.ofNat, SimpleGraph.Walk.getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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.dist v w ≤ p.tail.tail.length

Tactic:
simpa [hv, p.getVert_tail] using dist_le p.tail.tail

Premises used: SimpleGraph.Walk.getVert_tail, SimpleGraph.dist_le, SimpleGraph.Walk.tail
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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.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
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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_2 : p.tail.length < p.length
hv : v = p.getVert 2
this : G.dist v w ≤ p.tail.tail.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

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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
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
⊢ 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)

Premises used: SimpleGraph.Adj, OfNat.ofNat, SimpleGraph.Walk.getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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.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
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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_2 : p.tail.length < p.length
hv : ¬v = p.getVert 2
hadj : G.Adj v (p.getVert 2)
this : G.dist v w ≤ p.tail.tail.length + 1
⊢ 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:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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

Tactic:
⟨p.adj_snd hnp, p.adj_getVert_succ (hp ▸ hl), hadj, hv⟩

Premises used: Eq.rec, SimpleGraph.Walk.adj_getVert_succ, And.intro, Eq.symm, SimpleGraph.Walk.adj_snd
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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

Tactic:
exact ⟨p.adj_snd hnp, p.adj_getVert_succ (hp ▸ hl), hadj, hv⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
c v : V
r : ℕ∞
⊢ v ∈ G.ball c r ↔ G.edist v c < r

Tactic:
.rfl

Premises used: SimpleGraph.ball, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
c : V
⊢ G.ball c 0 = ∅

Tactic:
simp [ball]

Premises used: SimpleGraph.ball
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
c : V
⊢ G.ball c 1 = {c}

Tactic:
simp [ball, ENat.lt_one_iff_eq_zero]

Premises used: SimpleGraph.ball, ENat.lt_one_iff_eq_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
c : V
h : ∀ (v : V), v ∈ G.ball c 2 ↔ v ∈ insert c (G.neighborSet c)
⊢ G.ball c 2 = insert c (G.neighborSet c)

Tactic:
ext v
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
c v : V
⊢ v ∈ G.ball c 2 ↔ v ∈ insert c (G.neighborSet c)

Tactic:
simp [one_add_one_eq_two.symm, ENat.lt_add_one_iff ENat.one_ne_top,
    edist_le_one_iff_adj_or_eq, adj_comm, or_comm]

Premises used: ENat.one_ne_top, one_add_one_eq_two, ENat.lt_add_one_iff, or_comm, Eq.symm, SimpleGraph.adj_comm, SimpleGraph.edist_le_one_iff_adj_or_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
c : V
⊢ G.ball c ⊤ = (G.connectedComponentMk c).supp

Tactic:
simp [Set.ext_iff, lt_top_iff_ne_top, edist_ne_top_iff_reachable]

Premises used: SimpleGraph.edist_ne_top_iff_reachable, lt_top_iff_ne_top, Set.ext_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
c v : V
⊢ v ∈ G.ball c ⊤ ↔ G.Reachable v c

Tactic:
simp [lt_top_iff_ne_top, edist_ne_top_iff_reachable]

Premises used: SimpleGraph.edist_ne_top_iff_reachable, lt_top_iff_ne_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
c : V
r₁ r₂ : ℕ∞
h : r₁ ≤ r₂
⊢ G.ball c r₁ ⊆ G.ball c r₂

Tactic:
fun _ hv ↦ lt_of_lt_of_le hv h

Premises used: SimpleGraph.ball, Set.Mem, setOf, Set.Subset, lt_of_lt_of_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
c : V
r : ℕ∞
hr : 0 < r
⊢ c ∈ G.ball c r

Tactic:
simp [ball, hr]

Premises used: SimpleGraph.ball
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
c v : V
r : ℕ∞
⊢ v ∈ G.ball c r ↔ c ∈ G.ball v r

Tactic:
simp [ball, edist_comm]

Premises used: SimpleGraph.ball, SimpleGraph.edist_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
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
neg₁ : ¬v = t → ¬w = t → G.Adj v w → G.Adj 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

Tactic:
split_ifs
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
v w : V
h : v = t
h_1 : w = t
⊢ False → False

Tactic:
simp [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
v w : V
h : v = t
h_1 : ¬w = t
⊢ G.Adj s w → G.Adj w s

Tactic:
simp [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
v w : V
h : ¬v = t
h_1 : w = t
⊢ G.Adj v s → G.Adj s v

Tactic:
simp [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
v w : V
h : ¬v = t
h_1 : ¬w = t
⊢ G.Adj v w → G.Adj w v

Tactic:
simp [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
⊢ ¬(G.replaceVertex s t).Adj s t

Tactic:
simp [replaceVertex]

Premises used: SimpleGraph.replaceVertex
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s : V
inst : DecidableEq V
Adj : ∀ (x x_1 : V), (G.replaceVertex s s).Adj x x_1 ↔ G.Adj x x_1
⊢ G.replaceVertex s s = G

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s : V
inst : DecidableEq V
x x_1 : V
⊢ { Adj := fun (v w : V) ↦ if v = s then if w = s then False else G.Adj s w else if w = s then G.Adj v s else G.Adj v w,
          symm := ⋯, loopless := ⋯ : SimpleGraph V }.Adj
      x x_1 ↔
    G.Adj x x_1

Tactic:
aesop (add simp or_iff_not_imp_left)

Premises used: Classical.or_iff_not_imp_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
w : V
hw : w ≠ t
⊢ (G.replaceVertex s t).Adj s w ↔ G.Adj s w

Tactic:
simp [replaceVertex, hw]

Premises used: SimpleGraph.replaceVertex
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
w : V
hw : w ≠ t
⊢ (G.replaceVertex s t).Adj t w ↔ G.Adj s w

Tactic:
simp [replaceVertex, hw]

Premises used: SimpleGraph.replaceVertex
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
v w : V
hv : v ≠ t
hw : w ≠ t
⊢ (G.replaceVertex s t).Adj v w ↔ G.Adj v w

Tactic:
simp [replaceVertex, hv, hw]

Premises used: SimpleGraph.replaceVertex
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : DecidableEq V
hn : ¬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
⊢ (G.replaceVertex s t).edgeSet = G.edgeSet \ G.incidenceSet t ∪ (fun (x : V) ↦ s(x, t)) '' G.neighborSet s

Tactic:
ext e
-- 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
⊢ e ∈ (G.replaceVertex s t).edgeSet ↔ e ∈ G.edgeSet \ G.incidenceSet t ∪ (fun (x : V) ↦ s(x, t)) '' G.neighborSet s

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
hn : ¬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
⊢ e ∈ (G.replaceVertex s t).edgeSet ↔ e ∈ G.edgeSet \ G.incidenceSet t ∪ (fun (x : V) ↦ s(x, t)) '' G.neighborSet s

Tactic:
refine e.inductionOn ?_
-- 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
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)
⊢ ∀ (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:
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
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))
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))
⊢ (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:
split_ifs
-- 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
⊢ 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:
simp_all
-- 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 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:
aesop