Can simp do this?

Stream: mathlib4

[Kenny Lau]

import Mathlib

open CategoryTheory
def A : CommRingCat.{0}ᵒᵖ := sorry
def B : CommRingCat.{0}ᵒᵖ := sorry
def C : CommRingCat.{0}ᵒᵖ := sorry
def D : CommRingCat.{0}ᵒᵖ := sorry
def f₁ : A ⟶ B := sorry
def g₁ : B ⟶ D := sorry
def f₂ : A ⟶ C := sorry
def g₂ : C ⟶ D := sorry
@[simp] lemma foo : f₁ ≫ g₁ = f₂ ≫ g₂ := sorry

open AlgebraicGeometry

theorem bar : Scheme.Spec.map f₁ ≫ Scheme.Spec.map g₁ = Scheme.Spec.map f₂ ≫ Scheme.Spec.map g₂ := by
  simp [-Scheme.Spec_obj, -Scheme.Spec_map]
-- fails

theorem bar' : Scheme.Spec.map f₁ ≫ Scheme.Spec.map g₁ = Scheme.Spec.map f₂ ≫ Scheme.Spec.map g₂ := by
  simpa [-foo] using congr_arg Scheme.Spec.map foo
-- succeeds

Basically, I have a functor F : C ⥤ D, and an equation in C (e.g. h : f₁ ≫ g₁ = f₂ ≫ g₂). I wonder if it's possible to tell simp to prove the corresponding theorem in D, i.e. F.map f₁ ≫ F.map g₁ = F.map f₂ ≫ F.map g₂ automatically, or via attributes (on h), etc.

[Markus Himmel]

Often in mathlib this is solved by invoking simp with the backwards direction of Functor.map_comp:

theorem bar : Scheme.Spec.map f₁ ≫ Scheme.Spec.map g₁ = Scheme.Spec.map f₂ ≫ Scheme.Spec.map g₂ := by
  simp [-Scheme.Spec_obj, -Scheme.Spec_map, ← Functor.map_comp]

See also the discussion at #Is there code for X? > Attribute to map rewrite rules through a functor?

[Kenny Lau]

Markus Himmel said:

Often in mathlib this is solved by invoking simp with the backwards direction of Functor.map_comp:

theorem bar : Scheme.Spec.map f₁ ≫ Scheme.Spec.map g₁ = Scheme.Spec.map f₂ ≫ Scheme.Spec.map g₂ := by
  simp [-Scheme.Spec_obj, -Scheme.Spec_map, ← Functor.map_comp]

See also the discussion at #Is there code for X? > Attribute to map rewrite rules through a functor?

just that i couldn't do it here because i also need the forward directions