case inl
α : Type u_1
E : Type ?u.459354
F : Type u_2
F' : Type u_3
G : Type ?u.459363
𝕜 : Type ?u.459366
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
x : F
m : MeasurableSpace α
h✝ : IsEmpty α
hα : (_ : IsEmpty α ∨ Nonempty α) = (_ : IsEmpty α ∨ Nonempty α)
⊢ setToSimpleFunc T (const α x) = ↑(T Set.univ) x

case inr
α : Type u_1
E : Type ?u.459354
F : Type u_2
F' : Type u_3
G : Type ?u.459363
𝕜 : Type ?u.459366
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
x : F
m : MeasurableSpace α
h✝ : Nonempty α
hα : (_ : IsEmpty α ∨ Nonempty α) = (_ : IsEmpty α ∨ Nonempty α)
⊢ setToSimpleFunc T (const α x) = ↑(T Set.univ) x
α : Type u_1
E : Type ?u.459354
F : Type u_2
F' : Type u_3
G : Type ?u.459363
𝕜 : Type ?u.459366
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
x : F
m : MeasurableSpace α
⊢ setToSimpleFunc T (const α x) = ↑(T Set.univ) x
cases hα : isEmpty_or_nonempty α
case inl
α : Type u_1
E : Type ?u.459354
F : Type u_2
F' : Type u_3
G : Type ?u.459363
𝕜 : Type ?u.459366
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
x : F
m : MeasurableSpace α
h✝ : IsEmpty α
hα : (_ : IsEmpty α ∨ Nonempty α) = (_ : IsEmpty α ∨ Nonempty α)
h_univ_empty : Set.univ = ∅
⊢ setToSimpleFunc T (const α x) = ↑(T Set.univ) x
case inl
α : Type u_1
E : Type ?u.459354
F : Type u_2
F' : Type u_3
G : Type ?u.459363
𝕜 : Type ?u.459366
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
x : F
m : MeasurableSpace α
h✝ : IsEmpty α
hα : (_ : IsEmpty α ∨ Nonempty α) = (_ : IsEmpty α ∨ Nonempty α)
⊢ setToSimpleFunc T (const α x) = ↑(T Set.univ) x
have h_univ_empty : (univ : Set α) = ∅ := Subsingleton.elim _ _
case inl
α : Type u_1
E : Type ?u.459354
F : Type u_2
F' : Type u_3
G : Type ?u.459363
𝕜 : Type ?u.459366
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
x : F
m : MeasurableSpace α
h✝ : IsEmpty α
hα : (_ : IsEmpty α ∨ Nonempty α) = (_ : IsEmpty α ∨ Nonempty α)
h_univ_empty : Set.univ = ∅
⊢ setToSimpleFunc T (const α x) = ↑0 x
case inl
α : Type u_1
E : Type ?u.459354
F : Type u_2
F' : Type u_3
G : Type ?u.459363
𝕜 : Type ?u.459366
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
x : F
m : MeasurableSpace α
h✝ : IsEmpty α
hα : (_ : IsEmpty α ∨ Nonempty α) = (_ : IsEmpty α ∨ Nonempty α)
h_univ_empty : Set.univ = ∅
⊢ setToSimpleFunc T (const α x) = ↑(T Set.univ) x
rw [h_univ_empty, hT_empty]
no goals
case inl
α : Type u_1
E : Type ?u.459354
F : Type u_2
F' : Type u_3
G : Type ?u.459363
𝕜 : Type ?u.459366
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
x : F
m : MeasurableSpace α
h✝ : IsEmpty α
hα : (_ : IsEmpty α ∨ Nonempty α) = (_ : IsEmpty α ∨ Nonempty α)
h_univ_empty : Set.univ = ∅
⊢ setToSimpleFunc T (const α x) = ↑0 x
simp only [setToSimpleFunc, ContinuousLinearMap.zero_apply, sum_empty,
  range_eq_empty_of_isEmpty]
no goals
case inr
α : Type u_1
E : Type ?u.459354
F : Type u_2
F' : Type u_3
G : Type ?u.459363
𝕜 : Type ?u.459366
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
x : F
m : MeasurableSpace α
h✝ : Nonempty α
hα : (_ : IsEmpty α ∨ Nonempty α) = (_ : IsEmpty α ∨ Nonempty α)
⊢ setToSimpleFunc T (const α x) = ↑(T Set.univ) x
exact setToSimpleFunc_const' T x