awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hl : G.Adj v w
h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
neg :
  ∀ (hnadj : ¬G'.Adj v w') (hu' : ∀ (u' : V), u' ≠ v → G.Adj w' u' → G'.Adj w' u')
    (hx' : ∀ (x' : V), x' ≠ w' → G.Adj x' v → G'.Adj x' v) (hadj : ¬G.Adj v w')
    (h2 : (v = v ∧ w' = w' ∨ v = w' ∧ w' = v) ∧ v ≠ w'), G'.Adj v w
⊢ G'.Adj v w
have neg₁ : ∀ (h2r1 : v = x) (h2r2 : w' = u), G'.Adj v w
Tactic: rcases h2.1 with ⟨rfl, rfl⟩ | ⟨h2r1, h2r2⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
h1 : G.Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'
have neg : G'.Adj u x ↔ ¬G'.Adj v w'
Tactic: rw [G'.adj_congr_of_sym2 (by grind : s(v, w) = s(u, x))]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
h1 : G.Adj v w'
⊢ G'.Adj u x ↔ ¬G'.Adj v w'
have neg : G'.Adj v w'
Tactic: simp only [hnadj, false_iff, not_not]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
h1 : G.Adj v w'
⊢ G'.Adj v w'
have neg : ∀ (hnadj : ¬G'.Adj v w) (hu' : ∀ (u' : V), u' ≠ v → G.Adj w u' → G'.Adj w u')
  (hx' : ∀ (x' : V), x' ≠ w → G.Adj x' v → G'.Adj x' v) (hadj : ¬G.Adj v w)
  (hr : (v = v ∧ w = w ∨ v = w ∧ w = v) ∧ v ≠ w), G'.Adj v w'
Tactic: rcases hr.1 with ⟨rfl, rfl⟩ | ⟨hrr1, hrr2⟩
Cleared hypotheses: u, x, hnadj, hu', hx', hadj, hr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
h1 : G.Adj v w'
neg :
  ∀ (hnadj : ¬G'.Adj v w) (hu' : ∀ (u' : V), u' ≠ v → G.Adj w u' → G'.Adj w u')
    (hx' : ∀ (x' : V), x' ≠ w → G.Adj x' v → G'.Adj x' v) (hadj : ¬G.Adj v w)
    (hr : (v = v ∧ w = w ∨ v = w ∧ w = v) ∧ v ≠ w), G'.Adj v w'
⊢ G'.Adj v w'
have neg₁ : ∀ (hrr1 : v = x) (hrr2 : w = u), G'.Adj v w'
Tactic: rcases hr.1 with ⟨rfl, rfl⟩ | ⟨hrr1, hrr2⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
⊢ IsPerfectMatching.{u_1} (V := V) (G := M.spanningCoe ∆ G') ⊤
have rw : ∀ (v : V), ∃! w : V, Adj (G := M.spanningCoe ∆ G') ⊤ v w
Tactic: rw [Subgraph.isPerfectMatching_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v : V
⊢ ∃! w : V, Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w
have obtain : ∀ (w : V) (hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w),
  ∃! w : V, Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w
Tactic: obtain ⟨w, hw⟩ := hM.1 (hM.2 v)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
⊢ ∃! w : V, Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w
have pos : ∀ (h : G'.Adj v w), ∃! w : V, Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w
Tactic: by_cases h : G'.Adj v w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
pos : ∀ (h : G'.Adj v w), ∃! w : V, Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w
⊢ ∃! w : V, Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w
have neg : ∀ (h : ¬G'.Adj v w), ∃! w : V, Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w
Tactic: by_cases h : G'.Adj v w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
h : G'.Adj v w
⊢ ∃! w : V, Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w
have pos : ∀ (w' : V) (hw' : w ≠ w' ∧ G'.Adj v w'), ∃! w : V, Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w
Tactic: obtain ⟨w', hw'⟩ := hG'cyc.other_adj_of_adj h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
h : G'.Adj v w
w' : V
hw' : w ≠ w' ∧ G'.Adj v w'
⊢ ∃! w : V, Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w
have hmadj : M.Adj v w ↔ ¬M.Adj v w'
Tactic: have hmadj : M.Adj v w ↔ ¬M.Adj v w' := by simpa using hG' hw'.1 h hw'.2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
h : G'.Adj v w
w' : V
hw' : w ≠ w' ∧ G'.Adj v w'
hmadj : M.Adj v w ↔ ¬M.Adj v w'
⊢ ∃! w : V, Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w
have h₁ : (fun (w : V) ↦ Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w) w' ∧
  ∀ (y : V), (fun (w : V) ↦ Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w) y → y = w'
Tactic: use w'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
h : G'.Adj v w
w' : V
hw' : w ≠ w' ∧ G'.Adj v w'
hmadj : M.Adj v w ↔ ¬M.Adj v w'
⊢ (fun (w : V) ↦ Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w) w' ∧
    ∀ (y : V), (fun (w : V) ↦ Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w) y → y = w'
have h₁ : ∀ (y : V), M.Adj v y ∧ ¬G'.Adj v y ∨ G'.Adj v y ∧ ¬M.Adj v y → y = w'
Tactic: simp only [Subgraph.top_adj, SimpleGraph.sup_adj, sdiff_adj, Subgraph.spanningCoe_adj,
      hmadj.mp hw.1, hw'.2, not_true_eq_false, and_self, not_false_eq_true, or_true, true_and]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
h : G'.Adj v w
w' : V
hw' : w ≠ w' ∧ G'.Adj v w'
hmadj : M.Adj v w ↔ ¬M.Adj v w'
y : V
hr : G'.Adj v y ∧ ¬M.Adj v y
⊢ y = w'
have h₁ : ∀ (w'' : V) (hw'' : y ≠ w'' ∧ G'.Adj v w''), y = w'
Tactic: obtain ⟨w'', hw''⟩ := hG'cyc.other_adj_of_adj hr.1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
h : G'.Adj v w
w' : V
hw' : w ≠ w' ∧ G'.Adj v w'
hmadj : M.Adj v w ↔ ¬M.Adj v w'
y : V
hr : G'.Adj v y ∧ ¬M.Adj v y
w'' : V
hw'' : y ≠ w'' ∧ G'.Adj v w''
⊢ y = w'
have h₁ : ∀ (hc : y ≠ w'), False
Tactic: by_contra! hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
h : ¬G'.Adj v w
⊢ ∃! w : V, Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w
have h₁ : (fun (w : V) ↦ Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w) w ∧
  ∀ (y : V), (fun (w : V) ↦ Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w) y → y = w
Tactic: use w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
h : ¬G'.Adj v w
⊢ (fun (w : V) ↦ Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w) w ∧
    ∀ (y : V), (fun (w : V) ↦ Adj (G := M.spanningCoe \ G' ⊔ G' \ M.spanningCoe) ⊤ v w) y → y = w
have h₁ : ∀ (y : V), M.Adj v y ∧ ¬G'.Adj v y ∨ G'.Adj v y ∧ ¬M.Adj v y → y = w
Tactic: simp only [Subgraph.top_adj, SimpleGraph.sup_adj, sdiff_adj, Subgraph.spanningCoe_adj, hw.1, h,
      not_false_eq_true, and_self, not_true_eq_false, or_false, true_and]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
h : ¬G'.Adj v w
y : V
hr : G'.Adj v y ∧ ¬M.Adj v y
⊢ y = w
have h₁ : ∀ (w' : V) (hw' : y ≠ w' ∧ G'.Adj v w'), y = w
Tactic: have ⟨w', hw'⟩ := hG'cyc.other_adj_of_adj hr.1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w w' : V
hww' : w ≠ w'
hvw : (M.spanningCoe ∆ M'.spanningCoe).Adj v w
hvw' : (M.spanningCoe ∆ M'.spanningCoe).Adj v w'
⊢ M.spanningCoe.Adj v w ↔ ¬M.spanningCoe.Adj v w'
have obtain : ∀ (v1 : V) (hm1 : M.Adj v v1) (hv1 : ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = v1),
  M.spanningCoe.Adj v w ↔ ¬M.spanningCoe.Adj v w'
Tactic: obtain ⟨v1, hm1, hv1⟩ := hM.1 (hM.2 v)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w w' : V
hww' : w ≠ w'
hvw : (M.spanningCoe ∆ M'.spanningCoe).Adj v w
hvw' : (M.spanningCoe ∆ M'.spanningCoe).Adj v w'
v1 : V
hm1 : M.Adj v v1
hv1 : ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = v1
⊢ M.spanningCoe.Adj v w ↔ ¬M.spanningCoe.Adj v w'
have obtain : ∀ (v2 : V) (hm2 : M'.Adj v v2) (hv2 : ∀ (y : V), (fun (w : V) ↦ M'.Adj v w) y → y = v2),
  M.spanningCoe.Adj v w ↔ ¬M.spanningCoe.Adj v w'
Tactic: obtain ⟨v2, hm2, hv2⟩ := hM'.1 (hM'.2 v)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w ≠ ⊤
⊢ G.edist u w ≤ G.edist u v + G.edist v w
have inr : ∀ (p : G.Walk u v) (hp : (↑p.length : ℕ∞) = G.edist u v), G.edist u w ≤ G.edist u v + G.edist v w
Tactic: obtain ⟨p, hp⟩ := exists_walk_of_edist_ne_top huv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w ≠ ⊤
p : G.Walk u v
hp : (↑p.length : ℕ∞) = G.edist u v
⊢ G.edist u w ≤ G.edist u v + G.edist v w
have inr : ∀ (q : G.Walk v w) (hq : (↑q.length : ℕ∞) = G.edist v w), G.edist u w ≤ G.edist u v + G.edist v w
Tactic: obtain ⟨q, hq⟩ := exists_walk_of_edist_ne_top hvw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w ≠ ⊤
p : G.Walk u v
hp : (↑p.length : ℕ∞) = G.edist u v
q : G.Walk v w
hq : (↑q.length : ℕ∞) = G.edist v w
⊢ G.edist u w ≤ G.edist u v + G.edist v w
have inr : G.edist u w ≤ (↑(p.append q).length : ℕ∞)
Tactic: rw [← hp, ← hq, ← Nat.cast_add, ← Walk.length_append]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
⊢ G.edist u w ≤ G.edist u v + G.edist v w
have x : G.edist v w = ⊤ ∨ G.edist v w ≠ ⊤
Tactic: cases eq_or_ne (G.edist v w) ⊤ with
    | inl hvw => simp [hvw]
    | inr hvw =>
      obtain ⟨p, hp⟩ := exists_walk_of_edist_ne_top huv
      obtain ⟨q, hq⟩ := exists_walk_of_edist_ne_top hvw
      rw [← hp, ← hq, ← Nat.cast_add, ← Walk.length_append]
      exact edist_le _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
⊢ G.edist u w ≤ G.edist u v + G.edist v w
have x : G.edist u v = ⊤ ∨ G.edist u v ≠ ⊤
Tactic: cases eq_or_ne (G.edist u v) ⊤ with
  | inl huv => simp [huv]
  | inr huv =>
    cases eq_or_ne (G.edist v w) ⊤ with
    | inl hvw => simp [hvw]
    | inr hvw =>
      obtain ⟨p, hp⟩ := exists_walk_of_edist_ne_top huv
      obtain ⟨q, hq⟩ := exists_walk_of_edist_ne_top hvw
      rw [← hp, ← hq, ← Nat.cast_add, ← Walk.length_append]
      exact edist_le _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.edist u v = G.edist v u
have rw : sInf (Set.range fun (x : G.Walk v u) ↦ (↑x.reverse.length : ℕ∞)) = G.edist v u
Tactic: rw [edist_eq_sInf, ← Set.image_univ, ← Set.image_univ_of_surjective Walk.reverse_surjective,
    ← Set.image_comp, Set.image_univ, Function.comp_def]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ sInf (Set.range fun (x : G.Walk v u) ↦ (↑x.reverse.length : ℕ∞)) = G.edist v u
have simp_rw : sInf (Set.range fun (x : G.Walk v u) ↦ (↑x.length : ℕ∞)) = G.edist v u
Tactic: simp_rw [Walk.length_reverse, ← edist_eq_sInf]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
k : ℕ
h : G.edist u v = (↑k : ℕ∞)
⊢ G.edist u v ≠ ⊤
have rw : Ne (α := ℕ∞) (↑k : ℕ∞) ⊤
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.edist u v ≠ ⊤ ↔ G.Reachable u v
have refine : ∀ (h : G.Reachable u v), G.edist u v ≠ ⊤
Tactic: refine ⟨reachable_of_edist_ne_top, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
hx : G.edist u v = ⊤
⊢ False
have hx₁ : ∀ (i : G.Walk u v), False
Tactic: simp only [edist, iInf_eq_top, ENat.coe_ne_top] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.edist u v = 1 ↔ G.Adj u v
have refine_1 : ∀ (h : G.edist u v = 1), G.Adj u v
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
refine_1 : ∀ (h : G.edist u v = 1), G.Adj u v
⊢ G.edist u v = 1 ↔ G.Adj u v
have refine_2 : ∀ (h : G.Adj u v), G.edist u v = 1
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 1
⊢ G.edist u v ≠ ⊤
have rw : Ne (α := ℕ∞) 1 ⊤
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 1
⊢ G.Adj u v
have refine_1 : ∀ (w : G.Walk u v) (hw : (↑w.length : ℕ∞) = G.edist u v), G.Adj u v
Tactic: obtain ⟨w, hw⟩ := exists_walk_of_edist_ne_top <| by rw [h]; simp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.edist u v ≤ 1 ↔ G.Adj u v ∨ u = v
have pos : ∀ (huv : u = v), G.edist u v ≤ 1 ↔ G.Adj u v ∨ u = v
Tactic: by_cases huv : u = v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
pos : ∀ (huv : u = v), G.edist u v ≤ 1 ↔ G.Adj u v ∨ u = v
⊢ G.edist u v ≤ 1 ↔ G.Adj u v ∨ u = v
have neg : ∀ (huv : ¬u = v), G.edist u v ≤ 1 ↔ G.Adj u v ∨ u = v
Tactic: by_cases huv : u = v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
⊢ G.edist u v ≤ 1 ↔ G.Adj u v ∨ u = v
have neg : G.edist u v ≤ 1 ↔ G.Adj u v
Tactic: simp only [huv, or_false]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
⊢ G.edist u v ≤ 1 ↔ G.Adj u v
have h : 0 < G.edist u v
Tactic: have h : 0 < G.edist u v := edist_pos_of_ne huv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
h : 0 < G.edist u v
⊢ G.edist u v ≤ 1 ↔ G.Adj u v
have neg : G.edist u v = 1 ↔ G.Adj u v
Tactic: rw [(Order.one_le_iff_pos.mpr h).ge_iff_eq']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.edist u v = 2 ↔ u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
have refine_1 : ∀ (h : G.edist u v = 2), u ≠ v
Tactic: refine ⟨fun h ↦ ⟨?_, ?_, ?_⟩, fun h ↦ le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
refine_1 : ∀ (h : G.edist u v = 2), u ≠ v
⊢ G.edist u v = 2 ↔ u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
have refine_2 : ∀ (h : G.edist u v = 2), ¬G.Adj u v
Tactic: refine ⟨fun h ↦ ⟨?_, ?_, ?_⟩, fun h ↦ le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
refine_1 : ∀ (h : G.edist u v = 2), u ≠ v
refine_2 : ∀ (h : G.edist u v = 2), ¬G.Adj u v
⊢ G.edist u v = 2 ↔ u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
have refine_3 : ∀ (h : G.edist u v = 2), (G.commonNeighbors u v).Nonempty
Tactic: refine ⟨fun h ↦ ⟨?_, ?_, ?_⟩, fun h ↦ le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
refine_1 : ∀ (h : G.edist u v = 2), u ≠ v
refine_2 : ∀ (h : G.edist u v = 2), ¬G.Adj u v
refine_3 : ∀ (h : G.edist u v = 2), (G.commonNeighbors u v).Nonempty
⊢ G.edist u v = 2 ↔ u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
have refine_4 : ∀ (h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty), G.edist u v ≤ 2
Tactic: refine ⟨fun h ↦ ⟨?_, ?_, ?_⟩, fun h ↦ le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
refine_1 : ∀ (h : G.edist u v = 2), u ≠ v
refine_2 : ∀ (h : G.edist u v = 2), ¬G.Adj u v
refine_3 : ∀ (h : G.edist u v = 2), (G.commonNeighbors u v).Nonempty
refine_4 : ∀ (h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty), G.edist u v ≤ 2
⊢ G.edist u v = 2 ↔ u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
have refine_5 : ∀ (h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty), 2 ≤ G.edist u v
Tactic: refine ⟨fun h ↦ ⟨?_, ?_, ?_⟩, fun h ↦ le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
⊢ (G.commonNeighbors u v).Nonempty
have refine_3 : ∀ (w : G.Walk u v) (hw : w.length = 2), (G.commonNeighbors u v).Nonempty
Tactic: obtain ⟨w, hw⟩ := exists_walk_of_edist_eq_coe h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
w : G.Walk u v
hw : w.length = 2
⊢ (G.commonNeighbors u v).Nonempty
have h₁ : w.getVert 1 ∈ G.commonNeighbors u v
Tactic: use w.getVert 1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
w : G.Walk u v
hw : w.length = 2
⊢ w.getVert 1 ∈ G.commonNeighbors u v
have h₁ : w.getVert 1 ∈ G.commonNeighbors (w.getVert 0) (w.getVert w.length)
Tactic: suffices w.getVert 1 ∈ G.commonNeighbors (w.getVert 0) (w.getVert w.length) by simpa
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
w : G.Walk u v
hw : w.length = 2
⊢ w.getVert 1 ∈ G.commonNeighbors (w.getVert 0) (w.getVert w.length)
have h₁ : w.getVert 1 ∈ G.commonNeighbors (w.getVert 0) (w.getVert 2)
Tactic: refine hw ▸ G.mem_commonNeighbors.mp ?_
-- 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).Nonempty
⊢ G.edist u v ≤ 2
have refine_4 : ∀ (w : V) (hw : w ∈ G.commonNeighbors u v), G.edist u v ≤ 2
Tactic: obtain ⟨w, hw⟩ := h.2.2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
w : V
hw : w ∈ G.commonNeighbors u v
⊢ G.edist u v ≤ 2
have hw₁ : G.Adj u w ∧ G.Adj v w
Tactic: rw [mem_commonNeighbors] at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
w : V
hw : G.Adj u w ∧ G.Adj v w
⊢ G.edist u v ≤ 2
have this : G.edist u v ≤ (↑(Walk.cons sorry (Walk.cons sorry Walk.nil)).length : ℕ∞)
Tactic: have := (Walk.cons hw.1 <| .cons hw.2.symm .nil).edist_le
-- 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).Nonempty
⊢ 2 ≤ G.edist u v
have refine_5 : ∀ (hc : G.edist u v < 2), 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).Nonempty
hc : G.edist u v < 2
⊢ False
have refine_5 : G.edist u v = 0 → False
Tactic: cases ENat.le_one_iff_eq_zero_or_eq_one.mp (Order.le_of_lt_succ 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).Nonempty
hc : G.edist u v < 2
refine_5 : G.edist u v = 0 → False
⊢ False
have refine_5₁ : G.edist u v = 1 → False
Tactic: cases ENat.le_one_iff_eq_zero_or_eq_one.mp (Order.le_of_lt_succ hc)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Metric (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ 2 < G.edist u v ↔ u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
have refine_1 : ∀ (h : 2 < G.edist u v), u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ lt_of_le_of_ne ?_ (Ne.symm ?_)⟩
-- 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 = ∅
⊢ 2 < G.edist u v ↔ u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
have refine_2 : ∀ (h : u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅), 2 ≤ G.edist u v
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ lt_of_le_of_ne ?_ (Ne.symm ?_)⟩