  We present the design and implementation of the Small Scale Reflection proof
methodology and tactic language (a.k.a. SSR) for the Lean 4 proof assistant.
Like its Coq predecessor SSReflect, our Lean 4 implementation, dubbed LeanSSR,
provides powerful rewriting principles and means for effective management of
hypotheses in the proof context. Unlike SSReflect for Coq, LeanSSR does not
require explicit switching between the logical and symbolic representation of a
goal, allowing for even more concise proof scripts that seamlessly combine
deduction steps with proofs by computation.
  In this paper, we first provide a gentle introduction to the principles of
structuring mechanised proofs using LeanSSR. Next, we show how the native
support for metaprogramming in Lean 4 makes it possible to develop LeanSSR
entirely within the proof assistant, greatly improving the overall experience
of both tactic implementers and proof engineers. Finally, we demonstrate the
utility of LeanSSR by conducting two case studies: (a) porting a collection of
Coq lemmas about sequences from the widely used Mathematical Components library
and (b) reimplementing proofs in the finite set library of Lean's mathlib4.
Both case studies show significant reduction in proof sizes.
