awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
α : Type u
β : Type v
inst : DecidableEq β
inst_1 : Fintype α
inst_2 : Fintype β
f : α → β
n : ℕ
inst_3 : Nonempty β
hn : card α ≤ card β * n
⊢ ∃ (y : β), Finset.card.{u} (α := α) {x : α | f x = y} ≤ n

Tactic:
exists_card_fiber_le_of_card_le_nsmul _ hn

Premises used: Fintype.exists_card_fiber_le_of_card_le_nsmul
-- Module: Mathlib.Combinatorics.Pigeonhole
Goal:
s : Set ℕ
hs : s.Infinite
k : ℕ
hk : 0 < k
⊢ ∃ m ∈ s, ∃ n ∈ s, m < n ∧ m ≡ n [MOD k]

Tactic:
(hs.exists_lt_map_eq_of_mapsTo fun n _ => show n % k ∈ Iio k from Nat.mod_lt n hk) <|
    finite_lt_nat k

Premises used: Nat.mod_lt, Set.Infinite.exists_lt_map_eq_of_mapsTo, Nat.ModEq, Set.finite_lt_nat
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
b : V
rcases : ∀ (n : ℕ) (hn : height b < n), Nonempty (Path.{u_1, u} r b)
⊢ Nonempty (Path.{u_1, u} r b)

Tactic:
rcases show ∃ n, height b < n from ⟨_, Nat.lt_add_one _⟩ with ⟨n, hn⟩

Premises used: Nat.lt_add_one, HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
b : V
hn : height b < 0
⊢ Nonempty (Path.{u_1, u} r b)

Tactic:
False.elim (Nat.not_lt_zero _ hn)

Premises used: False.elim, Nat.not_lt_zero
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
b : V
hn : height b < 0
⊢ Nonempty (Path.{u_1, u} r b)

Tactic:
exact False.elim (Nat.not_lt_zero _ hn)

Premises used: False.elim, Nat.not_lt_zero
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
n : ℕ
ih : ∀ (b : V) (hn : height b < n), Nonempty (Path.{u_1, u} r b)
b : V
hn : height b < n + 1
succ : ∀ (hn : height r < n + 1), Nonempty (Path.{u_1, u} r r)
succ₁ : ∀ (a : V) (e : a ⟶ b), Nonempty (Path.{u_1, u} r b)
⊢ Nonempty (Path.{u_1, u} r b)

Tactic:
rcases root_or_arrow b with (⟨⟨⟩⟩ | ⟨a, ⟨e⟩⟩)
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
n : ℕ
ih : ∀ (b : V) (hn : height b < n), Nonempty (Path.{u_1, u} r b)
hn : height r < n + 1
⊢ Nonempty (Path.{u_1, u} r r)

Tactic:
⟨Path.nil⟩

Premises used: Quiver.Path.nil, Nonempty.intro
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
n : ℕ
ih : ∀ (b : V) (hn : height b < n), Nonempty (Path.{u_1, u} r b)
hn : height r < n + 1
⊢ Nonempty (Path.{u_1, u} r r)

Tactic:
exact ⟨Path.nil⟩
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
n : ℕ
ih : ∀ (b : V) (hn : height b < n), Nonempty (Path.{u_1, u} r b)
b : V
hn : height b < n + 1
a : V
e : a ⟶ b
succ : ∀ (p : Path.{u_1, u} r a), Nonempty (Path.{u_1, u} r b)
⊢ Nonempty (Path.{u_1, u} r b)

Tactic:
rcases ih a (lt_of_lt_of_le (height_lt e) (Nat.lt_succ_iff.mp hn)) with ⟨p⟩

Premises used: Nat.lt_succ_iff, Iff.mp, lt_of_lt_of_le
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
n : ℕ
ih : ∀ (b : V) (hn : height b < n), Nonempty (Path.{u_1, u} r b)
b : V
hn : height b < n + 1
a : V
e : a ⟶ b
p : Path.{u_1, u} r a
⊢ Nonempty (Path.{u_1, u} r b)

Tactic:
⟨p.cons e⟩

Premises used: Nonempty.intro, Quiver.Path.cons
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
n : ℕ
ih : ∀ (b : V) (hn : height b < n), Nonempty (Path.{u_1, u} r b)
b : V
hn : height b < n + 1
a : V
e : a ⟶ b
p : Path.{u_1, u} r a
⊢ Nonempty (Path.{u_1, u} r b)

Tactic:
exact ⟨p.cons e⟩
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
b : V
n : ℕ
hn : height b < n
zero : ∀ (b : V) (hn : height b < 0), Nonempty (Path.{u_1, u} r b)
succ :
  ∀ (n : ℕ) (ih : ∀ (b : V) (hn : height b < n), Nonempty (Path.{u_1, u} r b)) (b : V) (hn : height b < n + 1),
    Nonempty (Path.{u_1, u} r b)
⊢ Nonempty (Path.{u_1, u} r b)

Tactic:
induction n generalizing b with
      | zero => exact False.elim (Nat.not_lt_zero _ hn)
      | succ n ih =>
      rcases root_or_arrow b with (⟨⟨⟩⟩ | ⟨a, ⟨e⟩⟩)
      · exact ⟨Path.nil⟩
      · rcases ih a (lt_of_lt_of_le (height_lt e) (Nat.lt_succ_iff.mp hn)) with ⟨p⟩
        exact ⟨p.cons e⟩

Premises used: False.elim, Nat.not_lt_zero
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
b_1 a b : V
⊢ height a ≤ height a

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_2 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
b_1 a b b_2 c : V
a_1 : Path.{u_1, u} a b_2
e : b_2 ⟶ c
ih : height a ≤ height b_2
⊢ height a ≤ height c

Tactic:
le_of_lt (lt_of_le_of_lt ih (height_lt e))

Premises used: lt_of_le_of_lt, le_of_lt
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_2 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
b_1 a b b_2 c : V
a_1 : Path.{u_1, u} a b_2
e : b_2 ⟶ c
ih : height a ≤ height b_2
⊢ height a ≤ height c

Tactic:
exact le_of_lt (lt_of_le_of_lt ih (height_lt e))

Premises used: lt_of_le_of_lt, le_of_lt
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
b_1 a b : V
p : Path.{u_1, u} a b
nil : height a ≤ height a
cons : ∀ {b c : V} (a_1 : Path.{u_1, u} a b) (e : b ⟶ c) (ih : height a ≤ height b), height a ≤ height c
⊢ height a ≤ height b

Tactic:
induction p with
        | nil => rfl
        | cons _ e ih => exact le_of_lt (lt_of_le_of_lt ih (height_lt e))
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
b : V
⊢ ∀ {a b : V} (a_1 : Path.{u_1, u} a b), height a ≤ height b

Tactic:
have height_le : ∀ {a b}, Path a b → height a ≤ height b := by
        intro a b p
        induction p with
        | nil => rfl
        | cons _ e ih => exact le_of_lt (lt_of_le_of_lt ih (height_lt e))
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path.{u_1, u} a b), height a ≤ height b
this : ∀ (p q : Path.{u_1, u} r b), p = q
p : Path.{u_1, u} r b
⊢ p = default

Tactic:
apply this
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path.{u_1, u} a b), height a ≤ height b
suffices : ∀ (p q : Path.{u_1, u} r b), p = q
⊢ ∀ (a : Path.{u_1, u} r b), a = default

Tactic:
suffices ∀ p q : Path r b, p = q by
        intro p
        apply this
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path.{u_1, u} a b), height a ≤ height b
q : Path.{u_1, u} r r
nil : Eq (α := Path.{u_1, u} r r) Path.nil Path.nil
nil₁ : ∀ {b : V} (q : Path.{u_1, u} r b) (f : b ⟶ r), Path.nil = q.cons f
⊢ Path.nil = q

Tactic:
rcases q with _ | ⟨q, f⟩
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path.{u_1, u} a b), height a ≤ height b
⊢ Eq (α := Path.{u_1, u} r r) Path.nil Path.nil

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path.{u_1, u} a b), height a ≤ height b
b_1 : V
q : Path.{u_1, u} r b_1
f : b_1 ⟶ r
⊢ Path.nil = q.cons f

Tactic:
False.elim (lt_irrefl _ (lt_of_le_of_lt (height_le q) (height_lt f)))

Premises used: lt_of_le_of_lt, lt_irrefl, False.elim
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path.{u_1, u} a b), height a ≤ height b
b_1 : V
q : Path.{u_1, u} r b_1
f : b_1 ⟶ r
⊢ Path.nil = q.cons f

Tactic:
exact False.elim (lt_irrefl _ (lt_of_le_of_lt (height_le q) (height_lt f)))

Premises used: lt_of_le_of_lt, lt_irrefl, False.elim
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path.{u_1, u} a b), height a ≤ height b
b_1 c : V
p : Path.{u_1, u} r b_1
e : b_1 ⟶ c
ih : ∀ (q : Path.{u_1, u} r b_1), p = q
q : Path.{u_1, u} r c
cons : ∀ (e : b_1 ⟶ r), p.cons e = Path.nil
cons₁ : ∀ {b : V} (q : Path.{u_1, u} r b) (f : b ⟶ c), p.cons e = q.cons f
⊢ p.cons e = q

Tactic:
rcases q with _ | ⟨q, f⟩
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path.{u_1, u} a b), height a ≤ height b
b_1 : V
p : Path.{u_1, u} r b_1
ih : ∀ (q : Path.{u_1, u} r b_1), p = q
e : b_1 ⟶ r
⊢ p.cons e = Path.nil

Tactic:
False.elim (lt_irrefl _ (lt_of_le_of_lt (height_le p) (height_lt e)))

Premises used: lt_of_le_of_lt, lt_irrefl, False.elim
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path.{u_1, u} a b), height a ≤ height b
b_1 : V
p : Path.{u_1, u} r b_1
ih : ∀ (q : Path.{u_1, u} r b_1), p = q
e : b_1 ⟶ r
⊢ p.cons e = Path.nil

Tactic:
exact False.elim (lt_irrefl _ (lt_of_le_of_lt (height_le p) (height_lt e)))

Premises used: lt_of_le_of_lt, lt_irrefl, False.elim
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path.{u_1, u} a b), height a ≤ height b
b_1 c : V
p : Path.{u_1, u} r b_1
e : b_1 ⟶ c
ih : ∀ (q : Path.{u_1, u} r b_1), p = q
b_2 : V
q : Path.{u_1, u} r b_2
f : b_2 ⟶ c
cons : ∀ (q : Path.{u_1, u} r b_1) {β : Type u_1}, p.cons e = q.cons e
⊢ p.cons e = q.cons f

Tactic:
rcases unique_arrow e f with ⟨⟨⟩, ⟨⟩⟩
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path.{u_1, u} a b), height a ≤ height b
b_1 c : V
p : Path.{u_1, u} r b_1
e : b_1 ⟶ c
ih : ∀ (q : Path.{u_1, u} r b_1), p = q
q : Path.{u_1, u} r b_1
β : Type u_1
cons : q.cons e = q.cons e
cons₁ : Path.{u_1, u} r b_1
cons₂ : q.cons e = q.cons e
cons₃ : Path.{u_1, u} r b_1
⊢ p.cons e = q.cons e

Tactic:
rw [ih]
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{u_1, u} V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ (a : V), Nonempty.{u_1 + 1} (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path.{u_1, u} a b), height a ≤ height b
p q : Path.{u_1, u} r b
nil : ∀ (q : Path.{u_1, u} r r), Path.nil = q
cons :
  ∀ {b c : V} (p : Path.{u_1, u} r b) (e : b ⟶ c) (ih : ∀ (q : Path.{u_1, u} r b), p = q) (q : Path.{u_1, u} r c),
    p.cons e = q
⊢ p = q

Tactic:
induction p with
      | nil =>
        rcases q with _ | ⟨q, f⟩
        · rfl
        · exact False.elim (lt_irrefl _ (lt_of_le_of_lt (height_le q) (height_lt f)))
      | cons p e ih =>
        rcases q with _ | ⟨q, f⟩
        · exact False.elim (lt_irrefl _ (lt_of_le_of_lt (height_le p) (height_lt e)))
        · rcases unique_arrow e f with ⟨⟨⟩, ⟨⟩⟩
          rw [ih]
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{v, u} V
r : V
inst_1 : RootedConnected.{u, v} r
a : V
p : Path.{v, u} r a
⊢ Path.length.{u, v} (shortestPath r a) ≤ p.length

Tactic:
not_lt.mp (WellFounded.not_lt_min (measure _).wf Set.univ trivial)

Premises used: trivial, Set.univ, not_lt, WellFoundedRelation.wf, Iff.mp, WellFounded.not_lt_min
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{v, u} V
r : V
inst_1 : RootedConnected.{u, v} r
a b : WideSubquiver.toType.{u, v} V (geodesicSubtree r)
e : a ⟶ b
p : Path.{v, u} r a
h : shortestPath r b = p.cons e
simp_rw : Path.length.{u, v} (shortestPath r a) ≤ p.length
⊢ LT.lt (α := ℕ)
    ((fun (a : WideSubquiver.toType.{u, v} V (geodesicSubtree r)) ↦ Path.length.{u, v} (shortestPath r a)) a)
    ((fun (a : WideSubquiver.toType.{u, v} V (geodesicSubtree r)) ↦ Path.length.{u, v} (shortestPath r a)) b)

Tactic:
simp_rw [h, Path.length_cons, Nat.lt_succ_iff]

Premises used: Quiver.Path.length_cons, Nat.lt_succ_iff
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{v, u} V
r : V
inst_1 : RootedConnected.{u, v} r
a b : WideSubquiver.toType.{u, v} V (geodesicSubtree r)
e : a ⟶ b
p : Path.{v, u} r a
h : shortestPath r b = p.cons e
⊢ Path.length.{u, v} (shortestPath r a) ≤ p.length

Tactic:
apply shortest_path_spec

Premises used: Quiver.shortest_path_spec
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{v, u} V
r : V
inst_1 : RootedConnected.{u, v} r
a b c : WideSubquiver.toType.{u, v} V (geodesicSubtree r)
e : a ⟶ c
p : Path.{v, u} r a
h : shortestPath r c = p.cons e
f : b ⟶ c
q : Path.{v, u} r b
j : shortestPath r c = q.cons f
refl :
  ∀ (j : shortestPath r c = p.cons e),
    a = a ∧
      HEq (α := a ⟶ c)
        (Subtype.mk (p := fun (f : a ⟶ c) ↦ Membership.mem (γ := Set (a ⟶ c)) (geodesicSubtree r a c) f) e ⋯) (β :=
        a ⟶ c) (Subtype.mk (p := fun (f : a ⟶ c) ↦ Membership.mem (γ := Set (a ⟶ c)) (geodesicSubtree r a c) f) e ⋯)
⊢ a = b ∧
    HEq (α := a ⟶ c)
      (Subtype.mk (p := fun (f : a ⟶ c) ↦ Membership.mem (γ := Set (a ⟶ c)) (geodesicSubtree r a c) f) e ⋯) (β := b ⟶ c)
      (Subtype.mk (p := fun (f : b ⟶ c) ↦ Membership.mem (γ := Set (b ⟶ c)) (geodesicSubtree r b c) f) f ⋯)

Tactic:
cases h.symm.trans j

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{v, u} V
r : V
inst_1 : RootedConnected.{u, v} r
a c : WideSubquiver.toType.{u, v} V (geodesicSubtree r)
e : a ⟶ c
p : Path.{v, u} r a
h j : shortestPath r c = p.cons e
refl : a = a
refl₁ :
  HEq (α := a ⟶ c) (Subtype.mk (p := fun (f : a ⟶ c) ↦ Membership.mem (γ := Set (a ⟶ c)) (geodesicSubtree r a c) f) e ⋯)
    (β := a ⟶ c) (Subtype.mk (p := fun (f : a ⟶ c) ↦ Membership.mem (γ := Set (a ⟶ c)) (geodesicSubtree r a c) f) e ⋯)
⊢ a = a ∧
    HEq (α := a ⟶ c)
      (Subtype.mk (p := fun (f : a ⟶ c) ↦ Membership.mem (γ := Set (a ⟶ c)) (geodesicSubtree r a c) f) e ⋯) (β := a ⟶ c)
      (Subtype.mk (p := fun (f : a ⟶ c) ↦ Membership.mem (γ := Set (a ⟶ c)) (geodesicSubtree r a c) f) e ⋯)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{v, u} V
r : V
inst_1 : RootedConnected.{u, v} r
a c : WideSubquiver.toType.{u, v} V (geodesicSubtree r)
e : a ⟶ c
p : Path.{v, u} r a
h j : shortestPath r c = p.cons e
⊢ a = a

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{v, u} V
r : V
inst_1 : RootedConnected.{u, v} r
a c : WideSubquiver.toType.{u, v} V (geodesicSubtree r)
e : a ⟶ c
p : Path.{v, u} r a
h j : shortestPath r c = p.cons e
⊢ HEq (α := a ⟶ c) (Subtype.mk (p := fun (f : a ⟶ c) ↦ Membership.mem (γ := Set (a ⟶ c)) (geodesicSubtree r a c) f) e ⋯)
    (β := a ⟶ c) (Subtype.mk (p := fun (f : a ⟶ c) ↦ Membership.mem (γ := Set (a ⟶ c)) (geodesicSubtree r a c) f) e ⋯)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{v, u} V
r : V
inst_1 : RootedConnected.{u, v} r
b : WideSubquiver.toType.{u, v} V (geodesicSubtree r)
nil :
  ∀ (hp : Eq (α := Path.{v, u} r r) (shortestPath r r) Path.nil),
    r = r ∨ ∃ (a : WideSubquiver.toType.{u, v} V (geodesicSubtree r)), Nonempty.{v + 1} (a ⟶ r)
cons :
  ∀ {b_1 : V} (p : Path.{v, u} r b_1) (e : b_1 ⟶ b) (hp : shortestPath r b = p.cons e),
    b = r ∨ ∃ (a : WideSubquiver.toType.{u, v} V (geodesicSubtree r)), Nonempty.{v + 1} (a ⟶ b)
⊢ b = r ∨ ∃ (a : WideSubquiver.toType.{u, v} V (geodesicSubtree r)), Nonempty.{v + 1} (a ⟶ b)

Tactic:
rcases hp : shortestPath r b with (_ | ⟨p, e⟩)

Premises used: Quiver.shortestPath
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{v, u} V
r : V
inst_1 : RootedConnected.{u, v} r
hp : Eq (α := Path.{v, u} r r) (shortestPath r r) Path.nil
⊢ r = r ∨ ∃ (a : WideSubquiver.toType.{u, v} V (geodesicSubtree r)), Nonempty.{v + 1} (a ⟶ r)

Tactic:
Or.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{v, u} V
r : V
inst_1 : RootedConnected.{u, v} r
hp : Eq (α := Path.{v, u} r r) (shortestPath r r) Path.nil
⊢ r = r ∨ ∃ (a : WideSubquiver.toType.{u, v} V (geodesicSubtree r)), Nonempty.{v + 1} (a ⟶ r)

Tactic:
exact Or.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{v, u} V
r : V
inst_1 : RootedConnected.{u, v} r
b : WideSubquiver.toType.{u, v} V (geodesicSubtree r)
b_1 : V
p : Path.{v, u} r b_1
e : b_1 ⟶ b
hp : shortestPath r b = p.cons e
⊢ b = r ∨ ∃ (a : WideSubquiver.toType.{u, v} V (geodesicSubtree r)), Nonempty.{v + 1} (a ⟶ b)

Tactic:
Or.inr ⟨_, ⟨⟨e, p, hp⟩⟩⟩

Premises used: Nonempty.intro, Subtype.mk, Exists.intro, Or.inr
-- Module: Mathlib.Combinatorics.Quiver.Arborescence
Goal:
V : Type u
inst : Quiver.{v, u} V
r : V
inst_1 : RootedConnected.{u, v} r
b : WideSubquiver.toType.{u, v} V (geodesicSubtree r)
b_1 : V
p : Path.{v, u} r b_1
e : b_1 ⟶ b
hp : shortestPath r b = p.cons e
⊢ b = r ∨ ∃ (a : WideSubquiver.toType.{u, v} V (geodesicSubtree r)), Nonempty.{v + 1} (a ⟶ b)

Tactic:
exact Or.inr ⟨_, ⟨⟨e, p, hp⟩⟩⟩

Premises used: Or.inr
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
rw : (u' ⟶ v) = (u' ⟶ v')
rw₁ rw₂ : (u' ⟶ v') = (u' ⟶ v')
⊢ (u ⟶ v) = (u' ⟶ v')

Tactic:
rw [hu, hv]
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
this : (u' ⟶ v) = (u' ⟶ v')
this₁ this₂ : (u' ⟶ v') = (u' ⟶ v')
⊢ (u ⟶ v) = (u' ⟶ v')

Tactic:
{rw [hu, hv]}
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
subst_vars : ∀ (e : u' ⟶ v'), cast ⋯ ⋯ e = _root_.cast ⋯ e
⊢ cast hu hv e = _root_.cast ⋯ e

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u' v' : U
e : u' ⟶ v'
⊢ cast ⋯ ⋯ e = _root_.cast ⋯ e

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v : U
e : u ⟶ v
⊢ cast ⋯ ⋯ e = e

Tactic:
rfl

Premises used: Quiver.Hom.cast, rfl
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v u' v' u'' v'' : U
e : u ⟶ v
hu : u = u'
hv : v = v'
hu' : u' = u''
hv' : v' = v''
subst_vars : ∀ (e : u'' ⟶ v''), cast ⋯ ⋯ (cast ⋯ ⋯ e) = cast ⋯ ⋯ e
⊢ cast hu' hv' (cast hu hv e) = cast ⋯ ⋯ e

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u'' v'' : U
e : u'' ⟶ v''
⊢ cast ⋯ ⋯ (cast ⋯ ⋯ e) = cast ⋯ ⋯ e

Tactic:
rfl