Theorem: eventually_mem_uIoo_of_mem_uIoc (RMT4/to_mathlib.lean)

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
⊢ ∀ᵐ (x : ℝ), x ∈ Ι a b → x ∈ uIoo a b
Tactic:
apply eventually_of_mem (U := {a, b}ᶜ)
State after:
case hU
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
⊢ {a, b}ᶜ ∈ Measure.ae volume

case h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
⊢ ∀ x ∈ {a, b}ᶜ, x ∈ Ι a b → x ∈ uIoo a b

State before:
case hU
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
⊢ {a, b}ᶜ ∈ Measure.ae volume
Tactic:
simpa only [mem_ae_iff, compl_compl] using measure_union_null volume_singleton volume_singleton
State after:
no goals

State before:
case h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
⊢ ∀ x ∈ {a, b}ᶜ, x ∈ Ι a b → x ∈ uIoo a b
Tactic:
rw [uIoo_eq_uIoc_sdiff_ends]
State after:
case h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
⊢ ∀ x ∈ {a, b}ᶜ, x ∈ Ι a b → x ∈ Ι a b \ {a, b}

State before:
case h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
⊢ ∀ x ∈ {a, b}ᶜ, x ∈ Ι a b → x ∈ Ι a b \ {a, b}
Tactic:
exact λ t h1 h2 => ⟨h2, h1⟩
State after:
no goals