mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
⊢ expGrowthSup u ≤ expGrowthSup v

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x ↦ ⨅ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ p, ⋃ q, u' ↑p ∩ v ↑p ↑q
⊢ μ t ≤ ∑' (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), μ (u' ↑p ∩ v ↑p ↑q)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x ↦ ⨅ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ p, ⋃ q, u' ↑p ∩ v ↑p ↑q
⊢ ∑' (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), μ (u' ↑p ∩ v ↑p ↑q) ≤ ∑' (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), μ (u ↑p ↑q ∩ v ↑p ↑q)

Tactic:
by

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

Goal state before:
pp: u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, b * u n ≤ v n
⊢ expGrowthInf u ≤ expGrowthInf v

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
⊢ ∃ m, Maximal (fun x ↦ x ∈ T) m

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x ↦ ⨅ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ p, ⋃ q, u' ↑p ∩ v ↑p ↑q
⊢ ∑' (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), μ (u ↑p ↑q ∩ v ↑p ↑q) = ∑' (p : ↑s) (x : ↑(s ∩ Ioi ↑p)), 0

Tactic:
by

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

Goal state before:
pp: u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, b * u n ≤ v n
⊢ expGrowthSup u ≤ expGrowthSup v

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x ↦ ⨅ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ p, ⋃ q, u' ↑p ∩ v ↑p ↑q
⊢ ∑' (p : ↑s) (x : ↑(s ∩ Ioi ↑p)), 0 = 0

Tactic:
by

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

Goal state before:
pp: u v : ℕ → ℝ≥0∞
⊢ expGrowthInf (u ⊓ v) = min (expGrowthInf u) (expGrowthInf v)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a
⊢ ∀ c ∈ u, Disjoint (B a) (B c)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Set α
hs : s.Finite
⊢ expGrowthInf (⨅ x ∈ s, u x) = ⨅ x ∈ s, expGrowthInf (u x)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
u : ι → ℕ → ℝ≥0∞
⊢ expGrowthInf (⨅ i, u i) = ⨅ i, expGrowthInf (u i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
⊢ BddAbove (δ '' A)

Tactic:
by

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

Goal state before:
pp: 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)
a : EReal
v_a : a > linearGrowthSup fun n ↦ ↑(v n)
b : EReal
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, ↑(v n) ≤ a' * ↑n
u_b : ∃ᶠ (x : ℕ) in atTop, (u x ≤ b * ↑x ∧ 0 < x) ∧ ∃ m, a⁻¹ * ↑x ≤ ↑m ∧ ↑m ≤ a'⁻¹ * ↑x
M M' : ℕ
aM_M' : a * ↑M ≤ ↑M'
n : ℕ
n_M' : M' ≤ n
un_bn : u n ≤ b * ↑n
right✝ : 0 < n
k : ℕ
an_k : ↑n ≤ a * ↑k
k_an' : a' * ↑k ≤ ↑n
vk_ak' : ↑(v k) ≤ a' * ↑k
vk_n : v k ≤ n
⊢ b * ↑n ≤ b * (a * ↑k)

Tactic:
by

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

Goal state before:
pp: u v : ℕ → ℝ≥0∞
⊢ expGrowthSup (u ⊔ v) = max (expGrowthSup u) (expGrowthSup v)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
u : ι → ℕ → ℝ≥0∞
⊢ expGrowthSup (⨆ i, u i) = ⨆ i, expGrowthSup (u i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x ↦ ⨅ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ p, ⋃ q, u' ↑p ∩ v ↑p ↑q
μt : μ t ≤ 0
⊢ ∀ᵐ (x : α) ∂μ, x ∉ t

Tactic:
by

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

Goal state before:
pp: u v : ℕ → ℝ≥0∞
⊢ expGrowthSup (u + v) = max (expGrowthSup u) (expGrowthSup v)

Tactic:
by

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:
by

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

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
v_0 : 0 < linearGrowthInf fun n ↦ ↑(v n)
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
a' : EReal
a_a' : a < a'
a_v' : a' < linearGrowthInf fun n ↦ ↑(v n)
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
⊢ ∀ᶠ (n : ℕ) in atTop, a' * ↑n ≤ ↑(v n)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
⊢ m / τ < m

Tactic:
by

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

Goal state before:
pp: u : ℕ → ℝ≥0∞
v : ℕ → ℕ
hu : 1 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
⊢ (linearGrowthInf fun n ↦ ↑(v n)) * expGrowthInf u ≤ expGrowthInf (u ∘ v)

Tactic:
by

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

Goal state before:
pp: case neg
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
v_0 : 0 < linearGrowthInf fun n ↦ ↑(v n)
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * ↑n ≤ ↑(v n)
⊢ (∀ᶠ (n : ℕ) in atTop, a' * ↑n ≤ ↑(v n)) → ∃ᶠ (n : ℕ) in atTop, a * b * ↑n ≤ (u ∘ v) n

Tactic:
rw [← frequently_imp_distrib]

Goal state after:
case neg
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
v_0 : 0 < linearGrowthInf fun n ↦ ↑(v n)
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * ↑n ≤ ↑(v n)
⊢ ∃ᶠ (x : ℕ) in atTop, a' * ↑x ≤ ↑(v x) → a * b * ↑x ≤ (u ∘ v) x
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 1 ≤ u n
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
hv₂ : Tendsto v atTop atTop
⊢ expGrowthSup (u ∘ v) ≤ (linearGrowthSup fun n ↦ ↑(v n)) * expGrowthSup u

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
⊢ ∃ a' ∈ A, m / τ ≤ δ a'

Tactic:
by

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

Goal state before:
pp: u : ℕ → ℝ≥0∞
h : Monotone u
h' : u ≠ 0
⊢ 0 ≤ expGrowthInf u

Tactic:
by

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:
by

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

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
v_0 : 0 < linearGrowthInf fun n ↦ ↑(v n)
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * ↑n ≤ ↑(v n)
b_u : ∃ᶠ (x : ℕ) in atTop, (b * ↑x ≤ u x ∧ 0 < x) ∧ ∃ m, a'⁻¹ * ↑x ≤ ↑m ∧ ↑m ≤ a⁻¹ * ↑x
M M' : ℕ
aM_M' : a' * ↑M ≤ ↑M'
n : ℕ
n_M' : M' ≤ n
bn_un : b * ↑n ≤ u n
right✝ : 0 < n
k : ℕ
an_k' : ↑n ≤ a' * ↑k
k_an : a * ↑k ≤ ↑n
ak_vk' : a' * ↑k ≤ ↑(v k)
n_vk : n ≤ v k
⊢ b * (a * ↑k) ≤ b * ↑n

Tactic:
by

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

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
⊢ (linearGrowthInf fun n ↦ ↑(v n)) * linearGrowthSup u ≤ linearGrowthSup (u ∘ v)

Tactic:
by

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

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun n ↦ ↑(v n) / ↑n) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ 0 < liminf (fun n ↦ ↑(v n) / ↑n) atTop

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
c : ι
ct : c ∈ t
b : ι
hcb : (B c ∩ B b).Nonempty
H : ∀ d ∈ u, Disjoint (B c) (B d)
a'A : b ∈ A
ha' : m / τ ≤ δ b
a'_ne_u : b ∉ u
ba'u : b ∈ insert b u
⊢ m = τ * (m / τ)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
c : ι
ct : c ∈ t
b : ι
hcb : (B c ∩ B b).Nonempty
H : ∀ d ∈ u, Disjoint (B c) (B d)
a'A : b ∈ A
ha' : m / τ ≤ δ b
a'_ne_u : b ∉ u
ba'u : b ∈ insert b u
⊢ τ * (m / τ) ≤ τ * δ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x ↦ ⨅ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ p, ⋃ q, u' ↑p ∩ v ↑p ↑q
μt : μ t ≤ 0
⊢ ∀ᵐ (x : α) ∂μ, f x = f' x

Tactic:
by

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

Goal state before:
pp: 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' : ∃ᶠ (n : ℕ) in atTop, u n ≤ 0
n : ℕ
⊢ u n ≤ 0

Tactic:
by

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

Goal state before:
pp: 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' : ∀ (n : ℕ), u n ≤ 0
⊢ linearGrowthInf u = 0

Tactic:
by

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

Goal state before:
pp: case pos
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' : ∀ (n : ℕ), u n ≤ 0
u_0' : linearGrowthInf u = 0
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u

Tactic:
u_0',

Goal state after:
case pos
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' : ∀ (n : ℕ), u n ≤ 0
u_0' : linearGrowthInf u = 0
⊢ linearGrowthInf (u ∘ v) = a * 0
Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
⊢ AEMeasurable f μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ ⨍⁻ (_x : α), 0 ∂μ = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
⊢ ⨍⁻ (x : α), f x ∂0 = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
⊢ ∃ u ⊆ t, u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ δ a ≤ τ * δ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h :
  ∀ (p q : ℝ≥0),
    p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < ↑p} ⊆ u ∧ {x | ↑q < f x} ⊆ v ∧ μ (u ∩ v) = 0
⊢ AEMeasurable f μ

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
x : ι → α
r : ι → ℝ
R τ : ℝ
hτ : 3 < τ
hr : ∀ a ∈ ∅, r a ≤ R
⊢ ∀ a ∈ ∅, ∃ b ∈ ∅, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
by

Goal state after:
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
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
s t : Set α
ht : MeasurableSet t
⊢ d s = d (s \ t) + d (s ∩ t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
f : α → ℝ≥0∞
⊢ ⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h✝ : t.Nonempty
ht : ∀ a ∈ t, r a < 0
a : ι
ha : a ∈ t
b : ι
x✝¹ : b ∈ t
x✝ : a ≠ b
⊢ Function.onFun Disjoint (fun a ↦ closedBall (x a) (r a)) a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h✝ : t.Nonempty
ht : ∀ a ∈ t, r a < 0
a : ι
ha : a ∈ t
⊢ closedBall (x a) (r a) ⊆ closedBall (x a) (τ * r a)

Tactic:
by

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

Goal state before:
pp: case a
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
⊢ a * linearGrowthInf u ≤ linearGrowthInf (u ∘ v)

Tactic:
· rw [← hv.liminf_eq]
      exact le_linearGrowthInf_comp h' v_top

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h✝ : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
⊢ 1 < (τ - 1) / 2

Tactic:
by

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

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun n ↦ ↑(v n) / ↑n) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u

Tactic:
by

Goal state after: