-- 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
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

Tactic:
rw [assoc] 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

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₁ :
  ((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
⊢ (((iteration I κ).obj f).hom ≫ ((iteration I κ).map φ).right) ≫ e₂.inv =
    (((iteration I κ).obj (Arrow.mk f.hom)).hom ≫ e₁.inv) ≫ φ.right

Tactic:
simp only [← cancel_mono e₂.hom, assoc, e₂.inv_hom_id, h₂, e₁.inv_hom_id_assoc]

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
⊢ ((iteration I κ).obj f).hom ≫ ((iteration I κ).map φ).right ≫ 𝟙 ((iteration I κ).obj (Arrow.mk g.hom)).right =
    ((iteration I κ).obj (Arrow.mk f.hom)).hom ≫ ((iteration I κ).map φ).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
⊢ objMap I κ φ ≫ ((iteration I κ).obj (Arrow.mk g.hom)).hom ≫ e₂.inv =
    (((iteration I κ).obj (Arrow.mk f.hom)).hom ≫ e₁.inv) ≫ φ.right

Tactic:
have h₂ : φ.right ≫ e₂.hom = e₁.hom ≫ ((iteration I κ).map φ).right :=
  ((whiskerRight (ιIteration I κ) Arrow.rightFunc).naturality φ)

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₁ :
  ((𝟭 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

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₁ :
  ((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
⊢ (((iteration I κ).obj f).hom ≫ ((iteration I κ).map φ).right) ≫ 𝟙 ((iteration I κ).obj (Arrow.mk g.hom)).right =
    ((iteration I κ).obj (Arrow.mk f.hom)).hom ≫ ((iteration I κ).map φ).right

Tactic:
apply comp_id

Result:
no goals