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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ AEStronglyMeasurable (fun x ↦ (f x).toReal) μ ∧ ∫⁻ (x : α), f x ∂μ ≠ ∞ ↔ ∫⁻ (x : α), f x ∂μ ≠ ∞

Tactic:
simp only [hf.ennreal_toReal.aestronglyMeasurable, ne_eq, true_and]

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

Goal state before:
pp: 𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i ≃ₗᵢ[𝕜] E₁ i
⊢ ‖g‖ ≤ ‖g.compContinuousLinearMap fun i ↦ (f i).toLinearIsometry.toContinuousLinearMap‖

Tactic:
have : g = (g.compContinuousLinearMap fun i => (f i : E i →L[𝕜] E₁ i)).compContinuousLinearMap
      fun i => ((f i).symm : E₁ i →L[𝕜] E i) := by
    ext1 m
    simp

Goal state after:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i ≃ₗᵢ[𝕜] E₁ i
this : g = (g.compContinuousLinearMap fun i ↦ ↑↑(f i)).compContinuousLinearMap fun i ↦ ↑↑(f i).symm
⊢ ‖g‖ ≤ ‖g.compContinuousLinearMap fun i ↦ (f i).toLinearIsometry.toContinuousLinearMap‖
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹² : Fintype ι'
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁶ : SeminormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : SeminormedAddCommGroup G'
inst✝³ : NormedSpace 𝕜 G'
inst✝² : Fintype ι
α : Type u_1
inst✝¹ : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : (i : { a // a ∉ s }) → E₁ ↑i
m : α → (i : ι) → E₁ i
⊢ ‖f‖ * ∏ i, ‖if h : i ∈ s then m (e.symm ⟨i, ⋯⟩) i else x ⟨i, ⋯⟩‖ ≤ (‖f‖ * ∏ i, ‖x i‖) * ∏ i, ‖m i‖

Tactic:
rw [← prod_compl_mul_prod s.toFinset, mul_assoc]

Goal state after:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹² : Fintype ι'
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁶ : SeminormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : SeminormedAddCommGroup G'
inst✝³ : NormedSpace 𝕜 G'
inst✝² : Fintype ι
α : Type u_1
inst✝¹ : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : (i : { a // a ∉ s }) → E₁ ↑i
m : α → (i : ι) → E₁ i
⊢ ‖f‖ *
      ((∏ i ∈ s.toFinsetᶜ, ‖if h : i ∈ s then m (e.symm ⟨i, ⋯⟩) i else x ⟨i, ⋯⟩‖) *
        ∏ i ∈ s.toFinset, ‖if h : i ∈ s then m (e.symm ⟨i, ⋯⟩) i else x ⟨i, ⋯⟩‖) ≤
    ‖f‖ * ((∏ i, ‖x i‖) * ∏ i, ‖m i‖)
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case mpr
X : Type u_1
ε : Type u_3
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace ε
inst✝⁴ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝³ : PseudoMetrizableSpace ε
inst✝² : LinearOrder X
inst✝¹ : OrderTop X
inst✝ : CompactIccSpace X
⊢ IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ → Integrable f μ

Tactic:
refine fun h ↦ integrable_iff_integrableAtFilter_cocompact.mpr ⟨?_, h.2⟩
    exact h.1.filter_mono cocompact_le_atBot

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

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

Tactic:
by_cases hp0 : p = 0
  · rw [hp0, memLp_zero_iff_aestronglyMeasurable]; exact f.aestronglyMeasurable
  by_cases hp_top : p = ∞
  · rw [hp_top]; exact memLp_top f μ
  refine ⟨f.aestronglyMeasurable, ?_⟩
  rw [eLpNorm_eq_eLpNorm' hp0 hp_top, f.eLpNorm'_eq]
  refine ENNReal.rpow_lt_top_of_nonneg (by simp) (ENNReal.sum_lt_top.mpr fun y _ => ?_).ne
  by_cases hy0 : y = 0
  · simp [hy0, ENNReal.toReal_pos hp0 hp_top]
  · refine ENNReal.mul_lt_top ?_ (hf y hy0)
    exact ENNReal.rpow_lt_top_of_nonneg ENNReal.toReal_nonneg ENNReal.coe_ne_top

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 α
inst✝ : DecidablePred fun x ↦ x ≠ 0
T : Set α → F →L[ℝ] F'
hT : T ∅ = 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx : x ∉ f.range ∨ x = 0
⊢ (T (⇑f ⁻¹' {x})) x = 0

Tactic:
rcases hx.symm with (rfl | hx)

Goal state after:
case inl
α : 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 α
inst✝ : DecidablePred fun x ↦ x ≠ 0
T : Set α → F →L[ℝ] F'
hT : T ∅ = 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
hx : 0 ∉ f.range ∨ 0 = 0
⊢ (T (⇑f ⁻¹' {0})) 0 = 0

case inr
α : 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 α
inst✝ : DecidablePred fun x ↦ x ≠ 0
T : Set α → F →L[ℝ] F'
hT : T ∅ = 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx✝ : x ∉ f.range ∨ x = 0
hx : x ∉ f.range
⊢ (T (⇑f ⁻¹' {x})) x = 0
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 α
s : Set α
x : F
⊢ (weightedSMul μ s) x = μ.real s • x

Tactic:
simp [weightedSMul]

Goal state after:
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 α
x✝ : Set α
⊢ weightedSMul 0 x✝ = 0 x✝

Tactic:
simp [weightedSMul]

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
g : α →ₛ G
hp : AEEqFun.mk ⇑g ⋯ ∈ Lp G p μ
hf : 0 ≤ ⟨⟨AEEqFun.mk ⇑g ⋯, hp⟩, ⋯⟩
⊢ ∃ f', 0 ≤ f' ∧ ↑↑↑⟨⟨AEEqFun.mk ⇑g ⋯, hp⟩, ⋯⟩ =ᵐ[μ] ⇑f'

Tactic:
change 0 ≤ᵐ[μ] g at hf

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
g : α →ₛ G
hp : AEEqFun.mk ⇑g ⋯ ∈ Lp G p μ
hf : 0 ≤ᵐ[μ] ⇑g
⊢ ∃ f', 0 ≤ f' ∧ ↑↑↑⟨⟨AEEqFun.mk ⇑g ⋯, hp⟩, ⋯⟩ =ᵐ[μ] ⇑f'
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 α
inst✝ : DecidablePred fun x ↦ x ≠ 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx : x ∉ f.range ∨ x = 0
⊢ μ.real (⇑f ⁻¹' {x}) • x = 0

Tactic:
rcases hx.symm with (rfl | hx)

Goal state after:
case inl
α : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x ↦ x ≠ 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
hx : 0 ∉ f.range ∨ 0 = 0
⊢ μ.real (⇑f ⁻¹' {0}) • 0 = 0

case inr
α : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x ↦ x ≠ 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx✝ : x ∉ f.range ∨ x = 0
hx : x ∉ f.range
⊢ μ.real (⇑f ⁻¹' {x}) • x = 0
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝⁶ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ Continuous integral

pp: α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝⁶ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ ∀ (a : ↥(α →₁ₛ[μ] E)), integral ↑a = (integralCLM' 𝕜) ↑a

Tactic:
· simp_rw [integral_def]
    exact (integralCLM (E := E)).continuous

Goal state after:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝⁶ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ ∀ (a : ↥(α →₁ₛ[μ] E)), integral ↑a = (integralCLM' 𝕜) ↑a
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁶ : NormedAddCommGroup G''
inst✝⁵ : PartialOrder G''
inst✝⁴ : IsOrderedAddMonoid G''
inst✝³ : NormedSpace ℝ G''
inst✝² : NormedAddCommGroup G'
inst✝¹ : PartialOrder G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable (⇑f) μ
i : G'
hi : i ∈ Set.range ⇑f
h0 : ¬i = 0
y : α
hy : f y = i
⊢ 0 ≤ f y

Tactic:
convert! hf y

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 α
f : α → G
hf : f =ᵐ[μ] 0
⊢ ∫ (a : α), f a ∂μ = 0

Tactic:
simp [integral_congr_ae hf, integral_zero]

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

Goal state before:
pp: case add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → motive (s.indicator fun x ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f | motive ↑↑f}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
f g : α →ₛ E
hfg : Disjoint (support ⇑f) (support ⇑g)
hf : MemLp (⇑f) p μ → motive ⇑f
hg : MemLp (⇑g) p μ → motive ⇑g
⊢ MemLp (⇑(f + g)) p μ → motive ⇑(f + g)

Tactic:
int_fg

Goal state after:
case add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → motive (s.indicator fun x ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f | motive ↑↑f}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
f g : α →ₛ E
hfg : Disjoint (support ⇑f) (support ⇑g)
hf : MemLp (⇑f) p μ → motive ⇑f
hg : MemLp (⇑g) p μ → motive ⇑g
int_fg : MemLp (⇑(f + g)) p μ
⊢ motive ⇑(f + g)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

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

Tactic:
integral_const_mul

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
⊢ 2 * ∫ (a : α), max (f a) 0 ∂μ - ∫ (a : α), f a ∂μ = 2 * ∫ (x : α), max (f x) 0 ∂μ - ∫ (x : α), f x ∂μ
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

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

Tactic:
integral_const_mul

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
⊢ 2 * ∫ (a : α), max (-f a) 0 ∂μ + ∫ (a : α), f a ∂μ = 2 * ∫ (x : α), max (-f x) 0 ∂μ + ∫ (x : α), f x ∂μ
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 : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
⊢ ∫ (x : α), p • f x a + q • f x b ∂μ = ∫ (x : α), p • f x a ∂μ + ∫ (x : α), q • f x b ∂μ

Tactic:
apply integral_add

Goal state after:
case hf
α : 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
hq : 0 ≤ q
hpq : p + q = 1
⊢ Integrable (fun a_1 ↦ p • f a_1 a) μ

case hg
α : 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
hq : 0 ≤ q
hpq : p + q = 1
⊢ Integrable (fun a ↦ q • f a b) μ
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T' s = c • T s
f : ↥(Lp E 1 μ)
⊢ (setToL1 hT') f = c • (setToL1 hT) f

Tactic:
apply setToL1_unique hT' (A := c • setToL1 hT) _ f
  simp [setToL1_eq_setToL1SCLM, setToL1SCLM_smul_left' c hT hT' h_smul]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: case refine_1
𝕜 : Type u_4
inst✝² : RCLike 𝕜
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
⊢ (↑‖x₀‖)⁻¹ • x₀ ∉ F

Tactic:
rwa [Submodule.smul_mem_iff]
    simpa

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

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hF : CompleteSpace F
⊢ setToFun μ T hT 0 = 0

Tactic:
setToFun_eq hT (integrable_zero _ _ _),

Goal state after:
case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hF : CompleteSpace F
⊢ (L1.setToL1 hT) (Integrable.toL1 0 ⋯) = 0
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
s✝ : Finset ι
f : ι → α → E
i : ι
s : Finset ι
his : i ∉ s
ih : (∀ i ∈ s, Integrable (f i) μ) → setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
⊢ setToFun μ T hT (f i) + setToFun μ T hT (∑ i ∈ s, f i) = setToFun μ T hT (f i) + ∑ i ∈ s, setToFun μ T hT (f i)

Tactic:
ih fun i hi => hf i (Finset.mem_insert_of_mem hi)

Goal state after:
case refine_2
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
s✝ : Finset ι
f : ι → α → E
i : ι
s : Finset ι
his : i ∉ s
ih : (∀ i ∈ s, Integrable (f i) μ) → setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
⊢ setToFun μ T hT (f i) + ∑ i ∈ s, setToFun μ T hT (f i) = setToFun μ T hT (f i) + ∑ i ∈ s, setToFun μ T hT (f i)
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalSeminormedRing R
s t : Set R
hs : ∃ C, ∀ ⦃x : R⦄, x ∈ s → ∀ ⦃y : R⦄, y ∈ s → dist x y ≤ C
ht : ∃ C, ∀ ⦃x : R⦄, x ∈ t → ∀ ⦃y : R⦄, y ∈ t → dist x y ≤ C
Af : ℝ
hAf : s ⊆ Metric.closedBall 0 Af
Ag : ℝ
hAg : t ⊆ Metric.closedBall 0 Ag
z : R
hz : z ∈ s * t
w : R
hw : w ∈ s * t
x₁ : R
hx₁ : x₁ ∈ s
y₁ : R
hy₁ : y₁ ∈ t
z_eq : x₁ * y₁ = z
x₂ : R
hx₂ : x₂ ∈ s
y₂ : R
hy₂ : y₂ ∈ t
w_eq : x₂ * y₂ = w
hAf' : 0 ≤ Af
⊢ ∀ {x y : R}, x ∈ s → y ∈ t → ‖x * y‖ ≤ Af * Ag

Tactic:
intro x y x_in_s y_in_t

Goal state after:
R : Type u_1
inst✝ : NonUnitalSeminormedRing R
s t : Set R
hs : ∃ C, ∀ ⦃x : R⦄, x ∈ s → ∀ ⦃y : R⦄, y ∈ s → dist x y ≤ C
ht : ∃ C, ∀ ⦃x : R⦄, x ∈ t → ∀ ⦃y : R⦄, y ∈ t → dist x y ≤ C
Af : ℝ
hAf : s ⊆ Metric.closedBall 0 Af
Ag : ℝ
hAg : t ⊆ Metric.closedBall 0 Ag
z : R
hz : z ∈ s * t
w : R
hw : w ∈ s * t
x₁ : R
hx₁ : x₁ ∈ s
y₁ : R
hy₁ : y₁ ∈ t
z_eq : x₁ * y₁ = z
x₂ : R
hx₂ : x₂ ∈ s
y₂ : R
hy₂ : y₂ ∈ t
w_eq : x₂ * y₂ = w
hAf' : 0 ≤ Af
x y : R
x_in_s : x ∈ s
y_in_t : y ∈ t
⊢ ‖x * y‖ ≤ Af * Ag
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
⊢ (L1.setToL1 hT) (Integrable.toL1 (-f) ⋯) = -(L1.setToL1 hT) (Integrable.toL1 f hf)

Tactic:
Integrable.toL1_neg,

Goal state after:
case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
⊢ (L1.setToL1 hT) (-Integrable.toL1 f ?pos.hf✝) = -(L1.setToL1 hT) (Integrable.toL1 f hf)

case pos.hf
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
⊢ Integrable f μ
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv
LA : LipschitzWith ‖↑A‖₊ ⇑A
L : LipschitzOnWith (‖↑A‖₊ * K) (⇑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (⇑A ∘ f) g s
⊢ EqOn f (⇑A.symm ∘ g) s

Tactic:
· intro x hx
    have : A (f x) = g x := gs hx
    simp only [(· ∘ ·), ← this, A.symm_apply_apply]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: case inl
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F
hf : f.ker = ⊥
h✝ : Subsingleton E
⊢ ∃ K > 0, AntilipschitzWith K ⇑f

pp: case inr
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F
hf : f.ker = ⊥
h✝ : Nontrivial E
⊢ ∃ K > 0, AntilipschitzWith K ⇑f

Tactic:
· exact ⟨1, zero_lt_one, AntilipschitzWith.of_subsingleton⟩

Goal state after:
case inr
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F
hf : f.ker = ⊥
h✝ : Nontrivial E
⊢ ∃ K > 0, AntilipschitzWith K ⇑f
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: case inr
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F
hf : f.ker = ⊥
h✝ : Nontrivial E
⊢ ∃ K > 0, AntilipschitzWith K ⇑f

Tactic:
rw [LinearMap.ker_eq_bot] at hf
    let e : E ≃L[𝕜] LinearMap.range f := (LinearEquiv.ofInjective f hf).toContinuousLinearEquiv
    exact ⟨_, e.nnnorm_symm_pos, e.antilipschitz⟩

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
hC : ∀ ⦃x : β⦄, x ∈ range ⇑f ∪ range ⇑g → ∀ ⦃y : β⦄, y ∈ range ⇑f ∪ range ⇑g → dist x y ≤ C
x : α
⊢ g x ∈ range ⇑f ∪ range ⇑g

Tactic:
right

Goal state after:
case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
hC : ∀ ⦃x : β⦄, x ∈ range ⇑f ∪ range ⇑g → ∀ ⦃y : β⦄, y ∈ range ⇑f ∪ range ⇑g → dist x y ≤ C
x : α
⊢ g x ∈ range ⇑g
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case hfm
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ AEStronglyMeasurable (fun a ↦ ‖g a‖ ^ q) μ

Tactic:
exact (hg.1.norm.aemeasurable.pow aemeasurable_const).aestronglyMeasurable

Goal state after: