mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h : |x| < 1
⊢ Tendsto (fun e ↦ ‖∑ i ∈ Finset.range e, x ^ (i + 1) / (↑i + 1) - -log (1 - x)‖) atTop (𝓝 0)

Tactic:
simp only [norm_eq_abs, sub_neg_eq_add]

Goal state after:
x : ℝ
h : |x| < 1
⊢ Tendsto (fun e ↦ |∑ i ∈ Finset.range e, x ^ (i + 1) / (↑i + 1) + log (1 - x)|) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n ↦ -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x ↦ 2 * x) = fun k ↦ 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
⊢ HasSum term (log (1 + x) - log (1 - x))

pp: x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n ↦ -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x ↦ 2 * x) = fun k ↦ 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
⊢ ∀ x ∉ Set.range fun x ↦ 2 * x, term x = 0

Tactic:
· have h₁ := (hasSum_pow_div_log_of_abs_lt_one (Eq.trans_lt (abs_neg x) h)).mul_left (-1)
    convert! h₁.add (hasSum_pow_div_log_of_abs_lt_one h) using 1
    ring_nf

Goal state after:
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n ↦ -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x ↦ 2 * x) = fun k ↦ 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
⊢ ∀ x ∉ Set.range fun x ↦ 2 * x, term x = 0
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
⊢ gauge 0 = 0

Tactic:
ext x
  rw [gauge_def']
  obtain rfl | hx := eq_or_ne x 0
  · simp only [csInf_Ioi, mem_zero, Pi.zero_apply, sep_true, smul_zero]
  · simp only [mem_zero, Pi.zero_apply, inv_eq_zero, smul_eq_zero]
    convert! Real.sInf_empty
    exact eq_empty_iff_forall_notMem.2 fun r hr => hr.2.elim (ne_of_gt hr.1) hx

Goal state after:
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:
integral_eq_lintegral_of_nonneg_ae,

Goal state after:
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) ∂μ < ∞
⊢ (∫⁻ (a : α), ENNReal.ofReal ↑(f a) ∂μ).toReal - ↑ε ≤ ∫ (x : α), ↑(g x) ∂μ

case refine_2.hf
α : 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) ∂μ < ∞
⊢ 0 ≤ᵐ[μ] fun x ↦ ↑(f x)

case refine_2.hfm
α : 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) ∂μ < ∞
⊢ AEStronglyMeasurable (fun x ↦ ↑(f x)) μ
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inr.mp
E : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
α : Type u_3
inst✝⁸ : Field α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : IsStrictOrderedModule α ℝ
inst✝³ : MulActionWithZero α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
r : ℝ
⊢ (r ∈ Ioi 0 ∧ ∃ y ∈ s, a • y = r⁻¹ • x) → ∃ y, (y ∈ Ioi 0 ∧ y⁻¹ • x ∈ s) ∧ a⁻¹ • y = r

pp: case inr.mpr
E : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
α : Type u_3
inst✝⁸ : Field α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : IsStrictOrderedModule α ℝ
inst✝³ : MulActionWithZero α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
r : ℝ
⊢ (∃ y, (y ∈ Ioi 0 ∧ y⁻¹ • x ∈ s) ∧ a⁻¹ • y = r) → r ∈ Ioi 0 ∧ ∃ y ∈ s, a • y = r⁻¹ • x

Tactic:
· rintro ⟨hr, y, hy, h⟩
    simp_rw [mem_Ioi] at hr ⊢
    refine ⟨a • r, ⟨smul_pos ha' hr, ?_⟩, inv_smul_smul₀ ha'.ne' _⟩
    rwa [smul_inv₀, smul_assoc, ← h, inv_smul_smul₀ ha'.ne']

Goal state after:
case inr.mpr
E : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
α : Type u_3
inst✝⁸ : Field α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : IsStrictOrderedModule α ℝ
inst✝³ : MulActionWithZero α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
r : ℝ
⊢ (∃ y, (y ∈ Ioi 0 ∧ y⁻¹ • x ∈ s) ∧ a⁻¹ • y = r) → r ∈ Ioi 0 ∧ ∃ y ∈ s, a • y = r⁻¹ • x
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
⊢ x ∈ {x | gauge s x < 1}

Tactic:
have H₁ : Tendsto (fun r : ℝ ↦ r⁻¹ • x) (𝓝[<] 1) (𝓝 ((1 : ℝ)⁻¹ • x)) :=
    ((tendsto_id.inv₀ one_ne_zero).smul tendsto_const_nhds).mono_left inf_le_left

Goal state after:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun r ↦ r⁻¹ • x) (𝓝[<] 1) (𝓝 (1⁻¹ • x))
⊢ x ∈ {x | gauge s x < 1}
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
⊢ ∃ f, f x₀ = 1 ∧ ∀ x ∈ s, f x < 1

Tactic:
by
  let f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (ne_of_mem_of_not_mem hs₀ hx₀).symm
  have := exists_extension_of_le_sublinear f (gauge s) (fun c hc => gauge_smul_of_nonneg hc.le)
    (gauge_add_le hs₁ <| absorbent_nhds_zero <| hs₂.mem_nhds hs₀) ?_
  · obtain ⟨φ, hφ₁, hφ₂⟩ := this
    have hφ₃ : φ x₀ = 1 := by
      rw [← f.domain.coe_mk x₀ (Submodule.mem_span_singleton_self _), hφ₁,
        LinearPMap.mkSpanSingleton'_apply_self]
    have hφ₄ : ∀ x ∈ s, φ x < 1 := fun x hx =>
      (hφ₂ x).trans_lt (gauge_lt_one_of_mem_of_isOpen hs₂ hx)
    refine ⟨⟨φ, ?_⟩, hφ₃, hφ₄⟩
    refine
      φ.continuous_of_nonzero_on_open _ (hs₂.vadd (-x₀)) (Nonempty.vadd_set ⟨0, hs₀⟩)
        (vadd_set_subset_iff.mpr fun x hx => ?_)
    change φ (-x₀ + x) ≠ 0
    rw [map_add, map_neg]
    specialize hφ₄ x hx
    linarith
  rintro ⟨x, hx⟩
  obtain ⟨y, rfl⟩ := Submodule.mem_span_singleton.1 hx
  rw [LinearPMap.mkSpanSingleton'_apply]
  simp only [mul_one, smul_eq_mul]
  obtain h | h := le_or_gt y 0
  · exact h.trans (gauge_nonneg _)
  · rw [gauge_smul_of_nonneg h.le, smul_eq_mul, RingHom.id_apply, le_mul_iff_one_le_right h]
    exact
      one_le_gauge_of_notMem (hs₁.starConvex hs₀)
        (absorbent_nhds_zero <| hs₂.mem_nhds hs₀).absorbs hx₀

Goal state after:
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr✝ : 0 ≤ r
x : E
hr : 0 < r
⊢ gauge (ball 0 r) x = ‖x‖ / r

Tactic:
← smul_unitBall_of_pos hr,

Goal state after:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr✝ : 0 ≤ r
x : E
hr : 0 < r
⊢ gauge (r • ball 0 1) x = ‖x‖ / r
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case e'_2.e'_3
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 0
⊢ {r | r ∈ Ioi 0 ∧ (r = 0 ∨ ‖x‖ = 0)} = Ioi 0

Tactic:
exact Set.ext fun r ↦ and_iff_left (.inr hx)

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝¹² : Field R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : TopologicalSpace V
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : Module R V
inst✝⁶ : SeparatingDual R V
W : Type u_3
inst✝⁵ : AddCommGroup W
inst✝⁴ : TopologicalSpace W
inst✝³ : Module R W
inst✝² : Nontrivial W
inst✝¹ : ContinuousSMul R W
inst✝ : Nontrivial V
v : V
hv : v ≠ 0
w : W
hw : w ≠ 0
ψ : StrongDual R V
hψ : ψ v ≠ 0
⊢ Nontrivial (V →L[R] W)

Tactic:
exact ⟨ψ.smulRight w, 0, DFunLike.ne_iff.mpr ⟨v, by simp_all⟩⟩

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun x ↦ (f x).toNNReal
int_fp : Integrable (fun x ↦ ↑(fp x)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ∞
gp_integrable : Integrable (fun x ↦ (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + ↑δ
fm : α → ℝ≥0 := fun x ↦ (-f x).toNNReal
int_fm : Integrable (fun x ↦ ↑(fm x)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (fun x ↦ ↑(gm x)) μ
gmint : ∫ (x : α), ↑(fm x) ∂μ - ↑δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x ↦ ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x)).toReal - (↑↑(gm x)).toReal
⊢ ∀ᵐ (x : α) ∂μ, g x < ⊤

Tactic:
filter_upwards [gp_lt_top] with ?_ hx

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun x ↦ (f x).toNNReal
int_fp : Integrable (fun x ↦ ↑(fp x)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ∞
gp_integrable : Integrable (fun x ↦ (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + ↑δ
fm : α → ℝ≥0 := fun x ↦ (-f x).toNNReal
int_fm : Integrable (fun x ↦ ↑(fm x)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (fun x ↦ ↑(gm x)) μ
gmint : ∫ (x : α), ↑(fm x) ∂μ - ↑δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x ↦ ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x)).toReal - (↑↑(gm x)).toReal
x✝ : α
hx : gp x✝ < ∞
⊢ g x✝ < ⊤
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
this✝ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖
m : ℝ
xm : m ∈ Ioi x
hm : Ico x m ⊆ {x_1 | (fun x_2 ↦ ‖f x_2 - f x - (x_2 - x) • derivWithin f (Ici x) x‖ ≤ ε / 2 * ‖x_2 - x‖) x_1}
r : ℝ
hr : r ∈ Ioo 0 (m - x)
this : r ∈ Ioc (r / 2) r
y : ℝ
hy : y ∈ Icc x (x + r)
z : ℝ
hz : z ∈ Icc x (x + r)
⊢ ε / 2 * ‖z - x‖ + ε / 2 * ‖y - x‖ ≤ ε / 2 * r + ε / 2 * r

Tactic:
by
      gcongr
      · rw [Real.norm_of_nonneg] <;> linarith [hz.1, hz.2]
      · rw [Real.norm_of_nonneg] <;> linarith [hy.1, hy.2]

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

Goal state before:
pp: case h₁.hy
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ x ∈ Icc x (x + r / 2)

Tactic:
simp [(half_pos hr).le]

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

Goal state before:
pp: case h₁.hz
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ x + r / 2 ∈ Icc x (x + r / 2)

Tactic:
simp [(half_pos hr).le]

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

Goal state before:
pp: case h₂.hy
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ x ∈ Icc x (x + r / 2)

Tactic:
simp [(half_pos hr).le]

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

Goal state before:
pp: case h₂.hz
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ x + r / 2 ∈ Icc x (x + r / 2)

Tactic:
simp [(half_pos hr).le]

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

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : ¬CompleteSpace E
⊢ HasSum (fun x ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)

pp: case pos
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
⊢ HasSum (fun x ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)

Tactic:
· simp [integral, hE, hasSum_zero]

Goal state after:
case pos
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
⊢ HasSum (fun x ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
μ : Measure X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : X → ℝ≥0
s : Set X
hf : AEMeasurable f (μ.restrict s)
g : X → E
⊢ (∫ (x : X) in s, g x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X) in s, f x • g x ∂μ

Tactic:
by
  rw [restrict_withDensity' s, integral_withDensity_eq_integral_smul₀ hf]

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

Goal state before:
pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b ↦ ∫ (x : ℝ) in b₁..b₂, {x | x ≤ b}.indicator f x ∂μ
⊢ ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, AEStronglyMeasurable ({x_1 | x_1 ≤ x}.indicator f) (μ.restrict (Ι b₁ b₂))

Tactic:
filter_upwards [self_mem_nhdsWithin]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b ↦ ∫ (x : ℝ) in b₁..b₂, {x | x ≤ b}.indicator f x ∂μ
⊢ ∀ a ∈ Icc b₁ b₂, AEStronglyMeasurable ({x | x ≤ a}.indicator f) (μ.restrict (Ι b₁ b₂))
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
h_int : IntegrableOn f (Icc a b) μ
h : ¬a ≤ b
⊢ ContinuousOn (fun x ↦ ∫ (t : ℝ) in Ioc a x, f t ∂μ) ∅

Tactic:
exact continuousOn_empty _

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : FloorRing α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsStrictOrderedRing α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
t : α
ht : ¬∃ n, t = ↑n
⊢ ContinuousAt (uncurry f ∘ Prod.map id fract) (s, t)

Tactic:
· replace ht : t ≠ ⌊t⌋ := fun ht' => ht ⟨_, ht'⟩
    refine (h.continuousAt ?_).comp (continuousAt_id.prodMap (continuousAt_fract ht))
    exact prod_mem_nhds univ_mem (Icc_mem_nhds (fract_pos.2 ht) (fract_lt_one _))

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

Goal state before:
pp: E✝ : Type u_1
inst✝¹ : NormedAddCommGroup E✝
f✝ : ℝ → E✝
T✝ : ℝ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT✝ : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ ↑n₁
⊢ IntervalIntegrable f volume a₁ a₂

Tactic:
obtain ⟨n₂, hn₂⟩ := exists_nat_ge ((max a₁ a₂ - t) / T)

Goal state after:
E✝ : Type u_1
inst✝¹ : NormedAddCommGroup E✝
f✝ : ℝ → E✝
T✝ : ℝ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT✝ : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ ↑n₂
⊢ IntervalIntegrable f volume a₁ a₂
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hf₁ : CircleIntegrable f₁ c R
hR : ¬R = 0
⊢ ∃ s ∈ codiscreteWithin (Ι 0 (2 * π)), EqOn (fun θ ↦ f₁ (circleMap c R θ)) (fun θ ↦ f₂ (circleMap c R θ)) s

Tactic:
exact ⟨(circleMap c R)⁻¹' {z | f₁ z = f₂ z},
    codiscreteWithin_mono (by simp only [Set.subset_univ]) (circleMap_preimage_codiscrete hR hf),
    by tauto⟩

Goal state after:
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
θ : ℝ
x✝ : θ ∈ Ι 0 (2 * π)
this : ‖w / (circleMap c R θ - c)‖ < 1
⊢ HasSum (fun n ↦ (w / (circleMap c R θ - c)) ^ n * (circleMap c R θ - c)⁻¹) (circleMap c R θ - (c + w))⁻¹

Tactic:
convert! (hasSum_geometric_of_norm_lt_one this).mul_right _ using 1

Goal state after:
case e'_6
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
θ : ℝ
x✝ : θ ∈ Ι 0 (2 * π)
this : ‖w / (circleMap c R θ - c)‖ < 1
⊢ (circleMap c R θ - (c + w))⁻¹ = (1 - w / (circleMap c R θ - c))⁻¹ * (circleMap c R θ - c)⁻¹
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: case hg
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[≠] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
hc' : ContinuousOn (fun z ↦ (z - c)⁻¹) (sphere c r)
⊢ ContinuousOn (fun z ↦ y) (sphere c r)

Tactic:
exact continuousOn_const

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: 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₁ * p₂)).Splits

Tactic:
rw [Polynomial.map_mul]

Goal state after:
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₁ * map (algebraMap F (q₁ * q₂).SplittingField) p₂).Splits
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case pos.inr
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r ↦ (map (algebraMap F (r.comp q).SplittingField) r).Splits
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : p₁.comp q = 0
h : eval (q.coeff 0) p₁ = 0 ∧ q = C (q.coeff 0)
⊢ P (p₁ * p₂)

Tactic:
exact False.elim (hq (by rw [h.2, natDegree_C]))

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case pos.inr
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r ↦ (map (algebraMap F (r.comp q).SplittingField) r).Splits
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬p₁.comp q = 0
h₂ : p₂.comp q = 0
h : eval (q.coeff 0) p₂ = 0 ∧ q = C (q.coeff 0)
⊢ P (p₁ * p₂)

Tactic:
exact False.elim (hq (by rw [h.2, natDegree_C]))

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
⊢ Function.Surjective ⇑(restrictComp p q hq)

Tactic:
by
  have : Fact (Splits (p.map (algebraMap F (SplittingField (comp p q))))) :=
    ⟨splits_in_splittingField_of_comp p q hq⟩
  simpa only [restrictComp] using! restrict_surjective _ _

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case a
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := ⋯
hα : IsIntegral F α
this : minpoly F α ∣ p
key : p ∣ minpoly F α
⊢ p.natDegree ≤ (minpoly F α).natDegree

Tactic:
exact natDegree_le_of_dvd key (minpoly.ne_zero hα)

Goal state after:
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * ↑π * I) • f w

Tactic:
← two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
    hs hw hc hd,

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * ↑π * I) • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i ↦ X i) univ.val
this : Fintype.card σ = s.card
⊢ ∏ i, (Polynomial.X + Polynomial.C (X i)) =
    ∑ x ∈ range (s.card + 1), Polynomial.C (esymm σ R x) * Polynomial.X ^ (s.card - x)

Tactic:
MvPolynomial.esymm_eq_multiset_esymm σ R,

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i ↦ X i) univ.val
this : Fintype.card σ = s.card
⊢ ∏ i, (Polynomial.X + Polynomial.C (X i)) =
    ∑ x ∈ range (s.card + 1), Polynomial.C ((Multiset.map X univ.val).esymm x) * Polynomial.X ^ (s.card - x)