case inl
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
x : F
hs : MeasurableSet ∅
⊢ setToSimpleFunc T (piecewise ∅ hs (const α x) (const α 0)) = ↑(T ∅) x

case inr
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
⊢ setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = ↑(T s) x
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
⊢ setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = ↑(T s) x
obtain rfl | hs_empty := s.eq_empty_or_nonempty
case inr
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
⊢ ∑ x_1 in SimpleFunc.range (piecewise s hs (const α x) (const α 0)),
      ↑(T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 =
    ↑(T s) x
case inr
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
⊢ setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = ↑(T s) x
simp_rw [setToSimpleFunc]
case inr.inl
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
x : F
hs : MeasurableSet Set.univ
hs_empty : Set.Nonempty Set.univ
⊢ ∑ x_1 in SimpleFunc.range (piecewise Set.univ hs (const α x) (const α 0)),
      ↑(T (↑(piecewise Set.univ hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 =
    ↑(T Set.univ) x

case inr.inr
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
⊢ ∑ x_1 in SimpleFunc.range (piecewise s hs (const α x) (const α 0)),
      ↑(T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 =
    ↑(T s) x
case inr
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
⊢ ∑ x_1 in SimpleFunc.range (piecewise s hs (const α x) (const α 0)),
      ↑(T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 =
    ↑(T s) x
obtain rfl | hs_univ := eq_or_ne s univ
case inr.inr
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
⊢ ∑ x_1 in {x, 0}, ↑(T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 = ↑(T s) x
case inr.inr
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
⊢ ∑ x_1 in SimpleFunc.range (piecewise s hs (const α x) (const α 0)),
      ↑(T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 =
    ↑(T s) x
rw [range_indicator hs hs_empty hs_univ]
case pos
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : x = 0
⊢ ∑ x_1 in {x, 0}, ↑(T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 = ↑(T s) x

case neg
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ∑ x_1 in {x, 0}, ↑(T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 = ↑(T s) x
case inr.inr
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
⊢ ∑ x_1 in {x, 0}, ↑(T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 = ↑(T s) x
by_cases hx0 : x = 0
case neg
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ↑(T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x})) x +
      ∑ x_1 in {0}, ↑(T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 =
    ↑(T s) x

case neg
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ¬x ∈ {0}
case neg
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ∑ x_1 in {x, 0}, ↑(T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 = ↑(T s) x
rw [sum_insert]
case neg
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ¬x ∈ {0}

case neg
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ↑(T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x})) x +
      ∑ x_1 in {0}, ↑(T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 =
    ↑(T s) x
case neg
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ↑(T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x})) x +
      ∑ x_1 in {0}, ↑(T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 =
    ↑(T s) x

case neg
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ¬x ∈ {0}
swap
case neg
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ↑(T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x})) x = ↑(T s) x
case neg
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ↑(T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x})) x +
      ∑ x_1 in {0}, ↑(T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 =
    ↑(T s) x
rw [sum_singleton, (T _).map_zero, add_zero]
case neg.e_a.e_a
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x} = s
case neg
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ↑(T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x})) x = ↑(T s) x
congr
case neg.e_a.e_a
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ indicator s (Function.const α x) ⁻¹' {x} = s
case neg.e_a.e_a
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x} = s
simp only [coe_piecewise, piecewise_eq_indicator, coe_const, Pi.const_zero,
  piecewise_eq_indicator]
case neg.e_a.e_a
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ Set.ite s Set.univ (0 ⁻¹' {x}) = s

case neg.e_a.e_a
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ x ∈ {x}
case neg.e_a.e_a
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ indicator s (Function.const α x) ⁻¹' {x} = s
rw [indicator_preimage, ← Function.const_def, preimage_const_of_mem]
case neg.e_a.e_a
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ x ∈ {x}

case neg.e_a.e_a
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ Set.ite s Set.univ (0 ⁻¹' {x}) = s
case neg.e_a.e_a
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ Set.ite s Set.univ (0 ⁻¹' {x}) = s

case neg.e_a.e_a
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ x ∈ {x}
swap
case neg.e_a.e_a
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ Set.ite s Set.univ ∅ = s

case neg.e_a.e_a
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ¬0 ∈ {x}
case neg.e_a.e_a
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ Set.ite s Set.univ (0 ⁻¹' {x}) = s
rw [← Pi.const_zero, ← Function.const_def, preimage_const_of_not_mem]
case neg.e_a.e_a
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ¬0 ∈ {x}

case neg.e_a.e_a
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ Set.ite s Set.univ ∅ = s
case neg.e_a.e_a
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ Set.ite s Set.univ ∅ = s

case neg.e_a.e_a
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ¬0 ∈ {x}
swap
no goals
case neg.e_a.e_a
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ Set.ite s Set.univ ∅ = s
simp
no goals
case inl
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
x : F
hs : MeasurableSet ∅
⊢ setToSimpleFunc T (piecewise ∅ hs (const α x) (const α 0)) = ↑(T ∅) x
simp only [hT_empty, ContinuousLinearMap.zero_apply, piecewise_empty, const_zero,
  setToSimpleFunc_zero_apply]
case inr.inl
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
x : F
hs : MeasurableSet Set.univ
hs_empty : Set.Nonempty Set.univ
hα : Nonempty α
⊢ ∑ x_1 in SimpleFunc.range (piecewise Set.univ hs (const α x) (const α 0)),
      ↑(T (↑(piecewise Set.univ hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 =
    ↑(T Set.univ) x
case inr.inl
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
x : F
hs : MeasurableSet Set.univ
hs_empty : Set.Nonempty Set.univ
⊢ ∑ x_1 in SimpleFunc.range (piecewise Set.univ hs (const α x) (const α 0)),
      ↑(T (↑(piecewise Set.univ hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 =
    ↑(T Set.univ) x
haveI hα := hs_empty.to_type
no goals
case inr.inl
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
x : F
hs : MeasurableSet Set.univ
hs_empty : Set.Nonempty Set.univ
hα : Nonempty α
⊢ ∑ x_1 in SimpleFunc.range (piecewise Set.univ hs (const α x) (const α 0)),
      ↑(T (↑(piecewise Set.univ hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 =
    ↑(T Set.univ) x
simp [← Function.const_def]
case pos
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : x = 0
⊢ ∑ x in {0, 0}, ↑(T (↑(piecewise s hs (const α 0) (const α 0)) ⁻¹' {x})) x = ↑(T s) 0
case pos
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : x = 0
⊢ ∑ x_1 in {x, 0}, ↑(T (↑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 = ↑(T s) x
simp_rw [hx0]
no goals
case pos
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : x = 0
⊢ ∑ x in {0, 0}, ↑(T (↑(piecewise s hs (const α 0) (const α 0)) ⁻¹' {x})) x = ↑(T s) 0
simp
case neg
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ¬x = 0
case neg
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ¬x ∈ {0}
rw [Finset.mem_singleton]
no goals
case neg
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ¬x = 0
exact hx0
no goals
case neg.e_a.e_a
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ x ∈ {x}
exact Set.mem_singleton x
case neg.e_a.e_a
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ¬0 = x
case neg.e_a.e_a
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ¬0 ∈ {x}
rw [Set.mem_singleton_iff]
no goals
case neg.e_a.e_a
α : Type u_1
E : Type ?u.425807
F : Type u_2
F' : Type u_3
G : Type ?u.425816
𝕜 : Type ?u.425819
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : Set.Nonempty s
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ¬0 = x
exact Ne.symm hx0