no goals
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.392356
γ : Path x y
a₁ a₂ a₃ : X
b₁ b₂ b₃ : Y
γ₁ : Path a₁ a₂
δ₁ : Path a₂ a₃
γ₂ : Path b₁ b₂
δ₂ : Path b₂ b₃
⊢ trans (Path.prod γ₁ γ₂) (Path.prod δ₁ δ₂) = Path.prod (trans γ₁ δ₁) (trans γ₂ δ₂)
ext t <;>
unfold Path.trans <;>
simp only [Path.coe_mk_mk, Path.prod_coe, Function.comp_apply] <;>
split_ifs <;>
rfl