mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: case refine_2
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
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0, (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2

Tactic:
·

Goal state after:
case refine_2
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
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0, (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case refine_1
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
n : ℕ
⊢ AEStronglyMeasurable
    (fun θ ↦ deriv (circleMap c R) θ • (fun z ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R θ))
    (volume.restrict (Ι 0 (2 * π)))

pp: case refine_2
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
n : ℕ
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) →
      ‖deriv (circleMap c R) t • (fun z ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t)‖ ≤
        ‖f (circleMap c R t)‖ * (‖w‖ / R) ^ n

pp: case refine_3
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
⊢ ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → Summable fun n ↦ ‖f (circleMap c R t)‖ * (‖w‖ / R) ^ n

pp: case refine_4
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
⊢ IntervalIntegrable (fun t ↦ ∑' (n : ℕ), ‖f (circleMap c R t)‖ * (‖w‖ / R) ^ n) volume 0 (2 * π)

pp: case refine_5
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
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) →
      HasSum (fun n ↦ deriv (circleMap c R) t • (fun z ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t))
        (deriv (circleMap c R) t • (fun z ↦ (z - (c + w))⁻¹ • f z) (circleMap c R t))

Tactic:
·

Goal state after:
case refine_1
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
n : ℕ
⊢ AEStronglyMeasurable
    (fun θ ↦ deriv (circleMap c R) θ • (fun z ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R θ))
    (volume.restrict (Ι 0 (2 * π)))
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 ν))
⊢ ↥(Lp E 1 (μ.prod ν)) → ℝ≥0∞

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 ν))
⊢ Tendsto ?m.112 (𝓝 g) (𝓝 0)

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 ν))
⊢ (fun i ↦ ∫⁻ (x : α), ‖∫ (y : β), ↑↑i (x, y) - ↑↑g (x, y) ∂ν‖ₑ ∂μ) ≤ ?m.112

Tactic:
·

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 ν))
⊢ ↥(Lp E 1 (μ.prod ν)) → ℝ≥0∞
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 ν))
⊢ (fun i ↦ ∫⁻ (x : α), ‖∫ (y : β), ↑↑i (x, y) - ↑↑g (x, y) ∂ν‖ₑ ∂μ) ≤ fun i ↦
    ∫⁻ (x : α), ∫⁻ (y : β), ‖↑↑i (x, y) - ↑↑g (x, y)‖ₑ ∂ν ∂μ

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 ν))
⊢ Tendsto (fun i ↦ ∫⁻ (x : α), ∫⁻ (y : β), ‖↑↑i (x, y) - ↑↑g (x, y)‖ₑ ∂ν ∂μ) (𝓝 g) (𝓝 0)

Tactic:
·

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 ν))
⊢ (fun i ↦ ∫⁻ (x : α), ‖∫ (y : β), ↑↑i (x, y) - ↑↑g (x, y) ∂ν‖ₑ ∂μ) ≤ fun i ↦
    ∫⁻ (x : α), ∫⁻ (y : β), ‖↑↑i (x, y) - ↑↑g (x, y)‖ₑ ∂ν ∂μ
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case refine_1.hf
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
n : ℕ
⊢ Measurable fun θ ↦ circleMap 0 R θ * I

pp: case refine_1.hg.hf
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
n : ℕ
⊢ Measurable fun θ ↦ (w / (circleMap c R θ - c)) ^ n

pp: case refine_1.hg.hg.hf
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
n : ℕ
⊢ Measurable fun θ ↦ (circleMap c R θ - c)⁻¹

Tactic:
·

Goal state after:
case refine_1.hf
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
n : ℕ
⊢ Measurable fun θ ↦ circleMap 0 R θ * I
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case refine_1.hg.hf
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
n : ℕ
⊢ Measurable fun θ ↦ (w / (circleMap c R θ - c)) ^ n

pp: case refine_1.hg.hg.hf
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
n : ℕ
⊢ Measurable fun θ ↦ (circleMap c R θ - c)⁻¹

Tactic:
·

Goal state after:
case refine_1.hg.hf
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
n : ℕ
⊢ Measurable fun θ ↦ (w / (circleMap c R θ - c)) ^ n
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case refine_1.hg.hg.hf
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
n : ℕ
⊢ Measurable fun θ ↦ (circleMap c R θ - c)⁻¹

Tactic:
·

Goal state after:
case refine_1.hg.hg.hf
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
n : ℕ
⊢ Measurable fun θ ↦ (circleMap c R θ - c)⁻¹
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: case neg
α : 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 μ
f : α × β → E
hf : Integrable f (μ.prod ν)
hE : ¬CompleteSpace E
⊢ ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ

pp: case pos
α : 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 μ
f : α × β → E
hf : Integrable f (μ.prod ν)
hE : CompleteSpace E
⊢ ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ

Tactic:
·

Goal state after:
case neg
α : 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 μ
f : α × β → E
hf : Integrable f (μ.prod ν)
hE : ¬CompleteSpace E
⊢ ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case refine_2
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
n : ℕ
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) →
      ‖deriv (circleMap c R) t • (fun z ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t)‖ ≤
        ‖f (circleMap c R t)‖ * (‖w‖ / R) ^ n

pp: case refine_3
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
⊢ ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → Summable fun n ↦ ‖f (circleMap c R t)‖ * (‖w‖ / R) ^ n

pp: case refine_4
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
⊢ IntervalIntegrable (fun t ↦ ∑' (n : ℕ), ‖f (circleMap c R t)‖ * (‖w‖ / R) ^ n) volume 0 (2 * π)

pp: case refine_5
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
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) →
      HasSum (fun n ↦ deriv (circleMap c R) t • (fun z ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t))
        (deriv (circleMap c R) t • (fun z ↦ (z - (c + w))⁻¹ • f z) (circleMap c R t))

Tactic:
·

Goal state after:
case refine_2
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
n : ℕ
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) →
      ‖deriv (circleMap c R) t • (fun z ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t)‖ ≤
        ‖f (circleMap c R t)‖ * (‖w‖ / R) ^ n
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case refine_3
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
⊢ ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → Summable fun n ↦ ‖f (circleMap c R t)‖ * (‖w‖ / R) ^ n

pp: case refine_4
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
⊢ IntervalIntegrable (fun t ↦ ∑' (n : ℕ), ‖f (circleMap c R t)‖ * (‖w‖ / R) ^ n) volume 0 (2 * π)

pp: case refine_5
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
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) →
      HasSum (fun n ↦ deriv (circleMap c R) t • (fun z ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t))
        (deriv (circleMap c R) t • (fun z ↦ (z - (c + w))⁻¹ • f z) (circleMap c R t))

Tactic:
·

Goal state after:
case refine_3
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
⊢ ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → Summable fun n ↦ ‖f (circleMap c R t)‖ * (‖w‖ / R) ^ n
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case refine_4
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
⊢ IntervalIntegrable (fun t ↦ ∑' (n : ℕ), ‖f (circleMap c R t)‖ * (‖w‖ / R) ^ n) volume 0 (2 * π)

pp: case refine_5
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
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) →
      HasSum (fun n ↦ deriv (circleMap c R) t • (fun z ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t))
        (deriv (circleMap c R) t • (fun z ↦ (z - (c + w))⁻¹ • f z) (circleMap c R t))

Tactic:
·

Goal state after:
case refine_4
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
⊢ IntervalIntegrable (fun t ↦ ∑' (n : ℕ), ‖f (circleMap c R t)‖ * (‖w‖ / R) ^ n) volume 0 (2 * π)
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case refine_5
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
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) →
      HasSum (fun n ↦ deriv (circleMap c R) t • (fun z ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t))
        (deriv (circleMap c R) t • (fun z ↦ (z - (c + w))⁻¹ • f z) (circleMap c R t))

Tactic:
·

Goal state after:
case refine_5
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
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) →
      HasSum (fun n ↦ deriv (circleMap c R) t • (fun z ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t))
        (deriv (circleMap c R) t • (fun z ↦ (z - (c + w))⁻¹ • f z) (circleMap c R t))
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: case pos.h_ind
α : 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
⊢ ∀ (c : E) ⦃s : Set (α × β)⦄,
    MeasurableSet s →
      (μ.prod ν) s < ∞ →
        ∫ (z : α × β), s.indicator (fun x ↦ c) z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), s.indicator (fun x ↦ c) (x, y) ∂ν ∂μ

pp: case pos.h_add
α : 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
⊢ ∀ ⦃f g : α × β → E⦄,
    Disjoint (support f) (support g) →
      Integrable f (μ.prod ν) →
        Integrable g (μ.prod ν) →
          ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ →
            ∫ (z : α × β), g z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ →
              ∫ (z : α × β), (f + g) z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), (f + g) (x, y) ∂ν ∂μ

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) ∂ν ∂μ}

pp: case h_ae
α : 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
⊢ ∀ ⦃f g : α × β → E⦄,
    f =ᵐ[μ.prod ν] g →
      Integrable f (μ.prod ν) →
        ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ →
          ∫ (z : α × β), g z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ

Tactic:
·

Goal state after:
case pos.h_ind
α : 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
⊢ ∀ (c : E) ⦃s : Set (α × β)⦄,
    MeasurableSet s →
      (μ.prod ν) s < ∞ →
        ∫ (z : α × β), s.indicator (fun x ↦ c) z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), s.indicator (fun x ↦ c) (x, y) ∂ν ∂μ
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: case pos.h_add
α : 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
⊢ ∀ ⦃f g : α × β → E⦄,
    Disjoint (support f) (support g) →
      Integrable f (μ.prod ν) →
        Integrable g (μ.prod ν) →
          ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ →
            ∫ (z : α × β), g z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ →
              ∫ (z : α × β), (f + g) z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), (f + g) (x, y) ∂ν ∂μ

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) ∂ν ∂μ}

pp: case h_ae
α : 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
⊢ ∀ ⦃f g : α × β → E⦄,
    f =ᵐ[μ.prod ν] g →
      Integrable f (μ.prod ν) →
        ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ →
          ∫ (z : α × β), g z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ

Tactic:
·

Goal state after:
case pos.h_add
α : 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
⊢ ∀ ⦃f g : α × β → E⦄,
    Disjoint (support f) (support g) →
      Integrable f (μ.prod ν) →
        Integrable g (μ.prod ν) →
          ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ →
            ∫ (z : α × β), g z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ →
              ∫ (z : α × β), (f + g) z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), (f + g) (x, y) ∂ν ∂μ
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) ∂ν ∂μ}

pp: case h_ae
α : 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
⊢ ∀ ⦃f g : α × β → E⦄,
    f =ᵐ[μ.prod ν] g →
      Integrable f (μ.prod ν) →
        ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ →
          ∫ (z : α × β), g z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ

Tactic:
·

Goal state after:
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) ∂ν ∂μ}
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: case h_ae
α : 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
⊢ ∀ ⦃f g : α × β → E⦄,
    f =ᵐ[μ.prod ν] g →
      Integrable f (μ.prod ν) →
        ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ →
          ∫ (z : α × β), g z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ

Tactic:
·

Goal state after:
case h_ae
α : 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
⊢ ∀ ⦃f g : α × β → E⦄,
    f =ᵐ[μ.prod ν] g →
      Integrable f (μ.prod ν) →
        ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ →
          ∫ (z : α × β), g z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: case e'_2
α : 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
f g : α × β → E
hfg : f =ᵐ[μ.prod ν] g
hf : ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
⊢ ∫ (z : α × β), g z ∂μ.prod ν = ∫ (z : α × β), f z ∂μ.prod ν

pp: case e'_3
α : 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
f g : α × β → E
hfg : f =ᵐ[μ.prod ν] g
hf : ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
⊢ ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ

Tactic:
·

Goal state after:
case e'_2
α : 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
f g : α × β → E
hfg : f =ᵐ[μ.prod ν] g
hf : ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
⊢ ∫ (z : α × β), g z ∂μ.prod ν = ∫ (z : α × β), f z ∂μ.prod ν