-- Mathlib/Analysis/BoundedVariation.lean
theorem ae_differentiableWithinAt_of_mem {f : ℝ → V} {s : Set ℝ}
    (h : LocallyBoundedVariationOn f s) : ∀ᵐ x, x ∈ s → DifferentiableWithinAt ℝ f s x

Proof state:
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ V) → ℝ := (Basis.ofVectorSpace ℝ V).equivFun.toContinuousLinearEquiv
H : ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
filter_upwards [H] with x hx xs

Result:
case h
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ V) → ℝ := (Basis.ofVectorSpace ℝ V).equivFun.toContinuousLinearEquiv
H : ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
x : ℝ
hx : x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
xs : x ∈ s
⊢ DifferentiableWithinAt ℝ f s x

Proof state:
case h
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ V) → ℝ := (Basis.ofVectorSpace ℝ V).equivFun.toContinuousLinearEquiv
H : ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
x : ℝ
hx : x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
xs : x ∈ s
this : f = (⇑A.symm ∘ ⇑A) ∘ f
⊢ DifferentiableWithinAt ℝ ((⇑A.symm ∘ ⇑A) ∘ f) s x

Tactic:
exact A.symm.differentiableAt.comp_differentiableWithinAt x (hx xs)

Result:
no goals

Proof state:
case h
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ V) → ℝ := (Basis.ofVectorSpace ℝ V).equivFun.toContinuousLinearEquiv
⊢ LocallyBoundedVariationOn (⇑A ∘ f) s

Tactic:
exact A.lipschitz.comp_locallyBoundedVariationOn h

Result:
no goals

Proof state:
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ V) → ℝ := (Basis.ofVectorSpace ℝ V).equivFun.toContinuousLinearEquiv
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
suffices H : ∀ᵐ x, x ∈ s → DifferentiableWithinAt ℝ (A ∘ f) s x by
  filter_upwards [H] with x hx xs
  have : f = (A.symm ∘ A) ∘ f := by
    simp only [ContinuousLinearEquiv.symm_comp_self, Function.id_comp]
  rw [this]
  exact A.symm.differentiableAt.comp_differentiableWithinAt x (hx xs)

Result:
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ V) → ℝ := (Basis.ofVectorSpace ℝ V).equivFun.toContinuousLinearEquiv
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x

Proof state:
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
let A := (Basis.ofVectorSpace ℝ V).equivFun.toContinuousLinearEquiv

Result:
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ V) → ℝ := (Basis.ofVectorSpace ℝ V).equivFun.toContinuousLinearEquiv
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x

Proof state:
case h
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ V) → ℝ := (Basis.ofVectorSpace ℝ V).equivFun.toContinuousLinearEquiv
H : ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
x : ℝ
hx : x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
xs : x ∈ s
⊢ DifferentiableWithinAt ℝ f s x

Tactic:
have : f = (A.symm ∘ A) ∘ f := by
  simp only [ContinuousLinearEquiv.symm_comp_self, Function.id_comp]

Result:
case h
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ V) → ℝ := (Basis.ofVectorSpace ℝ V).equivFun.toContinuousLinearEquiv
H : ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
x : ℝ
hx : x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
xs : x ∈ s
this : f = (⇑A.symm ∘ ⇑A) ∘ f
⊢ DifferentiableWithinAt ℝ f s x

Proof state:
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ V) → ℝ := (Basis.ofVectorSpace ℝ V).equivFun.toContinuousLinearEquiv
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x

Tactic:
apply ae_differentiableWithinAt_of_mem_pi

Result:
case h
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ V) → ℝ := (Basis.ofVectorSpace ℝ V).equivFun.toContinuousLinearEquiv
⊢ LocallyBoundedVariationOn (⇑A ∘ f) s

Proof state:
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ V) → ℝ := (Basis.ofVectorSpace ℝ V).equivFun.toContinuousLinearEquiv
H : ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
x : ℝ
hx : x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
xs : x ∈ s
⊢ f = (⇑A.symm ∘ ⇑A) ∘ f

Tactic:
simp only [ContinuousLinearEquiv.symm_comp_self, Function.id_comp]

Result:
no goals

Proof state:
case h
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ V) → ℝ := (Basis.ofVectorSpace ℝ V).equivFun.toContinuousLinearEquiv
H : ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
x : ℝ
hx : x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
xs : x ∈ s
this : f = (⇑A.symm ∘ ⇑A) ∘ f
⊢ DifferentiableWithinAt ℝ f s x

Tactic:
rw [this]

Result:
case h
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ V) → ℝ := (Basis.ofVectorSpace ℝ V).equivFun.toContinuousLinearEquiv
H : ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
x : ℝ
hx : x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
xs : x ∈ s
this : f = (⇑A.symm ∘ ⇑A) ∘ f
⊢ DifferentiableWithinAt ℝ ((⇑A.symm ∘ ⇑A) ∘ f) s x