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

Goal state before:
pp: X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝ : PseudoMetrizableSpace ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
⊢ ∃ u, IsOpen[inst✝³] u ∧ k ⊆ u ∧ IntegrableOn f u μ

Tactic:
refine IsCompact.induction_on hk ?_ ?_ ?_ ?_

Goal state after:
case refine_1
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝ : PseudoMetrizableSpace ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
⊢ ∃ u, IsOpen[inst✝³] u ∧ ∅ ⊆ u ∧ IntegrableOn f u μ

case refine_2
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝ : PseudoMetrizableSpace ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
⊢ ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ u, IsOpen[inst✝³] u ∧ t ⊆ u ∧ IntegrableOn f u μ) → ∃ u, IsOpen[inst✝³] u ∧ s ⊆ u ∧ IntegrableOn f u μ

case refine_3
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝ : PseudoMetrizableSpace ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
⊢ ∀ ⦃s t : Set X⦄,
    (∃ u, IsOpen[inst✝³] u ∧ s ⊆ u ∧ IntegrableOn f u μ) →
      (∃ u, IsOpen[inst✝³] u ∧ t ⊆ u ∧ IntegrableOn f u μ) → ∃ u, IsOpen[inst✝³] u ∧ s ∪ t ⊆ u ∧ IntegrableOn f u μ

case refine_4
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝ : PseudoMetrizableSpace ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
⊢ ∀ x ∈ k, ∃ t ∈ 𝓝[k] x, ∃ u, IsOpen[inst✝³] u ∧ t ⊆ u ∧ IntegrableOn f u μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case inl
X : Type u_1
E : Type u_6
inst✝⁹ : MeasurableSpace X
inst✝⁸ : TopologicalSpace X
inst✝⁷ : NormedAddCommGroup E
μ : Measure X
inst✝⁶ : BorelSpace X
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : ConditionallyCompleteLinearOrder E
inst✝³ : OrderTopology X
inst✝² : OrderTopology E
inst✝¹ : SecondCountableTopology E
p : ℝ≥0∞
f : X → E
inst✝ : IsFiniteMeasureOnCompacts μ
hs : IsCompact ∅
hmono : MonotoneOn f ∅
⊢ MemLp f p (μ.restrict ∅)

pp: case inr
X : Type u_1
E : Type u_6
inst✝⁹ : MeasurableSpace X
inst✝⁸ : TopologicalSpace X
inst✝⁷ : NormedAddCommGroup E
μ : Measure X
s : Set X
inst✝⁶ : BorelSpace X
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : ConditionallyCompleteLinearOrder E
inst✝³ : OrderTopology X
inst✝² : OrderTopology E
inst✝¹ : SecondCountableTopology E
p : ℝ≥0∞
f : X → E
inst✝ : IsFiniteMeasureOnCompacts μ
hs : IsCompact s
hmono : MonotoneOn f s
h : s.Nonempty
⊢ MemLp f p (μ.restrict s)

Tactic:
· simp

Goal state after:
case inr
X : Type u_1
E : Type u_6
inst✝⁹ : MeasurableSpace X
inst✝⁸ : TopologicalSpace X
inst✝⁷ : NormedAddCommGroup E
μ : Measure X
s : Set X
inst✝⁶ : BorelSpace X
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : ConditionallyCompleteLinearOrder E
inst✝³ : OrderTopology X
inst✝² : OrderTopology E
inst✝¹ : SecondCountableTopology E
p : ℝ≥0∞
f : X → E
inst✝ : IsFiniteMeasureOnCompacts μ
hs : IsCompact s
hmono : MonotoneOn f s
h : s.Nonempty
⊢ MemLp f p (μ.restrict s)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: β : Type u_2
inst✝¹ : MeasurableSpace β
p : ℝ≥0∞
E : Type u_7
inst✝ : NormedAddCommGroup E
f : β → E
μ : Measure β
hf : MemLp f p μ
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
f' : β → E := AEStronglyMeasurable.mk f ⋯
g : β →ₛ E
hg : eLpNorm (f' - ⇑g) p μ < ε
g_mem : MemLp (⇑g) p μ
x : β
hx : f x = AEStronglyMeasurable.mk f ⋯ x
⊢ (f - ⇑g) x = (f' - ⇑g) x

Tactic:
simpa only [Pi.sub_apply, sub_left_inj] using hx

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

Goal state before:
pp: 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

pp: 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

Tactic:
· simp

Goal state after:
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: 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

pp: 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

Tactic:
· simp

Goal state after:
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.FinMeasAdditive

Goal state before:
pp: case inl
α : 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) μ
hb : 0 ∈ f.range
⊢ ‖T (⇑f ⁻¹' {0})‖ * ‖0‖ ≤ C * μ.real (⇑f ⁻¹' {0}) * ‖0‖

pp: case inr
α : 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
hb : b ≠ 0
⊢ ‖T (⇑f ⁻¹' {b})‖ * ‖b‖ ≤ C * μ.real (⇑f ⁻¹' {b}) * ‖b‖

Tactic:
· simp

Goal state after:
case inr
α : 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
hb : b ≠ 0
⊢ ‖T (⇑f ⁻¹' {b})‖ * ‖b‖ ≤ C * μ.real (⇑f ⁻¹' {b}) * ‖b‖
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case e'_3
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x ↦ u x / v x - v x / v x) l (𝓝 0)
key : Tendsto (fun x ↦ v x / v x) l (𝓝 1)
x✝ : α
⊢ (u / v) x✝ = u x✝ / v x✝ - v x✝ / v x✝ + v x✝ / v x✝

pp: case e'_5
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x ↦ u x / v x - v x / v x) l (𝓝 0)
key : Tendsto (fun x ↦ v x / v x) l (𝓝 1)
⊢ 1 = 0 + 1

Tactic:
· simp

Goal state after:
case e'_5
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x ↦ u x / v x - v x / v x) l (𝓝 0)
key : Tendsto (fun x ↦ v x / v x) l (𝓝 1)
⊢ 1 = 0 + 1
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case e'_5
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x ↦ u x / v x - v x / v x) l (𝓝 0)
key : Tendsto (fun x ↦ v x / v x) l (𝓝 1)
⊢ 1 = 0 + 1

Tactic:
· simp

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

Goal state before:
pp: case e'_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst✝ : SeparableSpace ↑(range f ∪ {0})
n : ℕ
⊢ (∫⁻ (x : α), ‖(approxOn f fmeas (range f ∪ {0}) 0 ⋯ n) x - f x‖ₑ ∂μ).toReal =
    (ENNReal.toReal ∘ fun n ↦ ∫⁻ (x : α), ‖(approxOn f fmeas (range f ∪ {0}) 0 ⋯ n) x - f x‖ₑ ∂μ) n

pp: case e'_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst✝ : SeparableSpace ↑(range f ∪ {0})
n : ℕ
⊢ AEStronglyMeasurable (fun x ↦ (approxOn f fmeas (range f ∪ {0}) 0 ⋯ n) x - f x) μ

Tactic:
· simp

Goal state after:
case e'_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst✝ : SeparableSpace ↑(range f ∪ {0})
n : ℕ
⊢ AEStronglyMeasurable (fun x ↦ (approxOn f fmeas (range f ∪ {0}) 0 ⋯ n) x - f x) μ
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∫ (a : α), f a ∂μ = ∫ (a : α), ↑(f a).toNNReal - ↑(-f a).toNNReal ∂μ

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Integrable (fun a ↦ ↑(-f a).toNNReal) μ

Tactic:
· simp

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Integrable (fun a ↦ ↑(-f a).toNNReal) μ
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∫ (a : α), f a ∂μ = ∫ (a : α), ↑(f a).toNNReal ∂μ - ∫ (a : α), ↑(-f a).toNNReal ∂μ

Tactic:
by
  rw [← integral_sub hf.real_toNNReal]
  · simp
  · exact hf.neg.real_toNNReal

Goal state after:
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x ↦ a x • u x) - fun x ↦ b x • v x) =ᶠ[l] fun x ↦ b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
hc : 0 < c
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
⊢ ‖φ x • u x - v x‖ ≤ c * ‖v x‖

Tactic:
have key :=
    calc
      ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 / C * ‖u x‖ := by gcongr
      _ ≤ c / 2 / C * (C * ‖v x‖) := by gcongr
      _ = c / 2 * ‖v x‖ := by field

Goal state after:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x ↦ a x • u x) - fun x ↦ b x • v x) =ᶠ[l] fun x ↦ b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
hc : 0 < c
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
key : ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 * ‖v x‖
⊢ ‖φ x • u x - v x‖ ≤ c * ‖v x‖
Module: Mathlib.Analysis.Normed.Group.AddTorsor

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
⊢ nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ nndist p₁ p₃ + nndist p₂ p₄

Tactic:
simp only [← NNReal.coe_le_coe, NNReal.coe_add, ← dist_nndist, dist_vsub_vsub_le]

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

Goal state before:
pp: case inl
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
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddTorsor P
inst✝ : T1Space V
⊢ IsClosed ↑⊥.direction ↔ IsClosed ↑⊥

pp: case inr
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
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddTorsor P
inst✝ : T1Space V
s : AffineSubspace R P
x : P
hx : x ∈ ↑s
⊢ IsClosed ↑s.direction ↔ IsClosed ↑s

Tactic:
· simp

Goal state after:
case inr
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
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddTorsor P
inst✝ : T1Space V
s : AffineSubspace R P
x : P
hx : x ∈ ↑s
⊢ IsClosed ↑s.direction ↔ IsClosed ↑s
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝⁷ : RCLike 𝕜
𝓕 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 F
inst✝² : FunLike 𝓕 E F
inst✝¹ : AddMonoidHomClass 𝓕 E F
inst✝ : MulActionHomClass 𝓕 𝕜 E F
f : 𝓕
K : NNReal
h : ∀ (x : E), ‖x‖ = 1 → 1 ≤ ↑K * ‖f x‖
⊢ ‖0‖ ≤ ↑K * ‖f 0‖

pp: case inr
𝕜 : Type u_1
inst✝⁷ : RCLike 𝕜
𝓕 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 F
inst✝² : FunLike 𝓕 E F
inst✝¹ : AddMonoidHomClass 𝓕 E F
inst✝ : MulActionHomClass 𝓕 𝕜 E F
f : 𝓕
K : NNReal
h : ∀ (x : E), ‖x‖ = 1 → 1 ≤ ↑K * ‖f x‖
x : E
hx : x ≠ 0
⊢ ‖x‖ ≤ ↑K * ‖f x‖

Tactic:
· simp

Goal state after:
case inr
𝕜 : Type u_1
inst✝⁷ : RCLike 𝕜
𝓕 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 F
inst✝² : FunLike 𝓕 E F
inst✝¹ : AddMonoidHomClass 𝓕 E F
inst✝ : MulActionHomClass 𝓕 𝕜 E F
f : 𝓕
K : NNReal
h : ∀ (x : E), ‖x‖ = 1 → 1 ≤ ↑K * ‖f x‖
x : E
hx : x ≠ 0
⊢ ‖x‖ ≤ ↑K * ‖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
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
c : ℝ
f : ↥(α →₁ₛ[μ] E)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = SimpleFunc.setToSimpleFunc T (c • toSimpleFunc f)

Tactic:
refine SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable _) ?_

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
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
c : ℝ
f : ↥(α →₁ₛ[μ] E)
⊢ ⇑(toSimpleFunc (c • f)) =ᵐ[μ] ⇑(c • toSimpleFunc f)
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : 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 α
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
inst✝ : DistribSMul 𝕜 F
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : ↥(α →₁ₛ[μ] E)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = SimpleFunc.setToSimpleFunc T (c • toSimpleFunc f)

Tactic:
refine SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable _) ?_

Goal state after:
α : 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 α
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
inst✝ : DistribSMul 𝕜 F
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : ↥(α →₁ₛ[μ] E)
⊢ ⇑(toSimpleFunc (c • f)) =ᵐ[μ] ⇑(c • toSimpleFunc 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
s : Set α
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hs : MeasurableSet s
hμs : μ s < ∞
x : E
h_empty : T ∅ = 0
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (indicatorConst 1 hs ⋯ x)) =
    SimpleFunc.setToSimpleFunc T (SimpleFunc.piecewise s hs (SimpleFunc.const α x) (SimpleFunc.const α 0))

Tactic:
refine SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable _) ?_

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
s : Set α
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hs : MeasurableSet s
hμs : μ s < ∞
x : E
h_empty : T ∅ = 0
⊢ ⇑(toSimpleFunc (indicatorConst 1 hs ⋯ x)) =ᵐ[μ]
    ⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α x) (SimpleFunc.const α 0))
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
⊢ closedBall x (infDist x sᶜ) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
by
  rcases eq_or_ne (infDist x sᶜ) 0 with h₀ | h₀
  · rw [h₀, closedBall_zero']
    exact closure_mono (singleton_subset_iff.2 hx)
  · rw [← closure_ball x h₀]
    exact closure_mono ball_infDist_compl_subset

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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
⊢ ‖setToL1 hT‖ ≤ ↑1 * ‖setToL1SCLM α E μ hT‖

Tactic:
refine
        ContinuousLinearMap.opNorm_extend_le (setToL1SCLM α E μ hT)
          (simpleFunc.denseRange one_ne_top) fun x => le_of_eq ?_

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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
x : ↥(α →₁ₛ[μ] E)
⊢ ‖x‖ = ↑1 * ‖(coeToLp α E ℝ) x‖
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : Integrable f (Measure.sum μ)
i : ι
⊢ ∫ (x : X), ‖f x‖ ∂μ i = ∫ (a : X), ‖f a‖ₑ.toReal ∂μ i

pp: ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : Integrable f (Measure.sum μ)
i : ι
⊢ AEMeasurable (fun x ↦ ‖f x‖ₑ) (μ i)

Tactic:
· simp

Goal state after:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : Integrable f (Measure.sum μ)
i : ι
⊢ AEMeasurable (fun x ↦ ‖f x‖ₑ) (μ i)
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝⁴ : NormedAddCommGroup E
f : X → E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSingletonClass X
μ : Measure X
inst✝ : Countable X
hf : Integrable f (Measure.sum fun a ↦ μ {a} • Measure.dirac a)
⊢ ∫ (x : X), f x ∂μ = ∑' (x : X), μ.real {x} • f x

Tactic:
rw [← Measure.sum_smul_dirac μ, integral_sum_measure hf]

Goal state after:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝⁴ : NormedAddCommGroup E
f : X → E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSingletonClass X
μ : Measure X
inst✝ : Countable X
hf : Integrable f (Measure.sum fun a ↦ μ {a} • Measure.dirac a)
⊢ ∑' (i : X), ∫ (x : X), f x ∂μ {i} • Measure.dirac i =
    ∑' (x : X), (Measure.sum fun a ↦ μ {a} • Measure.dirac a).real {x} • f x
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 }
hf' : Integrable (fun x ↦ f ↑x) (Measure.comap Subtype.val μ)
⊢ ∫ (x : X) in s, f x ∂μ = ∑' (x : ↑s), μ.real {↑x} • f ↑x

Tactic:
rw [← integral_subtype_comap hs.measurableSet, integral_countable 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 : IntegrableOn f s μ
hi : Countable { x // x ∈ s }
hf' : Integrable (fun x ↦ f ↑x) (Measure.comap Subtype.val μ)
⊢ ∑' (x : ↑s), (Measure.comap Subtype.val μ).real {x} • f ↑x = ∑' (x : ↑s), μ.real {↑x} • f ↑x