case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
c : CU X
⊢ approx Nat.zero c x ∈ Icc (approx Nat.zero (right c) x) (approx Nat.zero (left c) x)

case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ∈ Icc (approx n (right c) x) (approx n (left c) x)
c : CU X
⊢ approx (Nat.succ n) c x ∈ Icc (approx (Nat.succ n) (right c) x) (approx (Nat.succ n) (left c) x)
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
n : ℕ
x : X
⊢ approx n c x ∈ Icc (approx n (right c) x) (approx n (left c) x)
induction' n with n ihn generalizing c
no goals
case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
c : CU X
⊢ approx Nat.zero c x ∈ Icc (approx Nat.zero (right c) x) (approx Nat.zero (left c) x)
exact ⟨le_rfl, indicator_le_indicator_of_subset (compl_subset_compl.2 c.left_U_subset)
  (fun _ => zero_le_one) _⟩
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ∈ Icc (approx n (right c) x) (approx n (left c) x)
c : CU X
⊢ midpoint ℝ (approx n (left (right c)) x) (approx n (right (right c)) x) ≤
      midpoint ℝ (approx n (left c) x) (approx n (right c) x) ∧
    midpoint ℝ (approx n (left c) x) (approx n (right c) x) ≤
      midpoint ℝ (approx n (left (left c)) x) (approx n (right (left c)) x)
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ∈ Icc (approx n (right c) x) (approx n (left c) x)
c : CU X
⊢ approx (Nat.succ n) c x ∈ Icc (approx (Nat.succ n) (right c) x) (approx (Nat.succ n) (left c) x)
simp only [approx, mem_Icc]
case succ.refine'_1.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ∈ Icc (approx n (right c) x) (approx n (left c) x)
c : CU X
⊢ (left c).U ⊆ (left (right c)).C

case succ.refine'_2.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ∈ Icc (approx n (right c) x) (approx n (left c) x)
c : CU X
⊢ (right (left c)).U ⊆ (right c).C
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ∈ Icc (approx n (right c) x) (approx n (left c) x)
c : CU X
⊢ midpoint ℝ (approx n (left (right c)) x) (approx n (right (right c)) x) ≤
      midpoint ℝ (approx n (left c) x) (approx n (right c) x) ∧
    midpoint ℝ (approx n (left c) x) (approx n (right c) x) ≤
      midpoint ℝ (approx n (left (left c)) x) (approx n (right (left c)) x)
refine' ⟨midpoint_le_midpoint _ (ihn _).1, midpoint_le_midpoint (ihn _).2 _⟩ <;>
  apply approx_le_approx_of_U_sub_C
no goals
case succ.refine'_1.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ∈ Icc (approx n (right c) x) (approx n (left c) x)
c : CU X
⊢ (left c).U ⊆ (left (right c)).C

case succ.refine'_2.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ∈ Icc (approx n (right c) x) (approx n (left c) x)
c : CU X
⊢ (right (left c)).U ⊆ (right c).C
exacts [subset_closure, subset_closure]