feat: @[gcongr] for indicator_le_indicator_of_subset (#31847)

This PR tags `indicator_le_indicator_of_subset` and `indicator_le_indicator_apply_of_subset` with `gcongr`, and uses this to golf some proofs.

It may be possible to improve `gcongr` in the future so that we only need to tag one of the two lemmas with `gcongr`.

Author: JovanGerb

Mathlib/Algebra/Order/Archimedean/IndicatorCard.lean

@@ -53,8 +53,8 @@ lemma infinite_iff_tendsto_sum_indicator_atTop {R : Type*}
     obtain ⟨n', hn'⟩ := exists_lt_nsmul h n
     obtain ⟨t, t_s, t_card⟩ := hs.exists_subset_card_eq n'
     obtain ⟨m, hm⟩ := t.bddAbove
-    refine ⟨m + 1, hn'.le.trans ?_⟩
-    apply (sum_le_sum fun i _ ↦ (indicator_le_indicator_of_subset t_s (fun _ ↦ h.le)) i).trans_eq'
+    use m + 1
+    grw [hn', ← t_s]
     have h : t ⊆ Finset.range (m + 1) := by
       intro i i_t
       rw [Finset.mem_range]

Mathlib/Algebra/Order/Group/Indicator.lean

@@ -117,14 +117,14 @@ lemma mulIndicator_le_mulIndicator (h : f a ≤ g a) : mulIndicator s f a ≤ mu
 lemma mulIndicator_mono (h : f ≤ g) : s.mulIndicator f ≤ s.mulIndicator g :=
   fun _ ↦ mulIndicator_le_mulIndicator (h _)
 
-@[to_additive]
+@[to_additive (attr := gcongr)]
 lemma mulIndicator_le_mulIndicator_apply_of_subset (h : s ⊆ t) (hf : 1 ≤ f a) :
     mulIndicator s f a ≤ mulIndicator t f a :=
   mulIndicator_apply_le'
     (fun ha ↦ le_mulIndicator_apply (fun _ ↦ le_rfl) fun hat ↦ (hat <| h ha).elim) fun _ ↦
     one_le_mulIndicator_apply fun _ ↦ hf
 
-@[to_additive]
+@[to_additive (attr := gcongr)]
 lemma mulIndicator_le_mulIndicator_of_subset (h : s ⊆ t) (hf : 1 ≤ f) :
     mulIndicator s f ≤ mulIndicator t f :=
   fun _ ↦ mulIndicator_le_mulIndicator_apply_of_subset h (hf _)
@@ -186,8 +186,9 @@ lemma iSup_mulIndicator {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] {
     {s : ι → Set α} (h1 : (⊥ : M) = 1) (hf : Monotone f) (hs : Monotone s) :
     ⨆ i, (s i).mulIndicator (f i) = (⋃ i, s i).mulIndicator (⨆ i, f i) := by
   simp only [le_antisymm_iff, iSup_le_iff]
-  refine ⟨fun i ↦ (mulIndicator_mono (le_iSup _ _)).trans (mulIndicator_le_mulIndicator_of_subset
-    (subset_iUnion _ _) (fun _ ↦ by simp [← h1])), fun a ↦ ?_⟩
+  refine ⟨fun i ↦ ?_, fun a ↦ ?_⟩
+  · grw [← le_iSup f i, ← subset_iUnion s i]
+    intro; simp [← h1]
   by_cases ha : a ∈ ⋃ i, s i
   · obtain ⟨i, hi⟩ : ∃ i, a ∈ s i := by simpa using ha
     rw [mulIndicator_of_mem ha, iSup_apply, iSup_apply]

Mathlib/Analysis/Normed/Group/Indicator.lean

@@ -34,7 +34,7 @@ lemma enorm_indicator_eq_indicator_enorm :
 theorem enorm_indicator_le_of_subset (h : s ⊆ t) (f : α → ε) (a : α) :
     ‖indicator s f a‖ₑ ≤ ‖indicator t f a‖ₑ := by
   simp only [enorm_indicator_eq_indicator_enorm]
-  apply indicator_le_indicator_of_subset ‹_› (zero_le _)
+  grw [h]
 
 theorem indicator_enorm_le_enorm_self : indicator s (fun a => ‖f a‖ₑ) a ≤ ‖f a‖ₑ :=
   indicator_le_self' (fun _ _ ↦ zero_le _) a
@@ -59,7 +59,7 @@ theorem nnnorm_indicator_eq_indicator_nnnorm :
 theorem norm_indicator_le_of_subset (h : s ⊆ t) (f : α → E) (a : α) :
     ‖indicator s f a‖ ≤ ‖indicator t f a‖ := by
   simp only [norm_indicator_eq_indicator_norm]
-  exact indicator_le_indicator_of_subset ‹_› (fun _ => norm_nonneg _) _
+  grw [h]
 
 theorem indicator_norm_le_norm_self : indicator s (fun a => ‖f a‖) a ≤ ‖f a‖ :=
   indicator_le_self' (fun _ _ => norm_nonneg _) a

Mathlib/MeasureTheory/Function/SimpleFunc.lean

@@ -1429,7 +1429,7 @@ lemma Measurable.ennreal_sigmaFinite_induction [SigmaFinite μ] {motive : (α 
   refine Measurable.ennreal_induction (fun c s hs ↦ ?_) add iSup hf
   convert iSup (f := fun n ↦ (s ∩ spanningSets μ n).indicator fun _ ↦ c)
     (fun n ↦ measurable_const.indicator (hs.inter (measurableSet_spanningSets ..)))
-    (fun m n hmn a ↦ Set.indicator_le_indicator_of_subset (by gcongr) (by simp) _)
+    (fun m n hmn a ↦ by dsimp; grw [hmn])
     (fun n ↦ indicator _ (hs.inter (measurableSet_spanningSets ..))
       (measure_inter_lt_top_of_right_ne_top (measure_spanningSets_lt_top ..).ne)) with a
   simp [← Set.indicator_iUnion_apply (M := ℝ≥0∞) rfl, ← Set.inter_iUnion]

Mathlib/MeasureTheory/Function/UniformIntegrable.lean

@@ -311,10 +311,8 @@ theorem MemLp.eLpNorm_indicator_norm_ge_pos_le (hf : MemLp f p μ) (hmeas : Stro
   obtain ⟨M, hM⟩ := hf.eLpNorm_indicator_norm_ge_le hmeas hε
   refine
     ⟨max M 1, lt_of_lt_of_le zero_lt_one (le_max_right _ _), le_trans (eLpNorm_mono fun x => ?_) hM⟩
-  rw [norm_indicator_eq_indicator_norm, norm_indicator_eq_indicator_norm]
-  refine Set.indicator_le_indicator_of_subset (fun x hx => ?_) (fun x => norm_nonneg (f x)) x
-  rw [Set.mem_setOf_eq] at hx -- removing the `rw` breaks the proof!
-  exact (max_le_iff.1 hx).1
+  simp only [norm_indicator_eq_indicator_norm]
+  grw [← le_max_left]
 
 end
 
@@ -689,8 +687,7 @@ theorem unifIntegrable_of (hp : 1 ≤ p) (hp' : p ≠ ∞) {f : ι → α → β
       rwa [Set.mem_setOf, hx] at hfx
   refine ⟨max C 1, lt_max_of_lt_right one_pos, fun i => le_trans (eLpNorm_mono fun x => ?_) (hCg i)⟩
   rw [norm_indicator_eq_indicator_norm, norm_indicator_eq_indicator_norm]
-  exact Set.indicator_le_indicator_of_subset
-    (fun x hx => Set.mem_setOf_eq ▸ le_trans (le_max_left _ _) hx) (fun _ => norm_nonneg _) _
+  grw [← le_max_left]
 
 end UnifIntegrable
 

Mathlib/MeasureTheory/Integral/Bochner/VitaliCaratheodory.lean

@@ -129,8 +129,8 @@ theorem SimpleFunc.exists_le_lowerSemicontinuous_lintegral_ge (f : α →ₛ ℝ
     refine ⟨Set.indicator u fun _ => c,
             fun x => ?_, u_open.lowerSemicontinuous_indicator (zero_le _), ?_⟩
     · simp only [SimpleFunc.coe_const, SimpleFunc.const_zero, SimpleFunc.coe_zero,
-        Set.piecewise_eq_indicator, SimpleFunc.coe_piecewise]
-      exact Set.indicator_le_indicator_of_subset su (fun x => zero_le _) _
+        Set.piecewise_eq_indicator, SimpleFunc.coe_piecewise, ← Function.const_def]
+      grw [su]
     · suffices (c : ℝ≥0∞) * μ u ≤ c * μ s + ε by
         classical
         simpa only [ENNReal.coe_indicator, u_open.measurableSet, lintegral_indicator,
@@ -340,8 +340,8 @@ theorem SimpleFunc.exists_upperSemicontinuous_le_lintegral_le (f : α →ₛ ℝ
       ⟨Set.indicator F fun _ => c, fun x => ?_, F_closed.upperSemicontinuous_indicator (zero_le _),
         ?_⟩
     · simp only [SimpleFunc.coe_const, SimpleFunc.const_zero, SimpleFunc.coe_zero,
-        Set.piecewise_eq_indicator, SimpleFunc.coe_piecewise]
-      exact Set.indicator_le_indicator_of_subset Fs (fun x => zero_le _) _
+        Set.piecewise_eq_indicator, SimpleFunc.coe_piecewise, ← Function.const_def]
+      grw [Fs]
     · suffices (c : ℝ≥0∞) * μ s ≤ c * μ F + ε by
         classical
         simpa only [hs, F_closed.measurableSet, SimpleFunc.coe_const, Function.const_apply,

Mathlib/MeasureTheory/Integral/DominatedConvergence.lean

@@ -197,7 +197,7 @@ theorem _root_.Antitone.tendsto_setIntegral (hsm : ∀ i, MeasurableSet (s i)) (
     exact hfi.norm
   · simp_rw [norm_indicator_eq_indicator_norm]
     refine fun n => Eventually.of_forall fun x => ?_
-    exact indicator_le_indicator_of_subset (h_anti (zero_le n)) (fun a => norm_nonneg _) _
+    grw [(h_anti (zero_le n)).subset]
   · filter_upwards [] with a using le_trans (h_anti.tendsto_indicator _ _ _) (pure_le_nhds _)
 
 end TendstoMono

Mathlib/MeasureTheory/Integral/Indicator.lean

@@ -53,7 +53,7 @@ lemma tendsto_measure_of_ae_tendsto_indicator {μ : Measure α} (A_mble : Measur
           (Eventually.of_forall ?_) ?_ ?_ ?_
   · exact fun i ↦ Measurable.indicator measurable_const (As_mble i)
   · filter_upwards [As_le_B] with i hi
-    exact Eventually.of_forall (fun x ↦ indicator_le_indicator_of_subset hi (by simp) x)
+    exact Eventually.of_forall fun x ↦ by grw [hi]
   · rwa [← lintegral_indicator_one B_mble] at B_finmeas
   · simpa only [Pi.one_def, tendsto_indicator_const_apply_iff_eventually] using h_lim
 

Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

@@ -355,8 +355,8 @@ private theorem lintegral_tendsto_of_monotone_of_nat {φ : ℕ → Set α} (hφ
     Tendsto (fun i => ∫⁻ x in φ i, f x ∂μ) atTop (𝓝 <| ∫⁻ x, f x ∂μ) :=
   let F n := (φ n).indicator f
   have key₁ : ∀ n, AEMeasurable (F n) μ := fun n => hfm.indicator (hφ.measurableSet n)
-  have key₂ : ∀ᵐ x : α ∂μ, Monotone fun n => F n x := ae_of_all _ fun x _i _j hij =>
-    indicator_le_indicator_of_subset (hmono hij) (fun x => zero_le <| f x) x
+  have key₂ : ∀ᵐ x : α ∂μ, Monotone fun n => F n x := ae_of_all _ fun x _i _j hij => by
+    dsimp [F]; grw [(hmono hij).subset]
   have key₃ : ∀ᵐ x : α ∂μ, Tendsto (fun n => F n x) atTop (𝓝 (f x)) := hφ.ae_tendsto_indicator f
   (lintegral_tendsto_of_tendsto_of_monotone key₁ key₂ key₃).congr fun n =>
     lintegral_indicator (hφ.measurableSet n) _

Mathlib/MeasureTheory/OuterMeasure/Operations.lean

@@ -244,7 +244,7 @@ instance instLawfulFunctor : LawfulFunctor OuterMeasure := by constructor <;> in
 def dirac (a : α) : OuterMeasure α where
   measureOf s := indicator s (fun _ => 1) a
   empty := by simp
-  mono {_ _} h := indicator_le_indicator_of_subset h (fun _ => zero_le _) a
+  mono {_ _} h := by grw [h]
   iUnion_nat s _ := calc
     indicator (⋃ n, s n) 1 a = ⨆ n, indicator (s n) 1 a :=
       indicator_iUnion_apply (M := ℝ≥0∞) rfl _ _ _