mathlib-initiative/mathlib-tactics huggingface dataset:
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 ν
f : α × β → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
x : α
hx : ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
⊢ ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν = ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν

pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
x : α
hx : ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
⊢ ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν ≠ ∞

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 ν
f : α × β → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
x : α
hx : ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
⊢ ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν ≠ ∞
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 ν
f : α × β → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
x : α
hx : ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
⊢ ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞

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 ν
f : α × β → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
x : α
hx : ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
⊢ ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
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 ν
f : α × β → E
h1f : AEStronglyMeasurable f (μ.prod ν)
⊢ (∀ᵐ (x : α) ∂μ, HasFiniteIntegral (fun y ↦ AEStronglyMeasurable.mk f h1f (x, y)) ν) ∧
      HasFiniteIntegral (fun x ↦ ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν) μ ↔
    (∀ᵐ (x : α) ∂μ, HasFiniteIntegral (fun y ↦ f (x, y)) ν) ∧ HasFiniteIntegral (fun x ↦ ∫ (y : β), ‖f (x, y)‖ ∂ν) μ

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 ν
f : α × β → E
h1f : AEStronglyMeasurable f (μ.prod ν)
⊢ (∀ᵐ (x : α) ∂μ, HasFiniteIntegral (fun y ↦ AEStronglyMeasurable.mk f h1f (x, y)) ν) ∧
      HasFiniteIntegral (fun x ↦ ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν) μ ↔
    (∀ᵐ (x : α) ∂μ, HasFiniteIntegral (fun y ↦ f (x, y)) ν) ∧ HasFiniteIntegral (fun x ↦ ∫ (y : β), ‖f (x, y)‖ ∂ν) μ
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: case e'_1
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : SFinite ν
inst✝ : SFinite μ
f : α × β → E
h1f : AEStronglyMeasurable f (μ.prod ν)
⊢ Integrable f (μ.prod ν) ↔ Integrable f (μ.prod ν)

Tactic:
]

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

Goal state before:
pp: case pos
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 = (f ∘ circleMap c R) (2 * π) - (f ∘ circleMap c R) 0

Tactic:
]

Goal state after:
case pos
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 = (f ∘ circleMap c R) (2 * π) - (f ∘ circleMap c R) 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 α
inst✝¹ : NormedAddCommGroup E
f : α → E
hf : MemLp f 1 μ
ν : Measure β
inst✝ : IsFiniteMeasure ν
⊢ MemLp (fun x ↦ f x.1) 1 (μ.prod ν)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
inst✝¹ : NormedAddCommGroup E
f : α → E
hf : MemLp f 1 μ
ν : Measure β
inst✝ : IsFiniteMeasure ν
⊢ MemLp (fun x ↦ f x.1) 1 (μ.prod ν)
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : SFinite ν
f : β → E
hf : MemLp f 1 ν
μ : Measure α
inst✝ : IsFiniteMeasure μ
⊢ MemLp (fun x ↦ f x.2) 1 (μ.prod ν)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : SFinite ν
f : β → E
hf : MemLp f 1 ν
μ : Measure α
inst✝ : IsFiniteMeasure μ
⊢ MemLp (fun x ↦ f x.2) 1 (μ.prod ν)
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

Tactic:
]

Goal state after:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| → -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ ¬n = -1
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
w : ℂ
⊢ w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z =
    w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z

Tactic:
]

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✝ : SFinite μ
f : α × β → E
s : Set α
t : Set β
hf : Integrable f ((μ.restrict s).prod (ν.restrict t))
⊢ Integrable (f ∘ Prod.swap) ((ν.restrict t).prod (μ.restrict s))

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✝ : SFinite μ
f : α × β → E
s : Set α
t : Set β
hf : Integrable f ((μ.restrict s).prod (ν.restrict t))
⊢ Integrable (f ∘ Prod.swap) ((ν.restrict t).prod (μ.restrict s))
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: 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 : ContinuousOn f (Box.Icc I)
Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x
J : ℕ →o Box (Fin (n + 1))
hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I
hJl : Tendsto (Box.lower ∘ ⇑J) atTop (𝓝 I.lower)
hJu : Tendsto (Box.upper ∘ ⇑J) atTop (𝓝 I.upper)
hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I
hJ_le : ∀ (k : ℕ), J k ≤ I
HcJ : ∀ (k : ℕ), ContinuousOn f (Box.Icc (J k))
HdJ : ∀ (k : ℕ), ∀ x ∈ Box.Icc (J k) \ s, HasFDerivWithinAt f (f' x) (Box.Icc (J k)) x
HiJ : ∀ (k : ℕ), IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc (J k)) volume
HJ_eq :
  ∀ (k : ℕ),
    ∫ (x : Fin (n + 1) → ℝ) in Box.Icc (J k), ∑ i, (f' x) (e i) i =
      ∑ i,
        ((∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).upper i) x) i) -
          ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).lower i) x) i)
Hi : Integrable (fun x ↦ ∑ i, (f' x) (e i) i) (volume.restrict (⋃ n_1, Box.Ioo (J n_1)))
⊢ Tendsto (fun k ↦ ∫ (x : Fin (n + 1) → ℝ) in Box.Ioo (J k), ∑ i, (f' x) (e i) i) atTop
    (𝓝 (∫ (x : Fin (n + 1) → ℝ) in ⋃ n_1, Box.Ioo (J n_1), ∑ i, (f' x) (e i) i))

Tactic:
]

Goal state after:
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 : ContinuousOn f (Box.Icc I)
Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x
J : ℕ →o Box (Fin (n + 1))
hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I
hJl : Tendsto (Box.lower ∘ ⇑J) atTop (𝓝 I.lower)
hJu : Tendsto (Box.upper ∘ ⇑J) atTop (𝓝 I.upper)
hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I
hJ_le : ∀ (k : ℕ), J k ≤ I
HcJ : ∀ (k : ℕ), ContinuousOn f (Box.Icc (J k))
HdJ : ∀ (k : ℕ), ∀ x ∈ Box.Icc (J k) \ s, HasFDerivWithinAt f (f' x) (Box.Icc (J k)) x
HiJ : ∀ (k : ℕ), IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc (J k)) volume
HJ_eq :
  ∀ (k : ℕ),
    ∫ (x : Fin (n + 1) → ℝ) in Box.Icc (J k), ∑ i, (f' x) (e i) i =
      ∑ i,
        ((∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).upper i) x) i) -
          ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).lower i) x) i)
Hi : Integrable (fun x ↦ ∑ i, (f' x) (e i) i) (volume.restrict (⋃ n_1, Box.Ioo (J n_1)))
⊢ Tendsto (fun k ↦ ∫ (x : Fin (n + 1) → ℝ) in Box.Ioo (J k), ∑ i, (f' x) (e i) i) atTop
    (𝓝 (∫ (x : Fin (n + 1) → ℝ) in ⋃ n_1, Box.Ioo (J n_1), ∑ i, (f' x) (e i) i))
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
f : α × β → E
hf : Integrable f (μ.prod ν)
x : α
⊢ ∫ (a : β), ‖f (x, a)‖ ∂ν ≤ ‖∫ (y : β), ‖f (x, y)‖ ∂ν‖

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
f : α × β → E
hf : Integrable f (μ.prod ν)
x : α
⊢ ∫ (a : β), ‖f (x, a)‖ ∂ν ≤ ‖∫ (y : β), ‖f (x, y)‖ ∂ν‖
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 μ
s : Set α
t : Set β
f : α × β → E
⊢ ∫ (z : α × β), f z ∂(μ.restrict s).prod (ν.restrict t) = ∫ (z : α × β), f z ∂(μ.restrict s).prod (ν.restrict t)

Tactic:
]

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 : ℝ
n : ℕ
hR : R ≠ 0
⊢ (2 * π)⁻¹ * ((∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c R x)‖) * |R|⁻¹ ^ n) ≤
    (2 * π)⁻¹ * ((∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c R θ)‖) * |R|⁻¹ ^ n)

pp: case inr.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
hR : R ≠ 0
⊢ |R| ≠ 0

Tactic:
]

Goal state after:
case inr.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
hR : R ≠ 0
⊢ |R| ≠ 0
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case inr.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
hR : R ≠ 0
⊢ ¬R = 0

Tactic:
]

Goal state after:
case inr.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
hR : R ≠ 0
⊢ ¬R = 0
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

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

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
⊢ ((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: 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:
]

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.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 < δ₁
hδ₁ : ∀ x_1 ∈ closedBall x δ₁ ∩ Box.Icc I, f x_1 ∈ closedBall (f x) (ε / 2 / 2)
δ : ℝ
hδ : δ ∈ Set.Ioc 0 δ₁
y₁ : Fin (n + 1) → ℝ
hy₁ : y₁ ∈ closedBall x δ ∩ Box.Icc I
y₂ : Fin (n + 1) → ℝ
hy₂ : y₂ ∈ closedBall x δ ∩ Box.Icc I
this : closedBall x δ ∩ Box.Icc I ⊆ closedBall x δ₁ ∩ Box.Icc I
⊢ dist (f y₁) (f y₂) ≤ ε / 2

Tactic:
]

Goal state after:
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 < δ₁
hδ₁ : ∀ x_1 ∈ closedBall x δ₁ ∩ Box.Icc I, f x_1 ∈ closedBall (f x) (ε / 2 / 2)
δ : ℝ
hδ : δ ∈ Set.Ioc 0 δ₁
y₁ : Fin (n + 1) → ℝ
hy₁ : y₁ ∈ closedBall x δ ∩ Box.Icc I
y₂ : Fin (n + 1) → ℝ
hy₂ : y₂ ∈ closedBall x δ ∩ Box.Icc I
this : closedBall x δ ∩ Box.Icc I ⊆ closedBall x δ₁ ∩ Box.Icc I
⊢ dist (f y₁) (f y₂) ≤ ε / 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 μ
f g : α × β → E
F : E → ℝ≥0∞
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
⊢ ∫⁻ (x : α), F (∫ (y : β), f (x, y) - g (x, y) ∂ν) ∂μ =
    ∫⁻ (x : α), F (∫ (y : β), f (x, y) ∂ν - ∫ (y : β), g (x, y) ∂ν) ∂μ

Tactic:
by
  refine lintegral_congr_ae ?_
  filter_upwards [hf.prod_right_ae, hg.prod_right_ae] with _ h2f h2g
  simp [integral_sub h2f h2g]

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 this : ↑R ^ n ≠ 0
⊢ (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R) θ)‖ ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R) θ)‖

Tactic:
]

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 μ
⊢ ∀ (x : ↥(Lp E 1 (μ.prod ν))), ContinuousAt (fun f ↦ ∫ (x : α), ∫ (y : β), ↑↑f (x, y) ∂ν ∂μ) x

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 μ
⊢ ∀ (x : ↥(Lp E 1 (μ.prod ν))), ContinuousAt (fun f ↦ ∫ (x : α), ∫ (y : β), ↑↑f (x, y) ∂ν ∂μ) x
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:
have : ContinuousWithinAt (fun δ : ℝ => (2 * δ) ^ (n + 1) * ‖f' x (Pi.single i 1)‖)
            (Ioi 0) 0 := ((continuousWithinAt_id.const_mul _).pow _).mul_const _

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
this : ContinuousWithinAt (fun δ ↦ (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖) (Set.Ioi 0) 0
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0, (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 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:
· exact fun i => ∫⁻ x, ∫⁻ y, ‖i (x, y) - g (x, y)‖ₑ ∂ν ∂μ

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) - ↑↑g (x, y)‖ₑ ∂ν ∂μ) (𝓝 g) (𝓝 0)

α : 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.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 ν))
this : ∀ (i : ↥(Lp E 1 (μ.prod ν))), Measurable fun z ↦ ‖↑↑i z - ↑↑g z‖ₑ
⊢ Tendsto (fun i ↦ i) (𝓝 g) (𝓝 g)

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 ν))
this : ∀ (i : ↥(Lp E 1 (μ.prod ν))), Measurable fun z ↦ ‖↑↑i z - ↑↑g z‖ₑ
⊢ Tendsto (fun i ↦ i) (𝓝 g) (𝓝 g)
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 (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s < ∞
⊢ (∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ).toReal • c = (∫⁻ (a : α), ν (Prod.mk a ⁻¹' s) ∂μ).toReal • c

Tactic:
]

Goal state after:
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
⊢ 0 = 0

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 ∈ sphere c R, (z - c)⁻¹ ^ n * (z - c)⁻¹ = (z - c) ^ (-↑n - 1)

Tactic:
]

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 ∈ sphere c R, (z - c)⁻¹ ^ n * (z - c)⁻¹ = (z - c) ^ (-↑n - 1)
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:
]

Goal state after: