mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case inr
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (a ^ 1 + b ^ 1) ^ (1 / 1) ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
rw [one_div_one, one_div] at h

Goal state after:
case inr
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (a ^ 1 + b ^ 1) ^ 1 ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case neg
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q)

Tactic:
let g := fun _ : α => (1 : ℝ≥0∞)

Goal state after:
case neg
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x ↦ 1
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
w z : ι → ℝ
hs : s.Nonempty
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 < z i
p_pos : 0 < ∏ i ∈ s, (z i)⁻¹ ^ w i
s_pos : 0 < ∑ i ∈ s, w i * (z i)⁻¹
this : (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ ≤ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹
p_pos₂ : 0 < (∏ i ∈ s, z i ^ w i)⁻¹
i : ι
hi : i ∈ s
⊢ 0 ≤ (z i ^ w i)⁻¹

Tactic:
positivity [hz i hi]

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

Goal state before:
pp: α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q) < ∞

Tactic:
rw [ENNReal.mul_lt_top_iff]
      refine Or.inl ⟨hfq_lt_top, ENNReal.rpow_lt_top_of_nonneg ?_ (by finiteness)⟩
      rwa [le_sub_comm, sub_zero, one_div, one_div, inv_le_inv₀ hq_pos hp_pos]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hz : ∀ i ∈ s, 0 < z i
n : ℝ := ∑ i ∈ s, w i
hw' : 0 < n
this : (∑ i ∈ s, w i / n / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ (w i / n)
i : ι
hi : i ∈ s
⊢ 0 ≤ z i ^ w i

Tactic:
positivity [hz i hi]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : SeminormedAddGroup E
ι : Type u_3
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → E
p : ℝ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
⊢ eLpNorm' f_lim p μ = (∫⁻ (a : α), liminf (fun x ↦ ‖f x a‖ₑ ^ p) atTop ∂μ) ^ (1 / p)

Tactic:
suffices h_no_pow : (∫⁻ a, ‖f_lim a‖ₑ ^ p ∂μ) = ∫⁻ a, atTop.liminf fun m => ‖f m a‖ₑ ^ p ∂μ by
    rw [eLpNorm'_eq_lintegral_enorm, h_no_pow]
  refine lintegral_congr_ae (h_lim.mono fun a ha => ?_)
  dsimp only
  rw [Tendsto.liminf_eq]
  refine (ENNReal.continuous_rpow_const.tendsto ‖f_lim a‖₊).comp ?_
  exact (continuous_enorm.tendsto (f_lim a)).comp ha

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case pos
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) = 0 ∨ (∑ i ∈ s, g i ^ q) ^ (1 / q) = 0
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Tactic:
replace H : (∀ i ∈ s, f i = 0) ∨ ∀ i ∈ s, g i = 0 := by
      simpa [ENNReal.rpow_eq_zero_iff, hpq.pos, hpq.symm.pos, asymm hpq.pos, asymm hpq.symm.pos,
        sum_eq_zero_iff_of_nonneg] using H

Goal state after:
case pos
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∀ i ∈ s, f i = 0) ∨ ∀ i ∈ s, g i = 0
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
⊢ hg.compLp g0 0 = 0

Tactic:
rw [Lp.eq_zero_iff_ae_eq_zero]

Goal state after:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
⊢ ↑↑(hg.compLp g0 0) =ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
h : (∫⁻ (a : α), (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
h_tsum_lt_top : (∑' (i : ℕ), B i) ^ p < ∞
⊢ ∫⁻ (a : α), (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p

Tactic:
rwa [one_div, ← ENNReal.le_rpow_inv_iff (by simp [hp_pos] : 0 < p⁻¹), inv_inv] at h

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : NormedAddCommGroup E
l : Filter ι
hp_ne_zero : p ≠ 0
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hfg : Tendsto (fun n ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
⊢ TendstoInMeasure μ f l g

Tactic:
by_cases hp_ne_top : p = ∞

Goal state after:
case pos
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : NormedAddCommGroup E
l : Filter ι
hp_ne_zero : p ≠ 0
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hfg : Tendsto (fun n ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
hp_ne_top : p = ∞
⊢ TendstoInMeasure μ f l g

case neg
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : NormedAddCommGroup E
l : Filter ι
hp_ne_zero : p ≠ 0
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hfg : Tendsto (fun n ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
hp_ne_top : ¬p = ∞
⊢ TendstoInMeasure μ f l g
Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
⊢ Absorbs 𝕜 V (⇑f '' s)

Tactic:
else

Goal state after:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
⊢ Absorbs 𝕜 V (⇑f '' s)
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
⊢ (fun t ↦ (↑x + t)⁻¹ʳ - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =O[𝓝 0] fun t ↦ ‖t‖ ^ 2

Tactic:
by
  convert! inverse_add_norm_diff_nth_order x 2 using 2
  simp only [sum_range_succ, sum_range_zero, zero_add, pow_zero, pow_one, add_mul, one_mul,
    ← sub_sub, neg_mul, sub_neg_eq_add]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: case inr
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝³ : RingHomInvPair σ₁₂ σ₂₁
inst✝² : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomIsometric σ₂₁
inst✝ : RingHomIsometric σ₁₂
e : E ≃SL[σ₁₂] F
_i : Nontrivial E
⊢ Subsingleton E ∨ 0 < ‖↑e.symm‖

Tactic:
right
    exact e.norm_symm_pos

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : Module 𝕜 F
f : E → F
hf : IsBoundedLinearMap 𝕜 f
⊢ ∃ M, 0 < M ∧ ∀ (x : E), ‖-f x‖ ≤ M * ‖x‖

Tactic:
simpa using hf.2

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
ι : Type u_9
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁴ : RingHomIsometric σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
tfae_3_to_2 : UniformEquicontinuous (DFunLike.coe ∘ f) → Equicontinuous (DFunLike.coe ∘ f)
tfae_2_to_1 : Equicontinuous (DFunLike.coe ∘ f) → EquicontinuousAt (DFunLike.coe ∘ f) 0
tfae_4_iff_5 : (∃ C, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖) ↔ ∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖
tfae_5_iff_7 : (∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖) ↔ ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
tfae_7_iff_8 : (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (Set.range fun x ↦ ‖f x‖)
tfae_6_iff_8 : (∃ C, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (Set.range fun x ↦ ‖f x‖)
tfae_8_iff_9 : BddAbove (Set.range fun x ↦ ‖f x‖) ↔ ⨆ i, ↑‖f i‖₊ < ⊤
⊢ (∀ (i : Fin 1),
      ∃ p,
        Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑p ∧
          ∀ (k : ι), (normSeminorm 𝕜₂ F).comp ↑(f k) ≤ p) ↔
    ∃ C, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖

Tactic:
forall_const

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
ι : Type u_9
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁴ : RingHomIsometric σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
tfae_3_to_2 : UniformEquicontinuous (DFunLike.coe ∘ f) → Equicontinuous (DFunLike.coe ∘ f)
tfae_2_to_1 : Equicontinuous (DFunLike.coe ∘ f) → EquicontinuousAt (DFunLike.coe ∘ f) 0
tfae_4_iff_5 : (∃ C, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖) ↔ ∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖
tfae_5_iff_7 : (∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖) ↔ ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
tfae_7_iff_8 : (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (Set.range fun x ↦ ‖f x‖)
tfae_6_iff_8 : (∃ C, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (Set.range fun x ↦ ‖f x‖)
tfae_8_iff_9 : BddAbove (Set.range fun x ↦ ‖f x‖) ↔ ⨆ i, ↑‖f i‖₊ < ⊤
⊢ (∃ p,
      Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑p ∧
        ∀ (k : ι), (normSeminorm 𝕜₂ F).comp ↑(f k) ≤ p) ↔
    ∃ C, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖
Module: Mathlib.Order.Filter.IndicatorFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : One β
s : ι → Set α
hs : Antitone s
f : α → β
a : α
⊢ (fun i ↦ (s i).mulIndicator f a) =ᶠ[atTop] fun x ↦ (⋂ i, s i).mulIndicator f a

Tactic:
classical exact hs.piecewise_eventually_eq_iInter f 1 a

Goal state after:
Module: Mathlib.Order.Filter.IndicatorFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s✝ t : Set α
h : s✝.mulIndicator f =ᶠ[l] t.mulIndicator f
s : Set α
⊢ Function.mulSupport (s.mulIndicator f) =ᶠ[l] s

Tactic:
by
    rw [mulSupport_mulIndicator]
    exact (hf.mono fun x hx ↦ and_iff_left hx).set_eq

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
h : Integrable f μ
⊢ Integrable f ((μ univ)⁻¹ • μ)

Tactic:
by
  rcases eq_or_ne μ 0 with (rfl | hne)
  · rwa [smul_zero]
  · apply h.smul_measure
    simpa

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s t : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
ht : MeasurableSet t
hts : t ⊆ s
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ f '' s

Tactic:
filter_upwards [ae_restrict_mem ht] with a ha using image_mono hts (mem_image_of_mem f ha)

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
⊢ ‖f m‖ ≤ ‖f‖ * ∏ a, ‖m a‖

Tactic:
exact f.le_opNorm m

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

Goal state before:
pp: X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ ν : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hf : LocallyIntegrableOn f s μ
h : ν.restrict s ≤ μ.restrict s
⊢ LocallyIntegrableOn f s ν

Tactic:
by
  intro x hx
  obtain ⟨t, ht, hf⟩ := hf x hx
  obtain ⟨u, hu, hxu, hut⟩ := mem_nhdsWithin.mp ht
  refine ⟨u ∩ s, inter_mem (mem_nhdsWithin.mpr ⟨u, hu, hxu, inter_subset_left⟩) self_mem_nhdsWithin,
    ?_⟩
  refine hf.mono_set hut |>.mono_measure' ?_
  simp_rw [← restrict_restrict hu.measurableSet]
  gcongr

Goal state after:
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
Eᵤ : Type u_6
inst✝⁵ : AddCommGroup Eᵤ
inst✝⁴ : Module 𝕜 Eᵤ
inst✝³ : UniformSpace Eᵤ
inst✝² : T2Space Eᵤ
inst✝¹ : IsUniformAddGroup Eᵤ
inst✝ : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : U ∈ 𝓝 0
hU_tb : TotallyBounded U
⊢ FiniteDimensional 𝕜 Eᵤ

Tactic:
by
  obtain ⟨c, hc0, hc1⟩ : ∃ c : 𝕜, 0 < ‖c‖ ∧ ‖c‖ < 1 := NormedField.exists_norm_lt 𝕜 zero_lt_one
  have hc_ne : c ≠ 0 := norm_pos_iff.mp hc0
  obtain ⟨F, hF_finite, hF_cover⟩ := totallyBounded_iff_subset_finite_iUnion_nhds_zero.mp hU_tb
    (c • U) ((set_smul_mem_nhds_zero_iff hc_ne).mpr hU_nhds)
  let M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
  let : FiniteDimensional 𝕜 M := Finite.span_of_finite 𝕜 hF_finite
  have h_cover : U ⊆ M + c • U := fun x hx ↦ by
    obtain ⟨f, hf, y, hy, rfl⟩ := Set.mem_iUnion₂.mp <| hF_cover hx
    exact ⟨f, Submodule.subset_span hf, y, hy, rfl⟩
  have h_ind (n : ℕ) : U ⊆ M + c ^ n • U := by
    induction n with
    | zero => simpa using! fun x hx ↦ ⟨0, M.zero_mem, x, hx, zero_add x⟩
    | succ n ih =>
      calc
        U ⊆ M + c ^ n • U := ih
        _ ⊆ M + c ^ n • (M + c • U) := by gcongr
        _ ⊆ M + c ^ (n + 1) • U := by
          rw [smul_add, smul_smul, pow_succ, ← add_assoc]
          congr!
          lift c to 𝕜ˣ using isUnit_iff_ne_zero.mpr hc_ne
          simp [← Units.val_pow_eq_pow_val, ← Units.smul_def]
  have h_small : Tendsto (fun n ↦ c ^ n • U) atTop (𝓝 0).smallSets :=
    (TotallyBounded.isVonNBounded 𝕜 hU_tb).tendsto_smallSets_nhds.comp
    (tendsto_pow_atTop_nhds_zero_of_norm_lt_one hc1)
  have hU_sub_M : U ⊆ M := by
    intro x hx
    choose m hm u hu h_eq using fun n ↦ h_ind n hx
    have hu_tendsto : Tendsto u atTop (𝓝 0) := by
      intro W hW
      exact (tendsto_smallSets_iff.mp h_small W hW).mono fun n hn ↦ hn (hu n)
    have hm_tendsto : Tendsto m atTop (𝓝 x) := by
      simpa [show m = fun n ↦ x - u n by grind] using! tendsto_const_nhds.sub hu_tendsto
    exact M.closed_of_finiteDimensional.mem_of_tendsto hm_tendsto (Eventually.of_forall hm)
  have hM_top : M = ⊤ := absorbent_nhds_zero (𝕜 := 𝕜) hU_nhds |>.mono hU_sub_M |>.submodule_eq_top
  exact FiniteDimensional.of_surjective M.subtype fun x ↦ ⟨⟨x, by simp [hM_top]⟩, rfl⟩

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

Goal state before:
pp: case hi
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
fmeas : Measurable f
hf : Integrable f μ
⊢ HasFiniteIntegral (fun x ↦ f x - 0) μ

Tactic:
simpa using hf.2

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

Goal state before:
pp: case pos
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞
hp0 : ¬p = 0
hp_top : p = ∞
⊢ MemLp (⇑f) p μ

Tactic:
rw [hp_top]; exact memLp_top f μ

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹⁷ : AddCommGroup E
inst✝¹⁶ : UniformSpace E
inst✝¹⁵ : IsUniformAddGroup E
inst✝¹⁴ : AddCommGroup F
inst✝¹³ : UniformSpace F
inst✝¹² : IsUniformAddGroup F
inst✝¹¹ : T0Space F
inst✝¹⁰ : AddCommMonoid Eₗ
inst✝⁹ : UniformSpace Eₗ
inst✝⁸ : ContinuousAdd Eₗ
inst✝⁷ : Semiring 𝕜
inst✝⁶ : Semiring 𝕜₂
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : Module 𝕜 Eₗ
inst✝² : ContinuousConstSMul 𝕜 Eₗ
inst✝¹ : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f g : E →SL[σ₁₂] F
inst✝ : CompleteSpace F
e : E →L[𝕜] Eₗ
h : DenseRange ⇑e ∧ IsUniformInducing ⇑e
cont : Continuous (⋯.extend ⇑f)
eq : ∀ (b : E), ⋯.extend (⇑f) (e b) = f b
k : 𝕜
⊢ ∀ (x : Eₗ), ⋯.extend (⇑f) (k • x) = σ₁₂ k • ⋯.extend (⇑f) x

Tactic:
refine fun b => h.1.induction_on b ?_ ?_

Goal state after:
case refine_1
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹⁷ : AddCommGroup E
inst✝¹⁶ : UniformSpace E
inst✝¹⁵ : IsUniformAddGroup E
inst✝¹⁴ : AddCommGroup F
inst✝¹³ : UniformSpace F
inst✝¹² : IsUniformAddGroup F
inst✝¹¹ : T0Space F
inst✝¹⁰ : AddCommMonoid Eₗ
inst✝⁹ : UniformSpace Eₗ
inst✝⁸ : ContinuousAdd Eₗ
inst✝⁷ : Semiring 𝕜
inst✝⁶ : Semiring 𝕜₂
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : Module 𝕜 Eₗ
inst✝² : ContinuousConstSMul 𝕜 Eₗ
inst✝¹ : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f g : E →SL[σ₁₂] F
inst✝ : CompleteSpace F
e : E →L[𝕜] Eₗ
h : DenseRange ⇑e ∧ IsUniformInducing ⇑e
cont : Continuous (⋯.extend ⇑f)
eq : ∀ (b : E), ⋯.extend (⇑f) (e b) = f b
k : 𝕜
b : Eₗ
⊢ IsClosed {b | ⋯.extend (⇑f) (k • b) = σ₁₂ k • ⋯.extend (⇑f) b}

case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹⁷ : AddCommGroup E
inst✝¹⁶ : UniformSpace E
inst✝¹⁵ : IsUniformAddGroup E
inst✝¹⁴ : AddCommGroup F
inst✝¹³ : UniformSpace F
inst✝¹² : IsUniformAddGroup F
inst✝¹¹ : T0Space F
inst✝¹⁰ : AddCommMonoid Eₗ
inst✝⁹ : UniformSpace Eₗ
inst✝⁸ : ContinuousAdd Eₗ
inst✝⁷ : Semiring 𝕜
inst✝⁶ : Semiring 𝕜₂
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : Module 𝕜 Eₗ
inst✝² : ContinuousConstSMul 𝕜 Eₗ
inst✝¹ : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f g : E →SL[σ₁₂] F
inst✝ : CompleteSpace F
e : E →L[𝕜] Eₗ
h : DenseRange ⇑e ∧ IsUniformInducing ⇑e
cont : Continuous (⋯.extend ⇑f)
eq : ∀ (b : E), ⋯.extend (⇑f) (e b) = f b
k : 𝕜
b : Eₗ
⊢ ∀ (a : E), ⋯.extend (⇑f) (k • e a) = σ₁₂ k • ⋯.extend (⇑f) (e a)
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
y : F
⊢ integral μ (const α y) = μ.real Set.univ • y

Tactic:
classical
  calc
    (const α y).integral μ = ∑ z ∈ {y}, μ.real (const α y ⁻¹' {z}) • z :=
      integral_eq_sum_of_subset <| (filter_subset _ _).trans (range_const_subset _ _)
    _ = μ.real univ • y := by simp [Set.preimage]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
f : α → E
hf : Integrable f μ
⊢ ∫ (a : α), f a ∂μ = L1.integral (Integrable.toL1 f hf)

Tactic:
by
  simp [integral, hE, hf]

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

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
R : Type u_6
inst✝³ : NormedRing R
inst✝² : Module R G
inst✝¹ : IsBoundedSMul R G
inst✝ : SMulCommClass ℝ R G
c : R
f : α → G
hf : Integrable f μ
⊢ ∫ (a : α), c • f a ∂μ = c • ∫ (a : α), f a ∂μ

Tactic:
by_cases hG : CompleteSpace G
  · simpa only [integral, hG, hf, hf.fun_smul c] using! L1.integral_smul c (toL1 f hf)
  · simp [integral, hG]

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

Goal state before:
pp: α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * μ.real s
f : α →ₛ F
⊢ ∑ x ∈ f.range, C * μ.real (⇑f ⁻¹' {x}) * ‖x‖ ≤ C * ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) * ‖x‖

Tactic:
simp_rw [mul_sum, ← mul_assoc]; rfl

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ‖T s‖ ≤ C * μ.real s
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ ∑ x ∈ f.range, C * μ.real (⇑f ⁻¹' {x}) * ‖x‖ ≤ C * ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) * ‖x‖

Tactic:
simp_rw [mul_sum, ← mul_assoc]; rfl

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

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
this : ((fun x ↦ a x • u x) - fun x ↦ b x • v x) =ᶠ[l] fun x ↦ b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : IsBigOWith C l u v
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖

Tactic:
IsBigOWith

Goal state after:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
this : ((fun x ↦ a x • u x) - fun x ↦ b x • v x) =ᶠ[l] fun x ↦ b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∫ (x : α), |f x| ∂μ = 2 * ∫ (x : α), max (f x) 0 ∂μ - ∫ (x : α), f x ∂μ

Tactic:
have h_eq : ∀ x, |f x| = 2 * max (f x) 0 - f x := by grind

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
h_eq : ∀ (x : α), |f x| = 2 * max (f x) 0 - f x
⊢ ∫ (x : α), |f x| ∂μ = 2 * ∫ (x : α), max (f x) 0 ∂μ - ∫ (x : α), f x ∂μ