-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
s : Set E
hs : s.Countable
B : Basis (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) ℝ E
I1 :
  ∀ᵐ (x : E) ∂μ,
    ∀ v ∈ s,
      lineDeriv ℝ f x
          (∑ i : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1),
            HSMul.hSMul (α := ℝ) (β := E)
              ((((B.repr : (a : E) → (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) v :
                      (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) :
                    (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → ℝ)
                  i :
                ℝ)
              ((B : (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → E) i : E)) =
        ∑ i : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1),
          HSMul.hSMul (α := ℝ)
            ((((B.repr : (a : E) → (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) v :
                    (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) :
                  (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → ℝ)
                i :
              ℝ)
            (lineDeriv ℝ f x ((B : (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → E) i))
I2 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, LineDifferentiableAt ℝ f x v
x : E
hx :
  ∀ v ∈ s,
    lineDeriv ℝ f x
        (∑ i : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1),
          HSMul.hSMul (α := ℝ) (β := E)
            ((((B.repr : (a : E) → (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) v :
                    (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) :
                  (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → ℝ)
                i :
              ℝ)
            ((B : (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → E) i : E)) =
      ∑ i : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1),
        HSMul.hSMul (α := ℝ)
          ((((B.repr : (a : E) → (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) v :
                  (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) :
                (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → ℝ)
              i :
            ℝ)
          (lineDeriv ℝ f x ((B : (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → E) i))
h'x : ∀ v ∈ s, LineDifferentiableAt ℝ f x v
L : StrongDual ℝ E :=
  ((LinearMap.toContinuousLinearMap : (E →ₗ[ℝ] ℝ) ≃ₗ[ℝ] E →L[ℝ] ℝ) : (a : E →ₗ[ℝ] ℝ) → E →L[ℝ] ℝ)
    ((B.constr ℝ : (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) → ℝ) → E →ₗ[ℝ] ℝ)
        fun (i : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) ↦
        lineDeriv ℝ f x ((B : (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → E) i) :
      E →ₗ[ℝ] ℝ)
v : E
hv : v ∈ s
h :
  Eq (α := ℝ) ((L : (a : E) → ℝ) v : ℝ)
    (∑ i : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1),
        HSMul.hSMul (α := ℝ)
          ((((B.repr : (a : E) → (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) v :
                  (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) :
                (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → ℝ)
              i :
            ℝ)
          (lineDeriv ℝ f x ((B : (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → E) i)) :
      ℝ)
⊢ (L : (a : E) → ℝ) v = lineDeriv ℝ f x v
have h₁ : v =
  ∑ i : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1),
    HSMul.hSMul (α := ℝ) (β := E)
      ((((B.repr : (a : E) → (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) v :
              (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) :
            (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → ℝ)
          i :
        ℝ)
      ((B : (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → E) i : E)
Tactic: convert! (hx v hv).symm