mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ n.factorial • choose (-r) n = n.factorial • (↑n).negOnePow • choose (r + ↑n - 1) n

Tactic:
rw [← descPochhammer_eq_factorial_smul_choose, smul_comm,
    ← descPochhammer_eq_factorial_smul_choose, descPochhammer_smeval_eq_ascPochhammer,
    show (-r - n + 1) = -(r + n - 1) by abel, ascPochhammer_smeval_neg_eq_descPochhammer]

Goal state after:
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: 𝕂 : Type u
inst✝⁵ : Field 𝕂
inst✝⁴ : CharZero 𝕂
𝔸 : Type v
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a : 𝕂
n : ℕ
v : Fin n → 𝔸
⊢ (binomialSeries 𝔸 a n) v = Ring.choose a n • (List.ofFn v).prod

Tactic:
by
  simp [binomialSeries, FormalMultilinearSeries.ofScalars]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
⊢ r * (descPochhammer ℤ k).smeval r + (descPochhammer ℤ k).smeval r =
    k • (descPochhammer ℤ k).smeval r + (descPochhammer ℤ k).smeval r +
      (r * (descPochhammer ℤ k).smeval r - (↑k).smeval r * (descPochhammer ℤ k).smeval r)

Tactic:
rw [← C_eq_natCast, smeval_C, npow_zero, add_comm (k • smeval (descPochhammer ℤ k) r) _,
    add_assoc, add_comm (k • smeval (descPochhammer ℤ k) r) _, ← add_assoc, ← add_sub_assoc,
    nsmul_eq_mul, zsmul_one, Int.cast_natCast, sub_add_cancel, add_comm]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case e'_12
p : ℝ × ℝ
hp : 0 < p.1
this : (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ rexp (log x.1 * x.2)
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
⊢ (p.2 * (p.1 ^ p.2 / p.1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    p.1 ^ p.2 • log p.1 • ContinuousLinearMap.snd ℝ ℝ ℝ + p.1 ^ p.2 • p.2 • p.1⁻¹ • ContinuousLinearMap.fst ℝ ℝ ℝ

Tactic:
smul_smul,

Goal state after:
case e'_12
p : ℝ × ℝ
hp : 0 < p.1
this : (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ rexp (log x.1 * x.2)
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
⊢ (p.2 * (p.1 ^ p.2 / p.1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ + p.1 ^ p.2 • p.2 • p.1⁻¹ • ContinuousLinearMap.fst ℝ ℝ ℝ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case e'_12
p : ℝ × ℝ
hp : 0 < p.1
this : (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ rexp (log x.1 * x.2)
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
⊢ (p.1 ^ p.2 * (p.2 * p.1⁻¹)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ + p.1 ^ p.2 • p.2 • p.1⁻¹ • ContinuousLinearMap.fst ℝ ℝ ℝ

Tactic:
smul_smul,

Goal state after:
case e'_12
p : ℝ × ℝ
hp : 0 < p.1
this : (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ rexp (log x.1 * x.2)
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
⊢ (p.1 ^ p.2 * (p.2 * p.1⁻¹)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ + (p.1 ^ p.2 * p.2) • p.1⁻¹ • ContinuousLinearMap.fst ℝ ℝ ℝ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case e'_12
p : ℝ × ℝ
hp : 0 < p.1
this : (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ rexp (log x.1 * x.2)
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
⊢ (p.1 ^ p.2 * (p.2 * p.1⁻¹)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ + (p.1 ^ p.2 * p.2) • p.1⁻¹ • ContinuousLinearMap.fst ℝ ℝ ℝ

Tactic:
smul_smul,

Goal state after:
case e'_12
p : ℝ × ℝ
hp : 0 < p.1
this : (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ rexp (log x.1 * x.2)
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
⊢ (p.1 ^ p.2 * (p.2 * p.1⁻¹)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ + (p.1 ^ p.2 * p.2 * p.1⁻¹) • ContinuousLinearMap.fst ℝ ℝ ℝ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case e'_12
p : ℝ × ℝ
hp : p.1 < 0
this : (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_8✝ : instAddCommGroup = normedCommRing.toCommRing.toAddCommGroup
e_9✝ : Semiring.toModule ≍ (NormedAlgebra.toNormedSpace ℝ).toModule
⊢ (p.2 * (p.1 ^ p.2 / p.1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    rexp (log p.1 * p.2) • -sin (p.2 * π) • π • ContinuousLinearMap.snd ℝ ℝ ℝ +
        cos (p.2 * π) • rexp (log p.1 * p.2) • log p.1 • ContinuousLinearMap.snd ℝ ℝ ℝ +
      cos (p.2 * π) • rexp (log p.1 * p.2) • p.2 • p.1⁻¹ • ContinuousLinearMap.fst ℝ ℝ ℝ

Tactic:
smul_smul,

Goal state after:
case e'_12
p : ℝ × ℝ
hp : p.1 < 0
this : (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_8✝ : instAddCommGroup = normedCommRing.toCommRing.toAddCommGroup
e_9✝ : Semiring.toModule ≍ (NormedAlgebra.toNormedSpace ℝ).toModule
⊢ (p.2 * (p.1 ^ p.2 / p.1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
      (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    (rexp (log p.1 * p.2) * (-sin (p.2 * π) * π)) • ContinuousLinearMap.snd ℝ ℝ ℝ +
        (cos (p.2 * π) * (rexp (log p.1 * p.2) * log p.1)) • ContinuousLinearMap.snd ℝ ℝ ℝ +
      (cos (p.2 * π) * (rexp (log p.1 * p.2) * (p.2 * p.1⁻¹))) • ContinuousLinearMap.fst ℝ ℝ ℝ
Module: Mathlib.Analysis.Analytic.RadiusLiminf

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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
n : ℕ
hn : 0 < n
this : 0 < ↑n
| r ^ 1 * ‖p n‖₊ ^ (↑n)⁻¹ ≤ 1

Tactic:
← mul_inv_cancel₀ this.ne',

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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
n : ℕ
hn : 0 < n
this : 0 < ↑n
| r ^ (↑n * (↑n)⁻¹) * ‖p n‖₊ ^ (↑n)⁻¹ ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case succ
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x ↦ x ^ p
p : ℝ
h : ↑n ≤ p - 1
h1 : 1 ≤ p
⊢ (Differentiable ℝ fun x ↦ x ^ p) ∧ ContDiff ℝ ↑n fun x ↦ p * x ^ (p - 1)

Tactic:
exact ⟨differentiable_rpow_const h1, contDiff_const.mul (ihn h)⟩

Goal state after:
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: ⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x)) (FormalMultilinearSeries.ofScalars ℝ 1) 0 1

Tactic:
simpa using! one_div_sub_hasFPowerSeriesOnBall_zero (r := 1)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ (ENNReal.ofReal x).log = ↑(Real.log x)

Tactic:
log_ofReal,

Goal state after:
x : ℝ
hx : 0 < x
⊢ (if x ≤ 0 then ⊥ else ↑(Real.log x)) = ↑(Real.log x)
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: case coe
a✝ : ℝ
⊢ (ENNReal.ofReal (Real.exp a✝)).log = ↑a✝

Tactic:
log_ofReal,

Goal state after:
case coe
a✝ : ℝ
⊢ (if Real.exp a✝ ≤ 0 then ⊥ else ↑(Real.log (Real.exp a✝))) = ↑a✝
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
⊢ x ^ y = (↑y * x.log).exp

Tactic:
rw [← log_rpow, exp_log]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case refine_1
a b : EReal
hb : 0 ≤ b
h : ⊥ < b
n : ℕ
⊢ ⊥ * ↑n ≤ 0

Tactic:
apply mul_nonpos_iff.2 -- Split apply and exact for a 0.5s. gain
      exact .inr ⟨bot_le, n.cast_nonneg'⟩

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case neg.inl
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : ¬u = ⊥
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
b : EReal
u_b : b > linearGrowthInf u
b_0 : 0 < b
v_a : ⊤ > linearGrowthSup fun n ↦ ↑(v n)
a_0 : 0 < ⊤
⊢ linearGrowthInf (u ∘ v) ≤ ⊤ * b

Tactic:
rw [top_mul_of_pos b_0]; exact le_top

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Finset α
⊢ expGrowthSup (∑ x ∈ s, u x) = ⨆ x ∈ s, expGrowthSup (u x)

Tactic:
induction s using Finset.induction_on with

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
v : ℕ → ℕ
h : Monotone u
h' : u ≠ 0
hv : Tendsto v atTop atTop
⊢ 0 ≤ expGrowthInf (u ∘ v)

Tactic:
apply linearGrowthInf_comp_nonneg (u := log ∘ u) (log_monotone.comp h) _ hv

Goal state after:
u : ℕ → ℝ≥0∞
v : ℕ → ℕ
h : Monotone u
h' : u ≠ 0
hv : Tendsto v atTop atTop
⊢ log ∘ u ≠ ⊥
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case neg
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun n ↦ ↑(v n) / ↑n) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : 0 < liminf (fun n ↦ ↑(v n) / ↑n) atTop
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∀ᶠ (x : ℕ) in atTop, 0 < u x
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u

Tactic:
replace h' := h'.mono fun _ hn ↦ hn.le
    apply le_antisymm
    · rw [← hv.limsup_eq] at ha ha' ⊢
      exact h.linearGrowthInf_comp_le ha ha'
    · rw [← hv.liminf_eq]
      exact le_linearGrowthInf_comp h' v_top

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

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : μ univ = ∞
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

Tactic:
simp [laverage_eq, hμ]

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
ε N : ℝ≥0
p : ℕ
εpos : 0 < ε
s : Set α := {x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p
s_lt_top : μ s < ∞
⊢ ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ

Tactic:
← Measure.restrict_toMeasurable s_lt_top.ne

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
ε N : ℝ≥0
p : ℕ
εpos : 0 < ε
s : Set α := {x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p
s_lt_top : μ s < ∞
⊢ ∫⁻ (x : α) in toMeasurable μ s, f x ∂μ ≤ ∫⁻ (x : α) in toMeasurable μ s, g x ∂μ
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : α → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), μ (closedBall x (20 * R x)) < ∞
⊢ ∃ u ⊆ t, u.Countable ∧ u.PairwiseDisjoint B ∧ μ (s \ ⋃ a ∈ u, B a) = 0

Tactic:
let t' := { a ∈ t | r a ≤ R (c a) }

Goal state after:
α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : α → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), μ (closedBall x (20 * R x)) < ∞
t' : Set ι := {a | a ∈ t ∧ r a ≤ R (c a)}
⊢ ∃ u ⊆ t, u.Countable ∧ u.PairwiseDisjoint B ∧ μ (s \ ⋃ a ∈ u, B a) = 0
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf₀ : 0 ≤ᵐ[μ] f
hμ : μ ≠ 0
⊢ ENNReal.ofReal ((μ univ)⁻¹.toReal * ∫ (x : α), f x ∂μ) = (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) / μ univ

Tactic:
ofReal_mul toReal_nonneg,

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf₀ : 0 ≤ᵐ[μ] f
hμ : μ ≠ 0
⊢ ENNReal.ofReal (μ univ)⁻¹.toReal * ENNReal.ofReal (∫ (x : α), f x ∂μ) = (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) / μ univ
Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfg : μ.withDensity f = μ.withDensity g
s : Set α
hs : MeasurableSet s
x✝ : μ s < ∞
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ

Tactic:
· rw [← withDensity_apply f hs, ← withDensity_apply g hs, ← hfg]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : α → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), μ (closedBall x (20 * R x)) < ∞
t' : Set ι := {a | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
x✝ : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : μ (closedBall x K) < ∞
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : ∑' (a : ↑v), μ (B ↑a) < ∞
⊢ 0 < ε / ↑C

Tactic:
simp only [ENNReal.div_pos_iff, εpos.ne', ENNReal.coe_ne_top, Ne, not_false_iff,
        and_self_iff]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (fun i ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (fun i ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
i : ι
hif : IntegrableOn f (a i) μ
hig : Integrable (g i) μ
hisupp : support (g i) ⊆ a i
hibound : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
⊢ ∫ (y : α), g i y • (f y - c) ∂μ + (∫ (y : α), g i y ∂μ) • c = ∫ (y : α), g i y • f y ∂μ

Tactic:
← integral_smul_const,

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (fun i ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (fun i ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
i : ι
hif : IntegrableOn f (a i) μ
hig : Integrable (g i) μ
hisupp : support (g i) ⊆ a i
hibound : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
⊢ ∫ (y : α), g i y • (f y - c) ∂μ + ∫ (x : α), g i x • c ∂μ = ∫ (y : α), g i y • f y ∂μ
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν = 0

Tactic:
by
  rw [singularPart, dif_neg h]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (fun i ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (fun i ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I : ∀ᶠ (i : ι) in l, ∫ (y : α), g i y • (f y - c) ∂μ + (∫ (y : α), g i y ∂μ) • c = ∫ (y : α), g i y • f y ∂μ
⊢ Tendsto (fun i ↦ ∫ (y : α), g i y • (f y - c) ∂μ) l (𝓝 0)

Tactic:
have := hf.const_mul K

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (fun i ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (fun i ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I : ∀ᶠ (i : ι) in l, ∫ (y : α), g i y • (f y - c) ∂μ + (∫ (y : α), g i y ∂μ) • c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (fun x ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 (K * 0))
⊢ Tendsto (fun i ↦ ∫ (y : α), g i y • (f y - c) ∂μ) l (𝓝 0)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case left.inr
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := max (f m.succ a) (⨆ k, ⨆ (_ : k ≤ m), f k a)
hd : d = max (f m.succ a) (⨆ k, ⨆ (_ : k ≤ m), f k a)
n : ℕ
hn : n ≤ m + 1
h : n = m.succ
⊢ f n a ≤ max (f m.succ a) (⨆ k, ⨆ (_ : k ≤ m), f k a)

Tactic:
exact h ▸ le_sup_left

Goal state after:
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
s : Set α
E : Type u_3
inst✝² : PseudoMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
l : E
a b : α
ha : a ∈ s
hb : b ∈ s
hf : LocallyBoundedVariationOn f s
h'f : Tendsto f (𝓝[s ∩ Iio b] b) (𝓝 l)
⊢ Tendsto (fun x ↦ (eVariationOn f (s ∩ Icc x b)).toReal) (𝓝[s ∩ Iio b] b) (𝓝 (dist (f b) l))

Tactic:
rw [dist_edist]

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
s : Set α
E : Type u_3
inst✝² : PseudoMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
l : E
a b : α
ha : a ∈ s
hb : b ∈ s
hf : LocallyBoundedVariationOn f s
h'f : Tendsto f (𝓝[s ∩ Iio b] b) (𝓝 l)
⊢ Tendsto (fun x ↦ (eVariationOn f (s ∩ Icc x b)).toReal) (𝓝[s ∩ Iio b] b) (𝓝 (edist (f b) l).toReal)
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
s : Set α
E : Type u_3
inst✝² : PseudoMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
l : E
a b : α
ha : a ∈ s
hb : b ∈ s
hf : LocallyBoundedVariationOn f s
h'f : Tendsto f (𝓝[s ∩ Ioi b] b) (𝓝 l)
⊢ Tendsto (fun x ↦ (eVariationOn f (s ∩ Icc b x)).toReal) (𝓝[s ∩ Ioi b] b) (𝓝 (dist (f b) l))

Tactic:
rw [dist_edist]

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
s : Set α
E : Type u_3
inst✝² : PseudoMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
l : E
a b : α
ha : a ∈ s
hb : b ∈ s
hf : LocallyBoundedVariationOn f s
h'f : Tendsto f (𝓝[s ∩ Ioi b] b) (𝓝 l)
⊢ Tendsto (fun x ↦ (eVariationOn f (s ∩ Icc b x)).toReal) (𝓝[s ∩ Ioi b] b) (𝓝 (edist (f b) l).toReal)
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
s : Set α
E : Type u_3
inst✝² : PseudoMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
l : E
a b : α
ha : a ∈ s
hb : b ∈ s
hf : LocallyBoundedVariationOn f s
h'f : Tendsto f (𝓝[s ∩ Ioi b] b) (𝓝 l)
⊢ Tendsto (variationOnFromTo f s a) (𝓝[s ∩ Ioi b] b) (𝓝 (variationOnFromTo f s a b + dist (f b) l))

Tactic:
by
  suffices H : Tendsto (fun x ↦ variationOnFromTo f s a b + variationOnFromTo f s b x)
      (𝓝[s ∩ Ioi b] b) (𝓝 (variationOnFromTo f s a b + dist (f b) l)) by
    apply Tendsto.congr' _ H
    filter_upwards [self_mem_nhdsWithin] with x hx
    rw [variationOnFromTo.add hf ha hb hx.1]
  apply Tendsto.const_add
  suffices H : Tendsto (fun x ↦ (eVariationOn f (s ∩ Icc b x)).toReal) (𝓝[s ∩ Ioi b] b)
      (𝓝 (dist (f b) l)) by
    apply Tendsto.congr' _ H
    filter_upwards [self_mem_nhdsWithin] with x hx using by simp [variationOnFromTo, hx.2.le]
  rw [dist_edist]
  exact (ENNReal.tendsto_toReal (by simp)).comp (hf.tendsto_eVariationOn_Icc_right h'f hb)

Goal state after:
Module: Mathlib.Analysis.BoundedVariation

Goal state before:
pp: ι : Type u_2
inst✝ : Fintype ι
f : ℝ → ι → ℝ
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : ∀ (i : ι), LipschitzWith 1 fun x ↦ x i
this : ∀ (i : ι), ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (fun x ↦ f x i) s x
x : ℝ
hx : ∀ (i : ι), x ∈ s → DifferentiableWithinAt ℝ (fun x ↦ f x i) s x
xs : x ∈ s
⊢ DifferentiableWithinAt ℝ f s x

Tactic:
exact differentiableWithinAt_pi.2 fun i => hx i xs

Goal state after: