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

Goal state before:
pp: Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω'
inst✝⁵ : TopologicalSpace Ω'
inst✝⁴ : BorelSpace Ω'
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : BorelSpace Ω
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') := {μ | μ (range f)ᶜ = 0}
A : IsEmbedding Subtype.val
μ : ↑M
s : Set Ω'
hs : MeasurableSet s
⊢ ↑(comap f ↑μ) (f ⁻¹' s) = ↑↑μ s

Tactic:
simp only [toMeasure_comap]

Goal state after:
Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω'
inst✝⁵ : TopologicalSpace Ω'
inst✝⁴ : BorelSpace Ω'
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : BorelSpace Ω
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') := {μ | μ (range f)ᶜ = 0}
A : IsEmbedding Subtype.val
μ : ↑M
s : Set Ω'
hs : MeasurableSet s
⊢ (Measure.comap f ↑↑μ) (f ⁻¹' s) = ↑↑μ s
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : PseudoMetrizableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
μs : ι → Measure Ω
h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i ↦ (μs i) E) L (𝓝 (μ E))
F : Set Ω
F_closed : IsClosed[inst✝³] F
this : PseudoMetricSpace Ω := pseudoMetrizableSpacePseudoMetric Ω
h✝ : L.NeBot
ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0
rs : ℕ → ℝ := Classical.choose ex
rs_pos : ∀ (n : ℕ), 0 < rs n
rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0
Fthicks_open : ∀ (n : ℕ), IsOpen[inst✝³] (Metric.thickening (rs n) F)
key : ∀ (n : ℕ), Tendsto (fun i ↦ (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))
ε : ℝ≥0
ε_pos : 0 < ε
μF_finite : μ F < ∞
keyB : Tendsto (fun r ↦ μ (Metric.cthickening r F)) (𝓝 0) (𝓝 (μ F))
nhds : Iio (μ F + ↑ε) ∈ 𝓝 (μ F)
rs_lim : ∃ a, ∀ (b : ℕ), a ≤ b → μ (Metric.cthickening (rs b) F) < μ F + ↑ε
⊢ limsup (fun i ↦ (μs i) F) L ≤ μ F + ↑ε

Tactic:
obtain ⟨m, hm⟩ := rs_lim

Goal state after:
case inr
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : PseudoMetrizableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
μs : ι → Measure Ω
h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i ↦ (μs i) E) L (𝓝 (μ E))
F : Set Ω
F_closed : IsClosed[inst✝³] F
this : PseudoMetricSpace Ω := pseudoMetrizableSpacePseudoMetric Ω
h✝ : L.NeBot
ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0
rs : ℕ → ℝ := Classical.choose ex
rs_pos : ∀ (n : ℕ), 0 < rs n
rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0
Fthicks_open : ∀ (n : ℕ), IsOpen[inst✝³] (Metric.thickening (rs n) F)
key : ∀ (n : ℕ), Tendsto (fun i ↦ (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))
ε : ℝ≥0
ε_pos : 0 < ε
μF_finite : μ F < ∞
keyB : Tendsto (fun r ↦ μ (Metric.cthickening r F)) (𝓝 0) (𝓝 (μ F))
nhds : Iio (μ F + ↑ε) ∈ 𝓝 (μ F)
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → μ (Metric.cthickening (rs b) F) < μ F + ↑ε
⊢ limsup (fun i ↦ (μs i) F) L ≤ μ F + ↑ε
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
⊢ IndepSets (s i) (s j) κ μ

Tactic:
intro t₁

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
t₁ : Set Ω
⊢ ∀ (t2 : Set Ω), t₁ ∈ s i → t2 ∈ s j → ∀ᵐ (a : α) ∂μ, (κ a) (t₁ ∩ t2) = (κ a) t₁ * (κ a) t2
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case inr
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πS
πTβ : Set (Set ((i : ↥T) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπT_pi : IsPiSystem πT
⊢ IndepFun (fun a i ↦ f (↑i) a) (fun a i ↦ f (↑i) a) η μ

Tactic:
have hπT_gen : (MeasurableSpace.pi.comap fun a (i : T) => f i a) = generateFrom πT := by
    rw [generateFrom_pi.symm, comap_generateFrom]
    congr

Goal state after:
case inr
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πS
πTβ : Set (Set ((i : ↥T) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπT_pi : IsPiSystem πT
hπT_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πT
⊢ IndepFun (fun a i ↦ f (↑i) a) (fun a i ↦ f (↑i) a) η μ
Module: Mathlib.Probability.Density

Goal state before:
pp: case e_f
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝¹ : IsFiniteMeasure ℙ
inst✝ : HasPDF X ℙ volume
x : ℝ
⊢ x * (pdf X ℙ volume x).toReal = (pdf X ℙ volume x).toReal * x

Tactic:
exact mul_comm _ _

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
a : ι
S : Finset ι
hp_ind : iIndepSets π κ μ
haS : a ∉ S
t1 t2 : Set Ω
s : Finset ι
hs_mem : s ⊆ S
ft1 : ι → Set Ω
hft1_mem : ∀ x ∈ s, ft1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ s, ft1 x
ht2_mem_pia : t2 ∈ π a
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
classical
  let f := fun n => ite (n = a) t2 (ite (n ∈ s) (ft1 n) Set.univ)
  have h_f_mem : ∀ n ∈ insert a s, f n ∈ π n := by
    intro n hn_mem_insert
    dsimp only [f]
    rcases Finset.mem_insert.mp hn_mem_insert with hn_mem | hn_mem
    · simp [hn_mem, ht2_mem_pia]
    · grind
  have h_f_mem_pi : ∀ n ∈ s, f n ∈ π n := fun x hxS => h_f_mem x (by simp [hxS])
  have h_t1 : t1 = ⋂ n ∈ s, f n := by
    suffices h_forall : ∀ n ∈ s, f n = ft1 n by grind
    intro n hnS
    have hn_ne_a : n ≠ a := by rintro rfl; exact haS (hs_mem hnS)
    simp_rw [f, if_pos hnS, if_neg hn_ne_a]
  have h_μ_t1 : ∀ᵐ a' ∂μ, κ a' t1 = ∏ n ∈ s, κ a' (f n) := by
    filter_upwards [hp_ind s h_f_mem_pi] with a' ha'
    rw [h_t1, ← ha']
  have h_t2 : t2 = f a := by simp [f]
  have h_μ_inter : ∀ᵐ a' ∂μ, κ a' (t1 ∩ t2) = ∏ n ∈ insert a s, κ a' (f n) := by
    have h_t1_inter_t2 : t1 ∩ t2 = ⋂ n ∈ insert a s, f n := by
      rw [h_t1, h_t2, Finset.set_biInter_insert, Set.inter_comm]
    filter_upwards [hp_ind (insert a s) h_f_mem] with a' ha'
    rw [h_t1_inter_t2, ← ha']
  have has : a ∉ s := fun has_mem => haS (hs_mem has_mem)
  filter_upwards [h_μ_t1, h_μ_inter] with a' ha1 ha2
  rw [ha2, Finset.prod_insert has, h_t2, mul_comm, ha1]

Goal state after:
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case e'_4
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
c : ℝ
hc : 0 < c
⊢ eVar[X; μ] / ENNReal.ofReal (c ^ 2) = eVar[X; μ] / ↑c.toNNReal ^ 2

Tactic:
rw [ENNReal.ofReal_pow hc.le]

Goal state after:
case e'_4
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
c : ℝ
hc : 0 < c
⊢ eVar[X; μ] / ENNReal.ofReal c ^ 2 = eVar[X; μ] / ↑c.toNNReal ^ 2
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s).Pairwise fun i j ↦ X i ⟂ᵢ[μ] X j
h'' : ∀ i ∈ s, X i =ᵐ[μ] 0
⊢ ∑ i ∈ s, Var[X i; μ] = 0

Tactic:
refine Finset.sum_eq_zero fun i hi ↦ ?_

Goal state after:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s).Pairwise fun i j ↦ X i ⟂ᵢ[μ] X j
h'' : ∀ i ∈ s, X i =ᵐ[μ] 0
i : ι
hi : i ∈ s
⊢ Var[X i; μ] = 0
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
u : γ → δ
h : IdentDistrib f g μ ν
hu : AEMeasurable u (Measure.map f μ)
⊢ Measure.map (u ∘ f) μ = Measure.map (u ∘ g) ν

Tactic:
rw [← AEMeasurable.map_map_of_aemeasurable hu h.aemeasurable_fst, ←
        AEMeasurable.map_map_of_aemeasurable _ h.aemeasurable_snd, h.map_eq]
      rwa [← h.map_eq]

Goal state after:
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g μ ν
hf : AEStronglyMeasurable f μ
⊢ ∫ (x : α), f x ∂μ = ∫ (x : β), g x ∂ν

Tactic:
have A : AEStronglyMeasurable id (Measure.map f μ) := by
      rw [aestronglyMeasurable_iff_aemeasurable_separable]
      rcases (aestronglyMeasurable_iff_aemeasurable_separable.1 hf).2 with ⟨t, t_sep, ht⟩
      refine ⟨aemeasurable_id, ⟨closure t, t_sep.closure, ?_⟩⟩
      rw [ae_map_iff h.aemeasurable_fst]
      · filter_upwards [ht] with x hx using subset_closure hx
      · exact isClosed_closure.measurableSet

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g μ ν
hf : AEStronglyMeasurable f μ
A : AEStronglyMeasurable id (Measure.map f μ)
⊢ ∫ (x : α), f x ∂μ = ∫ (x : β), g x ∂ν
Module: Mathlib.MeasureTheory.Function.FactorsThrough

Goal state before:
pp: case pcw
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst✝² : Nonempty Z
inst✝¹ : TopologicalSpace Z
inst✝ : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
t : Set Y
ht : MeasurableSet t
h₁ : Y → Z
mh₁ : StronglyMeasurable h₁
hg₁ : StronglyMeasurable (h₁ ∘ f)
h₂ : Y → Z
mh₂ : StronglyMeasurable h₂
hg₂ : StronglyMeasurable (h₂ ∘ f)
⊢ ∃ h, StronglyMeasurable h ∧ (f ⁻¹' t).piecewise (h₁ ∘ f) (h₂ ∘ f) = h ∘ f

Tactic:
exact ⟨t.piecewise h₁ h₂, mh₁.piecewise ht mh₂, by rw [piecewise_comp]⟩

Goal state after:
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
⊢ (if s.Nonempty then sInf ((fun f ↦ ↑f i) '' s) else m) ≤ m

Tactic:
by_cases h_nonempty : Set.Nonempty s
        swap; · simp only [h_nonempty, if_false, le_refl]
        simp only [h_nonempty, if_true]
        obtain ⟨f, hf_mem⟩ := h_nonempty
        exact le_trans (sInf_le ⟨f, hf_mem, rfl⟩) (f.le i)

Goal state after:
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t : Set Ω
n : ι
ht : MeasurableSet t
this : MeasurableSpace.generateFrom {t | n ≤ i ∧ MeasurableSet t} ≤ MeasurableSpace.generateFrom {t | ∃ j ≤ i, s j = t}
⊢ MeasurableSet t

Tactic:
exact this _ ht

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count

Goal state before:
pp: α : Type u_1
ε : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p : ℝ≥0∞
f : α → ε
i : α
hp : p ≠ 0
⊢ ‖f i‖ₑ = eLpNorm f p (dirac i)

Tactic:
eLpNorm_dirac f i hp

Goal state after:
α : Type u_1
ε : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p : ℝ≥0∞
f : α → ε
i : α
hp : p ≠ 0
⊢ ‖f i‖ₑ = ‖f i‖ₑ
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case pos
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst✝ : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ f n ω) atTop (𝓝 (g ω))
⊢ liminf (fun n ↦ eLpNorm (f n) p μ) atTop ≤ ↑R

Tactic:
simp_rw [liminf_eq, eventually_atTop]

Goal state after:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst✝ : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ f n ω) atTop (𝓝 (g ω))
⊢ sSup {a | ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a ≤ eLpNorm (f b) p μ} ≤ ↑R
Module: Mathlib.MeasureTheory.Integral.Indicator

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
inst✝ : IsFiniteMeasure μ
As_mble : ∀ (i : ι), MeasurableSet (As i)
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ Tendsto (fun i ↦ μ (As i)) L (𝓝 (μ A))

Tactic:
rcases L.eq_or_neBot with rfl | _
  · exact tendsto_bot
  apply tendsto_measure_of_ae_tendsto_indicator_of_isFiniteMeasure L ?_ As_mble (ae_of_all μ h_lim)
  exact measurableSet_of_tendsto_indicator L As_mble h_lim

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case e'_3
p : ℝ
hp : 1 ≤ p
⊢ π * Real.Gamma (2 / p + 1) = 2 * π / p * Real.Gamma ((0 + 2) / p)

Tactic:
rw [zero_add, Real.Gamma_add_one (div_ne_zero two_ne_zero (by linarith))]
    ring

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case e'_3
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ π * b ^ (-2 / p) * Real.Gamma (2 / p + 1) = 2 * π / p * b ^ (-(0 + 2) / p) * Real.Gamma ((0 + 2) / p)

Tactic:
rw [zero_add, Real.Gamma_add_one (div_ne_zero two_ne_zero (by linarith))]
    ring

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b : E
ω₁ ω₂ : E → E →L[𝕜] F
γ : Path a b
h₁ : CurveIntegrable ω₁ γ
h₂ : CurveIntegrable ω₂ γ
⊢ curveIntegral (ω₁ + ω₂) γ = ∫ᶜ (x : E) in γ, ω₁ x + ∫ᶜ (x : E) in γ, ω₂ x

Tactic:
by
  let : NormedSpace ℝ F := .restrictScalars ℝ 𝕜 F
  simp only [curveIntegral, curveIntegralFun_add]
  exact intervalIntegral.integral_add h₁ h₂

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: case e'_4
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd : ∀ t ∈ Ioo 0 1, LineDifferentiableAt ℝ f ((lineMap a b) t) (b - a)
hf' : ∀ᵐ (t : ℝ), t ∈ Ioo 0 1 → ‖lineDeriv ℝ f ((lineMap a b) t) (b - a)‖ ≤ C
g : ℝ → F := fun t ↦ f ((lineMap a b) t)
hgc : ContinuousOn g (Icc 0 1)
hdg : ∀ t ∈ Ioo 0 1, HasDerivAt g (lineDeriv ℝ f ((lineMap a b) t) (b - a)) t
this : ‖g 1 - g 0‖ ≤ C * volume.real {t | t ∈ Ioo 0 1 ∧ deriv g t ≠ 0}
⊢ C * volume.real {t | t ∈ Ioo 0 1 ∧ lineDeriv ℝ f ((lineMap a b) t) (b - a) ≠ 0} =
    C * volume.real {t | t ∈ Ioo 0 1 ∧ deriv g t ≠ 0}

Tactic:
congr 2 with t
      simp +contextual [(hdg _ _).deriv]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, ‖fderiv ℝ f x‖ ≤ C
⊢ ‖f b - f a‖ ≤ C * ‖b - a‖ * volume.real {t | t ∈ Ioo 0 1 ∧ fderiv ℝ f ((lineMap a b) t) ≠ 0}

Tactic:
have hmem_s : ∀ t ∈ Ioo (0 : ℝ) 1, lineMap a b t ∈ s := fun t ht ↦
    hab <| lineMap_mem_openSegment _ a b ht
  have hC₀ : 0 ≤ C := (norm_nonneg _).trans <| hC _ <| hmem_s (1 / 2) (by norm_num)
  have hfc : ContinuousOn f (segment ℝ a b) :=
    hf.continuousOn.mono <| segment_subset_closure_openSegment.trans <| closure_mono hab
  have hfd : ∀ t ∈ Ioo (0 : ℝ) 1, LineDifferentiableAt ℝ f (lineMap a b t) (b - a) := fun t ht ↦
    (hf.differentiableAt hs <| hmem_s t ht).lineDifferentiableAt
  have hfC : ∀ t ∈ Ioo (0 : ℝ) 1, ‖lineDeriv ℝ f (lineMap a b t) (b - a)‖ ≤ C * ‖b - a‖ := by
    intro t ht
    rw [DifferentiableAt.lineDeriv_eq_fderiv]
    · exact ContinuousLinearMap.le_of_opNorm_le _ (hC _ <| hmem_s t ht) _
    · exact hf.differentiableAt hs <| hmem_s t ht
  refine norm_sub_le_mul_volume_of_norm_lineDeriv_le hfc hfd (.of_forall hfC) |>.trans ?_
  gcongr
  · refine ne_top_of_le_ne_top ?_ (measure_mono inter_subset_left)
    simp
  · simp +contextual [(hf.differentiableAt hs <| hmem_s _ ‹_›).lineDeriv_eq_fderiv]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
h_f_int : IntervalIntegrable f volume a (a + ↑N * h)
k : ℕ
hk : k < N
⊢ ∀ {k : ℕ}, k ≤ N → a + ↑k * h ∈ [[a, a + ↑N * h]]

Tactic:
rcases le_total h 0 with h_neg | h_pos

Goal state after:
case inl
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
h_f_int : IntervalIntegrable f volume a (a + ↑N * h)
k : ℕ
hk : k < N
h_neg : h ≤ 0
⊢ ∀ {k : ℕ}, k ≤ N → a + ↑k * h ∈ [[a, a + ↑N * h]]

case inr
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
h_f_int : IntervalIntegrable f volume a (a + ↑N * h)
k : ℕ
hk : k < N
h_pos : 0 ≤ h
⊢ ∀ {k : ℕ}, k ≤ N → a + ↑k * h ∈ [[a, a + ↑N * h]]
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
⊢ (rieszContent Λ).ContentRegular

Tactic:
intro K
  simp only [rieszContent, le_antisymm_iff, le_iInf_iff, ENNReal.coe_le_coe, Content.mk_apply]
  refine ⟨fun K' hK' ↦ rieszContentAux_mono Λ (hK'.trans interior_subset), ?_⟩
  rw [iInf_le_iff]
  intro b hb
  rw [rieszContentAux, ENNReal.le_coe_iff]
  have : b < ⊤ := by
    obtain ⟨F, hF⟩ := exists_compact_superset K.2
    exact (le_iInf_iff.mp (hb ⟨F, hF.1⟩) hF.2).trans_lt ENNReal.coe_lt_top
  refine ⟨b.toNNReal, (ENNReal.coe_toNNReal this.ne).symm, NNReal.coe_le_coe.mp ?_⟩
  apply le_iff_forall_pos_le_add.mpr
  intro ε hε
  lift ε to ℝ≥0 using hε.le
  obtain ⟨f, hfleoneonK, hfle⟩ := exists_lt_rieszContentAux_add_pos Λ K (Real.toNNReal_pos.mpr hε)
  rw [rieszContentAux, Real.toNNReal_of_nonneg hε.le, ← NNReal.coe_lt_coe] at hfle
  refine ((le_iff_forall_one_lt_le_mul₀ (zero_le (a := Λ f))).mpr fun α hα ↦ ?_).trans hfle.le
  rw [mul_comm, ← smul_eq_mul, ← map_smul]
  set K' := f ⁻¹' Ici α⁻¹
  have hKK' : ↑K ⊆ interior K' :=
    subset_interior_iff.2 ⟨f ⁻¹' Ioi α⁻¹, isOpen_Ioi.preimage f.1.2,
      fun x hx ↦ (inv_lt_one_of_one_lt₀ hα).trans_le (hfleoneonK x hx),
      preimage_mono Ioi_subset_Ici_self⟩
  have hK'cp : IsCompact K' := .of_isClosed_subset f.2 (isClosed_Ici.preimage f.1.2) fun x hx ↦
    subset_closure ((inv_pos_of_pos <| zero_lt_one.trans hα).trans_le hx).ne'
  set hb' := hb ⟨K', hK'cp⟩
  simp only [Compacts.coe_mk, le_iInf_iff] at hb'
  exact (ENNReal.toNNReal_mono (by simp) <| hb' hKK').trans <| csInf_le'
    ⟨α • f, fun x ↦ (inv_le_iff_one_le_mul₀' (zero_lt_one.trans hα)).mp, by simp⟩

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: case inr
f : ℝ → ℝ
a b : ℝ
h_f_c2 : ContDiffOn ℝ 2 f [[a, b]]
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_ne : a ≠ b
⊢ |trapezoidal_error f N a b| ≤ |b - a| ^ 3 * ζ / (12 * ↑N ^ 2)

Tactic:
have h_ddf : DifferentiableOn ℝ (derivWithin f [[a, b]]) [[a, b]] := by
    rw [← iteratedDerivWithin_one]
    exact h_f_c2.differentiableOn_iteratedDerivWithin (by norm_cast) (uniqueDiffOn_uIcc h_ne)

Goal state after:
case inr
f : ℝ → ℝ
a b : ℝ
h_f_c2 : ContDiffOn ℝ 2 f [[a, b]]
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_ne : a ≠ b
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f [[a, b]]) [[a, b]]
⊢ |trapezoidal_error f N a b| ≤ |b - a| ^ 3 * ζ / (12 * ↑N ^ 2)
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: case refine_4
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
⊢ ∀ (f : ℕ → Set α),
    (∀ (n : ℕ),
        (∃ i, ∃ (_ : i < ω_ 1), f n ∈ generateMeasurableRec s i) ∧ ∃ j < ω_ 1, f n ∈ generateMeasurableRec s j) →
      ∃ i, ∃ (_ : i < ω_ 1), ⋃ n, f n ∈ generateMeasurableRec s i

Tactic:
intro f H
    choose I hI using fun n => (H n).1
    simp_rw [exists_prop] at hI
    refine ⟨_, Ordinal.lift_iSup_add_one_lt_of_lt_cof ?_ fun n => (hI n).1,
      iUnion_mem_generateMeasurableRec fun n => ⟨_, Ordinal.lt_iSup_add_one I n, (hI n).2⟩⟩
    simp

Goal state after:
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
s : Set X
a : X
hs : IsClosed[inst✝¹] s
ha : a ∉ s
f : X → ↑I
cf : Continuous[inst✝¹, _] f
hf : f a = 0
hhf : EqOn f 1 s
⊢ Disjoint (𝓝ˢ s) (𝓝 a)

Tactic:
apply disjoint_of_map (f := f)

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
s : Set X
a : X
hs : IsClosed[inst✝¹] s
ha : a ∉ s
f : X → ↑I
cf : Continuous[inst✝¹, _] f
hf : f a = 0
hhf : EqOn f 1 s
⊢ Disjoint (map f (𝓝ˢ s)) (map f (𝓝 a))
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_3
inst✝⁶ : MeasurableSpace E
μ ν : Measure E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
t : E
⊢ charFun (μ ∗ ν) t = charFun μ t * charFun ν t

Tactic:
by
  simp_rw [charFun_apply]
  rw [integral_conv]
  · simp [inner_add_left, add_mul, Complex.exp_add, integral_const_mul, integral_mul_const]
  · exact (integrable_const (1 : ℝ)).mono (by fun_prop) (by simp)

Goal state after: