English
Composition respects prodMap: (f2 ∘ f1) × (g2 ∘ g1) equals (f2 × g2) ∘ (f1 × g1).
Русский
Сложение сохраняет prodMap: (f2 ∘ f1) × (g2 ∘ g1) = (f2 × g2) ∘ (f1 × g1).
LaTeX
$$$$ (f_2 \\circ f_1) \\prodMap (g_2 \\circ g_1) = (f_2 \\prodMap g_2) \\circ (f_1 \\prodMap g_1). $$$$
Lean4
@[simp]
theorem prodMap_comp_comp (f₁ : α →. β) (f₂ : β →. γ) (g₁ : δ →. ε) (g₂ : ε →. ι) :
(f₂.comp f₁).prodMap (g₂.comp g₁) = (f₂.prodMap g₂).comp (f₁.prodMap g₁) :=
-- `aesop` can prove this but takes over a second, so we do it manually
ext <| fun ⟨_, _⟩ ⟨_, _⟩ ↦
⟨fun ⟨⟨⟨h1l1, h1l2⟩, ⟨h1r1, h1r2⟩⟩, h2⟩ ↦ ⟨⟨⟨h1l1, h1r1⟩, ⟨h1l2, h1r2⟩⟩, h2⟩,
fun ⟨⟨⟨h1l1, h1r1⟩, ⟨h1l2, h1r2⟩⟩, h2⟩ ↦ ⟨⟨⟨h1l1, h1l2⟩, ⟨h1r1, h1r2⟩⟩, h2⟩⟩
