case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : x ∈ c✝.C
c : CU X
hx : x ∈ c.C
⊢ approx Nat.zero c x = 0

case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : x ∈ c✝.C
n : ℕ
ihn : ∀ (c : CU X), x ∈ c.C → approx n c x = 0
c : CU X
hx : x ∈ c.C
⊢ approx (Nat.succ n) c x = 0
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
n : ℕ
x : X
hx : x ∈ c.C
⊢ approx n c x = 0
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
hx✝ : x ∈ c✝.C
c : CU X
hx : x ∈ c.C
⊢ approx Nat.zero c x = 0
exact indicator_of_not_mem (fun (hU : x ∈ c.Uᶜ) => hU <| c.subset hx) _
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : x ∈ c✝.C
n : ℕ
ihn : ∀ (c : CU X), x ∈ c.C → approx n c x = 0
c : CU X
hx : x ∈ c.C
⊢ midpoint ℝ (approx n (left c) x) (approx n (right c) x) = 0
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : x ∈ c✝.C
n : ℕ
ihn : ∀ (c : CU X), x ∈ c.C → approx n c x = 0
c : CU X
hx : x ∈ c.C
⊢ approx (Nat.succ n) c x = 0
simp only [approx]
case succ.hx
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : x ∈ c✝.C
n : ℕ
ihn : ∀ (c : CU X), x ∈ c.C → approx n c x = 0
c : CU X
hx : x ∈ c.C
⊢ x ∈ (right c).C

case succ.hx
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : x ∈ c✝.C
n : ℕ
ihn : ∀ (c : CU X), x ∈ c.C → approx n c x = 0
c : CU X
hx : x ∈ c.C
⊢ x ∈ (left c).C
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : x ∈ c✝.C
n : ℕ
ihn : ∀ (c : CU X), x ∈ c.C → approx n c x = 0
c : CU X
hx : x ∈ c.C
⊢ midpoint ℝ (approx n (left c) x) (approx n (right c) x) = 0
rw [ihn, ihn, midpoint_self]
no goals
case succ.hx
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : x ∈ c✝.C
n : ℕ
ihn : ∀ (c : CU X), x ∈ c.C → approx n c x = 0
c : CU X
hx : x ∈ c.C
⊢ x ∈ (right c).C

case succ.hx
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : x ∈ c✝.C
n : ℕ
ihn : ∀ (c : CU X), x ∈ c.C → approx n c x = 0
c : CU X
hx : x ∈ c.C
⊢ x ∈ (left c).C
exacts [c.subset_right_C hx, hx]