diff --git a/Mathlib/Dynamics/SymbolicDynamics/Basic.lean b/Mathlib/Dynamics/SymbolicDynamics/Basic.lean
index 7a1b4e3ff47d53..b2c2a08c4deaf2 100644
--- a/Mathlib/Dynamics/SymbolicDynamics/Basic.lean
+++ b/Mathlib/Dynamics/SymbolicDynamics/Basic.lean
@@ -579,7 +579,7 @@ end DefSubshiftByForbidden
 
 section Language
 
-variable {A : Type*} [Fintype A] [Inhabited A]
+variable {A : Type*} [Inhabited A]
 variable {G : Type*}
 
 /-- Patterns with support exactly `U` form a finite set. -/
@@ -616,6 +616,14 @@ This is the set of all finite patterns obtained by restricting some configuratio
 def LanguageOn (X : Set (G → A)) (U : Finset G) : Set (Pattern A G) :=
   { p | ∃ x ∈ X, Pattern.fromConfig x U = p }
 
+/-- Considering two sets of configurations `X` and `Y` such that `X ⊆ Y`, the language
+of `X` on (finite) shape `U` is included in the language of `Y` on shape `U`. -/
+lemma isMonotone_LanguageOn {X Y : Set (G → A)} (h : X ⊆ Y) (U : Finset G) :
+    LanguageOn X U ⊆ LanguageOn Y U := by
+  intro p hp
+  rcases hp with ⟨x, hxX, rfl⟩
+  exact ⟨x, h hxX, rfl⟩
+
 /-- The language of a subshift `Y` on a finite shape `U`. -/
 def MulSubshift.languageOn {A G} [TopologicalSpace A] [Inhabited A] [Monoid G]
     (Y : MulSubshift A G) (U : Finset G) : Set (Pattern A G) :=