mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case refine_1
𝕜 : 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 ι
⊢ ∀ (x : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'), ‖(flipMultilinearEquivₗ 𝕜 E G G') x‖ ≤ 1 * ‖x‖

Tactic:
intro f

Goal state after:
case refine_1
𝕜 : 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 : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
⊢ ‖(flipMultilinearEquivₗ 𝕜 E G G') f‖ ≤ 1 * ‖f‖
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case refine_2
𝕜 : 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 ι
⊢ ∀ (x : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')), ‖(flipMultilinearEquivₗ 𝕜 E G G').symm x‖ ≤ 1 * ‖x‖

Tactic:
intro f

Goal state after:
case refine_2
𝕜 : 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')
⊢ ‖(flipMultilinearEquivₗ 𝕜 E G G').symm f‖ ≤ 1 * ‖f‖
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
t : Set X
ht_nhds : t ∈ 𝓝[s] x
ht_int : IntegrableOn f t μ
u : Set X
hu_o : IsOpen[inst✝³] u
hu_x : x ∈ u
hu_sub : u ∩ s ⊆ t
⊢ Integrable f ((μ.restrict s).restrict u)

Tactic:
restrict_restrict hu_o.measurableSet

Goal state after:
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
t : Set X
ht_nhds : t ∈ 𝓝[s] x
ht_int : IntegrableOn f t μ
u : Set X
hu_o : IsOpen[inst✝³] u
hu_x : x ∈ u
hu_sub : u ∩ s ⊆ t
⊢ Integrable f (μ.restrict (u ∩ s))
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 ε
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ
s : Set X
hsl : s ∈ atBot
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Iic a) μ
⊢ IntegrableOn f (Iic a) μ

Tactic:
have : Nonempty X := Nonempty.intro a

Goal state after:
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
x✝ : IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ
s : Set X
hsl : s ∈ atBot
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Iic a) μ
this : Nonempty X
⊢ IntegrableOn f (Iic a) μ
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case add
α : 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 g : α →ₛ E⦄,
    Disjoint (support ⇑f) (support ⇑g) →
      (∀ (hf : MemLp (⇑f) p μ), P (f.toLp hf)) →
        (∀ (hf : MemLp (⇑g) p μ), P (g.toLp hf)) → ∀ (hf : MemLp (⇑(f + g)) p μ), P ((f + g).toLp hf)

Tactic:
intro f

Goal state after:
case add
α : 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 : α →ₛ E
⊢ ∀ ⦃g : α →ₛ E⦄,
    Disjoint (support ⇑f) (support ⇑g) →
      (∀ (hf : MemLp (⇑f) p μ), P (f.toLp hf)) →
        (∀ (hf : MemLp (⇑g) p μ), P (g.toLp hf)) → ∀ (hf : MemLp (⇑(f + g)) p μ), P ((f + g).toLp hf)
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 := ⋯
this✝ : BorelSpace E
⊢ DenseRange Subtype.val

Tactic:
intro f

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 μ)
⊢ f ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range Subtype.val)
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] E)
⊢ ‖f‖ = SimpleFunc.integral μ (SimpleFunc.map norm (toSimpleFunc f))

Tactic:
by
  rw [norm_eq_sum_mul f, (toSimpleFunc f).map_integral norm (SimpleFunc.integrable f) norm_zero]
  simp_rw [smul_eq_mul]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hsf : AEEqFun.mk ⇑s ⋯ = ↑f
⊢ Lp.posPart ↑⟨f, ⋯⟩ ∈ (α →₁ₛ[μ] ℝ)

Tactic:
use s.posPart

Goal state after:
case h
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hsf : AEEqFun.mk ⇑s ⋯ = ↑f
⊢ AEEqFun.mk ⇑s.posPart ⋯ = ↑(Lp.posPart ↑⟨f, ⋯⟩)
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
f : ↥(α →₁ₛ[μ] E)
⊢ ‖MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f)‖ ≤
    MeasureTheory.SimpleFunc.integral μ (SimpleFunc.map norm (toSimpleFunc f))

Tactic:
exact (toSimpleFunc f).norm_integral_le_integral_norm (SimpleFunc.integrable f)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
eq : ∀ (a : α), (toSimpleFunc f).posPart a = max ((toSimpleFunc f) a) 0
ae_eq : ∀ᵐ (a : α) ∂μ, (toSimpleFunc (posPart f)) a = max ((toSimpleFunc f) a) 0
a : α
h : (toSimpleFunc (posPart f)) a = max ((toSimpleFunc f) a) 0
⊢ (toSimpleFunc (posPart f)) a = (toSimpleFunc f).posPart a

Tactic:
rw [h, eq]

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
f : ↥(Lp E 1 μ)
⊢ ∀ (a : ↥(α →₁ₛ[μ] E)), integral ↑a = (integralCLM' 𝕜) ↑a

Tactic:
intro f

Goal state after:
α : 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
f✝ : ↥(Lp E 1 μ)
f : ↥(α →₁ₛ[μ] E)
⊢ integral ↑f = (integralCLM' 𝕜) ↑f
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → motive (s.indicator fun x ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f | motive ↑↑f}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
⊢ ∀ ⦃f g : α →ₛ E⦄,
    Disjoint (support ⇑f) (support ⇑g) →
      (MemLp (⇑f) p μ → motive ⇑f) → (MemLp (⇑g) p μ → motive ⇑g) → MemLp (⇑(f + g)) p μ → motive ⇑(f + g)

Tactic:
intro f

Goal state after:
case add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → motive (s.indicator fun x ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f | motive ↑↑f}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
f : α →ₛ E
⊢ ∀ ⦃g : α →ₛ E⦄,
    Disjoint (support ⇑f) (support ⇑g) →
      (MemLp (⇑f) p μ → motive ⇑f) → (MemLp (⇑g) p μ → motive ⇑g) → MemLp (⇑(f + g)) p μ → motive ⇑(f + g)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → motive (s.indicator fun x ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f | motive ↑↑f}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
this : ∀ (f : α →ₛ E), MemLp (⇑f) p μ → motive ⇑f
⊢ ∀ (f : ↥(Lp.simpleFunc E p μ)), motive ↑↑↑f

Tactic:
intro f

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → motive (s.indicator fun x ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f | motive ↑↑f}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
this : ∀ (f : α →ₛ E), MemLp (⇑f) p μ → motive ⇑f
f : ↥(Lp.simpleFunc E p μ)
⊢ motive ↑↑↑f
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
f_nn : 0 ≤ᵐ[μ] f
⊢ ENNReal.ofReal (∫ (x : α), f x ∂μ) = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ

Tactic:
have : f =ᵐ[μ] (‖f ·‖) := f_nn.mono fun _x hx ↦ (abs_of_nonneg hx).symm
  simp_rw [integral_congr_ae this, ofReal_integral_norm_eq_lintegral_enorm hfi,
    ← ofReal_norm]
  exact lintegral_congr_ae (this.symm.fun_comp ENNReal.ofReal)

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

Goal state before:
pp: case inr.add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
⊢ ∀ ⦃f g : α →ₛ E⦄,
    Disjoint (support ⇑f) (support ⇑g) →
      (∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f) p μ → ∃ g, eLpNorm (⇑f - g) p μ ≤ δ ∧ P g) →
        (∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑g) p μ → ∃ g_1, eLpNorm (⇑g - g_1) p μ ≤ δ ∧ P g_1) →
          ∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑(f + g)) p μ → ∃ g_1, eLpNorm (⇑(f + g) - g_1) p μ ≤ δ ∧ P g_1

Tactic:
intro f

Goal state after:
case inr.add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f✝ : α → E
hf : MemLp f✝ p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
f : α →ₛ E
⊢ ∀ ⦃g : α →ₛ E⦄,
    Disjoint (support ⇑f) (support ⇑g) →
      (∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f) p μ → ∃ g, eLpNorm (⇑f - g) p μ ≤ δ ∧ P g) →
        (∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑g) p μ → ∃ g_1, eLpNorm (⇑g - g_1) p μ ≤ δ ∧ P g_1) →
          ∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑(f + g)) p μ → ∃ g_1, eLpNorm (⇑(f + g) - g_1) p μ ≤ δ ∧ P g_1
Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module k V₁
inst✝⁵ : AddTorsor V₁ P₁
inst✝⁴ : TopologicalSpace P₁
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₂ P₂
inst✝ : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
⊢ ∀ ⦃a₂ : P₁ ≃ᴬ[k] P₂⦄, e.toContinuousAffineMap = a₂.toContinuousAffineMap → e = a₂

Tactic:
e'

Goal state after:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module k V₁
inst✝⁵ : AddTorsor V₁ P₁
inst✝⁴ : TopologicalSpace P₁
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₂ P₂
inst✝ : TopologicalSpace P₂
e e' : P₁ ≃ᴬ[k] P₂
⊢ e.toContinuousAffineMap = e'.toContinuousAffineMap → e = e'
Module: Mathlib.Topology.Algebra.AffineSubspace

Goal state before:
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 (⇑(Homeomorph.vaddConst x).symm '' ↑s)

Tactic:
AffineSubspace.coe_direction_eq_vsub_set_right hx

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 ((fun x_1 ↦ x_1 -ᵥ x) '' ↑s) ↔ IsClosed (⇑(Homeomorph.vaddConst x).symm '' ↑s)
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: case refine_2
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : f.contLinear = 0 ↔ (↑f).linear = 0
q : Q
h : ↑f = AffineMap.const R P q
x✝ : P
⊢ q = Function.const P q x✝

Tactic:
Function.const_apply

Goal state after:
case refine_2
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : f.contLinear = 0 ↔ (↑f).linear = 0
q : Q
h : ↑f = AffineMap.const R P q
x✝ : P
⊢ q = q
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
⊢ ‖f‖ = ∑ x ∈ (toSimpleFunc f).range, μ.real (⇑(toSimpleFunc f) ⁻¹' {x}) * ‖x‖

Tactic:
norm_toSimpleFunc,

Goal state after:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
⊢ (eLpNorm (⇑(toSimpleFunc f)) 1 μ).toReal = ∑ x ∈ (toSimpleFunc f).range, μ.real (⇑(toSimpleFunc f) ⁻¹' {x}) * ‖x‖
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
⊢ f z = ↑‖z‖ / ↑r * ↑r * (↑‖z‖)⁻¹ * f z

Tactic:
div_mul_cancel₀ _ r_ne_zero,

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
⊢ f z = ↑‖z‖ * (↑‖z‖)⁻¹ * f z
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case mem
α : 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✝³ : Module 𝕜 F
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 F
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
f : ↥(Lp E 1 μ)
h₁ : Dense (range ⇑(coeToLp α E ℝ))
⊢ ∀ x ∈ range ⇑(coeToLp α E ℝ), (setToL1 hT) x = (setToL1' 𝕜 hT h_smul) x

Tactic:
intro f

Goal state after:
case mem
α : 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✝³ : Module 𝕜 F
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 F
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
f✝ : ↥(Lp E 1 μ)
h₁ : Dense (range ⇑(coeToLp α E ℝ))
f : ↥(Lp E 1 μ)
⊢ f ∈ range ⇑(coeToLp α E ℝ) → (setToL1 hT) f = (setToL1' 𝕜 hT h_smul) 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 α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : ↥(Lp E 1 μ)
⊢ ∀ (f : ↥(α →₁ₛ[μ] E)), (setToL1SCLM α E μ hT) f = (setToL1 hT') ↑f

Tactic:
intro f

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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f✝ : ↥(Lp E 1 μ)
f : ↥(α →₁ₛ[μ] E)
⊢ (setToL1SCLM α E μ hT) f = (setToL1 hT') ↑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 α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T s = T' s
f : ↥(Lp E 1 μ)
⊢ ∀ (f : ↥(α →₁ₛ[μ] E)), (setToL1SCLM α E μ hT) f = (setToL1 hT') ↑f

Tactic:
intro f

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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T s = T' s
f✝ : ↥(Lp E 1 μ)
f : ↥(α →₁ₛ[μ] E)
⊢ (setToL1SCLM α E μ hT) f = (setToL1 hT') ↑f
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
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable fun i ↦ ∫ (x : X), ‖f x‖ ∂μ i
⊢ Integrable f (Measure.sum μ)

Tactic:
refine ⟨aestronglyMeasurable_sum_measure_iff.mpr fun i ↦ (hf i).aestronglyMeasurable, ?_⟩

Goal state after:
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝¹ : Countable ι
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable fun i ↦ ∫ (x : X), ‖f x‖ ∂μ i
⊢ HasFiniteIntegral f (Measure.sum μ)
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
⊢ setToFun μ T hT 0 = 0

Tactic:
by_cases hF : CompleteSpace F; swap
  · simp [setToFun, hF]
  rw [setToFun_eq hT (integrable_zero _ _ _), Integrable.toL1_zero, map_zero]

Goal state after: