-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / (↑N : ℝ)
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  Eq (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) (⋃ (j : Fin N), E j) ∧
    PairwiseDisjoint univ E ∧
      (∀ (n : Fin N),
          ∀ x ∈ E n,
            a + ε' * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧
              (f : (a : X) → ℝ) x ≤ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ∧
        ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hE' : ∀ (n : Fin N), Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Fin N → Opens X
hV :
  ∀ (n : Fin N),
    E n ⊆ (↑(V n) : Set X) ∧
      (∀ x ∈ V n, (f : (a : X) → ℝ) x < y n + ε') ∧
        (μ : (a : Set X) → ℝ≥0∞) (↑(V n) : Set X) ≤
          HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (ENNReal.ofReal (ε' / (↑N : ℝ)))
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport (α := ℝ) (⇑(g n) : (a : X) → ℝ) ⊆ (V n).carrier) ∧
    EqOn (β := ℝ) (∑ n : Fin N, (⇑(g n) : (a : X) → ℝ)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g n : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (n : Fin N), HasCompactSupport (α := X) (β := ℝ) (⇑(g n) : (a : X) → ℝ)
calc_1 : Eq (α := ℝ) ((Λ : (a : X →C_c ℝ) → ℝ) f : ℝ) ((Λ : (a : X →C_c ℝ) → ℝ) (∑ n : Fin N, g n • f) : ℝ)
calc_2 :
  LE.le (α := ℝ) (∑ n : Fin N, (Λ : (a : X →C_c ℝ) → ℝ) (g n • f))
    (∑ n : Fin N, (Λ : (a : X →C_c ℝ) → ℝ) ((y n + ε') • g n))
calc_3 :
  ∑ n : Fin N, HMul.hMul (β := ℝ) (|a| + y n + ε') ((Λ : (a : X →C_c ℝ) → ℝ) (g n) : ℝ) -
      |a| * ∑ n : Fin N, (Λ : (a : X →C_c ℝ) → ℝ) (g n) ≤
    ∑ n : Fin N, (|a| + y n + ε') * (μ.real (E n) + ε' / (↑N : ℝ)) - |a| * ∑ n : Fin N, (Λ : (a : X →C_c ℝ) → ℝ) (g n)
calc_4 :
  ∑ n : Fin N, (|a| + y n + ε') * (μ.real (E n) + ε' / (↑N : ℝ)) - |a| * ∑ n : Fin N, (Λ : (a : X →C_c ℝ) → ℝ) (g n) ≤
    ∑ n : Fin N, (|a| + y n + ε') * (μ.real (E n) + ε' / (↑N : ℝ)) - |a| * μ.real K
⊢ (Λ : (a : X →C_c ℝ) → ℝ) f ≤ (@integral _ _ _ _ inst_2 (rieszMeasure Λ) fun (x : X) ↦ (f : (a : X) → ℝ) x) + ε
have calc_5 : ∑ n : Fin N, (|a| + y n + ε') * (μ.real (E n) + ε' / (↑N : ℝ)) - |a| * μ.real K =
  ∑ n : Fin N, (y n - ε') * μ.real (E n) + 2 * ε' * μ.real K + ε' / (↑N : ℝ) * ∑ n : Fin N, (|a| + y n + ε')
Tactic: calc Λ f
    _ = Λ (∑ n, g n • f) := ?_
    _ = ∑ n, Λ (g n • f) := by simp
    _ ≤ ∑ n, Λ ((y n + ε') • g n) := ?_
    _ = ∑ n, (y n + ε') * Λ (g n) := by simp
    -- That `y n + ε'` can be negative is bad in the inequalities so we artificially include `|a|`.
    _ = ∑ n, (|a| + y n + ε') * Λ (g n) - |a| * ∑ n, Λ (g n) := by
      simp [add_assoc, add_mul |a|, Finset.sum_add_distrib, Finset.mul_sum]
    _ ≤ ∑ n, (|a| + y n + ε') * (μ.real (E n) + ε' / N) - |a| * ∑ n, Λ (g n) := ?_
    _ ≤ ∑ n, (|a| + y n + ε') * (μ.real (E n) + ε' / N) - |a| * μ.real K := ?_
    _ = ∑ n, (y n - ε') * μ.real (E n) +
      2 * ε' * μ.real K + ε' / N * ∑ n, (|a| + y n + ε') := ?_
    _ ≤ ∫ x, f x ∂μ + 2 * ε' * μ.real K + ε' / N * ∑ n, (|a| + y n + ε') := ?_
    _ ≤ ∫ x, f x ∂μ + ε' * (2 * μ.real K + |a| + b + ε') := ?_
    _ ≤ ∫ x, f x ∂μ + ε := by simp [hε'.2]