-- Mathlib/Topology/UrysohnsLemma.lean
theorem approx_mem_Icc_right_left (c : CU P) (n : ℕ) (x : X) :
    c.approx n x ∈ Icc (c.right.approx n x) (c.left.approx n x)

Proof state:
case zero
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
c : CU P
⊢ approx 0 c x ∈ Icc (approx 0 c.right x) (approx 0 c.left x)

Tactic:
exact ⟨le_rfl, indicator_le_indicator_of_subset (compl_subset_compl.2 c.left_U_subset)
  (fun _ => zero_le_one) _⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
c : CU P
n : ℕ
x : X
⊢ approx n c x ∈ Icc (approx n c.right x) (approx n c.left x)

Tactic:
induction n generalizing c with
| zero =>
  exact ⟨le_rfl, indicator_le_indicator_of_subset (compl_subset_compl.2 c.left_U_subset)
    (fun _ => zero_le_one) _⟩
| succ n ihn =>
  simp only [approx, mem_Icc]
  refine ⟨midpoint_le_midpoint ?_ (ihn _).1, midpoint_le_midpoint (ihn _).2 ?_⟩ <;>
    apply approx_le_approx_of_U_sub_C
  exacts [subset_closure, subset_closure]

Result:
no goals

Proof state:
case succ.refine_1.h
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ∈ Icc (approx n c.right x) (approx n c.left x)
c : CU P
⊢ c.left.U ⊆ c.right.left.C

case succ.refine_2.h
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ∈ Icc (approx n c.right x) (approx n c.left x)
c : CU P
⊢ c.left.right.U ⊆ c.right.C

Tactic:
exacts [subset_closure, subset_closure]

Result:
no goals

Proof state:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ∈ Icc (approx n c.right x) (approx n c.left x)
c : CU P
⊢ approx (n + 1) c x ∈ Icc (approx (n + 1) c.right x) (approx (n + 1) c.left x)

Tactic:
simp only [approx, mem_Icc]

Result:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ∈ Icc (approx n c.right x) (approx n c.left x)
c : CU P
⊢ midpoint ℝ (approx n c.right.left x) (approx n c.right.right x) ≤
      midpoint ℝ (approx n c.left x) (approx n c.right x) ∧
    midpoint ℝ (approx n c.left x) (approx n c.right x) ≤ midpoint ℝ (approx n c.left.left x) (approx n c.left.right x)

Proof state:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ∈ Icc (approx n c.right x) (approx n c.left x)
c : CU P
⊢ midpoint ℝ (approx n c.right.left x) (approx n c.right.right x) ≤
      midpoint ℝ (approx n c.left x) (approx n c.right x) ∧
    midpoint ℝ (approx n c.left x) (approx n c.right x) ≤ midpoint ℝ (approx n c.left.left x) (approx n c.left.right x)

Tactic:
refine ⟨midpoint_le_midpoint ?_ (ihn _).1, midpoint_le_midpoint (ihn _).2 ?_⟩ <;>
  apply approx_le_approx_of_U_sub_C

Result:
case succ.refine_1.h
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ∈ Icc (approx n c.right x) (approx n c.left x)
c : CU P
⊢ c.left.U ⊆ c.right.left.C

case succ.refine_2.h
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ∈ Icc (approx n c.right x) (approx n c.left x)
c : CU P
⊢ c.left.right.U ⊆ c.right.C