Theorem: localOscillation_of_same (Carleson/Theorem1_1/Carleson_on_the_real_line.lean)

State before:
X : Type
inst✝ : PseudoMetricSpace X
E : Set X
f : C(X, ℂ)
⊢ localOscillation E f f = 0
Tactic:
rw [localOscillation]
State after:
X : Type
inst✝ : PseudoMetricSpace X
E : Set X
f : C(X, ℂ)
⊢ ⨆ z ∈ E ×ˢ E, ‖f z.1 - f z.1 - f z.2 + f z.2‖ = 0

State before:
X : Type
inst✝ : PseudoMetricSpace X
E : Set X
f : C(X, ℂ)
⊢ ⨆ z ∈ E ×ˢ E, ‖f z.1 - f z.1 - f z.2 + f z.2‖ = 0
Tactic:
simp only [Set.mem_prod, sub_self, zero_sub, add_left_neg, norm_zero, Real.ciSup_const_zero]
State after:
no goals