fix: remove unused arguments from theorem statements (#44)

* fix: remove unused arguments from theorem statements

Remove unused arguments from:
- theorem_1_2: unused Group.FG instance
- theorem_1_8: unused _hK parameter
- theorem_4_4: unused _hK parameter

These are placeholder theorem statements with incomplete proofs.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <[email protected]>

* fix

---------

Co-authored-by: Claude <[email protected]>
Co-authored-by: Yaël Yanis Dillies <[email protected]>

Author: 3 people

LeanCamCombi/GrowthInGroups/Lecture1.lean

@@ -44,6 +44,7 @@ def HasPolynomialGrowth : Prop :=
 /-- **Gromov's theorem**.
 
 A group has polynomial growth iff it's virtually nilpotent. -/
+@[nolint unusedArguments]
 lemma theorem_1_2 [Group.FG G] : HasPolynomialGrowth G ↔ IsVirtuallyNilpotent G := showcased
 
 lemma fact_1_3 [Fintype G] (hn : X ^ n = univ) : log (card G) / log #X ≤ n := by
@@ -74,7 +75,7 @@ lemma proposition_1_7 :
         ∃ a : Fin 10000000 → SL(2, ℝ), (X : Set SL(2, ℝ)) ⊆ ⋃ i, a i • A := showcased
 
 /-- The **Breuillard-Green-Tao theorem**. -/
-lemma theorem_1_8 (_hK : 0 ≤ K) :
+lemma theorem_1_8 :
     ∃ C > 0, ∀ {G} [Group G] [DecidableEq G] (A : Finset G) (_hA : σₘ[A] ≤ K),
       ∃ (N : Subgroup G) (D : Subgroup N) (_hD : D.Normal),
         upperCentralSeries (N⧸ D) C = ⊤ ∧ ((↑) '' (D : Set N) : Set G) ⊆ (A / A) ^ 4 ∧

LeanCamCombi/GrowthInGroups/Lecture4.lean

@@ -30,7 +30,7 @@ lemma corollary_4_3 (K C₀ : ℝ) :
         #F ≤ C ∧ A ⊆ F * Z := sorry
 
 /-- The **Breuillard-Green-Tao theorem**. -/
-theorem theorem_4_4 (_hK : 0 ≤ K) :
+theorem theorem_4_4 :
     ∃ C > 0, ∀ {G} [Group G] [DecidableEq G] (A : Set G) (_hA : IsApproximateSubgroup K A),
       ∃ (H : Subgroup G) (N : Subgroup H) (_hD : N.Normal) (F : Finset G),
         upperCentralSeries (H ⧸ N) C = ⊤ ∧ ((↑) '' (N : Set H) : Set G) ⊆ (A / A) ^ 4 ∧