exact_mod_cast within sums

Stream: general

[Thomas Bloom]

Is there a more powerful version of exact_mod_cast that can handle casting issues 'inside sums'? (Or any chance of upgrading exact_mod_cast to do this). e.g.:

lemma test (D : finset ℕ) (h : 0 < ∑ d in D, ((1 : ℚ)/d)) : 0 < ∑ d in D, ((1 : ℝ)/d) :=
or
lemma test (D : finset ℕ) (h : (1:ℚ)/2 < ∑ d in D, 1/d) : (1:ℝ)/2 < ∑ d in D, 1/d :=

(Ideally both of these goals would be closed by exact_mod_cast h).

[Yaël Dillies]

Just noting that this works, as a comparison:

import data.real.basic

open_locale big_operators

variables {ι α : Type*}

@[simp, norm_cast]
lemma rat.cast_sum [division_ring α] [char_zero α] (s : finset ι) (f : ι → ℚ) :
  (↑(∑ i in s, f i) : α) = ∑ i in s, f i :=
map_sum (rat.cast_hom α) f s

lemma test (D : finset ℕ) (h : 0 < ∑ d in D, ((1 : ℚ)/d)) : 0 < ∑ d in D, ((1 : ℝ)/d) := begin
  have : ((0 : ℚ) : ℝ) < _ := rat.cast_lt.2 h,
  push_cast at this,
  exact this,
end

[Yaël Dillies]

(I'm PRing rat.cast_sum)

[Yaël Dillies]

I think the problem is that the norm_cast in exact_mod_cast brushes casts the wrong way. It doesn't manage to turn 0 : ℝ into (0 : ℚ) : ℝ, which is needed to make progress.

[Bhavik Mehta]

I think I also have rat.cast_sum in the unit fractions project because I also hit this issue!