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

Goal state before:
pp: u v : ℕ → EReal
h : ∃ᶠ (n : ℕ) in atTop, u n ≤ v n
n : ℕ
u_v : u n ≤ v n
⊢ u n / ↑n ≤ v n / ↑n

Tactic:
gcongr

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

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

Tactic:
log_rpow,

Goal state after:
x : ℝ≥0∞
n : ℕ
⊢ ↑↑n * x.log = ↑n * x.log
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
a : EReal
h : ∃ᶠ (n : ℕ) in atTop, u n ≤ a * ↑n
c : EReal
c_u : c > a
n : ℕ
hn : u n ≤ a * ↑n
⊢ a * ↑n ≤ c * ↑n

Tactic:
gcongr

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

Goal state before:
pp: u : ℕ → EReal
a : EReal
h : ∀ᶠ (n : ℕ) in atTop, a * ↑n ≤ u n
c : EReal
c_u : c < a
n : ℕ
hn : a * ↑n ≤ u n
⊢ c * ↑n ≤ a * ↑n

Tactic:
gcongr

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

Goal state before:
pp: u : ℕ → EReal
a : EReal
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ a * ↑n
c : EReal
c_u : c > a
n : ℕ
hn : u n ≤ a * ↑n
⊢ a * ↑n ≤ c * ↑n

Tactic:
gcongr

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

Goal state before:
pp: u : ℕ → EReal
a : EReal
h : ∃ᶠ (n : ℕ) in atTop, a * ↑n ≤ u n
c : EReal
c_u : c < a
n : ℕ
hn : a * ↑n ≤ u n
⊢ c * ↑n ≤ a * ↑n

Tactic:
gcongr

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

Goal state before:
pp: u v : ℕ → ℝ≥0∞
h : ∃ᶠ (n : ℕ) in atTop, u n ≤ v n
n : ℕ
u_v : u n ≤ v n
⊢ (u n).log / ↑n ≤ (v n).log / ↑n

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : CommSemiring β
inst✝² : PartialOrder β
inst✝¹ : IsOrderedRing β
inst✝ : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
x : α
hx : g x ≤ f x
hx' : 0 ≤ k x
⊢ k x ^ z * g x ≤ k x ^ z * f x

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : CommSemiring β
inst✝² : PartialOrder β
inst✝¹ : IsOrderedRing β
inst✝ : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
x : α
hx : f x ≤ g' x
hx' : 0 ≤ k x
⊢ k x ^ z * f x ≤ k x ^ z * g' x

Tactic:
gcongr

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

Goal state before:
pp: u : ℕ → ℝ≥0∞
a : EReal
h : ∃ᶠ (n : ℕ) in atTop, u n ≤ (a * ↑n).exp
c : EReal
c_u : c > a
n : ℕ
hn : u n ≤ (a * ↑n).exp
⊢ (a * ↑n).exp ≤ (c * ↑n).exp

Tactic:
gcongr

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

Goal state before:
pp: u : ℕ → ℝ≥0∞
a : EReal
h : ∀ᶠ (n : ℕ) in atTop, (a * ↑n).exp ≤ u n
c : EReal
c_u : c < a
n : ℕ
hn : (a * ↑n).exp ≤ u n
⊢ (c * ↑n).exp ≤ (a * ↑n).exp

Tactic:
gcongr

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

Goal state before:
pp: u : ℕ → ℝ≥0∞
a : EReal
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ (a * ↑n).exp
c : EReal
c_u : c > a
n : ℕ
hn : u n ≤ (a * ↑n).exp
⊢ (a * ↑n).exp ≤ (c * ↑n).exp

Tactic:
gcongr

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

Goal state before:
pp: u : ℕ → ℝ≥0∞
a : EReal
h : ∃ᶠ (n : ℕ) in atTop, (a * ↑n).exp ≤ u n
c : EReal
c_u : c < a
n : ℕ
hn : (a * ↑n).exp ≤ u n
⊢ (c * ↑n).exp ≤ (a * ↑n).exp

Tactic:
gcongr

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

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
a : EReal
x✝¹ : a ∈ Set.Ioo 0 (linearGrowthInf fun n ↦ ↑(v n))
b : EReal
x✝ : b ∈ Set.Ioo 0 (linearGrowthInf u)
left✝ : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b_0 : 0 < b
b_u : b < linearGrowthInf u
b_uv : ∀ᶠ (a : ℕ) in atTop, b * ↑(v a) ≤ u (v a)
n : ℕ
b_uvn : b * ↑(v n) ≤ u (v n)
n_0 : 0 < n
a_vn : a * ↑n ≤ ↑(v n)
⊢ b * (a * ↑n) ≤ b * ↑(v n)

Tactic:
gcongr

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

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
hv₂ : Tendsto v atTop atTop
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
a : EReal
v_a : a > linearGrowthSup fun n ↦ ↑(v n)
b : EReal
u_b : b > linearGrowthSup u
b_0 : 0 ≤ b
uv_b : ∀ᶠ (n : ℕ) in atTop, u (v n) ≤ b * ↑(v n)
n : ℕ
uvn_b : u (v n) ≤ b * ↑(v n)
n_0 : 0 < n
vn_a : ↑(v n) ≤ a * ↑n
⊢ b * ↑(v n) ≤ b * (a * ↑n)

Tactic:
gcongr

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:
exact le_top

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) ≤ ⊤

Tactic:
exact le_top

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' : ↑M ≤ a⁻¹ * ↑M'
n : ℕ
n_M' : M' ≤ n
un_bn : u n ≤ b * ↑n
right✝ : 0 < n
k : ℕ
an_k : a⁻¹ * ↑n ≤ ↑k
k_an' : ↑k ≤ a'⁻¹ * ↑n
⊢ a⁻¹ * ↑M' ≤ a⁻¹ * ↑n

Tactic:
gcongr

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

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

Goal state before:
pp: case inl
α : 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
mzero : 0 = m
⊢ ∃ a' ∈ A, m / τ ≤ δ a'

Tactic:
refine ⟨a, ⟨hat, a_disj⟩, ?_⟩
      simpa only [← mzero, zero_div] using δnonneg a hat

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:
apply le_linearGrowthInf_comp (hu.mono fun n h ↦ ?_) hv

Goal state after:
u : ℕ → ℝ≥0∞
v : ℕ → ℕ
hu : 1 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
n : ℕ
h : 1 n ≤ u n
⊢ 0 n ≤ (u n).log
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 * 1 < m * τ

Tactic:
gcongr

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

Goal state before:
pp: u : ℕ → ℝ≥0∞
v : ℕ → ℕ
hu : 1 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
n : ℕ
h : 1 ≤ u n
⊢ 0 n ≤ (u n).log

Tactic:
rwa [Pi.zero_apply, zero_le_log_iff]

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' : ↑M ≤ a'⁻¹ * ↑M'
n : ℕ
n_M' : M' ≤ n
bn_un : b * ↑n ≤ u n
right✝ : 0 < n
k : ℕ
an_k' : a'⁻¹ * ↑n ≤ ↑k
k_an : ↑k ≤ a⁻¹ * ↑n
⊢ a'⁻¹ * ↑M' ≤ a'⁻¹ * ↑n

Tactic:
gcongr

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

Goal state before:
pp: case refine_3
α : 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)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : a' ∉ u
c : ι
ct : c ∈ t
b : ι
ba'u : b ∈ insert a' u
⊢ (B c ∩ B b).Nonempty → ∃ c_1 ∈ insert a' u, (B c ∩ B c_1).Nonempty ∧ δ c ≤ τ * δ c_1

Tactic:
hcb

Goal state after:
case refine_3
α : 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)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : a' ∉ u
c : ι
ct : c ∈ t
b : ι
ba'u : b ∈ insert a' u
hcb : (B c ∩ B b).Nonempty
⊢ ∃ c_1 ∈ insert a' u, (B c ∩ B c_1).Nonempty ∧ δ c ≤ τ * δ c_1
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:
gcongr

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

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
⊢ ⨍⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α), f x ∂(μ s)⁻¹ • μ.restrict s

Tactic:
simp only [laverage_eq', restrict_apply_univ]

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
a : ι
hav : a ∈ v
⊢ B a ∩ ball x (R x) ⊆ closedBall (c a) (r a) ∩ closedBall x (R x)

Tactic:
gcongr

Goal state after:
case h₁
α : 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 ι := ⋯
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 ι := ⋯
vu : v ⊆ u
a : ι
hav : a ∈ v
⊢ B a ⊆ closedBall (c a) (r a)

case h₂
α : 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 ι := ⋯
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 ι := ⋯
vu : v ⊆ u
a : ι
hav : a ∈ v
⊢ ball x (R x) ⊆ closedBall x (R 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)) < ∞
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) < ∞
w : Finset ↑v
hw : ∑' (a : { a // a ∉ w }), μ (B ↑↑a) < ε / ↑C
k : Set α := ⋃ a ∈ w, B ↑a
k_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] k
d : ℝ
dpos : 0 < d
a : ι
hat : a ∈ t
hz : c a ∈ (s \ ⋃ a ∈ u, B a) ∩ ball x (R x)
z_notmem_k : c a ∉ k
this : ball x (R x) \ k ∈ 𝓝 (c a)
hd : closedBall (c a) d ⊆ ball x (R x) \ k
ad : r a ≤ min d (R (c a))
⊢ closedBall (c a) (r a) ⊆ closedBall (c a) d

Tactic:
gcongr

Goal state after:
case h
α : 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 ι := ⋯
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 ι := ⋯
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) < ∞
w : Finset ↑v
hw : ∑' (a : { a // a ∉ w }), μ (B ↑↑a) < ε / ↑C
k : Set α := ⋯
k_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] k
d : ℝ
dpos : 0 < d
a : ι
hat : a ∈ t
hz : c a ∈ (s \ ⋃ a ∈ u, B a) ∩ ball x (R x)
z_notmem_k : c a ∉ k
this : ball x (R x) \ k ∈ 𝓝 (c a)
hd : closedBall (c a) d ⊆ ball x (R x) \ k
ad : r a ≤ min d (R (c a))
⊢ r a ≤ d
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case right
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
x✝ : MeasurableSet s
hνs : (μ.withDensity (ν.rnDeriv μ)) s = 0
t : Set α
left✝ : MeasurableSet t
ht1 : (ν.singularPart μ) t = 0
ht2 : μ tᶜ = 0
⊢ μ (s ∩ tᶜ) = 0

Tactic:
exact measure_mono_null Set.inter_subset_right ht2

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
d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋃ n, s n)))
d_Inter :
  ∀ (s : ℕ → Set α),
    (∀ (n : ℕ), MeasurableSet (s n)) →
      (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋂ n, s n)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
this : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)
f : ℕ → ℕ → Set α := fun n m ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
f_subset_f : ∀ {a b c d : ℕ}, a ≤ b → c ≤ d → f a d ⊆ f b c
f_succ : ∀ (n m : ℕ), n ≤ m → f n (m + 1) = f n m ∩ e (m + 1)
le_d_f : ∀ (n m : ℕ), m ≤ n → γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
s : Set α := ⋃ m, ⋂ n, f m n
γ_le_d_s : γ ≤ d s
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ sᶜ
⊢ γ + d t ≤ d s + d t

Tactic:
gcongr

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) < ∞
w : Finset ↑v
hw : ∑' (a : { a // a ∉ w }), μ (B ↑↑a) < ε / ↑C
M : (s \ ⋃ a ∈ u, B a) ∩ ball x (R x) ⊆ ⋃ a, closedBall (c ↑↑a) (3 * r ↑↑a)
this : Countable ↑v
⊢ ↑C * ∑' (a : { a // a ∉ w }), μ (B ↑↑a) ≤ ↑C * (ε / ↑C)

Tactic:
gcongr

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst✝¹ : μ₁.HaveLebesgueDecomposition ν
inst✝ : μ₂.HaveLebesgueDecomposition ν
⊢ μ₁ + μ₂ = μ₁ + (ν.withDensity (μ₂.rnDeriv ν) + μ₂.singularPart ν)

Tactic:
add_comm (ν.withDensity (μ₂.rnDeriv ν)),

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst✝¹ : μ₁.HaveLebesgueDecomposition ν
inst✝ : μ₂.HaveLebesgueDecomposition ν
⊢ μ₁ + μ₂ = μ₁ + (μ₂.singularPart ν + ν.withDensity (μ₂.rnDeriv ν))
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 μ
C : ℝ≥0
h : ∀ (x : α), ∃ᶠ (r : ℝ) in 𝓝[>] 0, μ (closedBall x (3 * r)) ≤ ↑C * μ (closedBall x r)
x : α
ε : ℝ
εpos : ε > 0
r : ℝ
μr : μ (closedBall x (3 * r)) ≤ ↑C * μ (closedBall x r)
rpos : 0 < r
rε : r ≤ ε
⊢ closedBall x r ⊆ closedBall x ε

Tactic:
gcongr

Goal state after: