mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hfg : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = g x_1
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (fun z ↦ z - x) x
z : 𝕜
hz : z ∈ {x}ᶜ → f z = g z
hn : z ≠ x
⊢ (z - x) • (z - x) ^ m • g z = (z - x) ^ (m + 1) • g z

Tactic:
pow_succ',

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hfg : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = g x_1
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (fun z ↦ z - x) x
z : 𝕜
hz : z ∈ {x}ᶜ → f z = g z
hn : z ≠ x
⊢ (z - x) • (z - x) ^ m • g z = ((z - x) * (z - x) ^ m) • g z
Module: Mathlib.Analysis.Calculus.Deriv.Prod

Goal state before:
pp: case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_1
E' : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x ↦ φ x i) s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin φ s x = fun i ↦ derivWithin (fun x ↦ φ x i) s x

Tactic:
· rw [uniqueDiffWithinAt_iff_accPt] at hsx
    simp [derivWithin, fderivWithin_zero_of_not_accPt hsx, Pi.zero_def]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
k : ℕ
⊢ multichoose 1 k = 1

Tactic:
induction k with
  | zero => exact multichoose_zero_right 1
  | succ n ih =>
    rw [show (1 : R) = 0 + 1 by exact (@zero_add R _ 1).symm, multichoose_succ_succ,
      multichoose_zero_succ, zero_add, zero_add, ih]

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

Goal state before:
pp: x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y ↦ (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1))) ((r + 1) * (-↑x) ^ r * cexp (↑π * I * r)) x
| (r + 1) * (-↑x) ^ r * cexp (↑π * I * r) / (r + 1)

Tactic:
rw [mul_assoc, mul_comm, mul_div_cancel_right₀ _ hr]

Goal state after:
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y ↦ (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1))) ((r + 1) * (-↑x) ^ r * cexp (↑π * I * r)) x
| (-↑x) ^ r * cexp (↑π * I * r)
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: 𝕂 : Type v
inst✝² : RCLike 𝕂
𝔸 : Type u
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ ↑k
⊢ (binomialSeries 𝔸 a).radius = 1

Tactic:
simp only [binomialSeries_eq_ordinaryHypergeometricSeries (b := (1 : 𝕂)) (by norm_cast; simp),
    FormalMultilinearSeries.radius_compNeg]
  conv at ha => ext; rw [ne_comm]
  exact ordinaryHypergeometricSeries_radius_eq_one _ _ _ _ (by norm_cast; grind)

Goal state after:
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
hmul : ↑ε < edist (f x) (f y) * ↑K₁
⊢ ↑(ε / K₁) < edist (f x) (f y)

Tactic:
exact ENNReal.coe_div hK₁.ne' ▸ ENNReal.div_lt_of_lt_mul hmul

Goal state after:
Module: Mathlib.Topology.MetricSpace.Cover

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε
N : Set X
hNA : N ⊆ s
hN_finite : N.Finite
hN : s ⊆ ⋃ y ∈ N, eball y ↑ε
x : X
hx : x ∈ ⋃ y ∈ N, eball y ↑ε
⊢ x ∈ ⋃ y ∈ N, closedEBall y ↑ε

Tactic:
simp only [Set.mem_iUnion, Metric.mem_eball, exists_prop, Metric.mem_closedEBall] at hx ⊢

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε
N : Set X
hNA : N ⊆ s
hN_finite : N.Finite
hN : s ⊆ ⋃ y ∈ N, eball y ↑ε
x : X
hx : ∃ i ∈ N, edist x i < ↑ε
⊢ ∃ i ∈ N, edist x i ≤ ↑ε
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : CommRing β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
⊢ (∀ (n : ℕ), Tendsto (fun a ↦ |k a ^ n * f a|) l (𝓝 0)) ↔ SuperpolynomialDecay l (fun a ↦ |k a|) fun a ↦ |f a|

Tactic:
SuperpolynomialDecay,

Goal state after:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : CommRing β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
⊢ (∀ (n : ℕ), Tendsto (fun a ↦ |k a ^ n * f a|) l (𝓝 0)) ↔ ∀ (n : ℕ), Tendsto (fun a ↦ |k a| ^ n * |f a|) l (𝓝 0)
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)
x : α
hk0 : k x ≠ 0
hx : (fun x1 x2 ↦ x1 ≤ x2) |k x ^ (z + 1) * f x| m
⊢ |k x ^ z * f x| = |(k x)⁻¹ * k x ^ (z + 1) * f x|

Tactic:
pow_succ',

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 : α
hk0 : k x ≠ 0
hx : (fun x1 x2 ↦ x1 ≤ x2) |k x ^ (z + 1) * f x| m
⊢ |k x ^ z * f x| = |(k x)⁻¹ * (k x * k x ^ z) * f x|
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

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

Tactic:
by
  apply expGrowthInf_le_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans ?_
  gcongr

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

Goal state before:
pp: ⊢ log ∘ 0 = ⊥

Tactic:
ext _

Goal state after:
x✝ : ℕ
⊢ (log ∘ 0) x✝ = ⊥ x✝
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case neg.inr.refine_1
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 : a⁻¹ * ↑n ≤ ↑k
k_an' : ↑k ≤ a'⁻¹ * ↑n
⊢ M ≤ k

pp: case neg.inr.refine_2
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 : a⁻¹ * ↑n ≤ ↑k
k_an' : ↑k ≤ a'⁻¹ * ↑n
vk_ak' : ↑(v k) ≤ a' * ↑k
⊢ (u ∘ v) k ≤ a * b * ↑k

Tactic:
· rw [mul_comm a, ← le_div_iff_mul_le a_0 a_top, EReal.div_eq_inv_mul] at aM_M'
    apply Nat.cast_le.1 <| aM_M'.trans <| an_k.trans' _
    gcongr

Goal state after:
case neg.inr.refine_2
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 : a⁻¹ * ↑n ≤ ↑k
k_an' : ↑k ≤ a'⁻¹ * ↑n
vk_ak' : ↑(v k) ≤ a' * ↑k
⊢ (u ∘ v) k ≤ a * b * ↑k
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: case inl
α : 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
Idist_v : ∀ a ∈ v, dist (c a) x ≤ r a + R x
R0 : ℝ := sSup (r '' v)
R0_def : R0 = sSup (r '' v)
R0_bdd : BddAbove (r '' v)
H : R0 ≤ R x
⊢ ∃ K, μ (closedBall x K) < ∞ ∧ ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K

Tactic:
refine ⟨20 * R x, hRμ x, fun a au hax => ?_⟩

Goal state after:
case inl
α : 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
Idist_v : ∀ a ∈ v, dist (c a) x ≤ r a + R x
R0 : ℝ := sSup (r '' v)
R0_def : R0 = sSup (r '' v)
R0_bdd : BddAbove (r '' v)
H : R0 ≤ R x
a : ι
au : a ∈ u
hax : (B a ∩ ball x (R x)).Nonempty
⊢ B a ⊆ closedBall x (20 * R x)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
r : ℝ≥0∞
⊢ ∃ p, Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ r • μ = p.1 + ν.withDensity p.2

Tactic:
obtain ⟨hmeas, hsing, hadd⟩ := haveLebesgueDecomposition_spec μ ν

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
r : ℝ≥0∞
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ ∃ p, Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ r • μ = p.1 + ν.withDensity p.2
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
⊢ ∃ p, Measurable p.2 ∧ p.1 ⟂ₘ r • ν ∧ μ = p.1 + (r • ν).withDensity p.2

Tactic:
obtain ⟨hmeas, hsing, hadd⟩ := haveLebesgueDecomposition_spec μ ν

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ ∃ p, Measurable p.2 ∧ p.1 ⟂ₘ r • ν ∧ μ = p.1 + (r • ν).withDensity p.2
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : s S = 0
hS₃ : ν Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : (μ.singularPart ν) T = 0
hT₃ : ν Tᶜ = 0
hνinter : ν (S ∩ T)ᶜ = 0
A : Set α
hA : MeasurableSet A
⊢ ((ν.withDensity f).restrict (S ∩ T)) A = ((ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T)) A

Tactic:
have hs : s (A ∩ (S ∩ T)) = 0 := by
      rw [← nonpos_iff_eq_zero]
      exact hS₂ ▸ measure_mono (inter_subset_right.trans inter_subset_left)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : s S = 0
hS₃ : ν Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : (μ.singularPart ν) T = 0
hT₃ : ν Tᶜ = 0
hνinter : ν (S ∩ T)ᶜ = 0
A : Set α
hA : MeasurableSet A
hs : s (A ∩ (S ∩ T)) = 0
⊢ ((ν.withDensity f).restrict (S ∩ T)) A = ((ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T)) A
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a}
⊢ ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a

Tactic:
simp -zeta only [not_lt, not_eventually, nonpos_iff_eq_zero] at hs

Goal state after:
α : Type u_1
inst✝¹ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a}
hs : s = {x | ∃ᶠ (x : Set α) in v.filterAt x, μ x = 0}
⊢ ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
h : ν.rnDeriv (r.toNNReal • μ) =ᵐ[μ] r.toNNReal⁻¹ • ν.rnDeriv μ
⊢ ν.rnDeriv (r • μ) =ᵐ[μ] r⁻¹ • ν.rnDeriv μ

Tactic:
have : (r.toNNReal)⁻¹ • rnDeriv ν μ = r⁻¹ • rnDeriv ν μ := by
    ext x
    simp only [Pi.smul_apply, ENNReal.smul_def, smul_eq_mul]
    rw [ENNReal.coe_inv, ENNReal.coe_toNNReal hr_ne_top]
    rw [ne_eq, ENNReal.toNNReal_eq_zero_iff]
    simp [hr, hr_ne_top]

Goal state after:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
h : ν.rnDeriv (r.toNNReal • μ) =ᵐ[μ] r.toNNReal⁻¹ • ν.rnDeriv μ
this : r.toNNReal⁻¹ • ν.rnDeriv μ = r⁻¹ • ν.rnDeriv μ
⊢ ν.rnDeriv (r • μ) =ᵐ[μ] r⁻¹ • ν.rnDeriv μ
Module: Mathlib.MeasureTheory.Covering.DensityTheorem

Goal state before:
pp: case refine_2.inr
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[>] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : l.NeBot
hK : 0 ≤ K
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε

Tactic:
replace δlim := tendsto_nhds_of_tendsto_nhdsWithin δlim

Goal state after:
case refine_2.inr
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : l.NeBot
hK : 0 ≤ K
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall 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 μ
C : ℝ≥0
h : ∀ (x : α), ∃ᶠ (r : ℝ) in 𝓝[>] 0, μ (closedBall x (3 * r)) ≤ ↑C * μ (closedBall x r)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧ ∃ r, a ⊆ closedBall x r ∧ μ (closedBall x (3 * r)) ≤ ↑C * μ a}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      μ (closedBall p.2.1 (3 * p.1)) ≤ ↑C * μ p.2.2 ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
A : ∀ x ∈ s, ∀ ε > 0, ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x
t' : Set (ℝ × α × Set α)
t't : t' ⊆ t
left✝ : t'.Countable
t'_disj : t'.PairwiseDisjoint fun p ↦ p.2.2
μt' : μ (s \ ⋃ a ∈ t', a.2.2) = 0
⊢ ⋃ p ∈ (fun p ↦ p.2) '' t', p.2 = ⋃ a ∈ t', a.2.2

Tactic:
rw [biUnion_image]

Goal state after:
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ρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n ↦ s ∩ {x | v.limRatio ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n ↦ s ∩ {x | ↑q < v.limRatio ρ x} ∩ o n
m n : ℕ
I : (ρ + μ) (u m) ≠ ∞
J : (ρ + μ) (w n) ≠ ∞
A :
  ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
h : ¬μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ ↑p * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) <
    ↑q * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))

Tactic:
gcongr
      suffices H : (ρ + μ) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≠ ∞ by
        simp only [not_or, ENNReal.add_eq_top, Pi.add_apply, Ne, coe_add] at H
        exact H.2
      apply (lt_of_le_of_lt (measure_mono inter_subset_left) _).ne
      rw [measure_toMeasurable]
      apply lt_of_le_of_lt (measure_mono _) (measure_spanningSets_lt_top (ρ + μ) m)
      exact inter_subset_right

Goal state after:
Module: Mathlib.Analysis.Complex.Spectrum

Goal state before:
pp: A : Type u_1
inst✝³ : NonUnitalRing A
inst✝² : Module ℂ A
inst✝¹ : IsScalarTower ℂ A A
inst✝ : SMulCommClass ℂ A A
a : A
⊢ QuasispectrumRestricts a ⇑Complex.reCLM ↔ ∀ x ∈ σₙ ℂ a, x = ↑x.re

Tactic:
by
  rw [quasispectrumRestricts_iff_spectrumRestricts_inr,
    Unitization.quasispectrum_eq_spectrum_inr' _ ℂ, SpectrumRestricts.real_iff]

Goal state after:
Module: Mathlib.Analysis.BoundedVariation

Goal state before:

Tactic:
∑ i ∈ range n, edist (B (f (u (i + 1))) (g (u (i + 1)))) (B (f (u i)) (g (u i)))
  _ ≤ ∑ i ∈ range n, edist (B (f (u (i + 1))) (g (u (i + 1)))) (B (f (u i)) (g (u (i + 1)))) +
      ∑ i ∈ range n, edist (B (f (u i)) (g (u (i + 1)))) (B (f (u i)) (g (u i))) := by
    rw [← Finset.sum_add_distrib]
    gcongr with i hi
    apply edist_triangle
  _ = ∑ i ∈ range n, ‖B (f (u (i + 1)) - f (u i)) (g (u (i + 1)))‖ₑ +
      ∑ i ∈ range n, ‖B (f (u i)) (g (u (i + 1)) - g (u i))‖ₑ := by simp [edist_eq_enorm_sub]
  _ ≤ ∑ i ∈ range n, ‖B‖ₑ * ‖f (u (i + 1)) - f (u i)‖ₑ * ‖g (u (i + 1))‖ₑ +
      ∑ i ∈ range n, ‖B‖ₑ * ‖f (u i)‖ₑ * ‖g (u (i + 1)) - g (u i)‖ₑ := by
    gcongr with i hi i hi
    · apply ContinuousLinearMap.le_opENorm₂
    · apply ContinuousLinearMap.le_opENorm₂
  _ ≤ ∑ i ∈ range n, ‖B‖ₑ * ‖f (u (i + 1)) - f (u i)‖ₑ * D +
      ∑ i ∈ range n, ‖B‖ₑ * C * ‖g (u (i + 1)) - g (u i)‖ₑ := by
    gcongr with i hi i hi
    · apply hg _ (u_mem _)
    · apply hf _ (u_mem _)
  _ = ‖B‖ₑ * D * ∑ i ∈ range n, ‖f (u (i + 1)) - f (u i)‖ₑ +
      ‖B‖ₑ * C * ∑ i ∈ range n, ‖g (u (i + 1)) - g (u i)‖ₑ := by
    simp only [← sum_mul, ← mul_sum]
    ring
  _ ≤ ‖B‖ₑ * D * eVariationOn f s + ‖B‖ₑ * C * eVariationOn g s := by
    simp only [← edist_eq_enorm_sub]
    gcongr
    · exact eVariationOn.sum_le_of_monotoneOn_Iic (u_mono.monotoneOn _) (fun i hi ↦ u_mem i)
    · exact eVariationOn.sum_le_of_monotoneOn_Iic (u_mono.monotoneOn _) (fun i hi ↦ u_mem i)
  _ = ‖B‖ₑ * (C * eVariationOn g s + D * eVariationOn f s) := by ring

Goal state after:
Module: Mathlib.Analysis.BoundedVariation

Goal state before:
pp: case inr
α : Type u_2
inst✝⁶ : LinearOrder α
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set α
f : α → E
g : α → F
hf : BoundedVariationOn f s
hg : BoundedVariationOn g s
B : E →L[ℝ] F →L[ℝ] G
x : α
hx : x ∈ s
⊢ BoundedVariationOn (fun x ↦ (B (f x)) (g x)) s

Tactic:
suffices eVariationOn (fun x ↦ (B (f x)) (g x)) s < ∞ from ne_of_lt this

Goal state after:
case inr
α : Type u_2
inst✝⁶ : LinearOrder α
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set α
f : α → E
g : α → F
hf : BoundedVariationOn f s
hg : BoundedVariationOn g s
B : E →L[ℝ] F →L[ℝ] G
x : α
hx : x ∈ s
⊢ eVariationOn (fun x ↦ (B (f x)) (g x)) s < ∞
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
h : (𝓝[s ∩ Iio a] a).NeBot
h' : ContinuousWithinAt f (s ∩ Iic a) a
ha : a ∈ s
⊢ eVariationOn f (s ∩ Iio a) = eVariationOn f (s ∩ Iic a)

Tactic:
have : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 (f a)) := h'.mono (by grind)
    simp [eVariationOn_on_inter_Iic_eq_Iio_add_edist h ha this]

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

Goal state before:
pp: case zero
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : δ < ε
H : ∃ᶠ (x : α) in L, ε ≤ eVariationOn f (s ∩ Ici x)
y : α → α
y_mem : ∀ y_1 ∈ s, y y_1 ∈ s ∩ Ici y_1
le_y : ∀ y_1 ∈ s, δ ≤ eVariationOn f (s ∩ Icc y_1 (y y_1))
v : ℕ → α := fun n ↦ y^[n] x₀
⊢ v 0 ∈ s

Tactic:
simpa [v] using hx₀

Goal state after: