mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case h₁
α : Type u_1
ι : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Countable ι
inst✝ : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst✝²] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
this : PolishSpace ↑t
F : ↑t → α := fun x ↦ f i₀ (↑x i₀)
F_cont : Continuous[instTopologicalSpaceSubtype, inst✝²] F
x : ↑t
n : ι
⊢ F x ∈ s n

Tactic:
have : f n ((x : γ) n) = F x := (mem_iInter.1 x.2 n :)

Goal state after:
case h₁
α : Type u_1
ι : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Countable ι
inst✝ : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst✝²] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
this✝ : PolishSpace ↑t
F : ↑t → α := fun x ↦ f i₀ (↑x i₀)
F_cont : Continuous[instTopologicalSpaceSubtype, inst✝²] F
x : ↑t
n : ι
this : f n (↑x n) = F x
⊢ F x ∈ s n
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < μ s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
⊢ 1 - (1 - p) < μ s

Tactic:
convert! hμs

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < μ s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
⊢ 1 - (1 - p) = p
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
⊢ (dirac a) s = s.indicator 1 a

Tactic:
by_cases h : a ∈ s

Goal state after:
case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∈ s
⊢ (dirac a) s = s.indicator 1 a

case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
⊢ (dirac a) s = s.indicator 1 a
Module: Mathlib.MeasureTheory.Measure.Count

Goal state before:

Tactic:
(#t : ℝ≥0∞) = ∑ i ∈ t, 1 := by simp
    _ = ∑' i : (t : Set α), 1 := (t.tsum_subtype 1).symm
    _ ≤ count (t : Set α) := le_count_apply
    _ ≤ count s := measure_mono ht

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
⊢ count ∅ = 0

Tactic:
exact measure_empty

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
⊢ count univ = ↑(ENat.card α)

Tactic:
by simp [count_apply .univ, encard_univ]

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

Goal state before:
pp: case ht
α : 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
⊢ ↑c ≠ ∞ ∨ L ≠ ∞

Tactic:
· simp only [Ne, coe_ne_top, not_false_iff, true_or]

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

Goal state before:
pp: case const.refine_3.ht
α : 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 < ∞
⊢ ↑c ≠ ∞ ∨ L ≠ ∞

Tactic:
· simp only [Ne, coe_ne_top, not_false_iff, true_or]

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

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
s : Set X
μ : Measure X
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : T2Space X
h₂s : μ s = 0
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ n, K n = s
h : ∀ (n : ℕ), IsNowhereDense (K n)
⊢ ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S

Tactic:
exact ⟨range K, fun t ⟨n, hn⟩ ↦ hn ▸ h n, countable_range K, hcover.symm.subset⟩

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

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {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 f hf h2f h3f
    have : ∀ x, Monotone fun n y => f n (x, y) := fun x i j hij y => h2f hij (x, y)
    conv => enter [1, x]; erw [lintegral_iSup (fun n => (hf n).comp m) (this x)]
    exact .iSup h3f

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : ρ.IsMulLeftInvariant
inst✝ : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : ρ s = 0
x : M
| ∫⁻ (y : M), (HMul.hMul x ⁻¹' s).indicator 1 y ∂ν

Tactic:
lintegral_indicator_one (by apply MeasurableSet.preimage hs (by fun_prop))

Goal state after:
M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : ρ.IsMulLeftInvariant
inst✝ : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : ρ s = 0
x : M
| ν (HMul.hMul x ⁻¹' s)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: X : Type u_3
Z : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : StandardBorelSpace X
inst✝¹ : MeasurableSpace Z
inst✝ : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
⊢ MeasurableSet s

Tactic:
rcases exists_opensMeasurableSpace_of_countablySeparated Z with ⟨τ, _, _, _⟩

Goal state after:
X : Type u_3
Z : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : StandardBorelSpace X
inst✝¹ : MeasurableSpace Z
inst✝ : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left✝¹ : SecondCountableTopology Z
left✝ : T4Space Z
right✝ : OpensMeasurableSpace Z
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case hs
X : Type u_3
Z : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : StandardBorelSpace X
inst✝¹ : MeasurableSpace Z
inst✝ : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left✝¹ : SecondCountableTopology Z
left✝ : T4Space Z
right✝ : OpensMeasurableSpace Z
⊢ AnalyticSet s

Tactic:
rw [← image_preimage_eq s hsurj]
    exact h.analyticSet_image hf

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

Goal state before:
pp: X : Type u_3
Z : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : StandardBorelSpace X
inst✝¹ : MeasurableSpace Z
f : X → Z
inst✝ : CountablySeparated ↑(range f)
hf : Measurable f
hr : MeasurableSet (range f)
s : Set Z
⊢ MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ range f)

Tactic:
hf.measurableSet_preimage_iff_preimage_val,

Goal state after:
X : Type u_3
Z : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : StandardBorelSpace X
inst✝¹ : MeasurableSpace Z
f : X → Z
inst✝ : CountablySeparated ↑(range f)
hf : Measurable f
hr : MeasurableSet (range f)
s : Set Z
⊢ MeasurableSet (Subtype.val ⁻¹' s) ↔ MeasurableSet (s ∩ range f)
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
mβ : MeasurableSpace β
inst✝¹ : TopologicalSpace β
μ : Measure β
inst✝ : μ.OuterRegular
f : α → β
f_cont : Continuous[inst✝², inst✝¹] f
f_me : MeasurableEmbedding f
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > μ (f '' A)
U : Set β
hUA : U ⊇ f '' A
Uopen : IsOpen[inst✝¹] U
hμU : μ U < r
⊢ A ⊆ f ⁻¹' U

Tactic:
← image_subset_iff

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
mβ : MeasurableSpace β
inst✝¹ : TopologicalSpace β
μ : Measure β
inst✝ : μ.OuterRegular
f : α → β
f_cont : Continuous[inst✝², inst✝¹] f
f_me : MeasurableEmbedding f
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > μ (f '' A)
U : Set β
hUA : U ⊇ f '' A
Uopen : IsOpen[inst✝¹] U
hμU : μ U < r
⊢ f '' A ⊆ U
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:

Tactic:
μ (⋃ n, U n) ≤ ∑' n, μ (U n) := measure_iUnion_le _
    _ ≤ ∑' n, (μ (A n) + δ n) := ENNReal.tsum_le_tsum fun n => (hU n).le
    _ = ∑' n, μ (A n) + ∑' n, δ n := ENNReal.tsum_add
    _ = μ (⋃ n, A n) + ∑' n, δ n := (congr_arg₂ (· + ·) (measure_iUnion hAd hAm).symm rfl)
    _ < r := hδε

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
| μ.inv

Tactic:
← map_mul_left_eq_self μ g⁻¹

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 ↦ g⁻¹ * x) μ).inv
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
hsm : MeasurableSet s
hμs : μ s = 0
hf : Measurable fun z ↦ (z.2 * z.1, z.1⁻¹)
hsm' : MeasurableSet (s⁻¹ ×ˢ s⁻¹)
⊢ (map (fun z ↦ (z.2 * z.1, z.1⁻¹)) (μ.prod μ)) (s⁻¹ ×ˢ s⁻¹) = 0

Tactic:
simp_rw [map_apply hf hsm', prod_apply_symm (μ := μ) (ν := μ) (hf hsm'), preimage_preimage,
    mk_preimage_prod, inv_preimage, inv_inv, measure_mono_null inter_subset_right hμs,
    lintegral_zero]

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
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
h : Measurable fun z ↦ (z.2 * z.1, z.1⁻¹)
h2f : AEMeasurable (uncurry fun x y ↦ f (y * x) x⁻¹) (μ.prod ν)
| ∫⁻ (z : G × G), f z.1 z.2 ∂μ.prod ν

Tactic:
rw [← (measurePreserving_mul_prod_inv μ ν).map_eq]

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
h : Measurable fun z ↦ (z.2 * z.1, z.1⁻¹)
h2f : AEMeasurable (uncurry fun x y ↦ f (y * x) x⁻¹) (μ.prod ν)
| ∫⁻ (z : G × G), f z.1 z.2 ∂map (fun z ↦ (z.2 * z.1, z.1⁻¹)) (μ.prod ν)
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, r < (∑ i ∈ a, μ i) s

Tactic:
simp only [coe_finsetSum, Finset.sum_apply]

Goal state after:
α : 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, r < ∑ c ∈ a, (μ c) s
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
⊢ (∑ i ∈ a, μ i) K ≤ (sum μ) K

Tactic:
simp only [coe_finsetSum, Finset.sum_apply]

Goal state after:
α : 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
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case a
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
K : Set α
hK : IsCompact K
⊢ μ K ≤ ⨅ U, ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen[inst✝⁴] U), μ U

Tactic:
simp only [le_iInf_iff]
    exact fun U KU _ ↦ measure_mono KU

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
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
hν : ν ≠ 0
⊢ μ ≪ ν

Tactic:
by
  refine AbsolutelyContinuous.mk fun s sm hνs => ?_
  have h1 := measure_mul_lintegral_eq μ ν sm 1 measurable_one
  simp_rw [Pi.one_apply, lintegral_one, mul_one, (measure_mul_right_null ν _).mpr hνs,
    lintegral_zero, mul_eq_zero (M₀ := ℝ≥0∞), measure_univ_eq_zero.not.mpr hν, or_false] at h1
  exact h1

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✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
μ : Measure G
inst✝⁶ : μ.IsHaarMeasure
α : Type u_3
inst✝⁵ : BorelSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : Group α
inst✝² : MulAction α G
inst✝¹ : SMulCommClass α G G
inst✝ : ContinuousConstSMul α G
a : α
K : Set G
hK : IsCompact K
F : G ≃ᵐ G := (Homeomorph.smul a).toMeasurableEquiv
⊢ (map (⇑F) μ) K < ∞

Tactic:
F.map_apply K

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
μ : Measure G
inst✝⁶ : μ.IsHaarMeasure
α : Type u_3
inst✝⁵ : BorelSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : Group α
inst✝² : MulAction α G
inst✝¹ : SMulCommClass α G G
inst✝ : ContinuousConstSMul α G
a : α
K : Set G
hK : IsCompact K
F : G ≃ᵐ G := (Homeomorph.smul a).toMeasurableEquiv
⊢ μ (⇑F ⁻¹' K) < ∞
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f' x ≠ 0}
⊢ (fun x ↦ ↑(f x) * g x) =ᵐ[μ] fun x ↦ ↑(f' x) * g' x

Tactic:
apply ae_of_ae_restrict_of_ae_restrict_compl { x | f' x ≠ 0 }

Goal state after:
case mp.ht
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f' x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}, (fun x ↦ ↑(f x) * g x) x = (fun x ↦ ↑(f' x) * g' x) x

case mp.htc
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f' x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}ᶜ, (fun x ↦ ↑(f x) * g x) x = (fun x ↦ ↑(f' x) * g' x) x
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := ⋯
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := ⋯
⊢ f' * g' =ᵐ[μ] f' * g

Tactic:
apply ae_of_ae_restrict_of_ae_restrict_compl { x | f' x ≠ 0 }

Goal state after:
case ht
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := ⋯
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := ⋯
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}, (f' * g') x = (f' * g) x

case htc
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := ⋯
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := ⋯
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}ᶜ, (f' * g') x = (f' * g) x
Module: Mathlib.Analysis.Complex.Norm

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

Tactic:
simp [norm]

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

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

Tactic:
by
  rw [dist_of_re_eq (conj_re z), conj_im, dist_comm, Real.dist_eq, sub_neg_eq_add, ← two_mul,
    _root_.abs_mul, abs_of_pos (zero_lt_two' ℝ)]

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

Goal state before:
pp: z : ℂ
⊢ dist ((starRingEnd ℂ) z) z = 2 * ↑(Real.nnabs z.im)

Tactic:
Real.coe_nnabs,

Goal state after:
z : ℂ
⊢ dist ((starRingEnd ℂ) z) z = 2 * |z.im|
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f g : ι → α
hs : s.Nonempty
h : 𝔼 i ∈ s, g i ≤ 𝔼 i ∈ s, f i
⊢ ∃ x ∈ s, g x ≤ f x

Tactic:
obtain ⟨_, hx⟩ := hs

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f g : ι → α
h : 𝔼 i ∈ s, g i ≤ 𝔼 i ∈ s, f i
w✝ : ι
hx : w✝ ∈ s
⊢ ∃ x ∈ s, g x ≤ f x
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₁ V₂
g : NormedAddGroupHom V₂ V₃
h : g.comp f = 0
v w : V₁
⊢ ⟨f (v + w), ⋯⟩ = ⟨f v, ⋯⟩ + ⟨f w, ⋯⟩

Tactic:
by simp only [map_add, AddMemClass.mk_add_mk]

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

Goal state before:
pp: ⊢ (LinearMap.toMatrix basisOneI basisOneI) ↑↑conjAe = !![1, 0; 0, -1]

Tactic:
ext i j
  fin_cases i <;> fin_cases j <;> simp [LinearMap.toMatrix_apply]

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

Goal state before:
pp: case inr
K : Type u_1
inst✝ : RCLike K
z : K
h₀ : z ≠ 0
⊢ z⁻¹ = (starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹

Tactic:
apply inv_eq_of_mul_eq_one_right

Goal state after:
case inr
K : Type u_1
inst✝ : RCLike K
z : K
h₀ : z ≠ 0
⊢ z * ((starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹) = 1
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case hre
K : Type u_1
E : Type u_2
inst✝ : RCLike K
z : K
r : ℝ
a : K
⊢ re (star (r • a)) = re (star r • star a)

Tactic:
simp [RCLike.smul_re, RCLike.smul_im]

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

Goal state before:
pp: case him
K : Type u_1
E : Type u_2
inst✝ : RCLike K
z : K
r : ℝ
a : K
⊢ im (star (r • a)) = im (star r • star a)

Tactic:
simp [RCLike.smul_re, RCLike.smul_im]

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

Goal state before:
pp: case refine_1
A : Type u_1
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Module ℂ A
inst✝ : StarModule ℂ A
a : A
h : 0 ≤ a
⊢ 0 ≤ ℜ a

pp: case refine_2
A : Type u_1
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Module ℂ A
inst✝ : StarModule ℂ A
a : A
h : 0 ≤ ℜ a ∧ ℑ a = 0
⊢ 0 ≤ a

Tactic:
· simpa +singlePass [← h.isSelfAdjoint.coe_realPart] using! h

Goal state after:
case refine_2
A : Type u_1
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Module ℂ A
inst✝ : StarModule ℂ A
a : A
h : 0 ≤ ℜ a ∧ ℑ a = 0
⊢ 0 ≤ a
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝³ : RCLike K
inst✝² : NormedField E
inst✝¹ : CharZero E
inst✝ : NormedSpace K E
q : ℚ≥0
x : E
⊢ ‖q • x‖₊ = q • ‖x‖₊

Tactic:
simpa [NNRat.cast_smul_eq_nnqsmul] using! nnnorm_smul (q : K) x

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 ≤ z ↔ ∃ x ≥ 0, ↑x = z

Tactic:
simp_rw [nonneg_iff (K := K), ext_iff (K := K)]

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 ≤ re z ∧ im z = 0 ↔ ∃ x ≥ 0, re ↑x = re z ∧ im ↑x = im z
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
a' : ℝ
ha1 : a' > 0
ha2 : ↑a' = ↑a
h : a' < 0 ∧ c - b < 0 ∨ 0 < a' ∧ 0 < c - b
⊢ 0 ≤ c - b

Tactic:
exact le_of_lt <| h.rec (False.elim <| not_lt_of_gt ·.1 ha1) (·.2)

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i : ℕ
⊢ abv (∑ i ∈ range (0 + max n i), f i - ∑ i ∈ range (max n i), f i) ≤
    ∑ k ∈ range (0 + max n i), a k - ∑ k ∈ range (max n i), a k

Tactic:
simp [abv_zero abv]

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

Goal state before:
pp: x : ℝ
hx : |x| ≤ 1
⊢ |rexp x - 1 - x| ≤ x ^ 2

Tactic:
rw [← sq_abs]
  have : ‖(x : ℂ)‖ ≤ 1 := mod_cast hx
  exact_mod_cast Complex.norm_exp_sub_one_sub_id_le this

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

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖(cexp (-(↑x / 2) * I) - cexp (↑x / 2 * I)) * I‖

Tactic:
← one_mul (_ - _),

Goal state after:
x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖1 * (cexp (-(↑x / 2) * I) - cexp (↑x / 2 * I)) * I‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖2 * Real.sin (x / 2)‖

Tactic:
rw [show ‖2 * Real.sin (x / 2)‖ = ‖2 * sin (x / 2)‖ by norm_cast, two_sin]
  nth_rw 2 [← one_mul (_ - _), ← exp_zero]
  rw [← neg_add_cancel (x / 2 * I), exp_add, mul_assoc _ _ (_ - _), mul_sub, ← exp_add, ← exp_add,
    ← add_mul, ← add_mul]; norm_cast
  rw [add_neg_cancel, ofReal_zero, zero_mul, exp_zero, add_halves, ← neg_mul, Complex.norm_mul,
    norm_I, mul_one, Complex.norm_mul,
    show -(ofReal (x / 2)) = ofReal (-x / 2) by norm_cast; exact neg_div' 2 x,
    norm_exp_ofReal_mul_I, one_mul, ← norm_neg, neg_sub, mul_comm]

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

Goal state before:
pp: n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : |1 + x / ↑(n + 1) * a₂ - a₁| ≤ b₁ - |x| / ↑(n + 1) * b₂
h : |rexp x - expNear (n + 1) x a₂| ≤ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂
⊢ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂ + |x ^ n / ↑n.factorial| * |1 + x / (↑n + 1) * a₂ - a₁| =
    |x| ^ n / ↑n.factorial * (|x| / ↑(n + 1) * b₂ + |1 + x / ↑(n + 1) * a₂ - a₁|)

Tactic:
simp [mul_add, pow_succ', div_eq_mul_inv, abs_mul, abs_inv, Nat.factorial]
    ac_rfl

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

Goal state before:
pp: n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ rexp (-(t / ↑n)) ^ n = rexp (-t)

Tactic:
rw [← Real.exp_nat_mul, mul_neg, mul_comm, div_mul_cancel₀]

Goal state after:
case h
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ ↑n ≠ 0