no goals
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.794201
G : Type ?u.794204
𝕜 : Type ?u.794207
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✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : { x // x ∈ simpleFunc E 1 μ }
x✝² : Set α
x✝¹ : MeasurableSet x✝²
x✝ : ↑↑μ x✝² < ⊤
⊢ T x✝² = T' x✝²
rw [h]