mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
| ∫⁻ (a : α), f a ∂μ

Tactic:
rw [← sum_smul_dirac μ, lintegral_sum_measure]

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
| ∑' (i : α), ∫⁻ (a : α), f a ∂μ {i} • dirac i
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: case const
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ
⊢ ∃ g,
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0)) x) ∧
      ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Tactic:
simp only [hs, const_zero, coe_piecewise, coe_const, SimpleFunc.coe_zero, univ_inter,
      piecewise_eq_indicator, lintegral_indicator, lintegral_const, Measure.restrict_apply',
      ENNReal.coe_indicator, Function.const_apply] at hL

Goal state after:
case const
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
⊢ ∃ g,
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0)) x) ∧
      ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: case const.refine_3
α : 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 < ∞
⊢ L < ∫⁻ (x : α), ↑((piecewise t ht (const α c) (const α 0)) x) ∂μ

Tactic:
· simp only [ht, const_zero, coe_piecewise, coe_const, SimpleFunc.coe_zero,
        piecewise_eq_indicator, ENNReal.coe_indicator, Function.const_apply, lintegral_indicator,
        lintegral_const, Measure.restrict_apply', univ_inter]
      rwa [mul_comm, ← ENNReal.div_lt_iff]
      · simp only [c_ne_zero, Ne, ENNReal.coe_eq_zero, not_false_iff, true_or]
      · 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
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ
⊢ ∃ g,
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0)) x) ∧
      ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Tactic:
| @const c s hs =>

Goal state after:
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoMetricSpace (F i)
x✝ y✝ : (i : ι) → F i
i : ι
x y : (i : ι) → F i
⊢ 0 ≤ dist x y

Tactic:
by rw [dist_eq_tsum]; positivity

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
s t : Set α
hs : AnalyticSet s
ht : AnalyticSet t
h : Disjoint s t
⊢ MeasurablySeparable s t

Tactic:
rw [AnalyticSet] at hs ht

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
s t : Set α
hs : s = ∅ ∨ ∃ f, Continuous[_, inst✝³] f ∧ range f = s
ht : t = ∅ ∨ ∃ f, Continuous[_, inst✝³] f ∧ range f = t
h : Disjoint s t
⊢ MeasurablySeparable s t
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
H : μ.InnerRegularWRT p q
hU : q U
⊢ μ U = ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : p K), μ K

Tactic:
by
  refine
    le_antisymm (le_of_forall_lt fun r hr => ?_) (iSup₂_le fun K hK => iSup_le fun _ => μ.mono hK)
  simpa only [lt_iSup_iff, exists_prop] using H hU r hr

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✝ : 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

Tactic:
exact H c⁻¹ s hs

Goal state after:
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))
i : (ℕ × ℕ) × ℕ
⊢ ∀ s ∈ {s | MeasurableSet s},
    ∀ t ∈ image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} {t | MeasurableSet t},
      (map (⇑MeasurableEquiv.prodAssoc) (((sfiniteSeq μ i.1.1).prod (sfiniteSeq ν i.1.2)).prod (sfiniteSeq τ i.2)))
          (s ×ˢ t) =
        (sfiniteSeq μ i.1.1) s * ((sfiniteSeq ν i.1.2).prod (sfiniteSeq τ i.2)) t

Tactic:
rintro s hs _ ⟨t, ht, u, hu, rfl⟩

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))
i : (ℕ × ℕ) × ℕ
s : Set α
hs : s ∈ {s | MeasurableSet s}
t : Set β
ht : t ∈ {s | MeasurableSet s}
u : Set γ
hu : u ∈ {t | MeasurableSet t}
⊢ (map (⇑MeasurableEquiv.prodAssoc) (((sfiniteSeq μ i.1.1).prod (sfiniteSeq ν i.1.2)).prod (sfiniteSeq τ i.2)))
      (s ×ˢ (fun x1 x2 ↦ x1 ×ˢ x2) t u) =
    (sfiniteSeq μ i.1.1) s * ((sfiniteSeq ν i.1.2).prod (sfiniteSeq τ i.2)) ((fun x1 x2 ↦ x1 ×ˢ x2) t u)
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))
i : (ℕ × ℕ) × ℕ
s : Set α
hs : s ∈ {s | MeasurableSet s}
t : Set β
ht : t ∈ {s | MeasurableSet s}
u : Set γ
hu : u ∈ {t | MeasurableSet t}
⊢ (map (⇑MeasurableEquiv.prodAssoc) (((sfiniteSeq μ i.1.1).prod (sfiniteSeq ν i.1.2)).prod (sfiniteSeq τ i.2)))
      (s ×ˢ (fun x1 x2 ↦ x1 ×ˢ x2) t u) =
    (sfiniteSeq μ i.1.1) s * ((sfiniteSeq ν i.1.2).prod (sfiniteSeq τ i.2)) ((fun x1 x2 ↦ x1 ×ˢ x2) t u)

Tactic:
rw [mem_ofPred_eq] at hs ht hu

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))
i : (ℕ × ℕ) × ℕ
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
u : Set γ
hu : MeasurableSet u
⊢ (map (⇑MeasurableEquiv.prodAssoc) (((sfiniteSeq μ i.1.1).prod (sfiniteSeq ν i.1.2)).prod (sfiniteSeq τ i.2)))
      (s ×ˢ (fun x1 x2 ↦ x1 ×ˢ x2) t u) =
    (sfiniteSeq μ i.1.1) s * ((sfiniteSeq ν i.1.2).prod (sfiniteSeq τ i.2)) ((fun x1 x2 ↦ x1 ×ˢ x2) t u)
Module: Mathlib.MeasureTheory.Group.Pointwise

Goal state before:
pp: G₀ : Type u_1
α : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : Zero α
inst✝³ : MulActionWithZero G₀ α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableConstSMul G₀ α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
a : G₀
⊢ MeasurableSet (a • s)

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Goal state after:
case inl
G₀ : Type u_1
α : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : Zero α
inst✝³ : MulActionWithZero G₀ α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableConstSMul G₀ α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (0 • s)

case inr
G₀ : Type u_1
α : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : Zero α
inst✝³ : MulActionWithZero G₀ α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableConstSMul G₀ α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
a : G₀
ha : a ≠ 0
⊢ MeasurableSet (a • s)
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 α
⊢ (μ.restrict s).prod ν = (μ.prod ν).restrict (s ×ˢ univ)

Tactic:
have : ν = ν.restrict Set.univ := Measure.restrict_univ.symm

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
this : ν = ν.restrict univ
⊢ (μ.restrict s).prod ν = (μ.prod ν).restrict (s ×ˢ univ)
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:
| succ n IH =>

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
Lcompact : ∀ (n : ℕ), IsCompact (L n)
n : ℕ
IH : IsClosed[inst✝⁷] (L n)
⊢ IsClosed[inst✝⁷] (L (n + 1))

Tactic:
| succ n IH =>

Goal state after:
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : CommGroup G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : μ.IsInvInvariant
f g : G → ℝ≥0∞
⊢ f ⋆ₘₗ[μ] g = g ⋆ₘₗ[μ] f

Tactic:
by
  ext x
  simp only [mlconvolution_def]
  rw [← lintegral_mul_left_eq_self _ x, ← lintegral_inv_eq_self]
  simp [mul_comm]

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

Goal state before:

Tactic:
μ.withDensity f s ≤ μ.withDensity f t := measure_mono (subset_toMeasurable μ s)
  _ = ∫⁻ a in t, f a ∂μ := withDensity_apply f (measurableSet_toMeasurable μ s)
  _ = ∫⁻ a in s, f a ∂μ := by congr 1; exact restrict_toMeasurable_of_sFinite s

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
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed[inst✝⁷] (L n)
n : ℕ
IH : μ (L n) = ↑(n + 1) * μ K
⊢ μ (L (n + 1)) = ↑(n + 1 + 1) * μ K

Tactic:
| succ n IH =>

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x | f x = 0}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᵐ[μ] g
a : α
ha : f a = g a
⊢ {x | f x = 0} a = {x | g x = 0} a

Tactic:
rw [eq_iff_iff]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x | f x = 0}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᵐ[μ] g
a : α
ha : f a = g a
⊢ {x | f x = 0} a ↔ {x | g x = 0} a
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᵐ[μ] g
⊢ NullMeasurableSet {x | f x ≠ 0} μ

Tactic:
have nonneg_eq_ae : {x | g x ≠ 0} =ᵐ[μ] {x | f x ≠ 0} := by
      filter_upwards [hfg] with a ha
      simp only [eq_iff_iff]
      exact ⟨fun (h : g a ≠ 0) ↦ by rwa [← ha] at h,
             fun (h : f a ≠ 0) ↦ by rwa [ha] at h⟩

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᵐ[μ] g
nonneg_eq_ae : {x | g x ≠ 0} =ᵐ[μ] {x | f x ≠ 0}
⊢ NullMeasurableSet {x | f x ≠ 0} μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : 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' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a = f' a
h_a_nonneg : f' a ≠ 0
this : ↑(f a) ≠ 0
⊢ ↑(f a) * g a = ↑(f a) * g' a

Tactic:
rw [ha this]

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✝ : Countable ι
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 : ℕ
⊢ Tendsto (fun j ↦ μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)

Tactic:
rcases isEmpty_or_nonempty ι with h | h

Goal state after:
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : PseudoEMetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
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 : ℕ
h : IsEmpty ι
⊢ Tendsto (fun j ↦ μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)

case inr
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : PseudoEMetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
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 : ℕ
h : Nonempty ι
⊢ Tendsto (fun j ↦ μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)
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))
⊢ TendstoUniformlyOn f g atTop (s \ iUnionNotConvergentSeq hε hf hsm hs hfg)

Tactic:
rw [EMetric.tendstoUniformlyOn_iff]
  intro δ hδ
  obtain ⟨N, hN⟩ := ENNReal.exists_inv_nat_lt hδ.ne'
  rw [eventually_atTop]
  refine ⟨Egorov.notConvergentSeqLTIndex (half_pos hε) hf hsm hs hfg N, fun n hn x hx => ?_⟩
  refine lt_of_le_of_lt ?_ hN
  have : edist (f n x) (g x) ≤ (N : ℝ≥0∞)⁻¹ :=
    not_lt.mp fun h ↦ hx.2 <| Set.mem_iUnion.2 ⟨N, hx.1, mem_notConvergentSeq_iff.2 ⟨n, hn, h⟩⟩
  simpa [edist_comm]

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

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ √x ≠ 0 ↔ x ≠ 0

Tactic:
not_iff_not,

Goal state after:
x : ℝ
h : 0 ≤ x
⊢ √x = 0 ↔ x = 0
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ √x = 0 ↔ x = 0

Tactic:
sqrt_eq_zero h

Goal state after:
x : ℝ
h : 0 ≤ x
⊢ x = 0 ↔ x = 0
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
⊢ √x ≠ 0 ↔ ¬x ≤ 0

Tactic:
not_iff_not,

Goal state after:
x : ℝ
⊢ √x = 0 ↔ x ≤ 0
Module: Mathlib.Analysis.Real.Sqrt

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

Tactic:
by
  rw [← sqrt_one, sqrt_le_sqrt_iff zero_le_one, sqrt_one]

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
hf_ne_top✝ : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
x : α
hf_ne_zero : f x ≠ 0
hf_ne_top : f x ≠ ∞
⊢ 1 = 1 x

Tactic:
Pi.one_apply

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero✝ : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top✝ : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
x : α
hf_ne_zero : f x ≠ 0
hf_ne_top : f x ≠ ∞
⊢ 1 = 1
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
hfm : Measurable f
⊢ SFinite (μ.withDensity f)

Tactic:
wlog hμ : IsFiniteMeasure μ generalizing μ

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
hfm : Measurable f
this : ∀ {μ : Measure α} [SFinite μ], IsFiniteMeasure μ → SFinite (μ.withDensity f)
hμ : ¬IsFiniteMeasure μ
⊢ SFinite (μ.withDensity f)

α : Type u_1
m0 : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
⊢ SFinite (μ.withDensity f)
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x | f x = ∞}
hs : MeasurableSet s
key : μ.withDensity f = μ.withDensity (sᶜ.indicator f) + sum fun x ↦ μ.withDensity (s.indicator 1)
⊢ SigmaFinite (μ.withDensity (sᶜ.indicator f))

Tactic:
refine SigmaFinite.withDensity_of_ne_top <| ae_of_all _ fun x hx ↦ ?_

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x | f x = ∞}
hs : MeasurableSet s
key : μ.withDensity f = μ.withDensity (sᶜ.indicator f) + sum fun x ↦ μ.withDensity (s.indicator 1)
x : α
hx : sᶜ.indicator f x = ∞
⊢ False
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝² : SFinite μ
R : Type u_2
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
⊢ SFinite (c • μ)

Tactic:
have : c • μ = c • ((1 : ℝ≥0∞) • μ) := by simp
  rw [this, ← smul_assoc, ← withDensity_const]
  infer_instance

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : AddCommMonoid α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Module ℚ≥0 α
f : ι → α
hf : f ≤ 0
⊢ 𝔼 i, f i = 0 ↔ f = 0

Tactic:
by
  rw [Finset.expect_eq_zero_iff_of_nonpos (by aesop)]
  aesop

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

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ f g : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖f‖ * ‖v‖ + ‖g‖ * ‖v‖ = (‖f‖ + ‖g‖) * ‖v‖

Tactic:
rw [add_mul]

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₂
ψ : NormedAddGroupHom W₁ W₂
hf : ψ.comp f₁ = f₂.comp φ
hg : ψ.comp g₁ = g₂.comp φ
⊢ f₂.comp (φ.comp (ι f₁ g₁)) = g₂.comp (φ.comp (ι f₁ g₁))

Tactic:
simp only [← comp_assoc, ← hf, ← hg]

Goal state after:
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₂
ψ : NormedAddGroupHom W₁ W₂
hf : ψ.comp f₁ = f₂.comp φ
hg : ψ.comp g₁ = g₂.comp φ
⊢ (ψ.comp f₁).comp (ι f₁ g₁) = (ψ.comp g₁).comp (ι f₁ g₁)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ re 1 = 1

Tactic:
← ofReal_one,

Goal state after:
K : Type u_1
inst✝ : RCLike K
⊢ re ↑1 = 1
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ im 1 = 0

Tactic:
← ofReal_one,

Goal state after:
K : Type u_1
inst✝ : RCLike K
⊢ im ↑1 = 0
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: x : ℂ
hx : 0 ≤ x
⊢ ↑‖x‖ = x

Tactic:
rw [← RCLike.ofReal_eq_complex_ofReal]

Goal state after:
x : ℂ
hx : 0 ≤ x
⊢ ↑‖x‖ = x
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
a : A
a_eq : a = ↑(ℜ a) + I • ↑(ℑ a)
⊢ star (↑(ℜ a) + I • ↑(ℑ a)) * (↑(ℜ a) + I • ↑(ℑ a)) + (↑(ℜ a) + I • ↑(ℑ a)) * star (↑(ℜ a) + I • ↑(ℑ a)) =
    2 • (↑(ℜ a) * ↑(ℜ a) + ↑(ℑ a) * ↑(ℑ a))

Tactic:
simp [mul_add, add_mul, smul_smul, mul_smul_comm,
        smul_mul_assoc]

Goal state after:
A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
a : A
a_eq : a = ↑(ℜ a) + I • ↑(ℑ a)
⊢ ↑(ℜ a) * ↑(ℜ a) + -(I • (↑(ℑ a) * ↑(ℜ a))) + (I • (↑(ℜ a) * ↑(ℑ a)) + ↑(ℑ a) * ↑(ℑ a)) +
      (↑(ℜ a) * ↑(ℜ a) + I • (↑(ℑ a) * ↑(ℜ a)) + (↑(ℑ a) * ↑(ℑ a) + -(I • (↑(ℜ a) * ↑(ℑ a))))) =
    2 • (↑(ℜ a) * ↑(ℜ a)) + 2 • (↑(ℑ a) * ↑(ℑ a))
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ re z⁻¹ = re z / normSq z

Tactic:
rw [inv_def, normSq_eq_def', mul_comm, re_ofReal_mul, conj_re, div_eq_inv_mul]

Goal state after: