-- Mathlib/Analysis/Calculus/Rademacher.lean
theorem ae_exists_fderiv_of_countable
    (hf : LipschitzWith C f) {s : Set E} (hs : s.Countable) :
    ∀ᵐ x ∂μ, ∃ (L : E →L[ℝ] ℝ), ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v

Proof state:
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
s : Set E
hs : s.Countable
B : Basis ↑(Basis.ofVectorSpaceIndex ℝ E) ℝ E
I1 :
  ∀ᵐ (x : E) ∂μ,
    ∀ v ∈ s,
      lineDeriv ℝ f x (∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • B i) =
        ∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • lineDeriv ℝ f x (B i)
I2 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, LineDifferentiableAt ℝ f x v
x : E
hx :
  ∀ v ∈ s,
    lineDeriv ℝ f x (∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • B i) =
      ∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • lineDeriv ℝ f x (B i)
h'x : ∀ v ∈ s, LineDifferentiableAt ℝ f x v
⊢ ∃ L, ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v

Tactic:
let L : E →L[ℝ] ℝ :=
  LinearMap.toContinuousLinearMap (B.constr ℝ (fun i ↦ lineDeriv ℝ f x (B i)))

Result:
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
s : Set E
hs : s.Countable
B : Basis ↑(Basis.ofVectorSpaceIndex ℝ E) ℝ E
I1 :
  ∀ᵐ (x : E) ∂μ,
    ∀ v ∈ s,
      lineDeriv ℝ f x (∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • B i) =
        ∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • lineDeriv ℝ f x (B i)
I2 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, LineDifferentiableAt ℝ f x v
x : E
hx :
  ∀ v ∈ s,
    lineDeriv ℝ f x (∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • B i) =
      ∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • lineDeriv ℝ f x (B i)
h'x : ∀ v ∈ s, LineDifferentiableAt ℝ f x v
L : E →L[ℝ] ℝ := LinearMap.toContinuousLinearMap ((B.constr ℝ) fun i => lineDeriv ℝ f x (B i))
⊢ ∃ L, ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v

Proof state:
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
s : Set E
hs : s.Countable
B : Basis ↑(Basis.ofVectorSpaceIndex ℝ E) ℝ E
I1 :
  ∀ᵐ (x : E) ∂μ,
    ∀ v ∈ s,
      lineDeriv ℝ f x (∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • B i) =
        ∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • lineDeriv ℝ f x (B i)
I2 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, LineDifferentiableAt ℝ f x v
x : E
hx :
  ∀ v ∈ s,
    lineDeriv ℝ f x (∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • B i) =
      ∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • lineDeriv ℝ f x (B i)
h'x : ∀ v ∈ s, LineDifferentiableAt ℝ f x v
L : E →L[ℝ] ℝ := LinearMap.toContinuousLinearMap ((B.constr ℝ) fun i => lineDeriv ℝ f x (B i))
v : E
hv : v ∈ s
⊢ HasLineDerivAt ℝ f (L v) x v

Tactic:
have J : L v = lineDeriv ℝ f x v := by convert (hx v hv).symm <;> simp [L, B.sum_repr v]

Result:
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
s : Set E
hs : s.Countable
B : Basis ↑(Basis.ofVectorSpaceIndex ℝ E) ℝ E
I1 :
  ∀ᵐ (x : E) ∂μ,
    ∀ v ∈ s,
      lineDeriv ℝ f x (∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • B i) =
        ∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • lineDeriv ℝ f x (B i)
I2 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, LineDifferentiableAt ℝ f x v
x : E
hx :
  ∀ v ∈ s,
    lineDeriv ℝ f x (∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • B i) =
      ∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • lineDeriv ℝ f x (B i)
h'x : ∀ v ∈ s, LineDifferentiableAt ℝ f x v
L : E →L[ℝ] ℝ := LinearMap.toContinuousLinearMap ((B.constr ℝ) fun i => lineDeriv ℝ f x (B i))
v : E
hv : v ∈ s
J : L v = lineDeriv ℝ f x v
⊢ HasLineDerivAt ℝ f (L v) x v

Proof state:
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
s : Set E
hs : s.Countable
B : Basis ↑(Basis.ofVectorSpaceIndex ℝ E) ℝ E
I1 :
  ∀ᵐ (x : E) ∂μ,
    ∀ v ∈ s,
      lineDeriv ℝ f x (∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • B i) =
        ∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • lineDeriv ℝ f x (B i)
I2 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, LineDifferentiableAt ℝ f x v
x : E
hx :
  ∀ v ∈ s,
    lineDeriv ℝ f x (∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • B i) =
      ∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • lineDeriv ℝ f x (B i)
h'x : ∀ v ∈ s, LineDifferentiableAt ℝ f x v
L : E →L[ℝ] ℝ := LinearMap.toContinuousLinearMap ((B.constr ℝ) fun i => lineDeriv ℝ f x (B i))
v : E
hv : v ∈ s
J : L v = lineDeriv ℝ f x v
⊢ HasLineDerivAt ℝ f (L v) x v

Tactic:
simpa [J] using (h'x v hv).hasLineDerivAt

Result:
no goals

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
s : Set E
hs : s.Countable
⊢ ∀ᵐ (x : E) ∂μ, ∃ L, ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v

Tactic:
have B := Basis.ofVectorSpace ℝ E

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
s : Set E
hs : s.Countable
B : Basis ↑(Basis.ofVectorSpaceIndex ℝ E) ℝ E
⊢ ∀ᵐ (x : E) ∂μ, ∃ L, ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
s : Set E
hs : s.Countable
B : Basis ↑(Basis.ofVectorSpaceIndex ℝ E) ℝ E
⊢ ∀ᵐ (x : E) ∂μ, ∃ L, ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v

Tactic:
have I1 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, lineDeriv ℝ f x (∑ i, (B.repr v i) • B i) =
                                ∑ i, B.repr v i • lineDeriv ℝ f x (B i) :=
  (ae_ball_iff hs).2 (fun v _ ↦ hf.ae_lineDeriv_sum_eq _ _ _)

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
s : Set E
hs : s.Countable
B : Basis ↑(Basis.ofVectorSpaceIndex ℝ E) ℝ E
I1 :
  ∀ᵐ (x : E) ∂μ,
    ∀ v ∈ s,
      lineDeriv ℝ f x (∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • B i) =
        ∑ i : ↑(Basis.ofVectorSpaceIndex ℝ E), (B.repr v) i • lineDeriv ℝ f x (B i)
⊢ ∀ᵐ (x : E) ∂μ, ∃ L, ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v