-- Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
@[reassoc (attr := simp)]
lemma πObj_naturality {f g : Arrow C} (φ : f ⟶ g) :
    objMap I κ φ ≫ πObj I κ g.hom = πObj I κ f.hom ≫ φ.right

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f g : Arrow C
φ : f ⟶ g
e₁ : ((𝟭 (Arrow C)).obj (Arrow.mk f.hom)).right ≅ ((iteration I κ).obj (Arrow.mk f.hom)).right :=
  asIso ((ιIteration I κ).app (Arrow.mk f.hom)).right
e₂ : ((𝟭 (Arrow C)).obj (Arrow.mk g.hom)).right ≅ ((iteration I κ).obj (Arrow.mk g.hom)).right :=
  asIso ((ιIteration I κ).app (Arrow.mk g.hom)).right
⊢ objMap I κ φ ≫ πObj I κ g.hom = πObj I κ f.hom ≫ φ.right

Tactic:
change _ ≫ _ ≫ e₂.inv = (_ ≫ e₁.inv) ≫ _

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f g : Arrow C
φ : f ⟶ g
e₁ : ((𝟭 (Arrow C)).obj (Arrow.mk f.hom)).right ≅ ((iteration I κ).obj (Arrow.mk f.hom)).right :=
  asIso ((ιIteration I κ).app (Arrow.mk f.hom)).right
e₂ : ((𝟭 (Arrow C)).obj (Arrow.mk g.hom)).right ≅ ((iteration I κ).obj (Arrow.mk g.hom)).right :=
  asIso ((ιIteration I κ).app (Arrow.mk g.hom)).right
⊢ objMap I κ φ ≫ ((iteration I κ).obj (Arrow.mk g.hom)).hom ≫ e₂.inv =
    (((iteration I κ).obj (Arrow.mk f.hom)).hom ≫ e₁.inv) ≫ φ.right

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f g : Arrow C
φ : f ⟶ g
e₁ : ((𝟭 (Arrow C)).obj (Arrow.mk f.hom)).right ≅ ((iteration I κ).obj (Arrow.mk f.hom)).right :=
  asIso ((ιIteration I κ).app (Arrow.mk f.hom)).right
e₂ : ((𝟭 (Arrow C)).obj (Arrow.mk g.hom)).right ≅ ((iteration I κ).obj (Arrow.mk g.hom)).right :=
  asIso ((ιIteration I κ).app (Arrow.mk g.hom)).right
h₁ :
  ((𝟭 C).map ((iteration I κ).map φ).left ≫ ((iteration I κ).obj g).hom) ≫ e₂.inv =
    (((iteration I κ).obj f).hom ≫ (𝟭 C).map ((iteration I κ).map φ).right) ≫ e₂.inv
h₂ : φ.right ≫ e₂.hom = e₁.hom ≫ ((iteration I κ).map φ).right
⊢ objMap I κ φ ≫ ((iteration I κ).obj (Arrow.mk g.hom)).hom ≫ e₂.inv =
    (((iteration I κ).obj (Arrow.mk f.hom)).hom ≫ e₁.inv) ≫ φ.right

Tactic:
dsimp at h₁

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f g : Arrow C
φ : f ⟶ g
e₁ : ((𝟭 (Arrow C)).obj (Arrow.mk f.hom)).right ≅ ((iteration I κ).obj (Arrow.mk f.hom)).right :=
  asIso ((ιIteration I κ).app (Arrow.mk f.hom)).right
e₂ : ((𝟭 (Arrow C)).obj (Arrow.mk g.hom)).right ≅ ((iteration I κ).obj (Arrow.mk g.hom)).right :=
  asIso ((ιIteration I κ).app (Arrow.mk g.hom)).right
h₁ :
  (((iteration I κ).map φ).left ≫ ((iteration I κ).obj g).hom) ≫ e₂.inv =
    (((iteration I κ).obj f).hom ≫ ((iteration I κ).map φ).right) ≫ e₂.inv
h₂ : φ.right ≫ e₂.hom = e₁.hom ≫ ((iteration I κ).map φ).right
⊢ objMap I κ φ ≫ ((iteration I κ).obj (Arrow.mk g.hom)).hom ≫ e₂.inv =
    (((iteration I κ).obj (Arrow.mk f.hom)).hom ≫ e₁.inv) ≫ φ.right