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

Goal state before:
pp: case e'_3
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst✝³] f
hg : Continuous[_, inst✝³] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
I :
  ∀ (n : ℕ) (x y : ℕ → ℕ),
    ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) →
      ∃ x' y',
        x' ∈ cylinder x n ∧
          y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
A : Type := { p // ¬MeasurablySeparable (f '' cylinder p.2.1 p.1) (g '' cylinder p.2.2 p.1) }
F : A → A
hFn : ∀ (p : A), (↑(F p)).1 = (↑p).1 + 1
hFx : ∀ (p : A), (↑(F p)).2.1 ∈ cylinder (↑p).2.1 (↑p).1
hFy : ∀ (p : A), (↑(F p)).2.2 ∈ cylinder (↑p).2.2 (↑p).1
p0 : A := ⟨(0, fun x ↦ 0, fun x ↦ 0), ⋯⟩
p : ℕ → A := fun n ↦ F^[n] p0
prec : ∀ (n : ℕ), p (n + 1) = F (p n)
pn_fst : ∀ (n : ℕ), (↑(p n)).1 = n
Ix : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m
Iy : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.2 m = (↑(p (m + 1))).2.2 m
x : ℕ → ℕ := fun n ↦ (↑(p (n + 1))).2.1 n
hx : x = fun n ↦ (↑(p (n + 1))).2.1 n
y : ℕ → ℕ := fun n ↦ (↑(p (n + 1))).2.2 n
hy : y = fun n ↦ (↑(p (n + 1))).2.2 n
n : ℕ
⊢ cylinder x n = cylinder (↑(p n)).2.1 (↑(p n)).1

Tactic:
rw [pn_fst, ← mem_cylinder_iff_eq, mem_cylinder_iff]
      intro i hi
      rw [hx]
      exact (Ix i n hi).symm

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

Goal state before:
pp: case h₁.refine_2
γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝ : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable ↑b
A : Type (max 0 u_3) := { p // Disjoint ↑p.1 ↑p.2 }
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := fun s ↦ closure[inst✝³] (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := fun n ↦ ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s
y : γ
n : ℕ
s : Set γ
sb : s ∈ b
ys : y ∈ s
hs : s ⊆ ball y (u n / 2)
diam_s : diam s ≤ u n
t : ↑b
ht : Disjoint ↑⟨s, sb⟩ ↑t
⊢ f y ∉ q ⟨(t, ⟨s, sb⟩), ⋯⟩

Tactic:
apply disjoint_left.1 (hq2 ⟨(t, ⟨s, sb⟩), ht.symm⟩)
      exact mem_image_of_mem _ ys

Goal state after:
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
⊢ ⋃ n, F ∩ s n = F

Tactic:
rw [← inter_iUnion, univ_subset_iff.mp hs, inter_univ]

Goal state after:
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 μ
inst✝ : NeZero ν
s : Set α
h : NullMeasurableSet (Prod.fst ⁻¹' s) (μ.prod ν)
⊢ NullMeasurableSet (s ×ˢ univ) (μ.prod ν)

Tactic:
prod_univ

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : SFinite ν
inst✝¹ : SFinite μ
inst✝ : NeZero ν
s : Set α
h : NullMeasurableSet (Prod.fst ⁻¹' s) (μ.prod ν)
⊢ NullMeasurableSet (Prod.fst ⁻¹' s) (μ.prod ν)
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : MeasurableConstSMul G α
tfae_1_iff_2 : SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun x ↦ c • x) ⁻¹' s) = μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), Measure.map (fun x ↦ c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), Measure.map (fun x ↦ c • x) μ = μ) → ∀ (c : G), MeasurePreserving (fun x ↦ c • x) μ μ
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving (fun x ↦ c • x) μ μ) → ∀ (c : G) (s : Set α), μ ((fun x ↦ c • x) ⁻¹' s) = μ s
tfae_4_to_5 : (∀ (c : G) (s : Set α), μ ((fun x ↦ c • x) ⁻¹' s) = μ s) → ∀ (c : G) (s : Set α), μ (c • s) = μ s
tfae_5_to_3 : (∀ (c : G) (s : Set α), μ (c • s) = μ s) → ∀ (c : G) (s : Set α), MeasurableSet s → μ (c • s) = μ s
H : ∀ (c : G) (s : Set α), MeasurableSet s → μ (c • s) = μ s
c : G
s : Set α
hs : MeasurableSet s
⊢ μ ((fun x ↦ c • x) ⁻¹' s) = μ s

Tactic:
rw [preimage_smul]

Goal state after:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : MeasurableConstSMul G α
tfae_1_iff_2 : SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun x ↦ c • x) ⁻¹' s) = μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), Measure.map (fun x ↦ c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), Measure.map (fun x ↦ c • x) μ = μ) → ∀ (c : G), MeasurePreserving (fun x ↦ c • x) μ μ
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving (fun x ↦ c • x) μ μ) → ∀ (c : G) (s : Set α), μ ((fun x ↦ c • x) ⁻¹' s) = μ s
tfae_4_to_5 : (∀ (c : G) (s : Set α), μ ((fun x ↦ c • x) ⁻¹' s) = μ s) → ∀ (c : G) (s : Set α), μ (c • s) = μ s
tfae_5_to_3 : (∀ (c : G) (s : Set α), μ (c • s) = μ s) → ∀ (c : G) (s : Set α), MeasurableSet s → μ (c • s) = μ s
H : ∀ (c : G) (s : Set α), MeasurableSet s → μ (c • s) = μ s
c : G
s : Set α
hs : MeasurableSet s
⊢ μ (c⁻¹ • s) = μ s
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
x : α
i : ℕ
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (map (Prod.mk x) (sfiniteSeq ν i)) (s ×ˢ t) = (dirac x) s * (sfiniteSeq ν i) t

Tactic:
map_apply measurable_prodMk_left (hs.prod ht),

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
x : α
i : ℕ
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (sfiniteSeq ν i) (Prod.mk x ⁻¹' s ×ˢ t) = (dirac x) s * (sfiniteSeq ν i) t
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H :
  ∀ (i : ℕ) (ε : ℝ≥0∞),
    ε ≠ 0 → ∃ F ⊆ s i, ∃ U ⊇ s i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (s i) ≤ μ F + ε ∧ μ U ≤ μ (s i) + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
ε0' : ε / 2 ≠ 0
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : ∑' (i : ℕ), δ i < ε / 2
F : ℕ → Set α
hFs : ∀ (n : ℕ), F n ⊆ s n
U : ℕ → Set α
hsU : ∀ (n : ℕ), U n ⊇ s n
hFc : ∀ (n : ℕ), IsClosed[inst✝²] (F n)
hUo : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hF : ∀ (n : ℕ), μ (s n) ≤ μ (F n) + δ n
hU : ∀ (n : ℕ), μ (U n) ≤ μ (s n) + δ n
this : Tendsto (fun t ↦ ∑ k ∈ t, μ (s k) + ε / 2) atTop (𝓝 (μ (⋃ n, s n) + ε / 2))
t : Finset ℕ
ht : μ (⋃ n, s n) < ∑ k ∈ t, μ (s k) + ε / 2
⊢ ∑ k ∈ t, μ (s k) + ε / 2 ≤ ∑ k ∈ t, μ (F k) + ∑ k ∈ t, δ k + ε / 2

Tactic:
rw [← sum_add_distrib]

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H :
  ∀ (i : ℕ) (ε : ℝ≥0∞),
    ε ≠ 0 → ∃ F ⊆ s i, ∃ U ⊇ s i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (s i) ≤ μ F + ε ∧ μ U ≤ μ (s i) + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
ε0' : ε / 2 ≠ 0
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : ∑' (i : ℕ), δ i < ε / 2
F : ℕ → Set α
hFs : ∀ (n : ℕ), F n ⊆ s n
U : ℕ → Set α
hsU : ∀ (n : ℕ), U n ⊇ s n
hFc : ∀ (n : ℕ), IsClosed[inst✝²] (F n)
hUo : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hF : ∀ (n : ℕ), μ (s n) ≤ μ (F n) + δ n
hU : ∀ (n : ℕ), μ (U n) ≤ μ (s n) + δ n
this : Tendsto (fun t ↦ ∑ k ∈ t, μ (s k) + ε / 2) atTop (𝓝 (μ (⋃ n, s n) + ε / 2))
t : Finset ℕ
ht : μ (⋃ n, s n) < ∑ k ∈ t, μ (s k) + ε / 2
⊢ ∑ k ∈ t, μ (s k) + ε / 2 ≤ ∑ x ∈ t, (μ (F x) + δ x) + ε / 2
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: case e_f
G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_3
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable ⇑f
h_surj : Surjective ⇑f
g : G
⊢ (fun x ↦ f g * x) ∘ ⇑f = ⇑f ∘ fun x ↦ g * x

Tactic:
ext y

Goal state after:
case e_f
G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_3
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable ⇑f
h_surj : Surjective ⇑f
g y : G
⊢ ((fun x ↦ f g * x) ∘ ⇑f) y = (⇑f ∘ fun x ↦ g * x) y
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
μ : Measure G
inst✝ : MeasurableMul G
g : G
s : Set G
hs : MeasurableSet s
⊢ ↑((fun x ↦ x * g) ⁻¹' s).encard = ↑s.encard

Tactic:
encard_preimage_of_bijective (Group.mulRight_bijective _)

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSpace H
inst✝¹ : Group G
μ : Measure G
inst✝ : MeasurableMul G
g : G
s : Set G
hs : MeasurableSet s
⊢ ↑s.encard = ↑s.encard
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: case mp
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
x✝ : H
⊢ x✝ ∈ ⇑f '' (fun x ↦ g * x) ⁻¹' s → x✝ ∈ (fun x ↦ f g * x) ⁻¹' ⇑f '' s

pp: case mpr
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
x✝ : H
⊢ x✝ ∈ (fun x ↦ f g * x) ⁻¹' ⇑f '' s → x✝ ∈ ⇑f '' (fun x ↦ g * x) ⁻¹' s

Tactic:
· rintro ⟨y, hy, rfl⟩
        exact ⟨g * y, hy, by simp⟩

Goal state after:
case mpr
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
x✝ : H
⊢ x✝ ∈ (fun x ↦ f g * x) ⁻¹' ⇑f '' s → x✝ ∈ ⇑f '' (fun x ↦ g * x) ⁻¹' s
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 μ
s : Set G
hs : MeasurableSet s
⊢ Measurable fun x ↦ μ ((fun y ↦ y * x) ⁻¹' s)

Tactic:
by
  suffices
    Measurable fun y =>
      μ ((fun x => (x, y)) ⁻¹' ((fun z : G × G => ((1 : G), z.1 * z.2)) ⁻¹' univ ×ˢ s))
    by convert! this using 1; ext1 x; congr 1 with y : 1; simp
  apply measurable_measure_prodMk_right
  apply measurable_const.prodMk measurable_mul (MeasurableSet.univ.prod hs)
  infer_instance

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

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : BorelSpace G
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : μ.Regular
inst✝ : NeZero μ
f : G → ℝ≥0∞
hf : Continuous f
⊢ ∫⁻ (x : G), f x ∂μ = 0 ↔ f = 0

Tactic:
by
  rw [lintegral_eq_zero_iff hf.measurable, hf.ae_eq_iff_eq μ continuous_zero]

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

Goal state before:
pp: case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
hS : MeasurableSet S
⊢ (μ.withDensity fun x ↦ ENNReal.ofReal (f x)) S = 0

pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
hS : MeasurableSet S
⊢ (μ.withDensity fun x ↦ ENNReal.ofReal (-f x)) Sᶜ = 0

Tactic:
· rw [withDensity_apply _ hS, lintegral_eq_zero_iff hf.ennreal_ofReal, EventuallyEq]
    exact (ae_restrict_mem hS).mono fun x hx => ENNReal.ofReal_eq_zero.2 (le_of_lt hx)

Goal state after:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
hS : MeasurableSet S
⊢ (μ.withDensity fun x ↦ ENNReal.ofReal (-f x)) Sᶜ = 0
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
s : Set G
sm : MeasurableSet s
hνs : ν s = 0
h1 : μ s * ν univ = 0
⊢ μ s = 0

Tactic:
mul_eq_zero (M₀ := ℝ≥0∞),

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
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : ν s = 0
h1 : μ s = 0 ∨ ν univ = 0
⊢ μ s = 0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x

Tactic:
ae_iff,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (μ.withDensity f) {a | ¬p a} = 0 ↔ ∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (μ.withDensity f) {a | ¬p a} = 0 ↔ ∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x

Tactic:
ae_iff,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (μ.withDensity f) {a | ¬p a} = 0 ↔ μ {a | ¬(f a ≠ 0 → p a)} = 0
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'
⊢ AEMeasurable (fun x ↦ ↑(f x) * g x) μ

Tactic:
have A : MeasurableSet {x | f' x ≠ 0} := hf'_m (measurableSet_singleton _).compl

Goal state after:
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}
⊢ AEMeasurable (fun x ↦ ↑(f x) * g x) μ
Module: Mathlib.MeasureTheory.Function.Egorov

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

Tactic:
filter_upwards [hfg] with _ htendsto _ using htendsto

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

Goal state before:
pp: x y : ℝ
hy : 0 < y
⊢ √x < √y ↔ x < y

Tactic:
rw [Real.sqrt, Real.sqrt, NNReal.coe_lt_coe, NNReal.sqrt_lt_sqrt, toNNReal_lt_toNNReal_iff hy]

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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
this : IsAbsoluteValue fun x ↦ ‖x‖ := inferInstance
x✝ : ℕ
⊢ (↑(const (fun x ↦ ‖x‖) (limAux f)) x✝).re = (↑(const (fun x ↦ ‖x‖) (↑(cauSeqRe f).lim + ↑(cauSeqIm f).lim * I)) x✝).re

Tactic:
simp [limAux, cauSeqRe, ofReal]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
s : Set α
hs : MeasurableSet s
hμs : ∫⁻ (a : α) in s, f a ∂μ = 0
⊢ μ s = 0

Tactic:
lintegral_eq_zero_iff' hf.restrict,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
s : Set α
hs : MeasurableSet s
hμs : f =ᵐ[μ.restrict s] 0
⊢ μ s = 0
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
hz : ‖z‖ ^ 2 = 1
⊢ z.im * z.im = 1 - z.re * z.re

Tactic:
rw [Complex.sq_norm, normSq_apply] at hz

Goal state after:
z : ℂ
hz : z.re * z.re + z.im * z.im = 1
⊢ z.im * z.im = 1 - z.re * z.re
Module: Mathlib.Analysis.Complex.Order

Goal state before:
pp: z : ℂ
h : z.im = 0
⊢ 0 ≤ z.re ^ 2 - z.im ^ 2 ∧ (z.re = 0 ∨ z.im = 0)

Tactic:
by simpa [h] using sq_nonneg z.re

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

Goal state before:
pp: α : Type u_1
n : ℚ
z : ℂ
⊢ (n • z).re = (↑n * z).re ∧ (n • z).im = (↑n * z).im

Tactic:
simp [Rat.smul_def, smul_re, smul_im]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ (μ.withDensity f).prod (ν.withDensity g) = (μ.prod ν).withDensity fun z ↦ f z.1 * g z.2

Tactic:
by
  rw [prod_withDensity_left₀ hf, prod_withDensity_right₀ hg, ← withDensity_mul₀, mul_comm]
  · rfl
  all_goals fun_prop (disch := intro _ hs; simp [hs])

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

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝³ : Monoid A
inst✝² : Star A
inst✝¹ : Monoid B
inst✝ : Star B
f g : A →⋆* B
h : (fun f ↦ (↑f.toMonoidHom).toFun) f = (fun f ↦ (↑f.toMonoidHom).toFun) g
⊢ f = g

Tactic:
cases f; cases g; simp_all

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

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝⁷ : Mul A
inst✝⁶ : Mul B
inst✝⁵ : Mul C
inst✝⁴ : Mul D
inst✝³ : Star A
inst✝² : Star B
inst✝¹ : Star C
inst✝ : Star D
f g : A ≃⋆* B
h : f.toFun = g.toFun
⊢ f.invFun = g.invFun → f = g

Tactic:
cases f; cases g; simp_all

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

Goal state before:
pp: ⊢ Continuous ⇑normSq

Tactic:
by
  simpa [← Complex.normSq_eq_norm_sq] using continuous_norm (E := ℂ).fun_pow 2

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:
smul_def,

Goal state after:
case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * y₂ + y₁ * x₂) * I' = (algebraMap ℝ A) x₁ * y₂ • I' + y₁ • I' * (algebraMap ℝ A) x₂
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₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * y₂ + y₁ * x₂) * I' = (algebraMap ℝ A) x₁ * y₂ • I' + y₁ • I' * (algebraMap ℝ A) x₂

Tactic:
smul_def,

Goal state after:
case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * y₂ + y₁ * x₂) * I' =
    (algebraMap ℝ A) x₁ * ((algebraMap ℝ A) y₂ * I') + y₁ • I' * (algebraMap ℝ A) x₂
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₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * y₂ + y₁ * x₂) * I' =
    (algebraMap ℝ A) x₁ * ((algebraMap ℝ A) y₂ * I') + y₁ • I' * (algebraMap ℝ A) x₂

Tactic:
smul_def,

Goal state after:
case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * y₂ + y₁ * x₂) * I' =
    (algebraMap ℝ A) x₁ * ((algebraMap ℝ A) y₂ * I') + (algebraMap ℝ A) y₁ * I' * (algebraMap ℝ A) x₂
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✝
⊢ im z = 0

Tactic:
rw [← @ofReal_inj K, im_eq_conj_sub, h, sub_self, mul_zero, zero_div,
      ofReal_zero]

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

Goal state before:
pp: A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(ℜ (I • a)) = ↑(-ℑ a)

Tactic:
simp [realPart_apply_coe, imaginaryPart_apply_coe, smul_comm I, sub_eq_add_neg, add_comm]

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

Goal state before:
pp: z : ℂ
hz : ¬(z.re = re 0 ∧ z.im = im 0)
⊢ (0 < z.re ∨ z.im ≠ 0) ∨ 0 < (-z).re ∨ (-z).im ≠ 0

Tactic:
push Not at hz

Goal state after:
z : ℂ
hz : z.re = re 0 → z.im ≠ im 0
⊢ (0 < z.re ∨ z.im ≠ 0) ∨ 0 < (-z).re ∨ (-z).im ≠ 0
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
f : CauSeq K norm
x✝ : ℝ
ε0 : x✝ > 0
i : ℕ
H : ∀ j ≥ i, ‖↑f j - ↑f i‖ < x✝
j : ℕ
ij : j ≥ i
⊢ |(fun n ↦ re (↑f n)) j - (fun n ↦ re (↑f n)) i| ≤ ‖↑f j - ↑f i‖

Tactic:
simpa only [map_sub] using abs_re_le_norm (f j - f i)

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (r : ℝ) (x : 𝕜), ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
by subst h''; exact h.norm_smul_le

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
s : Set α
⊢ IsBigOWith c (𝓟 s) f g ↔ ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖

Tactic:
by
  rw [IsBigOWith_def, eventually_principal]

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

Goal state before:
pp: α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
l : Filter α
c : F''
hcf : c = 0 → f'' =ᶠ[l] 0
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f'' x‖
⊢ f'' =O[l] fun _x ↦ c

Tactic:
rcases eq_or_ne c 0 with (hc | hc)

Goal state after:
case inl
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
l : Filter α
c : F''
hcf : c = 0 → f'' =ᶠ[l] 0
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f'' x‖
hc : c = 0
⊢ f'' =O[l] fun _x ↦ c

case inr
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
l : Filter α
c : F''
hcf : c = 0 → f'' =ᶠ[l] 0
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f'' x‖
hc : c ≠ 0
⊢ f'' =O[l] fun _x ↦ c
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (f =O[l] fun x ↦ ‖c‖ * ‖f' x‖) ↔ f =O[l] f'

Tactic:
rw [isBigO_const_mul_right_iff cne0, isBigO_norm_right]

Goal state after: