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

Goal state before:
pp: X : Type u_1
E : Type u_3
Fₗ : Type u_5
inst✝⁹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup Fₗ
inst✝⁴ : NormedSpace 𝕜 Fₗ
inst✝³ : NormedSpace ℝ Fₗ
inst✝² : CompleteSpace Fₗ
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
L : E →L[𝕜] Fₗ
K : ℝ≥0
hL : AntilipschitzWith K ⇑L
φ : X → E
h : ¬Integrable φ μ
⊢ ¬Integrable (fun x ↦ L (φ x)) μ

Tactic:
rwa [← Function.comp_def,
      LipschitzWith.integrable_comp_iff_of_antilipschitz L.lipschitz hL L.map_zero]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun e ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
e : ℕ
⊢ ∀ (p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e

Tactic:
p

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun e ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
e p : ℕ
⊢ n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case refine_1
α : Type u_1
E : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun a ↦ ‖f a‖
h_int_eq : (fun i ↦ ∫ (a : α) in s i, f a ∂μ) = fun i ↦ ∫ (a : α), (s i).indicator f a ∂μ
⊢ ∀ (n : ℕ), AEStronglyMeasurable ((s n).indicator f) μ

Tactic:
intro n

Goal state after:
case refine_1
α : Type u_1
E : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun a ↦ ‖f a‖
h_int_eq : (fun i ↦ ∫ (a : α) in s i, f a ∂μ) = fun i ↦ ∫ (a : α), (s i).indicator f a ∂μ
n : ℕ
⊢ AEStronglyMeasurable ((s n).indicator f) μ
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case inr.h_lim
ι : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
l : Filter ι
inst✝¹ : l.IsCountablyGenerated
F : ι → ℝ → E
inst✝ : IsLocallyFiniteMeasure μ
hF : ∀ᶠ (i : ι) in l, ContinuousOn (F i) [[a, b]]
h_lim : TendstoUniformlyOn F f l [[a, b]]
hl : l.NeBot
C : ℝ
hC : C ∈ upperBounds ((fun x ↦ ‖f x‖) '' [[a, b]])
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → Tendsto (fun n ↦ F n x) l (𝓝 (f x))

Tactic:
case h_lim =>
    exact .of_forall fun x hx ↦ h_lim.tendsto_at <| uIoc_subset_uIcc hx

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
inst✝³ : NormedAddCommGroup E
a b : ℝ
μ : Measure ℝ
f : ℝ → 𝕜
g : ℝ → E
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
hg : IntervalIntegrable g μ a b
hf : ContinuousOn f [[a, b]]
⊢ IntervalIntegrable (fun x ↦ f x • g x) μ a b

Tactic:
rw [intervalIntegrable_iff] at hg ⊢
  exact hg.continuousOn_smul_of_subset hf isCompact_uIcc measurableSet_Ioc Ioc_subset_Icc_self

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

Goal state before:
pp: case e'_7
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntegrableOn f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding fun x ↦ x * c⁻¹
⊢ (fun x ↦ x * c⁻¹) ⁻¹' [[a / c, b / c]] = [[a, b]]

Tactic:
rw [preimage_mul_const_uIcc (inv_ne_zero hc)]

Goal state after:
case e'_7
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntegrableOn f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding fun x ↦ x * c⁻¹
⊢ [[a / c / c⁻¹, b / c / c⁻¹]] = [[a, b]]
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: a b : ℝ
μ : Measure ℝ
𝕜 : Type u_8
inst✝ : RCLike 𝕜
r : 𝕜
f : ℝ → 𝕜
⊢ ∫ (x : ℝ) in a..b, f x * r ∂μ = (∫ (x : ℝ) in a..b, f x ∂μ) * r

Tactic:
by
  simpa only [mul_comm r] using integral_const_mul r f

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

Goal state before:
pp: g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ico a b, g' x ≤ φ x
ε : ℝ
εpos : 0 < ε
G' : ℝ → EReal
f_lt_G' : ∀ (x : ℝ), ↑(φ x) < G' x
G'cont : LowerSemicontinuous G'
G'int : Integrable (fun x ↦ (G' x).toReal) (volume.restrict (Icc a b))
G'lt_top : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), G' x < ⊤
hG' : ∫ (x : ℝ) in Icc a b, (G' x).toReal < (∫ (x : ℝ) in Icc a b, φ x) + ε
s : Set ℝ := {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Icc a b
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : ↑(g' t) < ↑y
y_lt_G' : ↑y < G' t
I1 : ∀ᶠ (u : ℝ) in 𝓝[>] t, (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
I2 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ (u - t) * y
u : ℝ
hu1 : (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
⊢ g u - g t ≤ (u - t) * y → g u - g t ≤ ∫ (w : ℝ) in t..u, (G' w).toReal

Tactic:
hu2

Goal state after:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ico a b, g' x ≤ φ x
ε : ℝ
εpos : 0 < ε
G' : ℝ → EReal
f_lt_G' : ∀ (x : ℝ), ↑(φ x) < G' x
G'cont : LowerSemicontinuous G'
G'int : Integrable (fun x ↦ (G' x).toReal) (volume.restrict (Icc a b))
G'lt_top : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), G' x < ⊤
hG' : ∫ (x : ℝ) in Icc a b, (G' x).toReal < (∫ (x : ℝ) in Icc a b, φ x) + ε
s : Set ℝ := {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Icc a b
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : ↑(g' t) < ↑y
y_lt_G' : ↑y < G' t
I1 : ∀ᶠ (u : ℝ) in 𝓝[>] t, (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
I2 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ (u - t) * y
u : ℝ
hu1 : (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
hu2 : g u - g t ≤ (u - t) * y
⊢ g u - g t ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case inl
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ

Tactic:
rw [integral_of_le hab, ← integral_indicator measurableSet_Ioc, indicator_eq_self.2 h]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Ring α
inst✝³ : LinearOrder α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
x : α
⊢ ↑(⌊x⌋ + 1) - 1 ≤ x

Tactic:
by rw [cast_add, cast_one, add_sub_cancel_right]; exact floor_le _

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

Goal state before:
pp: c : ℂ
R : ℝ
⊢ circleMap c R '' Ioc 0 (2 * π) = range (circleMap c R)

Tactic:
← (periodic_circleMap c R).image_Ioc Real.two_pi_pos 0,

Goal state after:
c : ℂ
R : ℝ
⊢ circleMap c R '' Ioc 0 (2 * π) = circleMap c R '' Ioc 0 (0 + 2 * π)
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case hF.refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst✝ : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : TendstoUniformlyOn f g l (sphere c R)
i : ι
hi : ContinuousOn (f i) (sphere c R)
⊢ ContinuousOn (circleMap c R) [[0, 2 * π]]

pp: case hF.refine_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst✝ : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : TendstoUniformlyOn f g l (sphere c R)
i : ι
hi : ContinuousOn (f i) (sphere c R)
⊢ MapsTo (circleMap c R) [[0, 2 * π]] (sphere c R)

Tactic:
· fun_prop

Goal state after:
case hF.refine_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst✝ : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : TendstoUniformlyOn f g l (sphere c R)
i : ι
hi : ContinuousOn (f i) (sphere c R)
⊢ MapsTo (circleMap c R) [[0, 2 * π]] (sphere c R)
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
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

Tactic:
refine this.eventually (ge_mem_nhds ?_)

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
⊢ (fun δ ↦ (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖) 0 < ε / 2
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:
· fun_prop

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

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.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:
· fun_prop

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.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:
· fun_prop

Goal state after:
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
i_f : Integrable f (μ.prod ν)
i_g : Integrable g (μ.prod ν)
hf : ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
hg : ∫ (z : α × β), g z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ
⊢ ∫ (a : α × β), f a ∂μ.prod ν + ∫ (a : α × β), g a ∂μ.prod ν = ∫ (x : α), ∫ (y : β), (f + g) (x, y) ∂ν ∂μ

Tactic:
integral_integral_add' i_f i_g,

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
i_f : Integrable f (μ.prod ν)
i_g : Integrable g (μ.prod ν)
hf : ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
hg : ∫ (z : α × β), g z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ
⊢ ∫ (a : α × β), f a ∂μ.prod ν + ∫ (a : α × β), g a ∂μ.prod ν =
    ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ + ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: case inr
α : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
a b : ℝ
f : ℝ → α → E
hab : b ≤ a
h_int : Integrable (uncurry f) ((volume.restrict (Ioc b a)).prod μ)
⊢ -∫ (x : ℝ) in Ioc b a, ∫ (y : α), f x y ∂μ ∂volume = ∫ (y : α), -∫ (x : ℝ) in Ioc b a, f x y ∂volume ∂μ

Tactic:
rw [integral_integral_swap h_int, integral_neg]

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 a..b, ∫ (y : ℝ) in c..d, F x y = ∫ (y : ℝ) in c..d, ∫ (x : ℝ) in a..b, F x y

Tactic:
rw [intervalIntegral.intervalIntegral_eq_integral_uIoc, ← intervalIntegral_integral_swap,
    ← intervalIntegral.integral_smul]
  · simp_rw [intervalIntegral.intervalIntegral_eq_integral_uIoc]
  · rwa [← integrable_swap_iff, Measure.prod_restrict, ← Measure.volume_eq_prod, ← IntegrableOn]

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case hf
F : Type u_1
inst✝ : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : (map (algebraMap F q₁.SplittingField) p₁).Splits
h₂ : (map (algebraMap F q₂.SplittingField) p₂).Splits
⊢ (map (algebraMap F (q₁ * q₂).SplittingField) p₁).Splits

pp: case hg
F : Type u_1
inst✝ : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : (map (algebraMap F q₁.SplittingField) p₁).Splits
h₂ : (map (algebraMap F q₂.SplittingField) p₂).Splits
⊢ (map (algebraMap F (q₁ * q₂).SplittingField) p₂).Splits

Tactic:
· rw [←
      (SplittingField.lift q₁
          ((SplittingField.splits _).of_dvd (map_ne_zero (mul_ne_zero hq₁ hq₂))
             ((map_dvd_map' _).mpr (dvd_mul_right q₁ q₂)))).comp_algebraMap, ← map_map]
    exact h₁.map _

Goal state after:
case hg
F : Type u_1
inst✝ : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : (map (algebraMap F q₁.SplittingField) p₁).Splits
h₂ : (map (algebraMap F q₂.SplittingField) p₂).Splits
⊢ (map (algebraMap F (q₁ * q₂).SplittingField) p₂).Splits
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

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

Tactic:
simpa only [Set.mem_preimage, eL.apply_symm_apply, ← pi_univ_Icc,
          interior_pi_set (@finite_univ (Fin _) _), interior_Icc] using hx.1

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

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

Tactic:
refine integral_divergence_of_hasFDerivAt_off_countable' (eL a) (eL b)
        ((he_ord _ _).2 hle) (fun i x => f i (eL.symm x))
        (fun i x => f' i (eL.symm x) ∘L (eL.symm : ℝⁿ⁺¹ →L[ℝ] F)) (eL.symm ⁻¹' s)
        (hs.preimage eL.symm.injective) ?_ ?_ ?_
      · exact fun i => (Hc i).comp eL.symm.continuousOn hIcc'.subset
      · refine fun x hx i => (Hd (eL.symm x) ⟨?_, hx.2⟩ i).comp x eL.symm.hasFDerivAt
        rw [← hIcc]
        refine preimage_interior_subset_interior_preimage eL.continuous ?_
        simpa only [Set.mem_preimage, eL.apply_symm_apply, ← pi_univ_Icc,
          interior_pi_set (@finite_univ (Fin _) _), interior_Icc] using hx.1
      · rw [← he_vol.integrableOn_comp_preimage he_emb, hIcc]
        simp [← hDF, Function.comp_def, Hi]

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

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ Set.Ioo a b \ s, HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
e : ℝ ≃L[ℝ] Fin 1 → ℝ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm
F' : ℝ → ℝ →L[ℝ] E := fun x ↦ smulRight 1 (f' x)
⊢ ∑ i,
      ((∫ (x : Fin 0 → ℝ) in Set.Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove), f (e.symm (i.insertNth (e b i) x))) -
        ∫ (x : Fin 0 → ℝ) in Set.Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove), f (e.symm (i.insertNth (e a i) x))) =
    f b - f a

Tactic:
by
      simp [e, Subsingleton.elim (const (Fin 0) _) isEmptyElim, volume_pi,
        Measure.pi_of_empty fun _ : Fin 0 ↦ _]

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

Goal state before:
pp: F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
hB : B < 0
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
⊢ p.natDegree = 0

Tactic:
by
    contrapose! hB
    rw [← h1.natDegree_map f, Splits.natDegree_eq_card_roots h2] at hB
    obtain ⟨z, hz⟩ := card_pos_iff_exists_mem.mp (zero_lt_iff.mpr hB)
    exact le_trans (norm_nonneg _) (h3 z hz)

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

Goal state before:
pp: case refine_5
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a b : ℝ × ℝ
hle : a ≤ b
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f (Set.Icc a b)
Hcg : ContinuousOn g (Set.Icc a b)
Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm
x : ℝ × ℝ
⊢ (f' x) (1, 0) + (g' x) (0, 1) = ∑ i, (![f', g'] i x) (e.symm (Pi.single i 1))

Tactic:
Fin.sum_univ_two

Goal state after:
case refine_5
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a b : ℝ × ℝ
hle : a ≤ b
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f (Set.Icc a b)
Hcg : ContinuousOn g (Set.Icc a b)
Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm
x : ℝ × ℝ
⊢ (f' x) (1, 0) + (g' x) (0, 1) = (![f', g'] 0 x) (e.symm (Pi.single 0 1)) + (![f', g'] 1 x) (e.symm (Pi.single 1 1))