mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
⊢ iteratedDerivWithin n.succ (fun z ↦ c - f z) s x = iteratedDerivWithin n.succ (fun z ↦ -f z) s x

Tactic:
iteratedDerivWithin_succ',

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
⊢ iteratedDerivWithin n (derivWithin (fun z ↦ c - f z) s) s x = iteratedDerivWithin n.succ (fun z ↦ -f z) s x
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
n : ℕ
⊢ iteratedDerivWithin (n + 1) id s x = if n + 1 = 0 then x else if n + 1 = 1 then 1 else 0

Tactic:
iteratedDerivWithin_succ',

Goal state after:
case succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
n : ℕ
⊢ iteratedDerivWithin n (derivWithin id s) s x = if n + 1 = 0 then x else if n + 1 = 1 then 1 else 0
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
n✝ : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
𝔸 : Type u_5
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕜 𝔸
inst✝² : Module 𝔸 F
inst✝¹ : IsBoundedSMul 𝔸 F
inst✝ : IsScalarTower 𝕜 𝔸 F
n : ℕ
IH :
  ∀ {f : 𝕜 → 𝔸} {g : 𝕜 → F},
    ContDiffWithinAt 𝕜 (↑n) f s x →
      ContDiffWithinAt 𝕜 (↑n) g s x →
        iteratedDerivWithin n (f • g) s x =
          ∑ i ∈ Finset.range (n + 1), n.choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n - i) g s x
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1)) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1)) g s x
U : Set 𝕜
hU : U ∈ 𝓝[insert x s] x
H : ∀ y ∈ U, ContDiffWithinAt 𝕜 (↑(n + 1)) f s y ∧ ContDiffWithinAt 𝕜 (↑(n + 1)) g s y
⊢ iteratedDerivWithin (n + 1) (f • g) s x =
    ∑ i ∈ Finset.range (n + 1 + 1),
      (n + 1).choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n + 1 - i) g s x

Tactic:
iteratedDerivWithin_succ',

Goal state after:
case succ
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
n✝ : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
𝔸 : Type u_5
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕜 𝔸
inst✝² : Module 𝔸 F
inst✝¹ : IsBoundedSMul 𝔸 F
inst✝ : IsScalarTower 𝕜 𝔸 F
n : ℕ
IH :
  ∀ {f : 𝕜 → 𝔸} {g : 𝕜 → F},
    ContDiffWithinAt 𝕜 (↑n) f s x →
      ContDiffWithinAt 𝕜 (↑n) g s x →
        iteratedDerivWithin n (f • g) s x =
          ∑ i ∈ Finset.range (n + 1), n.choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n - i) g s x
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1)) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1)) g s x
U : Set 𝕜
hU : U ∈ 𝓝[insert x s] x
H : ∀ y ∈ U, ContDiffWithinAt 𝕜 (↑(n + 1)) f s y ∧ ContDiffWithinAt 𝕜 (↑(n + 1)) g s y
⊢ iteratedDerivWithin n (derivWithin (f • g) s) s x =
    ∑ i ∈ Finset.range (n + 1 + 1),
      (n + 1).choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n + 1 - i) g s x
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, 0 < deriv f x
⊢ StrictMonoOn f D

Tactic:
by
  intro x hx y hy
  have : DifferentiableOn ℝ f (interior D) := fun z hz =>
    (differentiableAt_of_deriv_ne_zero (hf' z hz).ne').differentiableWithinAt
  simpa only [zero_mul, sub_pos] using
    hD.mul_sub_lt_image_sub_of_lt_deriv hf this hf' x hx y hy

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), ↑(w x) ∂μ < ε / 2
f' : α → ℝ≥0∞ := fun x ↦ ↑(f x + w x)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
⊢ ∫⁻ (x : α), ↑(f x) ∂μ + ∫⁻ (x : α), ↑(w x) ∂μ + ε / 2 ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε / 2 + ε / 2

Tactic:
by grw [wint]

Goal state after:
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inr.mp
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
α : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : MulActionWithZero α ℝ
inst✝² : IsStrictOrderedModule α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hx : a • x ∈ r • s
hr : 0 < r
this : 0 < a⁻¹ • r
⊢ ∃ y, (0 < y ∧ y⁻¹ • x ∈ s) ∧ a • y = r

Tactic:
refine ⟨a⁻¹ • r, ⟨this, ?_⟩, smul_inv_smul₀ ha'.ne' _⟩

Goal state after:
case inr.mp
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
α : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : MulActionWithZero α ℝ
inst✝² : IsStrictOrderedModule α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hx : a • x ∈ r • s
hr : 0 < r
this : 0 < a⁻¹ • r
⊢ (a⁻¹ • r)⁻¹ • x ∈ s
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), ↑f x ≤ N ↑x
N_0 : N 0 = 0
s : PointedCone ℝ (E × ℝ) := { carrier := {p | N p.1 ≤ p.2}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (LinearMap.id.toPMap ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), ↑x ∈ s → 0 ≤ ↑f' x
hf'_dense : ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_nonneg : ∀ x ∈ s, 0 ≤ g x
g_eq : ∀ (x : ↥f.domain) (y : ℝ), g (↑x, y) = y - ↑f x
x : E
⊢ -g (x, 0) = g (0, N x) - g (x, N x)

Tactic:
simp [← map_sub, ← map_neg]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun x ↦ (f x).toNNReal
int_fp : Integrable (fun x ↦ ↑(fp x)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ∞
gp_integrable : Integrable (fun x ↦ (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + ↑δ
fm : α → ℝ≥0 := fun x ↦ (-f x).toNNReal
int_fm : Integrable (fun x ↦ ↑(fm x)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (fun x ↦ ↑(gm x)) μ
gmint : ∫ (x : α), ↑(fm x) ∂μ - ↑δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x ↦ ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x)).toReal - (↑↑(gm x)).toReal
⊢ ∫ (x : α), (gp x).toReal - ↑(gm x) ∂μ = ∫ (x : α), (gp x).toReal ∂μ - ∫ (x : α), ↑(gm x) ∂μ

Tactic:
exact integral_sub gp_integrable gm_integrable

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
s : Set E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
⊢ ⋂ l, {x | ∃ y ∈ s, re (l x) ≤ re (l y)} = s

Tactic:
rw [Set.iInter_ofPred]
  refine Set.Subset.antisymm (fun x hx => ?_) fun x hx l => ⟨x, hx, le_rfl⟩
  by_contra h
  obtain ⟨l, s, hlA, hl⟩ := geometric_hahn_banach_closed_point (𝕜 := 𝕜) hs₁ hs₂ h
  obtain ⟨y, hy, hxy⟩ := hx l
  exact ((hxy.trans_lt (hlA y hy)).trans hl).false

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : Zero R
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace R
inst✝ : Zero X
f : X → R
g : C(X, R)₀
hf : f 0 ≠ 0
⊢ mkD f g = g

Tactic:
by
  simp only [mkD, not_and_of_not_right _ hf, ↓reduceDIte]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : Zero R
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace R
s : Set X
inst✝ : Zero ↑s
f : X → R
g : C(↑s, R)₀
hf : ¬ContinuousOn f s
⊢ mkD (s.domRestrict f) g = g

Tactic:
continuousOn_iff_continuous_domRestrict

Goal state after:
X : Type u_1
R : Type u_2
inst✝³ : Zero R
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace R
s : Set X
inst✝ : Zero ↑s
f : X → R
g : C(↑s, R)₀
hf : ¬Continuous[instTopologicalSpaceSubtype, inst✝¹] (s.domRestrict f)
⊢ mkD (s.domRestrict f) g = g
Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero

Goal state before:
pp: X✝ : Type u_1
R✝ : Type u_2
inst✝⁷ : Zero X✝
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : TopologicalSpace R✝
X : Type u_3
R : Type u_4
inst✝⁴ : Zero X
inst✝³ : TopologicalSpace X
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous fun a ↦ -a

Tactic:
by
    rw [continuous_induced_rng]
    exact continuous_neg.comp continuous_induced_dom

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: ε : Type u_3
inst✝³ : TopologicalSpace ε
inst✝² : ENormedAddMonoid ε
inst✝¹ : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f [[a, b]] μ

Tactic:
by
  rw [intervalIntegrable_iff, ← Icc_min_max, uIoc, integrableOn_Icc_iff_integrableOn_Ioc h]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:

Tactic:
∫ x, g x ∂μ.withDensity (fun x => f x) = ∫ x, g x ∂μ.withDensity fun x => f' x := by
      congr 1
      apply withDensity_congr_ae
      filter_upwards [hf.ae_eq_mk] with x hx
      rw [hx]
    _ = ∫ x, f' x • g x ∂μ := integral_withDensity_eq_integral_smul hf.measurable_mk _
    _ = ∫ x, f x • g x ∂μ := by
      apply integral_congr_ae
      filter_upwards [hf.ae_eq_mk] with x hx
      rw [hx]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
l : Filter ι
inst✝¹ : l.IsCountablyGenerated
F : ι → ℝ → E
inst✝ : IsLocallyFiniteMeasure μ
hF : ∀ᶠ (i : ι) in l, ContinuousOn (F i) [[a, b]]
h_lim : TendstoUniformlyOn F f l [[a, b]]
hl : l.NeBot
C : ℝ
hC : C ∈ upperBounds ((fun x ↦ ‖f x‖) '' [[a, b]])
⊢ ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → ‖F n x‖ ≤ C + 1

Tactic:
have := uniformContinuous_norm.comp_tendstoUniformlyOn h_lim
      |>.eventually_forall_le (show C < C + 1 by simp) (by simpa [upperBounds] using hC)
    exact this.mono fun i hi ↦ .of_forall fun x hx ↦ hi x <| uIoc_subset_uIcc hx

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
f : ℝ → F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
⊢ Measurable fun x ↦ derivWithin f (Ici x) x

Tactic:
by
  refine measurable_of_isClosed fun s hs => ?_
  have :
    (fun x => derivWithin f (Ici x) x) ⁻¹' s =
      { x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ s } ∪
        { x | ¬DifferentiableWithinAt ℝ f (Ici x) x } ∩ { _x | (0 : F) ∈ s } :=
    Set.ext fun x => mem_preimage.trans derivWithin_mem_iff
  rw [this]
  exact
    (measurableSet_of_differentiableWithinAt_Ici_of_isComplete _ hs.isComplete).union
      ((measurableSet_of_differentiableWithinAt_Ici _).compl.inter (MeasurableSet.const _))

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst✝² : CompleteSpace E
inst✝¹ : l'.IsMeasurablyGenerated
inst✝ : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
huv : v ≤ᶠ[lt] u
t : ι
⊢ -(∫ (x : ℝ) in v t..u t, f x ∂μ - μ.real (Ioc (v t) (u t)) • c) =
    ∫ (x : ℝ) in u t..v t, f x ∂μ + μ.real (Ioc (v t) (u t)) • c

Tactic:
simp [integral_symm (u t), add_comm]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable (fun x ↦ f (c + x)) volume (a - c) (b - c)

Tactic:
simpa [add_comm] using IntervalIntegrable.comp_add_right hf c h

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : TopologicalSpace X
μ : Measure ℝ
inst✝ : FirstCountableTopology X
F : X → ℝ → E
bound : ℝ → ℝ
a b a₀ b₀ : ℝ
x₀ : X
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x ↦ F x t) x₀
ha₀ : a₀ ∈ Ioo a b
hb₀ : b₀ ∈ Ioo a b
hμb₀ : μ {b₀} = 0
hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b
Ioo_nhds : Ioo a b ∈ 𝓝 b₀
Icc_nhds : Icc a b ∈ 𝓝 b₀
hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t
⊢ ∀ (x : X × ℝ),
    (∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x.1 t‖ ≤ bound t) ∧ a < x.2 ∧ x.2 < b →
      ∫ (s : ℝ) in a₀..x.2, F x.1 s ∂μ =
        ∫ (s : ℝ) in a₀..b₀, F x.1 s ∂μ + ∫ (s : ℝ) in b₀..x.2, F x₀ s ∂μ + ∫ (s : ℝ) in b₀..x.2, F x.1 s - F x₀ s ∂μ

Tactic:
rintro ⟨x, t⟩ ⟨hx : ∀ᵐ t : ℝ ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t, ht : t ∈ Ioo a b⟩

Goal state after:
E : Type u_1
X : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : TopologicalSpace X
μ : Measure ℝ
inst✝ : FirstCountableTopology X
F : X → ℝ → E
bound : ℝ → ℝ
a b a₀ b₀ : ℝ
x₀ : X
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x ↦ F x t) x₀
ha₀ : a₀ ∈ Ioo a b
hb₀ : b₀ ∈ Ioo a b
hμb₀ : μ {b₀} = 0
hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b
Ioo_nhds : Ioo a b ∈ 𝓝 b₀
Icc_nhds : Icc a b ∈ 𝓝 b₀
hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t
x : X
t : ℝ
hx : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
ht : t ∈ Ioo a b
⊢ ∫ (s : ℝ) in a₀..(x, t).2, F (x, t).1 s ∂μ =
    ∫ (s : ℝ) in a₀..b₀, F (x, t).1 s ∂μ + ∫ (s : ℝ) in b₀..(x, t).2, F x₀ s ∂μ +
      ∫ (s : ℝ) in b₀..(x, t).2, F (x, t).1 s - F x₀ s ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f : ℝ → E
μ : Measure ℝ
a b : ℝ
ha : IntegrableOn f (Iic a) μ
hb : IntegrableOn f (Iic b) μ
hab : a ≤ b
⊢ ∫ (x : ℝ) in Iic b, f x ∂μ - ∫ (x : ℝ) in Iic a, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
sub_eq_iff_eq_add',

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f : ℝ → E
μ : Measure ℝ
a b : ℝ
ha : IntegrableOn f (Iic a) μ
hb : IntegrableOn f (Iic b) μ
hab : a ≤ b
⊢ ∫ (x : ℝ) in Iic b, f x ∂μ = ∫ (x : ℝ) in Iic a, f x ∂μ + ∫ (x : ℝ) in a..b, f x ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Iio b) μ
hab : a ≤ b
ha : IntegrableOn f (Iio a) μ
h : IntegrableOn f (Ico a b) μ
⊢ ∫ (x : ℝ) in Iio b, f x ∂μ - ∫ (x : ℝ) in Iio a, f x ∂μ = ∫ (x : ℝ) in Ico a b, f x ∂μ

Tactic:
sub_eq_iff_eq_add',

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Iio b) μ
hab : a ≤ b
ha : IntegrableOn f (Iio a) μ
h : IntegrableOn f (Ico a b) μ
⊢ ∫ (x : ℝ) in Iio b, f x ∂μ = ∫ (x : ℝ) in Iio a, f x ∂μ + ∫ (x : ℝ) in Ico a b, f x ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Ici a) μ
hab : a ≤ b
ha : IntegrableOn f (Ici b) μ
h : IntegrableOn f (Ico a b) μ
⊢ ∫ (x : ℝ) in Ici a, f x ∂μ - ∫ (x : ℝ) in Ici b, f x ∂μ = ∫ (x : ℝ) in Ico a b, f x ∂μ

Tactic:
sub_eq_iff_eq_add',

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Ici a) μ
hab : a ≤ b
ha : IntegrableOn f (Ici b) μ
h : IntegrableOn f (Ico a b) μ
⊢ ∫ (x : ℝ) in Ici a, f x ∂μ = ∫ (x : ℝ) in Ici b, f x ∂μ + ∫ (x : ℝ) in Ico a b, f x ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᵐ[μ.restrict (Ioc a b)] g
hlt : (μ.restrict (Ioc a b)) {x | f x < g x} ≠ 0
⊢ 0 < (μ.restrict (Ioc a b)) (support fun x ↦ g x - f x)

Tactic:
refine pos_iff_ne_zero.2 (mt (measure_mono_null ?_) hlt)

Goal state after:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᵐ[μ.restrict (Ioc a b)] g
hlt : (μ.restrict (Ioc a b)) {x | f x < g x} ≠ 0
⊢ {x | f x < g x} ⊆ support fun x ↦ g x - f x
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : FloorRing α
inst✝ : IsStrictOrderedRing α
b : ℤ
⊢ ⌈↑(b - 1)⌉ ≤ b

Tactic:
ceil_intCast

Goal state after:
α : Type u_1
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : FloorRing α
inst✝ : IsStrictOrderedRing α
b : ℤ
⊢ b - 1 ≤ b
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
a : ℝ
h : Measurable ⇑(measurableEquivIoc T a)
s : Set ↑(Ioc a (a + T))
hs : MeasurableSet s
x : ℝ
⊢ (equivIoc T a) ↑x ∈ s ∧ x ∈ Ioc a (a + T) ↔ ∃ (x_1 : x ∈ Ioc a (a + T)), ⟨x, ⋯⟩ ∈ s

Tactic:
and_comm,

Goal state after:
T : ℝ
hT : Fact (0 < T)
a : ℝ
h : Measurable ⇑(measurableEquivIoc T a)
s : Set ↑(Ioc a (a + T))
hs : MeasurableSet s
x : ℝ
⊢ x ∈ Ioc a (a + T) ∧ (equivIoc T a) ↑x ∈ s ↔ ∃ (x_1 : x ∈ Ioc a (a + T)), ⟨x, ⋯⟩ ∈ s
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
h₀ : R = 0
⊢ CircleIntegrable f c R ↔ IntervalIntegrable (fun θ ↦ deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)

Tactic:
simp +unfoldPartialApp [h₀, const]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst✝ : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : TendstoUniformlyOn f g l (sphere c R)
⊢ Tendsto (fun n ↦ ∮ (z : ℂ) in C(c, R), f n z) l (𝓝 (∮ (z : ℂ) in C(c, R), g z))

Tactic:
apply TendstoUniformlyOn.tendsto_intervalIntegral_of_continuousOn

Goal state after:
case hF
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst✝ : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : TendstoUniformlyOn f g l (sphere c R)
⊢ ∀ᶠ (i : ι) in l, ContinuousOn (fun x ↦ deriv (circleMap c R) x • (fun z ↦ f i z) (circleMap c R x)) [[0, 2 * π]]

case h_lim
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst✝ : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : TendstoUniformlyOn f g l (sphere c R)
⊢ TendstoUniformlyOn (fun n x ↦ deriv (circleMap c R) x • (fun z ↦ f n z) (circleMap c R x))
    (fun x ↦ deriv (circleMap c R) x • (fun z ↦ g z) (circleMap c R x)) l [[0, 2 * π]]
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c w : ℂ
R : ℝ
hR : R ≠ 0
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z = ∮ (z : ℂ) in C(c, R), f z

Tactic:
have : (circleMap c R ⁻¹' {w}).Countable := (countable_singleton _).preimage_circleMap c hR

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c w : ℂ
R : ℝ
hR : R ≠ 0
this : (circleMap c R ⁻¹' {w}).Countable
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z = ∮ (z : ℂ) in C(c, R), f z
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
g : ↥(Lp E 1 (μ.prod ν))
⊢ (fun i ↦ ∫⁻ (x : α), ‖∫ (y : β), ↑↑i (x, y) - ↑↑g (x, y) ∂ν‖ₑ ∂μ) ≤ fun i ↦
    ∫⁻ (x : α), ∫⁻ (y : β), ‖↑↑i (x, y) - ↑↑g (x, y)‖ₑ ∂ν ∂μ

pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
g : ↥(Lp E 1 (μ.prod ν))
⊢ Tendsto (fun i ↦ ∫⁻ (x : α), ∫⁻ (y : β), ‖↑↑i (x, y) - ↑↑g (x, y)‖ₑ ∂ν ∂μ) (𝓝 g) (𝓝 0)

Tactic:
· exact fun i => lintegral_mono fun x => enorm_integral_le_lintegral_enorm _

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
g : ↥(Lp E 1 (μ.prod ν))
⊢ Tendsto (fun i ↦ ∫⁻ (x : α), ∫⁻ (y : β), ‖↑↑i (x, y) - ↑↑g (x, y)‖ₑ ∂ν ∂μ) (𝓝 g) (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this✝ : Fact (μ U < ∞)
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (ν V < ∞)
⊢ ∫ (y : Y), ∫ (x : X) in U, f x y ∂μ ∂ν = ∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν

Tactic:
by
    congr 1 with y
    apply setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)
    contrapose! hx
    have : (x, y) ∈ Function.support f.uncurry := hx
    exact mem_image_of_mem _ (subset_tsupport _ this)

Goal state after: