[GOAL]
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
⊢ Nonempty (Path r b)
[PROOFSTEP]
rcases show ∃ n, height b < n from ⟨_, Nat.lt.base _⟩ with ⟨n, hn⟩
[GOAL]
case intro
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
n : ℕ
hn : height b < n
⊢ Nonempty (Path r b)
[PROOFSTEP]
induction' n with n ih generalizing b
[GOAL]
case intro.zero
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b✝ : V
n : ℕ
hn✝ : height b✝ < n
b : V
hn : height b < Nat.zero
⊢ Nonempty (Path r b)
[PROOFSTEP]
exact False.elim (Nat.not_lt_zero _ hn)
[GOAL]
case intro.succ
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b✝ : V
n✝ : ℕ
hn✝ : height b✝ < n✝
n : ℕ
ih : ∀ (b : V), height b < n → Nonempty (Path r b)
b : V
hn : height b < Nat.succ n
⊢ Nonempty (Path r b)
[PROOFSTEP]
rcases root_or_arrow b with (⟨⟨⟩⟩ | ⟨a, ⟨e⟩⟩)
[GOAL]
case intro.succ.inl.refl
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
n✝ : ℕ
hn✝ : height b < n✝
n : ℕ
ih : ∀ (b : V), height b < n → Nonempty (Path r b)
hn : height r < Nat.succ n
⊢ Nonempty (Path r r)
[PROOFSTEP]
exact ⟨Path.nil⟩
[GOAL]
case intro.succ.inr.intro.intro
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b✝ : V
n✝ : ℕ
hn✝ : height b✝ < n✝
n : ℕ
ih : ∀ (b : V), height b < n → Nonempty (Path r b)
b : V
hn : height b < Nat.succ n
a : V
e : a ⟶ b
⊢ Nonempty (Path r b)
[PROOFSTEP]
rcases ih a (lt_of_lt_of_le (height_lt e) (Nat.lt_succ_iff.mp hn)) with ⟨p⟩
[GOAL]
case intro.succ.inr.intro.intro.intro
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b✝ : V
n✝ : ℕ
hn✝ : height b✝ < n✝
n : ℕ
ih : ∀ (b : V), height b < n → Nonempty (Path r b)
b : V
hn : height b < Nat.succ n
a : V
e : a ⟶ b
p : Path r a
⊢ Nonempty (Path r b)
[PROOFSTEP]
exact ⟨p.cons e⟩
[GOAL]
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
⊢ ∀ (a : Path r b), a = default
[PROOFSTEP]
have height_le : ∀ {a b}, Path a b → height a ≤ height b :=
  by
  intro a b p
  induction' p with b c _ e ih
  rfl
  exact le_of_lt (lt_of_le_of_lt ih (height_lt e))
[GOAL]
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
⊢ ∀ {a b : V}, Path a b → height a ≤ height b
[PROOFSTEP]
intro a b p
[GOAL]
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b✝ a b : V
p : Path a b
⊢ height a ≤ height b
[PROOFSTEP]
induction' p with b c _ e ih
[GOAL]
case nil
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b✝ a b : V
⊢ height a ≤ height a
case cons
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b✝¹ a b✝ b c : V
a✝ : Path a b
e : b ⟶ c
ih : height a ≤ height b
⊢ height a ≤ height c
[PROOFSTEP]
rfl
[GOAL]
case cons
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b✝¹ a b✝ b c : V
a✝ : Path a b
e : b ⟶ c
ih : height a ≤ height b
⊢ height a ≤ height c
[PROOFSTEP]
exact le_of_lt (lt_of_le_of_lt ih (height_lt e))
[GOAL]
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V}, Path a b → height a ≤ height b
⊢ ∀ (a : Path r b), a = default
[PROOFSTEP]
suffices ∀ p q : Path r b, p = q by
  intro p
  apply this
[GOAL]
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V}, Path a b → height a ≤ height b
this : ∀ (p q : Path r b), p = q
⊢ ∀ (a : Path r b), a = default
[PROOFSTEP]
intro p
[GOAL]
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V}, Path a b → height a ≤ height b
this : ∀ (p q : Path r b), p = q
p : Path r b
⊢ p = default
[PROOFSTEP]
apply this
[GOAL]
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V}, Path a b → height a ≤ height b
⊢ ∀ (p q : Path r b), p = q
[PROOFSTEP]
intro p q
[GOAL]
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V}, Path a b → height a ≤ height b
p q : Path r b
⊢ p = q
[PROOFSTEP]
induction' p with a c p e ih
[GOAL]
case nil
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V}, Path a b → height a ≤ height b
q✝ : Path r b
q : Path r r
⊢ Path.nil = q
[PROOFSTEP]
cases' q with b _ q f
[GOAL]
case cons
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V}, Path a b → height a ≤ height b
q✝ : Path r b
a c : V
p : Path r a
e : a ⟶ c
ih : ∀ (q : Path r a), p = q
q : Path r c
⊢ Path.cons p e = q
[PROOFSTEP]
cases' q with b _ q f
[GOAL]
case nil.nil
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V}, Path a b → height a ≤ height b
q : Path r b
⊢ Path.nil = Path.nil
[PROOFSTEP]
rfl
[GOAL]
case nil.cons
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b✝ : V
height_le : ∀ {a b : V}, Path a b → height a ≤ height b
q✝ : Path r b✝
b : V
q : Path r b
f : b ⟶ r
⊢ Path.nil = Path.cons q f
[PROOFSTEP]
exact False.elim (lt_irrefl _ (lt_of_le_of_lt (height_le q) (height_lt f)))
[GOAL]
case cons.nil
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V}, Path a b → height a ≤ height b
q : Path r b
a : V
p : Path r a
ih : ∀ (q : Path r a), p = q
e : a ⟶ r
⊢ Path.cons p e = Path.nil
[PROOFSTEP]
exact False.elim (lt_irrefl _ (lt_of_le_of_lt (height_le p) (height_lt e)))
[GOAL]
case cons.cons
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b✝ : V
height_le : ∀ {a b : V}, Path a b → height a ≤ height b
q✝ : Path r b✝
a c : V
p : Path r a
e : a ⟶ c
ih : ∀ (q : Path r a), p = q
b : V
q : Path r b
f : b ⟶ c
⊢ Path.cons p e = Path.cons q f
[PROOFSTEP]
rcases unique_arrow e f with ⟨⟨⟩, ⟨⟩⟩
[GOAL]
case cons.cons.intro.refl.refl
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V}, Path a b → height a ≤ height b
q✝ : Path r b
a c : V
p : Path r a
e : a ⟶ c
ih : ∀ (q : Path r a), p = q
q : Path r a
β : Sort ?u.237
⊢ Path.cons p e = Path.cons q e
[PROOFSTEP]
rw [ih]
[GOAL]
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
⊢ ∀ ⦃a b : WideSubquiver.toType V (geodesicSubtree r)⦄,
    (a ⟶ b) → (fun a => Path.length (shortestPath r a)) a < (fun a => Path.length (shortestPath r a)) b
[PROOFSTEP]
rintro a b ⟨e, p, h⟩
[GOAL]
case mk.intro
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a b : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ b
p : Path r a
h : shortestPath r b = Path.cons p e
⊢ (fun a => Path.length (shortestPath r a)) a < (fun a => Path.length (shortestPath r a)) b
[PROOFSTEP]
simp_rw [h, Path.length_cons, Nat.lt_succ_iff]
[GOAL]
case mk.intro
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a b : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ b
p : Path r a
h : shortestPath r b = Path.cons p e
⊢ Path.length (shortestPath r a) ≤ Path.length p
[PROOFSTEP]
apply shortest_path_spec
[GOAL]
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
⊢ ∀ ⦃a b c : WideSubquiver.toType V (geodesicSubtree r)⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
[PROOFSTEP]
rintro a b c ⟨e, p, h⟩ ⟨f, q, j⟩
[GOAL]
case mk.intro.mk.intro
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a b c : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ c
p : Path r a
h : shortestPath r c = Path.cons p e
f : b ⟶ c
q : Path r b
j : shortestPath r c = Path.cons q f
⊢ a = b ∧
    HEq { val := e, property := (_ : ∃ p, shortestPath r c = Path.cons p e) }
      { val := f, property := (_ : ∃ p, shortestPath r c = Path.cons p f) }
[PROOFSTEP]
cases h.symm.trans j
[GOAL]
case mk.intro.mk.intro.refl
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a c : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ c
p : Path r a
h j : shortestPath r c = Path.cons p e
⊢ a = a ∧
    HEq { val := e, property := (_ : ∃ p, shortestPath r c = Path.cons p e) }
      { val := e, property := (_ : ∃ p, shortestPath r c = Path.cons p e) }
[PROOFSTEP]
constructor
[GOAL]
case mk.intro.mk.intro.refl.left
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a c : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ c
p : Path r a
h j : shortestPath r c = Path.cons p e
⊢ a = a
[PROOFSTEP]
rfl
[GOAL]
case mk.intro.mk.intro.refl.right
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a c : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ c
p : Path r a
h j : shortestPath r c = Path.cons p e
⊢ HEq { val := e, property := (_ : ∃ p, shortestPath r c = Path.cons p e) }
    { val := e, property := (_ : ∃ p, shortestPath r c = Path.cons p e) }
[PROOFSTEP]
rfl
[GOAL]
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
⊢ ∀ (b : WideSubquiver.toType V (geodesicSubtree r)), b = r ∨ ∃ a, Nonempty (a ⟶ b)
[PROOFSTEP]
intro b
[GOAL]
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
b : WideSubquiver.toType V (geodesicSubtree r)
⊢ b = r ∨ ∃ a, Nonempty (a ⟶ b)
[PROOFSTEP]
rcases hp : shortestPath r b with (_ | ⟨p, e⟩)
[GOAL]
case nil
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
hp : shortestPath r r = Path.nil
⊢ r = r ∨ ∃ a, Nonempty (a ⟶ r)
[PROOFSTEP]
exact Or.inl rfl
[GOAL]
case cons
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
b : WideSubquiver.toType V (geodesicSubtree r)
b✝ : V
p : Path r b✝
e : b✝ ⟶ b
hp : shortestPath r b = Path.cons p e
⊢ b = r ∨ ∃ a, Nonempty (a ⟶ b)
[PROOFSTEP]
exact Or.inr ⟨_, ⟨⟨e, p, hp⟩⟩⟩
