-- Mathlib/CategoryTheory/PathCategory/Basic.lean
/-- To prove a property on morphisms of a path category with given target `b`, it suffices to prove
it for the identity and prove that the property is preserved under composition on the left
with length 1 paths. -/
lemma induction_fixed_target {b : Paths V} (P : ∀ {a : Paths V}, (a ⟶ b) → Prop)
    (id : P (𝟙 b))
    (comp : ∀ {u v : V} (p : of.obj v ⟶ b) (q : u ⟶ v), P p → P (of.map q ≫ p)) :
    ∀ {a : Paths V} (f : a ⟶ b), P f

Proof state:
case zero.nil
V : Type u₁
inst✝ : Quiver V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : of.obj v ⟶ b) (q : u ⟶ v), P p → P (of.map q ≫ p)
h : Quiver.Path.nil.length = 0
⊢ P Quiver.Path.nil

Tactic:
exact id

Result:
no goals

Proof state:
V : Type u₁
inst✝ : Quiver V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : of.obj v ⟶ b) (q : u ⟶ v), P p → P (of.map q ≫ p)
a : Paths V
f : a ⟶ b
⊢ P f

Tactic:
generalize h : f.length = k

Result:
V : Type u₁
inst✝ : Quiver V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : of.obj v ⟶ b) (q : u ⟶ v), P p → P (of.map q ≫ p)
a : Paths V
f : a ⟶ b
k : ℕ
h : Quiver.Path.length f = k
⊢ P f

Proof state:
case succ.intro.intro.intro.intro
V : Type u₁
inst✝ : Quiver V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : of.obj v ⟶ b) (q : u ⟶ v), P p → P (of.map q ≫ p)
k : ℕ
h' : ∀ {a : Paths V} (f : a ⟶ b), Quiver.Path.length f = k → P f
a : Paths V
c : V
f : a ⟶ c
q : Quiver.Path c b
hq : q.length = k
h : (f.toPath.comp q).length = k + 1
⊢ P (f.toPath.comp q)

Tactic:
exact comp _ _ (h' _ hq)

Result:
no goals

Proof state:
case succ
V : Type u₁
inst✝ : Quiver V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : of.obj v ⟶ b) (q : u ⟶ v), P p → P (of.map q ≫ p)
k : ℕ
h' : ∀ {a : Paths V} (f : a ⟶ b), Quiver.Path.length f = k → P f
a : Paths V
f : a ⟶ b
h : Quiver.Path.length f = k + 1
⊢ P f

Tactic:
obtain ⟨c, f, q, hq, rfl⟩ := f.eq_toPath_comp_of_length_eq_succ h

Result:
case succ.intro.intro.intro.intro
V : Type u₁
inst✝ : Quiver V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : of.obj v ⟶ b) (q : u ⟶ v), P p → P (of.map q ≫ p)
k : ℕ
h' : ∀ {a : Paths V} (f : a ⟶ b), Quiver.Path.length f = k → P f
a : Paths V
c : V
f : a ⟶ c
q : Quiver.Path c b
hq : q.length = k
h : (f.toPath.comp q).length = k + 1
⊢ P (f.toPath.comp q)

Proof state:
case zero.cons
V : Type u₁
inst✝ : Quiver V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : of.obj v ⟶ b) (q : u ⟶ v), P p → P (of.map q ≫ p)
a b✝ : Paths V
a✝¹ : Quiver.Path a b✝
a✝ : b✝ ⟶ b
h : (a✝¹.cons a✝).length = 0
⊢ P (a✝¹.cons a✝)

Tactic:
simp at h

Result:
no goals

Proof state:
V : Type u₁
inst✝ : Quiver V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : of.obj v ⟶ b) (q : u ⟶ v), P p → P (of.map q ≫ p)
a : Paths V
f : a ⟶ b
k : ℕ
h : Quiver.Path.length f = k
⊢ P f

Tactic:
induction k generalizing f a with
| zero => cases f with
  | nil => exact id
  | cons _ _ => simp at h
| succ k h' =>
  obtain ⟨c, f, q, hq, rfl⟩ := f.eq_toPath_comp_of_length_eq_succ h
  exact comp _ _ (h' _ hq)

Result:
no goals

Proof state:
V : Type u₁
inst✝ : Quiver V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : of.obj v ⟶ b) (q : u ⟶ v), P p → P (of.map q ≫ p)
⊢ ∀ {a : Paths V} (f : a ⟶ b), P f

Tactic:
intro a f

Result:
V : Type u₁
inst✝ : Quiver V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : of.obj v ⟶ b) (q : u ⟶ v), P p → P (of.map q ≫ p)
a : Paths V
f : a ⟶ b
⊢ P f

Proof state:
case zero
V : Type u₁
inst✝ : Quiver V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : of.obj v ⟶ b) (q : u ⟶ v), P p → P (of.map q ≫ p)
a : Paths V
f : a ⟶ b
h : Quiver.Path.length f = 0
⊢ P f

Tactic:
cases f with
| nil => exact id
| cons _ _ => simp at h

Result:
no goals