mathlib-initiative/mathlib-tactics huggingface dataset:
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₀ : 𝕜
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hzero : f z₀ = 0
n : ℕ
H : ∀ {m : ℕ} {n : ℕ∞}, n = ↑m ↔ ↑m ≤ n ∧ ¬↑m + 1 ≤ n
⊢ ↑(n + 1) ≤ analyticOrderAt f z₀ ∧ ¬↑(n + 1) + 1 ≤ analyticOrderAt f z₀ ↔
    ↑(n + 1) ≤ analyticOrderAt f z₀ ∧ ¬↑(n + 1) ≤ analyticOrderAt (deriv f) z₀

Tactic:
analyticOrderAt_deriv_ge_iff hf hzero

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
z₀ : 𝕜
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hzero : f z₀ = 0
n : ℕ
H : ∀ {m : ℕ} {n : ℕ∞}, n = ↑m ↔ ↑m ≤ n ∧ ¬↑m + 1 ≤ n
⊢ ↑(n + 1) ≤ analyticOrderAt f z₀ ∧ ¬↑(n + 1) + 1 ≤ analyticOrderAt f z₀ ↔
    ↑(n + 1) ≤ analyticOrderAt f z₀ ∧ ¬↑(n + 1) + 1 ≤ analyticOrderAt f z₀
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
inst✝¹ : SecondCountableTopology 𝕜
inst✝ : CompleteSpace E
h : Meromorphic f
⊢ {z | AnalyticAt 𝕜 f z}ᶜ.Countable

Tactic:
simpa using (h.meromorphicOn (s := univ)).countable_compl_analyticAt_inter

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

Goal state before:
pp: case inl
⊢ (deriv fun x ↦ ↑x ^ 0) =O[atTop] fun x ↦ x ^ (re 0 - 1)

Tactic:
cpow_zero,

Goal state after:
case inl
⊢ (deriv fun x ↦ 1) =O[atTop] fun x ↦ x ^ (re 0 - 1)
Module: Mathlib.Analysis.Analytic.RadiusLiminf

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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
⊢ ∀ {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)

Tactic:
n

Goal state after:
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
n : ℕ
⊢ 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
Module: Mathlib.Topology.MetricSpace.MetricSeparated

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
⊢ AreSeparated (s ∪ s') t

Tactic:
refine ⟨min r r', ?_, fun x hx y hy => hx.elim ?_ ?_⟩

Goal state after:
case refine_1
X : Type u_1
inst✝ : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
⊢ min r r' ≠ 0

case refine_2
X : Type u_1
inst✝ : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
x : X
hx : x ∈ s ∪ s'
y : X
hy : y ∈ t
⊢ x ∈ s → min r r' ≤ edist x y

case refine_3
X : Type u_1
inst✝ : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
x : X
hx : x ∈ s ∪ s'
y : X
hy : y ∈ t
⊢ x ∈ s' → min r r' ≤ edist x y
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: ⊢ linearGrowthInf ⊤ = ⊤

Tactic:
nth_rw 2 [← liminf_const (f := atTop (α := ℕ)) ⊤]

Goal state after:
⊢ linearGrowthInf ⊤ = liminf (fun x ↦ ⊤) atTop
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : CommRing β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a ↦ |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
⊢ |k x ^ z| * |g x| ≤ |k x ^ z| * |f x|

Tactic:
by gcongr _ * ?_; exact hx

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

Goal state before:
pp: case inl
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mzero : 0 = m
⊢ ∃ a' ∈ A, m / τ ≤ δ a'

Tactic:
refine ⟨a, ⟨hat, a_disj⟩, ?_⟩

Goal state after:
case inl
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mzero : 0 = m
⊢ m / τ ≤ δ a
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
⊢ ∃ a' ∈ A, m / τ ≤ δ a'

Tactic:
· have I : m / τ < m := by
        rw [div_lt_iff₀ (zero_lt_one.trans hτ)]
        conv_lhs => rw [← mul_one m]
        gcongr
      rcases exists_lt_of_lt_csSup (Anonempty.image _) I with ⟨x, xA, hx⟩
      rcases (mem_image _ _ _).1 xA with ⟨a', ha', rfl⟩
      exact ⟨a', ha', hx.le⟩

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

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x ↦ ⨅ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ p, ⋃ q, u' ↑p ∩ v ↑p ↑q
μt : μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, x ∉ t
x : α
i : ↑s
H : x ∈ u' ↑i
hx : ↑i < f x
r : β
rs : r ∈ s
xr : ↑i < r
rq : r < f x
A : x ∈ v (↑i) r
⊢ x ∈ t

Tactic:
refine mem_iUnion.2 ⟨i, ?_⟩

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x ↦ ⨅ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ p, ⋃ q, u' ↑p ∩ v ↑p ↑q
μt : μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, x ∉ t
x : α
i : ↑s
H : x ∈ u' ↑i
hx : ↑i < f x
r : β
rs : r ∈ s
xr : ↑i < r
rq : r < f x
A : x ∈ v (↑i) r
⊢ x ∈ ⋃ q, u' ↑i ∩ v ↑i ↑q
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 α),
    MeasurableSet t →
      ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ → ∫⁻ (x : α) in tᶜ, f x ∂μ = ∫⁻ (x : α) in tᶜ, g x ∂μ

pp: 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 ∂μ

Tactic:
· intro t ht h_eq
    rw [setLIntegral_compl ht, setLIntegral_compl ht, h_eq, h_univ]
    · refine ne_of_lt ?_
      calc ∫⁻ x in t, g x ∂μ
      _ ≤ ∫⁻ x, g x ∂μ := setLIntegral_le_lintegral t _
      _ < ∞ := by rw [← h_univ]; exact hf_int.lt_top
    · refine ne_of_lt ?_
      calc ∫⁻ x in t, f x ∂μ
      _ ≤ ∫⁻ x, f x ∂μ := setLIntegral_le_lintegral t _
      _ < ∞ := hf_int.lt_top

Goal state after:
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.Sub

Goal state before:
pp: case a.refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
t : Set α
h_meas_t : MeasurableSet t
⊢ μ t ≤ (ν' + ν + ⊤.restrict sᶜ) t

Tactic:
← measure_inter_add_sdiff t h_meas_s

Goal state after:
case a.refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
t : Set α
h_meas_t : MeasurableSet t
⊢ μ (t ∩ s) + μ (t \ s) ≤ (ν' + ν + ⊤.restrict sᶜ) t
Module: Mathlib.MeasureTheory.Measure.Sub

Goal state before:
pp: case a.refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
t : Set α
h_meas_t : MeasurableSet t
⊢ μ (t ∩ s) + μ (t \ s) ≤ (ν' + ν + ⊤.restrict sᶜ) t

Tactic:
← measure_inter_add_sdiff t h_meas_s

Goal state after:
case a.refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
t : Set α
h_meas_t : MeasurableSet t
⊢ μ (t ∩ s) + μ (t \ s) ≤ (ν' + ν + ⊤.restrict sᶜ) (t ∩ s) + (ν' + ν + ⊤.restrict sᶜ) (t \ s)
Module: Mathlib.MeasureTheory.Measure.Sub

Goal state before:
pp: case a.refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
t : Set α
h_meas_t : MeasurableSet t
⊢ μ (t ∩ s) + μ (t \ s) ≤ (ν' + ν + ⊤.restrict sᶜ) (t ∩ s) + (ν' + ν + ⊤.restrict sᶜ) (t \ s)

Tactic:
← measure_inter_add_sdiff t h_meas_s

Goal state after:
case a.refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
t : Set α
h_meas_t : MeasurableSet t
⊢ μ (t ∩ s) + μ (t \ s) ≤ (ν' + ν + ⊤.restrict sᶜ) (t ∩ s) + (ν' + ν + ⊤.restrict sᶜ) (t \ s)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν = 0 ↔ μ ≪ ν

Tactic:
have h_dec := haveLebesgueDecomposition_add μ ν

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ μ.singularPart ν = 0 ↔ μ ≪ ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
⊢ ν.withDensity (μ.rnDeriv ν) = 0 ↔ μ ⟂ₘ ν

Tactic:
have h_dec := haveLebesgueDecomposition_add μ ν

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ ν.withDensity (μ.rnDeriv ν) = 0 ↔ μ ⟂ₘ ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ (μ.singularPart ν).singularPart ν = μ.singularPart ν

Tactic:
rw [Measure.singularPart_eq_self]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ.singularPart ν ⟂ₘ ν
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, ∃ᶠ (ε : ℝ) in 𝓝[>] 0, ∃ a ∈ t, r a = ε ∧ c a = x
x : α
hx : x ∈ s
ε : ℝ
⊢ ε > 0 → ∃ a ∈ t, r a ≤ ε ∧ c a = x

Tactic:
hε

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, ∃ᶠ (ε : ℝ) in 𝓝[>] 0, ∃ a ∈ t, r a = ε ∧ c a = x
x : α
hx : x ∈ s
ε : ℝ
hε : ε > 0
⊢ ∃ a ∈ t, r a ≤ ε ∧ c a = x
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
n : ℕ
s : Set α
hs : MeasurableSet s
hs_le : ∀ (t : Set α), MeasurableSet t → t ⊆ s → ((1 / (↑n + 1)) • ν) t ≤ μ t
hs_ge : ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ((1 / (↑n + 1)) • ν) t
t : Set α
ht : MeasurableSet t
⊢ μ (t ∩ sᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ sᶜ)

Tactic:
· exact hs_ge (t ∩ sᶜ) (ht.inter hs.compl) inter_subset_right

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

Goal state before:
pp: case refine_5
α : 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 : ℕ), μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0

Tactic:
n

Goal state after:
case refine_5
α : 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 : ℕ
⊢ μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
⊢ ⨆ p, ∑ i ∈ Finset.range p.fst, edist (f (↑p.snd (i + 1))) (f (↑p.snd i)) ≤ eVariationOn f s

Tactic:
apply iSup_le
    rintro ⟨n, u, u_mono, u_mem⟩
    apply sum_le_of_monotoneOn_Iic (by grind [MonotoneOn, StrictMonoOn]) (by grind)

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

Goal state before:

Tactic:
(∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) =
          ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) := by grind [Finset.sum_congr]
      _ ≤ ∑ j ∈ Finset.range (n + 2), edist (f (v (j + 1))) (f (v j)) := by
        gcongr
        apply Nat.le_add_right

Goal state after:
Module: Mathlib.Topology.ContinuousMap.StarOrdered

Goal state before:
pp: α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : PartialOrder R
inst✝⁶ : NonUnitalSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : TopologicalSpace R
inst✝² : ContinuousStar R
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousSqrt R
⊢ StarOrderedRing C(α, R)

Tactic:
refine StarOrderedRing.of_le_iff ?_
  intro f g
  constructor
  · rw [ContinuousMap.le_def]
    intro h
    use (mk _ ContinuousSqrt.continuousOn_sqrt.domRestrict).comp
      ⟨_, map_continuous (f.prodMk g) |>.codRestrict (s := {x | x.1 ≤ x.2}) (by exact h)⟩
    ext x
    simpa [IsSelfAdjoint.star_eq <| .of_nonneg (ContinuousSqrt.sqrt_nonneg (f x, g x) (h x))]
      using ContinuousSqrt.sqrt_mul_sqrt (f x, g x) (h x)
  · rintro ⟨p, rfl⟩
    exact fun x ↦ le_add_of_nonneg_right (star_mul_self_nonneg (p x))

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

Goal state before:
pp: case e_a
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this✝ : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
m : ℕ
v : ℕ → α
hv : Monotone v
vt : ∀ (i : ℕ), v i ∈ t
w : ℕ → α := fun i ↦ if i ≤ n then u i else v (i - (n + 1))
⊢ ∑ i ∈ Finset.Ico 0 m, edist (f (w (n + 1 + i + 1))) (f (w (n + 1 + i))) =
    ∑ i ∈ Finset.Ico (n + 1) (n + 1 + m), edist (f (w (i + 1))) (f (w i))

Tactic:
convert!
          Finset.sum_Ico_add (fun i : ℕ => edist (f (w (i + 1))) (f (w i))) 0 m (n + 1) using 3 <;>
        abel

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 μ
s : Set α
t : Set α := ⋯
⊢ {x | (fun x ↦ Tendsto (fun a ↦ μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))) x} ∈ ae μ

Tactic:
apply ae_tendsto_measure_inter_div_of_measurableSet

Goal state after:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set α := ⋯
⊢ MeasurableSet t
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 μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
⊢ ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ∞

Tactic:
convert! h'f using 1

Goal state after:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
⊢ ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ = ∫⁻ (y : α), f 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
f✝ g : R → R
a✝ : A
ha : p a✝
hf : ContinuousOn f✝ (spectrum R a✝)
hg : ContinuousOn g (spectrum R a✝)
f : R → R
a : A
⊢ Commute (star (cfc f a)) (cfc f a)

Tactic:
Commute,

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
f✝ g : R → R
a✝ : A
ha : p a✝
hf : ContinuousOn f✝ (spectrum R a✝)
hg : ContinuousOn g (spectrum R a✝)
f : R → R
a : A
⊢ SemiconjBy (star (cfc f a)) (cfc f a) (cfc f 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✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing 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
ha : p a
hf : ContinuousOn f (spectrum R a)
⊢ cfc (fun x ↦ -f x) a = -cfc f a

Tactic:
rw [cfc_apply f a, ← map_neg, cfc_apply ..]

Goal state after:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing 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
ha : p a
hf : ContinuousOn f (spectrum R a)
⊢ (cfcHom ha) { toFun := (spectrum R a).domRestrict fun x ↦ -f x, continuous_toFun := ⋯ } =
    (cfcHom ha) (-{ toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ })