Slashaction generators

theorem slashaction_generators'    (f : ℍ → ℂ) {G : Subgroup SL(2, ℤ)} (s : Set G) (hG : ⊤ = Subgroup.closure s) (k : ℤ) :    (∀ γ : G, f ∣[k] γ.1 = f) ↔ (∀ γ ∈ s, f ∣[k] γ.1 = f) := by  constructor <;> intro h  · intro γ _    exact h _  · intro ⟨γ, hγ⟩    -- key idea: this lemma allows induction on the "words" of the group    apply Subgroup.closure_induction (G := G) (p := fun γ _ ↦ f ∣[k] γ.1 = f) (k := s) ?_ ?_    · intro _ _ _ _ hf₁ hf₂      rw [@Subgroup.coe_mul]      rw [SlashAction.slash_mul, hf₁, hf₂]    · intro x _ hf      rw [← hf, ← SlashAction.slash_mul]      simp [hf]    · simp [← hG]    · intro γ hγ      exact h γ hγ    · exact SlashAction.slash_one k f