no goals
V : Type u
inst✝ : Quiver V
a b c d : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
h : length p₁ = length p₂
h_eq : comp p₁ q₁ = comp p₂ q₂
⊢ ?m.9164 h h_eq + length q₁ = ?m.9164 h h_eq + length q₂
simpa [h] using congr_arg length h_eq
case intro
V : Type u
inst✝ : Quiver V
a b c d : V
p₁ : Path a b
q₁ : Path b c
h : length p₁ = length p₁
⊢ comp p₁ q₁ = comp p₁ q₁
V : Type u
inst✝ : Quiver V
a b c d : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
h : length p₁ = length p₂
⊢ p₁ = p₂ ∧ q₁ = q₂ → comp p₁ q₁ = comp p₂ q₂
rintro ⟨rfl, rfl⟩
no goals
case intro
V : Type u
inst✝ : Quiver V
a b c d : V
p₁ : Path a b
q₁ : Path b c
h : length p₁ = length p₁
⊢ comp p₁ q₁ = comp p₁ q₁
rfl