awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
C : ℝ≥0
inst_4 : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → F) v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : ((↑C : ℝ) + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
v : E
hv : Membership.mem (γ := Set E) (ball 0 r) v
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : Membership.mem (γ := Set E) (sphere 0 1) w
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
bc : 0 ≤ (↑C : ℝ)
bc₁ bc₂ : 0 ≤ ρ
bc₃ : 0 ≤ ‖L‖
⊢ (↑C : ℝ) * (ρ * ‖w - y‖) + ρ * (‖L‖ * ‖y - w‖) + δ * ρ ≤ (↑C : ℝ) * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ

Tactic:
gcongr
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
C : ℝ≥0
inst_4 : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → F) v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : ((↑C : ℝ) + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
v : E
hv : Membership.mem (γ := Set E) (ball 0 r) v
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : Membership.mem (γ := Set E) (sphere 0 1) w
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
⊢ (↑C : ℝ) * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ = ((↑C : ℝ) + ‖L‖ + 1) * δ * ρ

Tactic:
ring
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
C : ℝ≥0
inst_4 : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → F) v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : ((↑C : ℝ) + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
v : E
hv : Membership.mem (γ := Set E) (ball 0 r) v
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : Membership.mem (γ := Set E) (sphere 0 1) w
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
rw : ε * ρ = ε * ‖v‖
rw₁ rw₂ : ε * ‖v‖ = ε * ‖v‖
⊢ ((↑C : ℝ) + ‖L‖ + 1) * δ * ρ = ε * ‖v‖

Tactic:
rw [hδ, hρ]
-- Module: Mathlib.Analysis.Calculus.Rademacher
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), s.Countable ∧ Dense s

Tactic:
TopologicalSpace.exists_countable_dense E

Premises used: TopologicalSpace.exists_countable_dense
-- Module: Mathlib.Analysis.Calculus.Rademacher
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
obtain : ∀ (s : Set E) (s_count : s.Countable) (s_dense : Dense s), ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x
⊢ ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x

Tactic:
obtain ⟨s, s_count, s_dense⟩ : ∃ (s : Set E), s.Countable ∧ Dense s :=
    TopologicalSpace.exists_countable_dense E

Premises used: TopologicalSpace.exists_countable_dense, Set
-- Module: Mathlib.Analysis.Calculus.Rademacher
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
s_count : s.Countable
s_dense : Dense s
rw : Subset.{u_1} (α := Set E) (sphere 0 1) univ
⊢ sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
rw [s_dense.closure_eq]

Premises used: Dense.closure_eq
-- Module: Mathlib.Analysis.Calculus.Rademacher
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
s_count : s.Countable
s_dense : Dense s
⊢ Subset.{u_1} (α := Set E) (sphere 0 1) univ

Tactic:
subset_univ _

Premises used: Set.subset_univ
-- Module: Mathlib.Analysis.Calculus.Rademacher
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
s_count : s.Countable
s_dense : Dense s
⊢ Subset.{u_1} (α := Set E) (sphere 0 1) univ

Tactic:
exact subset_univ _

Premises used: Set.subset_univ
-- Module: Mathlib.Analysis.Calculus.Rademacher
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
s_count : s.Countable
s_dense : Dense s
⊢ sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
have hs : sphere 0 1 ⊆ closure s := by rw [s_dense.closure_eq]; exact subset_univ _
-- Module: Mathlib.Analysis.Calculus.Rademacher
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
s_count : s.Countable
s_dense : Dense s
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h : ∀ (a : E), (∃ (L : StrongDual ℝ E), ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → ℝ) v) a v) → DifferentiableAt ℝ f a
⊢ ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x

Tactic:
filter_upwards [hf.ae_exists_fderiv_of_countable s_count]

Premises used: LipschitzWith.ae_exists_fderiv_of_countable
-- Module: Mathlib.Analysis.Calculus.Rademacher
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
s_count : s.Countable
s_dense : Dense s
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : E
L : StrongDual ℝ E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → ℝ) v) x v
⊢ DifferentiableAt ℝ f x

Tactic:
(hf.hasFDerivAt_of_hasLineDerivAt_of_closure hs hL).differentiableAt

Premises used: LipschitzWith.hasFDerivAt_of_hasLineDerivAt_of_closure, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.Rademacher
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
s_count : s.Countable
s_dense : Dense s
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : E
L : StrongDual ℝ E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → ℝ) v) x v
⊢ DifferentiableAt ℝ f x

Tactic:
exact (hf.hasFDerivAt_of_hasLineDerivAt_of_closure hs hL).differentiableAt

Premises used: LipschitzWith.hasFDerivAt_of_hasLineDerivAt_of_closure, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
s : Set E
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzOnWith C f s
⊢ ∃ (g : E → ℝ), LipschitzWith C g ∧ EqOn f g s

Tactic:
hf.extend_real

Premises used: LipschitzOnWith.extend_real
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
s : Set E
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzOnWith C f s
obtain :
  ∀ (g : E → ℝ) (g_lip : LipschitzWith C g) (hg : EqOn f g s), ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
obtain ⟨g, g_lip, hg⟩ : ∃ (g : E → ℝ), LipschitzWith C g ∧ EqOn f g s := hf.extend_real

Premises used: LipschitzOnWith.extend_real
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
s : Set E
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzOnWith C f s
g : E → ℝ
g_lip : LipschitzWith C g
hg : EqOn f g s
h : ∀ (x : E) (hx : DifferentiableAt ℝ g x) (xs : x ∈ s), DifferentiableWithinAt ℝ f s x
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
filter_upwards [g_lip.ae_differentiableAt_of_real] with x hx xs

Premises used: LipschitzWith.ae_differentiableAt_of_real
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
s : Set E
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzOnWith C f s
g : E → ℝ
g_lip : LipschitzWith C g
hg : EqOn f g s
x : E
hx : DifferentiableAt ℝ g x
xs : x ∈ s
⊢ DifferentiableWithinAt ℝ f s x

Tactic:
hx.differentiableWithinAt.congr hg (hg xs)

Premises used: DifferentiableWithinAt.congr, DifferentiableAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
s : Set E
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzOnWith C f s
g : E → ℝ
g_lip : LipschitzWith C g
hg : EqOn f g s
x : E
hx : DifferentiableAt ℝ g x
xs : x ∈ s
⊢ DifferentiableWithinAt ℝ f s x

Tactic:
exact hx.differentiableWithinAt.congr hg (hg xs)

Premises used: DifferentiableWithinAt.congr, DifferentiableAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
ι : Type u_3
inst_6 : Fintype ι
f : E → ι → ℝ
s : Set E
hf : LipschitzOnWith C f s
⊢ ∀ (i : ι), LipschitzWith (β := ℝ) 1 fun (x : ι → ℝ) ↦ x i

Tactic:
have A : ∀ i : ι, LipschitzWith 1 (fun x : ι → ℝ ↦ x i) := fun i => LipschitzWith.eval i
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
ι : Type u_3
inst_6 : Fintype ι
f : E → ι → ℝ
s : Set E
hf : LipschitzOnWith C f s
A : ∀ (i : ι), LipschitzWith (β := ℝ) 1 fun (x : ι → ℝ) ↦ x i
i : ι
hf₁ : LipschitzOnWith (β := ℝ) (1 * C) (fun (x : E) ↦ f x i) s
C₁ : ℝ≥0
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ (F := ℝ) (fun (x : E) ↦ f x i) s x

Tactic:
apply ae_differentiableWithinAt_of_mem_of_real

Premises used: LipschitzOnWith.ae_differentiableWithinAt_of_mem_of_real
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
ι : Type u_3
inst_6 : Fintype ι
f : E → ι → ℝ
s : Set E
hf : LipschitzOnWith C f s
A : ∀ (i : ι), LipschitzWith (β := ℝ) 1 fun (x : ι → ℝ) ↦ x i
i : ι
⊢ LipschitzOnWith (β := ℝ) (1 * C) (fun (x : E) ↦ f x i) s

Tactic:
LipschitzWith.comp_lipschitzOnWith (A i) hf

Premises used: LipschitzWith.comp_lipschitzOnWith
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
ι : Type u_3
inst_6 : Fintype ι
f : E → ι → ℝ
s : Set E
hf : LipschitzOnWith C f s
A : ∀ (i : ι), LipschitzWith (β := ℝ) 1 fun (x : ι → ℝ) ↦ x i
⊢ ∀ (i : ι), ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ (F := ℝ) (fun (x : E) ↦ f x i) s x

Tactic:
have : ∀ i : ι, ∀ᵐ x ∂μ, x ∈ s → DifferentiableWithinAt ℝ (fun x : E ↦ f x i) s x := fun i ↦ by
    apply ae_differentiableWithinAt_of_mem_of_real
    exact LipschitzWith.comp_lipschitzOnWith (A i) hf
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
ι : Type u_3
inst_6 : Fintype ι
f : E → ι → ℝ
s : Set E
hf : LipschitzOnWith C f s
A : ∀ (i : ι), LipschitzWith (β := ℝ) 1 fun (x : ι → ℝ) ↦ x i
this : ∀ (i : ι), ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ (F := ℝ) (fun (x : E) ↦ f x i) s x
h :
  ∀ (x : E) (hx : ∀ (i : ι), x ∈ s → DifferentiableWithinAt ℝ (F := ℝ) (fun (x : E) ↦ f x i) s x) (xs : x ∈ s),
    DifferentiableWithinAt ℝ f s x
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
filter_upwards [ae_all_iff.2 this] with x hx xs

Premises used: Iff.mpr, MeasureTheory.ae_all_iff
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
ι : Type u_3
inst_6 : Fintype ι
f : E → ι → ℝ
s : Set E
hf : LipschitzOnWith C f s
A : ∀ (i : ι), LipschitzWith (β := ℝ) 1 fun (x : ι → ℝ) ↦ x i
this : ∀ (i : ι), ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ (F := ℝ) (fun (x : E) ↦ f x i) s x
x : E
hx : ∀ (i : ι), x ∈ s → DifferentiableWithinAt ℝ (F := ℝ) (fun (x : E) ↦ f x i) s x
xs : x ∈ s
⊢ DifferentiableWithinAt ℝ f s x

Tactic:
differentiableWithinAt_pi.2 (fun i ↦ hx i xs)

Premises used: Iff.mpr, differentiableWithinAt_pi
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
ι : Type u_3
inst_6 : Fintype ι
f : E → ι → ℝ
s : Set E
hf : LipschitzOnWith C f s
A : ∀ (i : ι), LipschitzWith (β := ℝ) 1 fun (x : ι → ℝ) ↦ x i
this : ∀ (i : ι), ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ (F := ℝ) (fun (x : E) ↦ f x i) s x
x : E
hx : ∀ (i : ι), x ∈ s → DifferentiableWithinAt ℝ (F := ℝ) (fun (x : E) ↦ f x i) s x
xs : x ∈ s
⊢ DifferentiableWithinAt ℝ f s x

Tactic:
exact differentiableWithinAt_pi.2 (fun i ↦ hx i xs)

Premises used: Iff.mpr, differentiableWithinAt_pi
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
F : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : FiniteDimensional ℝ F
inst_8 : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
have :
  ∀ (A : F ≃L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ),
    ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
have A := (Basis.ofVectorSpace ℝ F).equivFun.toContinuousLinearEquiv
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
F : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : FiniteDimensional ℝ F
inst_8 : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
A : F ≃L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ
H :
  ∀ᵐ (x : E) ∂μ,
    x ∈ s →
      DifferentiableWithinAt ℝ (F := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
        ((⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘ f) s x
h :
  ∀ (x : E)
    (hx :
      x ∈ s →
        DifferentiableWithinAt ℝ (F := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
          ((⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘ f) s x)
    (xs : x ∈ s), DifferentiableWithinAt ℝ f s x
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
filter_upwards [H] with x hx xs
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
F : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : FiniteDimensional ℝ F
inst_8 : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
A : F ≃L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ
H :
  ∀ᵐ (x : E) ∂μ,
    x ∈ s →
      DifferentiableWithinAt ℝ (F := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
        ((⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘ f) s x
x : E
hx :
  x ∈ s →
    DifferentiableWithinAt ℝ (F := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
      ((⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘ f) s x
xs : x ∈ s
⊢ f =
    Function.comp (β := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
        (⇑A.symm : (a : (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) → F)
        (⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘
      f

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

Premises used: ContinuousLinearEquiv.symm_comp_self, Function.id_comp
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
F : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : FiniteDimensional ℝ F
inst_8 : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
A : F ≃L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ
H :
  ∀ᵐ (x : E) ∂μ,
    x ∈ s →
      DifferentiableWithinAt ℝ (F := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
        ((⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘ f) s x
x : E
hx :
  x ∈ s →
    DifferentiableWithinAt ℝ (F := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
      ((⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘ f) s x
xs : x ∈ s
⊢ f =
    Function.comp (β := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
        (⇑A.symm : (a : (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) → F)
        (⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘
      f

Tactic:
have : f = (A.symm ∘ A) ∘ f := by
      simp only [ContinuousLinearEquiv.symm_comp_self, Function.id_comp]
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
F : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : FiniteDimensional ℝ F
inst_8 : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
A : F ≃L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ
H :
  ∀ᵐ (x : E) ∂μ,
    x ∈ s →
      DifferentiableWithinAt ℝ (F := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
        ((⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘ f) s x
x : E
hx :
  x ∈ s →
    DifferentiableWithinAt ℝ (F := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
      ((⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘ f) s x
xs : x ∈ s
this :
  f =
    Function.comp (β := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
        (⇑A.symm : (a : (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) → F)
        (⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘
      f
h :
  DifferentiableWithinAt ℝ (F := F)
    (Function.comp (β := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
        (⇑A.symm : (a : (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) → F)
        (⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘
      f)
    s x
⊢ DifferentiableWithinAt ℝ f s x

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
F : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : FiniteDimensional ℝ F
inst_8 : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
A : F ≃L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ
H :
  ∀ᵐ (x : E) ∂μ,
    x ∈ s →
      DifferentiableWithinAt ℝ (F := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
        ((⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘ f) s x
x : E
hx :
  x ∈ s →
    DifferentiableWithinAt ℝ (F := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
      ((⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘ f) s x
xs : x ∈ s
this :
  f =
    Function.comp (β := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
        (⇑A.symm : (a : (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) → F)
        (⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘
      f
⊢ DifferentiableWithinAt ℝ (F := F)
    (Function.comp (β := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
        (⇑A.symm : (a : (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) → F)
        (⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘
      f)
    s x

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

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.differentiableAt, DifferentiableAt.comp_differentiableWithinAt