awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (goal)
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
half_sharp :
  Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])) <
    (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
⊢ HSMul.hSMul (α := ℕ) (β := C) 2
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
    HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
have rw : HAdd.hAdd (α := C)
    (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])))
    (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
  (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum + (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
Tactic: rw [two_nsmul, two_nsmul]
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (hypothesis)
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
⊢ False
have sharp : HSMul.hSMul (α := ℕ) (β := C) 2
    (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
Tactic: have sharp :
    2 • ((ω.tt ![![a, b], ![b, a]]).map (fun _ => f ![a, b])).sum <
    2 • ((ω.tt ![![a, b], ![b, a]]).map f).sum := by
    have half_sharp :
      ((ω.tt ![![a, b], ![b, a]]).map (fun _ => f ![a, b])).sum <
      ((ω.tt ![![a, b], ![b, a]]).map f).sum := by
      apply Multiset.sum_lt_sum
      · intro r rin
        exact le_of_lt (mcfab.rows_lt_aux hab symmega rin)
      · obtain ⟨g, _⟩ := valid.contains
        have : (fun i => g ((Function.swap ![![a, b], ![b, a]]) i)) ∈ ω.tt ![![a, b], ![b, a]] := by
          simp only [FractionalOperation.tt, Multiset.mem_map]
          use g
        exact ⟨_, this, mcfab.rows_lt_aux hab symmega this⟩
    rw [two_nsmul, two_nsmul]
    exact add_lt_add half_sharp half_sharp
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (goal)
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
sharp :
  HSMul.hSMul (α := ℕ) (β := C) 2
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
    HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
⊢ HSMul.hSMul (α := ℕ) (β := C) 2 (Multiset.sum (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω)) <
    ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
have h : Eq.{u_3 + 1} (α := Multiset C) (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω)
  (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))
Tactic: convert! lt_of_lt_of_le sharp contr
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (hypothesis)
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
sharp :
  HSMul.hSMul (α := ℕ) (β := C) 2
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
    HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
⊢ False
have impos : HSMul.hSMul (α := ℕ) (β := C) 2 (Multiset.sum (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω)) <
  ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
Tactic: have impos : 2 • (ω.map (fun _ => f ![a, b])).sum < ω.size • 2 • f ![a, b] := by
    convert! lt_of_lt_of_le sharp contr
    simp [FractionalOperation.tt, Multiset.map_map]
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (hypothesis)
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
sharp :
  HSMul.hSMul (α := ℕ) (β := C) 2
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
    HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos :
  HSMul.hSMul (α := ℕ) (β := C) 2 (Multiset.sum (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω)) <
    ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
⊢ False
have rhs_swap : ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b]) = HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b])
Tactic: have rhs_swap : ω.size • 2 • f ![a, b] = 2 • ω.size • f ![a, b] := nsmul_left_comm ..
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (hypothesis)
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
sharp :
  HSMul.hSMul (α := ℕ) (β := C) 2
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
    HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos :
  HSMul.hSMul (α := ℕ) (β := C) 2 (Multiset.sum (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω)) <
    ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
rhs_swap : ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b]) = HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b])
⊢ False
have distrib : Multiset.sum (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω) = ω.size • f ![a, b]
Tactic: have distrib : (ω.map (fun _ => f ![a, b])).sum = ω.size • f ![a, b] := by simp
-- Lean 4 proof step from Mathlib.Combinatorics.Optimization.ValuedCSP (hypothesis)
Goal:
D : Type u_1
C : Type u_3
inst : AddCommMonoid C
inst_1 : PartialOrder C
inst_2 : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
contr :
  HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
sharp :
  HSMul.hSMul (α := ℕ) (β := C) 2
      (Multiset.sum (Multiset.map (fun (x : Fin (Nat.succ 0).succ → D) ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]]))) <
    HSMul.hSMul (α := ℕ) 2 (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos :
  HSMul.hSMul (α := ℕ) (β := C) 2 (Multiset.sum (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω)) <
    ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b])
rhs_swap : ω.size • HSMul.hSMul (α := ℕ) 2 (f ![a, b]) = HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b])
distrib : Multiset.sum (Multiset.map (fun (x : (Fin 2 → D) → D) ↦ f ![a, b]) ω) = ω.size • f ![a, b]
⊢ False
have impos₁ : HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b]) < HSMul.hSMul (α := ℕ) 2 (ω.size • f ![a, b])
Tactic: rw [rhs_swap, distrib] at impos
Cleared hypotheses: impos, rhs_swap, distrib
-- Lean 4 proof step from Mathlib.Combinatorics.Pigeonhole (goal)
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst_1 : CommSemiring M
inst_2 : LinearOrder M
inst_3 : IsStrictOrderedRing M
hf : ∀ a ∈ s, f a ∈ t
ht : #t • b < (↑(#s) : M)
⊢ ∃ y ∈ t, b < (↑(#({x ∈ s | f x = y})) : M)
have simp_rw : ∀ (ht : #t • b < ∑ x ∈ s, 1), ∃ y ∈ t, b < ∑ x ∈ s with f x = y, 1
Tactic: simp_rw [cast_card] at ht ⊢
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Combinatorics.Pigeonhole (goal)
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst_1 : CommSemiring M
inst_2 : LinearOrder M
inst_3 : IsStrictOrderedRing M
ht : (↑(#s) : M) < #t • b
⊢ ∃ y ∈ t, (↑(#({x ∈ s | f x = y})) : M) < b
have simp_rw : ∀ (ht : ∑ x ∈ s, 1 < #t • b), ∃ y ∈ t, ∑ x ∈ s with f x = y, 1 < b
Tactic: simp_rw [cast_card] at ht ⊢
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Combinatorics.Pigeonhole (goal)
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst_1 : CommSemiring M
inst_2 : LinearOrder M
inst_3 : IsStrictOrderedRing M
hf : ∀ a ∈ s, f a ∈ t
ht : t.Nonempty
hb : #t • b ≤ (↑(#s) : M)
⊢ ∃ y ∈ t, b ≤ (↑(#({x ∈ s | f x = y})) : M)
have simp_rw : ∀ (hb : #t • b ≤ ∑ x ∈ s, 1), ∃ y ∈ t, b ≤ ∑ x ∈ s with f x = y, 1
Tactic: simp_rw [cast_card] at hb ⊢
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Combinatorics.Pigeonhole (goal)
Goal:
α : Type u
β : Type v
M : Type w
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst_1 : CommSemiring M
inst_2 : LinearOrder M
inst_3 : IsStrictOrderedRing M
ht : t.Nonempty
hb : (↑(#s) : M) ≤ #t • b
⊢ ∃ y ∈ t, (↑(#({x ∈ s | f x = y})) : M) ≤ b
have simp_rw : ∀ (hb : ∑ x ∈ s, 1 ≤ #t • b), ∃ y ∈ t, ∑ x ∈ s with f x = y, 1 ≤ b
Tactic: simp_rw [cast_card] at hb ⊢
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Arborescence (goal)
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
⊢ Nonempty (Path.{u_1, u} r b)
have rcases : ∀ (n : ℕ) (hn : height b < n), Nonempty (Path.{u_1, u} r b)
Tactic: rcases show ∃ n, height b < n from ⟨_, Nat.lt_add_one _⟩ with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Arborescence (goal)
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
⊢ Nonempty (Path.{u_1, u} r b)
have succ : ∀ (hn : height r < n + 1), Nonempty (Path.{u_1, u} r r)
Tactic: rcases root_or_arrow b with (⟨⟨⟩⟩ | ⟨a, ⟨e⟩⟩)
Cleared hypotheses: b, hn
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Arborescence (goal)
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)
⊢ Nonempty (Path.{u_1, u} r b)
have succ₁ : ∀ (a : V) (e : a ⟶ b), Nonempty (Path.{u_1, u} r b)
Tactic: rcases root_or_arrow b with (⟨⟨⟩⟩ | ⟨a, ⟨e⟩⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Arborescence (goal)
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
⊢ Nonempty (Path.{u_1, u} r b)
have succ : ∀ (p : Path.{u_1, u} r a), 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⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Arborescence (goal)
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
⊢ Nonempty (Path.{u_1, u} r b)
have zero : ∀ (b : V) (hn : height b < 0), 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⟩
Cleared hypotheses: b, n, hn
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Arborescence (goal)
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)
⊢ Nonempty (Path.{u_1, u} r b)
have 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)
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⟩
Cleared hypotheses: b, n, hn
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Arborescence (goal)
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
⊢ height a ≤ height b
have nil : height a ≤ height a
Tactic: induction p with
        | nil => rfl
        | cons _ e ih => exact le_of_lt (lt_of_le_of_lt ih (height_lt e))
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Arborescence (goal)
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
⊢ height a ≤ height b
have cons : ∀ {b c : V} (a_1 : Path.{u_1, u} a b) (e : b ⟶ c) (ih : height a ≤ height b), height a ≤ height c
Tactic: induction p with
        | nil => rfl
        | cons _ e ih => exact le_of_lt (lt_of_le_of_lt ih (height_lt e))
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Arborescence (hypothesis)
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 : Path.{u_1, u} r b), a = default
have height_le : ∀ {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))
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Arborescence (goal)
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
⊢ ∀ (a : Path.{u_1, u} r b), a = default
have suffices : ∀ (p q : Path.{u_1, u} r b), p = q
Tactic: suffices ∀ p q : Path r b, p = q by
        intro p
        apply this
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Arborescence (goal)
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
⊢ Path.nil = q
have nil : Eq (α := Path.{u_1, u} r r) Path.nil Path.nil
Tactic: rcases q with _ | ⟨q, f⟩
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Arborescence (goal)
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
⊢ Path.nil = q
have nil₁ : ∀ {b : V} (q : Path.{u_1, u} r b) (f : b ⟶ r), Path.nil = q.cons f
Tactic: rcases q with _ | ⟨q, f⟩
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Arborescence (goal)
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
⊢ p.cons e = q
have cons : ∀ (e : b_1 ⟶ r), p.cons e = Path.nil
Tactic: rcases q with _ | ⟨q, f⟩
Cleared hypotheses: c, e, q
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Arborescence (goal)
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
⊢ p.cons e = q
have cons₁ : ∀ {b : V} (q : Path.{u_1, u} r b) (f : b ⟶ c), p.cons e = q.cons f
Tactic: rcases q with _ | ⟨q, f⟩
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Arborescence (goal)
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
⊢ p.cons e = q.cons f
have cons : ∀ (q : Path.{u_1, u} r b_1) {β : Type u_1}, p.cons e = q.cons e
Tactic: rcases unique_arrow e f with ⟨⟨⟩, ⟨⟩⟩
Cleared hypotheses: b_2, q, f
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Arborescence (goal)
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
⊢ p.cons e = q.cons e
have cons : q.cons e = q.cons e
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Arborescence (goal)
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
⊢ p = q
have nil : ∀ (q : Path.{u_1, u} r r), Path.nil = 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]
Cleared hypotheses: p, q
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Arborescence (goal)
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
⊢ p = q
have 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
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]
Cleared hypotheses: p, q
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Arborescence (goal)
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
⊢ 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)
have simp_rw : Path.length.{u, v} (shortestPath r a) ≤ p.length
Tactic: simp_rw [h, Path.length_cons, Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Arborescence (goal)
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
⊢ 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 ⋯)
have 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 sorry) (β := a ⟶ c)
      (Subtype.mk (p := fun (f : a ⟶ c) ↦ Membership.mem (γ := Set (a ⟶ c)) (geodesicSubtree r a c) f) e sorry)
Tactic: cases h.symm.trans j
Cleared hypotheses: b, f, q, j