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 ≤ 1

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 ≤ 1
c : CU X
⊢ approx (Nat.succ n) c x ≤ 1
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
n : ℕ
x : X
⊢ approx n c x ≤ 1
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 ≤ 1
exact indicator_apply_le' (fun _ => le_rfl) 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 ≤ 1
c : CU X
⊢ (approx n (left c) x + approx n (right c) x) / 2 ≤ 1
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 ≤ 1
c : CU X
⊢ approx (Nat.succ n) c x ≤ 1
simp only [approx, midpoint_eq_smul_add, invOf_eq_inv, smul_eq_mul, ← div_eq_inv_mul]
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 ≤ 1
c : CU X
this : approx n (left c) x + approx n (right c) x ≤ 1 + 1
⊢ (approx n (left c) x + approx n (right c) x) / 2 ≤ 1
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 ≤ 1
c : CU X
⊢ (approx n (left c) x + approx n (right c) x) / 2 ≤ 1
have := add_le_add (ihn (left c)) (ihn (right 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 ≤ 1
c : CU X
this : approx n (left c) x + approx n (right c) x ≤ 2
⊢ (approx n (left c) x + approx n (right c) x) / 2 ≤ 1
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 ≤ 1
c : CU X
this : approx n (left c) x + approx n (right c) x ≤ 1 + 1
⊢ (approx n (left c) x + approx n (right c) x) / 2 ≤ 1
norm_num at this
no goals
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 ≤ 1
c : CU X
this : approx n (left c) x + approx n (right c) x ≤ 2
⊢ (approx n (left c) x + approx n (right c) x) / 2 ≤ 1
exact Iff.mpr (div_le_one zero_lt_two) this