case pos
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1651275
G : Type ?u.1651278
𝕜 : Type ?u.1651281
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 α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c c' : ℝ≥0∞
hc : c ≠ ⊤
hc' : c' ≠ ⊤
hμ_le : μ ≤ c • μ'
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hf : Integrable f
⊢ setToFun μ T hT f = setToFun μ' T hT' f

case neg
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1651275
G : Type ?u.1651278
𝕜 : Type ?u.1651281
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 α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c c' : ℝ≥0∞
hc : c ≠ ⊤
hc' : c' ≠ ⊤
hμ_le : μ ≤ c • μ'
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hf : ¬Integrable f
⊢ setToFun μ T hT f = setToFun μ' T hT' f
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1651275
G : Type ?u.1651278
𝕜 : Type ?u.1651281
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 α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c c' : ℝ≥0∞
hc : c ≠ ⊤
hc' : c' ≠ ⊤
hμ_le : μ ≤ c • μ'
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
⊢ setToFun μ T hT f = setToFun μ' T hT' f
by_cases hf : Integrable f μ
no goals
case pos
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1651275
G : Type ?u.1651278
𝕜 : Type ?u.1651281
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 α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c c' : ℝ≥0∞
hc : c ≠ ⊤
hc' : c' ≠ ⊤
hμ_le : μ ≤ c • μ'
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hf : Integrable f
⊢ setToFun μ T hT f = setToFun μ' T hT' f
exact setToFun_congr_measure_of_integrable c' hc' hμ'_le hT hT' f hf
case neg
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1651275
G : Type ?u.1651278
𝕜 : Type ?u.1651281
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 α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c c' : ℝ≥0∞
hc : c ≠ ⊤
hc' : c' ≠ ⊤
hμ_le : μ ≤ c • μ'
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hf : ¬Integrable f
h_int : ∀ (g : α → E), ¬Integrable g → ¬Integrable g
⊢ setToFun μ T hT f = setToFun μ' T hT' f
case neg
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1651275
G : Type ?u.1651278
𝕜 : Type ?u.1651281
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 α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c c' : ℝ≥0∞
hc : c ≠ ⊤
hc' : c' ≠ ⊤
hμ_le : μ ≤ c • μ'
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hf : ¬Integrable f
⊢ setToFun μ T hT f = setToFun μ' T hT' f
have h_int : ∀ g : α → E, ¬Integrable g μ → ¬Integrable g μ' := fun g =>
  mt fun h => h.of_measure_le_smul _ hc hμ_le
no goals
case neg
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1651275
G : Type ?u.1651278
𝕜 : Type ?u.1651281
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 α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c c' : ℝ≥0∞
hc : c ≠ ⊤
hc' : c' ≠ ⊤
hμ_le : μ ≤ c • μ'
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hf : ¬Integrable f
h_int : ∀ (g : α → E), ¬Integrable g → ¬Integrable g
⊢ setToFun μ T hT f = setToFun μ' T hT' f
simp_rw [setToFun_undef _ hf, setToFun_undef _ (h_int f hf)]