mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹⁷ : AddCommGroup E
inst✝¹⁶ : UniformSpace E
inst✝¹⁵ : IsUniformAddGroup E
inst✝¹⁴ : AddCommGroup F
inst✝¹³ : UniformSpace F
inst✝¹² : IsUniformAddGroup F
inst✝¹¹ : T0Space F
inst✝¹⁰ : AddCommMonoid Eₗ
inst✝⁹ : UniformSpace Eₗ
inst✝⁸ : ContinuousAdd Eₗ
inst✝⁷ : Semiring 𝕜
inst✝⁶ : Semiring 𝕜₂
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : Module 𝕜 Eₗ
inst✝² : ContinuousConstSMul 𝕜 Eₗ
inst✝¹ : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f g : E →SL[σ₁₂] F
inst✝ : CompleteSpace F
e : E →L[𝕜] Eₗ
h : DenseRange ⇑e ∧ IsUniformInducing ⇑e
cont : Continuous (⋯.extend ⇑f)
eq : ∀ (b : E), ⋯.extend (⇑f) (e b) = f b
k : 𝕜
b : Eₗ
⊢ ∀ (a : E), ⋯.extend (⇑f) (k • e a) = σ₁₂ k • ⋯.extend (⇑f) (e a)

Tactic:
intro x
        rw [← map_smul]
        simp only [eq]
        exact map_smulₛₗ _ _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
x : 𝕜
f g : ↥(simpleFunc E p μ)
⊢ x • (f + g) = x • f + x • g

Tactic:
by ext1; exact smul_add _ _ _

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

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : α →ₛ E
hf : MemLp (⇑f) p μ
hg : MemLp (⇑g) p μ
⊢ (f - g).toLp ⋯ = f.toLp hf - g.toLp hg

Tactic:
by
  simp only [sub_eq_add_neg, ← toLp_neg, ← toLp_add]

Goal state after:
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
inst✝¹⁰ : NormedDivisionRing 𝕜
inst✝⁹ : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁸ : AddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : IsBoundedSMul 𝕜₂ F
inst✝² : Module 𝕜 Eₗ
inst✝¹ : IsBoundedSMul 𝕜 Eₗ
inst✝ : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange ⇑e
C : ℝ
h_norm : ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖
x✝ x : Eₗ
⊢ x ∈ e.range → ‖(f.extendOfNorm e) x‖ ≤ C * ‖x‖

Tactic:
⟨y, hxy⟩

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝¹⁰ : NormedDivisionRing 𝕜
inst✝⁹ : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁸ : AddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : IsBoundedSMul 𝕜₂ F
inst✝² : Module 𝕜 Eₗ
inst✝¹ : IsBoundedSMul 𝕜 Eₗ
inst✝ : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange ⇑e
C : ℝ
h_norm : ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖
x✝ x : Eₗ
y : E
hxy : e y = x
⊢ ‖(f.extendOfNorm e) x‖ ≤ C * ‖x‖
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ∞
a : α
hb : f a ∈ f.range
h0 : g (f a) = 0
x : G
hx : x ∈ f.range ∧ g x = 0
⊢ (T (⇑f ⁻¹' {x})) (g x) = 0

Tactic:
rw [hx.2, map_zero]

Goal state after:
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
c : 𝕜
f : ↥(Lp E 1 μ)
⊢ integral (c • f) = c • integral f

Tactic:
by
  rw [integral_eq' 𝕜 f, integral_eq' 𝕜 (c • f), map_smul (integralCLM' 𝕜) c f]

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

Goal state before:
pp: α : Type u_1
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'
m : MeasurableSpace α
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α) (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α →ₛ G'
hf : 0 ≤ f
i : G'
hi : i ∈ Set.range ⇑f
y : α
hy : f y = i
⊢ 0 ≤ f y

Tactic:
refine le_trans ?_ (hf y)

Goal state after:
α : Type u_1
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'
m : MeasurableSpace α
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α) (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α →ₛ G'
hf : 0 ≤ f
i : G'
hi : i ∈ Set.range ⇑f
y : α
hy : f y = i
⊢ 0 ≤ 0 y
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ‖T s‖ ≤ C * μ.real s
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ ∑ x ∈ f.range, ‖T (⇑f ⁻¹' {x})‖ * ‖x‖ ≤ ∑ x ∈ f.range, C * μ.real (⇑f ⁻¹' {x}) * ‖x‖

Tactic:
refine Finset.sum_le_sum fun b hb => ?_

Goal state after:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ‖T s‖ ≤ C * μ.real s
f : α →ₛ E
hf : Integrable (⇑f) μ
b : E
hb : b ∈ f.range
⊢ ‖T (⇑f ⁻¹' {b})‖ * ‖b‖ ≤ C * μ.real (⇑f ⁻¹' {b}) * ‖b‖
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst✝ : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
⊢ 0 ≤ᵐ[μ] fun x ↦ ‖f x‖

Tactic:
filter_upwards

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst✝ : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
⊢ ∀ (a : α), 0 a ≤ ‖f a‖
Module: Mathlib.Topology.Algebra.AffineSubspace

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : TopologicalSpace P
inst✝² : AddTorsor V P
s : AffineSubspace R P
inst✝¹ inst✝ : Nonempty ↥s
__AffineEquiv✝ : ↥s ≃ᵃ[R] ↥s := AffineEquiv.ofEq s s ⋯
⊢ Continuous (AffineEquiv.ofEq s s ⋯).toFun

Tactic:
exact continuous_id

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : TopologicalSpace P
inst✝² : AddTorsor V P
s : AffineSubspace R P
inst✝¹ inst✝ : Nonempty ↥s
__AffineEquiv✝ : ↥s ≃ᵃ[R] ↥s := AffineEquiv.ofEq s s ⋯
⊢ Continuous (AffineEquiv.ofEq s s ⋯).invFun

Tactic:
exact continuous_id

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

Goal state before:
pp: case f_nn
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)
⊢ 0 ≤ᵐ[μ] fun a ↦ F a - f 0 a

Tactic:
· filter_upwards [hf_bound] with a h_bound
      simp [h_bound 0]

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

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : Countable ι
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst✝ : CompleteSpace E
hc : ∀ (i : ι), c i ≠ ∞
hf : Summable fun i ↦ (c i).toReal * ‖f (x i)‖
⊢ HasSum (fun i ↦ (c i).toReal • f (x i)) (∫ (x : X), f x ∂Measure.sum fun i ↦ c i • Measure.dirac (x i))

Tactic:
simpa using hasSum_integral_measure (integrable_sum_dirac hc hf)

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

Goal state before:
pp: X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable { x // x ∈ s }
⊢ Integrable (fun x ↦ f ↑x) (Measure.comap Subtype.val μ)

Tactic:
rw [IntegrableOn, ← map_comap_subtype_coe, integrable_map_measure] at hf

Goal state after:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : Integrable (f ∘ Subtype.val) (Measure.comap Subtype.val μ)
hi : Countable { x // x ∈ s }
⊢ Integrable (fun x ↦ f ↑x) (Measure.comap Subtype.val μ)

case hg
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : Integrable f (Measure.map Subtype.val (Measure.comap Subtype.val μ))
hi : Countable { x // x ∈ s }
⊢ AEStronglyMeasurable f (Measure.map Subtype.val (Measure.comap Subtype.val μ))

case hf
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : Integrable f (Measure.map Subtype.val (Measure.comap Subtype.val μ))
hi : Countable { x // x ∈ s }
⊢ AEMeasurable Subtype.val (Measure.comap Subtype.val μ)

case hs
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : Integrable f (μ.restrict s)
hi : Countable { x // x ∈ s }
⊢ MeasurableSet s
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
⊢ ‖f‖ = sInf {C | 0 ≤ C ∧ ∀ (x : α), ‖f x‖ ≤ C}

Tactic:
simp [norm_def, BoundedContinuousFunction.dist_eq]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
n : ℕ
⊢ ⇑(zsmulRec (fun x1 x2 ↦ x1 • x2) (Int.negSucc n) f) = Int.negSucc n • ⇑f

Tactic:
by rw [zsmulRec, negSucc_zsmul, coe_neg, coe_nsmul]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
⊢ ‖f x - g x‖ ≤ dist f g

Tactic:
rw [dist_eq_norm]
  exact (f - g).norm_coe_le_norm x

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

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
R : Type u_1
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg : ∀ (x : α), f x = 0 ∨ g x = 0
x : α
⊢ ‖(f + g) x‖ = max ‖f x‖ ‖g x‖

Tactic:
obtain (h | h) := hfg x

Goal state after:
case inl
α : Type u
inst✝² : TopologicalSpace α
R : Type u_1
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
f g : α →ᵇ R
h✝ : f * g = 0
hfg : ∀ (x : α), f x = 0 ∨ g x = 0
x : α
h : f x = 0
⊢ ‖(f + g) x‖ = max ‖f x‖ ‖g x‖

case inr
α : Type u
inst✝² : TopologicalSpace α
R : Type u_1
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
f g : α →ᵇ R
h✝ : f * g = 0
hfg : ∀ (x : α), f x = 0 ∨ g x = 0
x : α
h : g x = 0
⊢ ‖(f + g) x‖ = max ‖f x‖ ‖g x‖
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 𝕜
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
x : X
⊢ ContinuousAt f x ↔ ∀ (y : E), ContinuousAt (fun q ↦ (f q) y) x

Tactic:
← continuousWithinAt_univ,

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 𝕜
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
x : X
⊢ ContinuousWithinAt f univ x ↔ ∀ (y : E), ContinuousWithinAt (fun q ↦ (f q) y) univ x
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᵐ[μ] f
hg_nonneg : 0 ≤ᵐ[μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
x : α
hxf : 0 x ≤ f x
hxg : 0 x ≤ g x
⊢ f x * g x = f x * ‖g x‖

Tactic:
Real.norm_of_nonneg hxg

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᵐ[μ] f
hg_nonneg : 0 ≤ᵐ[μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
x : α
hxf : 0 x ≤ f x
hxg : 0 x ≤ g x
⊢ f x * g x = f x * g x
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᵐ[μ] f
hg_nonneg : 0 ≤ᵐ[μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫ (a : α), f a * g a ∂μ = ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ
h_right_f : ∫ (a : α), f a ^ p ∂μ = ∫ (a : α), ‖f a‖ ^ p ∂μ
x : α
hxg : 0 x ≤ g x
⊢ g x ^ q = ‖g x‖ ^ q

Tactic:
Real.norm_of_nonneg hxg

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᵐ[μ] f
hg_nonneg : 0 ≤ᵐ[μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫ (a : α), f a * g a ∂μ = ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ
h_right_f : ∫ (a : α), f a ^ p ∂μ = ∫ (a : α), ‖f a‖ ^ p ∂μ
x : α
hxg : 0 x ≤ g x
⊢ g x ^ q = g x ^ q
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : α → E
⊢ (Summable fun x ↦ ‖f x‖) ↔ Summable f

Tactic:
refine ⟨Summable.of_norm, fun hf ↦ ?_⟩
  -- First we use a finite basis to reduce the problem to the case `E = Fin N → ℝ`
  suffices ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x => ‖g x‖ by
    obtain v := Module.finBasis ℝ E
    set e := v.equivFunL
    have H : Summable fun x => ‖e (f x)‖ := this (e.summable.2 hf)
    refine .of_norm_bounded (H.mul_left ↑‖(e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E)‖₊) fun i ↦ ?_
    simpa using (e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E).le_opNorm (e <| f i)
  clear! E
  -- Now we deal with `g : α → Fin N → ℝ`
  intro N g hg
  have : ∀ i, Summable fun x => ‖g x i‖ := fun i => (Pi.summable.1 hg i).abs
  refine .of_norm_bounded (summable_sum fun i (_ : i ∈ Finset.univ) => this i) fun x => ?_
  rw [norm_norm, pi_norm_le_iff_of_nonneg]
  · refine fun i => Finset.single_le_sum (f := fun i => ‖g x i‖) (fun i _ => ?_) (Finset.mem_univ i)
    exact norm_nonneg (g x i)
  · exact Finset.sum_nonneg fun _ _ => norm_nonneg _

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 T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T' C'
hT'' : DominatedFinMeasAdditive μ'' T'' C''
h : ∀ (s : Set α), MeasurableSet s → (μ + μ') s < ∞ → T'' s = T s + T' s
hf : Integrable f μ
hf' : Integrable f μ'
hμ : μ'' ≤ μ + μ'
hC : 0 ≤ C
hC' : 0 ≤ C'
hC'' : 0 ≤ C''
I : DominatedFinMeasAdditive (μ + μ') T C
A : setToFun (μ + μ') T I f = setToFun μ T hT f
I' : DominatedFinMeasAdditive (μ + μ') T' C'
A' : setToFun (μ + μ') T' I' f = setToFun μ' T' hT' f
I'' : DominatedFinMeasAdditive (μ + μ') T'' C''
A'' : setToFun (μ + μ') T'' I'' f = setToFun μ'' T'' hT'' f
⊢ setToFun (μ + μ') T'' I'' f = setToFun (μ + μ') T I f + setToFun (μ + μ') T' I' f

Tactic:
apply setToFun_add_left' _ _ _ h

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 : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst✝ : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
⊢ Tendsto x atTop l → Tendsto ((fun n ↦ setToFun μ T hT (fs n)) ∘ x) atTop (𝓝 (setToFun μ T hT f))

Tactic:
xl

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 : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst✝ : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
⊢ Tendsto ((fun n ↦ setToFun μ T hT (fs n)) ∘ x) atTop (𝓝 (setToFun μ T hT f))
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → β
a : α
A : (𝓝 (f a) ⊓ map f (𝓝[≤] a)).NeBot
h' : (𝓝[<] a).NeBot
H : ¬∃ y, Tendsto f (𝓝[<] a) (𝓝 y)
⊢ MapClusterPt (leftLim f a) (𝓝[≤] a) f

Tactic:
simp [MapClusterPt, ClusterPt, H, leftLim_eq_of_not_tendsto, A]

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

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : TopologicalSpace R
inst✝ : OrderTopology R
a b : R
⊢ IsOpen[inst✝¹] (Iotop a b)

Tactic:
by
  simp only [Iotop]
  split_ifs with h
  · have : Ioc a b = Ioi a := Subset.antisymm (fun x hx ↦ hx.1) (fun x hx ↦ by exact ⟨hx, h _⟩)
    simp [this, isOpen_Ioi]
  · simp [isOpen_Ioo]

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

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
A : ∀ u ∈ {x ∈ t.powerset | x.Nonempty}, MeasurableSet (⋂ i ∈ u, s i)
this :
  ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, (-1) ^ (#x + 1) • f a ∂μ =
    ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X), (⋂ i ∈ x, s i).indicator (fun a ↦ (-1) ^ (#x + 1) • f a) a ∂μ
⊢ ∫ (x : X), (⋃ i ∈ t, s i).indicator f x ∂μ =
    ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X), (⋂ i ∈ x, s i).indicator (fun a ↦ (-1) ^ (#x + 1) • f a) a ∂μ

Tactic:
← integral_finsetSum

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
A : ∀ u ∈ {x ∈ t.powerset | x.Nonempty}, MeasurableSet (⋂ i ∈ u, s i)
this :
  ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, (-1) ^ (#x + 1) • f a ∂μ =
    ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X), (⋂ i ∈ x, s i).indicator (fun a ↦ (-1) ^ (#x + 1) • f a) a ∂μ
⊢ ∫ (x : X), (⋃ i ∈ t, s i).indicator f x ∂μ =
    ∫ (a : X), ∑ i ∈ t.powerset with i.Nonempty, (⋂ i_1 ∈ i, s i_1).indicator (fun a ↦ (-1) ^ (#i + 1) • f a) a ∂μ

case hf
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
A : ∀ u ∈ {x ∈ t.powerset | x.Nonempty}, MeasurableSet (⋂ i ∈ u, s i)
this :
  ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, (-1) ^ (#x + 1) • f a ∂μ =
    ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X), (⋂ i ∈ x, s i).indicator (fun a ↦ (-1) ^ (#x + 1) • f a) a ∂μ
⊢ ∀ i ∈ {x ∈ t.powerset | x.Nonempty}, Integrable ((⋂ i_1 ∈ i, s i_1).indicator fun a ↦ (-1) ^ (#i + 1) • f a) μ
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ∞
δ : ℝ≥0 := ε / 2
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), f.length (s i) + ↑ε

Tactic:
have δpos : 0 < (δ : ℝ≥0∞) := by simpa [δ] using εpos.ne'

Goal state after:
R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), f.length (s i) + ↑ε
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : Countable G
h_meas : NullMeasurableSet s μ
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x ↦ g • x) μ μ
h_measure_univ_le : μ univ ≤ ∑' (g : G), μ (g • s)
aedisjoint : Pairwise (AEDisjoint μ on fun g ↦ g • s)
g : G
⊢ NullMeasurableSet (g⁻¹⁻¹ • s) μ

Tactic:
← preimage_smul

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : Countable G
h_meas : NullMeasurableSet s μ
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x ↦ g • x) μ μ
h_measure_univ_le : μ univ ≤ ∑' (g : G), μ (g • s)
aedisjoint : Pairwise (AEDisjoint μ on fun g ↦ g • s)
g : G
⊢ NullMeasurableSet ((fun x ↦ g⁻¹ • x) ⁻¹' s) μ
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure X
inst✝ : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
⊢ ∫ (x : X) in {x | f x < 0}, f x ∂μ = ∫ (x : X) in {x | f x ≤ 0}, f x ∂μ

Tactic:
by
  have h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0} := by
    simp_rw [le_iff_lt_or_eq, ofPred_or]
  rw [h_union]
  have B : NullMeasurableSet {x | f x = 0} μ :=
    hf.nullMeasurableSet_eq_fun aestronglyMeasurable_zero
  symm
  refine integral_union_eq_left_of_ae ?_
  filter_upwards [ae_restrict_mem₀ B] with x hx using hx

Goal state after: