-- 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:
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

Tactic:
have I2 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, LineDifferentiableAt ℝ f x v :=
  (ae_ball_iff hs).2 (fun v _ ↦ hf.ae_lineDifferentiableAt v)

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)
I2 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, LineDifferentiableAt ℝ f x v
⊢ ∀ᵐ (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
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) ∂μ, ∃ L, ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v

Tactic:
filter_upwards [I1, I2] with x hx h'x

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, ∀ 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))
⊢ ∃ L, ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v

Tactic:
refine ⟨L, fun v hv ↦ ?_⟩

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
⊢ 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
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
⊢ L v = lineDeriv ℝ f x v

Tactic:
convert (hx v hv).symm <;> simp [L, B.sum_repr v]

Result:
no goals