mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Analytic.Polynomial

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CommSemiring A
z : E
inst✝² : NormedCommRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt 𝕜 (fun x ↦ f x i) z
p✝ p : MvPolynomial σ A
i : σ
hp : AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) p) z
⊢ AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) p * f x i) z

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CommSemiring A
z : E
inst✝² : NormedCommRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt 𝕜 (fun x ↦ f x i) z
p✝ p : MvPolynomial σ A
i : σ
hp : AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) p) z
⊢ AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) p * f x i) z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case e'_9
x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : x < 0
this :
  HasStrictDerivAt ((fun x ↦ x.1 ^ x.2) ∘ fun x ↦ (id x, p))
    ((((x, p).2 * (x, p).1 ^ ((x, p).2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
        ((x, p).1 ^ (x, p).2 * log (x, p).1 - rexp (log (x, p).1 * (x, p).2) * sin ((x, p).2 * π) * π) •
          ContinuousLinearMap.snd ℝ ℝ ℝ)
      (1, 0))
    x
⊢ p * x ^ (p - 1) =
    (((x, p).2 * (x, p).1 ^ ((x, p).2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
        ((x, p).1 ^ (x, p).2 * log (x, p).1 - rexp (log (x, p).1 * (x, p).2) * sin ((x, p).2 * π) * π) •
          ContinuousLinearMap.snd ℝ ℝ ℝ)
      (1, 0)

Tactic:
;

Goal state after:
case e'_9
x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : x < 0
this :
  HasStrictDerivAt ((fun x ↦ x.1 ^ x.2) ∘ fun x ↦ (id x, p))
    ((((x, p).2 * (x, p).1 ^ ((x, p).2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
        ((x, p).1 ^ (x, p).2 * log (x, p).1 - rexp (log (x, p).1 * (x, p).2) * sin ((x, p).2 * π) * π) •
          ContinuousLinearMap.snd ℝ ℝ ℝ)
      (1, 0))
    x
⊢ p * x ^ (p - 1) =
    (((x, p).2 * (x, p).1 ^ ((x, p).2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
        ((x, p).1 ^ (x, p).2 * log (x, p).1 - rexp (log (x, p).1 * (x, p).2) * sin ((x, p).2 * π) * π) •
          ContinuousLinearMap.snd ℝ ℝ ℝ)
      (1, 0)
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 (z := 1)

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

Goal state before:
pp: case e'_10
a b : ℂ
n✝ : ℕ
⊢ ((FormalMultilinearSeries.ofScalars ℂ (fun n ↦ a * ↑n + b) n✝) fun x ↦ 1) =
    (((b - a) • FormalMultilinearSeries.ofScalars ℂ 1 + a • FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑n + 1) n✝)
      fun x ↦ 1

Tactic:
;

Goal state after:
case e'_10
a b : ℂ
n✝ : ℕ
⊢ ((FormalMultilinearSeries.ofScalars ℂ (fun n ↦ a * ↑n + b) n✝) fun x ↦ 1) =
    (((b - a) • FormalMultilinearSeries.ofScalars ℂ 1 + a • FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑n + 1) n✝)
      fun x ↦ 1
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_10
a b : ℂ
n✝ : ℕ
⊢ a * ↑n✝ + b = b - a + a * (↑n✝ + 1)

Tactic:
;

Goal state after:
case e'_10
a b : ℂ
n✝ : ℕ
⊢ a * ↑n✝ + b = b - a + a * (↑n✝ + 1)
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 : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)

Tactic:
intro r

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 : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_10
a : ℝ
H : binomialSeries ℂ a = FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ ↑a)
this : HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ ↑a) (binomialSeries ℂ a) (Complex.ofRealCLM 0) 1
n✝ : ℕ
⊢ ((binomialSeries ℝ a n✝) fun x ↦ 1) =
    (Complex.reCLM.compFormalMultilinearSeries ((binomialSeries ℂ a).compContinuousLinearMap Complex.ofRealCLM) n✝)
      fun x ↦ 1

Tactic:
;

Goal state after:
case e'_10
a : ℝ
H : binomialSeries ℂ a = FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ ↑a)
this : HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ ↑a) (binomialSeries ℂ a) (Complex.ofRealCLM 0) 1
n✝ : ℕ
⊢ ((binomialSeries ℝ a n✝) fun x ↦ 1) =
    (Complex.reCLM.compFormalMultilinearSeries ((binomialSeries ℂ a).compContinuousLinearMap Complex.ofRealCLM) n✝)
      fun x ↦ 1
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case convert_2
a : ℝ
H : binomialSeries ℂ a = FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ ↑a)
this : HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ ↑a) (binomialSeries ℂ a) (Complex.ofRealCLM 0) 1
x : ℝ
hx : x ∈ Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ)
⊢ (⇑Complex.reCLM ∘ (fun x ↦ (1 + x) ^ ↑a) ∘ ⇑Complex.ofRealCLM) x = (fun x ↦ (1 + x) ^ a) x

Tactic:
;

Goal state after:
case convert_2
a : ℝ
H : binomialSeries ℂ a = FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ ↑a)
this : HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ ↑a) (binomialSeries ℂ a) (Complex.ofRealCLM 0) 1
x : ℝ
hx : x ∈ Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ)
⊢ (⇑Complex.reCLM ∘ (fun x ↦ (1 + x) ^ ↑a) ∘ ⇑Complex.ofRealCLM) x = (fun x ↦ (1 + x) ^ a) x
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case convert_2
a : ℝ
H : binomialSeries ℂ a = FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ ↑a)
x : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ ↑a) (FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ ↑a)) 0 1
hx : ‖x‖ₑ < 1
⊢ ((1 + ↑x) ^ ↑a).re = (1 + x) ^ a

Tactic:
;

Goal state after:
case convert_2
a : ℝ
H : binomialSeries ℂ a = FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ ↑a)
x : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ ↑a) (FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ ↑a)) 0 1
hx : ‖x‖ₑ < 1
⊢ ((1 + ↑x) ^ ↑a).re = (1 + x) ^ a
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x : E
p : ℝ
m : ℕ
hf : ContDiffWithinAt ℝ (↑m) f Set.univ x
h : ↑m ≤ p
⊢ ContDiffWithinAt ℝ (↑m) (fun x ↦ f x ^ p) Set.univ x

Tactic:
;

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x : E
p : ℝ
m : ℕ
hf : ContDiffWithinAt ℝ (↑m) f Set.univ x
h : ↑m ≤ p
⊢ ContDiffWithinAt ℝ (↑m) (fun x ↦ f x ^ p) Set.univ x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: f g : ℝ → ℝ
f' g' x : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h : 0 < f x
⊢ f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x) =
    g x * f x ^ (g x - 1) * f' + f x ^ g x * Real.log (f x) * g'

Tactic:
;

Goal state after:
f g : ℝ → ℝ
f' g' x : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h : 0 < f x
⊢ f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x) =
    g x * f x ^ (g x - 1) * f' + f x ^ g x * Real.log (f x) * g'
Module: Mathlib.Topology.MetricSpace.MetricSeparated

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
s : Set X
ε K₁ : ℝ≥0
f : X → Y
hs : IsSeparated (↑ε) s
hf : AntilipschitzWith K₁ f
hK₁ : 0 < K₁
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hne : f x ≠ f y
⊢ edist x y ≤ ↑K₁ * edist (f x) (f y)

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
s : Set X
ε K₁ : ℝ≥0
f : X → Y
hs : IsSeparated (↑ε) s
hf : AntilipschitzWith K₁ f
hK₁ : 0 < K₁
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hne : f x ≠ f y
⊢ edist x y ≤ ↑K₁ * edist (f x) (f y)
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_10
a b : ℝ
n✝ : ℕ
⊢ ((FormalMultilinearSeries.ofScalars ℝ (fun x ↦ a * ↑x + b) n✝) fun x ↦ 1) =
    (((b - a) • FormalMultilinearSeries.ofScalars ℝ 1 + a • FormalMultilinearSeries.ofScalars ℝ fun n ↦ ↑n + 1) n✝)
      fun x ↦ 1

Tactic:
;

Goal state after:
case e'_10
a b : ℝ
n✝ : ℕ
⊢ ((FormalMultilinearSeries.ofScalars ℝ (fun x ↦ a * ↑x + b) n✝) fun x ↦ 1) =
    (((b - a) • FormalMultilinearSeries.ofScalars ℝ 1 + a • FormalMultilinearSeries.ofScalars ℝ fun n ↦ ↑n + 1) n✝)
      fun x ↦ 1
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_10
a b : ℝ
n✝ : ℕ
⊢ a * ↑n✝ + b = b - a + a * (↑n✝ + 1)

Tactic:
;

Goal state after:
case e'_10
a b : ℝ
n✝ : ℕ
⊢ a * ↑n✝ + b = b - a + a * (↑n✝ + 1)
Module: Mathlib.Topology.MetricSpace.Cover

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
ε δ : ℝ≥0
s N : Set X
hεδ : ε ≤ δ
hε : IsCover ε s N
xy : X × X
hxy : edist xy.1 xy.2 ≤ ↑ε
⊢ edist xy.1 xy.2 ≤ ↑δ

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε δ : ℝ≥0
s N : Set X
hεδ : ε ≤ δ
hε : IsCover ε s N
xy : X × X
hxy : edist xy.1 xy.2 ≤ ↑ε
⊢ edist xy.1 xy.2 ≤ ↑δ
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

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
f : E → F
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 ω f (s ∩ u)
this : iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x
⊢ (iteratedFDerivWithin 𝕜 n f (s ∩ u) x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f (s ∩ u) x) v

Tactic:
exact AnalyticOn.iteratedFDerivWithin_comp_perm hu.analyticOn (hs.inter u_open) ⟨hx, xu⟩ _ _

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
r : ℝ≥0
hr : r ≤ D.packingRadius / 2
x y z : X
hx : x ∈ D
hy : y ∈ D
hxz : x ∈ ball z ↑r
hyz : y ∈ ball z ↑r
hne : ¬x = y
⊢ ↑r + ↑r ≤ ↑(D.packingRadius / 2) + ↑(D.packingRadius / 2)

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
r : ℝ≥0
hr : r ≤ D.packingRadius / 2
x y z : X
hx : x ∈ D
hy : y ∈ D
hxz : x ∈ ball z ↑r
hyz : y ∈ ball z ↑r
hne : ¬x = y
⊢ ↑r + ↑r ≤ ↑(D.packingRadius / 2) + ↑(D.packingRadius / 2)
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case h
⊢ log 0 = ⊥

Tactic:
;

Goal state after:
case h
⊢ log 0 = ⊥
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case h
⊢ ∞.log = ⊤

Tactic:
;

Goal state after:
case h
⊢ ∞.log = ⊤
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case h
y : ℝ
⊢ (ENNReal.ofReal (Real.exp y)).log = ↑y

Tactic:
;

Goal state after:
case h
y : ℝ
⊢ (ENNReal.ofReal (Real.exp y)).log = ↑y
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inl
y : ℝ≥0∞
⊢ (∞ * y).log = ∞.log + y.log

Tactic:
log_top

Goal state after:
case inr.inl
y : ℝ≥0∞
⊢ (∞ * y).log = ⊤ + y.log
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ 0 < ↑y

Tactic:
;

Goal state after:
case inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ 0 < ↑y
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ 0 < ↑y

Tactic:
;

Goal state after:
case inr.inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ 0 < ↑y
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: case hbc
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : CommRing β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a ↦ |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
⊢ |g x| ≤ |f x|

Tactic:
;

Goal state after:
case hbc
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : CommRing β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a ↦ |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
⊢ |g x| ≤ |f x|
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: α : Type u_1
u : α → ℕ → EReal
s : Set α
hs : s.Finite
⊢ linearGrowthInf (⨅ x ∈ s, u x) = ⨅ x ∈ s, linearGrowthInf (u x)

Tactic:
have := map_finset_inf linearGrowthInfTopHom hs.toFinset u
  simpa only [linearGrowthInfTopHom, InfTopHom.coe_mk, InfHom.coe_mk, Finset.inf_eq_iInf,
    hs.mem_toFinset, comp_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝³ : NormedField β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
this✝ : (fun x ↦ 1) =o[l] k
this : f =o[l] fun x ↦ k x * k x ^ (z - 1)
x : α
hkx : k x ≠ 0
⊢ ‖k x * k x ^ (z - 1)‖ = ‖k x ^ z‖

Tactic:
simp [← zpow_one_add₀ hkx]

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

Goal state before:
pp: case inl
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Tendsto v atTop atTop
m : ℕ
hum : ¬u m = ⊥ m
um_uvn : ∀ᶠ (n : ℕ) in atTop, u m ≤ (u ∘ v) n
hum' : u m = ⊤
⊢ 0 ≤ ⊤

Tactic:
;

Goal state after:
case inl
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Tendsto v atTop atTop
m : ℕ
hum : ¬u m = ⊥ m
um_uvn : ∀ᶠ (n : ℕ) in atTop, u m ≤ (u ∘ v) n
hum' : u m = ⊤
⊢ 0 ≤ ⊤
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case pos
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : u = ⊥
⊢ ⊥ ≤ (linearGrowthSup fun n ↦ ↑(v n)) * ⊥

Tactic:
;

Goal state after:
case pos
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : u = ⊥
⊢ ⊥ ≤ (linearGrowthSup fun n ↦ ↑(v n)) * ⊥
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) ≤ ⊤

Tactic:
;

Goal state after:
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) ≤ ⊤
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case pos
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
v_0 : 0 < linearGrowthInf fun n ↦ ↑(v n)
u_0 : u = ⊥
⊢ ⊥ ≤ linearGrowthSup (⊥ ∘ v)

Tactic:
;

Goal state after:
case pos
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
v_0 : 0 < linearGrowthInf fun n ↦ ↑(v n)
u_0 : u = ⊥
⊢ ⊥ ≤ linearGrowthSup (⊥ ∘ v)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
⊢ ∃ s,
    MeasurableSet s ∧
      (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t

Tactic:
have hμ : ∀ s, μ s ≠ ∞ := measure_ne_top μ

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
⊢ ∃ s,
    MeasurableSet s ∧
      (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
Module: Mathlib.MeasureTheory.Integral.Average

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

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

Tactic:
;

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

case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : ¬IsFiniteMeasure μ
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν
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 = ⊥
u_1 : ∃ᶠ (x : ℕ) in atTop, 0 < u x
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u

Tactic:
· replace u_1 := u_1.mono fun x hx ↦ hx.le
    apply le_antisymm
    · rw [← hv.limsup_eq] at ha ha' ⊢
      exact linearGrowthSup_comp_le u_1 ha ha' v_top
    · rw [← hv.liminf_eq]
      exact h.le_linearGrowthSup_comp hv₁.ne.symm

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

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

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

Tactic:
;

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

case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
hν : ¬IsFiniteMeasure ν
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure (μ.restrict s)
⊢ ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ

pp: case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : ¬IsFiniteMeasure (μ.restrict s)
⊢ ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ

Tactic:
;

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure (μ.restrict s)
⊢ ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ

case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : ¬IsFiniteMeasure (μ.restrict s)
⊢ ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ
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 α
f : α → E
s : Set α
⊢ ⨍ (x : α) in s, f x ∂μ = ∫ (x : α), f x ∂(μ s)⁻¹ • μ.restrict s

Tactic:
by
  simp only [average_eq', restrict_apply_univ]

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 α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ∞
htμ : μ t ≠ ∞
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
this : Fact (μ s < ∞)
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ =
    (μ.real s / (μ.real s + μ.real t)) • ⨍ (x : α) in s, f x ∂μ +
      (μ.real t / (μ.real s + μ.real t)) • ⨍ (x : α) in t, f x ∂μ

Tactic:
;

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ∞
htμ : μ t ≠ ∞
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
this : Fact (μ s < ∞)
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ =
    (μ.real s / (μ.real s + μ.real t)) • ⨍ (x : α) in s, f x ∂μ +
      (μ.real t / (μ.real s + μ.real t)) • ⨍ (x : α) in t, f x ∂μ
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✝ : IsFiniteMeasure μ
f : α → E
s : Set α
hs : NullMeasurableSet s μ
hs₀ : μ s ≠ 0
hsc₀ : μ sᶜ ≠ 0
hfi : Integrable f μ
⊢ ⨍ (x : α), f x ∂μ ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in sᶜ, f x ∂μ)

Tactic:
simpa only [union_compl_self, restrict_univ] using
    average_union_mem_openSegment aedisjoint_compl_right hs.compl hs₀ hsc₀ (measure_ne_top _ _)
      (measure_ne_top _ _) hfi.integrableOn hfi.integrableOn

Goal state after: