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

Goal state before:
pp: case h1
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
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✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
m : (i : ι) → E i
i : ι
a✝ : i ∈ univ
⊢ ‖(f i) (m i)‖ ≤ ‖f i‖ * ‖m i‖

Tactic:
;

Goal state after:
case h1
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
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✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
m : (i : ι) → E i
i : ι
a✝ : i ∈ univ
⊢ ‖(f i) (m i)‖ ≤ ‖f i‖ * ‖m i‖
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✝ : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : μ U < ∞
this : Fact (μ U < ∞)
⊢ IntegrableAtFilter f (𝓝 x) μ

Tactic:
refine ⟨U, hU, ?_⟩

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✝ : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : μ U < ∞
this : Fact (μ U < ∞)
⊢ IntegrableOn f U μ
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✝ : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : μ U < ∞
this : Fact (μ U < ∞)
⊢ IntegrableOn f U μ

Tactic:
rw [IntegrableOn, ← memLp_one_iff_integrable]

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✝ : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : μ U < ∞
this : Fact (μ U < ∞)
⊢ MemLp f 1 (μ.restrict U)
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T : Set α → β
inst✝ : AddMonoid β
c : ℝ≥0∞
hc_ne_zero : c ≠ 0
hT : FinMeasAdditive μ T
⊢ FinMeasAdditive (c • μ) T

Tactic:
by
  refine of_eq_top_imp_eq_top (fun s _ hμs => ?_) hT
  rw [Measure.smul_apply, smul_eq_mul, ENNReal.mul_eq_top]
  simp only [hc_ne_zero, true_and, Ne, not_false_iff]
  exact Or.inl hμs

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝ : AddCancelMonoid β
T : Set α → β
hT : FinMeasAdditive μ T
⊢ T ∅ = 0

Tactic:
have h_empty : μ ∅ ≠ ∞ := (measure_empty.le.trans_lt ENNReal.coe_lt_top).ne
  specialize hT ∅ ∅ MeasurableSet.empty MeasurableSet.empty h_empty h_empty (disjoint_empty _)
  rw [Set.union_empty] at hT
  nth_rw 1 [← add_zero (T ∅)] at hT
  exact (add_left_cancel hT).symm

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

Goal state before:
pp: α : Type u_1
F : Type u_5
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup F
p : ℝ
f : α →ₛ F
μ : Measure α
⊢ (fun x ↦ ‖f x‖ₑ ^ p) = (fun x ↦ ‖x‖ₑ ^ p) ∘ ⇑f

Tactic:
;

Goal state after:
α : Type u_1
F : Type u_5
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup F
p : ℝ
f : α →ₛ F
μ : Measure α
⊢ (fun x ↦ ‖f x‖ₑ ^ p) = (fun x ↦ ‖x‖ₑ ^ p) ∘ ⇑f
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : a ∉ s
h : (∀ i ∈ s, μ (S i) ≠ ∞) → (∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)
hps : ∀ i ∈ insert a s, μ (S i) ≠ ∞
h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)
⊢ ⋃ i ∈ insert a s, S i = S a ∪ ⋃ i ∈ s, S i

Tactic:
;

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : a ∉ s
h : (∀ i ∈ s, μ (S i) ≠ ∞) → (∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)
hps : ∀ i ∈ insert a s, μ (S i) ≠ ∞
h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)
⊢ ⋃ i ∈ insert a s, S i = S a ∪ ⋃ i ∈ s, S i
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case pos
α : 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
⊢ AEStronglyMeasurable (⇑f) μ

Tactic:
;

Goal state after:
case pos
α : 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
⊢ AEStronglyMeasurable (⇑f) μ
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case pos
α : 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 = ∞
⊢ MemLp ⇑f ∞ μ

Tactic:
;

Goal state after:
case pos
α : 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 = ∞
⊢ MemLp ⇑f ∞ μ
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
x y : 𝕜
f : ↥(simpleFunc E p μ)
⊢ ↑((x * y) • f) = ↑(x • y • f)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : ↥(simpleFunc E p μ)
⊢ ↑(1 • f) = ↑f
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
x : 𝕜
⊢ ↑(x • 0) = ↑0
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝ : NormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hs_zero : μ s = 0
⊢ ‖T s‖ = 0

Tactic:
refine ((hT.2 s hs (by simp [hs_zero])).trans (le_of_eq ?_)).antisymm (norm_nonneg _)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝ : NormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hs_zero : μ s = 0
⊢ C * μ.real s = 0
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

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

Tactic:
;

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

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

Tactic:
;

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

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : ↥(simpleFunc E p μ)
⊢ ↑(0 • f) = ↑0
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 : α →ₛ E
hfi : MemLp (⇑f) p μ
⊢ AEEqFun.mk ⇑(toSimpleFunc (f.toLp hfi)) ?m.37 = AEEqFun.mk ⇑f ?m.38

pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₛ E
hfi : MemLp (⇑f) p μ
⊢ AEStronglyMeasurable (⇑(toSimpleFunc (f.toLp hfi))) μ

pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₛ E
hfi : MemLp (⇑f) p μ
⊢ AEStronglyMeasurable (⇑f) μ

Tactic:
;

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₛ E
hfi : MemLp (⇑f) p μ
⊢ AEEqFun.mk ⇑(toSimpleFunc (f.toLp hfi)) ?m.37 = AEEqFun.mk ⇑f ?m.38

α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₛ E
hfi : MemLp (⇑f) p μ
⊢ AEStronglyMeasurable (⇑(toSimpleFunc (f.toLp hfi))) μ

α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₛ E
hfi : MemLp (⇑f) p μ
⊢ AEStronglyMeasurable (⇑f) μ
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝¹⁷ : AddCommGroup E
inst✝¹⁶ : UniformSpace E
inst✝¹⁵ : IsUniformAddGroup E
inst✝¹⁴ : AddCommGroup F
inst✝¹³ : UniformSpace F
inst✝¹² : IsUniformAddGroup F
inst✝¹¹ : T0Space F
inst✝¹⁰ : AddCommMonoid Eₗ
inst✝⁹ : UniformSpace Eₗ
inst✝⁸ : ContinuousAdd Eₗ
inst✝⁷ : Semiring 𝕜
inst✝⁶ : Semiring 𝕜₂
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : Module 𝕜 Eₗ
inst✝² : ContinuousConstSMul 𝕜 Eₗ
inst✝¹ : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
inst✝ : CompleteSpace F
e : E →L[𝕜] Eₗ
h_dense : DenseRange ⇑e
h_e : IsUniformInducing ⇑e
x : E
⊢ (f.extend e) (e x) = f x

Tactic:
simp only [extend, h_dense, h_e, and_self, ↓reduceDIte, coe_mk', LinearMap.coe_mk, AddHom.coe_mk]

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝¹⁷ : AddCommGroup E
inst✝¹⁶ : UniformSpace E
inst✝¹⁵ : IsUniformAddGroup E
inst✝¹⁴ : AddCommGroup F
inst✝¹³ : UniformSpace F
inst✝¹² : IsUniformAddGroup F
inst✝¹¹ : T0Space F
inst✝¹⁰ : AddCommMonoid Eₗ
inst✝⁹ : UniformSpace Eₗ
inst✝⁸ : ContinuousAdd Eₗ
inst✝⁷ : Semiring 𝕜
inst✝⁶ : Semiring 𝕜₂
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : Module 𝕜 Eₗ
inst✝² : ContinuousConstSMul 𝕜 Eₗ
inst✝¹ : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
inst✝ : CompleteSpace F
e : E →L[𝕜] Eₗ
h_dense : DenseRange ⇑e
h_e : IsUniformInducing ⇑e
x : E
⊢ ⋯.extend (⇑f) (e x) = f x
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✝ → (toSimpleFunc (f + g)) a✝ = (toSimpleFunc f) a✝ + (toSimpleFunc g) a✝

Tactic:
;

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✝
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✝

Tactic:
;

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✝
h : (toSimpleFunc g) a✝ = ↑↑↑g a✝
⊢ ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + ↑↑↑g a✝ → ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + (toSimpleFunc g) a✝

Tactic:
;

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✝
h : ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + ↑↑↑g a✝
⊢ ↑(↑↑f + ↑↑g) a✝ = ↑↑↑f a✝ + ↑↑↑g a✝

Tactic:
;

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.Analysis.Normed.Operator.Extend

Goal state before:
pp: case hbc
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup Eₗ
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 Eₗ
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst✝ : RingHomIsometric σ₁₂
h_dense : DenseRange ⇑e
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
x : E
⊢ ‖x‖ ≤ ↑N * ‖e x‖

Tactic:
;

Goal state after:
case hbc
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup Eₗ
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 Eₗ
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst✝ : RingHomIsometric σ₁₂
h_dense : DenseRange ⇑e
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
x : E
⊢ ‖x‖ ≤ ↑N * ‖e x‖
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✝ → (toSimpleFunc (-f)) a✝ = -(toSimpleFunc f) a✝

Tactic:
;

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✝
h : (toSimpleFunc f) a✝ = ↑↑↑f a✝
⊢ ↑(-↑↑f) a✝ = -↑↑↑f a✝ → ↑(-↑↑f) a✝ = -(toSimpleFunc f) a✝

Tactic:
;

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✝
h : ↑(-↑↑f) a✝ = -↑↑↑f a✝
⊢ ↑(-↑↑f) a✝ = -↑↑↑f a✝

Tactic:
;

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:
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✝ → (toSimpleFunc (f - g)) a✝ = (toSimpleFunc f) a✝ - (toSimpleFunc g) a✝

Tactic:
;

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✝
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✝

Tactic:
;

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✝
h : (toSimpleFunc g) a✝ = ↑↑↑g a✝
⊢ ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝ → ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - (toSimpleFunc g) a✝

Tactic:
;

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✝
h : ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝
⊢ ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝

Tactic:
;

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✝