-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToL1S_congr_measure {μ' : Measure α} (T : Set α → E →L[ℝ] F)
    (h_zero : ∀ s, MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T) (hμ : μ ≪ μ')
    (f : α →₁ₛ[μ] E) (f' : α →₁ₛ[μ'] E) (h : (f : α → E) =ᵐ[μ] f') :
    setToL1S T f = setToL1S T f'

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : ↥(simpleFunc E 1 μ)
f' : ↥(simpleFunc E 1 μ')
h : ↑↑↑f =ᶠ[ae μ] ↑↑↑f'
⊢ setToL1S T f = setToL1S T f'

Tactic:
refine SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable f) ?_

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : ↥(simpleFunc E 1 μ)
f' : ↥(simpleFunc E 1 μ')
h : ↑↑↑f =ᶠ[ae μ] ↑↑↑f'
⊢ ⇑(toSimpleFunc f) =ᶠ[ae μ] ⇑(toSimpleFunc f')

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : ↥(simpleFunc E 1 μ)
f' : ↥(simpleFunc E 1 μ')
h : ↑↑↑f =ᶠ[ae μ] ↑↑↑f'
goal' : ↑↑↑f' =ᶠ[ae μ'] ⇑(toSimpleFunc f')
⊢ ↑↑↑f' =ᶠ[ae μ] ⇑(toSimpleFunc f')

Tactic:
exact hμ.ae_eq goal'

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : ↥(simpleFunc E 1 μ)
f' : ↥(simpleFunc E 1 μ')
h : ↑↑↑f =ᶠ[ae μ] ↑↑↑f'
⊢ ↑↑↑f' =ᶠ[ae μ] ⇑(toSimpleFunc f')

Tactic:
have goal' : (f' : α → E) =ᵐ[μ'] simpleFunc.toSimpleFunc f' := (toSimpleFunc_eq_toFun f').symm

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : ↥(simpleFunc E 1 μ)
f' : ↥(simpleFunc E 1 μ')
h : ↑↑↑f =ᶠ[ae μ] ↑↑↑f'
goal' : ↑↑↑f' =ᶠ[ae μ'] ⇑(toSimpleFunc f')
⊢ ↑↑↑f' =ᶠ[ae μ] ⇑(toSimpleFunc f')

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : ↥(simpleFunc E 1 μ)
f' : ↥(simpleFunc E 1 μ')
h : ↑↑↑f =ᶠ[ae μ] ↑↑↑f'
⊢ ⇑(toSimpleFunc f) =ᶠ[ae μ] ⇑(toSimpleFunc f')

Tactic:
refine (toSimpleFunc_eq_toFun f).trans ?_

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : ↥(simpleFunc E 1 μ)
f' : ↥(simpleFunc E 1 μ')
h : ↑↑↑f =ᶠ[ae μ] ↑↑↑f'
⊢ ↑↑↑f =ᶠ[ae μ] ⇑(toSimpleFunc f')

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : ↥(simpleFunc E 1 μ)
f' : ↥(simpleFunc E 1 μ')
h : ↑↑↑f =ᶠ[ae μ] ↑↑↑f'
⊢ ↑↑↑f =ᶠ[ae μ] ⇑(toSimpleFunc f')

Tactic:
suffices (f' : α → E) =ᵐ[μ] simpleFunc.toSimpleFunc f' from h.trans this

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : ↥(simpleFunc E 1 μ)
f' : ↥(simpleFunc E 1 μ')
h : ↑↑↑f =ᶠ[ae μ] ↑↑↑f'
⊢ ↑↑↑f' =ᶠ[ae μ] ⇑(toSimpleFunc f')