mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
hr : ¬c = 0
hf' : ¬Integrable (c • f) μ
⊢ 0 = 0

Tactic:
]

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 α
inst✝ : IsFiniteMeasure μ
f : α → G
C : ℝ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ C * μ.real univ = C * μ.real univ

Tactic:
]

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

Goal state before:
pp: case refine_1
α : 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
LAsymm : LipschitzWith ‖↑A.symm‖₊ ⇑A.symm
⊢ ‖↑A.symm‖₊ * ‖↑A‖₊ * K ≤
    (have A := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv;
      max (‖↑A.symm‖₊ * ‖↑A‖₊) 1) *
      K

Tactic:
]

Goal state after:
case refine_1
α : 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
LAsymm : LipschitzWith ‖↑A.symm‖₊ ⇑A.symm
⊢ ‖↑A.symm‖₊ * ‖↑A‖₊ * K ≤
    (have A := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv;
      max (‖↑A.symm‖₊ * ‖↑A‖₊) 1) *
      K
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 : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᵐ[μ] g
hF : CompleteSpace F
hfi : Integrable f μ
hgi : Integrable g μ
⊢ (L1.setToL1 hT) (Integrable.toL1 g hgi) = (L1.setToL1 hT) (Integrable.toL1 g hgi)

Tactic:
]

Goal state after:
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 α
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᵐ[μ] g
hF : CompleteSpace F
hfi : ¬Integrable g μ
⊢ ¬Integrable g μ

Tactic:
]

Goal state after:
α : 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 : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᵐ[μ] g
hF : CompleteSpace F
hfi : ¬Integrable g μ
⊢ ¬Integrable g μ
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case neg
α : 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 : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᵐ[μ] g
hF : CompleteSpace F
hfi : ¬Integrable f μ
hgi : ¬Integrable g μ
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case cons
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_6
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
a✝ : ι
s✝ : Finset ι
h : a✝ ∉ s✝
ih : (∀ i ∈ s✝, Integrable f (μ i)) → ∫ (a : α), f a ∂∑ i ∈ s✝, μ i = ∑ i ∈ s✝, ∫ (a : α), f a ∂μ i
hf : Integrable f (μ a✝) ∧ ∀ x ∈ s✝, Integrable f (μ x)
⊢ ∫ (a : α), f a ∂∑ i ∈ Finset.cons a✝ s✝ h, μ i = ∑ i ∈ Finset.cons a✝ s✝ h, ∫ (a : α), f a ∂μ i

Tactic:
]

Goal state after:
case cons
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_6
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
a✝ : ι
s✝ : Finset ι
h : a✝ ∉ s✝
ih : (∀ i ∈ s✝, Integrable f (μ i)) → ∫ (a : α), f a ∂∑ i ∈ s✝, μ i = ∑ i ∈ s✝, ∫ (a : α), f a ∂μ i
hf : Integrable f (μ a✝) ∧ ∀ x ∈ s✝, Integrable f (μ x)
⊢ ∫ (a : α), f a ∂∑ i ∈ Finset.cons a✝ s✝ h, μ i = ∑ i ∈ Finset.cons a✝ s✝ h, ∫ (a : α), f a ∂μ i
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 : Function.Injective ⇑f
h✝ : Nontrivial E
⊢ ∃ K > 0, AntilipschitzWith K ⇑f

Tactic:
]

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 : Function.Injective ⇑f
h✝ : Nontrivial E
⊢ ∃ K > 0, AntilipschitzWith K ⇑f
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case cons
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_6
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
a✝ : ι
s✝ : Finset ι
h : a✝ ∉ s✝
ih : (∀ i ∈ s✝, Integrable f (μ i)) → ∫ (a : α), f a ∂∑ i ∈ s✝, μ i = ∑ i ∈ s✝, ∫ (a : α), f a ∂μ i
hf : Integrable f (μ a✝) ∧ ∀ x ∈ s✝, Integrable f (μ x)
⊢ ∫ (a : α), f a ∂(μ a✝ + ∑ x ∈ s✝, μ x) = ∫ (a : α), f a ∂μ a✝ + ∫ (a : α), f a ∂∑ i ∈ s✝, μ i

Tactic:
]

Goal state after:
case cons
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_6
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
a✝ : ι
s✝ : Finset ι
h : a✝ ∉ s✝
ih : (∀ i ∈ s✝, Integrable f (μ i)) → ∫ (a : α), f a ∂∑ i ∈ s✝, μ i = ∑ i ∈ s✝, ∫ (a : α), f a ∂μ i
hf : Integrable f (μ a✝) ∧ ∀ x ∈ s✝, Integrable f (μ x)
⊢ ∫ (a : α), f a ∂(μ a✝ + ∑ x ∈ s✝, μ x) = ∫ (a : α), f a ∂μ a✝ + ∫ (a : α), f a ∂∑ i ∈ s✝, μ i
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 α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h : μ = 0
this : f =ᵐ[μ] 0
⊢ 0 = 0

Tactic:
]

Goal state after:
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 α
T : Set α → E →L[ℝ] F
C : ℝ
inst✝ : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E
⊢ setToFun μ T hT ↑↑(indicatorConstLp 1 hs hμs x) = (T s) x

Tactic:
]

Goal state after:
α : 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 : ℝ
inst✝ : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E
⊢ setToFun μ T hT ↑↑(indicatorConstLp 1 hs hμs x) = (T s) x
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: case mp
𝕜 : 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
⊢ f.ker = ⊥ → ∃ K > 0, AntilipschitzWith K ⇑f

Tactic:
]

Goal state after:
case mp
𝕜 : 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
⊢ f.ker = ⊥ → ∃ K > 0, AntilipschitzWith K ⇑f
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 α
T : Set α → E →L[ℝ] F
C : ℝ
inst✝ : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E
⊢ (L1.setToL1 hT) (indicatorConstLp 1 hs hμs x) = (T s) x

Tactic:
]

Goal state after:
α : 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 : ℝ
inst✝ : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E
⊢ (L1.setToL1 hT) (indicatorConstLp 1 hs hμs x) = (T s) x
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
h₁ : Integrable f μ
h₂ : Integrable f ν
⊢ ↑‖∫ (x : α), f x ∂ν‖₊ ≤ ∫⁻ (x : α), ‖f x‖ₑ ∂ν

Tactic:
]

Goal state after:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ ν : Measure α
f : α → G
h₁ : Integrable f μ
h₂ : Integrable f ν
⊢ ↑‖∫ (x : α), f x ∂ν‖₊ ≤ ∫⁻ (x : α), ‖f x‖ₑ ∂ν
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 α
T : Set α → E →L[ℝ] F
C : ℝ
inst✝¹ : CompleteSpace F
inst✝ : IsFiniteMeasure μ
hT : DominatedFinMeasAdditive μ T C
x : E
this : (fun x_1 ↦ x) = univ.indicator fun x_1 ↦ x
⊢ setToFun μ T hT (univ.indicator fun x_1 ↦ x) = (T univ) x

Tactic:
]

Goal state after:
α : 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 : ℝ
inst✝¹ : CompleteSpace F
inst✝ : IsFiniteMeasure μ
hT : DominatedFinMeasAdditive μ T C
x : E
this : (fun x_1 ↦ x) = univ.indicator fun x_1 ↦ x
⊢ setToFun μ T hT (univ.indicator fun x_1 ↦ x) = (T univ) x
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case inl
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: 𝕜 : Type u
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type w
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : CompleteSpace 𝕜
PE : Type u_1
PF : Type u_2
inst✝⁴ : MetricSpace PE
inst✝³ : NormedAddTorsor E PE
inst✝² : MetricSpace PF
inst✝¹ : NormedAddTorsor F PF
inst✝ : FiniteDimensional 𝕜 E
f : PE →ᵃ[𝕜] PF
hf : Function.Injective ⇑f
K : ℝ≥0
hK : AntilipschitzWith K ⇑f.linear
x y : PE
⊢ ‖x -ᵥ y‖ ≤ ↑K * ‖f.linear (x -ᵥ y)‖

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type w
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : CompleteSpace 𝕜
PE : Type u_1
PF : Type u_2
inst✝⁴ : MetricSpace PE
inst✝³ : NormedAddTorsor E PE
inst✝² : MetricSpace PF
inst✝¹ : NormedAddTorsor F PF
inst✝ : FiniteDimensional 𝕜 E
f : PE →ᵃ[𝕜] PF
hf : Function.Injective ⇑f
K : ℝ≥0
hK : AntilipschitzWith K ⇑f.linear
x y : PE
⊢ ‖x -ᵥ y‖ ≤ ↑K * ‖f.linear (x -ᵥ y)‖
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case inr
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hc : c ≠ ∞
hdfma : DominatedFinMeasAdditive μ (weightedSMul (c • μ)) c.toReal
hdfma_smul : DominatedFinMeasAdditive (c • μ) (weightedSMul (c • μ)) 1
⊢ setToFun μ (weightedSMul (c • μ)) hdfma f = setToFun μ (fun s ↦ c.toReal • weightedSMul μ s) ⋯ f

Tactic:
]

Goal state after:
case inr
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hc : c ≠ ∞
hdfma : DominatedFinMeasAdditive μ (weightedSMul (c • μ)) c.toReal
hdfma_smul : DominatedFinMeasAdditive (c • μ) (weightedSMul (c • μ)) 1
⊢ setToFun μ (weightedSMul (c • μ)) hdfma f = setToFun μ (fun s ↦ c.toReal • weightedSMul μ s) ⋯ f
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : 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
⊢ ∀ x ∈ {L | Injective ⇑L}, ∀ᶠ (y : E →L[𝕜] F) in 𝓝 x, y ∈ {L | Injective ⇑L}

Tactic:
]

Goal state after:
𝕜 : 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
⊢ ∀ x ∈ {L | Injective ⇑L}, ∀ᶠ (y : E →L[𝕜] F) in 𝓝 x, y ∈ {L | Injective ⇑L}
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 α
T : Set α → E →L[ℝ] F
C : ℝ
inst✝ : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
f : SimpleFunc α E
hf : Integrable (⇑f) μ
h'f : MemLp (⇑f) 1 μ
g : ↥(α →₁ₛ[μ] E) := f.toLp h'f
A : ⇑f =ᵐ[μ] ↑↑↑g
⊢ (L1.SimpleFunc.setToL1SCLM α E μ hT) g = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) x

Tactic:
]

Goal state after:
α : 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 : ℝ
inst✝ : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
f : SimpleFunc α E
hf : Integrable (⇑f) μ
h'f : MemLp (⇑f) 1 μ
g : ↥(α →₁ₛ[μ] E) := f.toLp h'f
A : ⇑f =ᵐ[μ] ↑↑↑g
⊢ (L1.SimpleFunc.setToL1SCLM α E μ hT) g = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) x
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case neg
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hfi : ¬Integrable f (Measure.map φ μ)
⊢ 0 = 0

pp: case neg
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hfi : ¬Integrable f (Measure.map φ μ)
⊢ ¬Integrable (fun x ↦ f (φ x)) μ

Tactic:
]

Goal state after:
case neg
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hfi : ¬Integrable f (Measure.map φ μ)
⊢ ¬Integrable (fun x ↦ f (φ x)) μ
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 α
T : Set α → E →L[ℝ] F
C : ℝ
inst✝ : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
f : SimpleFunc α E
hf : Integrable (⇑f) μ
h'f : MemLp (⇑f) 1 μ
g : ↥(α →₁ₛ[μ] E) := f.toLp h'f
A : ⇑f =ᵐ[μ] ↑↑↑g
⊢ ↑↑↑g =ᵐ[μ] ↑↑↑g

Tactic:
]

Goal state after:
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 α
T : Set α → E →L[ℝ] F
C : ℝ
inst✝ : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
f : SimpleFunc α E
hf : Integrable (⇑f) μ
⊢ ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) x = SimpleFunc.setToSimpleFunc T f

Tactic:
]

Goal state after:
α : 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 : ℝ
inst✝ : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
f : SimpleFunc α E
hf : Integrable (⇑f) μ
⊢ ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) x = SimpleFunc.setToSimpleFunc T f
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
g : β → G
hgm : ¬AEStronglyMeasurable g (Measure.map f μ)
⊢ 0 = 0

pp: case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
g : β → G
hgm : ¬AEStronglyMeasurable g (Measure.map f μ)
⊢ ¬AEStronglyMeasurable (fun x ↦ g (f x)) μ

Tactic:
]

Goal state after:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
g : β → G
hgm : ¬AEStronglyMeasurable g (Measure.map f μ)
⊢ ¬AEStronglyMeasurable (fun x ↦ g (f x)) μ
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
α : Type u_6
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → G
⊢ ∫ (x : ↑s), f ↑x ∂Measure.comap Subtype.val μ = ∫ (x : α), f x ∂Measure.map Subtype.val (Measure.comap Subtype.val μ)

Tactic:
]

Goal state after:
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
α : Type u_6
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → G
⊢ ∫ (x : ↑s), f ↑x ∂Measure.comap Subtype.val μ = ∫ (x : α), f x ∂Measure.map Subtype.val (Measure.comap Subtype.val μ)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
hE : CompleteSpace E
inst✝ : MeasurableSpace α
f : α → E
a : α
hfm : StronglyMeasurable f
⊢ ∫ (x : α), f x ∂Measure.dirac a = f a

Tactic:
borelize E

Goal state after:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
hE : CompleteSpace E
inst✝ : MeasurableSpace α
f : α → E
a : α
hfm : StronglyMeasurable f
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ ∫ (x : α), f x ∂Measure.dirac a = f a
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
hE : CompleteSpace E
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
⊢ (∫ (x : α), f x ∂if a ∈ s then Measure.dirac a else 0) = if a ∈ s then f a else 0

Tactic:
]

Goal state after:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
hE : CompleteSpace E
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
⊢ (∫ (x : α), f x ∂if a ∈ s then Measure.dirac a else 0) = if a ∈ s then f a else 0
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : ι → E
⊢ ‖(↑LinearMap.toContinuousLinearMap ∘ₗ ↑(LinearEquiv.piRing 𝕜 E ι 𝕜).symm) g‖ ≤ Fintype.card ι • ‖g‖

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : ι → E
⊢ ‖(↑LinearMap.toContinuousLinearMap ∘ₗ ↑(LinearEquiv.piRing 𝕜 E ι 𝕜).symm) g‖ ≤ Fintype.card ι • ‖g‖
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
hE : CompleteSpace E
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
f : α → E
a : α
s : Set α
inst✝ : Decidable (a ∈ s)
⊢ (∫ (x : α), f x ∂if a ∈ s then Measure.dirac a else 0) = if a ∈ s then f a else 0

Tactic:
]

Goal state after:
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
hE : CompleteSpace E
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
f : α → E
a : α
s : Set α
inst✝ : Decidable (a ∈ s)
⊢ (∫ (x : α), f x ∂if a ∈ s then Measure.dirac a else 0) = if a ∈ s then f a else 0
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ sInf {C | 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C} ≤ 0

Tactic:
]

Goal state after:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
h : ¬Nonempty α
⊢ sInf {C | 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C} ≤ 0
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : ι → E
t : ι → 𝕜
⊢ ∑ i, ‖t i • g i‖ ≤ Fintype.card ι • (‖g‖ * ‖t‖)

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : ι → E
t : ι → 𝕜
⊢ ∑ i, ‖t i • g i‖ ≤ Fintype.card ι • (‖g‖ * ‖t‖)
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
⊢ sInf {C | 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C} =
    sInf {x | ∃ (h : 0 ≤ x), NNReal.mk x h ∈ {C | ∀ (x : α), nndist (f x) (g x) ≤ C}}

Tactic:
]

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
⊢ sInf {C | 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C} =
    sInf {x | ∃ (h : 0 ≤ x), NNReal.mk x h ∈ {C | ∀ (x : α), nndist (f x) (g x) ≤ C}}