mathlib-initiative/mathlib-tactics huggingface dataset:
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 : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesWithinOnBall f p s x r
⊢ (∑ σ_1, (p n) fun i ↦ (v ∘ ⇑σ) (σ_1 i)) = ∑ σ, (p n) fun i ↦ v (σ i)

Tactic:
conv_rhs => rw [← Equiv.sum_comp (Equiv.mulLeft σ)]

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
f : E → F
s : Set E
x : E
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesWithinOnBall f p s x r
⊢ (∑ σ_1, (p n) fun i ↦ (v ∘ ⇑σ) (σ_1 i)) = ∑ i, (p n) fun i_1 ↦ v (((Equiv.mulLeft σ) i) i_1)
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case bot
⊢ ∃ a, a.log = ⊥

Tactic:
use 0

Goal state after:
case h
⊢ log 0 = ⊥
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
a : EReal
⊢ linearGrowthInf u ≤ a ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ b * ↑n

Tactic:
linearGrowthInf,

Goal state after:
u : ℕ → EReal
a : EReal
⊢ liminf (fun n ↦ u n / ↑n) atTop ≤ a ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ b * ↑n
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inl.inr.inr
x : ℝ≥0∞
y : ℝ
y_neg : y < 0
x_real : 0 < x.toReal
⊢ (x ^ y).log = ↑y * x.log

Tactic:
have x_ne_zero := (ENNReal.toReal_pos_iff.1 x_real).1.ne'

Goal state after:
case inl.inr.inr
x : ℝ≥0∞
y : ℝ
y_neg : y < 0
x_real : 0 < x.toReal
x_ne_zero : x ≠ 0
⊢ (x ^ y).log = ↑y * x.log
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
a : EReal
⊢ a ≤ linearGrowthInf u ↔ ∀ b < a, ∀ᶠ (n : ℕ) in atTop, b * ↑n ≤ u n

Tactic:
linearGrowthInf,

Goal state after:
u : ℕ → EReal
a : EReal
⊢ a ≤ liminf (fun n ↦ u n / ↑n) atTop ↔ ∀ b < a, ∀ᶠ (n : ℕ) in atTop, b * ↑n ≤ u n
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inr.inr.inr
x : ℝ≥0∞
y : ℝ
y_pos : 0 < y
x_real : 0 < x.toReal
⊢ (x ^ y).log = ↑y * x.log

Tactic:
have x_ne_zero := (ENNReal.toReal_pos_iff.1 x_real).1.ne'

Goal state after:
case inr.inr.inr.inr
x : ℝ≥0∞
y : ℝ
y_pos : 0 < y
x_real : 0 < x.toReal
x_ne_zero : x ≠ 0
⊢ (x ^ y).log = ↑y * x.log
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: x : ℝ≥0∞
⊢ x⁻¹.log = -x.log

Tactic:
by
  simp [← rpow_neg_one, log_rpow]

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

Goal state before:
pp: ⊢ linearGrowthSup ⊥ = ⊥

Tactic:
nth_rw 2 [← limsup_const (f := atTop (α := ℕ)) ⊥]
  refine limsup_congr <| (eventually_gt_atTop 0).mono fun n n_pos ↦ ?_
  exact bot_div_of_pos_ne_top (by positivity) (natCast_ne_top n)

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

Goal state before:
pp: u : ℕ → EReal
⊢ linearGrowthSup (-u) = -linearGrowthInf u

Tactic:
linearGrowthInf,

Goal state after:
u : ℕ → EReal
⊢ linearGrowthSup (-u) = -liminf (fun n ↦ u n / ↑n) atTop
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝³ : TopologicalSpace β
inst✝² : CommSemiring β
inst✝¹ : ContinuousAdd β
inst✝ : ContinuousMul β
hf : SuperpolynomialDecay l k f
p✝ p q : β[X]
hp : SuperpolynomialDecay l k fun x ↦ eval (k x) p * f x
hq : SuperpolynomialDecay l k fun x ↦ eval (k x) q * f x
⊢ SuperpolynomialDecay l k fun x ↦ eval (k x) (p + q) * f x

Tactic:
by simpa [add_mul] using! hp.add hq

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

Goal state before:
pp: α : 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
⊢ ∀ (n : ℕ), Tendsto (fun a ↦ |k a ^ n * g a|) l (𝓝 0)

Tactic:
refine fun z =>
    tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds (hf z)
      (Eventually.of_forall fun x => abs_nonneg _) (hfg.mono fun x hx => ?_)

Goal state after:
α : 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
⊢ |k x ^ z * g x| ≤ |k x ^ z * f x|
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun a ↦ |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun a ↦ |k a ^ (z + 1) * f a|) l, (fun x1 x2 ↦ x1 ≤ x2) x m
h1 : Tendsto (fun x ↦ 0) l (𝓝 0)
h2 : Tendsto (fun a ↦ |(k a)⁻¹| * m) l (𝓝 0)
⊢ Tendsto (fun a ↦ |k a ^ z * f a|) l (𝓝 0)

Tactic:
refine
    tendsto_of_tendsto_of_tendsto_of_le_of_le' h1 h2 (Eventually.of_forall fun x => abs_nonneg _)
      ((eventually_map.1 hm).mp ?_)

Goal state after:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun a ↦ |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun a ↦ |k a ^ (z + 1) * f a|) l, (fun x1 x2 ↦ x1 ≤ x2) x m
h1 : Tendsto (fun x ↦ 0) l (𝓝 0)
h2 : Tendsto (fun a ↦ |(k a)⁻¹| * m) l (𝓝 0)
⊢ ∀ᶠ (x : α) in l, (fun x1 x2 ↦ x1 ≤ x2) |k x ^ (z + 1) * f x| m → |k x ^ z * f x| ≤ |(k x)⁻¹| * m
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
⊢ linearGrowthInf (u ⊓ v) = min (linearGrowthInf u) (linearGrowthInf v)

Tactic:
linearGrowthInf,

Goal state after:
u v : ℕ → EReal
⊢ liminf (fun n ↦ (u ⊓ v) n / ↑n) atTop = min (linearGrowthInf u) (linearGrowthInf v)
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
⊢ liminf (fun n ↦ (u ⊓ v) n / ↑n) atTop = min (linearGrowthInf u) (linearGrowthInf v)

Tactic:
linearGrowthInf,

Goal state after:
u v : ℕ → EReal
⊢ liminf (fun n ↦ (u ⊓ v) n / ↑n) atTop = min (liminf (fun n ↦ u n / ↑n) atTop) (linearGrowthInf v)
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
⊢ liminf (fun n ↦ (u ⊓ v) n / ↑n) atTop = min (liminf (fun n ↦ u n / ↑n) atTop) (linearGrowthInf v)

Tactic:
linearGrowthInf,

Goal state after:
u v : ℕ → EReal
⊢ liminf (fun n ↦ (u ⊓ v) n / ↑n) atTop = min (liminf (fun n ↦ u n / ↑n) atTop) (liminf (fun n ↦ v n / ↑n) atTop)
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
n : ℕ
⊢ (u⁻¹ n).log / ↑n = (-fun n ↦ (u n).log / ↑n) n

Tactic:
rw [Pi.neg_apply, Pi.inv_apply, div_eq_mul_inv, div_eq_mul_inv, ← EReal.neg_mul, log_inv]

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)
⊢ False

Tactic:
obtain ⟨a', a'A, ha'⟩ : ∃ a' ∈ A, m / τ ≤ δ a' := by
    have : 0 ≤ m := (δnonneg a hat).trans (le_csSup bddA (mem_image_of_mem _ ⟨hat, a_disj⟩))
    rcases eq_or_lt_of_le this with (mzero | mpos)
    · refine ⟨a, ⟨hat, a_disj⟩, ?_⟩
      simpa only [← mzero, zero_div] using δnonneg a hat
    · have I : m / τ < m := by
        rw [div_lt_iff₀ (zero_lt_one.trans hτ)]
        conv_lhs => rw [← mul_one m]
        gcongr
      rcases exists_lt_of_lt_csSup (Anonempty.image _) I with ⟨x, xA, hx⟩
      rcases (mem_image _ _ _).1 xA with ⟨a', ha', rfl⟩
      exact ⟨a', ha', hx.le⟩

Goal state after:
α : 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'A : a' ∈ A
ha' : m / τ ≤ δ a'
⊢ False
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 = ⊥
u_1 : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u

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:
· have u_0' : linearGrowthSup u = 0 := by
      apply le_antisymm _ (h.linearGrowthSup_nonneg u_0)
      apply (linearGrowthSup_eventually_monotone u_1).trans_eq
      exact (linearGrowthSup_const zero_ne_bot zero_ne_top)
    rw [u_0', mul_zero]
    apply le_antisymm _ (linearGrowthSup_comp_nonneg h u_0 v_top)
    apply (linearGrowthSup_eventually_monotone (v_top.eventually u_1)).trans_eq
    exact linearGrowthSup_const zero_ne_bot zero_ne_top

Goal state after:
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
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 ∂μ
A : ∀ (ε N : ℝ≥0) (p : ℕ), 0 < ε → μ ({x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p) = 0
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : ℕ → Set α := ⋯
μs : ∀ (n : ℕ), μ (s n) = 0
x : α
hx : g x < f x
L1 : ∀ᶠ (n : ℕ) in atTop, g x + ↑(u n) ≤ f x
L2 : ∀ᶠ (n : ℕ) in atTop, g x ≤ ↑↑n
⊢ ∃ i, x ∈ s i

Tactic:
exact ((L1.and L2).and (eventually_mem_spanningSets μ x)).exists

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 < τ
⊢ ∃ u ⊆ t, (u.PairwiseDisjoint fun a ↦ ball (x a) (r a)) ∧ ∀ a ∈ t, ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b)

Tactic:
by
  rcases eq_empty_or_nonempty t with (rfl | _)
  · exact ⟨∅, Subset.refl _, pairwiseDisjoint_empty, by simp⟩
  by_cases! ht : ∀ a ∈ t, r a ≤ 0
  · exact ⟨t, Subset.rfl, fun a ha b _ _ => by
      simp only [ball_eq_empty.2 (ht a ha), empty_disjoint, Function.onFun],
      fun a ha => ⟨a, ha, by simp only [ball_eq_empty.2 (ht a ha), empty_subset]⟩⟩
  let t' := { a ∈ t | 0 < r a }
  rcases exists_disjoint_subfamily_covering_enlargement (fun a => ball (x a) (r a)) t' r
      ((τ - 1) / 2) (by linarith) (fun a ha => ha.2.le) R (fun a ha => hr a ha.1) fun a ha =>
      ⟨x a, mem_ball_self ha.2⟩ with
    ⟨u, ut', u_disj, hu⟩
  have A : ∀ a ∈ t', ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b) := by
    intro a ha
    rcases hu a ha with ⟨b, bu, hb, rb⟩
    refine ⟨b, bu, ?_⟩
    have : dist (x a) (x b) < r a + r b := dist_lt_add_of_nonempty_ball_inter_ball hb
    apply ball_subset_ball'
    linarith
  refine ⟨u, ut'.trans fun a ha => ha.1, u_disj, fun a ha => ?_⟩
  rcases lt_or_ge 0 (r a) with (h'a | h'a)
  · exact A a ⟨ha, h'a⟩
  · rcases ht with ⟨b, rb⟩
    rcases A b ⟨rb.1, rb.2⟩ with ⟨c, cu, _⟩
    exact ⟨c, cu, by simp only [ball_eq_empty.2 h'a, empty_subset]⟩

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
n m : ℕ
hnm : n ≤ m
this : n ≤ m + 1
⊢ f n (m + 1) = f n m ∩ e (m + 1)

Tactic:
simp_rw [f, ← Finset.insert_Ico_right_eq_Ico_add_one this, Finset.inf_insert,
      Set.inter_comm]

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 ≠ ∞
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
n m : ℕ
hnm : n ≤ m
this : n ≤ m + 1
⊢ e (m + 1) ⊓ (Finset.Ico n (m + 1)).inf e = e (m + 1) ∩ (Finset.Ico n (m + 1)).inf e
Module: Mathlib.MeasureTheory.Measure.Sub

Goal state before:
pp: case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x ↦ μ t - ν t) ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
d : Measure α
h_d : d ∈ {d | μ ≤ d + ν}
⊢ measure_sub ≤ d

Tactic:
rw [← h_measure_sub_add, mem_ofPred_eq, add_comm d] at h_d

Goal state after:
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x ↦ μ t - ν t) ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
d : Measure α
h_d : ν + measure_sub ≤ ν + d
⊢ measure_sub ≤ d
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hs : NullMeasurableSet s μ
hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
⊢ 0 < μ {x | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x}

Tactic:
obtain hμ₁ | hμ₁ := eq_or_ne (μ s) ∞
  · simp [setLAverage_eq, hμ₁]
  obtain ⟨g, hg, hgf, hfg⟩ := exists_measurable_le_lintegral_eq (μ.restrict s) f
  have hfg' : ⨍⁻ a in s, f a ∂μ = ⨍⁻ a in s, g a ∂μ := by simp_rw [laverage_eq, hfg]
  rw [hfg] at hint
  have :=
    measure_setAverage_le_pos hμ hμ₁ (integrable_toReal_of_lintegral_ne_top hg.aemeasurable hint)
  simp_rw [← ofPred_inter_eq_sep, ← Measure.restrict_apply₀' hs, hfg']
  rw [← ofPred_inter_eq_sep, ← Measure.restrict_apply₀' hs, ←
    measure_sdiff_null (measure_eq_top_of_lintegral_ne_top hg.aemeasurable hint)] at this
  refine this.trans_le (measure_mono ?_)
  rintro x ⟨hfx, hx⟩
  dsimp at hfx
  rw [← toReal_laverage hg.aemeasurable, toReal_le_toReal (setLAverage_lt_top hint).ne hx] at hfx
  · exact hfx.trans (hgf _)
  · simp_rw [ae_iff, not_ne_iff]
    exact measure_eq_top_of_lintegral_ne_top hg.aemeasurable hint

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h✝ : ¬μ ⟂ₘ ν
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ f n) ≤ μ (t ∩ f n)
hf₃ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ (f n)ᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ (f n)ᶜ)
A : Set α := ⋂ n, (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ A) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A)
μA νA : ℝ≥0
hA₃ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ↑νA
hb : 0 < νA
this : ∀ (b : ℝ≥0), 0 < b → μA ≤ b
h : ¬μA = 0
⊢ False

Tactic:
have h' := this (μA / 2) (half_pos (zero_lt_iff.2 h))

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h✝ : ¬μ ⟂ₘ ν
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ f n) ≤ μ (t ∩ f n)
hf₃ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ (f n)ᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ (f n)ᶜ)
A : Set α := ⋂ n, (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ A) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A)
μA νA : ℝ≥0
hA₃ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ↑νA
hb : 0 < νA
this : ∀ (b : ℝ≥0), 0 < b → μA ≤ b
h : ¬μA = 0
h' : μA ≤ μA / 2
⊢ False
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ ε > 0, ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a
x : α
hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
z : ℝ≥0∞
hz : z > 0
w : ℝ≥0
w_pos : 0 < ↑w
w_lt : ↑w < z
n : ℕ
hn : u n < w
a : Set α
ha : ρ a < ↑(u n) * μ a
μa_pos : 0 < μ a
μa_lt_top : μ a < ∞
⊢ ↑(u n) * μ a ≤ z * μ a

Tactic:
hn,

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ ε > 0, ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a
x : α
hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
z : ℝ≥0∞
hz : z > 0
w : ℝ≥0
w_pos : 0 < ↑w
w_lt : ↑w < z
n : ℕ
hn : u n < w
a : Set α
ha : ρ a < ↑(u n) * μ a
μa_pos : 0 < μ a
μa_lt_top : μ a < ∞
⊢ ↑w * μ a ≤ z * μ a
Module: Mathlib.MeasureTheory.Covering.OneDim

Goal state before:
pp: x y : ℝ
hxy : x < y
⊢ Icc x y ∈ (vitaliFamily volume 1).setsAt x

Tactic:
rw [Icc_eq_closedBall]
  refine closedBall_mem_vitaliFamily_of_dist_le_mul _ ?_ (by linarith)
  rw [dist_comm, Real.dist_eq, abs_of_nonneg] <;> linarith

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

Goal state before:
pp: case hc
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
c : ℝ≥0
hc : ↑c ∈ w
d : ℝ≥0
hd : ↑d ∈ w
hcd : ↑c < ↑d
⊢ ∀ (x : α),
    (∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < ↑c) →
      (∃ᶠ (x : Set α) in v.filterAt x, ↑d < ρ x / μ x) → ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ↑c * μ a

Tactic:
intro x h1x _

Goal state after:
case hc
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
c : ℝ≥0
hc : ↑c ∈ w
d : ℝ≥0
hd : ↑d ∈ w
hcd : ↑c < ↑d
x : α
h1x : ∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < ↑c
a✝ : ∃ᶠ (x : Set α) in v.filterAt x, ↑d < ρ x / μ x
⊢ ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ↑c * μ a
Module: Mathlib.Analysis.Calculus.Monotone

Goal state before:
pp: f : StieltjesFunction ℝ
x : ℝ
hx : Tendsto (fun a ↦ f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
h'x : f.measure.rnDeriv volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 : Tendsto (fun y ↦ (↑f y - ↑f x) / (y - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
⊢ HasDerivAt (↑f) (f.measure.rnDeriv volume x).toReal x

Tactic:
have L2 : Tendsto (fun y => (leftLim f y - f x) / (y - x)) (𝓝[<] x)
      (𝓝 (rnDeriv f.measure volume x).toReal) := by
    apply Tendsto.congr' _
      ((ENNReal.tendsto_toReal h'x.ne).comp (hx.comp (Real.tendsto_Icc_vitaliFamily_left x)))
    filter_upwards [self_mem_nhdsWithin]
    rintro y (hxy : y < x)
    simp only [comp_apply, StieltjesFunction.measure_Icc, Real.volume_Icc]
    rw [← ENNReal.ofReal_div_of_pos (sub_pos.2 hxy), ENNReal.toReal_ofReal, ← neg_neg (y - x),
      div_neg, neg_div', neg_sub, neg_sub]
    exact div_nonneg (sub_nonneg.2 (f.mono.leftLim_le hxy.le)) (sub_pos.2 hxy).le

Goal state after:
f : StieltjesFunction ℝ
x : ℝ
hx : Tendsto (fun a ↦ f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
h'x : f.measure.rnDeriv volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 : Tendsto (fun y ↦ (↑f y - ↑f x) / (y - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L2 : Tendsto (fun y ↦ (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
⊢ HasDerivAt (↑f) (f.measure.rnDeriv volume x).toReal x