no goals
ι✝ : Type ?u.29939
inst✝ : Fintype ι✝
I J : Box ι✝
c c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι✝ → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I
l✝ l₁ l₂ : IntegrationParams
ι : Type u_1
l : IntegrationParams
hl : l.bRiemann = false
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ RCond l r
simp [RCond, hl]