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
u v : V
refine_1 : ∀ (h : 2 < G.edist u v), u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
refine_2 : ∀ (h : u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅), 2 ≤ G.edist u v
⊢ 2 < G.edist u v ↔ u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
have refine_3 : ∀ (h : u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅), G.edist u v ≠ 2
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ lt_of_le_of_ne ?_ (Ne.symm ?_)⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : 2 < G.edist u v
⊢ u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
have hn : u ≠ v
Tactic: have hn : u ≠ v := fun hc ↦ by simp [hc] at h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : 2 < G.edist u v
hn : u ≠ v
⊢ u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
have this : ¬G.Adj u v
Tactic: have : ¬ G.Adj u v := fun hc ↦ by simp +decide [edist_eq_one_iff_adj.mpr hc] at h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : 2 < G.edist u v
hn : u ≠ v
this : ¬G.Adj u v
⊢ u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
have right : G.commonNeighbors u v = ∅
Tactic: use hn, this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : 2 < G.edist u v
hn : u ≠ v
this : ¬G.Adj u v
⊢ G.commonNeighbors u v = ∅
have right : ∀ (hc : (G.commonNeighbors u v).Nonempty), False
Tactic: by_contra! hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
⊢ HAdd.hAdd (α := ℕ∞) 1 1 ≤ G.edist u v
have refine_2 : 1 ≤ G.edist u v
Tactic: refine Order.add_one_le_of_lt <| lt_of_le_of_ne ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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
⊢ HAdd.hAdd (α := ℕ∞) 1 1 ≤ G.edist u v
have refine_2₁ : 1 ≠ G.edist u v
Tactic: refine Order.add_one_le_of_lt <| lt_of_le_of_ne ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
u v : V
h : u ≠ v
⊢ edist ⊥ u v = ⊤
have rwa : ∀ (h : ¬u = v), edist ⊥ u v = ⊤
Tactic: rwa [ne_eq, ← reachable_bot.not, ← edist_ne_top_iff_reachable.not, not_not] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
u v : V
h : u ≠ v
rwa : ∀ (h : ¬u = v), edist ⊥ u v = ⊤
⊢ edist ⊥ u v = ⊤
have rwa₁ : ∀ (h : ¬Reachable ⊥ u v), edist ⊥ u v = ⊤
Tactic: rwa [ne_eq, ← reachable_bot.not, ← edist_ne_top_iff_reachable.not, not_not] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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 = ⊤
⊢ edist ⊥ u v = ⊤
have rwa₂ : ∀ (h : ¬edist ⊥ u v ≠ ⊤), edist ⊥ u v = ⊤
Tactic: rwa [ne_eq, ← reachable_bot.not, ← edist_ne_top_iff_reachable.not, not_not] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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 = ⊤
⊢ edist ⊥ u v = ⊤
have rwa₃ : ∀ (h : edist ⊥ u v = ⊤), edist ⊥ u v = ⊤
Tactic: rwa [ne_eq, ← reachable_bot.not, ← edist_ne_top_iff_reachable.not, not_not] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
u v : V
inst : DecidableEq V
⊢ edist ⊥ u v = if u = v then 0 else ⊤
have pos : ∀ (h : u = v), edist ⊥ u v = if u = v then 0 else ⊤
Tactic: by_cases h : u = v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
u v : V
inst : DecidableEq V
pos : ∀ (h : u = v), edist ⊥ u v = if u = v then 0 else ⊤
⊢ edist ⊥ u v = if u = v then 0 else ⊤
have neg : ∀ (h : ¬u = v), edist ⊥ u v = if u = v then 0 else ⊤
Tactic: by_cases h : u = v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
u v : V
inst : DecidableEq V
⊢ edist ⊤ u v = if u = v then 0 else 1
have pos : ∀ (h : u = v), edist ⊤ u v = if u = v then 0 else 1
Tactic: by_cases h : u = v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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
⊢ edist ⊤ u v = if u = v then 0 else 1
have neg : ∀ (h : ¬u = v), edist ⊤ u v = if u = v then 0 else 1
Tactic: by_cases h : u = v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
⊢ G'.edist u v ≤ G.edist u v
have pos : ∀ (hr : G.Reachable u v), G'.edist u v ≤ G.edist u v
Tactic: by_cases hr : G.Reachable u v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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
⊢ G'.edist u v ≤ G.edist u v
have neg : ∀ (hr : ¬G.Reachable u v), G'.edist u v ≤ G.edist u v
Tactic: by_cases hr : G.Reachable u v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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
have pos : ∀ (w : G.Walk u v) (hw : (↑w.length : ℕ∞) = G.edist u v), G'.edist u v ≤ G.edist u v
Tactic: obtain ⟨_, hw⟩ := hr.exists_walk_length_eq_edist
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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 ≤ G.edist u v
have pos : G'.edist u v ≤ (↑(Walk.map (Hom.ofLE h) w).length : ℕ∞)
Tactic: rw [← hw, ← Walk.length_map (.ofLE h)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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
⊢ False
have obtain : ∀ (p : G.Walk u v) (hp : p.length = G.dist u v), False
Tactic: obtain ⟨p, hp⟩ := Reachable.exists_walk_length_eq_dist h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : 0 < G.dist u v
⊢ Set.Nonempty.{u_1} (α := G.Walk u v) Set.univ
have h₁ : 0 < sInf (Set.range.{0, u_1 + 1} (ι := G.Walk u v) Walk.length)
Tactic: rw [dist_eq_sInf] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
hconn : G.Connected
⊢ G.dist u w ≤ G.dist u v + G.dist v w
have 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
Tactic: obtain ⟨p, hp⟩ := hconn.exists_walk_length_eq_dist u v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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
⊢ G.dist u w ≤ G.dist u v + G.dist v w
have 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
Tactic: obtain ⟨q, hq⟩ := hconn.exists_walk_length_eq_dist v w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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 ≤ G.dist u v + G.dist v w
have rw : G.dist u w ≤ (p.append q).length
Tactic: rw [← hp, ← hq, ← Walk.length_append]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
w : V
⊢ G.dist u w ≤ G.dist u v + G.dist v w
have pos : ∀ (h' : ¬G.Reachable u w), G.dist u w ≤ G.dist u v + G.dist v w
Tactic: by_cases! h' : ¬G.Reachable u w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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
⊢ G.dist u w ≤ G.dist u v + G.dist v w
have neg : ∀ (h' : G.Reachable u w), G.dist u w ≤ G.dist u v + G.dist v w
Tactic: by_cases! h' : ¬G.Reachable u w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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
have neg : (↑(G.dist u w) : ℕ∞) ≤ HAdd.hAdd (α := ℕ∞) (↑(G.dist u v) : ℕ∞) (↑(G.dist v w) : ℕ∞)
Tactic: rw [← ENat.coe_le_coe, ENat.coe_add]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Reachable v w
u : V
⊢ G.dist u w ≤ G.dist u v + G.dist v w
have pos : ∀ (h' : ¬G.Reachable u w), G.dist u w ≤ G.dist u v + G.dist v w
Tactic: by_cases! h' : ¬G.Reachable u w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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
⊢ G.dist u w ≤ G.dist u v + G.dist v w
have neg : ∀ (h' : G.Reachable u w), G.dist u w ≤ G.dist u v + G.dist v w
Tactic: by_cases! h' : ¬G.Reachable u w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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
have neg : (↑(G.dist u w) : ℕ∞) ≤ HAdd.hAdd (α := ℕ∞) (↑(G.dist u v) : ℕ∞) (↑(G.dist v w) : ℕ∞)
Tactic: rw [← ENat.coe_le_coe, ENat.coe_add]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.dist u v = G.dist v u
have rw : (G.edist u v).toNat = G.dist v u
Tactic: rw [dist, dist, edist_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
rw : (G.edist u v).toNat = G.dist v u
⊢ G.dist u v = G.dist v u
have rw₁ : (G.edist u v).toNat = (G.edist v u).toNat
Tactic: rw [dist, dist, edist_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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
⊢ G.dist u v = G.dist v u
have rw₂ : (G.edist v u).toNat = (G.edist v u).toNat
Tactic: rw [dist, dist, edist_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.dist u v = 1 ↔ G.Adj u v
have rw : Ne (α := ℕ) 1 0
Tactic: rw [dist, ENat.toNat_eq_iff, ENat.coe_one, edist_eq_one_iff_adj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
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
have 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
Tactic: by_cases! huw : ¬G.Reachable u w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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
⊢ 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
have 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
Tactic: by_cases! huw : ¬G.Reachable u w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (hypothesis)
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
have this : G.dist v w = 1
Tactic: have : G.dist v w = 1 := dist_eq_one_iff_adj.mpr hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (hypothesis)
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 u w = G.dist u v ∨ G.dist u w = G.dist u v + 1 ∨ G.dist u w = G.dist u v - 1
have this₁ : G.dist w v = 1
Tactic: have : G.dist w v = 1 := dist_eq_one_iff_adj.mpr hadj.symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (hypothesis)
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 u w = G.dist u v + 1 ∨ G.dist u w = G.dist u v - 1
have this₁ : 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (hypothesis)
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 w = G.dist u v ∨ G.dist u w = G.dist u v + 1 ∨ G.dist u w = G.dist u v - 1
have this₁ : 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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
have h : p.length ≤ p.bypass.length
Tactic: apply Walk.bypass_eq_self_of_length_le
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
⊢ p.IsPath
have this : 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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.IsPath
have rw : p.bypass.IsPath
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
⊢ p.IsPath
have have : p.bypass = p
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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
⊢ p.IsPath
have have₁ : ∀ (this : p.bypass = p), 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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
⊢ p.IsPath
have have₅ : ∀ (this : p.bypass = p), p.bypass.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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
hr : G.Reachable u v
⊢ ∃ (p : G.Walk u v), p.IsPath ∧ p.length = G.dist u v
have 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
Tactic: obtain ⟨p, h⟩ := hr.exists_walk_length_eq_dist
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u v : V
⊢ ∃ (p : G.Walk u v), p.IsPath ∧ p.length = G.dist u v
have 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
Tactic: obtain ⟨p, h⟩ := hconn.exists_walk_length_eq_dist u v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
u v : V
⊢ dist ⊥ u v = 0
have pos : ∀ (h : u = v), dist ⊥ u v = 0
Tactic: by_cases h : u = v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
u v : V
pos : ∀ (h : u = v), dist ⊥ u v = 0
⊢ dist ⊥ u v = 0
have neg : ∀ (h : ¬u = v), dist ⊥ u v = 0
Tactic: by_cases h : u = v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
u v : V
inst : DecidableEq V
⊢ dist ⊤ u v = if u = v then 0 else 1
have pos : ∀ (h : u = v), dist ⊤ u v = if u = v then 0 else 1
Tactic: by_cases h : u = v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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
⊢ dist ⊤ u v = if u = v then 0 else 1
have neg : ∀ (h : ¬u = v), dist ⊤ u v = if u = v then 0 else 1
Tactic: by_cases h : u = v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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'
have refine : ∀ (hh : G.dist u' v' < p₂.length), False
Tactic: refine (dist_le _).eq_of_not_lt' fun hh ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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
⊢ False
have obtain : ∀ (ru : G.Walk u u') (rv : G.Walk v' v) (h : p₁ = (ru.append p₂).append rv), False
Tactic: obtain ⟨ru, rv, h⟩ := h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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
⊢ False
have obtain : ∀ (s : G.Walk u' v'), s.IsPath ∧ s.length = G.dist u' v' → False
Tactic: obtain ⟨s, _⟩ := p₂.reachable.exists_path_of_dist
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (hypothesis)
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
⊢ False
have this : p₁.length = ru.length + p₂.length + rv.length
Tactic: have : p₁.length = ru.length + p₂.length + rv.length := by simp [h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (hypothesis)
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
⊢ False
have this₁ : r.length = ru.length + s.length + rv.length
Tactic: have : r.length = ru.length + s.length + rv.length := by simp [r]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (hypothesis)
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
⊢ False
have this₁ : G.dist u v ≤ r.length
Tactic: have := dist_le r
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
⊢ G'.dist u v ≤ G.dist u v
have obtain : ∀ (w : G.Walk u v) (hw : w.length = G.dist u v), G'.dist u v ≤ G.dist u v
Tactic: obtain ⟨_, hw⟩ := hr.exists_walk_length_eq_dist
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
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 ≤ G.dist u v
have rw : G'.dist u v ≤ (Walk.map (Hom.ofLE h) w).length
Tactic: rw [← hw, ← Walk.length_map (.ofLE h)]
-- 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
⊢ ∃ (x : V) (a : V) (b : V), G.Adj x a ∧ G.Adj a b ∧ ¬G.Adj x b ∧ x ≠ b
have 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
Tactic: use v, p.getVert 1, 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
⊢ 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 hnp : ¬p.Nil
Tactic: have hnp : ¬p.Nil := by grind [Nil.length_eq_zero]
-- 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
⊢ ¬p.tail.Nil
have simp : ∀ (hp : p.tail.length + 1 = G.dist v w), 0 < p.tail.length
Tactic: simp only [not_nil_iff_lt_length, ← p.length_tail_add_one hnp] at hp ⊢
Cleared hypotheses: hp
-- 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
⊢ p.tail.tail.length < p.tail.length
have rw : p.tail.tail.length < p.tail.tail.length + 1
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)]
-- 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
⊢ 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 : 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
-- 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 : p.tail.tail.length < p.tail.length
⊢ p.tail.length < p.length
have rw : p.tail.length < p.tail.length + 1
Tactic: rw [← p.length_tail_add_one hnp]
-- 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 : p.tail.tail.length < p.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
have this₁ : p.tail.length < p.length
Tactic: have : p.tail.length < p.length := by rw [← p.length_tail_add_one hnp]; lia