α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.490028
G : Type ?u.490031
𝕜 : Type ?u.490034
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
μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : { x // x ∈ simpleFunc E 1 μ }
f' : { x // x ∈ simpleFunc E 1 μ' }
h : ↑↑↑f =ᵐ[μ] ↑↑↑f'
⊢ ↑(toSimpleFunc f) =ᵐ[μ] ↑(toSimpleFunc f')
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.490028
G : Type ?u.490031
𝕜 : Type ?u.490034
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
μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : { x // x ∈ simpleFunc E 1 μ }
f' : { x // x ∈ simpleFunc E 1 μ' }
h : ↑↑↑f =ᵐ[μ] ↑↑↑f'
⊢ setToL1S T f = setToL1S T f'
refine' SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable f) _
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.490028
G : Type ?u.490031
𝕜 : Type ?u.490034
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
μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : { x // x ∈ simpleFunc E 1 μ }
f' : { x // x ∈ simpleFunc E 1 μ' }
h : ↑↑↑f =ᵐ[μ] ↑↑↑f'
⊢ ↑↑↑f =ᵐ[μ] ↑(toSimpleFunc f')
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.490028
G : Type ?u.490031
𝕜 : Type ?u.490034
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
μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : { x // x ∈ simpleFunc E 1 μ }
f' : { x // x ∈ simpleFunc E 1 μ' }
h : ↑↑↑f =ᵐ[μ] ↑↑↑f'
⊢ ↑(toSimpleFunc f) =ᵐ[μ] ↑(toSimpleFunc f')
refine' (toSimpleFunc_eq_toFun f).trans _
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.490028
G : Type ?u.490031
𝕜 : Type ?u.490034
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
μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : { x // x ∈ simpleFunc E 1 μ }
f' : { x // x ∈ simpleFunc E 1 μ' }
h : ↑↑↑f =ᵐ[μ] ↑↑↑f'
this : ↑↑↑f' =ᵐ[μ] ↑(toSimpleFunc f')
⊢ ↑↑↑f =ᵐ[μ] ↑(toSimpleFunc f')

case this
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.490028
G : Type ?u.490031
𝕜 : Type ?u.490034
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
μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : { x // x ∈ simpleFunc E 1 μ }
f' : { x // x ∈ simpleFunc E 1 μ' }
h : ↑↑↑f =ᵐ[μ] ↑↑↑f'
⊢ ↑↑↑f' =ᵐ[μ] ↑(toSimpleFunc f')
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.490028
G : Type ?u.490031
𝕜 : Type ?u.490034
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
μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : { x // x ∈ simpleFunc E 1 μ }
f' : { x // x ∈ simpleFunc E 1 μ' }
h : ↑↑↑f =ᵐ[μ] ↑↑↑f'
⊢ ↑↑↑f =ᵐ[μ] ↑(toSimpleFunc f')
suffices : (f' : α → E) =ᵐ[μ] simpleFunc.toSimpleFunc f'
case this
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.490028
G : Type ?u.490031
𝕜 : Type ?u.490034
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
μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : { x // x ∈ simpleFunc E 1 μ }
f' : { x // x ∈ simpleFunc E 1 μ' }
h : ↑↑↑f =ᵐ[μ] ↑↑↑f'
⊢ ↑↑↑f' =ᵐ[μ] ↑(toSimpleFunc f')
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.490028
G : Type ?u.490031
𝕜 : Type ?u.490034
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
μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : { x // x ∈ simpleFunc E 1 μ }
f' : { x // x ∈ simpleFunc E 1 μ' }
h : ↑↑↑f =ᵐ[μ] ↑↑↑f'
this : ↑↑↑f' =ᵐ[μ] ↑(toSimpleFunc f')
⊢ ↑↑↑f =ᵐ[μ] ↑(toSimpleFunc f')

case this
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.490028
G : Type ?u.490031
𝕜 : Type ?u.490034
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
μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : { x // x ∈ simpleFunc E 1 μ }
f' : { x // x ∈ simpleFunc E 1 μ' }
h : ↑↑↑f =ᵐ[μ] ↑↑↑f'
⊢ ↑↑↑f' =ᵐ[μ] ↑(toSimpleFunc f')
exact h.trans this
case this
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.490028
G : Type ?u.490031
𝕜 : Type ?u.490034
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
μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : { x // x ∈ simpleFunc E 1 μ }
f' : { x // x ∈ simpleFunc E 1 μ' }
h : ↑↑↑f =ᵐ[μ] ↑↑↑f'
goal' : ↑↑↑f' =ᵐ[μ'] ↑(toSimpleFunc f')
⊢ ↑↑↑f' =ᵐ[μ] ↑(toSimpleFunc f')
case this
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.490028
G : Type ?u.490031
𝕜 : Type ?u.490034
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
μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : { x // x ∈ simpleFunc E 1 μ }
f' : { x // x ∈ simpleFunc E 1 μ' }
h : ↑↑↑f =ᵐ[μ] ↑↑↑f'
⊢ ↑↑↑f' =ᵐ[μ] ↑(toSimpleFunc f')
have goal' : (f' : α → E) =ᵐ[μ'] simpleFunc.toSimpleFunc f' := (toSimpleFunc_eq_toFun f').symm
no goals
case this
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.490028
G : Type ?u.490031
𝕜 : Type ?u.490034
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
μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : { x // x ∈ simpleFunc E 1 μ }
f' : { x // x ∈ simpleFunc E 1 μ' }
h : ↑↑↑f =ᵐ[μ] ↑↑↑f'
goal' : ↑↑↑f' =ᵐ[μ'] ↑(toSimpleFunc f')
⊢ ↑↑↑f' =ᵐ[μ] ↑(toSimpleFunc f')
exact hμ.ae_eq goal'