-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToFun_congr_measure_of_integrable {μ' : Measure α} (c' : ℝ≥0∞) (hc' : 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

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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : 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

Tactic:
apply hfμ.induction (P := fun f => setToFun μ T hT f = setToFun μ' T hT' f)

Result:
case h_ind
α : 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : 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 μ'
⊢ ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ⊤ → (fun f => setToFun μ T hT f = setToFun μ' T hT' f) (s.indicator fun x => c)

case h_add
α : 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : 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 μ'
⊢ ∀ ⦃f g : α → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      Integrable f μ →
        Integrable g μ →
          (fun f => setToFun μ T hT f = setToFun μ' T hT' f) f →
            (fun f => setToFun μ T hT f = setToFun μ' T hT' f) g →
              (fun f => setToFun μ T hT f = setToFun μ' T hT' f) (f + g)

case h_closed
α : 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : 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 μ'
⊢ IsClosed {f | (fun f => setToFun μ T hT f = setToFun μ' T hT' f) ↑↑f}

case h_ae
α : 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : 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 μ'
⊢ ∀ ⦃f g : α → E⦄,
    f =ᶠ[ae μ] g →
      Integrable f μ →
        (fun f => setToFun μ T hT f = setToFun μ' T hT' f) f → (fun f => setToFun μ T hT f = setToFun μ' T hT' f) g

Proof state:
case h_closed
α : 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : 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 μ'
⊢ IsClosed {f | (fun f => setToFun μ T hT f = setToFun μ' T hT' f) ↑↑f}

Tactic:
refine isClosed_eq (continuous_setToFun hT) ?_

Result:
case h_closed
α : 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : 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 μ'
⊢ Continuous fun f => setToFun μ' T hT' ↑↑f

Proof state:
case h
α : 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : 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 μ'
f : ↥(Lp E 1 μ)
⊢ setToFun μ' T hT' ↑↑f = setToFun μ' T hT' ↑↑(Integrable.toL1 ↑↑f ⋯)

Tactic:
exact setToFun_congr_ae hT' (Integrable.coeFn_toL1 _).symm

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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : 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 μ'
⊢ (fun f => setToFun μ' T hT' ↑↑f) = fun f => setToFun μ' T hT' ↑↑(Integrable.toL1 ↑↑f ⋯)

Tactic:
ext1 f

Result:
case h
α : 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : 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 μ'
f : ↥(Lp E 1 μ)
⊢ setToFun μ' T hT' ↑↑f = setToFun μ' T hT' ↑↑(Integrable.toL1 ↑↑f ⋯)

Proof state:
case h_closed
α : 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : 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 μ'
this : (fun f => setToFun μ' T hT' ↑↑f) = fun f => setToFun μ' T hT' ↑↑(Integrable.toL1 ↑↑f ⋯)
⊢ Continuous fun f => setToFun μ' T hT' ↑↑(Integrable.toL1 ↑↑f ⋯)

Tactic:
exact (continuous_setToFun hT').comp (continuous_L1_toL1 c' hc' hμ'_le)

Result:
no goals