diff --git a/RealRooted/Tactic/Examples/FiniteSymbol.lean b/RealRooted/Tactic/Examples/FiniteSymbol.lean
index c60802d16..81d30db84 100644
--- a/RealRooted/Tactic/Examples/FiniteSymbol.lean
+++ b/RealRooted/Tactic/Examples/FiniteSymbol.lean
@@ -29,5 +29,21 @@ example {sigma tau : Type*} [Fintype sigma]
     symbol_stable := hSymbol,
     input_stable := hf
 
+example {sigma tau : Type*} [Fintype sigma]
+    (T : MvPolynomial.degreeOfLE sigma ℂ (fun _ => 1) →ₗ[ℂ]
+      MvPolynomial tau ℂ)
+    (S : MvPolynomial.degreeOfLE sigma ℂ (fun _ => 1) →ₗ[ℂ]
+      MvPolynomial tau ℂ)
+    (_hSymbolS : MvUpperHalfPlaneStable
+      (MvPolynomial.algebraicSymbol (fun _ : sigma => 1) S))
+    (hSymbol : MvUpperHalfPlaneStable
+      (MvPolynomial.algebraicSymbol (fun _ : sigma => 1) T))
+    (g : MvPolynomial.degreeOfLE sigma ℂ (fun _ => 1))
+    (_hg : MvUpperHalfPlaneStable g.1)
+    (f : MvPolynomial.degreeOfLE sigma ℂ (fun _ => 1))
+    (hf : MvUpperHalfPlaneStable f.1) :
+    MvUpperHalfPlaneStableOrZero (T f) := by
+  rr_finite_symbol_stable_or_zero_auto
+
 end Tactic
 end RealRooted
diff --git a/RealRooted/Tactic/FiniteSymbol.lean b/RealRooted/Tactic/FiniteSymbol.lean
index ce424cc45..c11e52ba7 100644
--- a/RealRooted/Tactic/FiniteSymbol.lean
+++ b/RealRooted/Tactic/FiniteSymbol.lean
@@ -3,8 +3,8 @@ import RealRooted.BorceaBranden.FiniteSymbolPreserver
 /-!
 # Finite-symbol stable-or-zero tactic frontend
 
-Thin certificate-driven wrappers around the proved multiaffine finite-symbol
-stability theorem.
+Thin explicit and automatic wrappers around the proved multiaffine
+finite-symbol stability theorem.
 -/
 
 namespace RealRooted
@@ -24,6 +24,9 @@ syntax (name := rr_finite_symbol_stable_or_zero_inferred)
     "input_stable" ":=" term :
   tactic
 
+syntax (name := rr_finite_symbol_stable_or_zero_auto)
+  "rr_finite_symbol_stable_or_zero_auto" : tactic
+
 macro_rules
   | `(tactic|
       rr_finite_symbol_stable_or_zero using
@@ -41,6 +44,11 @@ macro_rules
       `(tactic|
         exact RealRooted.BorceaBranden.finiteSymbol_preserves_stability
           _ $hSymbol _ $hf)
+  | `(tactic| rr_finite_symbol_stable_or_zero_auto) =>
+      `(tactic|
+        rr_finite_symbol_stable_or_zero using
+          symbol_stable := (by assumption),
+          input_stable := (by assumption))
 
 end Tactic
 end RealRooted