mathlib-initiative/mathlib-tactics huggingface dataset:
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
hπT_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πT
s : Set ((i : ↥S) → β ↑i)
sets_s : (i : ↥S) → Set (β ↑i)
hs2 : univ.pi sets_s = s
t : Set ((i : ↥T) → β ↑i)
sets_t : (i : ↥T) → Set (β ↑i)
ht2 : univ.pi sets_t = t
hs1 : ∀ (i : ↥S), MeasurableSet (sets_s i)
ht1 : ∀ (i : ↥T), MeasurableSet (sets_t i)
sets_s' : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ S then sets_s ⟨i, hi⟩ else univ
⊢ ∀ᵐ (a : α) ∂μ,
    (η a) ((fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_s ∩ (fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_t) =
      (η a) ((fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_s) * (η a) ((fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_t)

Tactic:
have h_sets_s'_eq : ∀ {i} (hi : i ∈ S), sets_s' i = sets_s ⟨i, hi⟩ := by
    intro i hi; simp_rw [sets_s', dif_pos hi]

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
s : Set ((i : ↥S) → β ↑i)
sets_s : (i : ↥S) → Set (β ↑i)
hs2 : univ.pi sets_s = s
t : Set ((i : ↥T) → β ↑i)
sets_t : (i : ↥T) → Set (β ↑i)
ht2 : univ.pi sets_t = t
hs1 : ∀ (i : ↥S), MeasurableSet (sets_s i)
ht1 : ∀ (i : ↥T), MeasurableSet (sets_t i)
sets_s' : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ S then sets_s ⟨i, hi⟩ else univ
h_sets_s'_eq : ∀ {i : ι} (hi : i ∈ S), sets_s' i = sets_s ⟨i, hi⟩
⊢ ∀ᵐ (a : α) ∂μ,
    (η a) ((fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_s ∩ (fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_t) =
      (η a) ((fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_s) * (η a) ((fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_t)
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᵐ[volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
⊢ (fun i ↦ ENNReal.ofReal (pdf X ℙ volume i).toReal) =ᵐ[volume] fun x ↦ ‖(pdf X ℙ volume x).toReal‖ₑ

Tactic:
simp only [Real.enorm_eq_ofReal ENNReal.toReal_nonneg, ae_eq_refl]

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst✝¹] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst✝¹] G
r : ℝ≥0
hr : r < ν G
s : ↑G → Set Ω
hsS : ∀ (x : ↑G), s x ∈ S
hs_nhds : ∀ (x : ↑G), s x ∈ 𝓝 ↑x
hsG : ∀ (x : ↑G), s x ⊆ G
T₀ : Set ↑G
T₀_count : T₀.Countable
hT₀ : ⋃ i ∈ T₀, interior (s i) = ⋃ i, interior (s i)
this : G ⊆ ⋃ i, interior (s i)
⊢ G ⊆ ⋃ t ∈ s '' T₀, t

Tactic:
apply this.trans

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst✝¹] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst✝¹] G
r : ℝ≥0
hr : r < ν G
s : ↑G → Set Ω
hsS : ∀ (x : ↑G), s x ∈ S
hs_nhds : ∀ (x : ↑G), s x ∈ 𝓝 ↑x
hsG : ∀ (x : ↑G), s x ⊆ G
T₀ : Set ↑G
T₀_count : T₀.Countable
hT₀ : ⋃ i ∈ T₀, interior (s i) = ⋃ i, interior (s i)
this : G ⊆ ⋃ i, interior (s i)
⊢ ⋃ i, interior (s i) ⊆ ⋃ t ∈ s '' T₀, t
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: case neg
α : 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:
rw [integral_non_aestronglyMeasurable hf]
    rw [h.aestronglyMeasurable_iff] at hf
    rw [integral_non_aestronglyMeasurable hf]

Goal state after:
Module: Mathlib.MeasureTheory.Function.FactorsThrough

Goal state before:
pp: 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✝¹ : MeasurableSpace Z
inst✝ : StandardBorelSpace Z
hg : Measurable g
⊢ ∃ h, Measurable h ∧ g = h ∘ f

Tactic:
let := upgradeStandardBorel Z

Goal state after:
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✝¹ : MeasurableSpace Z
inst✝ : StandardBorelSpace Z
hg : Measurable g
this : UpgradedStandardBorel Z := upgradeStandardBorel Z
⊢ ∃ h, Measurable h ∧ g = h ∘ f
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : 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
hf_indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
⊢ IndepFun (fun a ↦ (f i a, f j a)) (fun a ↦ (f k a, f l a)) κ μ

Tactic:
have h : IndepFun (fun a ↦ ((hf_meas i).mk (f i) a, (hf_meas j).mk (f j) a))
      (fun a ↦ ((hf_meas k).mk (f k) a, (hf_meas l).mk (f l) a)) κ μ := by
    refine iIndepFun.indepFun_prodMk_prodMk ?_ (fun i ↦ (hf_meas i).measurable_mk) _ _ _ _ hik hil
      hjk hjl
    exact iIndepFun.congr' hf_indep fun i ↦ Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk
  refine IndepFun.congr' h ?_ ?_
  · filter_upwards [Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk,
      Measure.ae_ae_of_ae_comp (hf_meas j).ae_eq_mk] with a hi hj
    filter_upwards [hi, hj] with ω hωi hωj
    rw [← hωi, ← hωj]
  · filter_upwards [Measure.ae_ae_of_ae_comp (hf_meas k).ae_eq_mk,
      Measure.ae_ae_of_ae_comp (hf_meas l).ae_eq_mk] with a hk hl
    filter_upwards [hk, hl] with ω hωk hωl
    rw [← hωk, ← hωl]

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
f g : Filtration ι m
h : ↑f = ↑g
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
g : Filtration ι m
seq✝ : ι → MeasurableSpace Ω
mono'✝ : Monotone seq✝
le'✝ : ∀ (i : ι), seq✝ i ≤ m
h : ↑{ seq := seq✝, mono' := mono'✝, le' := le'✝ } = ↑g
⊢ { seq := seq✝, mono' := mono'✝, le' := le'✝ } = g
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: case h₂
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
F : E → ℝ
M : ℝ
hF_bounded : ∀ (x y : E), dist (F x) (F y) ≤ M
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
ε : ℝ
hε : ε > 0
n : ι
h_int_Y : Integrable (fun x ↦ F (Y n x)) μ''
h_int_X : Integrable (fun x ↦ F (X n x)) μ''
h_int_sub : Integrable (fun a ↦ ‖F (Y n a) - F (X n a)‖) μ''
a : Ω''
⊢ ‖F (Y n a) - F (X n a)‖ ≤ M

Tactic:
rw [← dist_eq_norm]

Goal state after:
case h₂
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
F : E → ℝ
M : ℝ
hF_bounded : ∀ (x y : E), dist (F x) (F y) ≤ M
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
ε : ℝ
hε : ε > 0
n : ι
h_int_Y : Integrable (fun x ↦ F (Y n x)) μ''
h_int_X : Integrable (fun x ↦ F (X n x)) μ''
h_int_sub : Integrable (fun a ↦ ‖F (Y n a) - F (X n a)‖) μ''
a : Ω''
⊢ dist (F (Y n a)) (F (X n a)) ≤ M
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i j : ι
hij : i ≤ j
hi : ¬(𝓝[>] i).NeBot
hj : ¬(𝓝[>] j).NeBot
⊢ ↑𝓕 i ≤ ↑𝓕 j

Tactic:
exact 𝓕.mono hij

Goal state after:
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
⊢ ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε

Tactic:
obtain rfl | hμ := eq_or_ne μ 0

Goal state after:
case pos.inl
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hg' : MemLp g p 0
hui : UnifIntegrable f p 0
hut : UnifTight f p 0
hfg : ∀ᵐ (x : α) ∂0, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p 0 ≤ ε

case pos.inr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
⊢ ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
Module: Mathlib.MeasureTheory.Group.ModularCharacter

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : LocallyCompactSpace G
g : G
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
⊢ 0 < (map (fun x ↦ x * g) haar).haarScalarFactor haar

Tactic:
exact haarScalarFactor_pos_of_isHaarMeasure _ _

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

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : LocallyCompactSpace G
g h : G
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
mul_g_meas : Measurable fun x ↦ x * g
mul_h_meas : Measurable fun x ↦ x * h
ν : Measure G := haar
⊢ modularCharacterFun h * modularCharacterFun g =
    (map (fun x ↦ x * h) (map (fun x ↦ x * g) ν)).haarScalarFactor (map (fun x ↦ x * g) ν) * modularCharacterFun g

Tactic:
rw [modularCharacterFun_eq_haarScalarFactor (map (· * g) ν) _]

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

Goal state before:
pp: case refine_2
E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯.choose
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun n ↦ (1 + u n) • K
Z : ℕ → Set E := fun n ↦ ↑(S n) ∩ (↑L \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
⊢ μ s < μ (↑(1 + u n) • ↑K)

Tactic:
addHaar_smul_of_nonneg _ (NNReal.coe_nonneg _)

Goal state after:
case refine_2
E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯.choose
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun n ↦ (1 + u n) • K
Z : ℕ → Set E := fun n ↦ ↑(S n) ∩ (↑L \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
⊢ μ s < ENNReal.ofReal (↑(1 + u n) ^ finrank ℝ E) * μ ↑K
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : TendstoInMeasure μ f atTop g
⊢ Tendsto (fun n ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)

Tactic:
refine tendsto_of_subseq_tendsto fun ns hns => ?_
  obtain ⟨ms, _, hms'⟩ := TendstoInMeasure.exists_seq_tendsto_ae fun ε hε => (hfg ε hε).comp hns
  exact ⟨ms,
    tendsto_Lp_of_tendsto_ae hp hp' (fun _ => hf _) hg
      (fun ε hε => -- `UnifIntegrable` on a subsequence
        let ⟨δ, hδ, hδ'⟩ := hui hε
        ⟨δ, hδ, fun i s hs hμs => hδ' _ s hs hμs⟩)
      (fun ε hε => -- `UnifTight` on a subsequence
        let ⟨s, hμs, hfε⟩ := hut hε
        ⟨s, hμs, fun i => hfε _⟩)
      hms'⟩

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hBi : IntervalIntegrable B volume a b
this✝ :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E},
    ContinuousOn f (Icc a b) →
      DifferentiableOn ℝ f (Ioo a b) →
        (∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t) → CompleteSpace E → ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
hE : ¬CompleteSpace E
g : ℝ → UniformSpace.Completion E := UniformSpace.Completion.coe' ∘ f
hg : g = UniformSpace.Completion.coe' ∘ f
hgc : ContinuousOn g (Icc a b)
hgd : DifferentiableOn ℝ g (Ioo a b)
t : ℝ
ht : t ∈ Ioo a b
this : HasFDerivAt UniformSpace.Completion.coe' UniformSpace.Completion.toComplL (f t)
⊢ deriv g t = ↑(deriv f t)

Tactic:
have hdft : HasDerivAt f (deriv f t) t := hfd.hasDerivAt <| Ioo_mem_nhds ht.1 ht.2

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hBi : IntervalIntegrable B volume a b
this✝ :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E},
    ContinuousOn f (Icc a b) →
      DifferentiableOn ℝ f (Ioo a b) →
        (∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t) → CompleteSpace E → ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
hE : ¬CompleteSpace E
g : ℝ → UniformSpace.Completion E := UniformSpace.Completion.coe' ∘ f
hg : g = UniformSpace.Completion.coe' ∘ f
hgc : ContinuousOn g (Icc a b)
hgd : DifferentiableOn ℝ g (Ioo a b)
t : ℝ
ht : t ∈ Ioo a b
this : HasFDerivAt UniformSpace.Completion.coe' UniformSpace.Completion.toComplL (f t)
hdft : HasDerivAt f (deriv f t) t
⊢ deriv g t = ↑(deriv f t)
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 (-ω) γ
⊢ CurveIntegrable ω γ

Tactic:
by simpa using h.neg

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

Goal state before:
pp: case pos
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : a = b
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ

pp: case neg
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
· subst h
    exact ⟨a, by simp, by simp⟩

Goal state after:
case neg
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: case h₂
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
⊢ CurveIntegrable (fun x ↦ ω a) (Path.segment a b)

Tactic:
· rw [curveIntegrable_segment]
    exact intervalIntegrable_const

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)
⊢ trapezoidal_integral f N a (a + ↑N * h) - ∑ x ∈ Finset.range N, ∫ (x : ℝ) in a + ↑x * h..a + ↑(x + 1) * h, f x =
    trapezoidal_integral f N a (a + ↑N * h) - ∫ (x : ℝ) in a..a + ↑N * h, f x

Tactic:
sum_integral_adjacent_intervals

Goal state after:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
h_f_int : IntervalIntegrable f volume a (a + ↑N * h)
⊢ trapezoidal_integral f N a (a + ↑N * h) - ∫ (x : ℝ) in a + ↑0 * h..a + ↑N * h, f x =
    trapezoidal_integral f N a (a + ↑N * h) - ∫ (x : ℝ) in a..a + ↑N * h, f x

f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
h_f_int : IntervalIntegrable f volume a (a + ↑N * h)
⊢ ∀ k < N, IntervalIntegrable f volume (a + ↑k * h) (a + ↑(k + 1) * h)
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: case h.refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : Disjoint s₀ s₁
hst : s₀ ⊆ t ∧ s₁ ⊆ t
so : Fin 2 → Set X := fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
hsot : t ⊆ ⋃ j, so j
f : Fin 2 → C(X, ℝ)
f_supp_in_so : ∀ (i : Fin 2), tsupport ⇑(f i) ⊆ so i
sum_f_one_on_t : EqOn (∑ i, ⇑(f i)) 1 t
f_in_icc : ∀ (i : Fin 2) (x : X), (f i) x ∈ Icc 0 1
f_hcs : ∀ (i : Fin 2), HasCompactSupport ⇑(f i)
sum_one_x : ∀ x ∈ t, (f 0) x + (f 1) x = 1
x : X
hx : x ∈ s₁
this : (f 1) x = 0
⊢ (f 0) x = (f 0) x + 0

Tactic:
exact Eq.symm (AddMonoid.add_zero ((f 0) x))

Goal state after:
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range ⇑f ⊆ Ioo a (a + ↑N * ε)
b : ℝ := a + ↑N * ε
y : Fin N → ℝ := fun n ↦ a + ε * (↑↑n + 1)
n m : Fin N
h : n < m
⊢ y n + ε ≤ a + ε * ↑↑m + ε

Tactic:
exact add_le_add_three (by rfl) ((mul_le_mul_iff_of_pos_left hε).mpr (by norm_cast)) (by rfl)

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: α : Type u
s : Set (Set α)
i : Ordinal.{v}
this : ∀ i ≤ ω_ 1, #↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
⊢ #↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀

Tactic:
by
    obtain hi | hi := le_or_gt i ω₁
    · exact this i hi
    · rw [generateMeasurableRec_of_omega_one_le s hi.le]
      exact this _ le_rfl

Goal state after:
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ
ε : ℝ
hε : 0 < ε
E : Set X
μ : Content X
hμ : μ.outerMeasure E ≠ ∞
hμ' : MeasurableSet E
c : ℝ
hfE : ∀ x ∈ E, f x < c
hε' : ε.toNNReal ≠ 0
V₁ : Opens X
hV₁ : E ⊆ ↑V₁ ∧ μ.outerMeasure ↑V₁ ≤ μ.outerMeasure E + ↑ε.toNNReal
V₂ : Opens X := { carrier := ⇑f ⁻¹' Iio c, is_open' := ⋯ }
⊢ μ.measure ↑(V₁ ⊓ V₂) ≤ μ.measure ↑V₁

Tactic:
by simp [measure_mono]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion

Goal state before:
pp: μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
n : ℕ
hint : MemLp id (↑n) μ
t : ℝ
⊢ taylorWithinEval (charFun μ) n univ 0 t = ∑ k ∈ Finset.range (n + 1), (↑k !)⁻¹ * (↑t * I) ^ k * ↑(∫ (x : ℝ), x ^ k ∂μ)

Tactic:
simp_rw [taylor_within_apply, sub_zero, RCLike.real_smul_eq_coe_mul]
  refine Finset.sum_congr rfl fun k hkn ↦ ?_
  push_cast
  have hint' : MemLp id k μ := hint.mono_exponent (by simp_all)
  simp [iteratedDeriv_charFun_zero hint', mul_pow, mul_comm, mul_assoc, mul_left_comm]

Goal state after:
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
r t : E
⊢ charFun (Measure.map (fun x ↦ r + x) μ) t = charFun μ t * cexp (↑⟪r, t⟫ * I)

Tactic:
by
  simp_rw [add_comm r]
  exact charFun_map_add_const _ _

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

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyRegularSpace Y
f : X → Y
hf : IsInducing f
x : X
K : Set X
hK : IsClosed[inst✝²] K
hxK : x ∉ K
⊢ ∃ f, Continuous[inst✝², _] f ∧ f x = 0 ∧ EqOn f 1 K

Tactic:
by
    rw [hf.isClosed_iff] at hK
    obtain ⟨K, hK, rfl⟩ := hK
    rw [mem_preimage] at hxK
    obtain ⟨g, hcf, egfx, hgK⟩ := CompletelyRegularSpace.completely_regular _ _ hK hxK
    refine ⟨g ∘ f, hcf.comp hf.continuous, egfx, ?_⟩
    conv => arg 2; equals (1 : Y → ↥I) ∘ f => rfl
    exact hgK.comp_right <| mapsTo_preimage _ _

Goal state after: