Theorem: intervalIntegral.integral_congr_uIoo (RMT4/to_mathlib.lean)

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
h : EqOn f g (uIoo a b)
⊢ ∫ (t : ℝ) in a..b, f t = ∫ (t : ℝ) in a..b, g t
Tactic:
apply intervalIntegral.integral_congr_ae
State after:
case h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
h : EqOn f g (uIoo a b)
⊢ ∀ᵐ (x : ℝ) ∂volume, x ∈ Ι a b → f x = g x

State before:
case h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
h : EqOn f g (uIoo a b)
⊢ ∀ᵐ (x : ℝ) ∂volume, x ∈ Ι a b → f x = g x
Tactic:
filter_upwards [eventually_mem_uIoo_of_mem_uIoc] with t ht1 ht2 using h (ht1 ht2)
State after:
no goals