mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
μ ν : Measure α
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : TopologicalSpace β
inst✝⁵ : TopologicalSpace γ
𝕜 : Type u_5
𝕜' : Type u_6
inst✝⁴ : SMul 𝕜 γ
inst✝³ : ContinuousConstSMul 𝕜 γ
inst✝² : SMul 𝕜' γ
inst✝¹ : ContinuousConstSMul 𝕜' γ
inst✝ : SMulCommClass 𝕜 𝕜' γ
a : 𝕜
b : 𝕜'
f✝ : α →ₘ[μ] γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ a • b • mk f hf = b • a • mk f hf

Tactic:
smul_mk,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
μ ν : Measure α
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : TopologicalSpace β
inst✝⁵ : TopologicalSpace γ
𝕜 : Type u_5
𝕜' : Type u_6
inst✝⁴ : SMul 𝕜 γ
inst✝³ : ContinuousConstSMul 𝕜 γ
inst✝² : SMul 𝕜' γ
inst✝¹ : ContinuousConstSMul 𝕜' γ
inst✝ : SMulCommClass 𝕜 𝕜' γ
a : 𝕜
b : 𝕜'
f✝ : α →ₘ[μ] γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ mk (a • b • f) ⋯ = mk (b • a • f) ⋯
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁹ : MeasurableSpace α
μ ν : Measure α
inst✝⁸ : TopologicalSpace δ
inst✝⁷ : TopologicalSpace β
inst✝⁶ : TopologicalSpace γ
𝕜 : Type u_5
𝕜' : Type u_6
inst✝⁵ : SMul 𝕜 γ
inst✝⁴ : ContinuousConstSMul 𝕜 γ
inst✝³ : SMul 𝕜' γ
inst✝² : ContinuousConstSMul 𝕜' γ
inst✝¹ : SMul 𝕜 𝕜'
inst✝ : IsScalarTower 𝕜 𝕜' γ
a : 𝕜
b : 𝕜'
f✝ : α →ₘ[μ] γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ (a • b) • mk f hf = a • b • mk f hf

Tactic:
smul_mk,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁹ : MeasurableSpace α
μ ν : Measure α
inst✝⁸ : TopologicalSpace δ
inst✝⁷ : TopologicalSpace β
inst✝⁶ : TopologicalSpace γ
𝕜 : Type u_5
𝕜' : Type u_6
inst✝⁵ : SMul 𝕜 γ
inst✝⁴ : ContinuousConstSMul 𝕜 γ
inst✝³ : SMul 𝕜' γ
inst✝² : ContinuousConstSMul 𝕜' γ
inst✝¹ : SMul 𝕜 𝕜'
inst✝ : IsScalarTower 𝕜 𝕜' γ
a : 𝕜
b : 𝕜'
f✝ : α →ₘ[μ] γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ mk ((a • b) • f) ⋯ = mk (a • b • f) ⋯
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁹ : MeasurableSpace α
μ ν : Measure α
inst✝⁸ : TopologicalSpace δ
inst✝⁷ : TopologicalSpace β
inst✝⁶ : TopologicalSpace γ
𝕜 : Type u_5
𝕜' : Type u_6
inst✝⁵ : SMul 𝕜 γ
inst✝⁴ : ContinuousConstSMul 𝕜 γ
inst✝³ : SMul 𝕜' γ
inst✝² : ContinuousConstSMul 𝕜' γ
inst✝¹ : SMul 𝕜ᵐᵒᵖ γ
inst✝ : IsCentralScalar 𝕜 γ
a : 𝕜
f✝ : α →ₘ[μ] γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ MulOpposite.op a • mk f hf = a • mk f hf

Tactic:
smul_mk,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁹ : MeasurableSpace α
μ ν : Measure α
inst✝⁸ : TopologicalSpace δ
inst✝⁷ : TopologicalSpace β
inst✝⁶ : TopologicalSpace γ
𝕜 : Type u_5
𝕜' : Type u_6
inst✝⁵ : SMul 𝕜 γ
inst✝⁴ : ContinuousConstSMul 𝕜 γ
inst✝³ : SMul 𝕜' γ
inst✝² : ContinuousConstSMul 𝕜' γ
inst✝¹ : SMul 𝕜ᵐᵒᵖ γ
inst✝ : IsCentralScalar 𝕜 γ
a : 𝕜
f✝ : α →ₘ[μ] γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ mk (MulOpposite.op a • f) ⋯ = mk (a • f) ⋯
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
γ : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace γ
inst✝¹ : CommMonoid γ
inst✝ : ContinuousMul γ
ι : Type u_5
s : Finset ι
f : ι → α →ₘ[μ] γ
⊢ ↑(∏ i ∈ s, f i) =ᵐ[μ] fun x ↦ ∏ i ∈ s, ↑(f i) x

Tactic:
grw [coeFn_finsetProd]
  filter_upwards with x using by simp

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

Goal state before:
pp: α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
f : α → ε'
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
⊢ ↑ε ≠ 0

Tactic:
by simp [hε]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
⊢ ↑ε ≠ 0

Tactic:
by simp [hε]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ (Measure.pi μ).restrict (univ.pi fun i ↦ s i) = Measure.pi fun i ↦ (μ i).restrict (s i)

Tactic:
refine (pi_eq fun _ h ↦ ?_).symm

Goal state after:
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s x✝ : (i : ι) → Set (α i)
h : ∀ (i : ι), MeasurableSet (x✝ i)
⊢ ((Measure.pi μ).restrict (univ.pi fun i ↦ s i)) (univ.pi x✝) = ∏ i, ((μ i).restrict (s i)) (x✝ i)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NullSingletonClass (μ i)
f g : (i : ι) → α i
⊢ (univ.pi fun i ↦ Ioc (f i) (g i)) =ᵐ[Measure.pi μ] Icc f g

Tactic:
rw [← pi_univ_Icc]; exact pi_Ioc_ae_eq_pi_Icc

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
e : ((i : ι) → X i) ≃ᵐ X default := MeasurableEquiv.piUnique X
s : Set ((i : ι) → X i)
⊢ (μ default).toOuterMeasure (eval default '' s) = (Measure.map (⇑e.symm) (μ default)) s

Tactic:
e.symm.map_apply,

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
e : ((i : ι) → X i) ≃ᵐ X default := MeasurableEquiv.piUnique X
s : Set ((i : ι) → X i)
⊢ (μ default).toOuterMeasure (eval default '' s) = (μ default) (⇑e.symm ⁻¹' s)
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inl
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 ≤ -1
hs' : -1 ≠ 0
⊢ 1 + p * -1 < 0

Tactic:
mul_neg_one,

Goal state after:
case inl
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 ≤ -1
hs' : -1 ≠ 0
⊢ 1 + -p < 0
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inl
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 ≤ -1
hs' : -1 ≠ 0
⊢ 0 < 1 + p * -1

Tactic:
mul_neg_one,

Goal state after:
case inl
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 ≤ -1
hs' : -1 ≠ 0
⊢ 0 < 1 + -p
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)

Tactic:
rcases lt_or_gt_of_ne hya with hya | hya
    · convert! hf.secant_mono_aux3 hx ha hxy hya using 1 <;> rw [← neg_div_neg_eq] <;> simp
    · convert! hf.slope_mono_adjacent hx hy hxa hya using 1
      rw [← neg_div_neg_eq]; simp

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
c : ℝ≥0∞
μ μ' : Measure α
h : μ' ≤ c • μ
f : α → ε
p : ℝ≥0∞
⊢ eLpNorm f p μ' ≤ c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
by
  grw [h, eLpNorm_smul_measure_le]

Goal state after:
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 μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ ∫⁻ (a : α), f a ^ p * (ENNReal.ofReal p)⁻¹ ∂μ + ∫⁻ (a : α), g a ^ q * (ENNReal.ofReal q)⁻¹ ∂μ = 1

pp: case hf
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ AEMeasurable (fun a ↦ f a ^ p * (ENNReal.ofReal p)⁻¹) μ

Tactic:
· rw [lintegral_mul_const'' _ (hf.pow_const p), lintegral_mul_const', hf_norm, hg_norm,
          one_mul, one_mul, hpq.inv_add_inv_ennreal]
        simp [hpq.symm.pos]

Goal state after:
case hf
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ AEMeasurable (fun a ↦ f a ^ p * (ENNReal.ofReal p)⁻¹) μ
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case neg
p : ℝ
b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
hb_top : b ≠ ∞
a : ℝ≥0
h_top : ¬↑a + b = ∞
⊢ ↑a ^ p + b ^ p ≤ (↑a + b) ^ p

Tactic:
lift b to ℝ≥0 using hb_top

Goal state after:
case neg
p : ℝ
hp1 : 1 ≤ p
hp_pos : 0 < p
a b : ℝ≥0
h_top : ¬↑a + ↑b = ∞
⊢ ↑a ^ p + ↑b ^ p ≤ (↑a + ↑b) ^ p
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 : ℝ
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
h_rw : ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ = ∫⁻ (a : α), (‖f a‖ₑ * g a) ^ p ∂μ
r : ℝ := p * q / (q - p)
hpqr : 1 / p = 1 / q + 1 / r
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r) =
    (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) * μ Set.univ ^ (1 / q + 1 / r - 1 / q)

Tactic:
simp [r, g]

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

Goal state before:
pp: α : Type u_2
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
p2 : ℝ := q / p
q2 : ℝ := p2.conjExponent
hp2q2 : p2.HolderConjugate q2
hpp2 : p * p2 = q
hpq2 : p * q2 = r
⊢ (∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / (p * p2)) * (∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / (q2 * p)) =
    (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)

Tactic:
mul_comm q2,

Goal state after:
α : Type u_2
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
p2 : ℝ := q / p
q2 : ℝ := p2.conjExponent
hp2q2 : p2.HolderConjugate q2
hpp2 : p * p2 = q
hpq2 : p * q2 = r
⊢ (∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / (p * p2)) * (∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / (p * q2)) =
    (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
⊢ ∑ i ∈ s, ?m.71 i ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) * (∑ i ∈ s, |g i| ^ q) ^ (1 / q)

Tactic:
by simpa using Lr_rpow_le_Lp_mul_Lq s f g hpq

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

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun i ↦ μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)

pp: case refine_2
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h : ∀ (ε : ℝ), 0 < ε → Tendsto (fun i ↦ μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
⊢ TendstoInMeasure μ f l g

Tactic:
· convert! h (ENNReal.ofReal ε) (ENNReal.ofReal_pos.mpr hε) with i a
    rw [edist_dist, ENNReal.ofReal_le_ofReal_iff (by positivity)]

Goal state after:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h : ∀ (ε : ℝ), 0 < ε → Tendsto (fun i ↦ μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
⊢ TendstoInMeasure μ f l g
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α✝ : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E✝ : Type u_4
F : Type u_5
m✝ : MeasurableSpace α✝
p✝ : ℝ≥0∞
μ✝ : Measure α✝
inst✝² : NormedAddCommGroup E✝
inst✝¹ : NormedAddCommGroup F
α : Type ?u.18
E : Type u_6
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₘ[μ] E
hf : f ∈ {f | eLpNorm (↑f) p μ < ∞}
⊢ -f ∈ {f | eLpNorm (↑f) p μ < ∞}

Tactic:
by rwa [Set.mem_ofPred_eq, eLpNorm_congr_ae (AEEqFun.coeFn_neg f), eLpNorm_neg]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜' E
inst✝¹ : IsBoundedSMul 𝕜 E
inst✝ : IsBoundedSMul 𝕜' E
c : 𝕜
f : α →ₘ[μ] E
hf : f ∈ (Lp E p μ).carrier
⊢ c • f ∈ (Lp E p μ).carrier

Tactic:
by simpa using const_smul_mem_Lp c ⟨f, hf⟩

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
⊢ eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ≠ ∞

Tactic:
rw [ENNReal.ofReal_toReal q_top, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
    mul_one]

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
⊢ eLpNorm f p μ ≠ ∞
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
⊢ eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ≠ ∞

Tactic:
rw [ENNReal.ofReal_toReal q_top, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
    mul_one]

Goal state after:
case neg
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
⊢ eLpNorm f p μ ≠ ∞
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: case h
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k ↦ {x | 2⁻¹ ^ k ≤ edist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
⊢ StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f (ns i) x) atTop (𝓝 (g x))

Tactic:
have hμs : μ s = 0 := by
    refine measure_limsup_atTop_eq_zero (ne_top_of_le_ne_top ?_ (ENNReal.tsum_le_tsum hμS_le))
    simpa only [ENNReal.tsum_geometric, ENNReal.one_sub_inv_two, inv_inv] using ENNReal.ofNat_ne_top

Goal state after:
case h
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k ↦ {x | 2⁻¹ ^ k ≤ edist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : μ s = 0
⊢ StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f (ns i) x) atTop (𝓝 (g x))
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
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
⊢ eLpNorm (f n - f_lim) p μ ≤ liminf (fun m_1 ↦ eLpNorm (f n - f m_1) p μ) atTop

Tactic:
refine eLpNorm_lim_le_liminf_eLpNorm (fun m => (hf n).sub (hf m)) (f n - f_lim) ?_

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n_1 ↦ (f n - f n_1) x) atTop (𝓝 ((f n - f_lim) x))
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: case left
α : 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 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
h_neg : f_lim - f N = -(f N - f_lim)
⊢ eLpNorm (f_lim - f N) p μ ≤ 1

Tactic:
h_neg,

Goal state after:
case left
α : 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 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
h_neg : f_lim - f N = -(f N - f_lim)
⊢ eLpNorm (-(f N - f_lim)) p μ ≤ 1
Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded

Goal state before:
pp: case inl
ι : 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
y : (i : ι) → E i := I.piecewise (fun i ↦ c i • x i) x
i : ι
hi : i ∈ ↑I
⊢ update y i ((a / ∏ i ∈ I, c i) • y i) i ∈ t i

Tactic:
update_self,

Goal state after:
case inl
ι : 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
y : (i : ι) → E i := I.piecewise (fun i ↦ c i • x i) x
i : ι
hi : i ∈ ↑I
⊢ (a / ∏ i ∈ I, c i) • y i ∈ t i
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
⊢ 0 < ‖↑e.symm‖

Tactic:
exact e.norm_symm_pos

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

Goal state before:
pp: case mpr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := ⋯
h_O : Continuous O
f' : E →L[𝕜] F
⊢ f' ∈ O ⁻¹' {x | IsUnit x} → f' ∈ range toContinuousLinearMap

Tactic:
rintro ⟨w, hw⟩
    use (unitsEquiv 𝕜 E w).trans e
    ext x
    simp [O, hw]

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
this : μ (s ∪ t) ≠ ∞
⊢ μ.real t + μ.real (s \ t) + μ.real (s ∩ t) = μ.real s + μ.real t

Tactic:
← measureReal_inter_add_sdiff₀ ht h₁

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
this : μ (s ∪ t) ≠ ∞
⊢ μ.real t + μ.real (s \ t) + μ.real (s ∩ t) = μ.real (s ∩ t) + μ.real (s \ t) + μ.real t
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsFiniteMeasure μ
h₁ : MeasurableSet s
⊢ μ.real sᶜ = μ.real univ - μ.real s

Tactic:
rw [compl_eq_univ_sdiff]

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsFiniteMeasure μ
h₁ : MeasurableSet s
⊢ μ.real (univ \ s) = μ.real univ - μ.real s
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
l l' : Filter α
⊢ IntegrableAtFilter f (l ⊔ l') μ ↔ IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ

Tactic:
by
  constructor
  · exact fun h => ⟨h.filter_mono le_sup_left, h.filter_mono le_sup_right⟩
  · exact fun ⟨⟨s, hsl, hs⟩, ⟨t, htl, ht⟩⟩ ↦ ⟨s ∪ t, union_mem_sup hsl htl, hs.union ht⟩

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

Goal state before:
pp: X : Type u_1
E : Type u_6
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
μ : Measure X
f : X → E
⊢ LocallyIntegrable (-f) μ ↔ LocallyIntegrable f μ

Tactic:
simp [← locallyIntegrableOn_univ]

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

Goal state before:
pp: X : Type u_1
E : Type u_6
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
f : X → E
c : 𝕜
⊢ LocallyIntegrable (c • f) μ ↔ c = 0 ∨ LocallyIntegrable f μ

Tactic:
simp [← locallyIntegrableOn_univ]

Goal state after: