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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z₀ : 𝕜
h₁ : AnalyticAt 𝕜 g z₀
h₂ : z₀ ∈ {x}ᶜ
⊢ deriv (fun z ↦ (z - x) ^ n • g z) z₀ = (↑n * (z₀ - x) ^ (n - 1)) • g z₀ + (z₀ - x) ^ n • deriv g z₀

Tactic:
deriv_fun_smul (DifferentiableAt.zpow (by fun_prop) (by simp_all [sub_ne_zero_of_ne h₂]))
      (by fun_prop),

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z₀ : 𝕜
h₁ : AnalyticAt 𝕜 g z₀
h₂ : z₀ ∈ {x}ᶜ
⊢ (z₀ - x) ^ n • deriv g z₀ + deriv (fun z ↦ (z - x) ^ n) z₀ • g z₀ =
    (↑n * (z₀ - x) ^ (n - 1)) • g z₀ + (z₀ - x) ^ n • deriv g z₀
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case succ
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
ih : (ascPochhammer ℕ k).smeval (-r) = (↑k).negOnePow • (descPochhammer ℤ k).smeval r
h : (X + ↑k).smeval (-r) = -(X + -↑k).smeval r
⊢ (↑k).negOnePow • (descPochhammer ℤ k).smeval r * (X + ↑k).smeval (-r) =
    (↑(k + 1)).negOnePow • ((descPochhammer ℤ k).smeval r * (X + -↑k).smeval r)

Tactic:
rw [h, ← neg_mul_comm, Int.natCast_add, Int.natCast_one, Int.negOnePow_succ, Units.neg_smul,
      Units.smul_def, Units.smul_def, ← smul_mul_assoc, neg_mul]

Goal state after:
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 • (descPochhammer ℤ n).smeval r =
    n.choose k • ((descPochhammer ℤ k).smeval r * (descPochhammer ℤ (n - k)).smeval (r - ↑k))

Tactic:
nth_rw 2 [← Nat.sub_add_cancel hkn]

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 - k + k)).smeval r =
    n.choose k • ((descPochhammer ℤ k).smeval r * (descPochhammer ℤ (n - k)).smeval (r - ↑k))
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: c : ℂ
hc : c ≠ 0
x : ℝ
hx : x ≠ 0
⊢ deriv (fun x ↦ ↑x ^ c) x = c * ↑x ^ (c - 1)

Tactic:
deriv_ofReal_cpow_const hx hc

Goal state after:
c : ℂ
hc : c ≠ 0
x : ℝ
hx : x ≠ 0
⊢ c * ↑x ^ (c - 1) = c * ↑x ^ (c - 1)
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
⊢ 1 + z ∈ slitPlane

Tactic:
apply Complex.mem_slitPlane_of_norm_lt_one
      simpa [B] using hz

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

Goal state before:
pp: case zero
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ HasFPowerSeriesWithinOnBall (iteratedFDerivWithin 𝕜 0 f s) (p.iteratedFDerivSeries 0) s x r

Tactic:
exact (continuousMultilinearCurryFin0 𝕜 E F).symm
      |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall h

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

Goal state before:

Tactic:
|k x ^ z * g x| = |k x ^ z| * |g x| := abs_mul (k x ^ z) (g x)
    _ ≤ |k x ^ z| * |f x| := by gcongr _ * ?_; exact hx
    _ = |k x ^ z * f x| := (abs_mul (k x ^ z) (f x)).symm

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
h : ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun a ↦ |k a ^ z * f a|
z : ℕ
⊢ Tendsto (fun a ↦ |k a ^ z * f a|) l (𝓝 0)

Tactic:
obtain ⟨m, hm⟩ := h (z + 1)

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
⊢ Tendsto (fun a ↦ |k a ^ z * f a|) l (𝓝 0)
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: case inl
u v : ℕ → ℝ≥0∞
hb : 0 ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0 * v n
⊢ (expGrowthSup fun x ↦ 0 * v x) ≤ expGrowthSup v

Tactic:
simp only [zero_mul, ← Pi.zero_def, expGrowthSup_zero, bot_le]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
⊢ ⨍ (x : α), f x ∂μ = (μ.real univ)⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
by
  rw [average_eq', integral_smul_measure, ENNReal.toReal_inv, measureReal_def]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᵐ[μ.restrict (s ∪ t)] g
h1✝ : ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ → f x = 0 x
h2✝ : ∀ᵐ (x : α) ∂μ, x ∈ hg'.sigmaFiniteSetᶜ → g x = 0 x
x : α
h1 : x ∈ hf'.sigmaFiniteSetᶜ → f x = 0 x
h2 : x ∈ hg'.sigmaFiniteSetᶜ → g x = 0 x
hx : x ∈ hf'.sigmaFiniteSetᶜ ∩ hg'.sigmaFiniteSetᶜ
⊢ 0 x = g x

Tactic:
h2 (Set.inter_subset_right hx)

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᵐ[μ.restrict (s ∪ t)] g
h1✝ : ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ → f x = 0 x
h2✝ : ∀ᵐ (x : α) ∂μ, x ∈ hg'.sigmaFiniteSetᶜ → g x = 0 x
x : α
h1 : x ∈ hf'.sigmaFiniteSetᶜ → f x = 0 x
h2 : x ∈ hg'.sigmaFiniteSetᶜ → g x = 0 x
hx : x ∈ hf'.sigmaFiniteSetᶜ ∩ hg'.sigmaFiniteSetᶜ
⊢ 0 x = 0 x
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)
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
hγ : Tendsto (fun m ↦ γ - 2 * (1 / 2) ^ m) atTop (𝓝 γ)
hd : Tendsto (fun m ↦ d (⋂ n, f m n)) atTop (𝓝 (d (⋃ m, ⋂ n, f m n)))
m n : ℕ
⊢ ∀ (m_1 : ℕ), n ≤ m_1 → f m m_1 ⊆ f m n

Tactic:
m

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)
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
hγ : Tendsto (fun m ↦ γ - 2 * (1 / 2) ^ m) atTop (𝓝 γ)
hd : Tendsto (fun m ↦ d (⋂ n, f m n)) atTop (𝓝 (d (⋃ m, ⋂ n, f m n)))
m✝ n m : ℕ
⊢ n ≤ m → f m✝ m ⊆ f m✝ n
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 • ν).withDensity (μ.singularPart ν, r⁻¹ • μ.rnDeriv ν).2

Tactic:
rw [this, withDensity_smul _ hmeas, ENNReal.smul_def r, withDensity_smul_measure,
      ← smul_assoc, smul_eq_mul, ENNReal.coe_inv hr, ENNReal.inv_mul_cancel, one_smul]

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 + ν.withDensity (μ.rnDeriv ν)

case neg.h0
α : 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 ν
⊢ ↑r ≠ 0

case neg.ht
α : 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 ν
⊢ ↑r ≠ ∞
Module: Mathlib.Order.Monotone.Extension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
⊢ ∃ g, Monotone g ∧ EqOn f g s

Tactic:
refine ⟨g, fun x y hxy => ?_, hgs⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
⊢ g x ≤ g y
Module: Mathlib.Analysis.Calculus.Monotone

Goal state before:
pp: f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx : HasDerivAt (↑hf.stieltjesFunction) (hf.stieltjesFunction.measure.rnDeriv volume x).toReal x
h'x : ¬¬ContinuousAt f x
A : ↑hf.stieltjesFunction x = f x
⊢ HasDerivAt f (hf.stieltjesFunction.measure.rnDeriv volume x).toReal x

Tactic:
rw [hasDerivAt_iff_tendsto_slope, (nhdsLT_sup_nhdsGT x).symm, tendsto_sup,
    slope_fun_def_field, A] at hx

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 neg
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
a b : α
hab : ¬a ≤ b
⊢ |variationOnFromTo f s a b| ≤ (eVariationOn f s).toReal

Tactic:
simp only [variationOnFromTo, hab, ↓reduceIte, abs_neg, ENNReal.abs_toReal]
    exact ENNReal.toReal_mono hf (eVariationOn.mono _ inter_subset_left)

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

Goal state before:
pp: case refine_1
α : 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
ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A, ξ a ∂ν ≤ μ A
hle : ν.withDensity ξ ≤ μ
this✝ : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ν E
hE₃ : ∀ (A : Set α), MeasurableSet A → ↑ε * ν (A ∩ E) ≤ (μ - ν.withDensity ξ) (A ∩ E)
hε₂ : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν ≤ μ (A ∩ E)
hξε : (ξ + E.indicator fun x ↦ ↑ε) ∈ measurableLE ν μ
this : ∫⁻ (a : α), ξ a + E.indicator (fun x ↦ ↑ε) a ∂ν ≤ sSup (measurableLEEval ν μ)
⊢ ∫⁻ (a : α), ξ a ∂ν ≠ ∞

Tactic:
have := measure_ne_top (ν.withDensity ξ) univ

Goal state after:
case refine_1
α : 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
ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A, ξ a ∂ν ≤ μ A
hle : ν.withDensity ξ ≤ μ
this✝¹ : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ν E
hE₃ : ∀ (A : Set α), MeasurableSet A → ↑ε * ν (A ∩ E) ≤ (μ - ν.withDensity ξ) (A ∩ E)
hε₂ : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν ≤ μ (A ∩ E)
hξε : (ξ + E.indicator fun x ↦ ↑ε) ∈ measurableLE ν μ
this✝ : ∫⁻ (a : α), ξ a + E.indicator (fun x ↦ ↑ε) a ∂ν ≤ sSup (measurableLEEval ν μ)
this : (ν.withDensity ξ) univ ≠ ∞
⊢ ∫⁻ (a : α), ξ a ∂ν ≠ ∞
Module: Mathlib.Analysis.BoundedVariation

Goal state before:
pp: s : Set ℝ
p q : ℝ → ℝ
hp : MonotoneOn p s
hq : MonotoneOn q s
h : LocallyBoundedVariationOn (p - q) s
x : ℝ
hxp : x ∈ s → DifferentiableWithinAt ℝ p s x
hxq : x ∈ s → DifferentiableWithinAt ℝ q s x
xs : x ∈ s
⊢ DifferentiableWithinAt ℝ (p - q) s x

Tactic:
exact (hxp xs).sub (hxq xs)

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

Goal state before:
pp: case inr
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : y ≤ x
⊢ eVariationOn (f ∘ φ) (t ∩ Icc x y) = eVariationOn f (φ '' t ∩ Icc (φ x) (φ y))

Tactic:
· rw [eVariationOn.subsingleton, eVariationOn.subsingleton]
    exacts [(Set.subsingleton_Icc_of_ge (hφ hy hx h)).anti Set.inter_subset_right,
      (Set.subsingleton_Icc_of_ge h).anti Set.inter_subset_right]

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

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

Tactic:
obtain ⟨b, hb⟩ : (s ∩ Iio a).Nonempty := by contrapose! h; simp [h]

Goal state after:
case refine_2
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
b : α
hb : b ∈ s ∩ Iio a
⊢ eVariationOn f (s ∩ Iio a) + edist (f a) l ≤ eVariationOn f (s ∩ Iic a)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
ha : p a
hsum : s.sum f = fun z ↦ ∑ i ∈ s, f i z
hf' : ContinuousOn (∑ i, f ↑i) (spectrum R a)
⊢ cfc (∑ i, f ↑i) a = ∑ i, cfc (f ↑i) a

Tactic:
cfc_apply_pi _ a ha (fun ⟨i, hi⟩ => hf i hi),

Goal state after:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
ha : p a
hsum : s.sum f = fun z ↦ ∑ i ∈ s, f i z
hf' : ContinuousOn (∑ i, f ↑i) (spectrum R a)
⊢ cfc (∑ i, f ↑i) a = ∑ i, (cfcHom ha) { toFun := (spectrum R a).domRestrict (f ↑i), continuous_toFun := ⋯ }
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
inst✝ : CompleteSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
h : L.NeBot
ε : ℝ≥0∞
εpos : ε > 0
W : Tendsto (fun y ↦ eVariationOn f (s ∩ Ici y)) L (𝓝 0)
⊢ ∃ y ∈ s, eVariationOn f (s ∩ Ici y) < ε

Tactic:
rcases (((tendsto_order.1 W).2 ε εpos).and (hL x₀ hx₀)).exists with ⟨y, hy, h'y⟩

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
inst✝ : CompleteSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
h : L.NeBot
ε : ℝ≥0∞
εpos : ε > 0
W : Tendsto (fun y ↦ eVariationOn f (s ∩ Ici y)) L (𝓝 0)
y : α
hy : eVariationOn f (s ∩ Ici y) < ε
h'y : (s ∩ Ici x₀) y
⊢ ∃ y ∈ s, eVariationOn f (s ∩ Ici y) < ε
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst✝ : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
⊢ p a

Tactic:
exact ha

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : Semifield R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ IsUnit (cfc f a) ↔ ∀ x ∈ spectrum R a, f x ≠ 0

Tactic:
← spectrum.zero_notMem_iff R,

Goal state after:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : Semifield R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ 0 ∉ spectrum R (cfc f a) ↔ ∀ x ∈ spectrum R a, f x ≠ 0
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : x ≤ y
⊢ eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)

Tactic:
rw [eVariationOn.subsingleton, eVariationOn.subsingleton] <;>
      grind [Set.Subsingleton]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: case negSucc
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : ContinuousInv₀ R
a : Aˣ
ha : p ↑a
n : ℕ
⊢ cfc (fun x ↦ x⁻¹ ^ (n + 1)) ↑a = ↑a⁻¹ ^ (n + 1)

Tactic:
have := cfc_pow (fun x ↦ x⁻¹ : R → R) (n + 1) (a : A)

Goal state after:
case negSucc
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : ContinuousInv₀ R
a : Aˣ
ha : p ↑a
n : ℕ
this : cfc (fun x ↦ x⁻¹ ^ (n + 1)) ↑a = cfc (fun x ↦ x⁻¹) ↑a ^ (n + 1)
⊢ cfc (fun x ↦ x⁻¹ ^ (n + 1)) ↑a = ↑a⁻¹ ^ (n + 1)