-- 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) → ℝ)
this_1 : ∀ (n : Fin N), (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
this : ∑ i : Fin N, μ.real (E i) = μ.real K
linarith linarith₁ linarith₂ linarith₃ linarith₄ linarith₅ linarith₆ :
  (|a| + 2 * ε') * μ.real K + ∑ x : Fin N, (y x - ε') * μ.real (E x) +
          (∑ i : Fin N, (|a| + y i + ε')) * (ε' / (↑N : ℝ)) -
        |a| * μ.real K <
      ∑ n : Fin N, (y n - ε') * μ.real (E n) + 2 * ε' * μ.real K + ε' / (↑N : ℝ) * ∑ n : Fin N, (|a| + y n + ε') →
    HMul.hMul (α := ℝ) 1 1 = 1
linarith₇ :
  (|a| + 2 * ε') * μ.real K + ∑ x : Fin N, (y x - ε') * μ.real (E x) +
          (∑ i : Fin N, (|a| + y i + ε')) * (ε' / (↑N : ℝ)) -
        |a| * μ.real K <
      ∑ n : Fin N, (y n - ε') * μ.real (E n) + 2 * ε' * μ.real K + ε' / (↑N : ℝ) * ∑ n : Fin N, (|a| + y n + ε') →
    (1 * |a| + HMul.hMul (α := ℝ) 1 2 * (1 * ε')) * (1 * μ.real K) +
              HMul.hMul (α := ℝ) 1 (∑ x : Fin N, (y x - ε') * μ.real (E x)) +
            HMul.hMul (α := ℝ) 1 (∑ i : Fin N, (|a| + y i + ε')) * (1 * (ε' / (↑N : ℝ))) -
          1 * |a| * (1 * μ.real K) -
        (HMul.hMul (α := ℝ) 1 (∑ x : Fin N, (y x - ε') * μ.real (E x)) +
            HMul.hMul (α := ℝ) 1 2 * (1 * ε') * (1 * μ.real K) +
          1 * (ε' / (↑N : ℝ)) * HMul.hMul (α := ℝ) 1 (∑ i : Fin N, (|a| + y i + ε'))) =
      0
⊢ (|a| + 2 * ε') * μ.real K + ∑ x : Fin N, (y x - ε') * μ.real (E x) +
        (∑ i : Fin N, (|a| + y i + ε')) * (ε' / (↑N : ℝ)) -
      |a| * μ.real K =
    ∑ n : Fin N, (y n - ε') * μ.real (E n) + 2 * ε' * μ.real K + ε' / (↑N : ℝ) * ∑ n : Fin N, (|a| + y n + ε')
have linarith₈ : ∑ n : Fin N, (y n - ε') * μ.real (E n) + 2 * ε' * μ.real K + ε' / (↑N : ℝ) * ∑ n : Fin N, (|a| + y n + ε') <
    (|a| + 2 * ε') * μ.real K + ∑ x : Fin N, (y x - ε') * μ.real (E x) +
        (∑ i : Fin N, (|a| + y i + ε')) * (ε' / (↑N : ℝ)) -
      |a| * μ.real K →
  HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith