Caccioppoli localize on subset

theorem caccioppoli_localize_on_subset    {α : Type*} [MeasurableSpace α] {μ : Measure α}    {s t : Set α} (hst : s ⊆ t)    {G v η ζ : α → ℝ} {C_coeff C_grad : ℝ}    (hs_meas : MeasurableSet s) (ht_meas : MeasurableSet t)    (hη_eq_one : ∀ x ∈ s, η x = 1)    (hC_coeff : 0 ≤ C_coeff) (hC_grad : 0 ≤ C_grad)    (hζ_nonneg : ∀ x ∈ t, 0 ≤ ζ x)    (hζ_bound : ∀ x ∈ t, ζ x ≤ C_grad)    (h_weighted :      ∫ x in t, η x ^ 2 * ‖G x‖ ^ 2 ∂μ ≤        C_coeff * ∫ x in t, ζ x ^ 2 * |v x| ^ 2 ∂μ)    (hweighted_int : IntegrableOn (fun x => η x ^ 2 * ‖G x‖ ^ 2) t μ)    (hzv_int : IntegrableOn (fun x => ζ x ^ 2 * |v x| ^ 2) t μ)    (hv_sq_int : IntegrableOn (fun x => |v x| ^ 2) t μ) :    ∫ x in s, ‖G x‖ ^ 2 ∂μ ≤      C_coeff * C_grad ^ 2 * ∫ x in t, |v x| ^ 2 ∂μ := by  have hleft_eq :      ∫ x in s, ‖G x‖ ^ 2 ∂μ = ∫ x in s, η x ^ 2 * ‖G x‖ ^ 2 ∂μ := by    refine integral_congr_ae ?_    refine (ae_restrict_iff' (μ := μ) ?_).2 ?_    · exact hs_meas    · filter_upwards with x hx      simp [hη_eq_one x hx]  have hweighted_nonneg : ∀ x, 0 ≤ η x ^ 2 * ‖G x‖ ^ 2 := by    intro x    positivity  have hleft_mono :      ∫ x in s, η x ^ 2 * ‖G x‖ ^ 2 ∂μ ≤ ∫ x in t, η x ^ 2 * ‖G x‖ ^ 2 ∂μ := by    exact setIntegral_mono_set hweighted_int      (ae_of_all _ hweighted_nonneg) (ae_of_all _ hst)  have hgrad_pt :      ∀ x ∈ t, ζ x ^ 2 * |v x| ^ 2 ≤ C_grad ^ 2 * |v x| ^ 2 := by    intro x hx    have hsq : ζ x ^ 2 ≤ C_grad ^ 2 := by      nlinarith [hζ_nonneg x hx, hζ_bound x hx, hC_grad]    apply mul_le_mul_of_nonneg_right ?_ (sq_nonneg _)    exact hsq  have hgrad_int :      IntegrableOn (fun x => C_grad ^ 2 * |v x| ^ 2) t μ := by    simpa using hv_sq_int.const_mul (C_grad ^ 2)  have hgrad_bound :      ∫ x in t, ζ x ^ 2 * |v x| ^ 2 ∂μ ≤ ∫ x in t, C_grad ^ 2 * |v x| ^ 2 ∂μ := by    refine integral_mono_ae hzv_int hgrad_int ?_    refine (ae_restrict_iff' (μ := μ) ?_).2 ?_    · exact ht_meas    · filter_upwards with x hx      exact hgrad_pt x hx  have hconst_mul :      ∫ x in t, C_grad ^ 2 * |v x| ^ 2 ∂μ =        C_grad ^ 2 * ∫ x in t, |v x| ^ 2 ∂μ := by    rw [integral_const_mul]  calc    ∫ x in s, ‖G x‖ ^ 2 ∂μ = ∫ x in s, η x ^ 2 * ‖G x‖ ^ 2 ∂μ := hleft_eq    _ ≤ ∫ x in t, η x ^ 2 * ‖G x‖ ^ 2 ∂μ := hleft_mono    _ ≤ C_coeff * ∫ x in t, ζ x ^ 2 * |v x| ^ 2 ∂μ := h_weighted    _ ≤ C_coeff * ∫ x in t, C_grad ^ 2 * |v x| ^ 2 ∂μ := by      gcongr    _ = C_coeff * C_grad ^ 2 * ∫ x in t, |v x| ^ 2 ∂μ := by      rw [hconst_mul]      ring