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

Goal state before:
pp: case hs
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)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ Ι b₀ s ⊆ Icc (b₀ - δ) (b₀ + δ)

Tactic:
apply uIoc_subset_uIcc.trans (uIcc_subset_Icc ?_ ⟨hs.1.le, hs.2.le⟩ )

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)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ b₀ ∈ Icc (b₀ - δ) (b₀ + δ)
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G : Type u_1
inst✝¹⁴ : Group G
inst✝¹³ : MeasurableSpace G
inst✝¹² : TopologicalSpace G
inst✝¹¹ : IsTopologicalGroup G
inst✝¹⁰ : BorelSpace G
inst✝⁹ : PolishSpace G
Γ : Subgroup G
inst✝⁸ : Γ.Normal
inst✝⁷ : T2Space (G ⧸ Γ)
inst✝⁶ : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst✝⁵ : ν.IsMulLeftInvariant
inst✝⁴ : Countable ↥Γ
inst✝³ : ν.IsMulRightInvariant
inst✝² : SigmaFinite ν
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SigmaFinite μ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
V : Set (G ⧸ Γ)
meas_V : MeasurableSet V
neZeroV : μ V ≠ 0
hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)
neTopV : μ V ≠ ∞
U : Set (G ⧸ Γ)
a✝ : MeasurableSet U
meas_π : Measurable QuotientGroup.mk
μ' : Measure (G ⧸ Γ) := map QuotientGroup.mk (ν.restrict s)
has_fund : HasFundamentalDomain (↥Γ.op) G ν
i : QuotientMeasureEqMeasurePreimage ν μ'
this✝¹ : μ'.IsMulLeftInvariant
this✝ : SigmaFinite μ'
this : μ' V / ν (QuotientGroup.mk ⁻¹' V ∩ s) = 1
⊢ 1 • μ = μ

Tactic:
one_smul

Goal state after:
G : Type u_1
inst✝¹⁴ : Group G
inst✝¹³ : MeasurableSpace G
inst✝¹² : TopologicalSpace G
inst✝¹¹ : IsTopologicalGroup G
inst✝¹⁰ : BorelSpace G
inst✝⁹ : PolishSpace G
Γ : Subgroup G
inst✝⁸ : Γ.Normal
inst✝⁷ : T2Space (G ⧸ Γ)
inst✝⁶ : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst✝⁵ : ν.IsMulLeftInvariant
inst✝⁴ : Countable ↥Γ
inst✝³ : ν.IsMulRightInvariant
inst✝² : SigmaFinite ν
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SigmaFinite μ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
V : Set (G ⧸ Γ)
meas_V : MeasurableSet V
neZeroV : μ V ≠ 0
hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)
neTopV : μ V ≠ ∞
U : Set (G ⧸ Γ)
a✝ : MeasurableSet U
meas_π : Measurable QuotientGroup.mk
μ' : Measure (G ⧸ Γ) := map QuotientGroup.mk (ν.restrict s)
has_fund : HasFundamentalDomain (↥Γ.op) G ν
i : QuotientMeasureEqMeasurePreimage ν μ'
this✝¹ : μ'.IsMulLeftInvariant
this✝ : SigmaFinite μ'
this : μ' V / ν (QuotientGroup.mk ⁻¹' V ∩ s) = 1
⊢ μ = μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: case left
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := ⋯
hε : ε < T / 2
y : ℝ
hy₁ : -ε ≤ y
hy₂ : y ≤ ε
⊢ -(T / 2) < y

Tactic:
linarith

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

Goal state before:
pp: case right
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := ⋯
hε : ε < T / 2
y : ℝ
hy₁ : -ε ≤ y
hy₂ : y ≤ ε
⊢ y ≤ T / 2

Tactic:
linarith

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ : QuotientAddGroup.mk ⁻¹' Metric.closedBall 0 ε ∩ I = if ε < T / 2 then Metric.closedBall 0 ε else I
⊢ -(T / 2) + T = T / 2

Tactic:
linarith

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ : QuotientAddGroup.mk ⁻¹' Metric.closedBall 0 ε ∩ I = if ε < T / 2 then Metric.closedBall 0 ε else I
hε : ε < T / 2
⊢ 2 * ε ≤ T

Tactic:
linarith

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ : QuotientAddGroup.mk ⁻¹' Metric.closedBall 0 ε ∩ I = if ε < T / 2 then Metric.closedBall 0 ε else I
hε : ¬ε < T / 2
⊢ T ≤ 2 * ε

Tactic:
linarith

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: case neZeroV
G : Type u_1
inst✝¹⁴ : Group G
inst✝¹³ : MeasurableSpace G
inst✝¹² : TopologicalSpace G
inst✝¹¹ : IsTopologicalGroup G
inst✝¹⁰ : BorelSpace G
inst✝⁹ : PolishSpace G
Γ : Subgroup G
inst✝⁸ : Γ.Normal
inst✝⁷ : T2Space (G ⧸ Γ)
inst✝⁶ : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
inst✝⁵ : Countable ↥Γ
ν : Measure G
inst✝⁴ : ν.IsHaarMeasure
inst✝³ : ν.IsMulRightInvariant
inst✝² : SigmaFinite ν
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SigmaFinite μ
V : Set (G ⧸ Γ)
hV : (interior V).Nonempty
meas_V : MeasurableSet V
hμK : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ 𝓕)
neTopV : μ V ≠ ∞
⊢ μ V ≠ 0

Tactic:
rw [hμK]

Goal state after:
case neZeroV
G : Type u_1
inst✝¹⁴ : Group G
inst✝¹³ : MeasurableSpace G
inst✝¹² : TopologicalSpace G
inst✝¹¹ : IsTopologicalGroup G
inst✝¹⁰ : BorelSpace G
inst✝⁹ : PolishSpace G
Γ : Subgroup G
inst✝⁸ : Γ.Normal
inst✝⁷ : T2Space (G ⧸ Γ)
inst✝⁶ : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
inst✝⁵ : Countable ↥Γ
ν : Measure G
inst✝⁴ : ν.IsHaarMeasure
inst✝³ : ν.IsMulRightInvariant
inst✝² : SigmaFinite ν
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SigmaFinite μ
V : Set (G ⧸ Γ)
hV : (interior V).Nonempty
meas_V : MeasurableSet V
hμK : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ 𝓕)
neTopV : μ V ≠ ∞
⊢ ν (QuotientGroup.mk ⁻¹' V ∩ 𝓕) ≠ 0
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: case neTopV
G : Type u_1
inst✝¹² : Group G
inst✝¹¹ : MeasurableSpace G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : IsTopologicalGroup G
inst✝⁸ : BorelSpace G
inst✝⁷ : PolishSpace G
Γ : Subgroup G
inst✝⁶ : Γ.Normal
inst✝⁵ : T2Space (G ⧸ Γ)
inst✝⁴ : SecondCountableTopology (G ⧸ Γ)
inst✝³ : Countable ↥Γ
ν : Measure G
inst✝² : ν.IsHaarMeasure
inst✝¹ : ν.IsMulRightInvariant
inst✝ : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : ν 𝓕 ≠ ∞
c : ℝ≥0∞ := ⋯
c_ne_top : c ≠ ∞
μ : Measure (G ⧸ Γ) := ⋯
hμK : μ ↑K = c
this : SigmaFinite μ
⊢ μ ↑K ≠ ∞

Tactic:
rw [hμK]

Goal state after:
case neTopV
G : Type u_1
inst✝¹² : Group G
inst✝¹¹ : MeasurableSpace G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : IsTopologicalGroup G
inst✝⁸ : BorelSpace G
inst✝⁷ : PolishSpace G
Γ : Subgroup G
inst✝⁶ : Γ.Normal
inst✝⁵ : T2Space (G ⧸ Γ)
inst✝⁴ : SecondCountableTopology (G ⧸ Γ)
inst✝³ : Countable ↥Γ
ν : Measure G
inst✝² : ν.IsHaarMeasure
inst✝¹ : ν.IsMulRightInvariant
inst✝ : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : ν 𝓕 ≠ ∞
c : ℝ≥0∞ := ν (QuotientGroup.mk ⁻¹' ↑K ∩ 𝓕)
c_ne_top : c ≠ ∞
μ : Measure (G ⧸ Γ) := c • haarMeasure K
hμK : μ ↑K = c
this : SigmaFinite μ
⊢ c ≠ ∞
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)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
x : ℝ
hx : x ∈ Icc (b₀ - δ) (b₀ + δ)
⊢ M + δ ≤ M + 1

Tactic:
linarith

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

Goal state before:
pp: case inr.inl
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT✝ : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T t : ℝ},
    Periodic f T →
      T ≠ 0 → IntervalIntegrable f volume t (t + T) → ∀ (a₁ a₂ : ℝ), 0 < T → IntervalIntegrable f volume a₁ a₂
hT : ¬0 < T
h : T = 0
⊢ IntervalIntegrable f volume a₁ a₂

Tactic:
tauto

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

Goal state before:
pp: case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
ι : Type u_3
f : ι → ℂ → E
h : ∀ (i : ι), CircleIntegrable (f i) c R
h₁ : ¬(support f).Finite
⊢ CircleIntegrable (∑ᶠ (i : ι), f i) c R

Tactic:
· rw [finsum_of_infinite_support h₁]
    apply circleIntegrable_const

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = m • ∫ (x : ℝ) in 0..T, f x
n : ℕ
⊢ (-1 + -↑n) * T + (↑n + 1) * T = 0

Tactic:
linarith

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hf₁ : CircleIntegrable f₁ c R
hR : ¬R = 0
⊢ EqOn (fun θ ↦ f₁ (circleMap c R θ)) (fun θ ↦ f₂ (circleMap c R θ)) (circleMap c R ⁻¹' {z | f₁ z = f₂ z})

Tactic:
tauto

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

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

Tactic:
by
  by_cases h₀ : R = 0
  · simp +unfoldPartialApp [h₀, const]
  refine ⟨fun h => h.out, fun h => ?_⟩
  simp only [CircleIntegrable, intervalIntegrable_iff, deriv_circleMap] at h ⊢
  refine (h.norm.const_mul |R|⁻¹).mono' ?_ ?_
  · have H : ∀ {θ}, circleMap 0 R θ * I ≠ 0 := fun {θ} => by simp [h₀, I_ne_zero]
    simpa only [inv_smul_smul₀ H]
      using ((continuous_circleMap 0 R).aestronglyMeasurable.mul_const
        I).aemeasurable.fun_inv.aestronglyMeasurable.fun_smul h.aestronglyMeasurable
  · simp [norm_smul, h₀]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
⊢ ∫ (θ : ℝ) in 0..2 * π, deriv (circleMap c R) θ • f (circleMap c R θ) =
    ∫ (θ : ℝ) in Icc 0 (2 * π), deriv (circleMap c R) θ • f (circleMap c R θ)

Tactic:
intervalIntegral.integral_of_le Real.two_pi_pos.le,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
⊢ ∫ (x : ℝ) in Ioc 0 (2 * π), deriv (circleMap c R) x • f (circleMap c R x) ∂volume =
    ∫ (θ : ℝ) in Icc 0 (2 * π), deriv (circleMap c R) θ • f (circleMap c R θ)
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℂ
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hR : R ≠ 0
⊢ Ι 0 (2 * π) ⊆ univ

Tactic:
tauto

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

Goal state before:
pp: case refine_1
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
I : Box (Fin (n + 1))
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 : ∀ (i : Fin (n + 1)), ContinuousOn (fun y ↦ f y i) (Box.Icc I)
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc I) volume
hE : CompleteSpace E
A :
  HasIntegral I ⊥ (fun x ↦ ∑ i, (f' x) (e i) i) volume.toBoxAdditive.toSMul
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i, (f' x) (e i) i ∂volume)
B :
  HasIntegral I IntegrationParams.GP (fun x ↦ ∑ i, (f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i,
      (BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x ↦ f (i.insertNth (I.upper i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x ↦ f (i.insertNth (I.lower i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
this : ContinuousOn ((fun y ↦ f y i) ∘ i.insertNth (I.upper i)) (Box.Icc (I.face i))
⊢ BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x ↦ f (i.insertNth (I.upper i) x) i) BoxAdditiveMap.volume =
    ∫ (x : Fin n → ℝ) in ↑(I.face i), f (i.insertNth (I.upper i) x) i

Tactic:
have := (this.integrableOn_compact (μ := volume) (Box.isCompact_Icc _)).mono_set
      Box.coe_subset_Icc

Goal state after:
case refine_1
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
I : Box (Fin (n + 1))
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 : ∀ (i : Fin (n + 1)), ContinuousOn (fun y ↦ f y i) (Box.Icc I)
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc I) volume
hE : CompleteSpace E
A :
  HasIntegral I ⊥ (fun x ↦ ∑ i, (f' x) (e i) i) volume.toBoxAdditive.toSMul
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i, (f' x) (e i) i ∂volume)
B :
  HasIntegral I IntegrationParams.GP (fun x ↦ ∑ i, (f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i,
      (BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x ↦ f (i.insertNth (I.upper i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x ↦ f (i.insertNth (I.lower i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
this✝ : ContinuousOn ((fun y ↦ f y i) ∘ i.insertNth (I.upper i)) (Box.Icc (I.face i))
this : IntegrableOn ((fun y ↦ f y i) ∘ i.insertNth (I.upper i)) (↑(I.face i)) volume
⊢ BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x ↦ f (i.insertNth (I.upper i) x) i) BoxAdditiveMap.volume =
    ∫ (x : Fin n → ℝ) in ↑(I.face i), f (i.insertNth (I.upper i) x) i
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case refine_2
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
I : Box (Fin (n + 1))
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 : ∀ (i : Fin (n + 1)), ContinuousOn (fun y ↦ f y i) (Box.Icc I)
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc I) volume
hE : CompleteSpace E
A :
  HasIntegral I ⊥ (fun x ↦ ∑ i, (f' x) (e i) i) volume.toBoxAdditive.toSMul
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i, (f' x) (e i) i ∂volume)
B :
  HasIntegral I IntegrationParams.GP (fun x ↦ ∑ i, (f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i,
      (BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x ↦ f (i.insertNth (I.upper i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x ↦ f (i.insertNth (I.lower i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
this : ContinuousOn ((fun y ↦ f y i) ∘ i.insertNth (I.lower i)) (Box.Icc (I.face i))
⊢ BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x ↦ f (i.insertNth (I.lower i) x) i) BoxAdditiveMap.volume =
    ∫ (x : Fin n → ℝ) in ↑(I.face i), f (i.insertNth (I.lower i) x) i

Tactic:
have := (this.integrableOn_compact (μ := volume) (Box.isCompact_Icc _)).mono_set
      Box.coe_subset_Icc

Goal state after:
case refine_2
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
I : Box (Fin (n + 1))
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 : ∀ (i : Fin (n + 1)), ContinuousOn (fun y ↦ f y i) (Box.Icc I)
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc I) volume
hE : CompleteSpace E
A :
  HasIntegral I ⊥ (fun x ↦ ∑ i, (f' x) (e i) i) volume.toBoxAdditive.toSMul
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i, (f' x) (e i) i ∂volume)
B :
  HasIntegral I IntegrationParams.GP (fun x ↦ ∑ i, (f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i,
      (BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x ↦ f (i.insertNth (I.upper i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x ↦ f (i.insertNth (I.lower i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
this✝ : ContinuousOn ((fun y ↦ f y i) ∘ i.insertNth (I.lower i)) (Box.Icc (I.face i))
this : IntegrableOn ((fun y ↦ f y i) ∘ i.insertNth (I.lower i)) (↑(I.face i)) volume
⊢ BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x ↦ f (i.insertNth (I.lower i) x) i) BoxAdditiveMap.volume =
    ∫ (x : Fin n → ℝ) in ↑(I.face i), f (i.insertNth (I.lower i) x) i
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ z ∈ sphere c |R|, HasDerivWithinAt f (f' z) (sphere c |R|) z
hi : ¬CircleIntegrable f' c R
⊢ ∮ (z : ℂ) in C(c, R), f' z = 0

Tactic:
· exact integral_undef hi

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
⊢ HasSum (fun n ↦ ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)

Tactic:
have hwR : ‖w‖ / R ∈ Ico (0 : ℝ) 1 :=
    ⟨div_nonneg (norm_nonneg w) hR.le, (div_lt_one hR).2 hw⟩

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : ‖w‖ / R ∈ Ico 0 1
⊢ HasSum (fun n ↦ ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)
Module: Mathlib.MeasureTheory.Integral.Prod

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

Tactic:
simp [this]

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

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

Tactic:
simp [this]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Vieta

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

Tactic:
map_bind,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
⊢ ((range (s.card + 1)).bind fun a ↦
        map ((fun p ↦ (map (fun r ↦ X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t ↦ (s - t, t)) (powersetCard a s)).sum =
    ∑ j ∈ Finset.range (s.card + 1), C (s.esymm j) * X ^ (s.card - j)
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
f : ℂ → E
c : ℂ
s : Set ℂ
h0 : 0 < R
n : ℕ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
this : (n.factorial • (cauchyPowerSeries f c (↑(NNReal.mk R ⋯)) n) fun x ↦ 1) = 1 • iteratedDeriv n f c
⊢ ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z = (2 * ↑π * I / ↑n.factorial) • iteratedDeriv n f c

Tactic:
one_smul

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
f : ℂ → E
c : ℂ
s : Set ℂ
h0 : 0 < R
n : ℕ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
this : (n.factorial • (cauchyPowerSeries f c (↑(NNReal.mk R ⋯)) n) fun x ↦ 1) = iteratedDeriv n f c
⊢ ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z = (2 * ↑π * I / ↑n.factorial) • iteratedDeriv n f c
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: f : ℂ[X]
hf : 0 < f.degree
hf' : ∀ (z : ℂ), ¬f.IsRoot z
this : ∀ (z : ℂ), (eval z f)⁻¹ = 0
z : ℂ
⊢ (eval z f)⁻¹ = (eval z (C 0))⁻¹

Tactic:
simp [this]

Goal state after: