mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case inr.convert_5
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)
⊢ HasDerivAt (fun y ↦ y) 1 ↑(-x)

pp: case inr.convert_6
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)
⊢ ↑(-x) ∈ slitPlane

Tactic:
· exact hasDerivAt_id ((-x : ℝ) : ℂ)

Goal state after:
case inr.convert_6
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)
⊢ ↑(-x) ∈ slitPlane
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
    simp only [ContinuousLinearMap.compFormalMultilinearSeries_apply,
      ContinuousLinearMap.compContinuousMultilinearMap_coe, Function.comp_apply,
      FormalMultilinearSeries.compContinuousLinearMap_apply]
    simp
    norm_cast

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : E → ℝ
x : E
n : WithTop ℕ∞
hf : ContDiffAt ℝ n f x
hg : ContDiffAt ℝ n g x
h : f x ≠ 0
⊢ ContDiffAt ℝ n (fun x ↦ f x ^ g x) x

Tactic:
exact (contDiffAt_rpow_of_ne (f x, g x) h).comp x (hf.prodMk hg)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
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
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n) f s
g : E → F := fun z ↦ (p n) fun x_1 ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F := fun k ↦ if h : n = k then h ▸ p n else 0
A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
B : HasFPowerSeriesWithinOnBall g q s x r
J1 : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n g s x + iteratedFDerivWithin 𝕜 n (f - g) s x
⊢ AnalyticOn 𝕜 g s

Tactic:
apply gcont.contDiffOn.analyticOn

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

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
ε : ℝ≥0
s N : Set X
inst✝ : ProperSpace X
hN : IsClosed N
⊢ IsCover ε (closure s) N ↔ IsCover ε s N

Tactic:
simpa [isCover_iff_subset_cthickening hN] using (isClosed_cthickening (E := N)).closure_subset_iff

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

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

Tactic:
by
  rw [expGrowthInf, le_liminf_iff']
  refine forall₂_congr fun b _ ↦ eventually_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)
  nth_rw 1 [le_div_iff_mul_le (by norm_cast) (natCast_ne_top n), ← log_exp (b * n)]
  exact logOrderIso.le_iff_le

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

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

Tactic:
log_mul_add,

Goal state after:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ (u n).log / ↑n + (v n).log / ↑n = ((u n).log + (v n).log) / ↑n
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
n : ℕ
⊢ (u n).log / ↑n + (v n).log / ↑n = (u n * v n).log / ↑n

Tactic:
log_mul_add,

Goal state after:
u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
n : ℕ
⊢ (u n).log / ↑n + (v n).log / ↑n = ((u n).log + (v n).log) / ↑n
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

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

Tactic:
apply (expGrowthSup_eventually_monotone h).trans' (le_expGrowthSup_mul'.trans' _)
  rcases eq_top_or_lt_top b with rfl | b_top
  · exact expGrowthInf_top ▸ le_add_of_nonneg_left le_top
  · rw [expGrowthInf_const hb b_top.ne, zero_add]

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

Goal state before:
pp: case empty
α : Type u_1
u : α → ℕ → ℝ≥0∞
⊢ expGrowthSup 0 = ⨆ x ∈ ↑∅, expGrowthSup (u x)

Tactic:
Finset.coe_empty,

Goal state after:
case empty
α : Type u_1
u : α → ℕ → ℝ≥0∞
⊢ expGrowthSup 0 = ⨆ x ∈ ∅, expGrowthSup (u x)
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : f =ᵐ[μ] g
⊢ ⨍⁻ (x : α), f x ∂μ = ⨍⁻ (x : α), g x ∂μ

Tactic:
by
  simp only [laverage_eq, lintegral_congr_ae h]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A : ∀ (ε N : ℝ≥0) (p : ℕ), 0 < ε → μ ({x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p) = 0
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : ℕ → Set α := fun n ↦ {x | g x + ↑(u n) ≤ f x ∧ g x ≤ ↑↑n} ∩ spanningSets μ n
μs : ∀ (n : ℕ), μ (s n) = 0
x : α
hx : g x < f x
L1 : ∀ᶠ (n : ℕ) in atTop, g x + ↑(u n) ≤ f x
⊢ Tendsto (fun n ↦ ↑↑n) atTop (𝓝 ∞)

Tactic:
by
        simp only [ENNReal.coe_natCast]
        exact ENNReal.tendsto_nat_nhds_top

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ᶜ
⊢ f x = g x

Tactic:
h1 (Set.inter_subset_left 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 = g x
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ᶜ
⊢ f x = g x

Tactic:
rw [h1 (Set.inter_subset_left hx), h2 (Set.inter_subset_right hx)]

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

Goal state before:
pp: 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 α
ht : MeasurableSet t
h_eq : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
⊢ ∫⁻ (x : α) in tᶜ, f x ∂μ = ∫⁻ (x : α) in tᶜ, g x ∂μ

Tactic:
rw [setLIntegral_compl ht, setLIntegral_compl ht, h_eq, h_univ]

Goal state after:
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 α
ht : MeasurableSet t
h_eq : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
⊢ ∫⁻ (x : α) in t, 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 α
ht : MeasurableSet t
h_eq : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
⊢ ∫⁻ (x : α) in t, f x ∂μ ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Sub

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
s : Set α
hs : MeasurableSet s
⊢ (μ + ν - ν) s = μ s

Tactic:
rw [sub_apply hs (Measure.le_add_left (le_refl _)), add_apply,
    ENNReal.add_sub_cancel_right (measure_ne_top ν s)]

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

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hs : NullMeasurableSet s μ
hμ₁ : μ s ≠ ∞
g : α → ℝ≥0∞
hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
this : 0 < (μ.restrict s) ({a | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x | g x = ∞})
x : α
hfx : ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal
hx : x ∉ {x | g x = ∞}
⊢ ∀ᵐ (x : α) ∂μ.restrict s, g x ≠ ∞

Tactic:
· simp_rw [ae_iff, not_ne_iff]
    exact measure_eq_top_of_lintegral_ne_top hg.aemeasurable hint

Goal state after:
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 μ
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
K : ℝ
μK : μ (closedBall x K) < ∞
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : ∑' (a : ↑v), μ (B ↑a) < ∞
w : Finset ↑v
hw : ∑' (a : { a // a ∉ w }), μ (B ↑↑a) < ε / ↑C
z : α
hz : z ∈ (s \ ⋃ a ∈ u, B a) ∩ ball x (R x)
k : Set α := ⋃ a ∈ w, B ↑a
k_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] k
z_notmem_k : z ∉ k
⊢ ball x (R x) \ k ∈ 𝓝 z

Tactic:
apply IsOpen.mem_nhds (isOpen_ball.sdiff k_closed) _

Goal state after:
α : 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 ι := ⋯
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 ι := ⋯
vu : v ⊆ u
K : ℝ
μK : μ (closedBall x K) < ∞
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : ∑' (a : ↑v), μ (B ↑a) < ∞
w : Finset ↑v
hw : ∑' (a : { a // a ∉ w }), μ (B ↑↑a) < ε / ↑C
z : α
hz : z ∈ (s \ ⋃ a ∈ u, B a) ∩ ball x (R x)
k : Set α := ⋯
k_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] k
z_notmem_k : z ∉ k
⊢ z ∈ ball x (R x) \ k
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))
x : α
hx : x ∈ s
⊢ f x = g x

Tactic:
simp only [g]

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))
x : α
hx : x ∈ s
⊢ f x = if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
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
n : ℕ
⊢ Measurable (⨆ k, ⨆ (_ : k ≤ n), f k)

Tactic:
convert! (iSup_mem_measurableLE _ hf₁ n).1

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
ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
n : ℕ
x✝ : α
⊢ (⨆ k, ⨆ (_ : k ≤ n), f k) x✝ = ⨆ k, ⨆ (_ : k ≤ n), f k x✝
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: case hinf
α : 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 α := ⋯
o : ℕ → Set α := ⋯
u : ℕ → Set α := ⋯
w : ℕ → Set α := ⋯
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
⊢ μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≠ ∞

Tactic:
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

Goal state after:
case hinf
α : 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
⊢ (ρ + μ) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≠ ∞
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a : α
⊢ ENNReal.toReal 0 = 0

pp: case hs
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a : α
⊢ (s ∩ {a}).Subsingleton

Tactic:
ENNReal.toReal_zero

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a : α
⊢ 0 = 0

case hs
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a : α
⊢ (s ∩ {a}).Subsingleton
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : 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
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)

Tactic:
by
  rcases le_total x y with (h | h)
  · rw [variationOnFromTo.eq_of_le _ _ h, variationOnFromTo.eq_of_le _ _ (hφ hx hy h),
      eVariationOn.comp_inter_Icc_eq_of_monotoneOn f φ hφ hx hy]
  · rw [variationOnFromTo.eq_of_ge _ _ h, variationOnFromTo.eq_of_ge _ _ (hφ hy hx h),
      eVariationOn.comp_inter_Icc_eq_of_monotoneOn f φ hφ hy hx]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst✝¹ : SigmaFinite ν
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (ν (s n) < ∞)
ξ : ℕ → Measure α := fun n ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun n ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
hξ : sum ξ ⟂ₘ ν
⊢ sum ξ + ν.withDensity (∑' (n : ℕ), f n) = sum fun n ↦ ξ n + ν.withDensity (f n)

Tactic:
rw [withDensity_tsum hfm, Measure.sum_add_sum]

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✝⁸ : 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
f g : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
⊢ cfc (fun x ↦ f x * g x) a = cfc f a * cfc g a

Tactic:
by_cases ha : p a
  · rw [cfc_apply f a, cfc_apply g a, ← map_mul, cfc_apply _ a]
    congr
  · simp [cfc_apply_of_not_predicate a 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✝⁹ : 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✝ : Nontrivial A
r : R
⊢ spectrum R ((algebraMap R A) r) = {r}

Tactic:
have hp : p 0 := cfc_predicate_zero R

Goal state after:
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✝ : Nontrivial A
r : R
hp : p 0
⊢ spectrum R ((algebraMap R A) r) = {r}
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✝ : Nontrivial A
r : R
hp : p 0
⊢ spectrum R ((algebraMap R A) r) = {r}

Tactic:
rw [← cfc_const r 0 hp, cfc_map_spectrum (fun _ => r) 0 hp]

Goal state after:
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✝ : Nontrivial A
r : R
hp : p 0
⊢ (fun x ↦ r) '' spectrum R 0 = {r}
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
inst✝ : ContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (fun x ↦ f x * (f x)⁻¹) a = cfc 1 a

Tactic:
exact cfc_congr fun _ _ ↦ by aesop

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
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
⊢ Tendsto (fun y ↦ eVariationOn f (s ∩ Icc y x)) (𝓝[s] x) (𝓝 0)

Tactic:
apply (hf.tendsto_eVariationOn_Ico_zero x).congr (fun y ↦ ?_)

Goal state after:
α : 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 : α
⊢ eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)