From 92b444a352373ec040d94c3b94680503ea886121 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Thu, 29 Feb 2024 09:37:35 +0000
Subject: [PATCH] chore(Data/Finset/Lattice): better docs for `gcongr` lemmas
 (#11067)

I accidentally merged #9520
before pushing these changes requested by @Vierkantor
---
 Mathlib/Data/Finset/Lattice.lean   | 8 ++++++--
 Mathlib/Order/Filter/AtTopBot.lean | 2 +-
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Data/Finset/Lattice.lean b/Mathlib/Data/Finset/Lattice.lean
index e50b4d69ba5cc6..0d7385b8204a14 100644
--- a/Mathlib/Data/Finset/Lattice.lean
+++ b/Mathlib/Data/Finset/Lattice.lean
@@ -966,7 +966,9 @@ theorem sup'_mono {s₁ s₂ : Finset β} (h : s₁ ⊆ s₂) (h₁ : s₁.Nonem
     s₁.sup' h₁ f ≤ s₂.sup' (h₁.mono h) f :=
   Finset.sup'_le h₁ _ (fun _ hb => le_sup' _ (h hb))
 
-/-- A version of `Finset.sup'_mono` acceptable for `@[gcongr]`. -/
+/-- A version of `Finset.sup'_mono` acceptable for `@[gcongr]`.
+Instead of deducing `s₂.Nonempty` from `s₁.Nonempty` and `s₁ ⊆ s₂`,
+this version takes it as an argument. -/
 @[gcongr]
 lemma _root_.GCongr.finset_sup'_le {s₁ s₂ : Finset β} (h : s₁ ⊆ s₂)
     {h₁ : s₁.Nonempty} {h₂ : s₂.Nonempty} : s₁.sup' h₁ f ≤ s₂.sup' h₂ f :=
@@ -1143,7 +1145,9 @@ theorem inf'_mono {s₁ s₂ : Finset β} (h : s₁ ⊆ s₂) (h₁ : s₁.Nonem
     s₂.inf' (h₁.mono h) f ≤ s₁.inf' h₁ f :=
   Finset.le_inf' h₁ _ (fun _ hb => inf'_le _ (h hb))
 
-/-- A version of `Finset.inf'_mono` acceptable for `@[gcongr]`. -/
+/-- A version of `Finset.inf'_mono` acceptable for `@[gcongr]`.
+Instead of deducing `s₂.Nonempty` from `s₁.Nonempty` and `s₁ ⊆ s₂`,
+this version takes it as an argument. -/
 @[gcongr]
 lemma _root_.GCongr.finset_inf'_mono {s₁ s₂ : Finset β} (h : s₁ ⊆ s₂)
     {h₁ : s₁.Nonempty} {h₂ : s₂.Nonempty} : s₂.inf' h₂ f ≤ s₁.inf' h₁ f :=
diff --git a/Mathlib/Order/Filter/AtTopBot.lean b/Mathlib/Order/Filter/AtTopBot.lean
index adefd5f2c382f4..e8ae22cdeb0947 100644
--- a/Mathlib/Order/Filter/AtTopBot.lean
+++ b/Mathlib/Order/Filter/AtTopBot.lean
@@ -1907,7 +1907,7 @@ theorem exists_seq_monotone_tendsto_atTop_atTop (α : Type*) [SemilatticeSup α]
   obtain ⟨ys, h⟩ := exists_seq_tendsto (atTop : Filter α)
   let xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) Finset.nonempty_range_succ ys
   have h_mono : Monotone xs := fun i j hij ↦ by
-    simp only -- Need to unfold `xs` and do alpha reduction, otherwise `gcongr` fails
+    simp only [xs] -- Need to unfold `xs` and do alpha reduction, otherwise `gcongr` fails
     gcongr
   refine ⟨xs, h_mono, tendsto_atTop_mono (fun n ↦ Finset.le_sup' _ ?_) h⟩
   simp