Theorem: Category.eq_whisker (CategoryTheory/Basic.lean)

State before:
α : Type u_2
β : Type ?u.23648
γ : Type ?u.23651
δ : Type ?u.23654
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
f g : B ⟶ C
w : f = g
h : A ⟶ B
⊢ f ∘ h = g ∘ h
Tactic:
rw [w]
State after:
no goals