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

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
h : ContDiffAt 𝕜 n f x
⊢ ContinuousAt f x

Tactic:
by
  simpa [continuousWithinAt_univ] using h.continuousWithinAt

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Exponential

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

Tactic:
Finset.noncommProd_insert_of_notMem _ _ _ _ ha,

Goal state after:
case insert
𝔸 : Type u_1
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_3
f : ι → 𝔸
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (h : (↑s).Pairwise (Commute on f)), exp (∑ i ∈ s, f i) = s.noncommProd (fun i ↦ exp (f i)) ⋯
h : (↑(insert a s)).Pairwise (Commute on f)
⊢ exp (∑ i ∈ insert a s, f i) = exp (f a) * s.noncommProd (fun i ↦ exp (f i)) ⋯
Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv

Goal state before:
pp: x : ℂ
this : 1 < 2
⊢ ∀ᶠ (x_1 : ℂ) in 𝓝 0, ‖cexp (x + x_1) - cexp x - x_1 • cexp x‖ ≤ ‖cexp x‖ * ‖x_1 ^ 2‖

Tactic:
filter_upwards [Metric.ball_mem_nhds (0 : ℂ) zero_lt_one]

Goal state after:
x : ℂ
this : 1 < 2
⊢ ∀ a ∈ Metric.ball 0 1, ‖cexp (x + a) - cexp x - a • cexp x‖ ≤ ‖cexp x‖ * ‖a ^ 2‖
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: case pos
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
hcont_Ioc : ∀ z ∈ Ioc a b, ContinuousWithinAt f (Icc a b) z
z : ℝ
hz : z ∈ Icc a b
hz' : z = a
⊢ ContinuousWithinAt f (Icc a b) z

Tactic:
hz'

Goal state after:
case pos
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
hcont_Ioc : ∀ z ∈ Ioc a b, ContinuousWithinAt f (Icc a b) z
z : ℝ
hz : z ∈ Icc a b
hz' : z = a
⊢ ContinuousWithinAt f (Icc a b) a
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : ℕ → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), (eapproxDiff f n) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg : ∀ (n : ℕ), ∫⁻ (x : α), ↑(g n x) ∂μ ≤ ∫⁻ (x : α), ↑((eapproxDiff f n) x) ∂μ + δ n
⊢ ∫⁻ (x : α), ∑' (n : ℕ), ↑(g n x) ∂μ = ∑' (n : ℕ), ∫⁻ (x : α), ↑(g n x) ∂μ

Tactic:
by
        rw [lintegral_tsum fun n => (gcont n).measurable.coe_nnreal_ennreal.aemeasurable]

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 : α → ℝ≥0
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), ↑(w x) ∂μ < ε / 2
f' : α → ℝ≥0∞ := fun x ↦ ↑(f x + w x)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
⊢ ∫⁻ (x : α), ↑(f x) ∂μ + ∫⁻ (x : α), ↑(w x) ∂μ + ε / 2 ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε / 2 + ε / 2

Tactic:
grw [wint]

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)
⊢ ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x)).toReal - (↑↑(gm x)).toReal

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)
a✝ : α
hx : gp a✝ < ∞
⊢ (g a✝).toReal = (↑(gp a✝)).toReal - (↑↑(gm a✝)).toReal
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inr.refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1}.Nonempty
r : ℝ
hr : r ∈ lowerBounds {r | 0 < r ∧ x ∈ r • p.ball 0 1}
ε : ℝ
hε : 0 < ε
hpε : 0 < p x + ε
⊢ r ≤ p x + ε

Tactic:
refine hr ⟨hpε, (p x + ε)⁻¹ • x, ?_, smul_inv_smul₀ hpε.ne' _⟩

Goal state after:
case inr.refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1}.Nonempty
r : ℝ
hr : r ∈ lowerBounds {r | 0 < r ∧ x ∈ r • p.ball 0 1}
ε : ℝ
hε : 0 < ε
hpε : 0 < p x + ε
⊢ (p x + ε)⁻¹ • x ∈ p.ball 0 1
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: R : Type u_4
V : Type u_5
W : Type u_6
inst✝¹³ : NormedField R
inst✝¹² : AddCommGroup V
inst✝¹¹ : AddCommGroup W
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : TopologicalSpace V
inst✝⁸ : TopologicalSpace W
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : Module R V
inst✝⁵ : Module R W
inst✝⁴ : SeparatingDual R V
inst✝³ : IsTopologicalAddGroup V
inst✝² : IsTopologicalAddGroup W
inst✝¹ : ContinuousSMul R V
inst✝ : ContinuousSMul R W
f g : V ≃L[R] W
x✝ : ∃ y, y • 1 = ↑g.symm ∘SL ↑f
y : R
h : y • 1 = ↑g.symm ∘SL ↑f
hy : ¬y = 0
⊢ ∃ α, ⇑f = ⇑(α • g)

Tactic:
else

Goal state after:
R : Type u_4
V : Type u_5
W : Type u_6
inst✝¹³ : NormedField R
inst✝¹² : AddCommGroup V
inst✝¹¹ : AddCommGroup W
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : TopologicalSpace V
inst✝⁸ : TopologicalSpace W
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : Module R V
inst✝⁵ : Module R W
inst✝⁴ : SeparatingDual R V
inst✝³ : IsTopologicalAddGroup V
inst✝² : IsTopologicalAddGroup W
inst✝¹ : ContinuousSMul R V
inst✝ : ContinuousSMul R W
f g : V ≃L[R] W
x✝ : ∃ y, y • 1 = ↑g.symm ∘SL ↑f
y : R
h : y • 1 = ↑g.symm ∘SL ↑f
hy : ¬y = 0
⊢ ∃ α, ⇑f = ⇑(α • g)
Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : Zero R
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace R
s : Set X
inst✝ : Zero ↑s
f : X → R
g : C(↑s, R)₀
hf : ¬ContinuousOn f s
⊢ mkD (s.domRestrict f) g = g

Tactic:
by
  rw [continuousOn_iff_continuous_domRestrict] at hf
  exact mkD_of_not_continuous hf

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')
⊢ x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}

Tactic:
have Lf' : ∀ e p, n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e := by
    intro e p hp
    apply le_of_tendsto (tendsto_const_nhds.sub hf').norm
    rw [eventually_atTop]
    exact ⟨e, fun e' he' => M _ _ _ _ _ _ le_rfl hp le_rfl le_rfl he'⟩

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')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
⊢ x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
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
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x ↦ ↑(f x))
C1 : Continuous fun u ↦ ∫ (x : X), ↑↑u x ∂μ.withDensity fun x ↦ ↑(f x)
this : Continuous ((fun u ↦ ∫ (x : X), ↑↑u x ∂μ) ∘ ⇑(withDensitySMulLI μ f_meas))
u : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
⊢ ∫ (x : X), f x • ↑↑u x ∂μ = ((fun u ↦ ∫ (x : X), ↑↑u x ∂μ) ∘ ⇑(withDensitySMulLI μ f_meas)) u

Tactic:
simp only [Function.comp_apply, withDensitySMulLI_apply]

Goal state after:
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x ↦ ↑(f x))
C1 : Continuous fun u ↦ ∫ (x : X), ↑↑u x ∂μ.withDensity fun x ↦ ↑(f x)
this : Continuous ((fun u ↦ ∫ (x : X), ↑↑u x ∂μ) ∘ ⇑(withDensitySMulLI μ f_meas))
u : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
⊢ ∫ (x : X), f x • ↑↑u x ∂μ = ∫ (x : X), ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case pos
ι : Type u_1
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst✝¹ : l'.IsMeasurablyGenerated
inst✝ : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
⊢ (fun t ↦ ∫ (x : ℝ) in u t..v t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t ↦ ∫ (x : ℝ) in u t..v t, 1 ∂μ

Tactic:
have A := hf.integral_sub_linear_isLittleO_ae hfm hl (hu.Ioc hv)

Goal state after:
case pos
ι : Type u_1
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst✝¹ : l'.IsMeasurablyGenerated
inst✝ : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  (fun i ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) =o[lt] fun i ↦ μ.real (Ioc (u i) (v i))
⊢ (fun t ↦ ∫ (x : ℝ) in u t..v t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t ↦ ∫ (x : ℝ) in u t..v t, 1 ∂μ
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
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
b✝ : ℝ
b_lt : b✝ < s * r
hb : ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b✝
ε : ℝ
εpos : 0 < ε
hε : b✝ + 2 * ε < s * r
C : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun p ↦ f a p.2
D : EqOn (Function.uncurry f) (fun p ↦ f a p.2) ({a} ×ˢ closedBall x t)
v : Set (α × E)
v_open : IsOpen[instTopologicalSpaceProd] v
sub_v : {a} ×ˢ closedBall x t ⊆ v
hv : ∀ p ∈ v, dist (Function.uncurry f p) (f a p.2) < ε
w : Set α
w' : Set E
w_open : IsOpen[inst✝] w
sub_w : {a} ⊆ w
sub_w' : closedBall x t ⊆ w'
hww' : w ×ˢ w' ⊆ v
b : α
y : E
h : (b, y).1 ∈ w
hby : (b, y).2 ∈ closedBall x t
⊢ dist (Function.uncurry f (b, y)) (Function.uncurry f (a, (b, y).2)) < ε

Tactic:
exact hv _ (hww' ⟨h, sub_w' hby⟩)

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

Goal state before:
pp: case pos
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
hc : c = 0
⊢ c • ∫ (x : ℝ) in a..b, f (d + c * x) = ∫ (x : ℝ) in d + c * a..d + c * b, f x

Tactic:
simp [hc, integral_comp_add_mul]

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

Goal state before:
pp: case neg
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
hc : ¬c = 0
⊢ c • ∫ (x : ℝ) in a..b, f (d + c * x) = ∫ (x : ℝ) in d + c * a..d + c * b, f x

Tactic:
simp [hc, integral_comp_add_mul]

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

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
⊢ 0 < ∫ (x : ℝ) in a..b, f x

Tactic:
by
  have hsupp : Ioo a b ⊆ support f ∩ Ioc a b := fun x hx =>
    ⟨mem_support.mpr (hpos x hx).ne', Ioo_subset_Ioc_self hx⟩
  have h₀ : 0 ≤ᵐ[volume.restrict (uIoc a b)] f := by
    rw [EventuallyLE, uIoc_of_le hab.le]
    refine ae_restrict_of_ae_eq_of_ae_restrict Ioo_ae_eq_Ioc ?_
    rw [ae_restrict_iff' measurableSet_Ioo]
    filter_upwards with x hx using (hpos x hx).le
  rw [integral_pos_iff_support_of_nonneg_ae' h₀ hfi]
  exact ⟨hab, ((Measure.measure_Ioo_pos _).mpr hab).trans_le (measure_mono hsupp)⟩

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✝² : IsStrictOrderedRing α
inst✝¹ : OrderClosedTopology α
inst✝ : IsTopologicalAddGroup α
n : ℤ
⊢ Tendsto fract (𝓝[<] ↑n) (𝓝 1)

Tactic:
by
  rw [← sub_sub_cancel (n : α) 1]
  refine (tendsto_id.mono_left nhdsWithin_le_nhds).sub ?_
  exact tendsto_floor_left' n

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
ε : ℝ
x : AddCircle T
⊢ T ≤ 2 * T

Tactic:
linarith [hT.out]

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
⊢ t ≤ t + T

Tactic:
linarith [hT.out]

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : ℝ → E
x : ℝ
hx : x ∈ uIoc t (t + T)
⊢ t ≤ t + T

Tactic:
linarith [hT.out]

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

Goal state before:
pp: case h₂
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this✝ : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
x : ℝ
hx : x ∈ Icc (b₀ - δ) (b₀ + δ)
⊢ ‖f p x - f q x‖ ≤ δ

Tactic:
exact le_of_lt (hv _ hp _ (h'δ hx))

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₁
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ ↑n₂
⊢ IntervalIntegrable f volume a₁ a₂

Tactic:
have : Set.uIcc a₁ a₂ ⊆ Set.uIcc (t - n₁ * T) (t + n₂ * T) := by
    rw [Set.uIcc_subset_uIcc_iff_le]
    constructor
    · calc min (t - n₁ * T) (t + n₂ * T)
      _ ≤ (t - n₁ * T) := by apply min_le_left
      _ ≤ min a₁ a₂ := by linarith [(div_le_iff₀ hT).1 hn₁]
    · calc max a₁ a₂
      _ ≤ t + n₂ * T := by linarith [(div_le_iff₀ hT).1 hn₂]
      _ ≤ max (t - n₁ * T) (t + n₂ * T) := by apply le_max_right

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₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
⊢ IntervalIntegrable f volume a₁ 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)‖
⊢ ∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞ ↔
    (∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞) ∧
      ∫⁻ (a : α), ENNReal.ofReal (∫⁻ (a_1 : β), ‖f (a, a_1)‖ₑ ∂ν).toReal ∂μ < ∞

Tactic:
have : ∀ {p q r : Prop} (_ : r → p), (r ↔ p ∧ q) ↔ p → (r ↔ q) := fun {p q r} h1 => by
    rw [← and_congr_right_iff, and_iff_right_of_imp h1]

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

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
⊢ ∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp b) θ) = ∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp a) θ)

Tactic:
set g : ℂ → ℂ := (c + exp ·)

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun x ↦ c + cexp x
⊢ ∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp b) θ) = ∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp a) θ)
Module: Mathlib.Analysis.Complex.Liouville

Goal state before:
pp: F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
z : ℂ
hz : z ∈ sphere c R
⊢ ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)

Tactic:
simpa [norm_smul, norm_pow, norm_inv, ← div_eq_inv_mul, mem_sphere_iff_norm.1 hz] using!
      (div_le_div_iff_of_pos_right (mul_pos (pow_pos hR n) hR)).2 (hC z hz)

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : p.Splits
f : p.Gal
y : F
⊢ (algebraMap F p.SplittingField) y = 1 ((algebraMap F p.SplittingField) y)

Tactic:
AlgEquiv.commutes

Goal state after:
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : p.Splits
f : p.Gal
y : F
⊢ (algebraMap F p.SplittingField) y = (algebraMap F p.SplittingField) y
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: case inr
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : B < 0
⊢ ‖(map f p).coeff i‖ ≤ max B 1 ^ d * ↑(d.choose (d / 2))

Tactic:
· rw [eq_one_of_roots_le hB h1 h2 h4, Polynomial.map_one, coeff_one]
    refine le_trans ?_ (one_le_mul_of_one_le_of_one_le (one_le_pow₀ (le_max_right B 1)) ?_)
    · split_ifs <;> norm_num
    · exact mod_cast Nat.succ_le_iff.mpr (Nat.choose_pos (d.div_le_self 2))

Goal state after:
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : One M
u v : ℚ
x y : M
hu : u.num • 1 < u.den • x
hv : v.num • 1 < v.den • y
⊢ (u.num * ↑v.den) • 1 < (↑u.den * ↑v.den) • x

Tactic:
simpa [mul_comm] using (mul_smul_one_lt_iff v.den_pos).mpr hu

Goal state after: