mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ μ Set.univ ≠ ∞

Tactic:
by finiteness

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 : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNormEssSup f μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : q = ∞
⊢ μ Set.univ ≠ ∞

Tactic:
by finiteness

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a ≠ ∞ ∧ b ≠ ∞
⊢ ↑(a.toNNReal * b.toNNReal) ≤ ↑(a.toNNReal ^ p) / ENNReal.ofReal p + ↑b.toNNReal ^ q / ENNReal.ofReal q

Tactic:
← coe_rpow_of_nonneg _ hpq.symm.nonneg,

Goal state after:
case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a ≠ ∞ ∧ b ≠ ∞
⊢ ↑(a.toNNReal * b.toNNReal) ≤ ↑(a.toNNReal ^ p) / ENNReal.ofReal p + ↑(b.toNNReal ^ q) / ENNReal.ofReal q
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h0 : a ≠ 0 ∧ b ≠ 0
h : a ≠ ∞ ∧ b ≠ ∞
⊢ ↑(a.toNNReal * b.toNNReal) = ↑(a.toNNReal ^ p) / ENNReal.ofReal p + ↑b.toNNReal ^ q / ENNReal.ofReal q ↔
    ↑a.toNNReal = ∞ ∧ ↑b.toNNReal ≠ 0 ∨ ↑a.toNNReal ≠ 0 ∧ ↑b.toNNReal = ∞ ∨ ↑(a.toNNReal ^ p) = ↑b.toNNReal ^ q

Tactic:
← coe_rpow_of_nonneg _ hpq.symm.nonneg,

Goal state after:
case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h0 : a ≠ 0 ∧ b ≠ 0
h : a ≠ ∞ ∧ b ≠ ∞
⊢ ↑(a.toNNReal * b.toNNReal) = ↑(a.toNNReal ^ p) / ENNReal.ofReal p + ↑(b.toNNReal ^ q) / ENNReal.ofReal q ↔
    ↑a.toNNReal = ∞ ∧ ↑b.toNNReal ≠ 0 ∨ ↑a.toNNReal ≠ 0 ∧ ↑b.toNNReal = ∞ ∨ ↑(a.toNNReal ^ p) = ↑(b.toNNReal ^ q)
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
h :
  1 ≤
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
      ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ ∞

Tactic:
by finiteness

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:

Tactic:
_ = ∑ i ∈ s, w i ^ (1 - p⁻¹) * (w i ^ p⁻¹ * f i) := ?_
    _ ≤ (∑ i ∈ s, (w i ^ (1 - p⁻¹)) ^ (1 - p⁻¹)⁻¹) ^ (1 / (1 - p⁻¹)⁻¹) *
          (∑ i ∈ s, (w i ^ p⁻¹ * f i) ^ p) ^ (1 / p) :=
        inner_le_Lp_mul_Lq _ _ _ (.symm <| Real.holderConjugate_iff.mpr ⟨hp, by simp⟩)
    _ = _ := ?_

Goal state after:
case inr.calc_1
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
⊢ ∑ i ∈ s, w i * f i = ∑ i ∈ s, w i ^ (1 - p⁻¹) * (w i ^ p⁻¹ * f i)

case inr.calc_2
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
⊢ (∑ i ∈ s, (w i ^ (1 - p⁻¹)) ^ (1 - p⁻¹)⁻¹) ^ (1 / (1 - p⁻¹)⁻¹) * (∑ i ∈ s, (w i ^ p⁻¹ * f i) ^ p) ^ (1 / p) =
    (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case cons
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x✝ : MeasurableSpace α
inst✝ : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : (∀ i ∈ s, MemLp (f i) (p i) μ) → MemLp (∏ i ∈ s, f i) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ
hf : ∀ i_1 ∈ cons i s hi, MemLp (f i_1) (p i_1) μ
⊢ MemLp (f i * ∏ x ∈ s, f x) (∑ i ∈ cons i s hi, (p i)⁻¹)⁻¹ μ

Tactic:
exact (ih <| forall_of_forall_cons hf).mul (hf i <| mem_cons_self ..) (hpqr := ⟨by simp⟩)

Goal state after:
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
c : ℝ≥0
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ c * ‖↑↑g x‖₊
this : eLpNorm (↑↑f) p μ ≤ c • eLpNorm (↑↑g) p μ
⊢ eLpNorm (↑↑g) p μ ≠ ∞

Tactic:
by finiteness

Goal state after:
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
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ‖↑↑g x‖
⊢ eLpNorm (↑↑g) p μ ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
c : 𝕜
f : ↥(Lp E p μ)
⊢ ‖c‖ₑ * eLpNorm (↑↑f) p μ < ∞

Tactic:
by finiteness

Goal state after:
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
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
h_nnnorm_nonneg :
  (fun a ↦ ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p) = fun a ↦
    (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p
⊢ (∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i

Tactic:
rwa [h_nnnorm_nonneg] at hn

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
⊢ (∑ i ∈ s, f i) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ i ∈ s, f i ^ p

Tactic:
rcases eq_or_lt_of_le hp with hp | hp
  · simp [← hp]
  let q : ℝ := p / (p - 1)
  have hpq : p.HolderConjugate q := .conjExponent hp
  have hp₁ : 1 / p * p = 1 := one_div_mul_cancel hpq.ne_zero
  have hq : 1 / q * p = p - 1 := by
    rw [← hpq.div_conj_eq_sub_one]
    ring
  simpa only [ENNReal.mul_rpow_of_nonneg _ _ hpq.nonneg, ← ENNReal.rpow_mul, hp₁, hq, coe_one,
    one_mul, one_rpow, rpow_one, Pi.one_apply, sum_const, Nat.smul_one_eq_cast] using
    ENNReal.rpow_le_rpow (inner_le_Lp_mul_Lq s 1 f hpq.symm) hpq.nonneg

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : Fact (1 ≤ p)
⊢ Continuous fun f ↦ negPart f

Tactic:
by
  unfold negPart
  exact continuous_posPart.comp continuous_neg

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
⊢ eLpNorm f_lim p μ < ∞

Tactic:
obtain ⟨N, h_tendsto_1⟩ := h_tendsto 1 zero_lt_one

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ 1
⊢ eLpNorm f_lim p μ < ∞
Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded

Goal state before:
pp: case inr
ι : 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
x✝ : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁷, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), t i ∈ 𝓝 0
hft : (↑I).pi t ⊆ ⇑f ⁻¹' V
c : ι → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : ∏ i ∈ I, c i ≠ 0
a : 𝕜
ha : a ∈ {y | ‖y‖ < ‖∏ i ∈ I, c i‖}
x : (i : ι) → E i
hx : x ∈ s
i₀ : ι
y : (i : ι) → E i := I.piecewise (fun i ↦ c i • x i) x
i : ι
hi : i ∈ ↑I
hne : i ≠ i₀
⊢ update y i₀ ((a / ∏ i ∈ I, c i) • y i₀) i ∈ t i

Tactic:
update_of_ne hne,

Goal state after:
case inr
ι : 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
x✝ : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁷, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), t i ∈ 𝓝 0
hft : (↑I).pi t ⊆ ⇑f ⁻¹' V
c : ι → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : ∏ i ∈ I, c i ≠ 0
a : 𝕜
ha : a ∈ {y | ‖y‖ < ‖∏ i ∈ I, c i‖}
x : (i : ι) → E i
hx : x ∈ s
i₀ : ι
y : (i : ι) → E i := I.piecewise (fun i ↦ c i • x i) x
i : ι
hi : i ∈ ↑I
hne : i ≠ i₀
⊢ y i ∈ t i
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsStrictMap f
⊢ Continuous[inst✝¹, inst✝] f

Tactic:
by
  rw [isStrictMap_iff_isQuotientMap_rangeFactorization] at hf
  exact continuous_rangeFactorization_iff.mp hf.continuous

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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
inst✝¹³ : NormedField 𝕜
inst✝¹² : (i : ι) → TopologicalSpace (E i)
inst✝¹¹ : (i : ι) → AddCommGroup (E i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
aux : (F →L[𝕜] G) →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G := ⋯
⊢ Filter.Tendsto (⇑aux) (𝓝 0) (𝓝 0)

Tactic:
rw [ContinuousLinearMap.hasBasis_nhds_zero.tendsto_iff <|
        ContinuousLinearMap.hasBasis_nhds_zero_of_basis <|
        ContinuousMultilinearMap.hasBasis_nhds_zero]

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
inst✝¹³ : NormedField 𝕜
inst✝¹² : (i : ι) → TopologicalSpace (E i)
inst✝¹¹ : (i : ι) → AddCommGroup (E i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
aux : (F →L[𝕜] G) →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  { toFun := fun g ↦ { toFun := g.compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ },
    map_add' := ⋯, map_smul' := ⋯ }
⊢ ∀ (ib : Set (ContinuousMultilinearMap 𝕜 E F) × Set ((i : ι) → E i) × Set G),
    IsVonNBounded 𝕜 ib.1 ∧ IsVonNBounded 𝕜 ib.2.1 ∧ ib.2.2 ∈ 𝓝 0 →
      ∃ ia,
        (IsVonNBounded 𝕜 ia.1 ∧ ia.2 ∈ 𝓝 0) ∧
          ∀ x ∈ {f | ∀ x ∈ ia.1, f x ∈ ia.2}, aux x ∈ {f | ∀ x ∈ ib.1, f x ∈ {f | MapsTo (⇑f) ib.2.1 ib.2.2}}
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : μ s ≠ ∞
⊢ (μ s).toReal = 0 ↔ μ s = 0

Tactic:
ENNReal.toReal_eq_zero_iff

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : μ s ≠ ∞
⊢ μ s = 0 ∨ μ s = ∞ ↔ μ s = 0
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
⊢ μ univ ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h₁ : μ s₁ ≠ ∞
h₂ : μ s₂ ≠ ∞
h : μ.real (s₁ ∪ s₂) = 0
⊢ μ (s₁ ∪ s₂) ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
h : μ s ≠ ∞
⊢ (μ (s ∩ t)).toReal + (μ (s \ t)).toReal = (μ s).toReal

Tactic:
rw [← ENNReal.toReal_add, measure_inter_add_sdiff _ ht]

Goal state after:
case ha
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
h : μ s ≠ ∞
⊢ μ (s ∩ t) ≠ ∞

case hb
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
h : μ s ≠ ∞
⊢ μ (s \ t) ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t u : Set α
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
hu : μ u < ∞
⊢ μ (s ∆ t) ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t u : Set α
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
hu : μ u < ∞
⊢ μ (t ∆ u) ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s).PairwiseDisjoint t
⊢ ∀ a ∈ s, μ (t a) ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s).PairwiseDisjoint t
⊢ μ univ ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (μ univ).toReal < ∑ i ∈ s, (μ (t i)).toReal
⊢ μ univ ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (μ univ).toReal < ∑ i ∈ s, (μ (t i)).toReal
⊢ ∀ a ∈ s, μ (t a) ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
⊢ μ (s ∆ t) ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
c : E
⊢ indicatorConstLp p ⋯ ⋯ c = 0

Tactic:
by
  simp only [indicatorConstLp, Set.indicator_empty', MemLp.toLp_zero]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s✝ : Set α
hs✝ : MeasurableSet s✝
hμs✝ : μ s✝ ≠ ∞
c✝ : E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
hst : Disjoint s t
c : E
⊢ μ (s ∪ t) ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: case pos
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this✝ : {ξ₀}ᶜ ∈ 𝓝 0
this : balancedCore 𝕜 {ξ₀}ᶜ ∈ 𝓝 0
ξ : 𝕜
hξ : ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ
hξ0 : ξ = 0
⊢ 0 ∈ Metric.closedBall 0 ε

Tactic:
exact Metric.mem_closedBall_self hε.le

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 ε
inst✝ : IsFiniteMeasure μ
f : α → ε
h : μ ≠ 0
⊢ μ univ ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_8
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
f : α → 𝕜
hf : MemLp f 1 μ
g : α → β
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x ↦ ‖g x‖ₑ) μ ≠ ∞
⊢ MemLp (fun x ↦ f x • g x) 1 μ

Tactic:
refine ⟨hf.1.smul g_aestronglyMeasurable, ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_8
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
f : α → 𝕜
hf : MemLp f 1 μ
g : α → β
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x ↦ ‖g x‖ₑ) μ ≠ ∞
⊢ eLpNorm (fun x ↦ f x • g x) 1 μ < ∞
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
a✝ : Nontrivial α
inhabited_h : Inhabited α
this : (s.piecewise f fun x ↦ f default) =ᵐ[μ.restrict s] f
t : Set β
ht : IsOpen[inst✝¹] t
u : Set α
u_open : IsOpen[inst✝⁴] u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ MeasurableSet ((s.piecewise f fun x ↦ f default) ⁻¹' t)

Tactic:
piecewise_preimage,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
a✝ : Nontrivial α
inhabited_h : Inhabited α
this : (s.piecewise f fun x ↦ f default) =ᵐ[μ.restrict s] f
t : Set β
ht : IsOpen[inst✝¹] t
u : Set α
u_open : IsOpen[inst✝⁴] u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ MeasurableSet (s.ite (f ⁻¹' t) ((fun x ↦ f default) ⁻¹' t))
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
⊢ ∀ (x : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))),
    ‖{ toFun := fun u ↦ MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯, map_add' := ⋯, map_smul' := ⋯ } x‖ = ‖x‖

Tactic:
by
    intro u
    simp only [eLpNorm, LinearMap.coe_mk, AddHom.coe_mk,
      one_ne_zero, ENNReal.one_ne_top, ENNReal.toReal_one, if_false, eLpNorm', ENNReal.rpow_one,
      _root_.div_one, Lp.norm_def]
    rw [lintegral_withDensity_eq_lintegral_mul_non_measurable _ f_meas.coe_nnreal_ennreal
        (Filter.Eventually.of_forall fun x => ENNReal.coe_lt_top)]
    congr 1
    apply lintegral_congr_ae
    filter_upwards [(memL1_smul_of_L1_withDensity f_meas u).coeFn_toLp] with x hx
    rw [hx]
    simp [NNReal.smul_def, enorm_smul]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f 1 μ
⊢ MemLp (fun x ↦ RCLike.re (f x)) 1 μ

Tactic:
exact hf.re

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

Goal state before:
pp: case pos
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁴ : PartialOrder α
inst✝³ : MeasurableSingletonClass α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : μ {b} ≠ ∞
hb' : ‖f b‖ₑ ≠ ∞
hab : a ≤ b
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ

Tactic:
rw [← Ico_union_right hab, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]

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✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
T : Set (Set X)
T_count : T.Countable
T_open : ∀ u ∈ T, IsOpen[inst✝³] u
sT : s ⊆ ⋃ u ∈ T, u
hT : ∀ u ∈ T, IntegrableOn f (u ∩ s) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
x : X
hx : x ∈ s
v : Set X
hv : v ∈ T
h'v : x ∈ v
⊢ v ∈ T'

Tactic:
exact subset_insert ∅ T hv

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

Goal state before:
pp: case pos
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
hs : IsClosed[inst✝³] s
hf : LocallyIntegrableOn f s μ
x : X
h : x ∈ s
t : Set X
ht_nhds : t ∈ 𝓝[s] x
ht_int : IntegrableOn f t μ
u : Set X
hu_o : IsOpen[inst✝³] u
hu_x : x ∈ u
hu_sub : u ∩ s ⊆ t
⊢ Integrable f (μ.restrict (u ∩ s))

Tactic:
exact ht_int.mono_set hu_sub

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
inst✝¹ : PseudoMetrizableSpace ε
inst✝ : SecondCountableTopology X
hf : LocallyIntegrable f μ
⊢ AEStronglyMeasurable f μ

Tactic:
by
  simpa only [restrict_univ] using (locallyIntegrableOn_univ.mpr hf).aestronglyMeasurable

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✝⁵ : Fintype ι
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : MultilinearMap 𝕜 E G
ε : ι → ℝ
C : ℝ
c : ι → 𝕜
hε : ∀ (i : ι), 0 < ε i
hc : ∀ (i : ι), 1 < ‖c i‖
hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖
m m✝ : (i : ι) → E i
i✝ : ι
h : ‖m✝ i✝‖ = 0
⊢ ‖0‖ = 0

Tactic:
norm_zero

Goal state after:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : Fintype ι
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : MultilinearMap 𝕜 E G
ε : ι → ℝ
C : ℝ
c : ι → 𝕜
hε : ∀ (i : ι), 0 < ε i
hc : ∀ (i : ι), 1 < ‖c i‖
hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖
m m✝ : (i : ι) → E i
i✝ : ι
h : ‖m✝ i✝‖ = 0
⊢ 0 = 0
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case neg
α : 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 = ∞
⊢ eLpNorm (⇑f) p μ < ∞

Tactic:
rw [eLpNorm_eq_eLpNorm' hp0 hp_top, f.eLpNorm'_eq]

Goal state after:
case neg
α : 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 = ∞
⊢ (∑ y ∈ f.range, ‖y‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {y})) ^ (1 / p.toReal) < ∞