mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

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
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
A : PartialEquiv E F := hf.toPartialEquiv hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ↑‖↑f'.symm‖₊ * ‖f' (x' - y' - f'.symm (↑A x' - ↑A y'))‖ = ↑‖↑f'.symm‖₊ * ‖↑A y' - ↑A x' - f' (y' - x')‖

Tactic:
congr 2
      simp only [ContinuousLinearEquiv.apply_symm_apply, map_sub]
      abel

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
z₀ : 𝕜
n : ℕ
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
IH : analyticOrderAt (deriv f) z₀ = ↑n ↔ (∀ k < n, iteratedDeriv (k + 1) f z₀ = 0) ∧ iteratedDeriv (n + 1) f z₀ ≠ 0
x✝ : (∀ k < n + 1, iteratedDeriv k f z₀ = 0) ∧ iteratedDeriv (n + 1) f z₀ ≠ 0
hz : ∀ k < n + 1, iteratedDeriv k f z₀ = 0
hnz : iteratedDeriv (n + 1) f z₀ ≠ 0
⊢ f z₀ = 0

Tactic:
simpa using hz 0 (by lia)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ analyticOrderAt (f ^ 0) z₀ = 0 • analyticOrderAt f z₀

Tactic:
simp [analyticOrderAt_eq_zero]

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_5
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ (i : ι), MeromorphicAt (F i) x
h₂f : ¬Function.HasFiniteMulSupport F
⊢ MeromorphicAt (∏ᶠ (i : ι), F i) x

Tactic:
exact finprod_of_not_hasFiniteMulSupport h₂f ▸ const (1 : 𝕜') x

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
⊢ MeromorphicAt (f - g) x

Tactic:
by
  convert hf.add hg.neg
  ext1 z
  simp_rw [Pi.sub_apply, Pi.add_apply, Pi.neg_apply, sub_eq_add_neg]

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case ofNat
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
m : ℕ
⊢ MeromorphicAt (f ^ Int.ofNat m) x

Tactic:
| ofNat m =>

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
x : 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) y
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) x_1 → AnalyticAt 𝕜 f x_1

Tactic:
rw [eventually_nhdsWithin_iff]

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
x : 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) y
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) x_1 → AnalyticAt 𝕜 f x_1
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
x : 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
h : MeromorphicAt f x
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 f y

Tactic:
by
  obtain ⟨n, h⟩ := h
  apply AnalyticAt.eventually_analyticAt at h
  refine (h.filter_mono ?_).mp ?_
  · simp [nhdsWithin]
  · rw [eventually_nhdsWithin_iff]
    apply Filter.Eventually.of_forall
    intro y hy hf
    rw [Set.mem_compl_iff, Set.mem_singleton_iff] at hy
    have := ((analyticAt_id (𝕜 := 𝕜).sub analyticAt_const).pow n).inv
      (pow_ne_zero _ (sub_ne_zero_of_ne hy))
    apply (this.smul hf).congr ∘ (eventually_ne_nhds hy).mono
    intro z hz
    simp [smul_smul, hz, sub_eq_zero]

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
x✝ : MeromorphicAt f x
n : ℕ
hn : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) x
z : 𝕜
hz : z ∈ {x}ᶜ
⊢ f z = (z - x) ^ (-↑n) • (z - x) ^ n • f z

Tactic:
match_scalars

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
x✝ : MeromorphicAt f x
n : ℕ
hn : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) x
z : 𝕜
hz : z ∈ {x}ᶜ
⊢ 1 = (z - x) ^ (-↑n) * ((z - x) ^ n * 1)
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ r * (ascPochhammer ℕ k).smeval (r + 1) + (↑k • 1 + 1) * (ascPochhammer ℕ k).smeval (r + 1) =
    k.succ • (ascPochhammer ℕ k).smeval (r + 1) + r * (ascPochhammer ℕ k).smeval (r + 1)

Tactic:
@nsmul_one,

Goal state after:
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ r * (ascPochhammer ℕ k).smeval (r + 1) + (↑↑k + 1) * (ascPochhammer ℕ k).smeval (r + 1) =
    k.succ • (ascPochhammer ℕ k).smeval (r + 1) + r * (ascPochhammer ℕ k).smeval (r + 1)
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝² : AddCommMonoid R
inst✝¹ : Module ℚ≥0 R
inst✝ : Pow R ℕ
r : R
n : ℕ
⊢ n.factorial • (↑n.factorial)⁻¹ • (ascPochhammer ℕ n).smeval r = (ascPochhammer ℕ n).smeval r

Tactic:
match_scalars

Goal state after:
R : Type u_1
inst✝² : AddCommMonoid R
inst✝¹ : Module ℚ≥0 R
inst✝ : Pow R ℕ
r : R
n : ℕ
⊢ ↑n.factorial * ((↑n.factorial)⁻¹ * 1) = 1
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n k : ℕ
hkn : k ≤ n
⊢ n.choose k • choose r n = choose r k * choose (r - ↑k) (n - k)

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero n),
    nsmul_left_comm, ← descPochhammer_eq_factorial_smul_choose,
    ← Nat.choose_mul_factorial_mul_factorial hkn, ← smul_mul_smul_comm,
    ← descPochhammer_eq_factorial_smul_choose, mul_nsmul',
    ← descPochhammer_eq_factorial_smul_choose, smul_mul_assoc]

Goal state after:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n k : ℕ
hkn : k ≤ n
⊢ n.choose k • (descPochhammer ℤ n).smeval r =
    n.choose k • ((descPochhammer ℤ k).smeval r * (descPochhammer ℤ (n - k)).smeval (r - ↑k))
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case succ
a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n))
    B
this✝ :
  iteratedDerivWithin (n + 1) (fun x ↦ (1 + x) ^ a) B = derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B
this :
  Set.EqOn (derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B)
    (derivWithin (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) B) B
z : ℂ
hz : z ∈ B
⊢ (descPochhammer ℤ n).smeval a * deriv (fun x ↦ (1 + x) ^ (a - ↑n)) z =
    (descPochhammer ℤ (n + 1)).smeval a * (1 + z) ^ (a - (↑n + 1))

Tactic:
_root_.deriv_cpow_const (by fun_prop),

Goal state after:
case succ
a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n))
    B
this✝ :
  iteratedDerivWithin (n + 1) (fun x ↦ (1 + x) ^ a) B = derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B
this :
  Set.EqOn (derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B)
    (derivWithin (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) B) B
z : ℂ
hz : z ∈ B
⊢ (descPochhammer ℤ n).smeval a * ((a - ↑n) * (1 + z) ^ (a - ↑n - 1) * deriv (HAdd.hAdd 1) z) =
    (descPochhammer ℤ (n + 1)).smeval a * (1 + z) ^ (a - (↑n + 1))

case succ
a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n))
    B
this✝ :
  iteratedDerivWithin (n + 1) (fun x ↦ (1 + x) ^ a) B = derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B
this :
  Set.EqOn (derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B)
    (derivWithin (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) B) B
z : ℂ
hz : z ∈ B
⊢ 1 + z ∈ slitPlane
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: c : ℂ
hc : c ≠ 0
⊢ (fun x ↦ ‖↑x ^ (c - 1)‖) =ᶠ[atTop] fun x ↦ x ^ (c.re - 1)

Tactic:
filter_upwards [eventually_gt_atTop 0] with x hx

Goal state after:
c : ℂ
hc : c ≠ 0
x : ℝ
hx : 0 < x
⊢ ‖↑x ^ (c - 1)‖ = x ^ (c.re - 1)
Module: Mathlib.Analysis.Analytic.Polynomial

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

Tactic:
simp_rw [map_add]

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

Goal state before:
pp: x p : ℝ
⊢ deriv (fun x ↦ x ^ p) x = p * x ^ (p - 1)

Tactic:
by_cases! h : p = 0

Goal state after:
case pos
x p : ℝ
h : p = 0
⊢ deriv (fun x ↦ x ^ p) x = p * x ^ (p - 1)

case neg
x p : ℝ
h : p ≠ 0
⊢ deriv (fun x ↦ x ^ p) x = p * x ^ (p - 1)
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_10
a : ℕ
r : ℝ
hr : r ≠ 0
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (↑r - x) ^ (a + 1))
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ (↑r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)))
    (Complex.ofRealCLM 0) ‖↑r‖ₑ
n : ℕ
⊢ ((FormalMultilinearSeries.ofScalars ℝ (fun n ↦ (r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)) n) fun x ↦ 1) =
    Complex.reCLM
      ((FormalMultilinearSeries.restrictScalars ℝ
          (FormalMultilinearSeries.ofScalars ℂ fun n ↦ (↑r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)) n)
        (⇑Complex.ofRealCLM ∘ fun x ↦ 1))

Tactic:
simp [-Complex.inv_re, ← Complex.ofReal_pow, ← Complex.ofReal_inv]

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 : TotallyBounded s
⊢ ∃ N ⊆ s, N.Finite ∧ IsCover ε s N

Tactic:
rw [EMetric.totallyBounded_iff'] at hs

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 ⊆ s, N.Finite ∧ IsCover ε s N
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: a✝ b : EReal
a : ℝ
hb : 0 ≤ ⊤
h : ↑a < ⊤
n : ℕ
n_0 : 0 < n
⊢ ∃ m, ↑a * ↑n ≤ ↑m ∧ ↑m ≤ ⊤ * ↑n

Tactic:
obtain ⟨m, hm⟩ := exists_nat_ge_mul h.ne n

Goal state after:
a✝ b : EReal
a : ℝ
hb : 0 ≤ ⊤
h : ↑a < ⊤
n : ℕ
n_0 : 0 < n
m : ℕ
hm : ↑a * ↑n ≤ ↑m
⊢ ∃ m, ↑a * ↑n ≤ ↑m ∧ ↑m ≤ ⊤ * ↑n
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u v : ℕ → ℝ≥0∞
n : ℕ
⊢ ((u ⊔ v) n).log / ↑n = max ((u n).log / ↑n) ((v n).log / ↑n)

Tactic:
rw [Pi.sup_apply, log_monotone.map_max]

Goal state after:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ max (u n).log (v n).log / ↑n = max ((u n).log / ↑n) ((v n).log / ↑n)
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hf_meas : AEMeasurable f μ
⊢ ∫⁻ (x : α), AEMeasurable.mk f hf_meas x ∂μ ≠ ∞

Tactic:
rwa [lintegral_congr_ae hf_meas.ae_eq_mk.symm]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Sub

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ μ - 0 = μ

Tactic:
by
  rw [sub_def]
  apply le_antisymm
  · simp [sInf_le]
  · simp

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : ¬r = 0
this : r⁻¹ • μ.rnDeriv ν = ↑r⁻¹ • μ.rnDeriv ν
⊢ μ = (μ.singularPart ν, ↑r⁻¹ • μ.rnDeriv ν).1 + ↑r⁻¹ • (r • ν).withDensity (μ.rnDeriv ν)

Tactic:
ENNReal.smul_def r,

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : ¬r = 0
this : r⁻¹ • μ.rnDeriv ν = ↑r⁻¹ • μ.rnDeriv ν
⊢ μ = (μ.singularPart ν, ↑r⁻¹ • μ.rnDeriv ν).1 + ↑r⁻¹ • (↑r • ν).withDensity (μ.rnDeriv ν)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn

Goal state before:
pp: case refine_1
α : 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
this : 0 ≤ d t
⊢ ↑(ν t).toNNReal ≤ ↑(μ t).toNNReal

Tactic:
simpa only [d, le_sub_iff_add_le, zero_add] using this

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

Goal state before:
pp: case pos.refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ μ = μ.singularPart ν + (r • ν).withDensity (r⁻¹ • μ.rnDeriv ν)

Tactic:
ENNReal.smul_def r,

Goal state after:
case pos.refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ μ = μ.singularPart ν + (↑r • ν).withDensity (r⁻¹ • μ.rnDeriv ν)
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 (s ∪ t) ≤ γ + 0

Tactic:
rw [add_zero]; exact d_le_γ _ (hs.union ht)

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
⊢ VitaliFamily μ

Tactic:
let R := scalingScaleOf μ (max (4 * K + 3) 3)

Goal state after:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
⊢ VitaliFamily μ
Module: Mathlib.MeasureTheory.Covering.DensityTheorem

Goal state before:
pp: α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
⊢ closedBall y r ∈ (vitaliFamily μ K).setsAt x

Tactic:
let R := scalingScaleOf μ (max (4 * K + 3) 3)

Goal state after:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
⊢ closedBall y r ∈ (vitaliFamily μ K).setsAt x
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
⊢ ν = ν.singularPart μ + r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)

Tactic:
ENNReal.smul_def r,

Goal state after:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν = ν.singularPart μ + r⁻¹ • (↑r • μ).withDensity (ν.rnDeriv μ)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∃ u,
    Monotone u ∧
      Filter.Tendsto u Filter.atTop (nhds (sSup (measurableLEEval ν μ))) ∧ ∀ (n : ℕ), u n ∈ measurableLEEval ν μ
⊢ ∃ p, Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2

Tactic:
choose g _ hg₂ f hf₁ hf₂ using h

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
⊢ ∃ p, Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2
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ρ : ρ ≪ μ
x : α
hx : Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x))
h'x : v.limRatio ρ x = AEMeasurable.mk (v.limRatio ρ) ⋯ x
⊢ Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))

Tactic:
rwa [h'x] at hx

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν = ν.singularPart μ + r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)

Tactic:
ENNReal.smul_def r,

Goal state after:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν = ν.singularPart μ + r⁻¹ • (↑r • μ).withDensity (ν.rnDeriv μ)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : BoundedVariationOn f s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ |f x - f y| ≤ (eVariationOn f s).toReal

Tactic:
← Real.dist_eq

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : BoundedVariationOn f s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ dist (f x) (f y) ≤ (eVariationOn f s).toReal
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: case inr
α : Type u_1
inst✝² : LinearOrder α
E : Type u_3
inst✝¹ : PseudoMetricSpace E
inst✝ : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
this✝¹ : TopologicalSpace α := Preorder.topology α
this✝ : OrderTopology α
hb : (𝓝[>] b).NeBot
this :
  Tendsto f (𝓝[>] b) (𝓝 (Function.rightLim f b)) →
    Tendsto (variationOnFromTo f univ a) (𝓝[>] b)
      (𝓝 (variationOnFromTo f univ a b + dist (f b) (Function.rightLim f b)))
⊢ Tendsto (variationOnFromTo f univ a) (𝓝[>] b) (𝓝 (variationOnFromTo f univ a b + dist (f b) (Function.rightLim f b)))

Tactic:
exact this (hf.tendsto_rightLim _)

Goal state after:
Module: Mathlib.Analysis.BoundedVariation

Goal state before:
pp: case h
α : 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
C D : ℝ≥0∞
hf : ∀ x ∈ s, ‖f x‖ₑ ≤ C
hg : ∀ x ∈ s, ‖g x‖ₑ ≤ D
B : E →L[ℝ] F →L[ℝ] G
n : ℕ
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
i : ℕ
hi : i ∈ Finset.range n
⊢ ‖(B (f (u (i + 1)) - f (u i))) (g (u (i + 1)))‖ₑ ≤ ‖B‖ₑ * ‖f (u (i + 1)) - f (u i)‖ₑ * ‖g (u (i + 1))‖ₑ

Tactic:
apply ContinuousLinearMap.le_opENorm₂

Goal state after:
Module: Mathlib.Analysis.BoundedVariation

Goal state before:
pp: case h
α : 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
C D : ℝ≥0∞
hf : ∀ x ∈ s, ‖f x‖ₑ ≤ C
hg : ∀ x ∈ s, ‖g x‖ₑ ≤ D
B : E →L[ℝ] F →L[ℝ] G
n : ℕ
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
i : ℕ
hi : i ∈ Finset.range n
⊢ ‖(B (f (u i))) (g (u (i + 1)) - g (u i))‖ₑ ≤ ‖B‖ₑ * ‖f (u i)‖ₑ * ‖g (u (i + 1)) - g (u i)‖ₑ

Tactic:
apply ContinuousLinearMap.le_opENorm₂

Goal state after: