mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst✝¹] (s n)
h'' : univ ⊆ ⋃ n, s n
r : ℝ≥0∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAs : ∀ (n : ℕ), A n ⊆ s n
hAd : Pairwise (Disjoint on A)
hA : MeasurableSet (⋃ n, A n)
hr : r > μ (⋃ n, A n)
HA : μ (⋃ n, A n) < ∞
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : μ (⋃ n, A n) + ∑' (i : ℕ), δ i < r
n : ℕ
H₁ : ∀ (t : Set α), (μ.restrict (s n)) t = μ (t ∩ s n)
⊢ (μ.restrict (s n)) (A n) ≠ ∞

Tactic:
H₁

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst✝¹] (s n)
h'' : univ ⊆ ⋃ n, s n
r : ℝ≥0∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAs : ∀ (n : ℕ), A n ⊆ s n
hAd : Pairwise (Disjoint on A)
hA : MeasurableSet (⋃ n, A n)
hr : r > μ (⋃ n, A n)
HA : μ (⋃ n, A n) < ∞
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : μ (⋃ n, A n) + ∑' (i : ℕ), δ i < r
n : ℕ
H₁ : ∀ (t : Set α), (μ.restrict (s n)) t = μ (t ∩ s n)
⊢ μ (A n ∩ s n) ≠ ∞
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h1 : Disjoint H K
h2 : ↑H * ↑K = univ
g h : G
hh : h ∈ ↑H
k : G
hk : k ∈ ↑K
hg : (fun x1 x2 ↦ x1 * x2) h k = g
⊢ ∃ a, (fun x ↦ ↑x.1 * ↑x.2) a = g

Tactic:
exact ⟨(⟨h, hh⟩, ⟨k, hk⟩), hg⟩

Goal state after:
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ μ (s ∩ c⁻¹ • t) = μ (c • s ∩ t)

Tactic:
← measure_smul _ c,

Goal state after:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ μ (c • (s ∩ c⁻¹ • t)) = μ (c • s ∩ t)
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ μ (s ∪ c⁻¹ • t) = μ (c • s ∪ t)

Tactic:
← measure_smul _ c,

Goal state after:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ μ (c • (s ∪ c⁻¹ • t)) = μ (c • s ∪ t)
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ μ (s \ c⁻¹ • t) = μ (c • s \ t)

Tactic:
← measure_smul _ c,

Goal state after:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ μ (c • (s \ c⁻¹ • t)) = μ (c • s \ t)
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ μ (s ∆ (c⁻¹ • t)) = μ ((c • s) ∆ t)

Tactic:
← measure_smul _ c,

Goal state after:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ μ (c • s ∆ (c⁻¹ • t)) = μ ((c • s) ∆ t)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
this :
  (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) =
    sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))
⊢ map Prod.swap ((sum (sfiniteSeq μ)).prod ν) = ν.prod (sum (sfiniteSeq μ))

Tactic:
← sum_sfiniteSeq ν,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
this :
  (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) =
    sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))
⊢ map Prod.swap ((sum (sfiniteSeq μ)).prod (sum (sfiniteSeq ν))) = (sum (sfiniteSeq ν)).prod (sum (sfiniteSeq μ))
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
inst✝² : SFinite ν
inst✝¹ : SFinite μ
inst✝ : SFinite τ
this :
  (sum fun p ↦ (sfiniteSeq μ p.1).prod ((sfiniteSeq ν p.2.1).prod (sfiniteSeq τ p.2.2))) =
    sum fun p ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2))
⊢ map (⇑MeasurableEquiv.prodAssoc) (((sum (sfiniteSeq μ)).prod ν).prod τ) = (sum (sfiniteSeq μ)).prod (ν.prod τ)

Tactic:
← sum_sfiniteSeq ν,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
inst✝² : SFinite ν
inst✝¹ : SFinite μ
inst✝ : SFinite τ
this :
  (sum fun p ↦ (sfiniteSeq μ p.1).prod ((sfiniteSeq ν p.2.1).prod (sfiniteSeq τ p.2.2))) =
    sum fun p ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2))
⊢ map (⇑MeasurableEquiv.prodAssoc) (((sum (sfiniteSeq μ)).prod (sum (sfiniteSeq ν))).prod τ) =
    (sum (sfiniteSeq μ)).prod ((sum (sfiniteSeq ν)).prod τ)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
⊢ ((sum (sfiniteSeq μ)).restrict s).prod (ν.restrict t) = ((sum (sfiniteSeq μ)).prod ν).restrict (s ×ˢ t)

Tactic:
← sum_sfiniteSeq ν,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
⊢ ((sum (sfiniteSeq μ)).restrict s).prod ((sum (sfiniteSeq ν)).restrict t) =
    ((sum (sfiniteSeq μ)).prod (sum (sfiniteSeq ν))).restrict (s ×ˢ t)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
x : α
⊢ (dirac x).prod ν = map (Prod.mk x) ν

Tactic:
← sum_sfiniteSeq ν,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
x : α
⊢ (dirac x).prod (sum (sfiniteSeq ν)) = map (Prod.mk x) (sum (sfiniteSeq ν))
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : SFinite ν
inst✝¹ : SFinite μ
ν' : Measure β
inst✝ : SFinite ν'
⊢ μ.prod (ν + ν') = μ.prod ν + μ.prod ν'

Tactic:
← sum_sfiniteSeq ν,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : SFinite ν
inst✝¹ : SFinite μ
ν' : Measure β
inst✝ : SFinite ν'
⊢ μ.prod (sum (sfiniteSeq ν) + ν') = μ.prod (sum (sfiniteSeq ν)) + μ.prod ν'
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : SFinite ν
inst✝¹ : SFinite μ
μ' : Measure α
inst✝ : SFinite μ'
⊢ (sum fun n ↦ sfiniteSeq μ n + sfiniteSeq μ' n).prod ν = (sum (sfiniteSeq μ)).prod ν + (sum (sfiniteSeq μ')).prod ν

Tactic:
← sum_sfiniteSeq ν,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : SFinite ν
inst✝¹ : SFinite μ
μ' : Measure α
inst✝ : SFinite μ'
⊢ (sum fun n ↦ sfiniteSeq μ n + sfiniteSeq μ' n).prod (sum (sfiniteSeq ν)) =
    (sum (sfiniteSeq μ)).prod (sum (sfiniteSeq ν)) + (sum (sfiniteSeq μ')).prod (sum (sfiniteSeq ν))
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case h₂
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := ⋯
hu : u.Countable
t' : Set α := ⋯
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ MeasurableSet (g '' t')

Tactic:
· exact hu.mono (by simp [t']) |>.measurableSet

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSpace H
inst✝³ : DivisionMonoid G
inst✝² : MeasurableMul G
inst✝¹ : MeasurableInv G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ map (fun x ↦ x * g) (map inv μ) = map inv (map (fun x ↦ g⁻¹ * x) μ)

Tactic:
map_map (measurable_mul_const g) measurable_inv,

Goal state after:
G : Type u_1
H : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSpace H
inst✝³ : DivisionMonoid G
inst✝² : MeasurableMul G
inst✝¹ : MeasurableInv G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ map ((fun x ↦ x * g) ∘ inv) μ = map inv (map (fun x ↦ g⁻¹ * x) μ)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
s : Set β
hs : MeasurableSet s
⊢ ρ.snd s = ρ (Prod.snd ⁻¹' s)

Tactic:
by
  rw [snd, Measure.map_apply measurable_snd hs]

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

Goal state before:
pp: case succ
G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed[inst✝⁷] K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n ↦ (fun T ↦ T ∪ g T • K)^[n] K
n : ℕ
IH : IsCompact (L n)
⊢ IsCompact (L (n + 1))

Tactic:
L,

Goal state after:
case succ
G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed[inst✝⁷] K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n ↦ (fun T ↦ T ∪ g T • K)^[n] K
n : ℕ
IH : IsCompact (L n)
⊢ IsCompact ((fun T ↦ T ∪ g T • K)^[n + 1] K)
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: case succ
G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed[inst✝⁷] K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n ↦ (fun T ↦ T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
n : ℕ
IH : IsClosed[inst✝⁷] (L n)
⊢ IsClosed[inst✝⁷] (L (n + 1))

Tactic:
L,

Goal state after:
case succ
G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed[inst✝⁷] K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n ↦ (fun T ↦ T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
n : ℕ
IH : IsClosed[inst✝⁷] (L n)
⊢ IsClosed[inst✝⁷] ((fun T ↦ T ∪ g T • K)^[n + 1] K)
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
s : Set G
x✝ : MeasurableSet s
⊢ μ.inv s = 0 → μ s = 0

Tactic:
simp_rw [inv_apply μ s, measure_inv_null, imp_self]

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

Goal state before:
pp: G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed[inst✝⁷] K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n ↦ (fun T ↦ T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed[inst✝⁷] (L n)
n : ℕ
IH : μ (L n) = ↑(n + 1) * μ K
⊢ μ (L (n + 1)) = μ (L n) + μ (g (L n) • K)

Tactic:
L,

Goal state after:
G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed[inst✝⁷] K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n ↦ (fun T ↦ T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed[inst✝⁷] (L n)
n : ℕ
IH : μ (L n) = ↑(n + 1) * μ K
⊢ μ ((fun T ↦ T ∪ g T • K)^[n + 1] K) = μ ((fun T ↦ T ∪ g T • K)^[n] K) + μ (g ((fun T ↦ T ∪ g T • K)^[n] K) • K)
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
⊢ μ.withDensity f ≤ μ.withDensity g

Tactic:
refine le_iff.2 fun s hs ↦ ?_
  rw [withDensity_apply _ hs, withDensity_apply _ hs]
  refine setLIntegral_mono_ae' hs ?_
  filter_upwards [hfg] with x h_le using fun _ ↦ h_le

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst✝ : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ) s
this : Tendsto (fun a ↦ ∑ i ∈ a, (μ i) s) atTop (𝓝 ((sum μ) s))
a : Finset ι
ha : r < (∑ i ∈ a, μ i) s
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : r < (∑ i ∈ a, μ i) K
⊢ ∑ c ∈ a, (μ c) K ≤ (sum μ) K

Tactic:
exact (ENNReal.sum_le_tsum _).trans (le_sum_apply _ _)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ μ.withDensity f ≪ μ

Tactic:
refine AbsolutelyContinuous.mk fun s hs₁ hs₂ => ?_

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs₁ : MeasurableSet s
hs₂ : μ s = 0
⊢ (μ.withDensity f) s = 0
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : ¬c = 0
⊢ (c • μ).InnerRegularCompactLTTop

Tactic:
by_cases h'c : c = ∞

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : ¬c = 0
h'c : c = ∞
⊢ (c • μ).InnerRegularCompactLTTop

case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : ¬c = 0
h'c : ¬c = ∞
⊢ (c • μ).InnerRegularCompactLTTop
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ∞
this : (μ.restrict A).WeaklyRegular
V : Set α
hV : IsOpen[inst✝³] V
r : ℝ≥0∞
hr : r < (μ.restrict A) V
R : (μ.restrict A) V ≠ ∞
⊢ ∃ K ⊆ V, IsCompact K ∧ r < (μ.restrict A) K

Tactic:
exact MeasurableSet.exists_lt_isCompact_of_ne_top hV.measurableSet R hr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : PseudoEMetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (f n a) (g a) < ε)} = 0
x : α
⊢ x ∈ s ∩ ⋂ j, notConvergentSeq f g n j → x ∈ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (f n a) (g a) < ε)}

Tactic:
simp only [Set.mem_inter_iff, Set.mem_iInter, mem_notConvergentSeq_iff]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : PseudoEMetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (f n a) (g a) < ε)} = 0
x : α
⊢ (x ∈ s ∧ ∀ (i : ι), ∃ k ≥ i, (↑n)⁻¹ < edist (f k x) (g x)) →
    x ∈ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (f n a) (g a) < ε)}
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ iUnionNotConvergentSeq hε hf hsm hs hfg ⊆ s

Tactic:
iUnionNotConvergentSeq,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ ⋃ n, s ∩ notConvergentSeq f g n (notConvergentSeqLTIndex ⋯ hf hsm hs hfg n) ⊆ s
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : HasFiniteIntegral f μ
x : α
⊢ ‖min (f x) 0‖ ≤ ‖f x‖

Tactic:
simpa [abs_le] using neg_abs_le _

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
C : ℝ
_C_pos : 0 < C
hC : ∀ (x : V₁), ‖φ x‖ ≤ C * ‖x‖
⊢ ∃ C, ∀ (v : V₁), ‖⟨φ v, ⋯⟩‖ ≤ C * ‖v‖

Tactic:
exact ⟨C, hC⟩

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : Group α
inst✝ : MulAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
H₁ : ∀ (a : α), π (a • b) = π b
⊢ ∑' (a : α), g (π (a • b)) • f (a • b) = g (π b) • ∑' (a : α), f (a • b)

Tactic:
H₁

Goal state after:
case h
α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : Group α
inst✝ : MulAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
H₁ : ∀ (a : α), π (a • b) = π b
⊢ ∑' (a : α), g (π b) • f (a • b) = g (π b) • ∑' (a : α), f (a • b)
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: z : ℂ
⊢ ‖equivRealProd z‖ ≤ 1 * ‖z‖

Tactic:
simpa using equivRealProd_apply_le z

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

Goal state before:
pp: x : ℂ
y : ℝ
hx : IsSelfAdjoint x
⊢ y = RCLike.re x ↔ ↑y = x

Tactic:
exact RCLike.ofReal_eq_re_of_isSelfAdjoint hx

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (x₁ * y₂ + y₁ * x₂) • I' = (algebraMap ℝ A) x₁ * y₂ • I' + y₁ • I' * (algebraMap ℝ A) x₂

Tactic:
· rw [smul_def, smul_def, smul_def, ← right_comm _ x₂,
      ← mul_assoc, ← add_mul, ← map_mul, ← map_mul, ← map_add]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ ↑(im z) = I * ((starRingEnd K) z - z) / 2

Tactic:
by
  rw [← neg_inj, ← ofReal_neg, ← I_mul_re, re_eq_add_conj, map_mul, conj_I, ← neg_div, ← mul_neg,
    neg_sub, mul_sub, neg_mul, sub_eq_add_neg]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
x✝ : (starRingEnd K) z = z
h : (starRingEnd K) z = z := x✝
⊢ 0 = ↑0

Tactic:
ofReal_zero

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
x✝ : (starRingEnd K) z = z
h : (starRingEnd K) z = z := x✝
⊢ 0 = 0
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: A : Type u_1
inst✝⁴ : SeminormedAddCommGroup A
inst✝³ : StarAddMonoid A
inst✝² : NormedSpace ℂ A
inst✝¹ : StarModule ℂ A
inst✝ : NormedStarGroup A
x : A
⊢ ‖realPart (Complex.I • -x)‖ ≤ ‖x‖

Tactic:
by simpa only [smul_neg, map_neg, realPart_I_smul, neg_neg,
        AddSubgroupClass.coe_norm, norm_neg, norm_smul, Complex.norm_I, one_mul] using
        realPart.norm_le (Complex.I • (-x))

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: z : ℂ
⊢ ↑(ℜ z) = ↑z.re

Tactic:
conv_lhs => rw [← re_add_im z]

Goal state after:
z : ℂ
⊢ ↑(ℜ (↑z.re + ↑z.im * I)) = ↑z.re
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z w : K
⊢ im (z / w) = im z * re w / normSq w - re z * im w / normSq w

Tactic:
by
  simp only [div_eq_mul_inv, mul_assoc, sub_eq_add_neg, add_comm, neg_mul, mul_neg,
    rclike_simps]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ re z ≤ -‖z‖ ↔ z = -↑‖z‖

Tactic:
simpa [neg_eq_iff_eq_neg, le_neg] using norm_le_re_iff_eq_norm (z := -z)

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Z → X
h : f ⁻¹' e.source = univ
⊢ Continuous[inst✝, inst✝²] f ↔ Continuous[inst✝, inst✝¹] (↑e ∘ f)

Tactic:
simp only [← continuousOn_univ]

Goal state after:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Z → X
h : f ⁻¹' e.source = univ
⊢ ContinuousOn f univ ↔ ContinuousOn (↑e ∘ f) univ