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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
⊢ eLpNorm' (fun x ↦ b (f x) (g x)) r μ ≤ ↑c * eLpNorm' f p μ * eLpNorm' g q μ

Tactic:
calc
    eLpNorm' (fun x => b (f x) (g x)) r μ
      ≤ eLpNorm' (fun x ↦ (c : ℝ) • ‖f x‖ * ‖g x‖) r μ := by
      simp only [eLpNorm']
      gcongr ?_ ^ _
      refine lintegral_mono_ae <| h.mono fun a ha ↦ ?_
      gcongr
      simp only [enorm_eq_nnnorm, ENNReal.coe_le_coe]
      simpa using! ha
    _ ≤ c * eLpNorm' f p μ * eLpNorm' g q μ := by
      simp only [smul_mul_assoc, ← Pi.smul_def, eLpNorm'_const_smul _ hro_lt]
      rw [Real.enorm_eq_ofReal c.coe_nonneg, ENNReal.ofReal_coe_nnreal, mul_assoc]
      gcongr
      simpa only [eLpNorm', enorm_mul, enorm_norm] using!
        ENNReal.lintegral_Lp_mul_le_Lq_mul_Lr hro_lt hrp hpqr μ hf.enorm hg.enorm

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

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

Tactic:
by
  refine le_trans (sum_le_sum fun i _ ↦ ?_) (by simpa using Lr_rpow_le_Lp_mul_Lq s f g hpq)
  simp only [← abs_mul, le_abs_self]

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
g✝ : E → F
c✝ : ℝ≥0
inst✝ : NormedSpace ℝ E
ν : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
h : μ ≤ c • ν
f g : ↥(Lp E p ν)
⊢ MemLp.toLp ↑↑(f + g) ⋯ = MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯

Tactic:
ext
    grw [MemLp.coeFn_toLp, Lp.coeFn_add, MemLp.coeFn_toLp, MemLp.coeFn_toLp]
    have : μ ≪ ν := Measure.absolutelyContinuous_of_le_smul h
    apply this.ae_eq
    grw [Lp.coeFn_add]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
a✝ : α
⊢ ↑↑(posPart (-f)) a✝ = max (↑↑(-f) a✝) 0 → ↑↑(-f) a✝ = (-↑↑f) a✝ → ↑↑(posPart (-f)) a✝ = max (-↑↑f a✝) 0

Tactic:
h₁

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
a✝ : α
h₁ : ↑↑(posPart (-f)) a✝ = max (↑↑(-f) a✝) 0
⊢ ↑↑(-f) a✝ = (-↑↑f) a✝ → ↑↑(posPart (-f)) a✝ = max (-↑↑f a✝) 0
Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
a : α
b : β
h : (inl.trans f, inr.trans f).1 a = (inl.trans f, inr.trans f).2 b
⊢ False

Tactic:
simp only at h

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
a : α
b : β
h : (inl.trans f) a = (inr.trans f) b
⊢ False
Module: Mathlib.Data.Fintype.CardEmbedding

Goal state before:
pp: case refine_1
β : Type u_2
inst✝ : Fintype β
α₁ α₂ : Type u_1
h₂ : Fintype α₂
e : α₁ ≃ α₂
ih : ‖α₁ ↪ β‖ = ‖β‖.descFactorial ‖α₁‖
this : Fintype α₁ := ofEquiv α₂ e.symm
⊢ ‖α₂ ↪ β‖ = ‖β‖.descFactorial ‖α₂‖

Tactic:
rw [← card_congr (Equiv.embeddingCongr e (Equiv.refl β)), ih, card_congr e]

Goal state after:
Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
a : α ↪ γ
f : β ↪ γ
⊢ Disjoint (Set.range ⇑a) (Set.range ⇑f) ↔ ∀ (a_1 : β), f a_1 ∈ (Set.range ⇑a)ᶜ

Tactic:
rw [← Set.range_subset_iff, Set.subset_compl_iff_disjoint_right, disjoint_comm]

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
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))
⊢ Tendsto (fun n ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)

Tactic:
rw [ENNReal.tendsto_atTop_zero]

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, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
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
inst✝ : CompleteSpace E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
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
f_lim : α → E
h_f_lim_meas : StronglyMeasurable f_lim
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
h_tendsto' : Tendsto (fun n ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
h_ℒp_lim : MemLp f_lim p μ
⊢ ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)

Tactic:
exact ⟨f_lim, h_ℒp_lim, h_tendsto'⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
t : R
h : ‖t‖ < ‖↑x⁻¹‖⁻¹
a✝ : Nontrivial R
hpos : 0 < ‖↑x⁻¹‖
⊢ ‖-(↑x⁻¹ * t)‖ = ‖↑x⁻¹ * t‖

Tactic:
norm_neg

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
t : R
h : ‖t‖ < ‖↑x⁻¹‖⁻¹
a✝ : Nontrivial R
hpos : 0 < ‖↑x⁻¹‖
⊢ ‖↑x⁻¹ * t‖ = ‖↑x⁻¹ * t‖
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‖₊ < ⊤
⊢ UniformEquicontinuous (DFunLike.coe ∘ f) ↔ ∃ C, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖

Tactic:
refine ((norm_withSeminorms 𝕜₂ F).uniformEquicontinuous_iff_exists_continuous_seminorm _).trans
      ?_

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‖₊ < ⊤
⊢ (∀ (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‖
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: case refine_1
𝕜 : 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
g : F →L[𝕜] G
aux₁ : ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  { toFun := g.compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯ }
U : Set ((i : ι) → E i)
V : Set G
hU : IsVonNBounded 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
⊢ (U, ⇑g ⁻¹' V).2 ∈ 𝓝 0

Tactic:
exact (map_continuous g).tendsto 0 <| by simpa

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

Goal state before:
pp: α : Type u_1
ε : Type u_5
m : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : MeasurableSingletonClass α
a : α
f : α → ε
hfa : ‖f a‖ₑ < ∞
⊢ HasFiniteIntegral f (Measure.dirac a)

Tactic:
simpa [HasFiniteIntegral]

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

Goal state before:
pp: 𝕜 : 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
h : ε < ‖ξ‖
this : (ξ₀ * ξ⁻¹) • ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ
⊢ False

Tactic:
rw [smul_eq_mul, mul_assoc, inv_mul_cancel₀ hξ0, mul_one] at this

Goal state after:
𝕜 : 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
h : ε < ‖ξ‖
this : ξ₀ ∈ balancedCore 𝕜 {ξ₀}ᶜ
⊢ False
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module 𝕜 E
inst✝¹ : ContinuousSMul 𝕜 E
s t : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 (E ⧸ s)
s_closed : IsClosed[inst✝⁴] ↑s
s_le_t : s ≤ t
⊢ IsClosed[inst✝⁴] ↑t

Tactic:
by
  rw [show t = comap s.mkQ (map s.mkQ t) by simpa]
  exact (map s.mkQ t).closed_of_finiteDimensional.preimage continuous_quot_mk

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
p : Submodule 𝕜 E
hp : IsClosed[inst✝³] ↑p
hq : FiniteDimensional 𝕜 (E ⧸ p)
⊢ p.ClosedComplemented

Tactic:
by
  obtain ⟨q, hq⟩ : ∃ q, IsCompl p q := p.exists_isCompl
  exact hq.isTopCompl_of_finiteDimensional_quotient hp |>.closedComplemented

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : Module 𝕜 E
inst✝² : ContinuousSMul 𝕜 E
A B : Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 ↥A
inst✝ : T2Space ↥A
hB : B ≤ A
p : E →L[𝕜] ↥A
hp : ∀ (x : ↥A), p ↑x = x
⊢ B.ClosedComplemented

Tactic:
obtain ⟨C, hBC⟩ := B.exists_isCompl

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : Module 𝕜 E
inst✝² : ContinuousSMul 𝕜 E
A B : Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 ↥A
inst✝ : T2Space ↥A
hB : B ≤ A
p : E →L[𝕜] ↥A
hp : ∀ (x : ↥A), p ↑x = x
C : Submodule 𝕜 E
hBC : IsCompl B C
⊢ B.ClosedComplemented
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
⊢ IntegrableAtFilter f (𝓝 x) (μ.restrict s)

Tactic:
obtain ⟨t, ht_nhds, ht_int⟩ := hf x h

Goal state after:
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 μ
⊢ IntegrableAtFilter f (𝓝 x) (μ.restrict s)
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case neg
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 : IsOpen[inst✝³] sᶜ
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
⊢ IntegrableOn f sᶜ (μ.restrict s)

Tactic:
rw [IntegrableOn, restrict_restrict, inter_comm, inter_compl_self, ← IntegrableOn]

Goal state after:
case neg
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 : IsOpen[inst✝³] sᶜ
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
⊢ IntegrableOn f ∅ μ

case neg
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 : IsOpen[inst✝³] sᶜ
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
⊢ MeasurableSet sᶜ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
ε'' : Type u_5
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace ε''
inst✝² : ESeminormedAddMonoid ε''
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → ε''
μ : Measure X
h : LocallyIntegrable (f ∘ ⇑e) μ
x : Y
⊢ IntegrableAtFilter f (𝓝 x) (Measure.map (⇑e) μ)

Tactic:
rcases h (e.symm x) with ⟨U, hU, h'U⟩

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
ε'' : Type u_5
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace ε''
inst✝² : ESeminormedAddMonoid ε''
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → ε''
μ : Measure X
h : LocallyIntegrable (f ∘ ⇑e) μ
x : Y
U : Set X
hU : U ∈ 𝓝 (e.symm x)
h'U : IntegrableOn (f ∘ ⇑e) U μ
⊢ IntegrableAtFilter f (𝓝 x) (Measure.map (⇑e) μ)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
a✝ : α
⊢ (toSimpleFunc 0) a✝ = ↑↑↑0 a✝ → ↑↑0 a✝ = 0 a✝ → (toSimpleFunc 0) a✝ = 0 a✝

Tactic:
h₁

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
a✝ : α
h₁ : (toSimpleFunc 0) a✝ = ↑↑↑0 a✝
⊢ ↑↑0 a✝ = 0 a✝ → (toSimpleFunc 0) a✝ = 0 a✝
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
a✝¹ : α
h₁ : (toSimpleFunc 0) a✝¹ = ↑↑↑0 a✝¹
a✝ : ↑↑0 a✝¹ = 0 a✝¹
⊢ (toSimpleFunc 0) a✝¹ = 0 a✝¹

Tactic:
h₁

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
a✝¹ : α
h₁ : (toSimpleFunc 0) a✝¹ = ↑↑↑0 a✝¹
a✝ : ↑↑0 a✝¹ = 0 a✝¹
⊢ ↑↑↑0 a✝¹ = 0 a✝¹
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✝¹³ : NormedField 𝕜
inst✝¹² : NormedField 𝕜₂
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜 E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₂ F
inst✝⁷ : NormedAddCommGroup Eₗ
inst✝⁶ : NormedSpace 𝕜 Eₗ
inst✝⁵ : CompleteSpace Eₗ
inst✝⁴ : NormedAddCommGroup Fₗ
inst✝³ : NormedSpace 𝕜₂ Fₗ
inst✝² : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange ⇑e₁
h_dense₂ : DenseRange ⇑e₂
h_norm : ∀ (x : E), ‖e₂ (f x)‖ = ‖e₁ x‖
h_norm₂ : ∀ (x : F), ‖e₁ (f.symm x)‖ = ‖e₂ x‖
⊢ ∀ (x : F), ‖e₁ (f.symm x)‖ ≤ 1 * ‖e₂ x‖

Tactic:
by simp [h_norm₂]

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

Goal state before:
pp: case neg
α : Type u_1
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : PartialOrder F
inst✝¹ : IsOrderedAddMonoid F
inst✝ : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : 0 ≤ᵐ[ν] ⇑f
hμν : μ ≤ ν
hfν : Integrable (⇑f) ν
x : α
hx : ¬0 ≤ f x
⊢ ν (⇑f ⁻¹' {f x}) ≤ ν {a | ¬0 a ≤ f a}

Tactic:
refine measure_mono fun y hy ↦ ?_

Goal state after:
case neg
α : Type u_1
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : PartialOrder F
inst✝¹ : IsOrderedAddMonoid F
inst✝ : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : 0 ≤ᵐ[ν] ⇑f
hμν : μ ≤ ν
hfν : Integrable (⇑f) ν
x : α
hx : ¬0 ≤ f x
y : α
hy : y ∈ ⇑f ⁻¹' {f x}
⊢ y ∈ {a | ¬0 a ≤ f a}
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
a : α
⊢ (toSimpleFunc (posPart (-f))) a = (toSimpleFunc (-f)).posPart a →
    (toSimpleFunc (-f)) a = (-⇑(toSimpleFunc f)) a → (toSimpleFunc (posPart (-f))) a = (-toSimpleFunc f).posPart a

Tactic:
h₁

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
a : α
h₁ : (toSimpleFunc (posPart (-f))) a = (toSimpleFunc (-f)).posPart a
⊢ (toSimpleFunc (-f)) a = (-⇑(toSimpleFunc f)) a → (toSimpleFunc (posPart (-f))) a = (-toSimpleFunc f).posPart a
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
a : α
h₁ : (toSimpleFunc (posPart (-f))) a = (toSimpleFunc (-f)).posPart a
h₂ : (toSimpleFunc (-f)) a = (-⇑(toSimpleFunc f)) a
⊢ (toSimpleFunc (posPart (-f))) a = (-toSimpleFunc f).posPart a

Tactic:
h₁

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
a : α
h₁ : (toSimpleFunc (posPart (-f))) a = (toSimpleFunc (-f)).posPart a
h₂ : (toSimpleFunc (-f)) a = (-⇑(toSimpleFunc f)) a
⊢ (toSimpleFunc (-f)).posPart a = (-toSimpleFunc f).posPart a
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ⇑(toSimpleFunc f).negPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
a✝ : α
⊢ (toSimpleFunc f).posPart a✝ = (SimpleFunc.map norm (toSimpleFunc (posPart f))) a✝ →
    (toSimpleFunc f).negPart a✝ = (SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝ →
      (toSimpleFunc f) a✝ =
        (SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝

Tactic:
h₁

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ⇑(toSimpleFunc f).negPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
a✝ : α
h₁ : (toSimpleFunc f).posPart a✝ = (SimpleFunc.map norm (toSimpleFunc (posPart f))) a✝
⊢ (toSimpleFunc f).negPart a✝ = (SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝ →
    (toSimpleFunc f) a✝ =
      (SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a✝ : α
⊢ ↑↑(Lp.posPart f₁) a✝ = max (↑↑f₁ a✝) 0 →
    ↑↑(Integrable.toL1 f hf) a✝ = f a✝ → ENNReal.ofReal (f a✝) = ‖↑↑(Lp.posPart f₁) a✝‖ₑ

Tactic:
h₁

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a✝ : α
h₁ : ↑↑(Lp.posPart f₁) a✝ = max (↑↑f₁ a✝) 0
⊢ ↑↑(Integrable.toL1 f hf) a✝ = f a✝ → ENNReal.ofReal (f a✝) = ‖↑↑(Lp.posPart f₁) a✝‖ₑ
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
a✝ : α
⊢ ↑↑(Lp.negPart f₁) a✝ = -min (↑↑f₁ a✝) 0 →
    ↑↑(Integrable.toL1 f hf) a✝ = f a✝ → ENNReal.ofReal (-f a✝) = ‖↑↑(Lp.negPart f₁) a✝‖ₑ

Tactic:
h₁

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
a✝ : α
h₁ : ↑↑(Lp.negPart f₁) a✝ = -min (↑↑f₁ a✝) 0
⊢ ↑↑(Integrable.toL1 f hf) a✝ = f a✝ → ENNReal.ofReal (-f a✝) = ‖↑↑(Lp.negPart f₁) a✝‖ₑ
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
huv : u ~[l] v
⊢ (fun x ↦ -u x) ~[l] fun x ↦ -v x

Tactic:
by
  rw [IsEquivalent]
  convert! huv.isLittleO.neg_left.neg_right
  simp [neg_add_eq_sub]

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 α
inst✝⁵ : PartialOrder E
inst✝⁴ : IsOrderedAddMonoid E
inst✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
β : Type u_6
inst✝¹ : AddCommMonoid β
inst✝ : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable (fun x ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
⊢ 0 ≤ p →
    0 ≤ q →
      p + q = 1 →
        (fun b ↦ ∫ (x : α), f x b ∂μ) (p • a + q • b) ≤
          p • (fun b ↦ ∫ (x : α), f x b ∂μ) a + q • (fun b ↦ ∫ (x : α), f x b ∂μ) b

Tactic:
hp

Goal state after:
α : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : PartialOrder E
inst✝⁴ : IsOrderedAddMonoid E
inst✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
β : Type u_6
inst✝¹ : AddCommMonoid β
inst✝ : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable (fun x ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
⊢ 0 ≤ q →
    p + q = 1 →
      (fun b ↦ ∫ (x : α), f x b ∂μ) (p • a + q • b) ≤
        p • (fun b ↦ ∫ (x : α), f x b ∂μ) a + q • (fun b ↦ ∫ (x : α), f x b ∂μ) b