mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case pos
X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : X → E × F
hf : Integrable f μ
hE : CompleteSpace E
⊢ (∫ (x : X), f x ∂μ).1 = ∫ (x : X), (f x).1 ∂μ

Tactic:
exact ((ContinuousLinearMap.fst ℝ E F).integral_comp_comm hf).symm

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

Goal state before:
pp: X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x ↦ ↑(f x))
C1 : Continuous fun u ↦ ∫ (x : X), ↑↑u x ∂μ.withDensity fun x ↦ ↑(f x)
this : Continuous ((fun u ↦ ∫ (x : X), ↑↑u x ∂μ) ∘ ⇑(withDensitySMulLI μ f_meas))
⊢ Continuous fun u ↦ ∫ (x : X), f x • ↑↑u x ∂μ

Tactic:
convert! this with u

Goal state after:
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x ↦ ↑(f x))
C1 : Continuous fun u ↦ ∫ (x : X), ↑↑u x ∂μ.withDensity fun x ↦ ↑(f x)
this : Continuous ((fun u ↦ ∫ (x : X), ↑↑u x ∂μ) ∘ ⇑(withDensitySMulLI μ f_meas))
u : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
⊢ ∫ (x : X), f x • ↑↑u x ∂μ = ((fun u ↦ ∫ (x : X), ↑↑u x ∂μ) ∘ ⇑(withDensitySMulLI μ f_meas)) u
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c : E
⊢ ‖c‖ₑ ≠ ∞

Tactic:
by simp

Goal state after:
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
inst✝ : Countable ι
F : ι → ℝ → E
bound : ι → ℝ → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) (μ.restrict (Ι a b))
h_bound : ∀ (n : ι), ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ‖F n t‖ ≤ bound n t
bound_summable : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → Summable fun n ↦ bound n t
bound_integrable : IntervalIntegrable (fun t ↦ ∑' (n : ι), bound n t) μ a b
h_lim : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → HasSum (fun n ↦ F n t) (f t)
⊢ HasSum (fun n ↦ ∫ (t : ℝ) in a..b, F n t ∂μ) (∫ (t : ℝ) in a..b, f t ∂μ)

Tactic:
simp only [intervalIntegrable_iff, intervalIntegral_eq_integral_uIoc, ←
    ae_restrict_iff' (α := ℝ) (μ := μ) measurableSet_uIoc] at *

Goal state after:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ι : Type u_3
inst✝ : Countable ι
F : ι → ℝ → E
bound : ι → ℝ → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) (μ.restrict (Ι a b))
h_bound : ∀ (n : ι), ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ‖F n x‖ ≤ bound n x
bound_summable : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), Summable fun n ↦ bound n x
bound_integrable : IntegrableOn (fun t ↦ ∑' (n : ι), bound n t) (Ι a b) μ
h_lim : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasSum (fun n ↦ F n x) (f x)
⊢ HasSum (fun n ↦ (if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F n t ∂μ)
    ((if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, f t ∂μ)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: ι : Type u_1
a b : ℝ
μ : Measure ℝ
ε : Type u_8
inst✝³ : TopologicalSpace ε
inst✝² : ENormedAddCommMonoid ε
inst✝¹ : ContinuousAdd ε
inst✝ : PseudoMetrizableSpace ε
f : ι → ℝ → ε
h : ∀ (i : ι), IntervalIntegrable (f i) μ a b
h₁ : ¬(support f).Finite
⊢ ‖0‖ₑ ≠ ∞

Tactic:
by simp

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

Goal state before:
pp: E : Type u_5
inst✝ : NormedAddCommGroup E
a b : ℝ
f : ℝ → E
c : ℝ
hc : c ≠ 0
h✝ : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
h : IntervalIntegrable (fun x ↦ f (c * x)) volume (a / c) (b / c)
⊢ ‖f (c * (c⁻¹ * min (a / c / c⁻¹) (b / c / c⁻¹)))‖ₑ ≠ ∞

Tactic:
by simp

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

Goal state before:
pp: E : Type u_5
inst✝ : NormedAddCommGroup E
a b : ℝ
f : ℝ → E
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ ‖f (-1 * min (a / -1) (b / -1))‖ₑ ≠ ∞

Tactic:
by simp

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

Goal state before:
pp: E : Type u_5
inst✝ : NormedAddCommGroup E
a b : ℝ
f : ℝ → E
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ ‖f (c + min (a - c) (b - c))‖ₑ ≠ ∞

Tactic:
by simp

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

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, f x ∂μ ∈ {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ}

Tactic:
intervalIntegral_eq_integral_uIoc

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a b : ℝ
⊢ (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ ∈ {∫ (x : ℝ) in Ι a b, 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
c d : ℝ
⊢ c • ∫ (x : ℝ) in a..b, f (d + c * x) = ∫ (x : ℝ) in d + c * a..d + c * b, f x

Tactic:
by_cases hc : c = 0 <;> simp [hc, integral_comp_add_mul]

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

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

Tactic:
by
  by_cases hc : c = 0 <;> simp [hc, integral_comp_mul_sub]

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

Goal state before:
pp: E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f' f : ℝ → E
hderiv : deriv f = f'
hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ f x
hcont : ContinuousOn f' [[a, b]]
⊢ ∫ (y : ℝ) in a..b, f' y = f b - f a

Tactic:
by
  rw [← hderiv, integral_deriv_eq_sub hdiff]
  rw [hderiv]
  exact hcont.intervalIntegrable

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

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hle : ∀ x ∈ Ioc a b, 0 ≤ f x
hlt : ∃ c ∈ Icc a b, 0 < f c
⊢ ∫ (x : ℝ) in a..b, 0 = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: case e'_5
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
c : K
x✝ : ℕ
⊢ c ^ x✝ = 1 * c ^ x✝

Tactic:
rw [one_mul]

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Floor

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

Tactic:
rw [floor_intCast]

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
⊢ volume univ < ∞

Tactic:
by simp

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

Goal state before:
pp: ⊢ volume univ = 1

Tactic:
by simp

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

Goal state before:
pp: c : ℂ
R θ : ℝ
⊢ ↑‖deriv (circleMap c R) θ‖₊ ≤ ↑(Real.nnabs R)

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: case convert_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
y : Fin n → ℝ
hy : y ∈ Box.Icc (I.face i)
g : (Fin (n + 1) → ℝ) → E
hfc : ContinuousOn (fun y ↦ a + f' (y - x) + g y) (Box.Icc I)
Hi :
  ∀ x_1 ∈ Set.Icc (I.lower i) (I.upper i),
    Integrable (I.face i) ⊥ ((fun y ↦ a + f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y ↦ (fun y ↦ a + f' (y - x) + g y) y - a - f' (y - x)
this : ∀ z ∈ Set.Icc (I.lower i) (I.upper i), e z y ∈ Box.Icc I
hε : ∀ y ∈ Box.Icc I, ‖g y‖ ≤ ε * diam (Box.Icc I)
⊢ ‖g (e (I.lower i) y) - g (e (I.upper i) y)‖ ≤ (ε + ε) * diam (Box.Icc I)

Tactic:
add_mul

Goal state after:
case convert_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
y : Fin n → ℝ
hy : y ∈ Box.Icc (I.face i)
g : (Fin (n + 1) → ℝ) → E
hfc : ContinuousOn (fun y ↦ a + f' (y - x) + g y) (Box.Icc I)
Hi :
  ∀ x_1 ∈ Set.Icc (I.lower i) (I.upper i),
    Integrable (I.face i) ⊥ ((fun y ↦ a + f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y ↦ (fun y ↦ a + f' (y - x) + g y) y - a - f' (y - x)
this : ∀ z ∈ Set.Icc (I.lower i) (I.upper i), e z y ∈ Box.Icc I
hε : ∀ y ∈ Box.Icc I, ‖g y‖ ≤ ε * diam (Box.Icc I)
⊢ ‖g (e (I.lower i) y) - g (e (I.upper i) y)‖ ≤ ε * diam (Box.Icc I) + ε * diam (Box.Icc I)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
μ : Measure α
p : ℝ≥0∞
f : α → ε
hf : MemLp f p μ
ν : Measure β
inst✝ : IsFiniteMeasure ν
⊢ ν Set.univ ≠ ∞

Tactic:
by simp

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
ν : Measure β
p : ℝ≥0∞
f : β → ε
hf : MemLp f p ν
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : SFinite ν
⊢ μ Set.univ ≠ ∞

Tactic:
by simp

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:
by
  apply TendstoUniformlyOn.tendsto_intervalIntegral_of_continuousOn
  · refine hf.mono fun i hi ↦ .smul ?_ (hi.comp ?_ ?_)
    · rw [funext (deriv_circleMap _ _)]
      fun_prop
    · fun_prop
    · simp [hR, MapsTo]
  · rw [Metric.tendstoUniformlyOn_iff] at h ⊢
    simp only [dist_smul₀, deriv_circleMap, norm_mul, norm_I, norm_circleMap_zero,
      abs_of_nonneg hR, mul_one]
    intro ε hε
    rcases exists_pos_mul_lt hε R with ⟨δ, hδ₀, hRδ⟩
    refine (h δ hδ₀).mono fun i hi x hx ↦ ?_
    grw [← hRδ, hi (circleMap c R x) (by simp [hR])]

Goal state after:
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 ν))
⊢ ContinuousAt (fun f ↦ ∫ (x : α), ∫ (y : β), ↑↑f (x, y) ∂ν ∂μ) g

Tactic:
refine
    tendsto_integral_of_L1 _ (L1.integrable_coeFn g).integral_prod_left.aestronglyMeasurable
      (Eventually.of_forall fun h => (L1.integrable_coeFn h).integral_prod_left) ?_

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) ∂ν - ∫ (y : β), ↑↑g (x, y) ∂ν‖ₑ ∂μ) (𝓝 g) (𝓝 0)
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J ↦ integral J GP (fun x ↦ f (i.insertNth y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x ↦ ⋯.toBoxAdditive
F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this✝ :
  ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ y₁ ∈ closedBall x δ ∩ Box.Icc I, ∀ y₂ ∈ closedBall x δ ∩ Box.Icc I, ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ : ∀ y₁ ∈ closedBall x δ ∩ Box.Icc I, ∀ y₂ ∈ closedBall x δ ∩ Box.Icc I, ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ Box.Icc J
x✝ : GP.bDistortion = true → J.distortion ≤ c
Hl : J.lower i ∈ Set.Icc (J.lower i) (J.upper i)
Hu : J.upper i ∈ Set.Icc (J.lower i) (J.upper i)
Hi : ∀ x ∈ Set.Icc (J.lower i) (J.upper i), Integrable (J.face i) GP (fun y ↦ f (i.insertNth x y)) BoxAdditiveMap.volume
hJδ' : Box.Icc J ⊆ closedBall x δ ∩ Box.Icc I
Hmaps : ∀ z ∈ Set.Icc (J.lower i) (J.upper i), MapsTo (i.insertNth z) (Box.Icc (J.face i)) (closedBall x δ ∩ Box.Icc I)
this : ∀ (j : Fin (n + 1)), |J.upper j - J.lower j| ≤ 2 * δ
⊢ ∏ j, 2 * δ = (2 * δ) ^ (n + 1)

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J ↦ integral J GP (fun x ↦ f (i.insertNth y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x ↦ ⋯.toBoxAdditive
F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ Box.Icc I \ s
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε'0 : 0 < ε'
hlt : 2 * ↑c * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : closedBall x δ ∩ Box.Icc I ⊆ {x_1 | (fun x_2 ↦ ‖f x_2 - f x - (f' x) (x_2 - x)‖ ≤ ε' * ‖x_2 - x‖) x_1}
J : Box (Fin (n + 1))
hle : J ≤ I
hJδ : Box.Icc J ⊆ closedBall x δ
hxJ : x ∈ Box.Icc J
hJc : GP.bDistortion = true → J.distortion ≤ c
⊢ volume.toBoxAdditive J ≤ (volume.toBoxAdditive.restrict ↑I ⋯) J

Tactic:
by simp

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ Splits 0

Tactic:
by simp

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x : F
⊢ (C x).Splits

Tactic:
by simp

Goal state after:
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)
hq : iteratedDeriv n f c = n.factorial • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z
⊢ ‖n.factorial • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z‖ ≤
    ↑n.factorial * (R * (C / R ^ (n + 1)))

Tactic:
RCLike.norm_nsmul (K := ℂ),

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)
hq : iteratedDeriv n f c = n.factorial • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z
⊢ n.factorial • ‖(2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z‖ ≤
    ↑n.factorial * (R * (C / R ^ (n + 1)))
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)
ψ : p.SplittingField ≃ₐ[F] ↥(IsScalarTower.toAlgHom F p.SplittingField E).range :=
  AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)
⊢ ϕ ↑((rootsEquivRoots p E) ((rootsEquivRoots p E).symm x)) = ϕ ↑x

Tactic:
rw [Equiv.apply_symm_apply (rootsEquivRoots p E)]

Goal state after:
Module: Mathlib.Analysis.Complex.Liouville

Goal state before:
pp: F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
⊢ ‖deriv f c‖ ≤ C / R

Tactic:
have : HasDerivAt (e ∘ f) (e (deriv f c)) c :=
    e.hasFDerivAt.comp_hasDerivAt c
      (hd.differentiableAt isOpen_ball <| mem_ball_self hR).hasDerivAt

Goal state after:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
this : HasDerivAt (⇑e ∘ f) (e (deriv f c)) c
⊢ ‖deriv f c‖ ≤ C / R
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
e : σ ≃ τ
p : ↥(symmetricSubalgebra τ R)
⊢ ↑(((((rename ⇑e).comp (symmetricSubalgebra σ R).val).codRestrict (symmetricSubalgebra τ R) ⋯).comp
          (((rename ⇑e.symm).comp (symmetricSubalgebra τ R).val).codRestrict (symmetricSubalgebra σ R) ⋯))
        p) =
    ↑((AlgHom.id R ↥(symmetricSubalgebra τ R)) p)

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝ : CommSemiring R
e : σ ≃ τ
p : ↥(symmetricSubalgebra σ R)
⊢ ↑(((((rename ⇑e.symm).comp (symmetricSubalgebra τ R).val).codRestrict (symmetricSubalgebra σ R) ⋯).comp
          (((rename ⇑e).comp (symmetricSubalgebra σ R).val).codRestrict (symmetricSubalgebra τ R) ⋯))
        p) =
    ↑((AlgHom.id R ↥(symmetricSubalgebra σ R)) p)

Tactic:
by simp

Goal state after:
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 : ℕ
s t : Finset σ
hst : s ≠ t
h : ∑ i ∈ t, Finsupp.single i 1 = ∑ i ∈ s, Finsupp.single i 1
this : (∑ i ∈ t, Finsupp.single i 1).support = (∑ i ∈ s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support

Tactic:
by simp

Goal state after:
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 : ℕ
s t : Finset σ
hst : s ≠ t
h : ∑ i ∈ t, Finsupp.single i 1 = ∑ i ∈ s, Finsupp.single i 1
this : (t.biUnion fun i ↦ (Finsupp.single i 1).support) = (∑ i ∈ s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support

Tactic:
by simp

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

Goal state before:
pp: case refine_2
E : Type u
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : Preorder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y
he_vol : MeasurePreserving (⇑eL) volume volume
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : s.Countable
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i, (f' i x) (eL.symm (e i))
Hi : IntegrableOn DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding ⇑eL
hIcc : ⇑eL ⁻¹' Set.Icc (eL a) (eL b) = Set.Icc a b
hIcc' : Set.Icc (eL a) (eL b) = ⇑eL.symm ⁻¹' Set.Icc a b
⊢ ∀ x ∈ (Set.univ.pi fun i ↦ Set.Ioo (eL a i) (eL b i)) \ ⇑eL.symm ⁻¹' s,
    ∀ (i : Fin (n + 1)), HasFDerivAt (fun x ↦ f i (eL.symm x)) (f' i (eL.symm x) ∘SL ↑eL.symm) x

Tactic:
refine fun x hx i => (Hd (eL.symm x) ⟨?_, hx.2⟩ i).comp x eL.symm.hasFDerivAt
        rw [← hIcc]
        refine preimage_interior_subset_interior_preimage eL.continuous ?_
        simpa only [Set.mem_preimage, eL.apply_symm_apply, ← pi_univ_Icc,
          interior_pi_set (@finite_univ (Fin _) _), interior_Icc] using hx.1

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r ↦ (map (algebraMap F (r.comp q).SplittingField) r).Splits
key1 : ∀ {r : F[X]}, Irreducible r → P r
key2 : ∀ {p₁ p₂ : F[X]}, P p₁ → P p₂ → P (p₁ * p₂)
⊢ (map (algebraMap F (comp 0 q).SplittingField) 0).Splits

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
f : ℂ → ℂ
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
⊢ ∮ (z : ℂ) in C(c, R), f z / (z - w) = 2 * ↑π * I * f w

Tactic:
simpa only [smul_eq_mul, div_eq_inv_mul] using
    circleIntegral_sub_inv_smul_of_differentiable_on_off_countable hs hw hc hd

Goal state after:
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case pos
p : ℚ[X]
hp : p = 0
this : IsEmpty ↑(p.rootSet ℂ)
⊢ (rootSet 0 ℂ).toFinset.card = (rootSet 0 ℝ).toFinset.card + ∅.card

Tactic:
rootSet_zero,

Goal state after:
case pos
p : ℚ[X]
hp : p = 0
this : IsEmpty ↑(p.rootSet ℂ)
⊢ ∅.toFinset.card = ∅.toFinset.card + ∅.card
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a b : ℝ × ℝ
hle : a ≤ b
Hcf : ContinuousOn f (Set.Icc a b)
Hcg : ContinuousOn g (Set.Icc a b)
Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume
⊢ ∅.Countable

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Valuation.Archimedean

Goal state before:
pp: F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : (Set.range (⇑v ∘ ⇑(algebraMap O F))).WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ ∀ a ∈ {x | x ≤ 1}, ∀ b ∈ {x | x ≤ 1}, a > b → ((fun x1 x2 ↦ x1 > x2) on Subtype.val) a b

Tactic:
by simp

Goal state after: