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
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
hf : ContDiffAt 𝕜 n (uncurry f) (x₀, g x₀)
hg : ContDiffAt 𝕜 m g x₀
hmn : m + 1 ≤ n
⊢ ContDiffAt 𝕜 m (fun x ↦ fderiv 𝕜 (f x) (g x)) x₀

Tactic:
← fderivWithin_univ

Goal state after:
𝕜 : 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
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
hf : ContDiffAt 𝕜 n (uncurry f) (x₀, g x₀)
hg : ContDiffAt 𝕜 m g x₀
hmn : m + 1 ≤ n
⊢ ContDiffAt 𝕜 m (fun x ↦ fderivWithin 𝕜 (f x) univ (g x)) x₀
Module: Mathlib.Analysis.Calculus.ContDiff.Comp

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x₀ : E
m n : ℕ∞ω
i : ℕ
hf : ContDiffAt 𝕜 n f x₀
hmn : m + ↑i ≤ n
⊢ ContDiffAt 𝕜 m (iteratedFDeriv 𝕜 i f) x₀

Tactic:
by
  rw [← iteratedFDerivWithin_univ, ← contDiffWithinAt_univ] at *
  exact hf.iteratedFDerivWithin_right uniqueDiffOn_univ hmn trivial

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ∞
h : ∀ (m : ℕ), ↑m ≤ n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s
⊢ ContDiffOn 𝕜 (↑n) f s

Tactic:
by
  apply contDiffOn_of_differentiableOn
  simpa only [iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_differentiableOn_iff]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ∞ω
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : ↑m < n
hs : UniqueDiffOn 𝕜 s
x : 𝕜
hx : x ∈ s
⊢ UniqueDiffOn 𝕜 (insert x s)

Tactic:
by rwa [insert_eq_of_mem hx]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
c : F
s : Set 𝕜
x : 𝕜
⊢ iteratedDerivWithin n (fun x ↦ c) s x = if n = 0 then c else 0

Tactic:
by
  induction n generalizing c with
  | zero => simp
  | succ n h => simp [iteratedDerivWithin_succ', Pi.zero_def, h]

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
H : ContinuousOn f s
x : E
hx : x ∈ s
m : ℕ
hm : ↑m ≤ 0
this : ↑m = 0
⊢ ContinuousOn f (insert x s)

Tactic:
by rwa [insert_eq_of_mem hx]

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

Goal state before:
pp: case neg.emb.refine_2.inl.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✝
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
⊢ c.emb (c.index 0) j = cases 0 (succ ∘ fun j ↦ (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯) (Fin.cast ⋯ ⟨↑j, ⋯⟩)

Tactic:
let j' := Fin.pred (j.cast B.symm) (by simpa using hj)
              have : j = (succ j').cast B := by simp [j']
              simp only [this, val_cast, val_succ, cast_mk, cases_succ', comp_apply, succ_mk,
                succ_pred]
              rfl

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

Goal state before:
pp: case mp
s : Set ℝ
a : ℝ
h : 1 ∈ posTangentConeAt s a
ι : Type
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → ℝ
hd₀ : Tendsto d l (𝓝 0)
hd : ∀ᶠ (n : ι) in l, a + d n ∈ s
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 1)
this : Tendsto (fun x ↦ a + d x) l (𝓝 a)
⊢ a ∈ closure (Ioi a ∩ s)

Tactic:
apply mem_closure_of_tendsto this

Goal state after:
case mp
s : Set ℝ
a : ℝ
h : 1 ∈ posTangentConeAt s a
ι : Type
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → ℝ
hd₀ : Tendsto d l (𝓝 0)
hd : ∀ᶠ (n : ι) in l, a + d n ∈ s
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 1)
this : Tendsto (fun x ↦ a + d x) l (𝓝 a)
⊢ ∀ᶠ (x : ι) in l, a + d x ∈ Ioi a ∩ s
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
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

Tactic:
have ne : (Icc a b).Nonempty := nonempty_Icc.2 (le_of_lt hab)

Goal state after:
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 ∈ Ioo a b, IsExtrOn f (Icc a b) c
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
hcont_Ioc : ∀ z ∈ Ioc a b, ContinuousWithinAt f (Icc a b) z
hcont : ContinuousOn f (Icc a b)
⊢ False

Tactic:
obtain ⟨x, hx₁, hx₂⟩ :=
        exists_deriv_eq_slope' f hab hcont (hdiff'.mono (Ioo_subset_Ioc_self))

Goal state after:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
hcont_Ioc : ∀ z ∈ Ioc a b, ContinuousWithinAt f (Icc a b) z
hcont : ContinuousOn f (Icc a b)
x : ℝ
hx₁ : x ∈ Ioo a b
hx₂ : deriv f x = slope f a b
⊢ False
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

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
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
⊢ ∃ R > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ε

Tactic:
let δ := (ε / 2) / 2

Goal state after:
𝕜 : 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
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
⊢ ∃ R > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ε
Module: Mathlib.Geometry.Convex.Cone.Pointed

Goal state before:
pp: case mp
R : Type u_1
E : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
x : E
s : Set E
⊢ (∃ c, ↑c.support ⊆ s ∧ (c.sum fun mi r ↦ r • mi) = x) →
    ∃ c, ↑c.support ⊆ s ∧ (∀ (y : E), 0 ≤ c y) ∧ (c.sum fun m r ↦ r • m) = x

Tactic:
rintro ⟨c, hc, rfl⟩
    exact ⟨⟨c.support, Subtype.val ∘ c, by simp [← Subtype.val_inj]⟩, hc, fun y ↦ (c y).2, rfl⟩

Goal state after:
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
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
xn : ↥f.domain
hxn : xn ∈ {x | -↑x - y ∈ s}
xp : ↥f.domain
hxp : xp ∈ {x | ↑x + y ∈ s}
this : 0 ≤ ↑f (xp - xn)
⊢ ↑f xn ≤ ↑f xp

Tactic:
f.map_sub,

Goal state after:
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
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
xn : ↥f.domain
hxn : xn ∈ {x | -↑x - y ∈ s}
xp : ↥f.domain
hxp : xp ∈ {x | ↑x + y ∈ s}
this : 0 ≤ ↑f xp - ↑f xn
⊢ ↑f xn ≤ ↑f xp
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)₀
x : X
hf : Continuous[inst✝², inst✝¹] f
hf₀ : f 0 = 0
⊢ (mkD f g) x = f x

Tactic:
mkD_of_continuous hf hf₀,

Goal state after:
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)₀
x : X
hf : Continuous[inst✝², inst✝¹] f
hf₀ : f 0 = 0
⊢ { toFun := f, continuous_toFun := hf, map_zero' := hf₀ } x = f x
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ι : Type u_3
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → ℝ → E
bound : ℝ → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → ‖F n x‖ ≤ bound x
bound_integrable : IntervalIntegrable bound μ a b
h_lim : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → Tendsto (fun n ↦ F n x) l (𝓝 (f x))
⊢ Tendsto (fun n ↦ ∫ (x : ℝ) in a..b, F n x ∂μ) l (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))

Tactic:
simp only [intervalIntegrable_iff, intervalIntegral_eq_integral_uIoc,
    ← ae_restrict_iff' (α := ℝ) (μ := μ) measurableSet_uIoc] at *
  exact tendsto_const_nhds.smul <|
    tendsto_integral_filter_of_dominated_convergence bound hF_meas h_bound bound_integrable h_lim

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

Goal state before:
pp: case inr.inr
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : 0 < t
⊢ IntervalIntegrable f volume 0 t

Tactic:
exact h₂f t h

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

Goal state before:
pp: case inr.inr
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : 0 < t
⊢ IntervalIntegrable f volume 0 t

Tactic:
exact h₂f t h

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
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)
⊢ HasFDerivWithinAt (fun p ↦ ∫ (x : ℝ) in p.1..p.2, f x) ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (s ×ˢ t)
    (a, b)

Tactic:
by
  have :=
    integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae hf hmeas_a hmeas_b ha hb
      (tendsto_const_pure.mono_right FTCFilter.pure_le : Tendsto _ _ (𝓝[s] a)) tendsto_fst
      (tendsto_const_pure.mono_right FTCFilter.pure_le : Tendsto _ _ (𝓝[t] b)) tendsto_snd
  rw [← nhdsWithin_prod_eq] at this
  refine .of_isLittleO <| (this.congr_left ?_).trans_isBigO ?_
  · simp [sub_smul]
  · exact isBigO_fst_prod.norm_left.add isBigO_snd_prod.norm_left

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✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
A : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, δ ∈ Ioo 0 1
I : Tendsto (fun δ ↦ b₀ - δ) (𝓝 0) (𝓝 b₀)
J : Tendsto (fun δ ↦ b₀ + δ) (𝓝 0) (𝓝 b₀)
δ : ℝ
hδ : a < b₀ - δ
⊢ b₀ + δ < b → Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b

Tactic:
h'δ

Goal state after:
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
A : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, δ ∈ Ioo 0 1
I : Tendsto (fun δ ↦ b₀ - δ) (𝓝 0) (𝓝 b₀)
J : Tendsto (fun δ ↦ b₀ + δ) (𝓝 0) (𝓝 b₀)
δ : ℝ
hδ : a < b₀ - δ
h'δ : b₀ + δ < b
⊢ Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
hint : ∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))
⊢ ∑ k ∈ Finset.Ico m n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a n, f x ∂μ

Tactic:
by
  revert hint
  refine Nat.le_induction ?_ ?_ n hmn
  · simp
  · intro p hmp IH h
    rw [Finset.sum_Ico_succ_top hmp, IH, integral_add_adjacent_intervals]
    · refine IntervalIntegrable.trans_iterate_Ico hmp fun k hk => h k ?_
      exact (Ico_subset_Ico le_rfl (Nat.le_succ _)) hk
    · apply h
      simp [hmp]
    · intro k hk
      exact h _ (Ico_subset_Ico_right p.le_succ hk)

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

Goal state before:
pp: case inr
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f f' : ℝ → E
hint : IntervalIntegrable f' volume a b
hab : b ≤ a
hcont : ContinuousOn f (Icc b a)
hderiv : ∀ x ∈ Ioo b a, HasDerivWithinAt f (f' x) (Ioi x) x
⊢ -∫ (x : ℝ) in b..a, f' x = f b - f a

Tactic:
integral_eq_sub_of_hasDeriv_right_of_le hab hcont hderiv hint.symm,

Goal state after:
case inr
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f f' : ℝ → E
hint : IntervalIntegrable f' volume a b
hab : b ≤ a
hcont : ContinuousOn f (Icc b a)
hderiv : ∀ x ∈ Ioo b a, HasDerivWithinAt f (f' x) (Ioi x) x
⊢ -(f a - f b) = f b - f a
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case inr
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
hab : b ≤ a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ

Tactic:
rw [Ioc_eq_empty hab.not_gt, subset_empty_iff, support_eq_empty_iff] at h

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

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : 0 ≤ᵐ[μ.restrict (Ioc a b)] f
hfi : IntervalIntegrable f μ a b
⊢ ∫ (x : ℝ) in Ioc a b, f x ∂μ = 0 ↔ f =ᵐ[μ.restrict (Ioc a b)] 0

Tactic:
integral_eq_zero_iff_of_nonneg_ae hf hfi.1

Goal state after:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : 0 ≤ᵐ[μ.restrict (Ioc a b)] f
hfi : IntervalIntegrable f μ a b
⊢ f =ᵐ[μ.restrict (Ioc a b)] 0 ↔ f =ᵐ[μ.restrict (Ioc a b)] 0
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case h
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NullSingletonClass μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ ∀ x ∈ Ioo a b, f x ≤ g x

Tactic:
· exact h

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a ∈ Ici a₀
x : ℝ
⊢ (Ioi a).indicator (fun a ↦ ‖f a‖) x ≤ (Ioi a₀).indicator (norm ∘ f) x

Tactic:
apply indicator_le_indicator_of_subset (Ioi_subset_Ioi (by grind)) (fun a ↦ norm_nonneg (f a))

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

Goal state before:
pp: case h_bound
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ ∀ᶠ (n : ℝ) in 𝓝[≥] a₀, ∀ᵐ (a : ℝ) ∂μ, ‖(Ioi n).indicator f a‖ ≤ (Ioi a₀).indicator (norm ∘ f) a

pp: case bound_integrable
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ Integrable ((Ioi a₀).indicator (norm ∘ f)) μ

pp: case h_lim
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ ∀ᵐ (a : ℝ) ∂μ, Tendsto (fun n ↦ (Ioi n).indicator f a) (𝓝[≥] a₀) (𝓝 ((Ioi a₀).indicator f a))

Tactic:
· filter_upwards [self_mem_nhdsWithin] with a ha
    refine ae_of_all _ fun x ↦ ?_
    rw [norm_indicator_eq_indicator_norm]
    apply indicator_le_indicator_of_subset (Ioi_subset_Ioi (by grind)) (fun a ↦ norm_nonneg (f a))

Goal state after:
case bound_integrable
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ Integrable ((Ioi a₀).indicator (norm ∘ f)) μ

case h_lim
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ ∀ᵐ (a : ℝ) ∂μ, Tendsto (fun n ↦ (Ioi n).indicator f a) (𝓝[≥] a₀) (𝓝 ((Ioi a₀).indicator f a))
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: E : Type u_5
F : Type u_6
G : Type u_7
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
mF : MeasurableSpace F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
μ : Measure E
inst✝² : IsProbabilityMeasure μ
ν : Measure F
inst✝¹ : IsProbabilityMeasure ν
L : E × F →L[ℝ] G
inst✝ : CompleteSpace G
hLμ : Integrable (fun x ↦ (L ∘SL ContinuousLinearMap.inl ℝ E F) x.1) (μ.prod ν)
hLν : Integrable (fun x ↦ (L ∘SL ContinuousLinearMap.inr ℝ E F) x.2) (μ.prod ν)
⊢ ∫ (p : E × F), (L ∘SL ContinuousLinearMap.inl ℝ E F) p.1 + (L ∘SL ContinuousLinearMap.inr ℝ E F) p.2 ∂μ.prod ν =
    ∫ (x : E), (L ∘SL ContinuousLinearMap.inl ℝ E F) x ∂μ + ∫ (y : F), (L ∘SL ContinuousLinearMap.inr ℝ E F) y ∂ν

Tactic:
integral_add hLμ hLν,

Goal state after:
E : Type u_5
F : Type u_6
G : Type u_7
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
mF : MeasurableSpace F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
μ : Measure E
inst✝² : IsProbabilityMeasure μ
ν : Measure F
inst✝¹ : IsProbabilityMeasure ν
L : E × F →L[ℝ] G
inst✝ : CompleteSpace G
hLμ : Integrable (fun x ↦ (L ∘SL ContinuousLinearMap.inl ℝ E F) x.1) (μ.prod ν)
hLν : Integrable (fun x ↦ (L ∘SL ContinuousLinearMap.inr ℝ E F) x.2) (μ.prod ν)
⊢ ∫ (a : E × F), (L ∘SL ContinuousLinearMap.inl ℝ E F) a.1 ∂μ.prod ν +
      ∫ (a : E × F), (L ∘SL ContinuousLinearMap.inr ℝ E F) a.2 ∂μ.prod ν =
    ∫ (x : E), (L ∘SL ContinuousLinearMap.inl ℝ E F) x ∂μ + ∫ (y : F), (L ∘SL ContinuousLinearMap.inr ℝ E F) y ∂ν
Module: Mathlib.Analysis.Complex.Liouville

Goal state before:
pp: F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ z ∈ sphere c R, ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
this : 2 * ↑π * I / ↑n.factorial ≠ 0
⊢ (2 * ↑π * I / ↑n.factorial)⁻¹ • (2 * ↑π * I / ↑n.factorial) • iteratedDeriv n f c =
    n.factorial • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z

Tactic:
inv_div,

Goal state after:
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ z ∈ sphere c R, ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
this : 2 * ↑π * I / ↑n.factorial ≠ 0
⊢ (↑n.factorial / (2 * ↑π * I)) • (2 * ↑π * I / ↑n.factorial) • iteratedDeriv n f c =
    n.factorial • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (map (algebraMap F E) p).Splits
ϕ : Gal(E/F)
x : ↑(p.rootSet E)
⊢ ↑((restrict p E) ϕ • x) = ϕ ↑x

Tactic:
let ψ := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)

Goal state after:
F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (map (algebraMap F E) p).Splits
ϕ : Gal(E/F)
x : ↑(p.rootSet E)
ψ : p.SplittingField ≃ₐ[F] ↥(IsScalarTower.toAlgHom F p.SplittingField E).range :=
  AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)
⊢ ↑((restrict p E) ϕ • x) = ϕ ↑x
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
⊢ (∑ t ∈ powersetCard n univ, (monomial (∑ i ∈ t, Finsupp.single i 1)) 1).support =
    (powersetCard n univ).biUnion fun t ↦ (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1).support

Tactic:
simp only [← single_eq_monomial]

Goal state after:
σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
⊢ (∑ t ∈ powersetCard n univ, AddMonoidAlgebra.single (∑ i ∈ t, Finsupp.single i 1) 1).support =
    (powersetCard n univ).biUnion fun t ↦ (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1).support
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
⊢ ∀ x ∈ range (s.card + 1),
    (map ((fun p ↦ (map (fun r ↦ X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t ↦ (s - t, t)) (powersetCard x s)).sum =
      C (s.esymm x) * X ^ (s.card - x)

Tactic:
intro _

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
x✝ : ℕ
⊢ x✝ ∈ range (s.card + 1) →
    (map ((fun p ↦ (map (fun r ↦ X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t ↦ (s - t, t)) (powersetCard x✝ s)).sum =
      C (s.esymm x✝) * X ^ (s.card - x✝)