diff --git a/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean b/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
index 6a0c16f4bea90..f3107d2d11cbf 100644
--- a/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
+++ b/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
@@ -38,15 +38,13 @@ the case of an ordered commutative multiplicative monoid. -/
 @[gcongr]
 lemma prod_le_prod (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i) :
     ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i := by
-  induction' s using Finset.cons_induction with a s has ih h
-  · simp
-  · simp only [prod_cons]
+  induction s using Finset.cons_induction with
+  | empty => simp
+  | cons a s has ih =>
+    simp only [prod_cons, forall_mem_cons] at h0 h1 ⊢
     have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
-    apply mul_le_mul
-    · exact h1 a (mem_cons_self a s)
-    · refine ih (fun x H ↦ h0 _ ?_) (fun x H ↦ h1 _ ?_) <;> exact subset_cons _ H
-    · apply prod_nonneg fun x H ↦ h0 x (subset_cons _ H)
-    · apply le_trans (h0 a (mem_cons_self a s)) (h1 a (mem_cons_self a s))
+    gcongr
+    exacts [prod_nonneg h0.2, h0.1.trans h1.1, h1.1, ih h0.2 h1.2]
 
 /-- If each `f i`, `i ∈ s` belongs to `[0, 1]`, then their product is less than or equal to one.
 See also `Finset.prod_le_one'` for the case of an ordered commutative multiplicative monoid. -/
@@ -112,11 +110,7 @@ lemma prod_add_prod_le {i : ι} {f g h : ι → R} (hi : i ∈ s) (h2i : g i + h
   simp_rw [prod_eq_mul_prod_diff_singleton hi]
   refine le_trans ?_ (mul_le_mul_of_nonneg_right h2i ?_)
   · rw [right_distrib]
-    refine add_le_add ?_ ?_ <;>
-    · refine mul_le_mul_of_nonneg_left ?_ ?_
-      · refine prod_le_prod ?_ ?_ <;> simp +contextual [*]
-      · try apply_assumption
-        try assumption
+    gcongr with j hj <;> aesop
   · apply prod_nonneg
     simp only [and_imp, mem_sdiff, mem_singleton]
     exact fun j hj hji ↦ le_trans (hg j hj) (hgf j hj hji)
@@ -151,14 +145,10 @@ variable [CanonicallyOrderedCommSemiring R] {f g h : ι → R} {s : Finset ι} {
 lemma prod_add_prod_le' (hi : i ∈ s) (h2i : g i + h i ≤ f i) (hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j)
     (hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j) : ((∏ i ∈ s, g i) + ∏ i ∈ s, h i) ≤ ∏ i ∈ s, f i := by
   classical
-    simp_rw [prod_eq_mul_prod_diff_singleton hi]
-    refine le_trans ?_ (mul_le_mul_right' h2i _)
-    rw [right_distrib]
-    apply add_le_add <;> apply mul_le_mul_left' <;> apply prod_le_prod' <;>
-            simp only [and_imp, mem_sdiff, mem_singleton] <;>
-          intros <;>
-        apply_assumption <;>
-      assumption
+  simp_rw [prod_eq_mul_prod_diff_singleton hi]
+  refine le_trans ?_ (mul_le_mul_right' h2i _)
+  rw [right_distrib]
+  gcongr with j hj j hj <;> simp_all
 
 end CanonicallyOrderedCommSemiring