mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_10
a : ℕ
z : ℂ
hz : z ≠ 0
this✝ :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)) ((z⁻¹ • 1) 0) 1
H : 1 / ‖z⁻¹ • 1‖ₑ = ‖z‖ₑ
this :
  HasFPowerSeriesOnBall (fun x ↦ ((1 - (z⁻¹ • ⇑1) x) ^ (a + 1))⁻¹)
    ((FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)).compContinuousLinearMap (z⁻¹ • 1)) 0 ‖z‖ₑ
⊢ (FormalMultilinearSeries.ofScalars ℂ fun n ↦ (z ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)) =
    (z ^ (a + 1))⁻¹ •
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)).compContinuousLinearMap (z⁻¹ • 1)

Tactic:
ext n

Goal state after:
case e'_10
a : ℕ
z : ℂ
hz : z ≠ 0
this✝ :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)) ((z⁻¹ • 1) 0) 1
H : 1 / ‖z⁻¹ • 1‖ₑ = ‖z‖ₑ
this :
  HasFPowerSeriesOnBall (fun x ↦ ((1 - (z⁻¹ • ⇑1) x) ^ (a + 1))⁻¹)
    ((FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)).compContinuousLinearMap (z⁻¹ • 1)) 0 ‖z‖ₑ
n : ℕ
⊢ ((FormalMultilinearSeries.ofScalars ℂ (fun n ↦ (z ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)) n) fun x ↦ 1) =
    (((z ^ (a + 1))⁻¹ •
          (FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)).compContinuousLinearMap (z⁻¹ • 1))
        n)
      fun x ↦ 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 : MvPolynomial σ A
⊢ AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) p) z

Tactic:
by
  apply p.induction_on (fun k ↦ ?_) (fun p q hp hq ↦ ?_) fun p i hp ↦ ?_ -- `refine` doesn't work
  · simp_rw [aeval_C]; apply analyticAt_const
  · simp_rw [map_add]; exact hp.add hq
  · simp_rw [map_mul, aeval_X]; exact hp.mul (hf i)

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

Goal state before:
pp: r : ℝ
hr : r < 1
hr' : r ≠ 0
h : DifferentiableAt ℝ (fun x ↦ x ^ r) 0
y : ℝ := ⋯
⊢ ∀ x ∈ Set.Ioi 0, x⁻¹ • ((0 + x) ^ r - 0 ^ r) = x ^ (r - 1)

Tactic:
intro x (hx : 0 < x)

Goal state after:
r : ℝ
hr : r < 1
hr' : r ≠ 0
h : DifferentiableAt ℝ (fun x ↦ x ^ r) 0
y : ℝ := deriv (fun x ↦ x ^ r) 0
x : ℝ
hx : 0 < x
⊢ x⁻¹ • ((0 + x) ^ r - 0 ^ r) = x ^ (r - 1)
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_10
a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    (Complex.ofRealCLM 0) 1
⊢ (FormalMultilinearSeries.ofScalars ℝ fun n ↦ Ring.choose (a + ↑n - 1) n) =
    Complex.reCLM.compFormalMultilinearSeries
      ((FormalMultilinearSeries.restrictScalars ℝ
            (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n)).compContinuousLinearMap
        Complex.ofRealCLM)

Tactic:
ext n

Goal state after:
case e'_10
a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    (Complex.ofRealCLM 0) 1
n : ℕ
⊢ ((FormalMultilinearSeries.ofScalars ℝ (fun n ↦ Ring.choose (a + ↑n - 1) n) n) fun x ↦ 1) =
    (Complex.reCLM.compFormalMultilinearSeries
        ((FormalMultilinearSeries.restrictScalars ℝ
              (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n)).compContinuousLinearMap
          Complex.ofRealCLM)
        n)
      fun x ↦ 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‖ₑ
⊢ (FormalMultilinearSeries.ofScalars ℝ fun n ↦ (r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)) =
    Complex.reCLM.compFormalMultilinearSeries
      ((FormalMultilinearSeries.restrictScalars ℝ
            (FormalMultilinearSeries.ofScalars ℂ fun n ↦
              (↑r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a))).compContinuousLinearMap
        Complex.ofRealCLM)

Tactic:
ext n

Goal state after:
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.compFormalMultilinearSeries
        ((FormalMultilinearSeries.restrictScalars ℝ
              (FormalMultilinearSeries.ofScalars ℂ fun n ↦
                (↑r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a))).compContinuousLinearMap
          Complex.ofRealCLM)
        n)
      fun x ↦ 1
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

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

Tactic:
rw [linearGrowthSup, le_limsup_iff']

Goal state after:
u : ℕ → EReal
a : EReal
⊢ (∀ y < a, ∃ᶠ (a : ℕ) in atTop, y ≤ u a / ↑a) ↔ ∀ b < a, ∃ᶠ (n : ℕ) in atTop, b * ↑n ≤ u n
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
hf : SuperpolynomialDecay l k f
n : ℕ
⊢ SuperpolynomialDecay l k (k ^ n * f)

Tactic:
induction n with

Goal state after:
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
n : ℕ
⊢ SuperpolynomialDecay l k (k ^ n * f) ↔ SuperpolynomialDecay l k f

Tactic:
induction n with

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

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

Tactic:
log_inv

Goal state after:
u : ℕ → ℝ≥0∞
n : ℕ
⊢ -(u n).log * (↑n)⁻¹ = -(u n).log * (↑n)⁻¹
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)
s : ℕ → Set α
hm : Monotone s
⊢ Tendsto (fun n ↦ ↑(μ (s n)).toNNReal) atTop (𝓝 ↑(μ (⋃ n, s n)).toNNReal)

Tactic:
refine NNReal.tendsto_coe.2 <| (ENNReal.tendsto_toNNReal ?_).comp <|
        tendsto_measure_iUnion_atTop hm

Goal state after:
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)
s : ℕ → Set α
hm : Monotone s
⊢ μ (⋃ n, s n) ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn

Goal state before:
pp: case refine_2
α : 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)
s : ℕ → Set α
hm : Monotone s
⊢ Tendsto (fun n ↦ ↑(ν (s n)).toNNReal) atTop (𝓝 ↑(ν (⋃ n, s n)).toNNReal)

Tactic:
refine NNReal.tendsto_coe.2 <| (ENNReal.tendsto_toNNReal ?_).comp <|
        tendsto_measure_iUnion_atTop hm

Goal state after:
case refine_2
α : 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)
s : ℕ → Set α
hm : Monotone s
⊢ ν (⋃ n, s n) ≠ ∞
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure (μ.restrict s)
hμ0 : μ s = 0
⊢ (((μ.restrict s) univ)⁻¹ • μ.restrict s) univ = 0

Tactic:
simp [hμ0]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ ∀ (t : Set α), MeasurableSet t → ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ

Tactic:
refine MeasurableSpace.induction_on_inter h_eq h_inter ?_ basic ?_ ?_

Goal state after:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ ∫⁻ (x : α) in ∅, f x ∂μ = ∫⁻ (x : α) in ∅, g x ∂μ

case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ ∀ (t : Set α),
    MeasurableSet t →
      ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ → ∫⁻ (x : α) in tᶜ, f x ∂μ = ∫⁻ (x : α) in tᶜ, g x ∂μ

case refine_3
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ ∀ (f_1 : ℕ → Set α),
    Pairwise (Function.onFun Disjoint f_1) →
      (∀ (i : ℕ), MeasurableSet (f_1 i)) →
        (∀ (i : ℕ), ∫⁻ (x : α) in f_1 i, f x ∂μ = ∫⁻ (x : α) in f_1 i, g x ∂μ) →
          ∫⁻ (x : α) in ⋃ i, f_1 i, f x ∂μ = ∫⁻ (x : α) in ⋃ i, f_1 i, g x ∂μ
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)
n✝ m : ℕ
h : m ≤ n✝
n : ℕ
hmn : m ≤ n
ih : γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
⊢ d (e (n + 1)) + d (f m n) ≤ d (e (n + 1)) + d (f m n \ e (n + 1)) + d (f m n ∩ e (n + 1))

Tactic:
d_split (f m n) (e (n + 1)) (he₁ _),

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
f_succ : ∀ (n m : ℕ), n ≤ m → f n (m + 1) = f n m ∩ e (m + 1)
n✝ m : ℕ
h : m ≤ n✝
n : ℕ
hmn : m ≤ n
ih : γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
⊢ d (e (n + 1)) + (d (f m n \ e (n + 1)) + d (f m n ∩ e (n + 1))) ≤
    d (e (n + 1)) + d (f m n \ e (n + 1)) + d (f m n ∩ e (n + 1))
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)
n✝ m : ℕ
h : m ≤ n✝
n : ℕ
hmn : m ≤ n
ih : γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
⊢ d (e (n + 1) ∪ f m n) + d (f m (n + 1)) ≤ γ + d (f m (n + 1))

Tactic:
d_le_γ _ <| (he₁ _).union (hf _ _)

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
f_succ : ∀ (n m : ℕ), n ≤ m → f n (m + 1) = f n m ∩ e (m + 1)
n✝ m : ℕ
h : m ≤ n✝
n : ℕ
hmn : m ≤ n
ih : γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
⊢ γ + d (f m (n + 1)) ≤ γ + d (f m (n + 1))
Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn

Goal state before:

Tactic:
γ + (γ - 2 * (1 / 2) ^ m + (1 / 2) ^ (n + 1)) =
            γ + (γ - 2 * (1 / 2) ^ m + ((1 / 2) ^ n - (1 / 2) ^ (n + 1))) := by
          rw [pow_succ, mul_one_div, _root_.sub_half]
        _ = γ - (1 / 2) ^ (n + 1) + (γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n) := by
          simp only [sub_eq_add_neg]; abel
        _ ≤ d (e (n + 1)) + d (f m n) := add_le_add (le_of_lt <| he₂ _) ih
        _ ≤ d (e (n + 1)) + d (f m n \ e (n + 1)) + d (f m (n + 1)) := by
          rw [f_succ _ _ hmn, d_split (f m n) (e (n + 1)) (he₁ _), add_assoc]
        _ = d (e (n + 1) ∪ f m n) + d (f m (n + 1)) := by
          rw [d_split (e (n + 1) ∪ f m n) (e (n + 1)), union_sdiff_left, union_inter_cancel_left]
          · abel
          · exact he₁ _
        _ ≤ γ + d (f m (n + 1)) := by grw [d_le_γ _ <| (he₁ _).union (hf _ _)]

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

Goal state before:
pp: case left.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
⊢ (μ.withDensity (ν.rnDeriv μ)) (s ∩ t) = 0

Tactic:
exact measure_mono_null Set.inter_subset_left hνs

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
⊢ μ.singularPart ν = 0

Tactic:
by
  rw [← MutuallySingular.self_iff]
  exact MutuallySingular.mono_ac (mutuallySingular_singularPart _ _)
    AbsolutelyContinuous.rfl ((absolutelyContinuous_of_le (singularPart_le _ _)).trans h)

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ρ : ρ ≪ μ
c d : ℝ≥0
hcd : c < d
s : Set α
hc : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ↑c * μ a
hd : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ↑d * μ a ≤ ρ a
x : α
x✝ : x ∈ s
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : μ o < ∞
⊢ μ (s ∩ o) = 0

Tactic:
let s' := s ∩ o

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
c d : ℝ≥0
hcd : c < d
s : Set α
hc : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ↑c * μ a
hd : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ↑d * μ a ≤ ρ a
x : α
x✝ : x ∈ s
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : μ o < ∞
s' : Set α := s ∩ o
⊢ μ (s ∩ o) = 0
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case succ
α : Type u_1
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun x ↦ ⨆ k, ⨆ (_ : k ≤ m), f k x) ∈ measurableLE μ ν
⊢ (fun x ↦ ⨆ k, ⨆ (_ : k ≤ m + 1), f k x) ∈ measurableLE μ ν

Tactic:
have :
      (fun a : α ↦ ⨆ (k : ℕ) (_ : k ≤ m + 1), f k a) = fun a ↦
        f m.succ a ⊔ ⨆ (k : ℕ) (_ : k ≤ m), f k a :=
      funext fun _ ↦ iSup_succ_eq_sup _ _ _

Goal state after:
case succ
α : Type u_1
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun x ↦ ⨆ k, ⨆ (_ : k ≤ m), f k x) ∈ measurableLE μ ν
this : (fun a ↦ ⨆ k, ⨆ (_ : k ≤ m + 1), f k a) = fun a ↦ max (f m.succ a) (⨆ k, ⨆ (_ : k ≤ m), f k a)
⊢ (fun x ↦ ⨆ k, ⨆ (_ : k ≤ m + 1), f k x) ∈ measurableLE μ ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
n : ℕ
⊢ (fun x ↦ ⨆ k, ⨆ (_ : k ≤ n), f k x) ∈ measurableLE μ ν

Tactic:
induction n with

Goal state after:
Module: Mathlib.Analysis.Calculus.Monotone

Goal state before:
pp: f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b ↦ (↑hf.stieltjesFunction b - ↑hf.stieltjesFunction x) / (b - x)) (𝓝[<] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal) ∧
    Tendsto (fun b ↦ (↑hf.stieltjesFunction b - ↑hf.stieltjesFunction x) / (b - x)) (𝓝[>] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : ↑hf.stieltjesFunction x = f x
⊢ HasDerivAt f (hf.stieltjesFunction.measure.rnDeriv volume x).toReal x

Tactic:
A

Goal state after:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal) ∧
    Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : ↑hf.stieltjesFunction x = f x
⊢ HasDerivAt f (hf.stieltjesFunction.measure.rnDeriv volume x).toReal x
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
ab : a < b
⊢ variationOnFromTo f s a b = -variationOnFromTo f s b a

Tactic:
simp only [variationOnFromTo, if_pos ab.le, if_neg ab.not_ge, neg_neg]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
n : ℕ
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
⊢ ∃ p,
    ↑p.snd p.fst = u n ∧
      ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) =
        ∑ i ∈ Finset.range p.fst, edist (f (↑p.snd (i + 1))) (f (↑p.snd i))

Tactic:
induction n with

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun i ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : 0 < N
A : N - 1 + 1 = N
⊢ Finset.Ico (N - 1) N = Finset.Ico (N - 1) (N - 1 + 1)

Tactic:
A

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun i ↦ if i < N then u i else if i = N then x else u (i - 1)
hw : Monotone w
Npos : 0 < N
A : N - 1 + 1 = N
⊢ Finset.Ico (N - 1) N = Finset.Ico (N - 1) N