∀ {m n : ℕ} (h : m.Coprime n),
  ¬m * n = 0 →
    Function.LeftInverse
        (fun x =>
          if m * n = 0 then
            if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
          else ↑↑(Nat.chineseRemainder h x.1.val x.2.val))
        ⇑(ZMod.castHom ⋯ (ZMod m × ZMod n)) ∧
      Function.RightInverse
        (fun x =>
          if m * n = 0 then
            if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
          else ↑↑(Nat.chineseRemainder h x.1.val x.2.val))
        ⇑(ZMod.castHom ⋯ (ZMod m × ZMod n))