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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → Measure α
h : ∀ (s : Set α), MeasurableSet s → Measurable fun b ↦ (f b) s
s : Set α
hs : MeasurableSet s
⊢ borel ℝ≥0∞ ≤ MeasurableSpace.map (fun μ ↦ μ s) (MeasurableSpace.map f mβ)

Tactic:
rw [MeasurableSpace.map_comp]; exact h s hs

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : ∑' (i : α), a i ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ count {i | ε ≤ a i} ≤ ↑c / ↑ε

Tactic:
rw [show (fun i => ε ≤ a i) = fun i => (ε : ℝ≥0∞) ≤ ((↑) ∘ a) i by
      simp only [ENNReal.coe_le_coe, Function.comp]]
  apply
    ENNReal.count_const_le_le_of_tsum_le (measurable_coe_nnreal_ennreal.comp a_mble) _
      (mod_cast ε_ne_zero) (@ENNReal.coe_ne_top ε)
  convert! ENNReal.coe_le_coe.mpr tsum_le_c
  simp_rw [Function.comp_apply]
  rw [ENNReal.tsum_coe_eq a_summable.hasSum]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun x ↦ ⨆ n, g n x
hφm : Measurable φ
hφle : φ ≤ f
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ

Tactic:
refine ⟨φ, hφm, hφle, fun s ↦ ?_⟩

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun x ↦ ⨆ n, g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, φ a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
s : ℕ → Set α := disjointed (spanningSets μ)
this : ∀ (n : ℕ), μ (s n) < ∞
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
δsum : ∑' (i : ℕ), μ (s i) * ↑(δ i) < ε
N : α → ℕ := spanningSetsIndex μ
hN_meas : Measurable N
hNs : ∀ (n : ℕ), N ⁻¹' {n} = s n
⊢ ∫⁻ (x : α), ↑(δ (N x)) ∂μ < ε

Tactic:
← Function.comp_apply (f := (fun n ↦ (↑(δ n) : ℝ≥0∞))),

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
s : ℕ → Set α := disjointed (spanningSets μ)
this : ∀ (n : ℕ), μ (s n) < ∞
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
δsum : ∑' (i : ℕ), μ (s i) * ↑(δ i) < ε
N : α → ℕ := spanningSetsIndex μ
hN_meas : Measurable N
hNs : ∀ (n : ℕ), N ⁻¹' {n} = s n
⊢ ∫⁻ (x : α), ((fun n ↦ ↑(δ n)) ∘ N) x ∂μ < ε
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → Measure β
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (μ : Measure β), μ s ∂map f m ≤ ∫⁻ (a : α), (f a) s ∂m

Tactic:
apply lintegral_map_le

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: case const.refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
this : L / ↑c < μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < μ t
t_top : μ t < ∞
x✝ x : α
⊢ 0 x ≤ (const α c) x

Tactic:
exact zero_le

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : AEMeasurable f m
hg : AEMeasurable g (m.bind f)
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (a : α), ∫⁻ (x : β), (g x) s ∂f a ∂m = ∫⁻ (a : α), ((f a).bind g) s ∂m

Tactic:
exact lintegral_congr_ae <| (hf.ae_of_bind hg).mono fun a ha ↦ .symm <| bind_apply hs ha

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
⊢ ∀ (c : ℝ≥0∞) ⦃s : Set (α × β)⦄, MeasurableSet s → Measurable fun x ↦ ∫⁻ (y : β), s.indicator (fun x ↦ c) (x, y) ∂ν

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
⊢ ∀ ⦃f g : α × β → ℝ≥0∞⦄,
    Disjoint (support f) (support g) →
      Measurable f →
        Measurable g →
          (Measurable fun x ↦ ∫⁻ (y : β), f (x, y) ∂ν) →
            (Measurable fun x ↦ ∫⁻ (y : β), g (x, y) ∂ν) → Measurable fun x ↦ ∫⁻ (y : β), (f + g) (x, y) ∂ν

pp: case refine_3
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
⊢ ∀ ⦃f : ℕ → α × β → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ), Measurable fun x ↦ ∫⁻ (y : β), f n (x, y) ∂ν) →
          Measurable fun x ↦ ∫⁻ (y : β), (fun x ↦ ⨆ n, f n x) (x, y) ∂ν

Tactic:
· intro c s hs
    simp only [← indicator_comp_right]
    suffices Measurable fun x => c * ν (Prod.mk x ⁻¹' s) by simpa [lintegral_indicator (m hs)]
    exact (measurable_measure_prodMk_left hs).const_mul _

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
⊢ ∀ ⦃f g : α × β → ℝ≥0∞⦄,
    Disjoint (support f) (support g) →
      Measurable f →
        Measurable g →
          (Measurable fun x ↦ ∫⁻ (y : β), f (x, y) ∂ν) →
            (Measurable fun x ↦ ∫⁻ (y : β), g (x, y) ∂ν) → Measurable fun x ↦ ∫⁻ (y : β), (f + g) (x, y) ∂ν

case refine_3
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
⊢ ∀ ⦃f : ℕ → α × β → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ), Measurable fun x ↦ ∫⁻ (y : β), f n (x, y) ∂ν) →
          Measurable fun x ↦ ∫⁻ (y : β), (fun x ↦ ⨆ n, f n x) (x, y) ∂ν
Module: Mathlib.MeasureTheory.Group.MeasurableEquiv

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ : Measure A
g : Gᵈᵐᵃ
s : Set A
⊢ (g • μ) s = μ (DomMulAct.mk.symm g • s)

Tactic:
by
  refine ((MeasurableEquiv.smul ((DomMulAct.mk.symm g : G)⁻¹)).map_apply _).trans ?_
  congr 1
  exact Set.preimage_smul_inv (DomMulAct.mk.symm g) s

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hst : IsComplement S T
⊢ S.Nonempty

Tactic:
contrapose! hst

Goal state after:
G : Type u_1
inst✝ : Group G
S T : Set G
hst : S = ∅
⊢ ¬IsComplement S T
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hst : IsComplement S T
⊢ T.Nonempty

Tactic:
contrapose! hst

Goal state after:
G : Type u_1
inst✝ : Group G
S T : Set G
hst : T = ∅
⊢ ¬IsComplement S T
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), ↑(f q) = q
⊢ Injective ((range f).domRestrict QuotientGroup.mk)

Tactic:
rintro ⟨-, q₁, rfl⟩ ⟨-, q₂, rfl⟩ h

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), ↑(f q) = q
q₁ q₂ : G ⧸ H
h : (range f).domRestrict QuotientGroup.mk ⟨f q₁, ⋯⟩ = (range f).domRestrict QuotientGroup.mk ⟨f q₂, ⋯⟩
⊢ ⟨f q₁, ⋯⟩ = ⟨f q₂, ⋯⟩
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
f : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
⊢ Injective ((range f).domRestrict Quotient.mk'')

Tactic:
rintro ⟨-, q₁, rfl⟩ ⟨-, q₂, rfl⟩ h

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
q₁ q₂ : Quotient (QuotientGroup.rightRel H)
h : (range f).domRestrict Quotient.mk'' ⟨f q₁, ⋯⟩ = (range f).domRestrict Quotient.mk'' ⟨f q₂, ⋯⟩
⊢ ⟨f q₁, ⋯⟩ = ⟨f q₂, ⋯⟩
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p : Set α → Prop
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet
hs : univ ⊆ ⋃ n, s n
hmono : Monotone s
F : Set α
hF : MeasurableSet F
r : ℝ≥0∞
hr : r < μ F
hBU : ⋃ n, F ∩ s n = F
this : μ F = ⨆ n, μ (F ∩ s n)
⊢ ∃ K ⊆ F, p K ∧ r < μ K

Tactic:
rw [this] at hr

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
p : Set α → Prop
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet
hs : univ ⊆ ⋃ n, s n
hmono : Monotone s
F : Set α
hF : MeasurableSet F
r : ℝ≥0∞
hr : r < ⨆ n, μ (F ∩ s n)
hBU : ⋃ n, F ∩ s n = F
this : μ F = ⨆ n, μ (F ∩ s n)
⊢ ∃ K ⊆ F, p K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p : Set α → Prop
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet
hs : univ ⊆ ⋃ n, s n
hmono : Monotone s
F : Set α
hF : MeasurableSet F
r : ℝ≥0∞
hr : r < ⨆ n, μ (F ∩ s n)
hBU : ⋃ n, F ∩ s n = F
this : μ F = ⨆ n, μ (F ∩ s n)
n : ℕ
hn : r < (μ.restrict (s n)) F
K : Set α
KF : K ⊆ F
hKp : p K
hK : r < (μ.restrict (s n)) K
⊢ ∃ K ⊆ F, p K ∧ r < μ K

Tactic:
exact ⟨K, KF, hKp, hK.trans_le (restrict_apply_le _ _)⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s
B : ℕ → Set α := spanningSets μ
hBU : ⋃ n, s ∩ B n = s
this : μ s = ⨆ n, μ (s ∩ B n)
⊢ ∃ K ⊆ s, (fun s ↦ MeasurableSet s ∧ μ s ≠ ∞) K ∧ r < μ K

Tactic:
rw [this] at hr

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
B : ℕ → Set α := spanningSets μ
hr : r < ⨆ n, μ (s ∩ B n)
hBU : ⋃ n, s ∩ B n = s
this : μ s = ⨆ n, μ (s ∩ B n)
⊢ ∃ K ⊆ s, (fun s ↦ MeasurableSet s ∧ μ s ≠ ∞) K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ν : Measure β
⊢ Measure.prod 0 ν = 0

Tactic:
rw [Measure.prod]
  exact bind_zero_left _

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
tβ : TopologicalSpace β
inst✝⁵ : T2Space β
s : Set γ
f : γ → β
inst✝⁴ : BorelSpace β
inst✝³ : TopologicalSpace γ
inst✝² : PolishSpace γ
inst✝¹ : MeasurableSpace γ
inst✝ : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
u : Set ↑s
hu : MeasurableSet u
⊢ MeasurableSet (s.domRestrict f '' u)

Tactic:
have A : MeasurableSet (((↑) : s → γ) '' u) :=
        (MeasurableEmbedding.subtype_coe hs).measurableSet_image.2 hu

Goal state after:
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
tβ : TopologicalSpace β
inst✝⁵ : T2Space β
s : Set γ
f : γ → β
inst✝⁴ : BorelSpace β
inst✝³ : TopologicalSpace γ
inst✝² : PolishSpace γ
inst✝¹ : MeasurableSpace γ
inst✝ : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
u : Set ↑s
hu : MeasurableSet u
A : MeasurableSet (Subtype.val '' u)
⊢ MeasurableSet (s.domRestrict f '' u)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case map_eq.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable fun p ↦ (f p.1, g p.1 p.2)
h✝ : NeZero μa
sf : SFinite μd
s : Set (β × δ)
hs : MeasurableSet s
⊢ (map (fun p ↦ (f p.1, g p.1 p.2)) (μa.prod μc)) s = (μb.prod μd) s

Tactic:
rw [map_apply this hs, Measure.prod_apply (this hs), Measure.prod_apply hs,
    ← hf.lintegral_comp (measurable_measure_prodMk_left hs)]

Goal state after:
case map_eq.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable fun p ↦ (f p.1, g p.1 p.2)
h✝ : NeZero μa
sf : SFinite μd
s : Set (β × δ)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), μc (Prod.mk x ⁻¹' (fun p ↦ (f p.1, g p.1 p.2)) ⁻¹' s) ∂μa = ∫⁻ (a : α), μd (Prod.mk (f a) ⁻¹' s) ∂μa
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed[inst✝²] F
r : ℝ≥0∞
hr : r < μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : ⋃ n, F ∩ B n = F
this : μ F = ⨆ n, μ (F ∩ B n)
⊢ ∃ K ⊆ F, IsCompact K ∧ r < μ K

Tactic:
rw [this] at hr

Goal state after:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed[inst✝²] F
r : ℝ≥0∞
B : ℕ → Set X := compactCovering X
hr : r < ⨆ n, μ (F ∩ B n)
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : ⋃ n, F ∩ B n = F
this : μ F = ⨆ n, μ (F ∩ B n)
⊢ ∃ K ⊆ F, IsCompact K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s + ν s
h : μ s ≠ 0
h' : ν s = 0
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν) K

Tactic:
simp only [h', add_zero] at hr
    rcases MeasurableSet.exists_lt_isCompact hs hr with ⟨K, Ks, hK, h'K⟩
    exact ⟨K, Ks, hK, h'K.trans_le (by simp)⟩

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

Goal state before:
pp: case bd
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁴] K
hμK : μ (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst✝⁴] U
hμU : μ U < μ K + ε / 2
⊢ μ (s \ U) < ε / 2

Tactic:
· exact lt_of_le_of_lt (by gcongr) hμK

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : ¬c = 0
h'c : c = ∞
s : Set α
hs : MeasurableSet s ∧ (c • μ) s ≠ ∞
r : ℝ≥0∞
hr : r < (c • μ) s
h's : μ s = 0
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (c • μ) K

Tactic:
simp [h's] at hr

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

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
hν : ν' = 0
⊢ ν' s = 0

Tactic:
rw [hν, Measure.coe_zero, Pi.zero_apply]

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : AddLeftMono β
f g : α → β
hg : HasFiniteIntegral g μ
hnonneg : ∀ᵐ (a : α) ∂μ, 0 ≤ f a
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
a : α
hn : 0 ≤ f a
ha : f a ≤ g a
⊢ |f a| ≤ |g a|

Tactic:
rwa [abs_of_nonneg hn, abs_of_nonneg (hn.trans ha)]

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

Goal state before:
pp: case add
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g h : α → ℝ≥0∞
a✝ : Disjoint (Function.support g) (Function.support h)
⊢ Measurable g →
    Measurable h →
      ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ →
        ∫⁻ (a : α), h a ∂μ.withDensity f = ∫⁻ (a : α), (f * h) a ∂μ →
          ∫⁻ (a : α), (g + h) a ∂μ.withDensity f = ∫⁻ (a : α), (f * (g + h)) a ∂μ

Tactic:
h_mea_g

Goal state after:
case add
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g h : α → ℝ≥0∞
a✝ : Disjoint (Function.support g) (Function.support h)
h_mea_g : Measurable g
⊢ Measurable h →
    ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ →
      ∫⁻ (a : α), h a ∂μ.withDensity f = ∫⁻ (a : α), (f * h) a ∂μ →
        ∫⁻ (a : α), (g + h) a ∂μ.withDensity f = ∫⁻ (a : α), (f * (g + h)) a ∂μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case iSup
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g : ℕ → α → ℝ≥0∞
⊢ (∀ (n : ℕ), Measurable (g n)) →
    Monotone g →
      (∀ (n : ℕ), ∫⁻ (a : α), g n a ∂μ.withDensity f = ∫⁻ (a : α), (f * g n) a ∂μ) →
        ∫⁻ (a : α), (fun x ↦ ⨆ n, g n x) a ∂μ.withDensity f = ∫⁻ (a : α), (f * fun x ↦ ⨆ n, g n x) a ∂μ

Tactic:
h_mea_g

Goal state after:
case iSup
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g : ℕ → α → ℝ≥0∞
h_mea_g : ∀ (n : ℕ), Measurable (g n)
⊢ Monotone g →
    (∀ (n : ℕ), ∫⁻ (a : α), g n a ∂μ.withDensity f = ∫⁻ (a : α), (f * g n) a ∂μ) →
      ∫⁻ (a : α), (fun x ↦ ⨆ n, g n x) a ∂μ.withDensity f = ∫⁻ (a : α), (f * fun x ↦ ⨆ n, g n x) a ∂μ
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ √x = y ↔ x = y ^ 2

Tactic:
by
  rw [sq, sqrt_eq_iff_mul_self_eq hx hy]

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
⊢ 0 ≤ᵐ[μ] bound

Tactic:
exact (h_bound 0).mono fun a h => le_trans (norm_nonneg _) h

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
⊢ x ≤ √x ↔ x ≤ 1

Tactic:
obtain hx | hx := le_or_gt x 0

Goal state after:
case inl
x : ℝ
hx : x ≤ 0
⊢ x ≤ √x ↔ x ≤ 1

case inr
x : ℝ
hx : 0 < x
⊢ x ≤ √x ↔ x ≤ 1
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
hg : AEMeasurable g (μ.withDensity f)
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ

Tactic:
by
  let f' := hf.mk f
  have : μ.withDensity f = μ.withDensity f' := withDensity_congr_ae hf.ae_eq_mk
  rw [this] at hg ⊢
  let g' := hg.mk g
  calc
    ∫⁻ a, g a ∂μ.withDensity f' = ∫⁻ a, g' a ∂μ.withDensity f' := lintegral_congr_ae hg.ae_eq_mk
    _ = ∫⁻ a, (f' * g') a ∂μ :=
      (lintegral_withDensity_eq_lintegral_mul _ hf.measurable_mk hg.measurable_mk)
    _ = ∫⁻ a, (f' * g) a ∂μ := by
      apply lintegral_congr_ae
      apply ae_of_ae_restrict_of_ae_restrict_compl { x | f' x ≠ 0 }
      · have Z := hg.ae_eq_mk
        rw [EventuallyEq, ae_withDensity_iff_ae_restrict hf.measurable_mk] at Z
        filter_upwards [Z]
        intro x hx
        simp only [g', hx, Pi.mul_apply]
      · have M : MeasurableSet { x : α | f' x ≠ 0 }ᶜ :=
          (hf.measurable_mk (measurableSet_singleton 0).compl).compl
        filter_upwards [ae_restrict_mem M]
        intro x hx
        simp only [Classical.not_not, mem_ofPred_eq, mem_compl_iff] at hx
        simp only [hx, zero_mul, Pi.mul_apply]
    _ = ∫⁻ a : α, (f * g) a ∂μ := by
      apply lintegral_congr_ae
      filter_upwards [hf.ae_eq_mk]
      intro x hx
      simp only [f', hx, Pi.mul_apply]

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

Goal state before:
pp: ⊢ ‖I‖ = 1

Tactic:
by simp [norm]

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

Goal state before:
pp: z : ℂ
⊢ dist z.im (-z.im) = 2 * |z.im|

Tactic:
Real.dist_eq,

Goal state after:
z : ℂ
⊢ |z.im - -z.im| = 2 * |z.im|
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: z w : ℂ
⊢ normSq (z - w) = normSq z + normSq w - 2 * (z * (starRingEnd ℂ) w).re

Tactic:
sub_eq_add_neg,

Goal state after:
z w : ℂ
⊢ normSq (z + -w) = normSq z + normSq w - 2 * (z * (starRingEnd ℂ) w).re
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C C' : ℝ
h : f.SurjectiveOnWith K C
H : C ≤ C'
⊢ f.SurjectiveOnWith K C'

Tactic:
intro k k_in
  rcases h k k_in with ⟨g, rfl, hg⟩
  use g, rfl
  by_cases Hg : ‖f g‖ = 0
  · simpa [Hg] using hg
  · exact hg.trans (by gcongr)

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
⊢ ∀ (r s : ↥(unitary R)), star (r * s) = star s * star r

Tactic:
by
    intro x y
    ext
    rw [coe_star, Submonoid.coe_mul, Submonoid.coe_mul, coe_star, coe_star, star_mul]

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

Goal state before:
pp: E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
U : ↥(unitary E)
A : E
⊢ ‖↑U * A‖ = ‖A‖

Tactic:
rw [← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)]

Goal state after:
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
U : ↥(unitary E)
A : E
⊢ ‖↑U * A‖ ^ 2 = ‖A‖ ^ 2
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.lift (fun b ↦ ∑' (a : α), g (Quotient.mk' (a • b)) • f (a • b)) ⋯ ⟦b⟧ =
    g ⟦b⟧ • Quotient.lift (fun b ↦ ∑' (a : α), f (a • b)) ⋯ ⟦b⟧

Tactic:
set π : β → Quotient (MulAction.orbitRel α β) := Quotient.mk (MulAction.orbitRel α β)

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 α β)
⊢ Quotient.lift (fun b ↦ ∑' (a : α), g (Quotient.mk' (a • b)) • f (a • b)) ⋯ (π b) =
    g (π b) • Quotient.lift (fun b ↦ ∑' (a : α), f (a • b)) ⋯ (π b)
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r : ℂ
⊢ 0 • r = 0

Tactic:
by ext <;> simp [smul_re, smul_im, zero_smul]

Goal state after: