mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.ContDiff.Comp

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
y : F
x : E
hg : ContDiffWithinAt 𝕜 n g t y
hf : ContDiffWithinAt 𝕜 n f s x
hy : f x = y
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) (s ∩ f ⁻¹' t) x

Tactic:
by
  subst hy; exact hg.comp_inter x hf

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Comp

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ∞ω
c : E → F →L[𝕜] G
hc : ContDiff 𝕜 n c
i : ℕ
hi : ↑i ≤ n
x : E
u : F
m : Fin i → E
⊢ (iteratedFDeriv 𝕜 i (fun y ↦ (c y) u) x) m = ((iteratedFDeriv 𝕜 i c x) m) u

Tactic:
by
  simp only [← iteratedFDerivWithin_univ]
  exact iteratedFDerivWithin_clm_apply_const_apply uniqueDiffOn_univ hc.contDiffOn hi (mem_univ _)

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage

Goal state before:
pp: case left
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ (e.restr e'.source).source = (e'.restr e.source).source

Tactic:
rw [e'.restr_source' _ e.open_source]

Goal state after:
case left
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ (e.restr e'.source).source = e'.source ∩ e.source
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ c : OrderedFinpartition n
m : Fin c.length
⊢ (if h : m = m then
        have this := ⋯;
        (fun i ↦ cases 0 (succ ∘ c.emb m) i) ∘ Fin.cast this
      else
        have this := ⋯;
        succ ∘ c.emb m ∘ Fin.cast this)
      ⟨update c.partSize m (c.partSize m + 1) m - 1, ⋯⟩ =
    (succ ∘ fun m ↦ c.emb m ⟨c.partSize m - 1, ⋯⟩) m

Tactic:
simp only [↓reduceDIte, update_self, add_tsub_cancel_right, comp_apply, cast_mk]

Goal state after:
case inl
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ c : OrderedFinpartition n
m : Fin c.length
⊢ cases 0 (succ ∘ c.emb m) ⟨c.partSize m, ⋯⟩ = (c.emb m ⟨c.partSize m - 1, ⋯⟩).succ
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) = {0}
x : Fin n
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
A : c.length = c.length - 1 + 1
h : i = 0
⊢ c.emb i j ∈ range (c.emb i)

Tactic:
apply mem_range_self

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
⊢ 0 < update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0)

pp: case inr
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
i : Fin c.length
hi : i ≠ c.index 0
⊢ 0 < update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i

Tactic:
· simpa using c.one_lt_partSize_index_zero hc

Goal state after:
case inr
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
i : Fin c.length
hi : i ≠ c.index 0
⊢ 0 < update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case pos.partSize.zero
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition (n + 1)
h : range (c.emb 0) = {0}
A : c.length - 1 + 1 = c.length
⊢ { length := c.length - 1 + 1, partSize := cons 1 fun i ↦ c.partSize (Fin.cast ⋯ i.succ), partSize_pos := ⋯,
          emb := fun i ↦
            cases (motive := fun x ↦ Fin (cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) x) → Fin (n + 1)) (fun x ↦ 0)
              (fun m ↦ succ ∘ fun j ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯) i,
          emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ }.partSize
      0 =
    c.partSize ⟨↑0, ⋯⟩

Tactic:
change 1 = c.partSize 0; simp [c.partSize_eq_one_of_range_emb_eq_singleton h]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁸ : NontriviallyNormedField 𝕂
inst✝⁷ : NormedRing 𝔸
inst✝⁶ : NormedRing 𝔹
inst✝⁵ : NormedAlgebra 𝕂 𝔸
inst✝⁴ : CompleteSpace 𝔸
inst✝³ : Algebra 𝕂 𝔹
inst✝² : CharZero 𝕂
F : Type u_4
inst✝¹ : FunLike F 𝔸 𝔹
inst✝ : RingHomClass F 𝔸 𝔹
f : F
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑f
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ f (exp x) = exp (f x)

Tactic:
by
  rw [exp_eq_tsum 𝕂, exp_eq_tsum 𝕂]
  refine ((expSeries_summable_of_mem_ball' _ hx).hasSum.map f hf).tsum_eq.symm.trans ?_
  dsimp only [Function.comp_def]
  simp_rw [map_inv_natCast_smul f 𝕂 𝕂, map_pow]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (c.emb 0) = {0}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
j : Fin (c.partSize (c.index 0))
hj : j ≠ 0
⊢ Fin.cast ⋯ j ≠ 0

Tactic:
simpa using hj

Goal state after:
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
ι : Type u
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
hd : Tendsto (fun n ↦ a + d n) l (𝓝[s] (a + 0))
⊢ ∀ᶠ (n : ι) in l, c n • (f (a + d n) - f a) ≤ 0

Tactic:
rw [add_zero] at hd

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
ι : Type u
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
hd : Tendsto (fun n ↦ a + d n) l (𝓝[s] a)
⊢ ∀ᶠ (n : ι) in l, c n • (f (a + d n) - f a) ≤ 0
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n m : ℕ
h : n < m
⊢ iteratedDeriv n (fun x ↦ x ^ m) 0 = ↑(if n = m then m.factorial else 0)

Tactic:
simp_all [Nat.descFactorial_self, Nat.descFactorial_eq_zero_iff_lt.mpr, ne_of_lt, ne_of_gt]

Goal state after:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n m : ℕ
h : n = m
⊢ iteratedDeriv n (fun x ↦ x ^ m) 0 = ↑(if n = m then m.factorial else 0)

Tactic:
simp_all [Nat.descFactorial_self, Nat.descFactorial_eq_zero_iff_lt.mpr, ne_of_lt, ne_of_gt]

Goal state after:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case inr.inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n m : ℕ
h : m < n
⊢ iteratedDeriv n (fun x ↦ x ^ m) 0 = ↑(if n = m then m.factorial else 0)

Tactic:
simp_all [Nat.descFactorial_self, Nat.descFactorial_eq_zero_iff_lt.mpr, ne_of_lt, ne_of_gt]

Goal state after:
Module: Mathlib.Topology.Order.Rolle

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : f c = f a
hC : ¬f C = f a
h : C = b
⊢ f C = f a

Tactic:
by rw [h, hfI]

Goal state after:
Module: Mathlib.Topology.Order.Rolle

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : ¬f c = f a
h : c = b
⊢ f c = f a

Tactic:
by rw [h, hfI]

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
fint : Integrable (fun x ↦ ↑(f x)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), ↑(f a) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ↑δ
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ (∫⁻ (a : α), ↑(f a) ∂μ + ↑δ).toReal = (∫⁻ (a : α), ↑(f a) ∂μ).toReal + ↑δ

Tactic:
ENNReal.toReal_add int_f_ne_top ENNReal.coe_ne_top,

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (fun x ↦ ↑(f x)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), ↑(f a) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ↑δ
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ (∫⁻ (a : α), ↑(f a) ∂μ).toReal + (↑δ).toReal = (∫⁻ (a : α), ↑(f a) ∂μ).toReal + ↑δ
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: case refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
g : ↥⊤ →ₗ[ℝ] ℝ
hfg : ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥{ domain := ⊤, toFun := g }.domain⦄, ↑x = ↑y → ↑f x = ↑{ domain := ⊤, toFun := g } y
hgs : ∀ (x : ↥{ domain := ⊤, toFun := g }.domain), ↑x ∈ s → 0 ≤ ↑{ domain := ⊤, toFun := g } x
⊢ ∀ x ∈ s, 0 ≤ (g ∘ₗ LinearMap.codRestrict ⊤ LinearMap.id ⋯) x

Tactic:
exact fun x hx => hgs ⟨x, _⟩ hx

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

Goal state before:
pp: E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ s - t
⊢ b₀ - a₀ + (a₀ - b₀) = 0

Tactic:
sub_add_sub_cancel',

Goal state after:
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ s - t
⊢ a₀ - a₀ = 0
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case e'_2
X : Type u_1
E : Type u_3
F : Type u_4
inst✝¹¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : RCLike 𝕜'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst✝³ : RingHomIsometric σ
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), σ (r • x) = r • σ x
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
f g : X → E
hfg : f =ᵐ[μ] g
a✝ : Integrable f μ
hf : ∫ (x : X), L (f x) ∂μ = L (∫ (x : X), f x ∂μ)
⊢ ∫ (x : X), L (g x) ∂μ = ∫ (x : X), L (f x) ∂μ

Tactic:
clear hf

Goal state after:
case e'_2
X : Type u_1
E : Type u_3
F : Type u_4
inst✝¹¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : RCLike 𝕜'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst✝³ : RingHomIsometric σ
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), σ (r • x) = r • σ x
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
f g : X → E
hfg : f =ᵐ[μ] g
a✝ : Integrable f μ
⊢ ∫ (x : X), L (g x) ∂μ = ∫ (x : X), L (f x) ∂μ
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case e'_3
X : Type u_1
E : Type u_3
F : Type u_4
inst✝¹¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : RCLike 𝕜'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst✝³ : RingHomIsometric σ
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), σ (r • x) = r • σ x
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
f g : X → E
hfg : f =ᵐ[μ] g
a✝ : Integrable f μ
hf : ∫ (x : X), L (f x) ∂μ = L (∫ (x : X), f x ∂μ)
⊢ L (∫ (x : X), g x ∂μ) = L (∫ (x : X), f x ∂μ)

Tactic:
clear hf

Goal state after:
case e'_3
X : Type u_1
E : Type u_3
F : Type u_4
inst✝¹¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : RCLike 𝕜'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst✝³ : RingHomIsometric σ
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), σ (r • x) = r • σ x
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
f g : X → E
hfg : f =ᵐ[μ] g
a✝ : Integrable f μ
⊢ L (∫ (x : X), g x ∂μ) = L (∫ (x : X), f x ∂μ)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case pos
ε : Type u_3
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
h : IntervalIntegrable f μ a b
hab : a ≤ b
⊢ AEStronglyMeasurable f (μ.restrict (Ι a b))

Tactic:
rw [uIoc_of_le hab]; exact h.aestronglyMeasurable

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
K : Set F
hK : IsComplete K
⊢ MeasurableSet {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}

Tactic:
simp only [differentiable_set_eq_D K hK, D]

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
⊢ MeasurableSet (⋂ e, ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e))
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

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

Tactic:
by
  simp_rw [add_comm c]
  rw [IntervalIntegrable.comp_add_right_iff (by grind)]
  simp

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

Goal state before:
pp: E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
ca cb : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) volume
ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 cb)
this :
  (fun t ↦
      ((∫ (x : ℝ) in t.1.1..t.1.2, f x) - ∫ (x : ℝ) in t.2.1..t.2.2, f x) -
        ((t.1.2 - t.2.2) • cb - (t.1.1 - t.2.1) • ca)) =o[𝓝 ((a, b), a, b)]
    fun t ↦ ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖
⊢ HasStrictFDerivAt (fun p ↦ ∫ (x : ℝ) in p.1..p.2, f x) ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (a, b)

Tactic:
refine .of_isLittleO <| (this.congr_left ?_).trans_isBigO ?_

Goal state after:
case refine_1
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
ca cb : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) volume
ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 cb)
this :
  (fun t ↦
      ((∫ (x : ℝ) in t.1.1..t.1.2, f x) - ∫ (x : ℝ) in t.2.1..t.2.2, f x) -
        ((t.1.2 - t.2.2) • cb - (t.1.1 - t.2.1) • ca)) =o[𝓝 ((a, b), a, b)]
    fun t ↦ ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖
⊢ ∀ (x : (ℝ × ℝ) × ℝ × ℝ),
    ((∫ (x : ℝ) in x.1.1..x.1.2, f x) - ∫ (x : ℝ) in x.2.1..x.2.2, f x) -
        ((x.1.2 - x.2.2) • cb - (x.1.1 - x.2.1) • ca) =
      ((∫ (x : ℝ) in x.1.1..x.1.2, f x) - ∫ (x : ℝ) in x.2.1..x.2.2, f x) -
        ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (x.1 - x.2)

case refine_2
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
ca cb : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) volume
ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 cb)
this :
  (fun t ↦
      ((∫ (x : ℝ) in t.1.1..t.1.2, f x) - ∫ (x : ℝ) in t.2.1..t.2.2, f x) -
        ((t.1.2 - t.2.2) • cb - (t.1.1 - t.2.1) • ca)) =o[𝓝 ((a, b), a, b)]
    fun t ↦ ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖
⊢ (fun t ↦ ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖) =O[𝓝 ((a, b), a, b)] fun p ↦ p.1 - p.2
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : ℝ → E
ca cb : E
la lb : Filter ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst✝¹ : FTCFilter a (𝓝[s] a) la
inst✝ : FTCFilter b (𝓝[t] b) lb
hmeas_a : StronglyMeasurableAtFilter f la volume
hmeas_b : StronglyMeasurableAtFilter f lb volume
ha : Tendsto f (la ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (lb ⊓ ae volume) (𝓝 cb)
this :
  (fun t ↦
      ((∫ (x : ℝ) in t.1..t.2, f x) - ∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca)) =o[𝓝[s ×ˢ t] (a, b)]
    fun t ↦ ‖t.1 - a‖ + ‖t.2 - b‖
⊢ HasFDerivWithinAt (fun p ↦ ∫ (x : ℝ) in p.1..p.2, f x) ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (s ×ˢ t)
    (a, b)

Tactic:
refine .of_isLittleO <| (this.congr_left ?_).trans_isBigO ?_

Goal state after:
case refine_1
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : ℝ → E
ca cb : E
la lb : Filter ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst✝¹ : FTCFilter a (𝓝[s] a) la
inst✝ : FTCFilter b (𝓝[t] b) lb
hmeas_a : StronglyMeasurableAtFilter f la volume
hmeas_b : StronglyMeasurableAtFilter f lb volume
ha : Tendsto f (la ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (lb ⊓ ae volume) (𝓝 cb)
this :
  (fun t ↦
      ((∫ (x : ℝ) in t.1..t.2, f x) - ∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca)) =o[𝓝[s ×ˢ t] (a, b)]
    fun t ↦ ‖t.1 - a‖ + ‖t.2 - b‖
⊢ ∀ (x : ℝ × ℝ),
    ((∫ (x : ℝ) in x.1..x.2, f x) - ∫ (x : ℝ) in a..b, f x) - ((x.2 - b) • cb - (x.1 - a) • ca) =
      ((∫ (x : ℝ) in x.1..x.2, f x) - ∫ (x : ℝ) in (a, b).1..(a, b).2, f x) -
        ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (x - (a, b))

case refine_2
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : ℝ → E
ca cb : E
la lb : Filter ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst✝¹ : FTCFilter a (𝓝[s] a) la
inst✝ : FTCFilter b (𝓝[t] b) lb
hmeas_a : StronglyMeasurableAtFilter f la volume
hmeas_b : StronglyMeasurableAtFilter f lb volume
ha : Tendsto f (la ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (lb ⊓ ae volume) (𝓝 cb)
this :
  (fun t ↦
      ((∫ (x : ℝ) in t.1..t.2, f x) - ∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca)) =o[𝓝[s ×ˢ t] (a, b)]
    fun t ↦ ‖t.1 - a‖ + ‖t.2 - b‖
⊢ (fun t ↦ ‖t.1 - a‖ + ‖t.2 - b‖) =O[𝓝[s ×ˢ t] (a, b)] fun x' ↦ x' - (a, b)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
inst✝³ : NormedDivisionRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : NormSMulClass 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
r : 𝕜
f : ℝ → E
⊢ ∫ (x : ℝ) in a..b, r • f x ∂μ = r • ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
by
  simp only [intervalIntegral, integral_smul, smul_sub]

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

Goal state before:
pp: case pos
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
hc : c = 0
⊢ c • ∫ (x : ℝ) in a..b, f (d - c * x) = ∫ (x : ℝ) in d - c * b..d - c * a, f x

Tactic:
simp [hc, integral_comp_sub_mul]

Goal state after: