Theorem: Tutorial.nestedIntervalSeq_mem (Solution/Advanced/Analysis/Lecture3.lean)

State before:
ι : Type
U : ι → Set ℝ
n : ℕ
⊢ nestedIntervalSeq U n ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
Tactic:
simp only [mem_Icc, nestedIntervalSeq]
State after:
ι : Type
U : ι → Set ℝ
n : ℕ
⊢ (nestedInterval U n).1 ≤ ((nestedInterval U n).1 + (nestedInterval U n).2) / 2 ∧
    ((nestedInterval U n).1 + (nestedInterval U n).2) / 2 ≤ (nestedInterval U n).2

State before:
ι : Type
U : ι → Set ℝ
n : ℕ
⊢ (nestedInterval U n).1 ≤ ((nestedInterval U n).1 + (nestedInterval U n).2) / 2 ∧
    ((nestedInterval U n).1 + (nestedInterval U n).2) / 2 ≤ (nestedInterval U n).2
Tactic:
have := nestedInterval_le U n
State after:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
⊢ (nestedInterval U n).1 ≤ ((nestedInterval U n).1 + (nestedInterval U n).2) / 2 ∧
    ((nestedInterval U n).1 + (nestedInterval U n).2) / 2 ≤ (nestedInterval U n).2

State before:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
⊢ (nestedInterval U n).1 ≤ ((nestedInterval U n).1 + (nestedInterval U n).2) / 2 ∧
    ((nestedInterval U n).1 + (nestedInterval U n).2) / 2 ≤ (nestedInterval U n).2
Tactic:
split_ands <;> linarith
State after:
no goals