∀ (A : Type u_1) {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : ValuativeRel A]
  [inst_3 : ValuativeRel B] [inst_4 : Algebra A B] [ValuativeExtension A B] {Γ : Type u_3}
  [inst_6 : LinearOrderedCommMonoidWithZero Γ] (w : Valuation B Γ) [w.Compatible],
  (Valuation.comap (algebraMap A B) w).Compatible