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

Goal state before:
pp: X : Type u_1
E : Type u_6
F : Type u_7
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure X
s : Set X
f : X → E
hf : LocallyIntegrableOn f s μ
g : X → F
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖
x : X
hx : x ∈ s
t : Set X
t_mem : t ∈ 𝓝[s] x
ht : IntegrableOn f t μ
⊢ IntegrableAtFilter g (𝓝[s] x) μ

Tactic:
exact ⟨t, t_mem, Integrable.mono ht hg.restrict (ae_restrict_of_ae h)⟩

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

Goal state before:
pp: case neg
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁴ : PartialOrder α
inst✝³ : MeasurableSingletonClass α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
ha : μ {a} ≠ ∞
ha' : ‖f a‖ₑ ≠ ∞
hab : ¬a < b
⊢ IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ

Tactic:
· rw [Ioo_eq_empty hab, Ico_eq_empty hab]

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

Goal state before:
pp: case h₁
𝕜 : 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 : ContinuousMultilinearMap 𝕜 E 𝕜
z : G
m : (i : ι) → E i
⊢ ‖LinearMap.id (f.toMultilinearMap m)‖₊ ≤ ‖f‖₊ * ∏ i, ‖m i‖₊

Tactic:
exact le_opNNNorm _ _

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

Goal state before:
pp: case pos
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsClosed[inst✝³] s
hf : LocallyIntegrableOn f s μ
x : X
h : x ∈ s
⊢ IntegrableAtFilter f (𝓝 x) (μ.restrict s)

pp: case neg
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsClosed[inst✝³] s
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
⊢ IntegrableAtFilter f (𝓝 x) (μ.restrict s)

Tactic:
· obtain ⟨t, ht_nhds, ht_int⟩ := hf x h
    obtain ⟨u, hu_o, hu_x, hu_sub⟩ := mem_nhdsWithin.mp ht_nhds
    refine ⟨u, hu_o.mem_nhds hu_x, ?_⟩
    rw [IntegrableOn, restrict_restrict hu_o.measurableSet]
    exact ht_int.mono_set hu_sub

Goal state after:
case neg
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsClosed[inst✝³] s
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
⊢ IntegrableAtFilter f (𝓝 x) (μ.restrict s)
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 : ContinuousMultilinearMap 𝕜 E₁ G
⊢ ∀ [inst : DecidableEq ι] (m : (i : ι) → E i →L[𝕜] E₁ i) (i : ι) (x y : E i →L[𝕜] E₁ i),
    g.compContinuousLinearMap (update m i (x + y)) =
      g.compContinuousLinearMap (update m i x) + g.compContinuousLinearMap (update m i y)

Tactic:
intro h

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 ι
g : ContinuousMultilinearMap 𝕜 E₁ G
h : DecidableEq ι
⊢ ∀ (m : (i : ι) → E i →L[𝕜] E₁ i) (i : ι) (x y : E i →L[𝕜] E₁ i),
    g.compContinuousLinearMap (update m i (x + y)) =
      g.compContinuousLinearMap (update m i x) + g.compContinuousLinearMap (update m i y)
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 : ContinuousMultilinearMap 𝕜 E₁ G
⊢ ∀ [inst : DecidableEq ι] (m : (i : ι) → E i →L[𝕜] E₁ i) (i : ι) (c : 𝕜) (x : E i →L[𝕜] E₁ i),
    g.compContinuousLinearMap (update m i (c • x)) = c • g.compContinuousLinearMap (update m i x)

Tactic:
intro h

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 ι
g : ContinuousMultilinearMap 𝕜 E₁ G
h : DecidableEq ι
⊢ ∀ (m : (i : ι) → E i →L[𝕜] E₁ i) (i : ι) (c : 𝕜) (x : E i →L[𝕜] E₁ i),
    g.compContinuousLinearMap (update m i (c • x)) = c • g.compContinuousLinearMap (update m i x)
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case mp
X : Type u_1
ε : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝⁴ : PseudoMetrizableSpace ε
a : X
inst✝³ : LinearOrder X
inst✝² : CompactIccSpace X
inst✝¹ : NoMinOrder X
inst✝ : OrderTopology X
⊢ IntegrableOn f (Iio a) μ →
    IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ

Tactic:
intro h

Goal state after:
case mp
X : Type u_1
ε : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝⁴ : PseudoMetrizableSpace ε
a : X
inst✝³ : LinearOrder X
inst✝² : CompactIccSpace X
inst✝¹ : NoMinOrder X
inst✝ : OrderTopology X
h : IntegrableOn f (Iio a) μ
⊢ IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞
hp0 : ¬p = 0
hp_top : ¬p = ∞
y : E
x✝ : y ∈ f.range
hy0 : ¬y = 0
⊢ ‖y‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {y}) < ∞

Tactic:
refine ENNReal.mul_lt_top ?_ (hf y hy0)

Goal state after:
case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞
hp0 : ¬p = 0
hp_top : ¬p = ∞
y : E
x✝ : y ∈ f.range
hy0 : ¬y = 0
⊢ ‖y‖ₑ ^ p.toReal < ∞
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case h
α : 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 α
f g : ↥(Lp E p μ)
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hs : AEEqFun.mk ⇑s ⋯ = ↑f
t : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
ht : AEEqFun.mk ⇑t ⋯ = ↑g
⊢ AEEqFun.mk ⇑(s + t) ⋯ = ↑(f + g)

Tactic:
simp only [← hs, ← ht, AEEqFun.mk_add_mk, AddSubgroup.coe_add,
      SimpleFunc.coe_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 : ↥(simpleFunc E p μ)
a✝ : α
⊢ (toSimpleFunc (f + g)) a✝ = ↑(↑↑f + ↑↑g) a✝ →
    (toSimpleFunc f) a✝ = ↑↑↑f a✝ →
      (toSimpleFunc g) a✝ = ↑↑↑g a✝ →
        ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + ↑↑↑g a✝ → (toSimpleFunc (f + g)) a✝ = (toSimpleFunc f) a✝ + (toSimpleFunc g) a✝

Tactic:
intro h

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a✝ : α
h : (toSimpleFunc (f + g)) a✝ = ↑(↑↑f + ↑↑g) a✝
⊢ (toSimpleFunc f) a✝ = ↑↑↑f a✝ →
    (toSimpleFunc g) a✝ = ↑↑↑g a✝ →
      ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + ↑↑↑g a✝ → (toSimpleFunc (f + g)) a✝ = (toSimpleFunc f) a✝ + (toSimpleFunc g) a✝
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
𝕜 : Type u_6
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝³ : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
inst✝² : SeminormedAddGroup 𝕜
inst✝¹ : DistribSMul 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
hT : DominatedFinMeasAdditive μ T C
c : 𝕜
⊢ DominatedFinMeasAdditive μ (fun s ↦ c • T s) (‖c‖ * C)

Tactic:
by
  refine ⟨hT.1.smul c, fun s hs hμs => (norm_smul_le _ _).trans ?_⟩
  rw [mul_assoc]
  exact mul_le_mul le_rfl (hT.2 s hs hμs) (norm_nonneg _) (norm_nonneg _)

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 : ↥(simpleFunc E p μ)
a✝ : α
h : (toSimpleFunc (f + g)) a✝ = ↑(↑↑f + ↑↑g) a✝
⊢ (toSimpleFunc f) a✝ = ↑↑↑f a✝ →
    (toSimpleFunc g) a✝ = ↑↑↑g a✝ →
      ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + ↑↑↑g a✝ → ↑(↑↑f + ↑↑g) a✝ = (toSimpleFunc f) a✝ + (toSimpleFunc g) a✝

Tactic:
intro h

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a✝ : α
h✝ : (toSimpleFunc (f + g)) a✝ = ↑(↑↑f + ↑↑g) a✝
h : (toSimpleFunc f) a✝ = ↑↑↑f a✝
⊢ (toSimpleFunc g) a✝ = ↑↑↑g a✝ →
    ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + ↑↑↑g a✝ → ↑(↑↑f + ↑↑g) a✝ = (toSimpleFunc f) a✝ + (toSimpleFunc g) a✝
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 : ↥(simpleFunc E p μ)
a✝ : α
h✝ : (toSimpleFunc (f + g)) a✝ = ↑(↑↑f + ↑↑g) a✝
h : (toSimpleFunc f) a✝ = ↑↑↑f a✝
⊢ (toSimpleFunc g) a✝ = ↑↑↑g a✝ → ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + ↑↑↑g a✝ → ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + (toSimpleFunc g) a✝

Tactic:
intro h

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a✝ : α
h✝¹ : (toSimpleFunc (f + g)) a✝ = ↑(↑↑f + ↑↑g) a✝
h✝ : (toSimpleFunc f) a✝ = ↑↑↑f a✝
h : (toSimpleFunc g) a✝ = ↑↑↑g a✝
⊢ ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + ↑↑↑g a✝ → ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + (toSimpleFunc g) a✝
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 : ↥(simpleFunc E p μ)
a✝ : α
h✝¹ : (toSimpleFunc (f + g)) a✝ = ↑(↑↑f + ↑↑g) a✝
h✝ : (toSimpleFunc f) a✝ = ↑↑↑f a✝
h : (toSimpleFunc g) a✝ = ↑↑↑g a✝
⊢ ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + ↑↑↑g a✝ → ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + ↑↑↑g a✝

Tactic:
intro h

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a✝ : α
h✝² : (toSimpleFunc (f + g)) a✝ = ↑(↑↑f + ↑↑g) a✝
h✝¹ : (toSimpleFunc f) a✝ = ↑↑↑f a✝
h✝ : (toSimpleFunc g) a✝ = ↑↑↑g a✝
h : ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + ↑↑↑g a✝
⊢ ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + ↑↑↑g a✝
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 : ↥(simpleFunc E p μ)
a✝ : α
⊢ (toSimpleFunc (-f)) a✝ = ↑(-↑↑f) a✝ →
    (toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑(-↑↑f) a✝ = -↑↑↑f a✝ → (toSimpleFunc (-f)) a✝ = -(toSimpleFunc f) a✝

Tactic:
intro h

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
a✝ : α
h : (toSimpleFunc (-f)) a✝ = ↑(-↑↑f) a✝
⊢ (toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑(-↑↑f) a✝ = -↑↑↑f a✝ → (toSimpleFunc (-f)) a✝ = -(toSimpleFunc f) a✝
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 : ↥(simpleFunc E p μ)
a✝ : α
h : (toSimpleFunc (-f)) a✝ = ↑(-↑↑f) a✝
⊢ (toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑(-↑↑f) a✝ = -↑↑↑f a✝ → ↑(-↑↑f) a✝ = -(toSimpleFunc f) a✝

Tactic:
intro h

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
a✝ : α
h✝ : (toSimpleFunc (-f)) a✝ = ↑(-↑↑f) a✝
h : (toSimpleFunc f) a✝ = ↑↑↑f a✝
⊢ ↑(-↑↑f) a✝ = -↑↑↑f a✝ → ↑(-↑↑f) a✝ = -(toSimpleFunc f) a✝
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 : ↥(simpleFunc E p μ)
a✝ : α
h✝ : (toSimpleFunc (-f)) a✝ = ↑(-↑↑f) a✝
h : (toSimpleFunc f) a✝ = ↑↑↑f a✝
⊢ ↑(-↑↑f) a✝ = -↑↑↑f a✝ → ↑(-↑↑f) a✝ = -↑↑↑f a✝

Tactic:
intro h

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
a✝ : α
h✝¹ : (toSimpleFunc (-f)) a✝ = ↑(-↑↑f) a✝
h✝ : (toSimpleFunc f) a✝ = ↑↑↑f a✝
h : ↑(-↑↑f) a✝ = -↑↑↑f a✝
⊢ ↑(-↑↑f) a✝ = -↑↑↑f a✝
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:

Tactic:
intro h

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 : ↥(simpleFunc E p μ)
a✝ : α
⊢ (toSimpleFunc (f - g)) a✝ = ↑(↑↑f - ↑↑g) a✝ →
    (toSimpleFunc f) a✝ = ↑↑↑f a✝ →
      (toSimpleFunc g) a✝ = ↑↑↑g a✝ →
        ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝ → (toSimpleFunc (f - g)) a✝ = (toSimpleFunc f) a✝ - (toSimpleFunc g) a✝

Tactic:
intro h

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a✝ : α
h : (toSimpleFunc (f - g)) a✝ = ↑(↑↑f - ↑↑g) a✝
⊢ (toSimpleFunc f) a✝ = ↑↑↑f a✝ →
    (toSimpleFunc g) a✝ = ↑↑↑g a✝ →
      ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝ → (toSimpleFunc (f - g)) a✝ = (toSimpleFunc f) a✝ - (toSimpleFunc g) a✝
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 : ↥(simpleFunc E p μ)
a✝ : α
h : (toSimpleFunc (f - g)) a✝ = ↑(↑↑f - ↑↑g) a✝
⊢ (toSimpleFunc f) a✝ = ↑↑↑f a✝ →
    (toSimpleFunc g) a✝ = ↑↑↑g a✝ →
      ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝ → ↑(↑↑f - ↑↑g) a✝ = (toSimpleFunc f) a✝ - (toSimpleFunc g) a✝

Tactic:
intro h

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a✝ : α
h✝ : (toSimpleFunc (f - g)) a✝ = ↑(↑↑f - ↑↑g) a✝
h : (toSimpleFunc f) a✝ = ↑↑↑f a✝
⊢ (toSimpleFunc g) a✝ = ↑↑↑g a✝ →
    ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝ → ↑(↑↑f - ↑↑g) a✝ = (toSimpleFunc f) a✝ - (toSimpleFunc g) a✝
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 : ↥(simpleFunc E p μ)
a✝ : α
h✝ : (toSimpleFunc (f - g)) a✝ = ↑(↑↑f - ↑↑g) a✝
h : (toSimpleFunc f) a✝ = ↑↑↑f a✝
⊢ (toSimpleFunc g) a✝ = ↑↑↑g a✝ → ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝ → ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - (toSimpleFunc g) a✝

Tactic:
intro h

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a✝ : α
h✝¹ : (toSimpleFunc (f - g)) a✝ = ↑(↑↑f - ↑↑g) a✝
h✝ : (toSimpleFunc f) a✝ = ↑↑↑f a✝
h : (toSimpleFunc g) a✝ = ↑↑↑g a✝
⊢ ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝ → ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - (toSimpleFunc g) a✝
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 : ↥(simpleFunc E p μ)
a✝ : α
h✝¹ : (toSimpleFunc (f - g)) a✝ = ↑(↑↑f - ↑↑g) a✝
h✝ : (toSimpleFunc f) a✝ = ↑↑↑f a✝
h : (toSimpleFunc g) a✝ = ↑↑↑g a✝
⊢ ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝ → ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝

Tactic:
intro h

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a✝ : α
h✝² : (toSimpleFunc (f - g)) a✝ = ↑(↑↑f - ↑↑g) a✝
h✝¹ : (toSimpleFunc f) a✝ = ↑↑↑f a✝
h✝ : (toSimpleFunc g) a✝ = ↑↑↑g a✝
h : ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝
⊢ ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(simpleFunc E p μ)
a✝ : α
⊢ (toSimpleFunc (k • f)) a✝ = ↑↑(k • ↑f) a✝ →
    (toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝ → (toSimpleFunc (k • f)) a✝ = k • (toSimpleFunc f) a✝

Tactic:
intro h

Goal state after:
α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(simpleFunc E p μ)
a✝ : α
h : (toSimpleFunc (k • f)) a✝ = ↑↑(k • ↑f) a✝
⊢ (toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝ → (toSimpleFunc (k • f)) a✝ = k • (toSimpleFunc f) a✝
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(simpleFunc E p μ)
a✝ : α
h : (toSimpleFunc (k • f)) a✝ = ↑↑(k • ↑f) a✝
⊢ (toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = k • (toSimpleFunc f) a✝

Tactic:
intro h

Goal state after:
α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(simpleFunc E p μ)
a✝ : α
h✝ : (toSimpleFunc (k • f)) a✝ = ↑↑(k • ↑f) a✝
h : (toSimpleFunc f) a✝ = ↑↑↑f a✝
⊢ ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = k • (toSimpleFunc f) a✝
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(simpleFunc E p μ)
a✝ : α
h✝ : (toSimpleFunc (k • f)) a✝ = ↑↑(k • ↑f) a✝
h : (toSimpleFunc f) a✝ = ↑↑↑f a✝
⊢ ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝

Tactic:
intro h

Goal state after:
α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(simpleFunc E p μ)
a✝ : α
h✝¹ : (toSimpleFunc (k • f)) a✝ = ↑↑(k • ↑f) a✝
h✝ : (toSimpleFunc f) a✝ = ↑↑↑f a✝
h : ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝
⊢ ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P (simpleFunc.indicatorConst p hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ),
    Disjoint (support ⇑f) (support ⇑g) → P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
f : ↥(simpleFunc E p μ)
this : ∀ (f : α →ₛ E) (hf : MemLp (⇑f) p μ), P (f.toLp hf)
⊢ P f

Tactic:
rw [← toLp_toSimpleFunc f]

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P (simpleFunc.indicatorConst p hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ),
    Disjoint (support ⇑f) (support ⇑g) → P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
f : ↥(simpleFunc E p μ)
this : ∀ (f : α →ₛ E) (hf : MemLp (⇑f) p μ), P (f.toLp hf)
⊢ P ((toSimpleFunc f).toLp ⋯)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝² : MeasurableSpace G := borel G
this✝¹ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this✝ : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n ↦ approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp (⇑(x n)) p μ
h_toLp : ∀ (n : ℕ), ↑↑(MemLp.toLp ⇑(x n) ⋯) =ᵐ[μ] ⇑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
hx_tendsto : Tendsto (fun n ↦ eLpNorm (⇑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
this : Tendsto (fun n ↦ ↑((x n).toLp ⋯)) atTop (𝓝 ↑g)
⊢ Tendsto (fun n ↦ coeSimpleFuncNonnegToLpNonneg p μ G ⟨(x n).toLp ⋯, ⋯⟩) atTop (𝓝 g)

Tactic:
by
    rw [tendsto_iff_dist_tendsto_zero] at this ⊢
    simp_rw [Subtype.dist_eq]
    exact this

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

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
f g : α →ₛ E
hf : Integrable (⇑f) μ
h : μ {a | ¬f a = g a} = 0
x y : E
hxy : x ≠ y
z : α
⊢ f z = x ∧ g z = y → ¬f z = g z

Tactic:
intro h

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
f g : α →ₛ E
hf : Integrable (⇑f) μ
h✝ : μ {a | ¬f a = g a} = 0
x y : E
hxy : x ≠ y
z : α
h : f z = x ∧ g z = y
⊢ ¬f z = g z