awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Decomposition (hypothesis)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
n : ℕ
ih :
  ∀ {a b : V} (p : Path.{u_2, u_1} a b) (S : Set V) (ha_not_in_S : ¬a ∈ S) (hb_in_S : b ∈ S) (h_len : p.length = n),
    ∃ (u : V),
      ¬u ∈ S ∧
        ∃ (v : V),
          v ∈ S ∧
            ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
a b : V
p : Path.{u_2, u_1} a b
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
h_len : p.length = n + 1
⊢ ∃ (u : V),
    ¬u ∈ S ∧
      ∃ (v : V),
        v ∈ S ∧
          ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
have h_pos : 0 < p.length
Tactic: have h_pos : 0 < p.length := by simp [h_len]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Decomposition (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
n : ℕ
ih :
  ∀ {a b : V} (p : Path.{u_2, u_1} a b) (S : Set V) (ha_not_in_S : ¬a ∈ S) (hb_in_S : b ∈ S) (h_len : p.length = n),
    ∃ (u : V),
      ¬u ∈ S ∧
        ∃ (v : V),
          v ∈ S ∧
            ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
a b : V
p : Path.{u_2, u_1} a b
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
h_len : p.length = n + 1
h_pos : 0 < p.length
⊢ ∃ (u : V),
    ¬u ∈ S ∧
      ∃ (v : V),
        v ∈ S ∧
          ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
have succ : ∀ (c : V) (p' : Path.{u_2, u_1} a c) (e : c ⟶ b) (h_len : (p'.cons e).length = n + 1) (h_pos : 0 < (p'.cons e).length),
  ∃ (u : V),
    ¬u ∈ S ∧
      ∃ (v : V),
        v ∈ S ∧
          ∃ (e_1 : u ⟶ v),
            ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p'.cons e = p₁.comp (e_1.toPath.comp p₂)
Tactic: obtain ⟨c, p', e, rfl⟩ := (length_ne_zero_iff_eq_cons p).mp h_pos.ne'
Cleared hypotheses: p, h_len, h_pos
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Decomposition (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
n : ℕ
ih :
  ∀ {a b : V} (p : Path.{u_2, u_1} a b) (S : Set V) (ha_not_in_S : ¬a ∈ S) (hb_in_S : b ∈ S) (h_len : p.length = n),
    ∃ (u : V),
      ¬u ∈ S ∧
        ∃ (v : V),
          v ∈ S ∧
            ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
a b : V
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
c : V
p' : Path.{u_2, u_1} a c
e : c ⟶ b
h_len : (p'.cons e).length = n + 1
h_pos : 0 < (p'.cons e).length
⊢ ∃ (u : V),
    ¬u ∈ S ∧
      ∃ (v : V),
        v ∈ S ∧
          ∃ (e_1 : u ⟶ v),
            ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p'.cons e = p₁.comp (e_1.toPath.comp p₂)
have pos : ∀ (hc_in_S : c ∈ S),
  ∃ (u : V),
    ¬u ∈ S ∧
      ∃ (v : V),
        v ∈ S ∧
          ∃ (e_1 : u ⟶ v),
            ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p'.cons e = p₁.comp (e_1.toPath.comp p₂)
Tactic: by_cases hc_in_S : c ∈ S
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Decomposition (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
n : ℕ
ih :
  ∀ {a b : V} (p : Path.{u_2, u_1} a b) (S : Set V) (ha_not_in_S : ¬a ∈ S) (hb_in_S : b ∈ S) (h_len : p.length = n),
    ∃ (u : V),
      ¬u ∈ S ∧
        ∃ (v : V),
          v ∈ S ∧
            ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
a b : V
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
c : V
p' : Path.{u_2, u_1} a c
e : c ⟶ b
h_len : (p'.cons e).length = n + 1
h_pos : 0 < (p'.cons e).length
pos :
  ∀ (hc_in_S : c ∈ S),
    ∃ (u : V),
      ¬u ∈ S ∧
        ∃ (v : V),
          v ∈ S ∧
            ∃ (e_1 : u ⟶ v),
              ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p'.cons e = p₁.comp (e_1.toPath.comp p₂)
⊢ ∃ (u : V),
    ¬u ∈ S ∧
      ∃ (v : V),
        v ∈ S ∧
          ∃ (e_1 : u ⟶ v),
            ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p'.cons e = p₁.comp (e_1.toPath.comp p₂)
have neg : ∀ (hc_in_S : ¬c ∈ S),
  ∃ (u : V),
    ¬u ∈ S ∧
      ∃ (v : V),
        v ∈ S ∧
          ∃ (e_1 : u ⟶ v),
            ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p'.cons e = p₁.comp (e_1.toPath.comp p₂)
Tactic: by_cases hc_in_S : c ∈ S
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Decomposition (hypothesis)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
n : ℕ
ih :
  ∀ {a b : V} (p : Path.{u_2, u_1} a b) (S : Set V) (ha_not_in_S : ¬a ∈ S) (hb_in_S : b ∈ S) (h_len : p.length = n),
    ∃ (u : V),
      ¬u ∈ S ∧
        ∃ (v : V),
          v ∈ S ∧
            ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
a b : V
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
c : V
p' : Path.{u_2, u_1} a c
e : c ⟶ b
h_len : (p'.cons e).length = n + 1
h_pos : 0 < (p'.cons e).length
hc_in_S : c ∈ S
⊢ ∃ (u : V),
    ¬u ∈ S ∧
      ∃ (v : V),
        v ∈ S ∧
          ∃ (e_1 : u ⟶ v),
            ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p'.cons e = p₁.comp (e_1.toPath.comp p₂)
have p'_len : p'.length = n
Tactic: have p'_len : p'.length = n := by simp_all
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Decomposition (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
n : ℕ
ih :
  ∀ {a b : V} (p : Path.{u_2, u_1} a b) (S : Set V) (ha_not_in_S : ¬a ∈ S) (hb_in_S : b ∈ S) (h_len : p.length = n),
    ∃ (u : V),
      ¬u ∈ S ∧
        ∃ (v : V),
          v ∈ S ∧
            ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
a b : V
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
c : V
p' : Path.{u_2, u_1} a c
e : c ⟶ b
h_len : (p'.cons e).length = n + 1
h_pos : 0 < (p'.cons e).length
hc_in_S : c ∈ S
p'_len : p'.length = n
⊢ ∃ (u : V),
    ¬u ∈ S ∧
      ∃ (v : V),
        v ∈ S ∧
          ∃ (e_1 : u ⟶ v),
            ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p'.cons e = p₁.comp (e_1.toPath.comp p₂)
have pos : ∀ (u : V) (hu_not_S : ¬u ∈ S) (v : V) (hv_S : v ∈ S) (e_uv : u ⟶ v) (p₁ : Path.{u_2, u_1} a u)
  (p₂ : Path.{u_2, u_1} v c) (hp' : p' = p₁.comp (e_uv.toPath.comp p₂)),
  ∃ (u : V),
    ¬u ∈ S ∧
      ∃ (v : V),
        v ∈ S ∧
          ∃ (e_1 : u ⟶ v),
            ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p'.cons e = p₁.comp (e_1.toPath.comp p₂)
Tactic: obtain ⟨u, hu_not_S, v, hv_S, e_uv, p₁, p₂, hp'⟩ :=
        ih p' S ha_not_in_S hc_in_S p'_len
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Decomposition (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
n : ℕ
ih :
  ∀ {a b : V} (p : Path.{u_2, u_1} a b) (S : Set V) (ha_not_in_S : ¬a ∈ S) (hb_in_S : b ∈ S) (h_len : p.length = n),
    ∃ (u : V),
      ¬u ∈ S ∧
        ∃ (v : V),
          v ∈ S ∧
            ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
a b : V
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
c : V
p' : Path.{u_2, u_1} a c
e : c ⟶ b
h_len : (p'.cons e).length = n + 1
h_pos : 0 < (p'.cons e).length
hc_in_S : c ∈ S
p'_len : p'.length = n
u : V
hu_not_S : ¬u ∈ S
v : V
hv_S : v ∈ S
e_uv : u ⟶ v
p₁ : Path.{u_2, u_1} a u
p₂ : Path.{u_2, u_1} v c
hp' : p' = p₁.comp (e_uv.toPath.comp p₂)
⊢ ∃ (u : V),
    ¬u ∈ S ∧
      ∃ (v : V),
        v ∈ S ∧
          ∃ (e_1 : u ⟶ v),
            ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p'.cons e = p₁.comp (e_1.toPath.comp p₂)
have pos : p'.cons e = p₁.comp (e_uv.toPath.comp (p₂.comp e.toPath))
Tactic: refine ⟨u, hu_not_S, v, hv_S, e_uv, p₁, p₂.comp e.toPath, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Decomposition (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
n : ℕ
ih :
  ∀ {a b : V} (p : Path.{u_2, u_1} a b) (S : Set V) (ha_not_in_S : ¬a ∈ S) (hb_in_S : b ∈ S) (h_len : p.length = n),
    ∃ (u : V),
      ¬u ∈ S ∧
        ∃ (v : V),
          v ∈ S ∧
            ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
a b : V
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
c : V
p' : Path.{u_2, u_1} a c
e : c ⟶ b
h_len : (p'.cons e).length = n + 1
h_pos : 0 < (p'.cons e).length
hc_in_S : ¬c ∈ S
⊢ ∃ (u : V),
    ¬u ∈ S ∧
      ∃ (v : V),
        v ∈ S ∧
          ∃ (e_1 : u ⟶ v),
            ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p'.cons e = p₁.comp (e_1.toPath.comp p₂)
have neg : p'.cons e = p'.comp (e.toPath.comp nil)
Tactic: refine ⟨c, hc_in_S, b, hb_in_S, e, p', Path.nil, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Decomposition (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
⊢ ∃ (u : V),
    ¬u ∈ S ∧
      ∃ (v : V),
        v ∈ S ∧
          ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
have induction : ∀ (x : ℕ) (h_len : p.length = x),
  ∃ (u : V),
    ¬u ∈ S ∧
      ∃ (v : V),
        v ∈ S ∧
          ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
Tactic: induction h_len : p.length generalizing a b S ha_not_in_S hb_in_S with
  | zero =>
    obtain rfl := eq_of_length_zero p h_len
    exact (ha_not_in_S hb_in_S).elim
  | succ n ih =>
    have h_pos : 0 < p.length := by simp [h_len]
    obtain ⟨c, p', e, rfl⟩ := (length_ne_zero_iff_eq_cons p).mp h_pos.ne'
    by_cases hc_in_S : c ∈ S
    · have p'_len : p'.length = n := by simp_all
      obtain ⟨u, hu_not_S, v, hv_S, e_uv, p₁, p₂, hp'⟩ :=
        ih p' S ha_not_in_S hc_in_S p'_len
      refine ⟨u, hu_not_S, v, hv_S, e_uv, p₁, p₂.comp e.toPath, ?_⟩
      simp [hp', comp_toPath_eq_cons]
    · refine ⟨c, hc_in_S, b, hb_in_S, e, p', Path.nil, ?_⟩
      simp [comp_toPath_eq_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Decomposition (hypothesis)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
S : Set V
ha_in_S : a ∈ S
hb_not_in_S : ¬b ∈ S
⊢ ∃ (u : V),
    u ∈ S ∧
      ∃ (v : V),
        ¬v ∈ S ∧
          ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
have ha_not_in_compl : ¬a ∈ Sᶜ
Tactic: have ha_not_in_compl : a ∉ Sᶜ := by simpa
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Decomposition (hypothesis)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
S : Set V
ha_in_S : a ∈ S
hb_not_in_S : ¬b ∈ S
ha_not_in_compl : ¬a ∈ Sᶜ
⊢ ∃ (u : V),
    u ∈ S ∧
      ∃ (v : V),
        ¬v ∈ S ∧
          ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
have hb_in_compl : b ∈ Sᶜ
Tactic: have hb_in_compl : b ∈ Sᶜ := by simpa
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Decomposition (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
S : Set V
ha_in_S : a ∈ S
hb_not_in_S : ¬b ∈ S
ha_not_in_compl : ¬a ∈ Sᶜ
hb_in_compl : b ∈ Sᶜ
⊢ ∃ (u : V),
    u ∈ S ∧
      ∃ (v : V),
        ¬v ∈ S ∧
          ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
have obtain : ∀ (u : V) (hu_not_in_compl : ¬u ∈ Sᶜ) (v : V) (hv_in_compl : v ∈ Sᶜ) (e : u ⟶ v) (p₁ : Path.{u_2, u_1} a u)
  (p₂ : Path.{u_2, u_1} v b) (hp : p = p₁.comp (e.toPath.comp p₂)),
  ∃ (u : V),
    u ∈ S ∧
      ∃ (v : V),
        ¬v ∈ S ∧
          ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
Tactic: obtain ⟨u, hu_not_in_compl, v, hv_in_compl, e, p₁, p₂, hp⟩ :=
    exists_notMem_mem_hom_path_path_of_notMem_mem p Sᶜ ha_not_in_compl hb_in_compl
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Decomposition (hypothesis)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
S : Set V
ha_in_S : a ∈ S
hb_not_in_S : ¬b ∈ S
ha_not_in_compl : ¬a ∈ Sᶜ
hb_in_compl : b ∈ Sᶜ
u : V
hu_not_in_compl : ¬u ∈ Sᶜ
v : V
hv_in_compl : v ∈ Sᶜ
e : u ⟶ v
p₁ : Path.{u_2, u_1} a u
p₂ : Path.{u_2, u_1} v b
hp : p = p₁.comp (e.toPath.comp p₂)
⊢ ∃ (u : V),
    u ∈ S ∧
      ∃ (v : V),
        ¬v ∈ S ∧
          ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
have hu_not_in_compl₁ : u ∈ S
Tactic: simp only [Set.mem_compl_iff, not_not] at hu_not_in_compl hv_in_compl
Cleared hypotheses: hu_not_in_compl, hv_in_compl
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Decomposition (hypothesis)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
S : Set V
ha_in_S : a ∈ S
hb_not_in_S : ¬b ∈ S
ha_not_in_compl : ¬a ∈ Sᶜ
hb_in_compl : b ∈ Sᶜ
u : V
hu_not_in_compl : ¬u ∈ Sᶜ
v : V
hv_in_compl : v ∈ Sᶜ
e : u ⟶ v
p₁ : Path.{u_2, u_1} a u
p₂ : Path.{u_2, u_1} v b
hp : p = p₁.comp (e.toPath.comp p₂)
hu_not_in_compl₁ : u ∈ S
⊢ ∃ (u : V),
    u ∈ S ∧
      ∃ (v : V),
        ¬v ∈ S ∧
          ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
have hv_in_compl₁ : ¬v ∈ S
Tactic: simp only [Set.mem_compl_iff, not_not] at hu_not_in_compl hv_in_compl
Cleared hypotheses: hu_not_in_compl, hv_in_compl
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Decomposition (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
S : Set V
ha_in_S : a ∈ S
hb_not_in_S : ¬b ∈ S
⊢ ∃ (u : V),
    u ∈ S ∧
      ∃ (v : V),
        ¬v ∈ S ∧
          ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
have have : ¬a ∈ Sᶜ
Tactic: classical
  have ha_not_in_compl : a ∉ Sᶜ := by simpa
  have hb_in_compl : b ∈ Sᶜ := by simpa
  obtain ⟨u, hu_not_in_compl, v, hv_in_compl, e, p₁, p₂, hp⟩ :=
    exists_notMem_mem_hom_path_path_of_notMem_mem p Sᶜ ha_not_in_compl hb_in_compl
  simp only [Set.mem_compl_iff, not_not] at hu_not_in_compl hv_in_compl
  refine ⟨u, hu_not_in_compl, v, hv_in_compl, e, p₁, p₂, hp⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Decomposition (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
S : Set V
ha_in_S : a ∈ S
hb_not_in_S : ¬b ∈ S
have : ¬a ∈ Sᶜ
⊢ ∃ (u : V),
    u ∈ S ∧
      ∃ (v : V),
        ¬v ∈ S ∧
          ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
have have₁ : ∀ (ha_not_in_compl : ¬a ∈ Sᶜ),
  ∃ (u : V),
    u ∈ S ∧
      ∃ (v : V),
        ¬v ∈ S ∧
          ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
Tactic: classical
  have ha_not_in_compl : a ∉ Sᶜ := by simpa
  have hb_in_compl : b ∈ Sᶜ := by simpa
  obtain ⟨u, hu_not_in_compl, v, hv_in_compl, e, p₁, p₂, hp⟩ :=
    exists_notMem_mem_hom_path_path_of_notMem_mem p Sᶜ ha_not_in_compl hb_in_compl
  simp only [Set.mem_compl_iff, not_not] at hu_not_in_compl hv_in_compl
  refine ⟨u, hu_not_in_compl, v, hv_in_compl, e, p₁, p₂, hp⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Decomposition (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
S : Set V
ha_in_S : a ∈ S
hb_not_in_S : ¬b ∈ S
have : ¬a ∈ Sᶜ
have₁ :
  ∀ (ha_not_in_compl : ¬a ∈ Sᶜ),
    ∃ (u : V),
      u ∈ S ∧
        ∃ (v : V),
          ¬v ∈ S ∧
            ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
have₂ : ¬a ∈ Sᶜ
have₃ have₄ :
  ∀ (ha_not_in_compl : ¬a ∈ Sᶜ),
    ∃ (u : V),
      u ∈ S ∧
        ∃ (v : V),
          ¬v ∈ S ∧
            ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
⊢ ∃ (u : V),
    u ∈ S ∧
      ∃ (v : V),
        ¬v ∈ S ∧
          ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
have have₅ : ∀ (ha_not_in_compl : ¬a ∈ Sᶜ) (hb_in_compl : b ∈ Sᶜ),
  ∃ (u : V),
    u ∈ S ∧
      ∃ (v : V),
        ¬v ∈ S ∧
          ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
Tactic: classical
  have ha_not_in_compl : a ∉ Sᶜ := by simpa
  have hb_in_compl : b ∈ Sᶜ := by simpa
  obtain ⟨u, hu_not_in_compl, v, hv_in_compl, e, p₁, p₂, hp⟩ :=
    exists_notMem_mem_hom_path_path_of_notMem_mem p Sᶜ ha_not_in_compl hb_in_compl
  simp only [Set.mem_compl_iff, not_not] at hu_not_in_compl hv_in_compl
  refine ⟨u, hu_not_in_compl, v, hv_in_compl, e, p₁, p₂, hp⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Decomposition (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
S : Set V
ha_in_S : a ∈ S
hb_not_in_S : ¬b ∈ S
have : ¬a ∈ Sᶜ
have₁ :
  ∀ (ha_not_in_compl : ¬a ∈ Sᶜ),
    ∃ (u : V),
      u ∈ S ∧
        ∃ (v : V),
          ¬v ∈ S ∧
            ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
have₂ : ¬a ∈ Sᶜ
have₃ have₄ :
  ∀ (ha_not_in_compl : ¬a ∈ Sᶜ),
    ∃ (u : V),
      u ∈ S ∧
        ∃ (v : V),
          ¬v ∈ S ∧
            ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
have₅ :
  ∀ (ha_not_in_compl : ¬a ∈ Sᶜ) (hb_in_compl : b ∈ Sᶜ),
    ∃ (u : V),
      u ∈ S ∧
        ∃ (v : V),
          ¬v ∈ S ∧
            ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
⊢ ∃ (u : V),
    u ∈ S ∧
      ∃ (v : V),
        ¬v ∈ S ∧
          ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
have have₆ : ∀ (ha_not_in_compl : ¬a ∈ Sᶜ) (hb_in_compl : b ∈ Sᶜ) (u : V) (hu_not_in_compl : ¬u ∈ Sᶜ) (v : V) (hv_in_compl : v ∈ Sᶜ)
  (e : u ⟶ v) (p₁ : Path.{u_2, u_1} a u) (p₂ : Path.{u_2, u_1} v b) (hp : p = p₁.comp (e.toPath.comp p₂)),
  ∃ (u : V),
    u ∈ S ∧
      ∃ (v : V),
        ¬v ∈ S ∧
          ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
Tactic: classical
  have ha_not_in_compl : a ∉ Sᶜ := by simpa
  have hb_in_compl : b ∈ Sᶜ := by simpa
  obtain ⟨u, hu_not_in_compl, v, hv_in_compl, e, p₁, p₂, hp⟩ :=
    exists_notMem_mem_hom_path_path_of_notMem_mem p Sᶜ ha_not_in_compl hb_in_compl
  simp only [Set.mem_compl_iff, not_not] at hu_not_in_compl hv_in_compl
  refine ⟨u, hu_not_in_compl, v, hv_in_compl, e, p₁, p₂, hp⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Decomposition (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
S : Set V
ha_in_S : a ∈ S
hb_not_in_S : ¬b ∈ S
have : ¬a ∈ Sᶜ
have₁ :
  ∀ (ha_not_in_compl : ¬a ∈ Sᶜ),
    ∃ (u : V),
      u ∈ S ∧
        ∃ (v : V),
          ¬v ∈ S ∧
            ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
have₂ : ¬a ∈ Sᶜ
have₃ have₄ :
  ∀ (ha_not_in_compl : ¬a ∈ Sᶜ),
    ∃ (u : V),
      u ∈ S ∧
        ∃ (v : V),
          ¬v ∈ S ∧
            ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
have₅ :
  ∀ (ha_not_in_compl : ¬a ∈ Sᶜ) (hb_in_compl : b ∈ Sᶜ),
    ∃ (u : V),
      u ∈ S ∧
        ∃ (v : V),
          ¬v ∈ S ∧
            ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
have₆ :
  ∀ (ha_not_in_compl : ¬a ∈ Sᶜ) (hb_in_compl : b ∈ Sᶜ) (u : V) (hu_not_in_compl : ¬u ∈ Sᶜ) (v : V)
    (hv_in_compl : v ∈ Sᶜ) (e : u ⟶ v) (p₁ : Path.{u_2, u_1} a u) (p₂ : Path.{u_2, u_1} v b)
    (hp : p = p₁.comp (e.toPath.comp p₂)),
    ∃ (u : V),
      u ∈ S ∧
        ∃ (v : V),
          ¬v ∈ S ∧
            ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
⊢ ∃ (u : V),
    u ∈ S ∧
      ∃ (v : V),
        ¬v ∈ S ∧
          ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
have have₇ : ∀ (ha_not_in_compl : ¬a ∈ Sᶜ) (hb_in_compl : b ∈ Sᶜ) (u v : V) (e : u ⟶ v) (p₁ : Path.{u_2, u_1} a u)
  (p₂ : Path.{u_2, u_1} v b) (hp : p = p₁.comp (e.toPath.comp p₂)) (hu_not_in_compl : u ∈ S) (hv_in_compl : ¬v ∈ S),
  ∃ (u : V),
    u ∈ S ∧
      ∃ (v : V),
        ¬v ∈ S ∧
          ∃ (e : u ⟶ v), ∃ (p₁ : Path.{u_2, u_1} a u), ∃ (p₂ : Path.{u_2, u_1} v b), p = p₁.comp (e.toPath.comp p₂)
Tactic: classical
  have ha_not_in_compl : a ∉ Sᶜ := by simpa
  have hb_in_compl : b ∈ Sᶜ := by simpa
  obtain ⟨u, hu_not_in_compl, v, hv_in_compl, e, p₁, p₂, hp⟩ :=
    exists_notMem_mem_hom_path_path_of_notMem_mem p Sᶜ ha_not_in_compl hb_in_compl
  simp only [Set.mem_compl_iff, not_not] at hu_not_in_compl hv_in_compl
  refine ⟨u, hu_not_in_compl, v, hv_in_compl, e, p₁, p₂, hp⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b c : V
p : Path.{u_2, u_1} a b
e : b ⟶ c
x : V
⊢ x ∈ (p.cons e).vertices ↔ x ∈ p.vertices ∨ x = c
have simp : x ∈ p.vertices.concat c ↔ x ∈ p.vertices ∨ x = c
Tactic: simp only [vertices_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a : V
⊢ Eq (α := Set V) {v : V | Membership.mem (γ := List V) (vertices.{u_1, u_2} (a := a) nil) v} {a}
have simp : ∀ (x : V), Membership.mem (γ := Set V) {v : V | v = a} x ↔ x = a
Tactic: simp only [vertices_nil, mem_singleton, Set.ext_iff, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
a b : V
p : Path.{u_3, u_2} a b
⊢ p.vertices.length = p.length + 1
have nil : List.length.{u_2} (α := V) (vertices.{u_2, u_3} (a := a) nil) = length.{u_2, u_3} (V := V) (a := a) nil + 1
Tactic: induction p with
  | nil => simp
  | cons p' e ih =>
    simp [vertices_cons, length_cons, ih]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
a b : V
p : Path.{u_3, u_2} a b
nil :
  List.length.{u_2} (α := V) (vertices.{u_2, u_3} (a := a) Path.nil) = length.{u_2, u_3} (V := V) (a := a) Path.nil + 1
⊢ p.vertices.length = p.length + 1
have cons : ∀ {b c : V} (p' : Path.{u_3, u_2} a b) (e : b ⟶ c) (ih : p'.vertices.length = p'.length + 1),
  (p'.cons e).vertices.length = (p'.cons e).length + 1
Tactic: induction p with
  | nil => simp
  | cons p' e ih =>
    simp [vertices_cons, length_cons, ih]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
⊢ a ∈ p.vertices
have nil : Membership.mem (γ := List V) (vertices.{u_1, u_2} (a := a) nil) a
Tactic: induction p with
  | nil => simp
  | cons p' e ih => simp [ih]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
nil : Membership.mem (γ := List V) (vertices.{u_1, u_2} (a := a) Path.nil) a
⊢ a ∈ p.vertices
have cons : ∀ {b c : V} (p' : Path.{u_2, u_1} a b) (e : b ⟶ c) (ih : a ∈ p'.vertices), a ∈ (p'.cons e).vertices
Tactic: induction p with
  | nil => simp
  | cons p' e ih => simp [ih]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
⊢ p.vertices.head? = some a
have nil : head? (vertices.{u_1, u_2} (a := a) nil) = some a
Tactic: induction p with
  | nil => simp only [vertices_nil, head?_cons]
  | cons p' e ih => simp [ih]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Path.Vertices (goal)
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
nil : head? (vertices.{u_1, u_2} (a := a) Path.nil) = some a
⊢ p.vertices.head? = some a
have cons : ∀ {b c : V} (p' : Path.{u_2, u_1} a b) (e : b ⟶ c) (ih : p'.vertices.head? = some a),
  (p'.cons e).vertices.head? = some a
Tactic: induction p with
  | nil => simp only [vertices_nil, head?_cons]
  | cons p' e ih => simp [ih]
Cleared hypotheses: p