diff --git a/Mathlib/Analysis/SpecificLimits/Basic.lean b/Mathlib/Analysis/SpecificLimits/Basic.lean
index fc946981f97cbc..6262996fb06eb4 100644
--- a/Mathlib/Analysis/SpecificLimits/Basic.lean
+++ b/Mathlib/Analysis/SpecificLimits/Basic.lean
@@ -460,8 +460,7 @@ then `f` is a Cauchy sequence. -/
 theorem cauchySeq_of_edist_le_geometric : CauchySeq f := by
   refine cauchySeq_of_edist_le_of_tsum_ne_top _ hu ?_
   rw [ENNReal.tsum_mul_left, ENNReal.tsum_geometric]
-  have := (tsub_pos_iff_lt.2 hr).ne'
-  finiteness
+  finiteness [(tsub_pos_iff_lt.2 hr).ne']
 
 include hu in
 /-- If `edist (f n) (f (n+1))` is bounded by `C * r^n`, then the distance from
diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
index d2ac1ffd61353f..b3685de32a539b 100644
--- a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
+++ b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
@@ -198,8 +198,7 @@ theorem eLpNorm'_const' [IsFiniteMeasure μ] (c : F) (hc_ne_zero : c ≠ 0) (hq_
     rw [← ENNReal.rpow_mul]
     suffices hp_cancel : q * (1 / q) = 1 by rw [hp_cancel, ENNReal.rpow_one]
     rw [one_div, mul_inv_cancel₀ hq_ne_zero]
-  · have : ‖c‖ₑ ≠ 0 := by simp [hc_ne_zero]
-    finiteness
+  · finiteness [show ‖c‖ₑ ≠ 0 by simp [hc_ne_zero]]
 
 theorem eLpNormEssSup_const (c : ε) (hμ : μ ≠ 0) : eLpNormEssSup (fun _ : α => c) μ = ‖c‖ₑ := by
   rw [eLpNormEssSup_eq_essSup_enorm, essSup_const _ hμ]
diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean
index 07bc68d1df6cd1..fe49f7193efda9 100644
--- a/Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean
+++ b/Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean
@@ -271,9 +271,7 @@ theorem MemLp.of_bilin {p q r : ℝ≥0∞} {f : α → E} {g : α → F} (b : E
     MemLp (fun x ↦ b (f x) (g x)) r μ := by
   refine ⟨h, ?_⟩
   apply (eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm hf.1 hg.1 b c hb (hpqr := hpqr)).trans_lt
-  have := hf.2
-  have := hg.2
-  finiteness
+  finiteness [hf.2, hg.2]
 
 end Bilinear
 
diff --git a/Mathlib/MeasureTheory/Integral/Average.lean b/Mathlib/MeasureTheory/Integral/Average.lean
index f5a57be2a96eab..2d29b2474a0c84 100644
--- a/Mathlib/MeasureTheory/Integral/Average.lean
+++ b/Mathlib/MeasureTheory/Integral/Average.lean
@@ -151,8 +151,7 @@ theorem laverage_lt_top (hf : ∫⁻ x, f x ∂μ ≠ ∞) : ⨍⁻ x, f x ∂μ
   obtain rfl | hμ := eq_or_ne μ 0
   · simp
   · rw [laverage_eq]
-    have := measure_univ_ne_zero.2 hμ
-    finiteness
+    finiteness [measure_univ_ne_zero.2 hμ]
 
 theorem setLAverage_lt_top : ∫⁻ x in s, f x ∂μ ≠ ∞ → ⨍⁻ x in s, f x ∂μ < ∞ :=
   laverage_lt_top
diff --git a/Mathlib/MeasureTheory/Integral/SetToL1.lean b/Mathlib/MeasureTheory/Integral/SetToL1.lean
index 1fbafdd96b78ce..1954747ef56b2d 100644
--- a/Mathlib/MeasureTheory/Integral/SetToL1.lean
+++ b/Mathlib/MeasureTheory/Integral/SetToL1.lean
@@ -93,8 +93,7 @@ theorem norm_eq_sum_mul (f : α →₁ₛ[μ] G) :
   · intro x _
     by_cases hx0 : x = 0
     · rw [hx0]; simp
-    · have := SimpleFunc.measure_preimage_lt_top_of_integrable _ (SimpleFunc.integrable f) hx0
-      finiteness
+    · finiteness [SimpleFunc.measure_preimage_lt_top_of_integrable _ (SimpleFunc.integrable f) hx0]
 
 section SetToL1S
 
diff --git a/Mathlib/Tactic/Finiteness.lean b/Mathlib/Tactic/Finiteness.lean
index 17964b44379994..b786345bcb9e85 100644
--- a/Mathlib/Tactic/Finiteness.lean
+++ b/Mathlib/Tactic/Finiteness.lean
@@ -20,13 +20,14 @@ set.
 
 Standard `aesop` syntax applies. Namely one can write
 * `finiteness (add unfold [def1, def2])` to make `finiteness` unfold `def1`, `def2`
-* `finiteness?` for the tactic to show what proof it found
-* etc
 * Note that `finiteness` disables `simp`, so `finiteness (add simp [lemma1, lemma2])` does not do
   anything more than a bare `finiteness`.
 
-We also provide `finiteness_nonterminal` as a version of `finiteness` that doesn't have to close the
-goal.
+One can pass additional expressions as local hypotheses: `finiteness [c]` is equivalent to
+`have := c; finiteness`. (This can be combined with the aesop syntax above.)
+
+* `finiteness?` (supporting the same syntax) shows the proof that `finiteness` found
+* `finiteness_nonterminal` is a version of `finiteness` that doesn't have to close the goal.
 
 Note to users: when tagging a lemma for finiteness, prefer tagging a lemma with `≠ ⊤`.
 Aesop can deduce `< ∞` from `≠ ∞` safely (`Ne.lt_top` is a safe rule), but not conversely
@@ -47,30 +48,49 @@ attribute [aesop (rule_sets := [finiteness]) safe -50] assumption intros
 set_option linter.unusedTactic false in
 add_aesop_rules safe tactic (rule_sets := [finiteness]) (by positivity)
 
-/-- Tactic to solve goals of the form `*** < ∞` and (equivalently) `*** ≠ ∞` in the extended
-nonnegative reals (`ℝ≥0∞`). -/
-macro (name := finiteness) "finiteness" c:Aesop.tactic_clause* : tactic =>
-`(tactic|
+/-- `finiteness` proves goals of the form `*** < ∞` and (equivalently) `*** ≠ ∞` in the extended
+nonnegative reals (`ℝ≥0∞`). Supports passing additional expressions as local hypotheses.
+
+* `finiteness?` additionally shows the proof that `finiteness` found
+* `finiteness_nonterminal` is a version of `finiteness` that may (but doesn't have to) close the
+  goal.
+-/
+syntax (name := finiteness) "finiteness" Aesop.tactic_clause* (ppSpace "[" term,* "]")? : tactic
+
+macro_rules
+| `(tactic | finiteness $c:Aesop.tactic_clause*) => `(tactic|
   aesop $c*
     (config := { introsTransparency? := some .reducible, terminal := true, enableSimp := false })
     (rule_sets := [$(Lean.mkIdent `finiteness):ident, -default, -builtin]))
+| `(tactic| finiteness $c:Aesop.tactic_clause* [$h,*]) =>
+  `(tactic| · ($[have := $h];*); finiteness $c*)
+
+@[tactic_alt finiteness]
+syntax (name := finiteness?) "finiteness?" Aesop.tactic_clause* (ppSpace "[" term,* "]")? : tactic
 
-/-- Tactic to solve goals of the form `*** < ∞` and (equivalently) `*** ≠ ∞` in the extended
-nonnegative reals (`ℝ≥0∞`). -/
-macro (name := finiteness?) "finiteness?" c:Aesop.tactic_clause* : tactic =>
+macro_rules
+| `(tactic | finiteness? $c:Aesop.tactic_clause*) =>
 `(tactic|
   aesop? $c*
     (config := { introsTransparency? := some .reducible, terminal := true, enableSimp := false })
     (rule_sets := [$(Lean.mkIdent `finiteness):ident, -default, -builtin]))
+| `(tactic| finiteness? $c:Aesop.tactic_clause* [$h,*]) =>
+  `(tactic| · ($[have := $h];*); finiteness? $c*)
+
+
+@[tactic_alt finiteness]
+syntax (name := finiteness_nonterminal)
+"finiteness_nonterminal" Aesop.tactic_clause* (ppSpace "[" term,* "]")? : tactic
 
-/-- Tactic to solve goals of the form `*** < ∞` and (equivalently) `*** ≠ ∞` in the extended
-nonnegative reals (`ℝ≥0∞`). -/
-macro (name := finiteness_nonterminal) "finiteness_nonterminal" c:Aesop.tactic_clause* : tactic =>
+macro_rules
+| `(tactic | finiteness_nonterminal $c:Aesop.tactic_clause*) =>
 `(tactic|
   aesop $c*
     (config := { introsTransparency? := some .reducible, terminal := false, enableSimp := false,
                  warnOnNonterminal := false  })
     (rule_sets := [$(Lean.mkIdent `finiteness):ident, -default, -builtin]))
+| `(tactic| finiteness_nonterminal $c:Aesop.tactic_clause* [$h,*]) =>
+  `(tactic| · ($[have := $h];*); finiteness_nonterminal $c*)
 
 /-!
  We register `finiteness` with the `hint` tactic.
diff --git a/MathlibTest/finiteness.lean b/MathlibTest/finiteness.lean
index d03f370c69f67b..f97848c5d115b7 100644
--- a/MathlibTest/finiteness.lean
+++ b/MathlibTest/finiteness.lean
@@ -42,6 +42,48 @@ example {a : ℝ≥0∞} : 2 * a⁻¹ * a ≠ ∞ := by rw [mul_assoc]; finitene
 example {a : ℝ≥0∞} (ha : a ≠ ∞) : max a 37 ≠ ∞ := by finiteness
 example {a b : ℝ≥0∞} (ha : a ≠ ∞) (hb : b ≠ ∞) : max a b < ∞ := by finiteness
 
+-- Basic tests for `finiteness?`
+/--
+info: Try this:
+
+  [apply]     apply max_ne_top
+    · exact ha
+    · apply ENNReal.ofNat_ne_top
+-/
+#guard_msgs in
+example {a : ℝ≥0∞} (ha : a ≠ ∞) : max a 37 ≠ ∞ := by finiteness?
+
+-- Also test supplying additional expressions.
+/--
+info: Try this:
+
+  [apply]     rename_i this
+    apply Ne.lt_top
+    exact this
+-/
+#guard_msgs in
+example {a b : ℝ≥0∞} (ha : a ≠ ∞) (hb : b ≠ ∞) : max a b < ∞ := by finiteness? [max_ne_top ha hb]
+
+section
+
+attribute [-aesop] max_ne_top
+-- now finiteness fails to close the goal
+axiom silentSorry {α} : α
+example {a b : ℝ≥0∞} (_ha : a ≠ ∞) (_hb : b ≠ ∞) : max a b < ∞ := by
+  fail_if_success finiteness
+  exact silentSorry
+
+-- but adding it as an expression works
+example {a b : ℝ≥0∞} (ha : a ≠ ∞) (hb : b ≠ ∞) : max a b < ∞ := by finiteness [max_ne_top ha hb]
+
+-- as does adding max_ne_top again via an aesop clause
+example {a b : ℝ≥0∞} (ha : a ≠ ∞) (hb : b ≠ ∞) : max a b < ∞ := by finiteness (add safe max_ne_top)
+
+end
+
+-- The attribute removal was confined to the previous section: this test confirms it.
+example {a b : ℝ≥0∞} (_ha : a ≠ ∞) (_hb : b ≠ ∞) : max a b < ∞ := by finiteness
+
 /--
 Test that `finiteness_nonterminal` makes progress but does not fail on not
 closing the goal.
@@ -50,6 +92,9 @@ example {a : ℝ≥0∞} (ha : a = 0) : a + 3 < ∞ := by finiteness_nonterminal
 
 example (a : ℝ) : (ENNReal.ofReal (1 + a ^ 2))⁻¹ < ∞ := by finiteness
 
+-- `finiteness_nonterminal` is allowed to close goals. (Though that is a code smell.)
+example (a : ℝ) : (ENNReal.ofReal (1 + a ^ 2))⁻¹ < ∞ := by finiteness_nonterminal
+
 example {α : Type*} (f : α → ℕ) : ∀ i, (f i : ℝ≥0∞) ≠ ∞ := by finiteness
 
 example {α} {_ : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] (s : Set α) : μ s ≠ ∞ := by