mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition n
o : Option (Fin c.length)
i : Fin c.length
⊢ (fun c ↦ if h : range (c.emb 0) = {0} then ⟨c.eraseLeft h, none⟩ else ⟨c.eraseMiddle h, some (c.index 0)⟩)
      ((fun c ↦ c.fst.extend c.snd) ⟨c, some i⟩) =
    ⟨c, some i⟩

Tactic:
simp only [extend, range_emb_extendMiddle_ne_singleton_zero, ↓reduceDIte,
        Sigma.mk.inj_iff, heq_eq_eq, and_true, eraseMiddle,
        index_extendMiddle_zero]

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition n
o : Option (Fin c.length)
i : Fin c.length
⊢ { length := (c.extendMiddle i).length,
      partSize :=
        update (c.extendMiddle i).partSize ((c.extendMiddle i).index 0)
          ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1),
      partSize_pos := ⋯,
      emb := fun i_1 j ↦
        if h : i_1 = i then ((c.extendMiddle i).emb i_1 (Fin.cast ⋯ j.succ)).pred ⋯
        else ((c.extendMiddle i).emb i_1 (Fin.cast ⋯ j)).pred ⋯,
      emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ } =
    c
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝔸 : Type u_1
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_3
s : Finset ι
f : ι → 𝔸
h : (↑s).Pairwise (Commute on f)
⊢ exp (∑ i ∈ s, f i) = s.noncommProd (fun i ↦ exp (f i)) ⋯

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert a s ha ih =>
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ ha, Finset.sum_insert ha, exp_add_of_commute,
      ih (h.mono <| Finset.subset_insert _ _)]
    refine Commute.sum_right _ _ _ fun i hi => ?_
    exact h.of_refl (Finset.mem_insert_self _ _) (Finset.mem_insert_of_mem hi)

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: case h.refine_3
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n✝ : ℕ∞ω
inst✝ : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑f.symm a)
n : ℕ
IH : ContDiffAt 𝕜 (↑↑n) (↑f) (↑f.symm a) → ContDiffAt 𝕜 (↑↑n) (↑f.symm) a
hf : ContDiffAt 𝕜 (↑↑n.succ) (↑f) (↑f.symm a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑f.symm a)
u : Set E
hu : u ∈ 𝓝 (↑f.symm a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑f.symm a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑f.symm a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
htf : ↑f.symm a ∈ t
x : F
hx : x ∈ f.target ∩ ↑f.symm ⁻¹' t
hxu : ↑f.symm x ∈ u
e : E ≃L[𝕜] F
he : ↑e = f' (↑f.symm x)
h_deriv : HasFDerivAt (↑f) (↑e) (↑f.symm x)
⊢ HasFDerivAt (↑f.symm) ((inverse ∘ f' ∘ ↑f.symm) x) x

Tactic:
convert! f.hasFDerivAt_symm hx.1 h_deriv

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n✝ : ℕ∞ω
inst✝ : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑f.symm a)
n : ℕ
IH : ContDiffAt 𝕜 (↑↑n) (↑f) (↑f.symm a) → ContDiffAt 𝕜 (↑↑n) (↑f.symm) a
hf : ContDiffAt 𝕜 (↑↑n.succ) (↑f) (↑f.symm a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑f.symm a)
u : Set E
hu : u ∈ 𝓝 (↑f.symm a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑f.symm a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑f.symm a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
htf : ↑f.symm a ∈ t
x : F
hx : x ∈ f.target ∩ ↑f.symm ⁻¹' t
hxu : ↑f.symm x ∈ u
e : E ≃L[𝕜] F
he : ↑e = f' (↑f.symm x)
h_deriv : HasFDerivAt (↑f) (↑e) (↑f.symm x)
⊢ (inverse ∘ f' ∘ ↑f.symm) x = ↑e.symm
Module: Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus

Goal state before:
pp: X : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure X
l : Filter X
inst✝ : l.IsMeasurablyGenerated
f : X → E
b : E
h : Tendsto f (l ⊓ ae μ) (𝓝 b)
hfm✝ : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
s✝ : ι → Set X
li : Filter ι
hs : Tendsto s✝ li l.smallSets
m : ι → ℝ
hsμ : (fun i ↦ μ.real (s✝ i)) =ᶠ[li] m
ε : ℝ
ε₀ : 0 < ε
this : ∀ᶠ (s : Set X) in l.smallSets, ∀ᵐ (x : X) ∂μ, x ∈ s → f x ∈ closedBall b ε
s : Set X
hμs : μ s < ⊤
h_integrable : IntegrableOn f s μ
hfm : AEStronglyMeasurable f (μ.restrict s)
h_norm : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x - b‖ ≤ ε
⊢ ‖∫ (x : X) in s, f x ∂μ - μ.real s • b‖ ≤ ε * ‖μ.real s‖

Tactic:
rw [← setIntegral_const,
    ← integral_sub h_integrable (integrableOn_const hμs.ne),
    Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]

Goal state after:
X : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure X
l : Filter X
inst✝ : l.IsMeasurablyGenerated
f : X → E
b : E
h : Tendsto f (l ⊓ ae μ) (𝓝 b)
hfm✝ : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
s✝ : ι → Set X
li : Filter ι
hs : Tendsto s✝ li l.smallSets
m : ι → ℝ
hsμ : (fun i ↦ μ.real (s✝ i)) =ᶠ[li] m
ε : ℝ
ε₀ : 0 < ε
this : ∀ᶠ (s : Set X) in l.smallSets, ∀ᵐ (x : X) ∂μ, x ∈ s → f x ∈ closedBall b ε
s : Set X
hμs : μ s < ⊤
h_integrable : IntegrableOn f s μ
hfm : AEStronglyMeasurable f (μ.restrict s)
h_norm : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x - b‖ ≤ ε
⊢ ‖∫ (a : X) in s, f a - b ∂μ‖ ≤ ε * μ.real s
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
hx : x = 0
⊢ deriv log x = x⁻¹

Tactic:
rw [deriv_zero_of_not_differentiableAt (differentiableAt_log_iff.not_left.2 hx), hx, inv_zero]

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: case smul_mem'
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
c : 𝕜
c_pos : 0 < c
c' : 𝕜
c'_pos : 0 < c'
x : M
hx : x ∈ s
⊢ ∃ i, ∃ (_ : 0 < i), ∃ y ∈ s, i • y = c • c' • x

Tactic:
exact ⟨c * c', mul_pos c_pos c'_pos, x, hx, (smul_smul _ _ _).symm⟩

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: case refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
H : (f.supSpanSingleton y (-c) hy).domain ≤ f.domain
⊢ False

Tactic:
LinearPMap.domain_supSpanSingleton,

Goal state after:
case refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
H : f.domain ⊔ ℝ ∙ y ≤ f.domain
⊢ False
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : μ s < ∞
this : 0 < ε / ↑c
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : μ s < μ F + ε / ↑c
⊢ ∃ g,
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0)) x) ∧
      UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε

Tactic:
refine
      ⟨Set.indicator F fun _ => c, fun x => ?_, F_closed.upperSemicontinuous_indicator zero_le,
        ?_⟩

Goal state after:
case neg.refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : μ s < ∞
this : 0 < ε / ↑c
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : μ s < μ F + ε / ↑c
x : α
⊢ F.indicator (fun x ↦ c) x ≤ (piecewise s hs (const α c) (const α 0)) x

case neg.refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : μ s < ∞
this : 0 < ε / ↑c
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : μ s < μ F + ε / ↑c
⊢ ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ ≤ ∫⁻ (x : α), ↑(F.indicator (fun x ↦ c) x) ∂μ + ε
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0
fint : Integrable (fun x ↦ ↑(f x)) μ
ε : ℝ≥0
εpos : 0 < ↑ε
If : ∫⁻ (x : α), ↑(f x) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ↑ε
Ig : ∫⁻ (x : α), ↑(g x) ∂μ < ∞
⊢ ∫ (x : α), ↑(f x) ∂μ - ↑ε ≤ ∫ (x : α), ↑(g x) ∂μ

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]
    · rw [sub_le_iff_le_add]
      convert! ENNReal.toReal_mono _ gint
      · simp
      · rw [ENNReal.toReal_add Ig.ne ENNReal.coe_ne_top]; simp
      · simpa using Ig.ne
    · apply Filter.Eventually.of_forall; simp
    · exact gcont.measurable.coe_nnreal_real.aemeasurable.aestronglyMeasurable
    · apply Filter.Eventually.of_forall; simp
    · exact fint.aestronglyMeasurable

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')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
e : ℕ
he : (1 / 2) ^ e < ε / 16
y : ℝ
hy : y ∈ Icc x (x + (1 / 2) ^ (n e + 1))
xy : x < y
yzero : 0 < y - x
y_le : y - x ≤ (1 / 2) ^ (n e + 1)
yone : y - x ≤ 1
k : ℕ
k_gt : n e < k
m : ℕ := k - 1
h'k : y - x ≤ (1 / 2) ^ (m + 1)
hk : (1 / 2) ^ (m + 1 + 1) < y - x
m_ge : n e ≤ m
km : k = m + 1
⊢ ‖f y - f x - (y - x) • L e (n e) m‖ ≤ (1 / 2) ^ e * (1 / 2) ^ m

Tactic:
apply le_of_mem_A (hn e (n e) m le_rfl m_ge).2.2
          · simp only [one_div, inv_pow, left_mem_Icc, le_add_iff_nonneg_right]
            positivity
          · simp only [pow_add, tsub_le_iff_left] at h'k
            simpa only [hy.1, mem_Icc, true_and, one_div, pow_one] using! h'k

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

Goal state before:
pp: case pos.h_bound
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum : Summable fun i ↦ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f i)‖
hE : CompleteSpace E
⊢ ∀ (n : ι),
    ∀ᵐ (t : ℝ), t ∈ Ι a b → ‖(f n) t‖ ≤ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f n)‖

pp: case pos.bound_summable
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum : Summable fun i ↦ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f i)‖
hE : CompleteSpace E
⊢ ∀ᵐ (t : ℝ), t ∈ Ι a b → Summable fun n ↦ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f n)‖

pp: case pos.bound_integrable
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum : Summable fun i ↦ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f i)‖
hE : CompleteSpace E
⊢ IntervalIntegrable (fun t ↦ ∑' (n : ι), ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f n)‖)
    volume a b

pp: case pos.h_lim
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum : Summable fun i ↦ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f i)‖
hE : CompleteSpace E
⊢ ∀ᵐ (t : ℝ), t ∈ Ι a b → HasSum (fun n ↦ (f n) t) (∑' (i : ι), (f i) t)

Tactic:
· intro i; filter_upwards with x hx
    apply ContinuousMap.norm_coe_le_norm ((f i).restrict _) ⟨x, _⟩
    exact ⟨hx.1.le, hx.2⟩

Goal state after:
case pos.bound_summable
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum : Summable fun i ↦ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f i)‖
hE : CompleteSpace E
⊢ ∀ᵐ (t : ℝ), t ∈ Ι a b → Summable fun n ↦ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f n)‖

case pos.bound_integrable
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum : Summable fun i ↦ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f i)‖
hE : CompleteSpace E
⊢ IntervalIntegrable (fun t ↦ ∑' (n : ι), ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f n)‖)
    volume a b

case pos.h_lim
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum : Summable fun i ↦ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f i)‖
hE : CompleteSpace E
⊢ ∀ᵐ (t : ℝ), t ∈ Ι a b → HasSum (fun n ↦ (f n) t) (∑' (i : ι), (f i) t)
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✝ : FirstCountableTopology X
F : X → ℝ → E
bound : ℝ → ℝ
a b a₀ b₀ : ℝ
x₀ : X
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x ↦ F x t) x₀
ha₀ : a₀ ∈ Ioo a b
hb₀ : b₀ ∈ Ioo a b
hμb₀ : μ {b₀} = 0
hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b
Ioo_nhds : Ioo a b ∈ 𝓝 b₀
⊢ ContinuousAt (fun p ↦ ∫ (t : ℝ) in a₀..p.2, F p.1 t ∂μ) (x₀, b₀)

Tactic:
have Icc_nhds : Icc a b ∈ 𝓝 b₀ := Icc_mem_nhds hb₀.1 hb₀.2

Goal state after:
E : Type u_1
X : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : TopologicalSpace X
μ : Measure ℝ
inst✝ : FirstCountableTopology X
F : X → ℝ → E
bound : ℝ → ℝ
a b a₀ b₀ : ℝ
x₀ : X
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x ↦ F x t) x₀
ha₀ : a₀ ∈ Ioo a b
hb₀ : b₀ ∈ Ioo a b
hμb₀ : μ {b₀} = 0
hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b
Ioo_nhds : Ioo a b ∈ 𝓝 b₀
Icc_nhds : Icc a b ∈ 𝓝 b₀
⊢ ContinuousAt (fun p ↦ ∫ (t : ℝ) in a₀..p.2, F p.1 t ∂μ) (x₀, b₀)
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : LocallyCompactSpace E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
α : Type u_4
inst✝⁴ : TopologicalSpace α
f : α → E → F
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
⊢ {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}

Tactic:
simp [← differentiable_set_eq_D K hK]

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

Goal state before:
pp: case hle
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : ∃ c ∈ Icc a b, f c < g c
⊢ f ≤ᵐ[volume.restrict (Ioc a b)] g

pp: case hlt
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : ∃ c ∈ Icc a b, f c < g c
⊢ (volume.restrict (Ioc a b)) {x | f x < g x} ≠ 0

Tactic:
· simpa only [measurableSet_Ioc, ae_restrict_eq]
      using! (ae_restrict_mem measurableSet_Ioc).mono hle

Goal state after:
case hlt
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : ∃ c ∈ Icc a b, f c < g c
⊢ (volume.restrict (Ioc a b)) {x | f x < g x} ≠ 0
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this : ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun x ↦ ↑↑x) volume = ∫⁻ (a : ↑(Ioc t (t + T))), f ↑↑a
⊢ ∫⁻ (a : ℝ) in Ioc t (t + T), f ↑a =
    ∫⁻ (b : AddCircle T), f b ∂Measure.map QuotientAddGroup.mk (volume.restrict (Ioc t (t + T)))

Tactic:
convert! this.symm using 1

Goal state after:
case e'_2
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this : ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun x ↦ ↑↑x) volume = ∫⁻ (a : ↑(Ioc t (t + T))), f ↑↑a
⊢ ∫⁻ (a : ℝ) in Ioc t (t + T), f ↑a = ∫⁻ (a : ↑(Ioc t (t + T))), f ↑↑a

case e'_3
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this : ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun x ↦ ↑↑x) volume = ∫⁻ (a : ↑(Ioc t (t + T))), f ↑↑a
⊢ ∫⁻ (b : AddCircle T), f b ∂Measure.map QuotientAddGroup.mk (volume.restrict (Ioc t (t + T))) =
    ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun x ↦ ↑↑x) volume
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
⊢ ∫⁻ (a : ℝ) in Ioc t (t + T), f ↑a = ∫⁻ (b : AddCircle T), f b

Tactic:
by
  have m : MeasurableSet (Ioc t (t + T)) := measurableSet_Ioc
  have := lintegral_map_equiv (μ := volume) f (measurableEquivIoc T t).symm
  simp only [measurableEquivIoc, equivIoc, QuotientAddGroup.equivIocMod, MeasurableEquiv.symm_mk,
    MeasurableEquiv.coe_mk, Equiv.coe_fn_symm_mk] at this
  rw [← (AddCircle.measurePreserving_mk T t).map_eq]
  convert! this.symm using 1
  · rw [← map_comap_subtype_coe m _]
    exact MeasurableEmbedding.lintegral_map (MeasurableEmbedding.subtype_coe m) _
  · congr 1
    have : ((↑) : Ioc t (t + T) → AddCircle T) = ((↑) : ℝ → AddCircle T) ∘ ((↑) : _ → ℝ) := by
      ext1 x; rfl
    simp_rw [this]
    rw [← map_map AddCircle.measurable_mk' measurable_subtype_coe, ← map_comap_subtype_coe m]
    rfl

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

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

Tactic:
← range_circleMap,

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

Goal state before:
pp: case h₂f
c : ℂ
R : ℝ
hR : R ≠ 0
s : Set ℂ
hs : s ∈ codiscreteWithin (sphere c |R|)
⊢ ∀ x ∈ univ, ¬EventuallyConst (circleMap c R) (𝓝 x)

pp: case hs
c : ℂ
R : ℝ
hR : R ≠ 0
s : Set ℂ
hs : s ∈ codiscreteWithin (sphere c |R|)
⊢ s ∈ codiscreteWithin (circleMap c R '' univ)

Tactic:
· intro x hx
    by_contra hCon
    obtain ⟨a, ha⟩ := eventuallyConst_iff_exists_eventuallyEq.1 hCon
    have := ha.deriv.eq_of_nhds
    simp [hR] at this

Goal state after:
case hs
c : ℂ
R : ℝ
hR : R ≠ 0
s : Set ℂ
hs : s ∈ codiscreteWithin (sphere c |R|)
⊢ s ∈ codiscreteWithin (circleMap c R '' univ)
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_cases h₀ : R = 0

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

case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
h₀ : ¬R = 0
⊢ CircleIntegrable f c R ↔ IntervalIntegrable (fun θ ↦ deriv (circleMap c R) θ • f (circleMap c R θ)) volume 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 ν
f : α × β → E
h1f : StronglyMeasurable f
this : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
⊢ ∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞ ↔
    (∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞) ∧ ∫⁻ (a : α), ‖∫ (y : β), ‖f (a, y)‖ ∂ν‖ₑ ∂μ < ∞

Tactic:
simp_rw [integral_eq_lintegral_of_nonneg_ae (this _)
      (h1f.norm.comp_measurable measurable_prodMk_left).aestronglyMeasurable,
    enorm_eq_ofReal toReal_nonneg, ofReal_norm]

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)‖
⊢ ∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞ ↔
    (∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞) ∧
      ∫⁻ (a : α), ENNReal.ofReal (∫⁻ (a_1 : β), ‖f (a, a_1)‖ₑ ∂ν).toReal ∂μ < ∞
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c : ℂ
R : ℝ
hR : R ≠ 0
⊢ ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ = 2 * ↑π * I

Tactic:
by
  simp [circleIntegral, ← div_eq_mul_inv, mul_div_cancel_left₀ _ (circleMap_ne_center hR)]

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 : ℝ≥0
⊢ ↑R ≤ (cauchyPowerSeries f c ↑R).radius

Tactic:
refine
    (cauchyPowerSeries f c R).le_radius_of_bound
      ((2 * π)⁻¹ * ∫ θ : ℝ in 0..2 * π, ‖f (circleMap c R θ)‖) fun n => ?_

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