awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
s : Set ℝ
p q : ℝ → ℝ
hp : MonotoneOn p s
hq : MonotoneOn q s
h : LocallyBoundedVariationOn (p - q) s
x : ℝ
hxp : x ∈ s → DifferentiableWithinAt ℝ p s x
hxq : x ∈ s → DifferentiableWithinAt ℝ q s x
xs : x ∈ s
⊢ DifferentiableWithinAt ℝ (p - q) s x

Tactic:
exact (hxp xs).sub (hxq xs)

Premises used: DifferentiableWithinAt.sub
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
ι : Type u_2
inst : Fintype ι
f : ℝ → ι → ℝ
s : Set ℝ
h : LocallyBoundedVariationOn 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.BoundedVariation
Goal:
ι : Type u_2
inst : Fintype ι
f : ℝ → ι → ℝ
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : ∀ (i : ι), LipschitzWith (β := ℝ) 1 fun (x : ι → ℝ) ↦ x i
i : ι
h₁ : LocallyBoundedVariationOn (E := ℝ) (fun (x : ℝ) ↦ f x i) s
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (F := ℝ) (fun (x : ℝ) ↦ f x i) s x

Tactic:
apply ae_differentiableWithinAt_of_mem_real

Premises used: LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem_real
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
ι : Type u_2
inst : Fintype ι
f : ℝ → ι → ℝ
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : ∀ (i : ι), LipschitzWith (β := ℝ) 1 fun (x : ι → ℝ) ↦ x i
i : ι
⊢ LocallyBoundedVariationOn (E := ℝ) (fun (x : ℝ) ↦ f x i) s

Tactic:
LipschitzWith.comp_locallyBoundedVariationOn (A i) h

Premises used: LipschitzWith.comp_locallyBoundedVariationOn
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
ι : Type u_2
inst : Fintype ι
f : ℝ → ι → ℝ
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : ∀ (i : ι), LipschitzWith (β := ℝ) 1 fun (x : ι → ℝ) ↦ x i
i : ι
⊢ LocallyBoundedVariationOn (E := ℝ) (fun (x : ℝ) ↦ f x i) s

Tactic:
exact LipschitzWith.comp_locallyBoundedVariationOn (A i) h

Premises used: LipschitzWith.comp_locallyBoundedVariationOn
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
ι : Type u_2
inst : Fintype ι
f : ℝ → ι → ℝ
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : ∀ (i : ι), LipschitzWith (β := ℝ) 1 fun (x : ι → ℝ) ↦ x i
⊢ ∀ (i : ι), ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (F := ℝ) (fun (x : ℝ) ↦ f x i) s x

Tactic:
have : ∀ i : ι, ∀ᵐ x, x ∈ s → DifferentiableWithinAt ℝ (fun x : ℝ => f x i) s x := fun i ↦ by
    apply ae_differentiableWithinAt_of_mem_real
    exact LipschitzWith.comp_locallyBoundedVariationOn (A i) h
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
ι : Type u_2
inst : Fintype ι
f : ℝ → ι → ℝ
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : ∀ (i : ι), LipschitzWith (β := ℝ) 1 fun (x : ι → ℝ) ↦ x i
this : ∀ (i : ι), ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (F := ℝ) (fun (x : ℝ) ↦ f x i) s x
h₁ :
  ∀ (x : ℝ) (hx : ∀ (i : ι), x ∈ s → DifferentiableWithinAt ℝ (F := ℝ) (fun (x : ℝ) ↦ f x i) s x) (xs : x ∈ s),
    DifferentiableWithinAt ℝ f s x
⊢ ∀ᵐ (x : ℝ), 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.BoundedVariation
Goal:
ι : Type u_2
inst : Fintype ι
f : ℝ → ι → ℝ
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : ∀ (i : ι), LipschitzWith (β := ℝ) 1 fun (x : ι → ℝ) ↦ x i
this : ∀ (i : ι), ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (F := ℝ) (fun (x : ℝ) ↦ f x i) s x
x : ℝ
hx : ∀ (i : ι), x ∈ s → DifferentiableWithinAt ℝ (F := ℝ) (fun (x : ℝ) ↦ 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.BoundedVariation
Goal:
ι : Type u_2
inst : Fintype ι
f : ℝ → ι → ℝ
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : ∀ (i : ι), LipschitzWith (β := ℝ) 1 fun (x : ι → ℝ) ↦ x i
this : ∀ (i : ι), ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (F := ℝ) (fun (x : ℝ) ↦ f x i) s x
x : ℝ
hx : ∀ (i : ι), x ∈ s → DifferentiableWithinAt ℝ (F := ℝ) (fun (x : ℝ) ↦ 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.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Module.Basis.equivFun (Module.Basis.ofVectorSpace ℝ V))
H :
  ∀ᵐ (x : ℝ),
    x ∈ s →
      DifferentiableWithinAt ℝ (F := (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ)
        ((⇑A : (a : V) → (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ) ∘ f) s x
h₁ :
  ∀ (x : ℝ)
    (hx :
      x ∈ s →
        DifferentiableWithinAt ℝ (F := (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ)
          ((⇑A : (a : V) → (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ) ∘ f) s x)
    (xs : x ∈ s), DifferentiableWithinAt ℝ f s x
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
filter_upwards [H] with x hx xs
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Module.Basis.equivFun (Module.Basis.ofVectorSpace ℝ V))
H :
  ∀ᵐ (x : ℝ),
    x ∈ s →
      DifferentiableWithinAt ℝ (F := (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ)
        ((⇑A : (a : V) → (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ) ∘ f) s x
x : ℝ
hx :
  x ∈ s →
    DifferentiableWithinAt ℝ (F := (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ)
      ((⇑A : (a : V) → (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ) ∘ f) s x
xs : x ∈ s
⊢ DifferentiableWithinAt ℝ f s x

Tactic:
(ContinuousLinearEquiv.comp_differentiableWithinAt_iff _).mp (hx xs)

Premises used: Iff.mp, ContinuousLinearEquiv.comp_differentiableWithinAt_iff
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Module.Basis.equivFun (Module.Basis.ofVectorSpace ℝ V))
H :
  ∀ᵐ (x : ℝ),
    x ∈ s →
      DifferentiableWithinAt ℝ (F := (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ)
        ((⇑A : (a : V) → (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ) ∘ f) s x
x : ℝ
hx :
  x ∈ s →
    DifferentiableWithinAt ℝ (F := (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ)
      ((⇑A : (a : V) → (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ) ∘ f) s x
xs : x ∈ s
⊢ DifferentiableWithinAt ℝ f s x

Tactic:
exact (ContinuousLinearEquiv.comp_differentiableWithinAt_iff _).mp (hx xs)

Premises used: Iff.mp, ContinuousLinearEquiv.comp_differentiableWithinAt_iff
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Module.Basis.equivFun (Module.Basis.ofVectorSpace ℝ V))
suffices :
  ∀ᵐ (x : ℝ),
    x ∈ s →
      DifferentiableWithinAt ℝ (F := (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ)
        ((⇑A : (a : V) → (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ) ∘ f) s x
⊢ ∀ᵐ (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
    exact (ContinuousLinearEquiv.comp_differentiableWithinAt_iff _).mp (hx xs)
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Module.Basis.equivFun (Module.Basis.ofVectorSpace ℝ V))
h₁ :
  LocallyBoundedVariationOn (E := (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ)
    ((⇑A : (a : V) → (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ) ∘ f) s
⊢ ∀ᵐ (x : ℝ),
    x ∈ s →
      DifferentiableWithinAt ℝ (F := (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ)
        ((⇑A : (a : V) → (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ) ∘ f) s x

Tactic:
apply ae_differentiableWithinAt_of_mem_pi

Premises used: LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem_pi
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Module.Basis.equivFun (Module.Basis.ofVectorSpace ℝ V))
⊢ LocallyBoundedVariationOn (E := (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ)
    ((⇑A : (a : V) → (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ) ∘ f) s

Tactic:
A.lipschitz.comp_locallyBoundedVariationOn h

Premises used: ContinuousLinearEquiv.lipschitz, LipschitzWith.comp_locallyBoundedVariationOn
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Module.Basis.equivFun (Module.Basis.ofVectorSpace ℝ V))
⊢ LocallyBoundedVariationOn (E := (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ)
    ((⇑A : (a : V) → (↑(Module.Basis.ofVectorSpaceIndex ℝ V) : Type u_1) → ℝ) ∘ f) s

Tactic:
exact A.lipschitz.comp_locallyBoundedVariationOn h

Premises used: ContinuousLinearEquiv.lipschitz, LipschitzWith.comp_locallyBoundedVariationOn
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
a b : ℝ
h : BoundedVariationOn f (uIcc a b)
⊢ ∀ᵐ (x : ℝ), x ≠ min a b

Tactic:
simp [ae_iff, measure_singleton]

Premises used: MeasureTheory.NoAtoms.measure_singleton, MeasureTheory.ae_iff
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
a b : ℝ
h : BoundedVariationOn f (uIcc a b)
⊢ ∀ᵐ (x : ℝ), x ≠ min a b

Tactic:
have h₁ : ∀ᵐ x, x ≠ min a b := by simp [ae_iff, measure_singleton]
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
a b : ℝ
h : BoundedVariationOn f (uIcc a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ min a b
⊢ ∀ᵐ (x : ℝ), x ≠ max a b

Tactic:
simp [ae_iff, measure_singleton]

Premises used: MeasureTheory.NoAtoms.measure_singleton, MeasureTheory.ae_iff
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
a b : ℝ
h : BoundedVariationOn f (uIcc a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ min a b
⊢ ∀ᵐ (x : ℝ), x ≠ max a b

Tactic:
have h₂ : ∀ᵐ x, x ≠ max a b := by simp [ae_iff, measure_singleton]
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
a b : ℝ
h : BoundedVariationOn f (uIcc a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ min a b
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
h₃ :
  ∀ (x : ℝ) (hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ f (uIcc a b) x) (hx₂ : x ≠ min a b) (hx₃ : x ≠ max a b)
    (hx₄ : x ∈ uIcc a b), DifferentiableAt ℝ f x
⊢ ∀ᵐ (x : ℝ), x ∈ uIcc a b → DifferentiableAt ℝ f x

Tactic:
filter_upwards [h.locallyBoundedVariationOn.ae_differentiableWithinAt_of_mem, h₁, h₂]
    with x hx₁ hx₂ hx₃ hx₄

Premises used: LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem, BoundedVariationOn.locallyBoundedVariationOn
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
a b : ℝ
h : BoundedVariationOn f (uIcc a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ min a b
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ f (uIcc a b) x
hx₂ : x ≠ min a b
hx₃ : x ≠ max a b
hx₄ : x ∈ uIcc a b
⊢ min a b ≤ x ∧ x ≤ max a b

Tactic:
rw [uIcc, mem_Icc] at hx₄

Premises used: Set.mem_Icc, Set.uIcc
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
a b : ℝ
h : BoundedVariationOn f (uIcc a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ min a b
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ f (uIcc a b) x
hx₂ : x ≠ min a b
hx₃ : x ≠ max a b
hx₄ : min a b ≤ x ∧ x ≤ max a b
⊢ DifferentiableAt ℝ f x

Tactic:
(hx₁ hx₄).differentiableAt
    (Icc_mem_nhds (lt_of_le_of_ne hx₄.left hx₂.symm) (lt_of_le_of_ne hx₄.right hx₃))

Premises used: DifferentiableWithinAt.differentiableAt, Ne.symm, And.right, And.left, lt_of_le_of_ne, Icc_mem_nhds
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
a b : ℝ
h : BoundedVariationOn f (uIcc a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ min a b
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ f (uIcc a b) x
hx₂ : x ≠ min a b
hx₃ : x ≠ max a b
hx₄ : min a b ≤ x ∧ x ≤ max a b
⊢ DifferentiableAt ℝ f x

Tactic:
exact (hx₁ hx₄).differentiableAt
    (Icc_mem_nhds (lt_of_le_of_ne hx₄.left hx₂.symm) (lt_of_le_of_ne hx₄.right hx₃))

Premises used: DifferentiableWithinAt.differentiableAt, Ne.symm, And.right, And.left, lt_of_le_of_ne, Icc_mem_nhds
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
hs : MeasurableSet s
rw : ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume s, DifferentiableWithinAt ℝ f s x

Tactic:
rw [ae_restrict_iff' hs]

Premises used: MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
hs : MeasurableSet s
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
h.ae_differentiableWithinAt_of_mem

Premises used: LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
hs : MeasurableSet s
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
exact h.ae_differentiableWithinAt_of_mem

Premises used: LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
h : LocallyBoundedVariationOn f univ
h₁ : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) univ x → DifferentiableWithinAt ℝ f univ x), DifferentiableAt ℝ f x
⊢ ∀ᵐ (x : ℝ), DifferentiableAt ℝ f x

Tactic:
filter_upwards [h.ae_differentiableWithinAt_of_mem] with x hx

Premises used: LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
h : LocallyBoundedVariationOn f univ
x : ℝ
hx : Membership.mem (γ := Set ℝ) univ x → DifferentiableWithinAt ℝ f univ x
⊢ Membership.mem (γ := Set ℝ) univ x → DifferentiableAt ℝ f x

Tactic:
rw [differentiableWithinAt_univ] at hx

Premises used: differentiableWithinAt_univ
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
h : LocallyBoundedVariationOn f univ
x : ℝ
hx : Membership.mem (γ := Set ℝ) univ x → DifferentiableAt ℝ f x
⊢ DifferentiableAt ℝ f x

Tactic:
hx (mem_univ _)

Premises used: Set.mem_univ
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
f : ℝ → V
h : LocallyBoundedVariationOn f univ
x : ℝ
hx : Membership.mem (γ := Set ℝ) univ x → DifferentiableAt ℝ f x
⊢ DifferentiableAt ℝ f x

Tactic:
exact hx (mem_univ _)

Premises used: Set.mem_univ
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
C : ℝ≥0
f : ℝ → V
s : Set ℝ
h : LipschitzOnWith C f s
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
h.locallyBoundedVariationOn.ae_differentiableWithinAt_of_mem

Premises used: LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem, LipschitzOnWith.locallyBoundedVariationOn
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
C : ℝ≥0
f : ℝ → V
s : Set ℝ
h : LipschitzOnWith C f s
hs : MeasurableSet s
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume s, DifferentiableWithinAt ℝ f s x

Tactic:
h.locallyBoundedVariationOn.ae_differentiableWithinAt hs

Premises used: LocallyBoundedVariationOn.ae_differentiableWithinAt, LipschitzOnWith.locallyBoundedVariationOn
-- Module: Mathlib.Analysis.BoundedVariation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
C : ℝ≥0
f : ℝ → V
h : LipschitzWith C f
⊢ ∀ᵐ (x : ℝ), DifferentiableAt ℝ f x

Tactic:
(h.locallyBoundedVariationOn univ).ae_differentiableAt

Premises used: LocallyBoundedVariationOn.ae_differentiableAt, Set.univ, LipschitzWith.locallyBoundedVariationOn
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
⊢ integralSum f vol (π.biUnionTagged πi) = ∑ J ∈ π.boxes, integralSum f vol (πi J)

Tactic:
(π.sum_biUnion_boxes _ _).trans <| sum_congr rfl fun J hJ => sum_congr rfl fun J' hJ' => ?_

Premises used: Multiset.toFinset, BoxIntegral.integralSum, BoxIntegral.Prepartition.sum_biUnion_boxes, Finset.biUnion, Finset.sum_congr, rfl, Eq.trans
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
refine :
  ∀ (J : Box ι) (hJ : J ∈ π.boxes) (J' : Box ι) (hJ' : J' ∈ (πi J).boxes),
    Eq.{w + 1} (α := F)
      ((((vol : (a : Box ι) → E →L[ℝ] F) J' : E →L[ℝ] F) : (a : E) → F) (f ((π.biUnionTagged πi).tag J')) : F)
      ((((vol : (a : Box ι) → E →L[ℝ] F) J' : E →L[ℝ] F) : (a : E) → F) (f ((πi J).tag J')) : F)
⊢ integralSum f vol (π.biUnionTagged πi) = ∑ J ∈ π.boxes, integralSum f vol (πi J)

Tactic:
refine (π.sum_biUnion_boxes _ _).trans <| sum_congr rfl fun J hJ => sum_congr rfl fun J' hJ' => ?_

Premises used: BoxIntegral.Prepartition.sum_biUnion_boxes, Finset.sum_congr, rfl, Eq.trans
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
J : Box ι
hJ : J ∈ π.boxes
J' : Box ι
hJ' : J' ∈ (πi J).boxes
rw rw₁ :
  Eq.{w + 1} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J' : E →L[ℝ] F) : (a : E) → F) (f ((πi J).tag J')) : F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J' : E →L[ℝ] F) : (a : E) → F) (f ((πi J).tag J')) : F)
⊢ Eq.{w + 1} (α := F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J' : E →L[ℝ] F) : (a : E) → F) (f ((π.biUnionTagged πi).tag J')) : F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J' : E →L[ℝ] F) : (a : E) → F) (f ((πi J).tag J')) : F)

Tactic:
rw [π.tag_biUnionTagged hJ hJ']

Premises used: BoxIntegral.Prepartition.tag_biUnionTagged
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
πi : (J : Box ι) → Prepartition J
hπi : ∀ J ∈ π, (πi J).IsPartition
⊢ integralSum f vol (π.biUnionPrepartition πi) = integralSum f vol π

Tactic:
(π.sum_biUnion_boxes _ _).trans (sum_congr rfl fun J hJ => ?_)

Premises used: Multiset.toFinset, BoxIntegral.integralSum, BoxIntegral.Prepartition.sum_biUnion_boxes, BoxIntegral.TaggedPrepartition.toPrepartition, Finset.biUnion, Finset.sum_congr, rfl, Eq.trans
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
πi : (J : Box ι) → Prepartition J
hπi : ∀ J ∈ π, (πi J).IsPartition
refine :
  ∀ (J : Box ι) (hJ : J ∈ π.boxes),
    Eq.{w + 1} (α := F)
      (∑ J' ∈ (πi J).boxes,
          (((vol : (a : Box ι) → E →L[ℝ] F) J' : E →L[ℝ] F) : (a : E) → F) (f ((π.biUnionPrepartition πi).tag J')) :
        F)
      ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π.tag J)) : F)
⊢ integralSum f vol (π.biUnionPrepartition πi) = integralSum f vol π

Tactic:
refine (π.sum_biUnion_boxes _ _).trans (sum_congr rfl fun J hJ => ?_)

Premises used: BoxIntegral.Prepartition.sum_biUnion_boxes, BoxIntegral.TaggedPrepartition.toPrepartition, Finset.sum_congr, rfl, Eq.trans
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
πi : (J : Box ι) → Prepartition J
hπi : ∀ J ∈ π, (πi J).IsPartition
J : Box ι
hJ : J ∈ π.boxes
J' : Box ι
hJ' : J' ∈ (πi J).boxes
rw rw₁ :
  Eq.{w + 1} (α := F) ((((vol : (a : Box ι) → E →L[ℝ] F) J' : E →L[ℝ] F) : (a : E) → F) (f (π.tag J)) : F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J' : E →L[ℝ] F) : (a : E) → F) (f (π.tag J)) : F)
⊢ Eq.{w + 1} (α := F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J' : E →L[ℝ] F) : (a : E) → F) (f (π.tag (π.biUnionIndex πi J'))) : F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J' : E →L[ℝ] F) : (a : E) → F) (f (π.tag J)) : F)

Tactic:
rw [Prepartition.biUnionIndex_of_mem _ hJ hJ']

Premises used: BoxIntegral.Prepartition.biUnionIndex_of_mem
-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
F : Type w
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
πi : (J : Box ι) → Prepartition J
hπi : ∀ J ∈ π, (πi J).IsPartition
J : Box ι
hJ : J ∈ π.boxes
⊢ Eq.{w + 1} (α := F)
    (∑ J' ∈ (πi J).boxes, (((vol : (a : Box ι) → E →L[ℝ] F) J' : E →L[ℝ] F) : (a : E) → F) (f (π.tag J)) : F)
    ((((vol : (a : Box ι) → E →L[ℝ] F) J : E →L[ℝ] F) : (a : E) → F) (f (π.tag J)) : F)

Tactic:
(vol.map ⟨⟨fun g : E →L[ℝ] F => g (f (π.tag J)), rfl⟩, fun _ _ => rfl⟩).sum_partition_boxes
        le_top (hπi J hJ)

Premises used: BoxIntegral.BoxAdditiveMap.map, AddMonoidHom.mk, BoxIntegral.TaggedPrepartition.tag, ZeroHom.mk, BoxIntegral.BoxAdditiveMap.sum_partition_boxes, le_top, DFunLike.coe, rfl