m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : n ≠ 0
hm : m ≠ 0
⊢ ↑(if hn : n = 0 then { val := a, property := (_ : a ≡ a [MOD n] ∧ a ≡ b [MOD m]) }
      else
        if hm : m = 0 then { val := b, property := (_ : b ≡ a [MOD n] ∧ b ≡ b [MOD m]) }
        else
          { val := Int.toNat ((↑n * (xgcd n m).fst * ↑b + ↑m * (xgcd n m).snd * ↑a) / ↑(gcd n m) % ↑(lcm n m)),
            property :=
              (_ :
                (match xgcd n m with
                    | (c, d) => Int.toNat ((↑n * c * ↑b + ↑m * d * ↑a) / ↑(gcd n m) % ↑(lcm n m))) ≡
                    a [MOD n] ∧
                  (match xgcd n m with
                    | (c, d) => Int.toNat ((↑n * c * ↑b + ↑m * d * ↑a) / ↑(gcd n m) % ↑(lcm n m))) ≡
                    b [MOD m]) }) <
    lcm n m
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : n ≠ 0
hm : m ≠ 0
⊢ ↑(chineseRemainder' h) < lcm n m
dsimp only [chineseRemainder']
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : n ≠ 0
hm : m ≠ 0
⊢ Int.toNat
      ((↑n * (gcdA n m, gcdB n m).fst * ↑b + ↑m * (gcdA n m, gcdB n m).snd * ↑a) / ↑(gcd n m) %
        ↑(Int.toNat ↑(lcm n m))) <
    Int.toNat ↑(lcm n m)
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : n ≠ 0
hm : m ≠ 0
⊢ ↑(if hn : n = 0 then { val := a, property := (_ : a ≡ a [MOD n] ∧ a ≡ b [MOD m]) }
      else
        if hm : m = 0 then { val := b, property := (_ : b ≡ a [MOD n] ∧ b ≡ b [MOD m]) }
        else
          { val := Int.toNat ((↑n * (xgcd n m).fst * ↑b + ↑m * (xgcd n m).snd * ↑a) / ↑(gcd n m) % ↑(lcm n m)),
            property :=
              (_ :
                (match xgcd n m with
                    | (c, d) => Int.toNat ((↑n * c * ↑b + ↑m * d * ↑a) / ↑(gcd n m) % ↑(lcm n m))) ≡
                    a [MOD n] ∧
                  (match xgcd n m with
                    | (c, d) => Int.toNat ((↑n * c * ↑b + ↑m * d * ↑a) / ↑(gcd n m) % ↑(lcm n m))) ≡
                    b [MOD m]) }) <
    lcm n m
rw [dif_neg hn, dif_neg hm, Subtype.coe_mk, xgcd_val, ← Int.toNat_coe_nat (lcm n m)]
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : n ≠ 0
hm : m ≠ 0
lcm_pos : 0 < ↑(lcm n m)
⊢ Int.toNat
      ((↑n * (gcdA n m, gcdB n m).fst * ↑b + ↑m * (gcdA n m, gcdB n m).snd * ↑a) / ↑(gcd n m) %
        ↑(Int.toNat ↑(lcm n m))) <
    Int.toNat ↑(lcm n m)
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : n ≠ 0
hm : m ≠ 0
⊢ Int.toNat
      ((↑n * (gcdA n m, gcdB n m).fst * ↑b + ↑m * (gcdA n m, gcdB n m).snd * ↑a) / ↑(gcd n m) %
        ↑(Int.toNat ↑(lcm n m))) <
    Int.toNat ↑(lcm n m)
have lcm_pos := Int.coe_nat_pos.mpr (Nat.pos_of_ne_zero (lcm_ne_zero hn hm))
no goals
m n a b c d : ℕ
h : a ≡ b [MOD gcd n m]
hn : n ≠ 0
hm : m ≠ 0
lcm_pos : 0 < ↑(lcm n m)
⊢ Int.toNat
      ((↑n * (gcdA n m, gcdB n m).fst * ↑b + ↑m * (gcdA n m, gcdB n m).snd * ↑a) / ↑(gcd n m) %
        ↑(Int.toNat ↑(lcm n m))) <
    Int.toNat ↑(lcm n m)
exact (Int.toNat_lt_toNat lcm_pos).mpr (Int.emod_lt_of_pos _ lcm_pos)