Slashaction generators

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