awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
refine_2 : 1 ≤ G.edist u v
refine_2₁ : 1 ≠ G.edist u v
⊢ HAdd.hAdd (α := ℕ∞) 1 1 ≤ G.edist u v

Tactic:
refine Order.add_one_le_of_lt <| lt_of_le_of_ne ?_ ?_

Premises used: Order.add_one_le_of_lt, lt_of_le_of_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
⊢ 1 ≤ G.edist u v

Tactic:
grind [Order.one_le_iff_pos, pos_iff_ne_zero, edist_eq_zero_iff, edist_eq_one_iff_adj]

Premises used: SimpleGraph.edist_eq_zero_iff, pos_iff_ne_zero, SimpleGraph.edist_eq_one_iff_adj, Order.one_le_iff_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
⊢ 1 ≠ G.edist u v

Tactic:
grind [Order.one_le_iff_pos, pos_iff_ne_zero, edist_eq_zero_iff, edist_eq_one_iff_adj]

Premises used: SimpleGraph.edist_eq_zero_iff, pos_iff_ne_zero, SimpleGraph.edist_eq_one_iff_adj, Order.one_le_iff_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
⊢ G.edist u v ≠ 2

Tactic:
simp_all [edist_eq_two_iff]

Premises used: SimpleGraph.edist_eq_two_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
u v : V
h : u ≠ v
rwa : ∀ (h : ¬u = v), edist ⊥ u v = ⊤
rwa₁ : ∀ (h : ¬Reachable ⊥ u v), edist ⊥ u v = ⊤
rwa₂ : ∀ (h : ¬edist ⊥ u v ≠ ⊤), edist ⊥ u v = ⊤
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (h : edist ⊥ u v = ⊤), edist ⊥ u v = ⊤
⊢ edist ⊥ u v = ⊤

Tactic:
rwa [ne_eq, ← reachable_bot.not, ← edist_ne_top_iff_reachable.not, not_not] at h

Premises used: Classical.not_not, SimpleGraph.edist_ne_top_iff_reachable, Iff.not, ne_eq, SimpleGraph.reachable_bot
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
u v : V
inst : DecidableEq V
pos : ∀ (h : u = v), edist ⊥ u v = if u = v then 0 else ⊤
neg : ∀ (h : ¬u = v), edist ⊥ u v = if u = v then 0 else ⊤
⊢ edist ⊥ u v = if u = v then 0 else ⊤

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
⊢ edist ⊥ u v = if u = v then 0 else ⊤

Tactic:
simp [h, edist_bot_of_ne]

Premises used: SimpleGraph.edist_bot_of_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
u v : V
inst : DecidableEq V
h : ¬u = v
⊢ edist ⊥ u v = if u = v then 0 else ⊤

Tactic:
simp [h, edist_bot_of_ne]

Premises used: SimpleGraph.edist_bot_of_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
u v : V
h : u ≠ v
⊢ edist ⊤ 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), edist ⊤ u v = if u = v then 0 else 1
neg : ∀ (h : ¬u = v), edist ⊤ u v = if u = v then 0 else 1
⊢ edist ⊤ 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
⊢ edist ⊤ 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
⊢ edist ⊤ 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 : V
G' : SimpleGraph V
h : G ≤ G'
pos : ∀ (hr : G.Reachable u v), G'.edist u v ≤ G.edist u v
neg : ∀ (hr : ¬G.Reachable u v), G'.edist u v ≤ G.edist u v
⊢ G'.edist u v ≤ G.edist u v

Tactic:
by_cases hr : G.Reachable u v

Premises used: SimpleGraph.Reachable
-- 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
pos : ∀ (w : G.Walk u v) (hw : (↑w.length : ℕ∞) = G.edist u v), G'.edist u v ≤ G.edist u v
⊢ G'.edist u v ≤ G.edist u v

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

Premises used: SimpleGraph.Reachable.exists_walk_length_eq_edist
-- 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.edist u v
pos : G'.edist u v ≤ (↑(Walk.map (Hom.ofLE h) w).length : ℕ∞)
⊢ G'.edist u v ≤ G.edist 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.edist u v
⊢ G'.edist u v ≤ (↑(Walk.map (Hom.ofLE h) w).length : ℕ∞)

Tactic:
apply edist_le

Premises used: SimpleGraph.edist_le
-- 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
⊢ G'.edist u v ≤ G.edist u v

Tactic:
edist_eq_top_of_not_reachable hr ▸ le_top

Premises used: SimpleGraph.edist_eq_top_of_not_reachable, Eq.rec, le_top, Eq.symm
-- 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
⊢ G'.edist u v ≤ G.edist u v

Tactic:
exact edist_eq_top_of_not_reachable hr ▸ le_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.dist u v = sInf (Set.range.{0, u_1 + 1} (ι := G.Walk u v) Walk.length)

Tactic:
ENat.iInf_toNat

Premises used: iInf, SimpleGraph.dist, ENat.iInf_toNat, Set.Mem, SimpleGraph.edist
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
⊢ (↑(G.dist u v) : ℕ∞) = G.edist u v

Tactic:
ENat.coe_toNat <| edist_ne_top_iff_reachable.mpr h

Premises used: Iff.mpr, SimpleGraph.dist, SimpleGraph.edist_ne_top_iff_reachable, ENat.coe_toNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
hr : G.Reachable u v
⊢ ∃ (p : G.Walk u v), p.length = G.dist u v

Tactic:
dist_eq_sInf ▸ Nat.sInf_mem (Set.range_nonempty_iff_nonempty.mpr hr)

Premises used: Iff.mpr, Set.range_nonempty_iff_nonempty, SimpleGraph.dist_eq_sInf, Nat.sInf_mem, Eq.rec, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u v : V
⊢ ∃ (p : G.Walk u v), p.length = G.dist u v

Tactic:
dist_eq_sInf ▸ (hconn u v).exists_walk_length_eq_dist

Premises used: SimpleGraph.Connected.preconnected, SimpleGraph.dist_eq_sInf, Eq.rec, SimpleGraph.Reachable.exists_walk_length_eq_dist, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ G.dist u v ≤ p.length

Tactic:
dist_eq_sInf ▸ Nat.sInf_le ⟨p, rfl⟩

Premises used: SimpleGraph.dist_eq_sInf, Eq.rec, Nat.sInf_le, Exists.intro, Eq.symm, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.dist u v = 0 ↔ u = v ∨ ¬G.Reachable u v

Tactic:
simp [dist_eq_sInf, Nat.sInf_eq_zero, Reachable]

Premises used: Nat.sInf_eq_zero, SimpleGraph.dist_eq_sInf, SimpleGraph.Reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
v : V
⊢ G.dist v v = 0

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
hr : G.Reachable u v
⊢ G.dist u v = 0 ↔ u = v

Tactic:
simp [hr]
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
hne : u ≠ v
⊢ G.dist u v ≠ 0

Tactic:
simp [h, hne]
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
hne : u ≠ v
hnadj : ¬G.Adj u v
by_contra : ∀ (hc : 1 = G.dist u v), False
⊢ ¬1 = G.dist u v

Tactic:
by_contra hc
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
hne : u ≠ v
hnadj : ¬G.Adj u v
hc : 1 = G.dist u v
obtain : ∀ (p : G.Walk u v) (hp : p.length = G.dist u v), False
⊢ False

Tactic:
obtain ⟨p, hp⟩ := Reachable.exists_walk_length_eq_dist h

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
h : G.Reachable u v
hne : u ≠ v
hnadj : ¬G.Adj u v
hc : 1 = G.dist u v
p : G.Walk u v
hp : p.length = G.dist u v
⊢ False

Tactic:
hnadj (Walk.exists_length_eq_one_iff.mp ⟨p, hc ▸ hp⟩)

Premises used: Eq.rec, Exists.intro, Iff.mp, Eq.symm, SimpleGraph.Walk.exists_length_eq_one_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
hne : u ≠ v
hnadj : ¬G.Adj u v
hc : 1 = G.dist u v
p : G.Walk u v
hp : p.length = G.dist u v
⊢ False

Tactic:
exact hnadj (Walk.exists_length_eq_one_iff.mp ⟨p, hc ▸ hp⟩)

Premises used: Eq.rec, Exists.intro, Iff.mp, Eq.symm, SimpleGraph.Walk.exists_length_eq_one_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
hconn : G.Connected
⊢ G.dist u v = 0 ↔ u = v

Tactic:
simp [hconn u v]

Premises used: SimpleGraph.Connected.preconnected
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
hconn : G.Connected
hne : u ≠ v
⊢ 0 < G.dist u v

Tactic:
Nat.pos_of_ne_zero fun h ↦ False.elim <| hne <| (hconn.dist_eq_zero_iff).mp h

Premises used: False.elim, Nat.pos_of_ne_zero, Iff.mp, SimpleGraph.Connected.dist_eq_zero_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Connected
hne : u ≠ v
hnadj : ¬G.Adj u v
⊢ 1 < G.dist u v

Tactic:
Reachable.one_lt_dist_of_ne_of_not_adj (h u v) hne hnadj

Premises used: SimpleGraph.Connected.preconnected, SimpleGraph.Reachable.one_lt_dist_of_ne_of_not_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : ¬G.Reachable u v
⊢ G.dist u v = 0

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : 0 < G.dist u v
⊢ 0 < sInf (Set.range.{0, u_1 + 1} (ι := G.Walk u v) Walk.length)

Tactic:
rw [dist_eq_sInf] at h

Premises used: SimpleGraph.dist_eq_sInf
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : 0 < sInf (Set.range.{0, u_1 + 1} (ι := G.Walk u v) Walk.length)
⊢ Set.Nonempty.{u_1} (α := G.Walk u v) Set.univ

Tactic:
simpa [Set.range_nonempty_iff_nonempty, Set.nonempty_iff_univ_nonempty] using
    Nat.nonempty_of_pos_sInf h

Premises used: Set.range_nonempty_iff_nonempty, Nat.nonempty_of_pos_sInf, Set.nonempty_iff_univ_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
hconn : G.Connected
obtain : ∀ (p : G.Walk u v) (hp : p.length = G.dist u v), G.dist u w ≤ G.dist u v + G.dist v w
⊢ G.dist u w ≤ G.dist u v + G.dist v w

Tactic:
obtain ⟨p, hp⟩ := hconn.exists_walk_length_eq_dist u v

Premises used: SimpleGraph.Connected.exists_walk_length_eq_dist
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
hconn : G.Connected
p : G.Walk u v
hp : p.length = G.dist u v
obtain : ∀ (q : G.Walk v w) (hq : q.length = G.dist v w), G.dist u w ≤ G.dist u v + G.dist v w
⊢ G.dist u w ≤ G.dist u v + G.dist v w

Tactic:
obtain ⟨q, hq⟩ := hconn.exists_walk_length_eq_dist v w

Premises used: SimpleGraph.Connected.exists_walk_length_eq_dist
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
hconn : G.Connected
p : G.Walk u v
hp : p.length = G.dist u v
q : G.Walk v w
hq : q.length = G.dist v w
rw : G.dist u w ≤ (p.append q).length
⊢ G.dist u w ≤ G.dist u v + G.dist v w

Tactic:
rw [← hp, ← hq, ← Walk.length_append]

Premises used: SimpleGraph.Walk.length_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
hconn : G.Connected
p : G.Walk u v
hp : p.length = G.dist u v
q : G.Walk v w
hq : q.length = G.dist v w
⊢ G.dist u w ≤ (p.append q).length

Tactic:
apply dist_le

Premises used: SimpleGraph.dist_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
w : V
pos : ∀ (h' : ¬G.Reachable u w), G.dist u w ≤ G.dist u v + G.dist v w
neg : ∀ (h' : G.Reachable u w), G.dist u w ≤ G.dist u v + G.dist v w
⊢ G.dist u w ≤ G.dist u v + G.dist v w

Tactic:
by_cases! h' : ¬G.Reachable u w

Premises used: SimpleGraph.Reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
w : V
h' : ¬G.Reachable u w
⊢ G.dist u w ≤ G.dist u v + G.dist v w

Tactic:
grind [dist_eq_zero_iff_eq_or_not_reachable]

Premises used: SimpleGraph.dist_eq_zero_iff_eq_or_not_reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
w : V
h' : G.Reachable u w
neg : (↑(G.dist u w) : ℕ∞) ≤ HAdd.hAdd (α := ℕ∞) (↑(G.dist u v) : ℕ∞) (↑(G.dist v w) : ℕ∞)
⊢ G.dist u w ≤ G.dist u v + G.dist v w

Tactic:
rw [← ENat.coe_le_coe, ENat.coe_add]

Premises used: ENat.coe_le_coe, ENat.coe_add
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
w : V
h' : G.Reachable u w
⊢ (↑(G.dist u w) : ℕ∞) ≤ HAdd.hAdd (α := ℕ∞) (↑(G.dist u v) : ℕ∞) (↑(G.dist v w) : ℕ∞)

Tactic:
grind [SimpleGraph.edist_triangle, Reachable.trans, Reachable.symm]

Premises used: SimpleGraph.Reachable.symm, SimpleGraph.Reachable.trans, SimpleGraph.edist_triangle
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Reachable v w
u : V
pos : ∀ (h' : ¬G.Reachable u w), G.dist u w ≤ G.dist u v + G.dist v w
neg : ∀ (h' : G.Reachable u w), G.dist u w ≤ G.dist u v + G.dist v w
⊢ G.dist u w ≤ G.dist u v + G.dist v w

Tactic:
by_cases! h' : ¬G.Reachable u w

Premises used: SimpleGraph.Reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Reachable v w
u : V
h' : ¬G.Reachable u w
⊢ G.dist u w ≤ G.dist u v + G.dist v w

Tactic:
grind [dist_eq_zero_iff_eq_or_not_reachable]

Premises used: SimpleGraph.dist_eq_zero_iff_eq_or_not_reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Reachable v w
u : V
h' : G.Reachable u w
neg : (↑(G.dist u w) : ℕ∞) ≤ HAdd.hAdd (α := ℕ∞) (↑(G.dist u v) : ℕ∞) (↑(G.dist v w) : ℕ∞)
⊢ G.dist u w ≤ G.dist u v + G.dist v w

Tactic:
rw [← ENat.coe_le_coe, ENat.coe_add]

Premises used: ENat.coe_le_coe, ENat.coe_add
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Reachable v w
u : V
h' : G.Reachable u w
⊢ (↑(G.dist u w) : ℕ∞) ≤ HAdd.hAdd (α := ℕ∞) (↑(G.dist u v) : ℕ∞) (↑(G.dist v w) : ℕ∞)

Tactic:
grind [SimpleGraph.edist_triangle, Reachable.trans, Reachable.symm]

Premises used: SimpleGraph.Reachable.symm, SimpleGraph.Reachable.trans, SimpleGraph.edist_triangle
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
rw : (G.edist u v).toNat = G.dist v u
rw₁ : (G.edist u v).toNat = (G.edist v u).toNat
rw₂ rw₃ : (G.edist v u).toNat = (G.edist v u).toNat
⊢ G.dist u v = G.dist v u

Tactic:
rw [dist, dist, edist_comm]

Premises used: SimpleGraph.dist, SimpleGraph.edist_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.dist u v ≠ 0 ↔ u ≠ v ∧ G.Reachable u v

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.dist u v ≠ 0
⊢ G.Reachable u v

Tactic:
(dist_ne_zero_iff_ne_and_reachable.mp h).2

Premises used: SimpleGraph.dist_ne_zero_iff_ne_and_reachable, And.right, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.dist u v ≠ 0
⊢ ∃ (p : G.Walk u v), p.length = G.dist u v

Tactic:
(Reachable.of_dist_ne_zero h).exists_walk_length_eq_dist

Premises used: SimpleGraph.Reachable.exists_walk_length_eq_dist, SimpleGraph.Reachable.of_dist_ne_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
rw : Ne (α := ℕ) 1 0
⊢ G.dist u v = 1 ↔ G.Adj u v

Tactic:
rw [dist, ENat.toNat_eq_iff, ENat.coe_one, edist_eq_one_iff_adj]

Premises used: ENat.coe_one, SimpleGraph.dist, ENat.toNat_eq_iff, SimpleGraph.edist_eq_one_iff_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ Ne (α := ℕ) 1 0

Tactic:
decide
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
hadj : G.Adj v w
pos : ∀ (huw : ¬G.Reachable u w), G.dist u w = G.dist u v ∨ G.dist u w = G.dist u v + 1 ∨ G.dist u w = G.dist u v - 1
neg : ∀ (huw : G.Reachable u w), G.dist u w = G.dist u v ∨ G.dist u w = G.dist u v + 1 ∨ G.dist u w = G.dist u v - 1
⊢ G.dist u w = G.dist u v ∨ G.dist u w = G.dist u v + 1 ∨ G.dist u w = G.dist u v - 1

Tactic:
by_cases! huw : ¬G.Reachable u w

Premises used: SimpleGraph.Reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
hadj : G.Adj v w
huw : ¬G.Reachable u w
⊢ G.dist u w = G.dist u v ∨ G.dist u w = G.dist u v + 1 ∨ G.dist u w = G.dist u v - 1

Tactic:
grind [dist_eq_zero_iff_eq_or_not_reachable, Reachable.trans, Adj.reachable]

Premises used: SimpleGraph.Adj.reachable, SimpleGraph.Reachable.trans, SimpleGraph.dist_eq_zero_iff_eq_or_not_reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
hadj : G.Adj v w
huw : G.Reachable u w
⊢ G.dist v w = 1

Tactic:
have : G.dist v w = 1 := dist_eq_one_iff_adj.mpr hadj
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
hadj : G.Adj v w
huw : G.Reachable u w
this : G.dist v w = 1
⊢ G.dist w v = 1

Tactic:
have : G.dist w v = 1 := dist_eq_one_iff_adj.mpr hadj.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
hadj : G.Adj v w
huw : G.Reachable u w
this_1 : G.dist v w = 1
this : G.dist w v = 1
⊢ G.dist u w ≤ G.dist u v + G.dist v w

Tactic:
have : G.dist u w ≤ G.dist u v + G.dist v w := hadj.reachable.dist_triangle_right u
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
hadj : G.Adj v w
huw : G.Reachable u w
this_1 : G.dist v w = 1
this_2 : G.dist w v = 1
this : G.dist u w ≤ G.dist u v + G.dist v w
⊢ G.dist u v ≤ G.dist u w + G.dist w v

Tactic:
have : G.dist u v ≤ G.dist u w + G.dist w v := huw.dist_triangle_left v
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
hadj : G.Adj v w
huw : G.Reachable u w
this_1 : G.dist v w = 1
this_2 : G.dist w v = 1
this_3 : G.dist u w ≤ G.dist u v + G.dist v w
this : G.dist u v ≤ G.dist u w + G.dist w v
⊢ G.dist u w = G.dist u v ∨ G.dist u w = G.dist u v + 1 ∨ G.dist u w = G.dist u v - 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
h : G.Connected
hadj : G.Adj v w
⊢ G.dist u w = G.dist u v ∨ G.dist u w = G.dist u v + 1 ∨ G.dist u w = G.dist u v - 1

Tactic:
apply Adj.diff_dist_adj hadj

Premises used: SimpleGraph.Adj.diff_dist_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
h : p.length ≤ p.bypass.length
⊢ p.bypass = p

Tactic:
apply Walk.bypass_eq_self_of_length_le

Premises used: SimpleGraph.Walk.bypass_eq_self_of_length_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
⊢ p.length = G.dist u v

Tactic:
hp
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
⊢ G.dist u v ≤ p.bypass.length

Tactic:
dist_le p.bypass

Premises used: SimpleGraph.Walk.bypass, SimpleGraph.dist_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
⊢ p.length ≤ p.bypass.length

Tactic:
calc p.length
      _ = G.dist u v := hp
      _ ≤ p.bypass.length := dist_le p.bypass

Premises used: SimpleGraph.dist, SimpleGraph.Walk.length, SimpleGraph.Walk.bypass, SimpleGraph.dist_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
⊢ p.bypass = p

Tactic:
have : p.bypass = p := by
    apply Walk.bypass_eq_self_of_length_le
    calc p.length
      _ = G.dist u v := hp
      _ ≤ p.bypass.length := dist_le p.bypass
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
this : p.bypass = p
rw : p.bypass.IsPath
⊢ p.IsPath

Tactic:
rw [← this]
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
this : p.bypass = p
⊢ p.bypass.IsPath

Tactic:
apply Walk.bypass_isPath

Premises used: SimpleGraph.Walk.bypass_isPath
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
have : p.bypass = p
have₁ : ∀ (this : p.bypass = p), p.IsPath
have₂ : p.bypass = p
have₃ have₄ : ∀ (this : p.bypass = p), p.IsPath
have₅ : ∀ (this : p.bypass = p), p.bypass.IsPath
⊢ p.IsPath

Tactic:
classical
  have : p.bypass = p := by
    apply Walk.bypass_eq_self_of_length_le
    calc p.length
      _ = G.dist u v := hp
      _ ≤ p.bypass.length := dist_le p.bypass
  rw [← this]
  apply Walk.bypass_isPath

Premises used: SimpleGraph.Walk.bypass_isPath
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
hr : G.Reachable u v
obtain : ∀ (p : G.Walk u v) (h : p.length = G.dist u v), ∃ (p : G.Walk u v), p.IsPath ∧ p.length = G.dist u v
⊢ ∃ (p : G.Walk u v), p.IsPath ∧ p.length = G.dist u v

Tactic:
obtain ⟨p, h⟩ := 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
hr : G.Reachable u v
p : G.Walk u v
h : p.length = G.dist u v
⊢ ∃ (p : G.Walk u v), p.IsPath ∧ p.length = G.dist u v

Tactic:
⟨p, p.isPath_of_length_eq_dist h, h⟩

Premises used: SimpleGraph.Walk.isPath_of_length_eq_dist, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
hr : G.Reachable u v
p : G.Walk u v
h : p.length = G.dist u v
⊢ ∃ (p : G.Walk u v), p.IsPath ∧ p.length = G.dist u v

Tactic:
exact ⟨p, p.isPath_of_length_eq_dist h, h⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u v : V
obtain : ∀ (p : G.Walk u v) (h : p.length = G.dist u v), ∃ (p : G.Walk u v), p.IsPath ∧ p.length = G.dist u v
⊢ ∃ (p : G.Walk u v), p.IsPath ∧ p.length = G.dist u v

Tactic:
obtain ⟨p, h⟩ := hconn.exists_walk_length_eq_dist u v

Premises used: SimpleGraph.Connected.exists_walk_length_eq_dist
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u v : V
p : G.Walk u v
h : p.length = G.dist u v
⊢ ∃ (p : G.Walk u v), p.IsPath ∧ p.length = G.dist u v

Tactic:
⟨p, p.isPath_of_length_eq_dist h, h⟩

Premises used: SimpleGraph.Walk.isPath_of_length_eq_dist, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u v : V
p : G.Walk u v
h : p.length = G.dist u v
⊢ ∃ (p : G.Walk u v), p.IsPath ∧ p.length = G.dist u v

Tactic:
exact ⟨p, p.isPath_of_length_eq_dist h, h⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
u v : V
pos : ∀ (h : u = v), dist ⊥ u v = 0
neg : ∀ (h : ¬u = v), dist ⊥ u v = 0
⊢ dist ⊥ u v = 0

Tactic:
by_cases h : u = v
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
u v : V
h : u = v
⊢ dist ⊥ u v = 0

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
u v : V
h : ¬u = v
⊢ dist ⊥ u v = 0

Tactic:
simp [h]