awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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
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'
⊢ M.spanningCoe.Adj v w ↔ ¬M.spanningCoe.Adj v w'

Tactic:
obtain ⟨v2, hm2, hv2⟩ := hM'.1 (hM'.2 v)

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
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 ⊔ M'.spanningCoe \ M.spanningCoe).Adj v w
hvw' : (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).Adj v w'
v1 : V
hm1 : M.Adj v v1
hv1 : ∀ (y : V), M.Adj v y → y = v1
v2 : V
hm2 : M'.Adj v v2
hv2 : ∀ (y : V), M'.Adj v y → y = v2
⊢ M.spanningCoe.Adj v w ↔ ¬M.spanningCoe.Adj v w'

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
⊢ (M.spanningCoe ∆ M'.spanningCoe).IsAlternating M'.spanningCoe

Tactic:
simpa [symmDiff_comm] using isAlternating_symmDiff_left hM' hM

Premises used: SimpleGraph.Subgraph.IsPerfectMatching.isAlternating_symmDiff_left, symmDiff_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.edist u v = sInf (Set.range fun (w : G.Walk u v) ↦ (↑w.length : ℕ∞))

Tactic:
rfl

Premises used: iInf, SimpleGraph.edist, rfl
-- 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.edist u v

Tactic:
csInf_mem <| Set.range_nonempty_iff_nonempty.mpr hr

Premises used: Iff.mpr, Set.range_nonempty_iff_nonempty, csInf_mem, iInf, Set.Mem, setOf, SimpleGraph.edist, Set.range
-- 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.edist u v

Tactic:
(hconn u v).exists_walk_length_eq_edist

Premises used: SimpleGraph.Connected.preconnected, SimpleGraph.Reachable.exists_walk_length_eq_edist
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ G.edist u v ≤ (↑p.length : ℕ∞)

Tactic:
sInf_le ⟨p, rfl⟩

Premises used: iInf, SimpleGraph.edist, sInf_le, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.edist u v = 0 ↔ u = v

Tactic:
simp [edist]

Premises used: SimpleGraph.edist
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
v : V
⊢ G.edist v v = 0

Tactic:
edist_eq_zero_iff.mpr rfl

Premises used: Iff.mpr, SimpleGraph.edist_eq_zero_iff, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
⊢ 0 < G.edist u v

Tactic:
pos_iff_ne_zero.mpr <| edist_eq_zero_iff.ne.mpr hne

Premises used: Iff.mpr, Iff.ne, SimpleGraph.edist_eq_zero_iff, pos_iff_ne_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : ¬G.Reachable u v
⊢ G.edist u v = ⊤

Tactic:
simp [edist, not_reachable_iff_isEmpty_walk.mp h]

Premises used: SimpleGraph.not_reachable_iff_isEmpty_walk, SimpleGraph.edist, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v ≠ ⊤
⊢ G.Reachable u v

Tactic:
not_not.mp <| edist_eq_top_of_not_reachable.mt h

Premises used: Function.mt, Classical.not_not, SimpleGraph.edist_eq_top_of_not_reachable, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v ≠ ⊤
⊢ ∃ (p : G.Walk u v), (↑p.length : ℕ∞) = G.edist u v

Tactic:
(reachable_of_edist_ne_top h).exists_walk_length_eq_edist

Premises used: SimpleGraph.reachable_of_edist_ne_top, SimpleGraph.Reachable.exists_walk_length_eq_edist
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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

Tactic:
simp [huv]
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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

Tactic:
simp [hvw]
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w ≠ ⊤
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
⊢ G.edist u w ≤ G.edist u v + G.edist v w

Tactic:
obtain ⟨p, hp⟩ := exists_walk_of_edist_ne_top huv

Premises used: SimpleGraph.exists_walk_of_edist_ne_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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
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
⊢ G.edist u w ≤ G.edist u v + G.edist v w

Tactic:
obtain ⟨q, hq⟩ := exists_walk_of_edist_ne_top hvw

Premises used: SimpleGraph.exists_walk_of_edist_ne_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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
inr : G.edist u w ≤ (↑(p.append q).length : ℕ∞)
⊢ G.edist u w ≤ G.edist u v + G.edist v w

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

Premises used: Nat.cast_add, SimpleGraph.Walk.length_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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 ≤ (↑(p.append q).length : ℕ∞)

Tactic:
edist_le _

Premises used: SimpleGraph.edist_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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 ≤ (↑(p.append q).length : ℕ∞)

Tactic:
exact edist_le _

Premises used: SimpleGraph.edist_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
⊢ 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 _

Premises used: Nat.cast_add, SimpleGraph.Walk.length_append, SimpleGraph.edist, eq_or_ne, SimpleGraph.exists_walk_of_edist_ne_top, Top.top, SimpleGraph.edist_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
⊢ 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 _

Premises used: Nat.cast_add, SimpleGraph.Walk.length_append, SimpleGraph.edist, eq_or_ne, Top.top, SimpleGraph.edist_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
rw : sInf (Set.range fun (x : G.Walk v u) ↦ (↑x.reverse.length : ℕ∞)) = G.edist v u
⊢ G.edist u v = 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]

Premises used: Set.image_univ, SimpleGraph.Walk.reverse_surjective, SimpleGraph.edist_eq_sInf, Function.comp_def, Set.image_univ_of_surjective, Set.image_comp
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
simp_rw : sInf (Set.range fun (x : G.Walk v u) ↦ (↑x.length : ℕ∞)) = G.edist v u
⊢ sInf (Set.range fun (x : G.Walk v u) ↦ (↑x.reverse.length : ℕ∞)) = G.edist v u

Tactic:
simp_rw [Walk.length_reverse, ← edist_eq_sInf]

Premises used: SimpleGraph.edist_eq_sInf, SimpleGraph.Walk.length_reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
k : ℕ
h : G.edist u v = (↑k : ℕ∞)
rw : Ne (α := ℕ∞) (↑k : ℕ∞) ⊤
⊢ G.edist u v ≠ ⊤

Tactic:
rw [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
k : ℕ
h : G.edist u v = (↑k : ℕ∞)
⊢ Ne (α := ℕ∞) (↑k : ℕ∞) ⊤

Tactic:
ENat.coe_ne_top _

Premises used: ENat.coe_ne_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
k : ℕ
h : G.edist u v = (↑k : ℕ∞)
⊢ Ne (α := ℕ∞) (↑k : ℕ∞) ⊤

Tactic:
exact ENat.coe_ne_top _

Premises used: ENat.coe_ne_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.edist u v ≠ ⊤ ↔ G.Reachable u v

Tactic:
⟨reachable_of_edist_ne_top, fun h ↦ ?_⟩

Premises used: Iff.intro, SimpleGraph.reachable_of_edist_ne_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
refine : ∀ (h : G.Reachable u v), G.edist u v ≠ ⊤
⊢ G.edist u v ≠ ⊤ ↔ G.Reachable u v

Tactic:
refine ⟨reachable_of_edist_ne_top, fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
by_contra : ∀ (hx : G.edist u v = ⊤), False
⊢ G.edist u v ≠ ⊤

Tactic:
by_contra hx
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
hx : G.edist u v = ⊤
⊢ ∀ (i : G.Walk u v), False

Tactic:
simp only [edist, iInf_eq_top, ENat.coe_ne_top] at hx

Premises used: iInf_eq_top, SimpleGraph.edist, ENat.coe_ne_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
hx : ∀ (i : G.Walk u v), False
⊢ False

Tactic:
h.elim hx

Premises used: SimpleGraph.Reachable.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
hx : ∀ (i : G.Walk u v), False
⊢ False

Tactic:
exact h.elim hx

Premises used: SimpleGraph.Reachable.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.edist u v = 1 ↔ G.Adj u v

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
refine_1 : ∀ (h : G.edist u v = 1), G.Adj u v
refine_2 : ∀ (h : G.Adj u v), G.edist u v = 1
⊢ G.edist u v = 1 ↔ G.Adj u v

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 1
rw : Ne (α := ℕ∞) 1 ⊤
⊢ G.edist u v ≠ ⊤

Tactic:
rw [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 1
⊢ Ne (α := ℕ∞) 1 ⊤

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 1
refine_1 : ∀ (w : G.Walk u v) (hw : (↑w.length : ℕ∞) = G.edist u v), G.Adj u v
⊢ G.Adj u v

Tactic:
obtain ⟨w, hw⟩ := exists_walk_of_edist_ne_top <| by rw [h]; simp

Premises used: SimpleGraph.exists_walk_of_edist_ne_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 1
w : G.Walk u v
hw : (↑w.length : ℕ∞) = G.edist u v
⊢ G.Adj u v

Tactic:
w.adj_of_length_eq_one <| Nat.cast_eq_one.mp <| h ▸ hw

Premises used: SimpleGraph.Walk.adj_of_length_eq_one, Nat.cast_eq_one, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 1
w : G.Walk u v
hw : (↑w.length : ℕ∞) = G.edist u v
⊢ G.Adj u v

Tactic:
exact w.adj_of_length_eq_one <| Nat.cast_eq_one.mp <| h ▸ hw

Premises used: SimpleGraph.Walk.adj_of_length_eq_one, Nat.cast_eq_one, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ G.edist u v = 1

Tactic:
le_antisymm (edist_le h.toWalk) (Order.one_le_iff_pos.mpr <| edist_pos_of_ne h.ne)

Premises used: SimpleGraph.Adj.toWalk, Iff.mpr, SimpleGraph.Adj.ne, SimpleGraph.edist_pos_of_ne, le_antisymm, SimpleGraph.edist_le, Order.one_le_iff_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ G.edist u v = 1

Tactic:
exact le_antisymm (edist_le h.toWalk) (Order.one_le_iff_pos.mpr <| edist_pos_of_ne h.ne)

Premises used: SimpleGraph.Adj.toWalk, Iff.mpr, SimpleGraph.Adj.ne, SimpleGraph.edist_pos_of_ne, le_antisymm, SimpleGraph.edist_le, Order.one_le_iff_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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
neg : ∀ (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

Tactic:
by_cases huv : u = v
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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

Tactic:
simp [huv]
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
neg : G.edist u v ≤ 1 ↔ G.Adj u v
⊢ G.edist u v ≤ 1 ↔ G.Adj u v ∨ u = v

Tactic:
simp only [huv, or_false]

Premises used: or_false
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
⊢ 0 < G.edist u v

Tactic:
have h : 0 < G.edist u v := edist_pos_of_ne huv
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
h : 0 < G.edist u v
neg : G.edist u v = 1 ↔ G.Adj u v
⊢ G.edist u v ≤ 1 ↔ G.Adj u v

Tactic:
rw [(Order.one_le_iff_pos.mpr h).ge_iff_eq']

Premises used: Iff.mpr, LE.le.ge_iff_eq', Order.one_le_iff_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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

Tactic:
edist_eq_one_iff_adj

Premises used: SimpleGraph.edist_eq_one_iff_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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

Tactic:
exact edist_eq_one_iff_adj

Premises used: SimpleGraph.edist_eq_one_iff_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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

Tactic:
⟨fun h ↦ ⟨?_, ?_, ?_⟩, fun h ↦ le_antisymm ?_ ?_⟩

Premises used: le_antisymm, And.intro, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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
refine_5 : ∀ (h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty), 2 ≤ G.edist u v
⊢ G.edist u v = 2 ↔ u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_, ?_⟩, fun h ↦ le_antisymm ?_ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
⊢ u ≠ v

Tactic:
simp +decide [← G.edist_eq_zero_iff.not (b := u = v), h]

Premises used: Iff.not, SimpleGraph.edist_eq_zero_iff, Decidable.decide
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
⊢ ¬G.Adj u v

Tactic:
simp +decide [← edist_eq_one_iff_adj, h]

Premises used: Decidable.decide, SimpleGraph.edist_eq_one_iff_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
refine_3 : ∀ (w : G.Walk u v) (hw : w.length = 2), (G.commonNeighbors u v).Nonempty
⊢ (G.commonNeighbors u v).Nonempty

Tactic:
obtain ⟨w, hw⟩ := exists_walk_of_edist_eq_coe h

Premises used: SimpleGraph.exists_walk_of_edist_eq_coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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
h₁ : w.getVert 1 ∈ G.commonNeighbors u v
⊢ (G.commonNeighbors u v).Nonempty

Tactic:
use w.getVert 1

Premises used: OfNat.ofNat, SimpleGraph.Walk.getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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
this : w.getVert 1 ∈ G.commonNeighbors (w.getVert 0) (w.getVert w.length)
⊢ w.getVert 1 ∈ G.commonNeighbors u v

Tactic:
simpa
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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
h₁ : w.getVert 1 ∈ G.commonNeighbors (w.getVert 0) (w.getVert w.length)
⊢ w.getVert 1 ∈ G.commonNeighbors u v

Tactic:
suffices w.getVert 1 ∈ G.commonNeighbors (w.getVert 0) (w.getVert w.length) by simpa
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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)

Tactic:
hw ▸ G.mem_commonNeighbors.mp ?_

Premises used: SimpleGraph.mem_commonNeighbors, Eq.rec, Iff.mp, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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
h₁ : w.getVert 1 ∈ G.commonNeighbors (w.getVert 0) (w.getVert 2)
⊢ w.getVert 1 ∈ G.commonNeighbors (w.getVert 0) (w.getVert w.length)

Tactic:
refine hw ▸ G.mem_commonNeighbors.mp ?_
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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
⊢ 0 < w.length

Tactic:
simp [hw]
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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
⊢ 1 < w.length

Tactic:
simp [hw]
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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 2)

Tactic:
exact ⟨w.adj_getVert_succ (by simp [hw]), (w.adj_getVert_succ (by simp [hw])).symm⟩
-- 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).Nonempty
refine_4 : ∀ (w : V) (hw : w ∈ G.commonNeighbors u v), G.edist u v ≤ 2
⊢ G.edist u v ≤ 2

Tactic:
obtain ⟨w, hw⟩ := h.2.2

Premises used: And.right
-- 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).Nonempty
w : V
hw : w ∈ G.commonNeighbors u v
⊢ G.Adj u w ∧ G.Adj v w

Tactic:
rw [mem_commonNeighbors] at hw

Premises used: SimpleGraph.mem_commonNeighbors
-- 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).Nonempty
w : V
hw : G.Adj u w ∧ G.Adj v w
⊢ G.edist u v ≤ (↑(Walk.cons ⋯ (Walk.cons ⋯ Walk.nil)).length : ℕ∞)

Tactic:
have := (Walk.cons hw.1 <| .cons hw.2.symm .nil).edist_le
-- 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).Nonempty
w : V
hw : G.Adj u w ∧ G.Adj v w
this : G.edist u v ≤ (↑(Walk.cons ⋯ (Walk.cons ⋯ Walk.nil)).length : ℕ∞)
⊢ G.edist u v ≤ 2

Tactic:
simp_all
-- 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).Nonempty
refine_5 : ∀ (hc : G.edist u v < 2), False
⊢ 2 ≤ G.edist u v

Tactic:
by_contra! hc
-- 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).Nonempty
hc : G.edist u v < 2
refine_5 : G.edist u v = 0 → False
refine_5₁ : G.edist u v = 1 → False
⊢ False

Tactic:
cases ENat.le_one_iff_eq_zero_or_eq_one.mp (Order.le_of_lt_succ hc)

Premises used: Iff.mp, ENat.le_one_iff_eq_zero_or_eq_one, Order.le_of_lt_succ
-- 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).Nonempty
hc : G.edist u v < 2
h_1 : G.edist u v = 0
⊢ False

Tactic:
simp_all
-- 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).Nonempty
hc : G.edist u v < 2
h_1 : G.edist u v = 1
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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 = ∅

Tactic:
⟨fun h ↦ ?_, fun h ↦ lt_of_le_of_ne ?_ (Ne.symm ?_)⟩

Premises used: Ne.symm, Iff.intro, lt_of_le_of_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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
refine_3 : ∀ (h : u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅), G.edist u v ≠ 2
⊢ 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 ?_)⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : 2 < G.edist u v
hc : u = v
⊢ False

Tactic:
simp [hc] at h
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : 2 < G.edist u v
⊢ u ≠ v

Tactic:
have hn : u ≠ v := fun hc ↦ by simp [hc] at h
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : 2 < G.edist u v
hn : u ≠ v
hc : G.Adj u v
⊢ False

Tactic:
simp +decide [edist_eq_one_iff_adj.mpr hc] at h

Premises used: Iff.mpr, Decidable.decide, SimpleGraph.edist_eq_one_iff_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : 2 < G.edist u v
hn : u ≠ v
⊢ ¬G.Adj u v

Tactic:
have : ¬ G.Adj u v := fun hc ↦ by simp +decide [edist_eq_one_iff_adj.mpr hc] at h
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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
right : G.commonNeighbors u v = ∅
⊢ u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅

Tactic:
use hn, this
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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
right : ∀ (hc : (G.commonNeighbors u v).Nonempty), False
⊢ G.commonNeighbors u v = ∅

Tactic:
by_contra! hc
-- Module: Mathlib.Combinatorics.SimpleGraph.Metric
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
hc : (G.commonNeighbors u v).Nonempty
⊢ False

Tactic:
simp [edist_eq_two_iff.mpr ⟨hn, this, hc⟩] at h

Premises used: Iff.mpr, SimpleGraph.edist_eq_two_iff, And.intro
-- 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 = ∅
⊢ HAdd.hAdd (α := ℕ∞) 1 1 ≤ G.edist u v

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

Premises used: Order.add_one_le_of_lt, lt_of_le_of_ne