Theorem: uIoo_eq_uIoc_sdiff_ends (RMT4/to_mathlib.lean)

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
⊢ uIoo a b = Ι a b \ {a, b}
Tactic:
ext t
State after:
case h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
⊢ t ∈ uIoo a b ↔ t ∈ Ι 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 : ℕ
t : ℝ
⊢ t ∈ uIoo a b ↔ t ∈ Ι a b \ {a, b}
Tactic:
constructor <;> intro hh
State after:
case h.mp
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : t ∈ uIoo a b
⊢ t ∈ Ι a b \ {a, b}

case h.mpr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : t ∈ Ι a b \ {a, b}
⊢ t ∈ uIoo a b

State before:
case h.mp
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : t ∈ uIoo a b
⊢ t ∈ Ι a b \ {a, b}
Tactic:
simp [mem_uIoo] at hh
State after:
case h.mp
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : a < t ∧ t < b ∨ b < t ∧ t < a
⊢ t ∈ Ι a b \ {a, b}

State before:
case h.mp
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : a < t ∧ t < b ∨ b < t ∧ t < a
⊢ t ∈ Ι a b \ {a, b}
Tactic:
cases hh with
| inl h => simp [uIoc, h, h.2.le, h.1.ne.symm, h.2.ne]
| inr h => simp [uIoc, h, h.2.le, h.1.ne.symm, h.2.ne]
State after:
no goals

State before:
case h.mp.inl
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
h : a < t ∧ t < b
⊢ t ∈ Ι a b \ {a, b}
Tactic:
simp [uIoc, h, h.2.le, h.1.ne.symm, h.2.ne]
State after:
no goals

State before:
case h.mp.inr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
h : b < t ∧ t < a
⊢ t ∈ Ι a b \ {a, b}
Tactic:
simp [uIoc, h, h.2.le, h.1.ne.symm, h.2.ne]
State after:
no goals

State before:
case h.mpr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : t ∈ Ι a b \ {a, b}
⊢ t ∈ uIoo a b
Tactic:
simp_rw [uIoc, mem_diff, mem_Ioc, mem_insert_iff, mem_singleton_iff] at hh
State after:
case h.mpr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : (min a b < t ∧ t ≤ max a b) ∧ ¬(t = a ∨ t = b)
⊢ t ∈ uIoo a b

State before:
case h.mpr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : (min a b < t ∧ t ≤ max a b) ∧ ¬(t = a ∨ t = b)
⊢ t ∈ uIoo a b
Tactic:
push_neg at hh
State after:
case h.mpr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : (min a b < t ∧ t ≤ max a b) ∧ t ≠ a ∧ t ≠ b
⊢ t ∈ uIoo a b

State before:
case h.mpr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : (min a b < t ∧ t ≤ max a b) ∧ t ≠ a ∧ t ≠ b
⊢ t ∈ uIoo a b
Tactic:
refine ⟨hh.1.1, lt_of_le_of_ne hh.1.2 ?_⟩
State after:
case h.mpr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : (min a b < t ∧ t ≤ max a b) ∧ t ≠ a ∧ t ≠ b
⊢ t ≠ a ⊔ b

State before:
case h.mpr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
t : ℝ
hh : (min a b < t ∧ t ≤ max a b) ∧ t ≠ a ∧ t ≠ b
⊢ t ≠ a ⊔ b
Tactic:
cases le_total a b <;> simp [*]
State after:
no goals