mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Mul

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁸ : CommRing 𝕜
inst✝¹⁷ : LinearOrder 𝕜
inst✝¹⁶ : IsStrictOrderedRing 𝕜
inst✝¹⁵ : CommRing E
inst✝¹⁴ : LinearOrder E
inst✝¹³ : IsStrictOrderedRing E
inst✝¹² : AddCommGroup F
inst✝¹¹ : LinearOrder F
inst✝¹⁰ : IsOrderedAddMonoid F
inst✝⁹ : AddCommGroup G
inst✝⁸ : Module 𝕜 G
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : IsOrderedModule 𝕜 F
inst✝¹ : IsStrictOrderedModule E F
s : Set G
f : G → E
g : G → F
inst✝ : IsOrderedModule 𝕜 E
hf : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
x : G
hx : x ∈ s
y : G
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • (f • g) x + b • (f • g) y ≤ (f • g) (a • x + b • y)

Tactic:
dsimp

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁸ : CommRing 𝕜
inst✝¹⁷ : LinearOrder 𝕜
inst✝¹⁶ : IsStrictOrderedRing 𝕜
inst✝¹⁵ : CommRing E
inst✝¹⁴ : LinearOrder E
inst✝¹³ : IsStrictOrderedRing E
inst✝¹² : AddCommGroup F
inst✝¹¹ : LinearOrder F
inst✝¹⁰ : IsOrderedAddMonoid F
inst✝⁹ : AddCommGroup G
inst✝⁸ : Module 𝕜 G
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : IsOrderedModule 𝕜 F
inst✝¹ : IsStrictOrderedModule E F
s : Set G
f : G → E
g : G → F
inst✝ : IsOrderedModule 𝕜 E
hf : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
x : G
hx : x ∈ s
y : G
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x • g x + b • f y • g y ≤ f (a • x + b • y) • g (a • x + b • y)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
p : ℝ
f g : ι → ℝ≥0
hp : 1 ≤ p
hf_sum : Summable fun a ↦ f a ^ p
hg_sum : Summable fun a ↦ g a ^ p
⊢ (Summable fun a ↦ (f a + g a) ^ p) ∧
    (∑' (a : ι), (f a + g a) ^ p) ^ (1 / p) ≤ (∑' (a : ι), f a ^ p) ^ (1 / p) + (∑' (a : ι), g a ^ p) ^ (1 / p)

Tactic:
exact NNReal.Lp_add_le_tsum hp hf_sum hg_sum

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ˣ
⊢ (fun t ↦ (↑x + t)⁻¹ʳ) =O[𝓝 0] fun _t ↦ 1

Tactic:
refine EventuallyEq.trans_isBigO (inverse_add x) (one_mul (1 : ℝ) ▸ ?_)
  simp only [← sub_neg_eq_add, ← neg_mul]
  have hzero : Tendsto (-(↑x⁻¹ : R) * ·) (𝓝 0) (𝓝 0) :=
    (mulLeft_continuous _).tendsto' _ _ <| mul_zero _
  exact (inverse_one_sub_norm.comp_tendsto hzero).mul (isBigO_const_const _ one_ne_zero _)

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

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

Tactic:
ext f'

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
O : (E →L[𝕜] F) → E →L[𝕜] E := fun f ↦ ↑e.symm ∘SL f
h_O : Continuous O
f' : E →L[𝕜] F
⊢ f' ∈ range toContinuousLinearMap ↔ f' ∈ O ⁻¹' {x | IsUnit x}
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : μ s ≠ ∞
⊢ μ.real s = 0 ↔ μ s = 0

Tactic:
by
  rw [Measure.real, ENNReal.toReal_eq_zero_iff]
  exact or_iff_left h

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
⊢ (eLpNorm (s.indicator fun x ↦ c) p μ).toReal ≤ ‖c‖ * μ.real s ^ (1 / p.toReal)

Tactic:
refine ENNReal.toReal_le_of_le_ofReal (by positivity) ?_

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
⊢ eLpNorm (s.indicator fun x ↦ c) p μ ≤ ENNReal.ofReal (‖c‖ * μ.real s ^ (1 / p.toReal))
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case inl
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑f
h✝ : IsEmpty ι
⊢ ∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖

Tactic:
refine ⟨‖f 0‖ + 1, add_pos_of_nonneg_of_pos (norm_nonneg _) zero_lt_one, fun m => ?_⟩

Goal state after:
case inl
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑f
h✝ : IsEmpty ι
m : (i : ι) → E i
⊢ ‖f m‖ ≤ (‖f 0‖ + 1) * ∏ i, ‖m i‖
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ENormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : NullMeasurableSet t μ
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u μ
v : Set α := toMeasurable μ u
⊢ Integrable f (μ.restrict u)

pp: α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ENormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : NullMeasurableSet t μ
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u μ
v : Set α := toMeasurable μ u
⊢ ∀ x ∈ u, ‖f x‖ₑ ≠ 0

Tactic:
· exact hu

Goal state after:
α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ENormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : NullMeasurableSet t μ
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u μ
v : Set α := toMeasurable μ u
⊢ ∀ x ∈ u, ‖f x‖ₑ ≠ 0
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec : ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
A : (insert i s).piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₂ i)
B : s.piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₁ i)
⊢ ‖f (update (s.piecewise m₂ m₁) i (m₁ i - m₂ i))‖ ≤ C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
apply le_trans (H _)

Goal state after:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec : ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
A : (insert i s).piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₂ i)
B : s.piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₁ i)
⊢ C * ∏ i_1, ‖update (s.piecewise m₂ m₁) i (m₁ i - m₂ i) i_1‖ ≤
    C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case pos
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec : ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
A : (insert i s).piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₂ i)
B : s.piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₁ i)
j : ι
a✝ : j ∈ univ
h : j = i
⊢ ‖update (s.piecewise m₂ m₁) i (m₁ i - m₂ i) j‖ ≤ if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
rw [h]
          simp

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

Goal state before:
pp: case neg
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec : ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
A : (insert i s).piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₂ i)
B : s.piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₁ i)
j : ι
a✝ : j ∈ univ
h : ¬j = i
⊢ ‖update (s.piecewise m₂ m₁) i (m₁ i - m₂ i) j‖ ≤ if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
by_cases h' : j ∈ s <;> simp [h', h]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
r : ℝ
u : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
x : α
h : ↑(f x) ≠ 0 → ↑↑(r • u) x = (r • ↑↑u) x
h' : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑(r • u) x) ⋯) x = f x • ↑↑(r • u) x
h'' : ↑↑(r • MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x = (r • ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯)) x
h''' : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x = f x • ↑↑u x
hx : f x = 0
⊢ f x • ↑↑(r • u) x = r • f x • ↑↑u x

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
r : ℝ
u : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
x : α
h : ↑(f x) ≠ 0 → ↑↑(r • u) x = (r • ↑↑u) x
h' : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑(r • u) x) ⋯) x = f x • ↑↑(r • u) x
h'' : ↑↑(r • MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x = (r • ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯)) x
h''' : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x = f x • ↑↑u x
hx : f x ≠ 0
⊢ f x • ↑↑(r • u) x = r • f x • ↑↑u x

Tactic:
· simp only [hx, zero_smul, smul_zero]

Goal state after:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
r : ℝ
u : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
x : α
h : ↑(f x) ≠ 0 → ↑↑(r • u) x = (r • ↑↑u) x
h' : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑(r • u) x) ⋯) x = f x • ↑↑(r • u) x
h'' : ↑↑(r • MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x = (r • ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯)) x
h''' : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x = f x • ↑↑u x
hx : f x ≠ 0
⊢ f x • ↑↑(r • u) x = r • f x • ↑↑u x
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
H : Type u_8
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f μ'
hf : StronglyMeasurable f
⊢ HasFiniteIntegral f (μ'.trim hm)

Tactic:
rw [HasFiniteIntegral, lintegral_trim hm _]

Goal state after:
α : Type u_1
m : MeasurableSpace α
H : Type u_8
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f μ'
hf : StronglyMeasurable f
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ' < ∞

α : Type u_1
m : MeasurableSpace α
H : Type u_8
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f μ'
hf : StronglyMeasurable f
⊢ Measurable fun a ↦ ‖f a‖ₑ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
ε : Type u_3
ε' : Type u_4
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : X → ε
μ : Measure X
s : Set X
hf : LocallyIntegrableOn f s μ
g : X → ε'
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ₑ ≤ ‖f x‖ₑ
⊢ LocallyIntegrableOn g s μ

Tactic:
by
  intro x hx
  rcases hf x hx with ⟨t, t_mem, ht⟩
  exact ⟨t, t_mem, ht.mono_enorm hg.restrict (ae_restrict_of_ae h)⟩

Goal state after:
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 ι
f : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')
x : G
m : (i : ι) → E i
⊢ ‖({ toFun := fun x ↦ { toFun := fun m ↦ (f m) x, map_update_add' := ⋯, map_update_smul' := ⋯ }, map_add' := ⋯,
            map_smul' := ⋯ }
          x)
        m‖ ≤
    ‖f‖ * ‖x‖ * ∏ i, ‖m i‖

Tactic:
rw [LinearMap.coe_mk, AddHom.coe_mk, MultilinearMap.coe_mk, mul_right_comm]

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 ι
f : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')
x : G
m : (i : ι) → E i
⊢ ‖(f m) x‖ ≤ (‖f‖ * ∏ i, ‖m i‖) * ‖x‖
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 ι
⊢ (G →L[𝕜] ContinuousMultilinearMap 𝕜 E G') ≃L[𝕜] ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')

Tactic:
by
  refine (flipMultilinearEquivₗ 𝕜 E G G').toContinuousLinearEquivOfBounds 1 1 ?_ ?_
  · intro f
    suffices ‖f.flipMultilinear‖ ≤ ‖f‖ by simpa
    apply MultilinearMap.mkContinuous_norm_le
    positivity
  · intro f
    suffices ‖f.flipLinear‖ ≤ ‖f‖ by simpa
    apply MultilinearMap.mkContinuousLinear_norm_le
    positivity

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

Goal state before:
pp: β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x ↦ y₀) p μ
n : ℕ
this✝ : eLpNorm (fun x ↦ (approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ∞
this : MemLp (fun x ↦ (approxOn f fmeas s y₀ h₀ n) x - y₀) p μ
⊢ eLpNorm (⇑(approxOn f fmeas s y₀ h₀ n)) p μ < ∞

Tactic:
convert! eLpNorm_add_lt_top this hi₀

Goal state after:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x ↦ y₀) p μ
n : ℕ
this✝ : eLpNorm (fun x ↦ (approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ∞
this : MemLp (fun x ↦ (approxOn f fmeas s y₀ h₀ n) x - y₀) p μ
⊢ ⇑(approxOn f fmeas s y₀ h₀ n) = (fun x ↦ (approxOn f fmeas s y₀ h₀ n) x - y₀) + fun x ↦ y₀
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝ : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
f : ↥(Lp E p μ)
hfi' : MemLp (↑↑f) p μ
this : SeparableSpace ↑(Set.range ↑↑f ∪ {0})
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range Subtype.val) ∧ Tendsto x atTop (𝓝 f)

Tactic:
refine
    ⟨fun n =>
      toLp
        (SimpleFunc.approxOn f (Lp.stronglyMeasurable f).measurable (range f ∪ {0}) 0 _ n)
        (SimpleFunc.memLp_approxOn_range (Lp.stronglyMeasurable f).measurable hfi' n),
      fun n => mem_range_self _, ?_⟩

Goal state after:
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝ : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
f : ↥(Lp E p μ)
hfi' : MemLp (↑↑f) p μ
this : SeparableSpace ↑(Set.range ↑↑f ∪ {0})
⊢ Tendsto (fun n ↦ ↑((approxOn ↑↑f ⋯ (Set.range ↑↑f ∪ {0}) 0 ⋯ n).toLp ⋯)) atTop (𝓝 f)
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: case refine_2
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ {x ∈ f.range | x ≠ 0}
⊢ μ.real (⇑(piecewise s hs f 0) ⁻¹' {y}) • y = (μ.restrict s).real (⇑f ⁻¹' {y}) • y

Tactic:
dsimp

Goal state after:
case refine_2
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ {x ∈ f.range | x ≠ 0}
⊢ μ.real (s.piecewise (⇑f) 0 ⁻¹' {y}) • y = (μ.restrict s).real (⇑f ⁻¹' {y}) • 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 T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T' s = c • T s
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ setToSimpleFunc T' f = c • setToSimpleFunc T f

Tactic:
simp_rw [setToSimpleFunc_eq_sum_filter]
  suffices ∀ x ∈ {x ∈ f.range | x ≠ 0}, T' (f ⁻¹' {x}) = c • T (f ⁻¹' {x}) by
    rw [smul_sum]
    refine Finset.sum_congr rfl fun x hx => ?_
    rw [this x hx, _root_.smul_apply]
  intro x hx
  refine
    h_smul (f ⁻¹' {x}) (measurableSet_preimage _ _) (measure_preimage_lt_top_of_integrable _ hf ?_)
  rw [mem_filter] at hx
  exact hx.2

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

Goal state before:
pp: case pos
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : x = 0
⊢ ∑ x_1 ∈ {x, 0}, (T (⇑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 = (T s) x

pp: case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ∑ x_1 ∈ {x, 0}, (T (⇑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 = (T s) x

Tactic:
· simp_rw [hx0]; simp

Goal state after:
case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ∑ x_1 ∈ {x, 0}, (T (⇑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 = (T s) x
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
⊢ 0 =o[l] u

Tactic:
exact isLittleO_zero _ _

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
f' : ℕ → α → ℝ := fun n x ↦ f n x - f 0 x
hf'_nonneg : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), 0 ≤ f' n x
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
this : Tendsto (fun n ↦ ∫ (x : α), f n x - f 0 x ∂μ) atTop (𝓝 (∫ (x : α), (F - f 0) x ∂μ))
⊢ Tendsto (fun n ↦ ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F x ∂μ))

Tactic:
integral_sub (hf _) (hf _),

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
f' : ℕ → α → ℝ := fun n x ↦ f n x - f 0 x
hf'_nonneg : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), 0 ≤ f' n x
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
this : Tendsto (fun n ↦ ∫ (a : α), f n a ∂μ - ∫ (a : α), f 0 a ∂μ) atTop (𝓝 (∫ (x : α), (F - f 0) x ∂μ))
⊢ Tendsto (fun n ↦ ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F x ∂μ))