mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case hft
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
⊢ IntegrableOn f (Ioc c b) μ

Tactic:
simp [*, hab.1, hab.2, hbc.1, hbc.2, hac.1, hac.2]

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

Goal state before:
pp: case hst
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
⊢ Disjoint (Ioc a b ∪ Ioc b c) (Ioc c a)

Tactic:
simp [*, hab.1, hab.2, hbc.1, hbc.2, hac.1, hac.2]

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

Goal state before:
pp: case ht
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
⊢ MeasurableSet (Ioc c a)

Tactic:
simp [*, hab.1, hab.2, hbc.1, hbc.2, hac.1, hac.2]

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

Goal state before:
pp: case hfs
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
⊢ IntegrableOn f (Ioc a b ∪ Ioc b c) μ

Tactic:
simp [*, hab.1, hab.2, hbc.1, hbc.2, hac.1, hac.2]

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

Goal state before:
pp: case hft
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
⊢ IntegrableOn f (Ioc c a) μ

Tactic:
simp [*, hab.1, hab.2, hbc.1, hbc.2, hac.1, hac.2]

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

Goal state before:
pp: case hst
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
⊢ Disjoint (Ioc a b) (Ioc b c)

Tactic:
simp [*, hab.1, hab.2, hbc.1, hbc.2, hac.1, hac.2]

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

Goal state before:
pp: case ht
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
⊢ MeasurableSet (Ioc b c)

Tactic:
simp [*, hab.1, hab.2, hbc.1, hbc.2, hac.1, hac.2]

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

Goal state before:
pp: case hfs
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
⊢ IntegrableOn f (Ioc a b) μ

Tactic:
simp [*, hab.1, hab.2, hbc.1, hbc.2, hac.1, hac.2]

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

Goal state before:
pp: case hft
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
⊢ IntegrableOn f (Ioc b c) μ

Tactic:
simp [*, hab.1, hab.2, hbc.1, hbc.2, hac.1, hac.2]

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
μ : Measure ℝ
hf : IntegrableOn f (Ici a) μ
hab : a ≤ b
ha : IntegrableOn f (Ici b) μ
⊢ ∫ (x : ℝ) in Ici a, f x ∂μ - ∫ (x : ℝ) in Ici b, f x ∂μ = ∫ (x : ℝ) in Ico a b, f x ∂μ

Tactic:
have h : IntegrableOn f (Ico a b) μ := hf.mono_set Ico_subset_Ici_self

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.Topology.Algebra.Order.Floor

Goal state before:
pp: α : Type u_1
inst✝⁵ : Ring α
inst✝⁴ : LinearOrder α
inst✝³ : FloorRing α
inst✝² : TopologicalSpace α
inst✝¹ : IsStrictOrderedRing α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ pure (IntCast.intCast (n - 1)) ≤ 𝓝[≤] (↑n - 1)

Tactic:
rw [← @cast_one α, ← cast_sub]

Goal state after:
α : Type u_1
inst✝⁵ : Ring α
inst✝⁴ : LinearOrder α
inst✝³ : FloorRing α
inst✝² : TopologicalSpace α
inst✝¹ : IsStrictOrderedRing α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ pure (IntCast.intCast (n - 1)) ≤ 𝓝[≤] ↑(n - 1)
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c : ℂ
R θ : ℝ
⊢ HasDerivAt (circleMap c R) (circleMap 0 R θ * I) θ

Tactic:
simpa only [mul_assoc, one_mul, ofRealCLM_apply, circleMap, ofReal_one, zero_add]
    using! (((ofRealCLM.hasDerivAt (x := θ)).mul_const I).cexp.const_mul (R : ℂ)).const_add c

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 : ℝ
⊢ a ∈ Ici a₀ → AEStronglyMeasurable ((Ioi a).indicator f) μ

Tactic:
ha

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a ∈ Ici a₀
⊢ AEStronglyMeasurable ((Ioi a).indicator f) μ
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 : ℝ
⊢ a ∈ Ici a₀ → ∀ᵐ (a_2 : ℝ) ∂μ, ‖(Ioi a).indicator f a_2‖ ≤ (Ioi a₀).indicator (norm ∘ f) a_2

Tactic:
ha

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a ∈ Ici a₀
⊢ ∀ᵐ (a_1 : ℝ) ∂μ, ‖(Ioi a).indicator f a_1‖ ≤ (Ioi a₀).indicator (norm ∘ f) a_1
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₀) μ
x : ℝ
hx : a₀ < x
a : ℝ
⊢ a ∈ Iio x → (if a₀ < x then f x else 0) = if a < x then f x else 0

Tactic:
ha

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
x : ℝ
hx : a₀ < x
a : ℝ
ha : a ∈ Iio x
⊢ (if a₀ < x then f x else 0) = if a < x then f x else 0
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₀) μ
x : ℝ
hx : ¬a₀ < x
a : ℝ
⊢ a ∈ Ici a₀ → (if a₀ < x then f x else 0) = if a < x then f x else 0

Tactic:
ha

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
x : ℝ
hx : ¬a₀ < x
a : ℝ
ha : a ∈ Ici a₀
⊢ (if a₀ < x then f x else 0) = if a < x then f x else 0
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 (Iio a₀) μ
a : ℝ
⊢ a ∈ Iic a₀ → AEStronglyMeasurable ((Iio a).indicator f) μ

Tactic:
ha

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ∈ Iic a₀
⊢ AEStronglyMeasurable ((Iio a).indicator f) μ
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 (Iio a₀) μ
a : ℝ
⊢ a ∈ Iic a₀ → ∀ᵐ (a_2 : ℝ) ∂μ, ‖(Iio a).indicator f a_2‖ ≤ (Iio a₀).indicator (norm ∘ f) a_2

Tactic:
ha

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ∈ Iic a₀
⊢ ∀ᵐ (a_1 : ℝ) ∂μ, ‖(Iio a).indicator f a_1‖ ≤ (Iio a₀).indicator (norm ∘ f) a_1
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 (Iio a₀) μ
x : ℝ
hx : x < a₀
a : ℝ
⊢ a ∈ Ioi x → (if x < a₀ then f x else 0) = if x < a then f x else 0

Tactic:
ha

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
x : ℝ
hx : x < a₀
a : ℝ
ha : a ∈ Ioi x
⊢ (if x < a₀ then f x else 0) = if x < a then f x else 0
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 (Iio a₀) μ
x : ℝ
hx : ¬x < a₀
a : ℝ
⊢ a ∈ Iic a₀ → (if x < a₀ then f x else 0) = if x < a then f x else 0

Tactic:
ha

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
x : ℝ
hx : ¬x < a₀
a : ℝ
ha : a ∈ Iic a₀
⊢ (if x < a₀ then f x else 0) = if x < a then f x else 0
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| → -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ ↑n + 1 ≠ 0

Tactic:
rwa [Ne, ← eq_neg_iff_add_eq_zero, ← Int.cast_one, ← Int.cast_neg, Int.cast_inj]

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

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
hR : ↑R ^ n ≠ 0
⊢ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R) θ)‖) * (↑R)⁻¹ ^ n * ↑R ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R) θ)‖

Tactic:
inv_pow

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
hR : ↑R ^ n ≠ 0
⊢ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R) θ)‖) * (↑R ^ n)⁻¹ * ↑R ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R) θ)‖
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → ∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1) = 0
this : ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹ = 2 * ↑π * I
n : ℕ
hn : n ≠ 0
z : ℂ
hz✝ : z ∈ sphere c R
⊢ (z - c)⁻¹ ^ (n + 1) = (z - c) ^ (-↑n - 1)

Tactic:
← zpow_natCast,

Goal state after:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → ∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1) = 0
this : ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹ = 2 * ↑π * I
n : ℕ
hn : n ≠ 0
z : ℂ
hz✝ : z ∈ sphere c R
⊢ (z - c)⁻¹ ^ ↑(n + 1) = (z - c) ^ (-↑n - 1)
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: case h_closed
α : 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 μ
hE : CompleteSpace E
⊢ IsClosed {f | ∫ (z : α × β), ↑↑f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), ↑↑f (x, y) ∂ν ∂μ}

Tactic:
exact isClosed_eq continuous_integral continuous_integral_integral

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

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
F : ℝ → ℝ → E
a b c d : ℝ
h : IntegrableOn (uncurry F) (uIoc a b ×ˢ uIoc c d) volume
⊢ ∫ (x : ℝ) in c..d, (if a ≤ b then 1 else -1) • ∫ (y : ℝ) in uIoc a b, F y x ∂volume =
    ∫ (y : ℝ) in c..d, ∫ (x : ℝ) in a..b, F x y

Tactic:
simp_rw [intervalIntegral.intervalIntegral_eq_integral_uIoc]

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

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z w : ℂ
Hd : DifferentiableOn ℝ f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hi : IntegrableOn (fun z ↦ I • (fderiv ℝ f z) 1 - (fderiv ℝ f z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
x : ℂ
hx : x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ ∅
⊢ [[z.re, w.re]] ×ℂ [[z.im, w.im]] ∈ 𝓝 x

Tactic:
by
      simpa only [← mem_interior_iff_mem_nhds, interior_reProdIm, uIcc, interior_Icc] using hx.1

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

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ (Set.univ.pi fun i ↦ Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Set.Icc a b) volume
⊢ ∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i, (f' x) (e i) i =
    ∑ i,
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (a i) x) i)

Tactic:
rcases em (∃ i, a i = b i) with (⟨i, hi⟩ | hne)

Goal state after:
case inl
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ (Set.univ.pi fun i ↦ Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Set.Icc a b) volume
i : Fin (n + 1)
hi : a i = b i
⊢ ∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i, (f' x) (e i) i =
    ∑ i,
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (a i) x) i)

case inr
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ (Set.univ.pi fun i ↦ Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Set.Icc a b) volume
hne : ¬∃ i, a i = b i
⊢ ∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i, (f' x) (e i) i =
    ∑ i,
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (a i) x) i)
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : Monoid S
inst✝² : DistribMulAction S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
s : S
n : ℕ
m : Multiset R
⊢ s ^ n • m.esymm n = (map (fun x ↦ s • x) m).esymm n

Tactic:
by
  rw [esymm, smul_sum, map_map]
  trans ((powersetCard n m).map (fun x : Multiset R ↦ s ^ card x • x.prod)).sum
  · refine congr_arg _ (map_congr rfl (fun x hx ↦ ?_))
    rw [Function.comp_apply, (mem_powersetCard.1 hx).2]
  · simp_rw [smul_prod, esymm, powersetCard_map, map_map, Function.comp_def]

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
⊢ p.natDegree ∣ Nat.card p.Gal

Tactic:
by
  rw [Gal.card_of_separable p_irr.separable]
  have hp : p.degree ≠ 0 := fun h =>
    Nat.Prime.ne_zero p_deg (natDegree_eq_zero_iff_degree_le_zero.mpr (le_of_eq h))
  let α : p.SplittingField :=
    rootOfSplits (SplittingField.splits p) (by rwa [degree_map])
  have hα : IsIntegral F α := .of_finite F α
  use Module.finrank F⟮α⟯ p.SplittingField
  suffices (minpoly F α).natDegree = p.natDegree by
    let _ : AddCommGroup F⟮α⟯ := Ring.toAddCommGroup
    rw [← Module.finrank_mul_finrank F F⟮α⟯ p.SplittingField,
      IntermediateField.adjoin.finrank hα, this]
  suffices minpoly F α ∣ p by
    have key := (minpoly.irreducible hα).dvd_symm p_irr this
    apply le_antisymm
    · exact natDegree_le_of_dvd this p_irr.ne_zero
    · exact natDegree_le_of_dvd key (minpoly.ne_zero hα)
  apply minpoly.dvd F α
  rw [← eval_map_algebraMap, eval_rootOfSplits]

Goal state after:
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: case inr
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : B < 0
⊢ ‖(map f p).coeff i‖ ≤ max B 1 ^ d * ↑(d.choose (d / 2))

Tactic:
rw [eq_one_of_roots_le hB h1 h2 h4, Polynomial.map_one, coeff_one]

Goal state after:
case inr
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : B < 0
⊢ ‖if i = 0 then 1 else 0‖ ≤ max B 1 ^ d * ↑(d.choose (d / 2))
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
A : Type u_2
inst✝³ : Field A
inst✝² : CharZero A
inst✝¹ : NumberField K
inst✝ : IsAlgClosed A
⊢ Nonempty (K →+* A)

Tactic:
rw [← Fintype.card_pos_iff, NumberField.Embeddings.card K A]

Goal state after:
K : Type u_1
inst✝⁴ : Field K
A : Type u_2
inst✝³ : Field A
inst✝² : CharZero A
inst✝¹ : NumberField K
inst✝ : IsAlgClosed A
⊢ 0 < finrank ℚ K
Module: Mathlib.RingTheory.Valuation.Archimedean

Goal state before:
pp: case refine_1
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
y : O
hx : v ((algebraMap O F) y) ≤ 1
⊢ ∃ y_1, v ((algebraMap O F) y_1) = v ((algebraMap O F) y)

Tactic:
exact ⟨y, by simp⟩

Goal state after:
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₁ a₂ b₁ b₂ : ℝ
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) volume
⊢ ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) =
    (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) -
      ∫ (y : ℝ) in a₂..b₂, f (a₁, y)

Tactic:
by
  wlog h₁ : a₁ ≤ b₁ generalizing a₁ b₁
  · specialize this b₁ a₁
    rw [uIcc_comm b₁ a₁, min_comm b₁ a₁, max_comm b₁ a₁] at this
    simp only [intervalIntegral.integral_symm b₁ a₁]
    refine (congr_arg Neg.neg (this Hcf Hcg Hdf Hdg Hi (le_of_not_ge h₁))).trans ?_; abel
  wlog h₂ : a₂ ≤ b₂ generalizing a₂ b₂
  · specialize this b₂ a₂
    rw [uIcc_comm b₂ a₂, min_comm b₂ a₂, max_comm b₂ a₂] at this
    simp only [intervalIntegral.integral_symm b₂ a₂, intervalIntegral.integral_neg]
    refine (congr_arg Neg.neg (this Hcf Hcg Hdf Hdg Hi (le_of_not_ge h₂))).trans ?_; abel
  simp only [uIcc_of_le h₁, uIcc_of_le h₂, min_eq_left, max_eq_right, h₁, h₂] at Hcf Hcg Hdf Hdg Hi
  calc
    (∫ x in a₁..b₁, ∫ y in a₂..b₂, f' (x, y) (1, 0) + g' (x, y) (0, 1)) =
        ∫ x in Icc a₁ b₁, ∫ y in Icc a₂ b₂, f' (x, y) (1, 0) + g' (x, y) (0, 1) := by
      simp only [intervalIntegral.integral_of_le, h₁, h₂,
        setIntegral_congr_set (Ioc_ae_eq_Icc (α := ℝ) (μ := volume))]
    _ = ∫ x in Icc a₁ b₁ ×ˢ Icc a₂ b₂, f' x (1, 0) + g' x (0, 1) := (setIntegral_prod _ Hi).symm
    _ = (((∫ x in a₁..b₁, g (x, b₂)) - ∫ x in a₁..b₁, g (x, a₂)) + ∫ y in a₂..b₂, f (b₁, y)) -
          ∫ y in a₂..b₂, f (a₁, y) := by
      rw [Icc_prod_Icc] at *
      apply integral_divergence_prod_Icc_of_hasFDerivAt_off_countable_of_le f g f' g'
        (a₁, a₂) (b₁, b₂) ⟨h₁, h₂⟩ s <;> assumption

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x y : S
h : ‖x‖ ≠ ‖y‖
⊢ max (dist x⁻¹ 1) (dist 1 y) = max ‖x⁻¹⁻¹‖ ‖y‖

Tactic:
simp only [dist_one_right, dist_one_left, norm_inv']

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case neg
K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H : Subsingleton (ofClass valuation).ValueGroup₀ˣ
x : K
hx : valuation.restrict x < 1
hx0 : ¬x = 0
⊢ False

Tactic:
← (valuation (K := K)).restrict.zero_iff,

Goal state after:
case neg
K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H : Subsingleton (ofClass valuation).ValueGroup₀ˣ
x : K
hx : valuation.restrict x < 1
hx0 : ¬valuation.restrict x = 0
⊢ False
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑(toLex d) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
this : ↑(toLex u) < φ.lexOrder ∨ ↑(toLex v) < ψ.lexOrder
⊢ (coeff u) φ * (coeff v) ψ = 0

Tactic:
rcases this with (hu | hv)
    · rw [coeff_eq_zero_of_lt_lexOrder hu, zero_mul]
    · rw [coeff_eq_zero_of_lt_lexOrder hv, mul_zero]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
h : constantCoeff φ = 0
n : σ →₀ ℕ
⊢ (if n = 0 then (constantCoeff φ)⁻¹
    else -(constantCoeff φ)⁻¹ * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff x.1) φ * (coeff x.2) φ⁻¹ else 0) =
    (coeff n) 0

Tactic:
split_ifs <;>
        simp only [h, map_zero, zero_mul, inv_zero, neg_zero]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R K
inst✝³ : IsDedekindDomain R
inst✝² : IsFractionRing R K
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
⊢ (HeightOneSpectrum.adicAbv K v) ((algebraMap R K) x) ≤ 1

Tactic:
exact v.adicAbv_coe_le_one (one_lt_absNorm_nnreal v) x

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R K
inst✝³ : IsDedekindDomain R
inst✝² : IsFractionRing R K
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
h_x_nezero : x ≠ 0
⊢ ↑(absNorm v.asIdeal) ^ Multiplicative.toAdd (unzero ⋯) *
      ↑(absNorm v.asIdeal) ^ (Associates.mk v.asIdeal).count (Associates.mk (span {x})).factors =
    1

Tactic:
← zpow_natCast,

Goal state after:
K : Type u_1
inst✝⁶ : Field K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R K
inst✝³ : IsDedekindDomain R
inst✝² : IsFractionRing R K
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
h_x_nezero : x ≠ 0
⊢ ↑(absNorm v.asIdeal) ^ Multiplicative.toAdd (unzero ⋯) *
      ↑(absNorm v.asIdeal) ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (span {x})).factors) =
    1