awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
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
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₂)
⊢ ∃ (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 ⟨c, p', e, rfl⟩ := (length_ne_zero_iff_eq_cons p).mp h_pos.ne'

Premises used: Quiver.Path.length_ne_zero_iff_eq_cons, LT.lt.ne', Iff.mp, rfl
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
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₂)
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₂)
⊢ ∃ (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
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
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'.length = n

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
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'.length = n

Tactic:
have p'_len : p'.length = n := by simp_all
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
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
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₂)
⊢ ∃ (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
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
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₂)

Tactic:
⟨u, hu_not_S, v, hv_S, e_uv, p₁, p₂.comp e.toPath, ?_⟩

Premises used: Quiver.Hom.toPath, And.intro, Exists.intro, Quiver.Path.comp
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
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₂)
pos : p'.cons e = p₁.comp (e_uv.toPath.comp (p₂.comp e.toPath))
⊢ ∃ (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:
refine ⟨u, hu_not_S, v, hv_S, e_uv, p₁, p₂.comp e.toPath, ?_⟩
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
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₂)
⊢ p'.cons e = p₁.comp (e_uv.toPath.comp (p₂.comp e.toPath))

Tactic:
simp [hp', comp_toPath_eq_cons]

Premises used: Quiver.Path.comp_toPath_eq_cons
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
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₂)

Tactic:
⟨c, hc_in_S, b, hb_in_S, e, p', Path.nil, ?_⟩

Premises used: Quiver.Path.nil, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
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
neg : p'.cons e = p'.comp (e.toPath.comp nil)
⊢ ∃ (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:
refine ⟨c, hc_in_S, b, hb_in_S, e, p', Path.nil, ?_⟩
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
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'.cons e = p'.comp (e.toPath.comp nil)

Tactic:
simp [comp_toPath_eq_cons]

Premises used: Quiver.Path.comp_toPath_eq_cons
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
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
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₂)
⊢ ∃ (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]

Premises used: Quiver.Path.length, Quiver.Path.comp_toPath_eq_cons, rfl
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
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
⊢ ¬a ∈ Sᶜ

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
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
⊢ ¬a ∈ Sᶜ

Tactic:
have ha_not_in_compl : a ∉ Sᶜ := by simpa
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
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ᶜ
⊢ b ∈ Sᶜ

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
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ᶜ
⊢ b ∈ Sᶜ

Tactic:
have hb_in_compl : b ∈ Sᶜ := by simpa
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
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ᶜ
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₂)
⊢ ∃ (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

Premises used: Quiver.Path.exists_notMem_mem_hom_path_path_of_notMem_mem, Compl.compl
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
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 ∈ S

Tactic:
simp only [Set.mem_compl_iff, not_not] at hu_not_in_compl hv_in_compl

Premises used: Classical.not_not, Set.mem_compl_iff
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
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
⊢ ¬v ∈ S

Tactic:
simp only [Set.mem_compl_iff, not_not] at hu_not_in_compl hv_in_compl

Premises used: Classical.not_not, Set.mem_compl_iff
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
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 : 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:
⟨u, hu_not_in_compl, v, hv_in_compl, e, p₁, p₂, hp⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
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 : 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:
refine ⟨u, hu_not_in_compl, v, hv_in_compl, e, p₁, p₂, hp⟩
-- Module: Mathlib.Combinatorics.Quiver.Path.Decomposition
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₂)
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₂)
⊢ ∃ (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⟩

Premises used: Classical.not_not, Set.mem_compl_iff
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
⊢ (p.cons e).end = c

Tactic:
rfl

Premises used: Quiver.Path.end, rfl
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a : V
⊢ vertices.{u_1, u_2} (a := a) nil = [a]

Tactic:
rfl

Premises used: rfl, Quiver.Path.vertices
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
⊢ (p.cons e).vertices = p.vertices.concat c

Tactic:
rfl

Premises used: Quiver.Path.end, rfl, Quiver.Path.vertices
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
simp : x ∈ p.vertices.concat c ↔ x ∈ p.vertices ∨ x = c
⊢ x ∈ (p.cons e).vertices ↔ x ∈ p.vertices ∨ x = c

Tactic:
simp only [vertices_cons]

Premises used: Quiver.Path.vertices_cons
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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.vertices.concat c ↔ x ∈ p.vertices ∨ x = c

Tactic:
simp_all only [concat_eq_append, mem_append, mem_cons, not_mem_nil, or_false]

Premises used: List.concat_eq_append, List.mem_append, or_false, List.mem_cons, List.not_mem_nil
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a : V
simp : ∀ (x : V), Membership.mem (γ := Set V) {v : V | v = a} x ↔ x = a
⊢ Eq (α := Set V) {v : V | Membership.mem (γ := List V) (vertices.{u_1, u_2} (a := a) nil) v} {a}

Tactic:
simp only [vertices_nil, mem_singleton, Set.ext_iff, Set.mem_singleton_iff]

Premises used: List.mem_singleton, Set.mem_singleton_iff, Set.ext_iff, Quiver.Path.vertices_nil
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a : V
⊢ ∀ (x : V), Membership.mem (γ := Set V) {v : V | v = a} x ↔ x = a

Tactic:
fun x ↦ Set.mem_setOf

Premises used: Set.mem_setOf
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a : V
⊢ ∀ (x : V), Membership.mem (γ := Set V) {v : V | v = a} x ↔ x = a

Tactic:
exact fun x ↦ Set.mem_setOf

Premises used: Set.mem_setOf
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
a b : V
⊢ 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:
simp
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
a b b_1 c : V
p' : Path.{u_3, u_2} a b_1
e : b_1 ⟶ c
ih : p'.vertices.length = p'.length + 1
⊢ (p'.cons e).vertices.length = (p'.cons e).length + 1

Tactic:
simp [vertices_cons, length_cons, ih]

Premises used: Quiver.Path.length_cons, Quiver.Path.vertices_cons
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
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
⊢ p.vertices.length = p.length + 1

Tactic:
induction p with
  | nil => simp
  | cons p' e ih =>
    simp [vertices_cons, length_cons, ih]

Premises used: Quiver.Path.length_cons, Quiver.Path.nil, Quiver.Path.vertices_cons, Quiver.Path.cons
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
p : Path.{u_2, u_1} a b
⊢ 0 < p.vertices.length

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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 ≠ []

Tactic:
simp [← length_pos_iff_ne_nil]

Premises used: List.length_pos_iff_ne_nil
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
⊢ Membership.mem (γ := List V) (vertices.{u_1, u_2} (a := a) nil) a

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b b_1 c : V
p' : Path.{u_2, u_1} a b_1
e : b_1 ⟶ c
ih : a ∈ p'.vertices
⊢ a ∈ (p'.cons e).vertices

Tactic:
simp [ih]
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
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
cons : ∀ {b c : V} (p' : Path.{u_2, u_1} a b) (e : b ⟶ c) (ih : a ∈ p'.vertices), a ∈ (p'.cons e).vertices
⊢ a ∈ p.vertices

Tactic:
induction p with
  | nil => simp
  | cons p' e ih => simp [ih]

Premises used: Quiver.Path.nil, Quiver.Path.cons
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b : V
⊢ head? (vertices.{u_1, u_2} (a := a) nil) = some a

Tactic:
simp only [vertices_nil, head?_cons]

Premises used: List.head?_cons, Quiver.Path.vertices_nil
-- Module: Mathlib.Combinatorics.Quiver.Path.Vertices
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
a b b_1 c : V
p' : Path.{u_2, u_1} a b_1
e : b_1 ⟶ c
ih : p'.vertices.head? = some a
⊢ (p'.cons e).vertices.head? = some a

Tactic:
simp [ih]