∀ {K : outParam (Type u_5)} {L : outParam (Type u_6)} {Γ₀ : outParam (Type u_7)} {Γ₁ : outParam (Type u_8)}
  [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_4 : LinearOrderedCommGroupWithZero Γ₁] (vK : Valuation K Γ₀) (vL : Valuation L Γ₁)
  [inst_5 : vK.HasExtension vL],
  Ideal.comap (algebraMap ↥vK.valuationSubring ↥vL.valuationSubring) (IsLocalRing.maximalIdeal ↥vL.valuationSubring) =
    IsLocalRing.maximalIdeal ↥vK.valuationSubring