-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToFun_congr_ae (hT : DominatedFinMeasAdditive μ T C) (h : f =ᵐ[μ] g) :
    setToFun μ T hT f = setToFun μ T hT g

Proof state:
case neg
α : 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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
hfi : ¬Integrable f μ
⊢ setToFun μ T hT f = setToFun μ T hT g

Tactic:
have hgi : ¬Integrable g μ := by rw [integrable_congr h] at hfi; exact hfi

Result:
case neg
α : 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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
hfi : ¬Integrable f μ
hgi : ¬Integrable g μ
⊢ setToFun μ T hT f = setToFun μ T hT g

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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
⊢ setToFun μ T hT f = setToFun μ T hT g

Tactic:
by_cases hfi : Integrable f μ

Result:
case pos
α : 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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
hfi : Integrable f μ
⊢ setToFun μ T hT f = setToFun μ T hT g

case neg
α : 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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
hfi : ¬Integrable f μ
⊢ setToFun μ T hT f = setToFun μ T hT g

Proof state:
case neg
α : 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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
hfi : ¬Integrable f μ
hgi : ¬Integrable g μ
⊢ setToFun μ T hT f = setToFun μ T hT g

Tactic:
rw [setToFun_undef hT hfi, setToFun_undef hT hgi]

Result:
no goals

Proof state:
case pos
α : 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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
hfi : Integrable f μ
hgi : Integrable g μ
⊢ setToFun μ T hT f = setToFun μ T hT g

Tactic:
rw [setToFun_eq hT hfi, setToFun_eq hT hgi, (Integrable.toL1_eq_toL1_iff f g hfi hgi).2 h]

Result:
no goals

Proof state:
case pos
α : 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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
hfi : Integrable f μ
⊢ setToFun μ T hT f = setToFun μ T hT g

Tactic:
have hgi : Integrable g μ := hfi.congr h

Result:
case pos
α : 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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
hfi : Integrable f μ
hgi : Integrable g μ
⊢ setToFun μ T hT f = setToFun μ T hT g

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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
hfi : ¬Integrable g μ
⊢ ¬Integrable g μ

Tactic:
exact hfi

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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
hfi : ¬Integrable f μ
⊢ ¬Integrable g μ

Tactic:
rw [integrable_congr h] at hfi

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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
hfi : ¬Integrable g μ
⊢ ¬Integrable g μ