Exists pow smul integer mem span

theorem exists_pow_smul_integer_mem_span {ι : Type*} [Finite ι] (b : Module.Basis ι K L)    {ϖ : 𝒪[K]} (hϖ : Irreducible ϖ) :    ∃ m : ℕ, ∀ x ∈ 𝒪[L], (ϖ : K) ^ m • x ∈ Submodule.span 𝒪[K] (Set.range b) := by  have := Fintype.ofFinite ι  let : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K  let : IsUniformAddGroup K := isUniformAddGroup_of_addCommGroup (G := K)  let := rankOneOfIoo K default  let : NontriviallyNormedField K := Valued.toNontriviallyNormedField (L := K) _  have hcont : Continuous (b.equivFun : L → ι → K) :=    IsModuleTopology.continuous_of_linearMap (b.equivFun : L →ₗ[K] ι → K)  have hcpt : IsCompact (𝒪[L] : Set L) :=    IsNonarchimedeanLocalField.isCompact_closedBall L 1  obtain ⟨C, hC⟩ :=    isBounded_iff_forall_norm_le.mp (hcpt.image hcont).isBounded  simp only [Module.Basis.equivFun_apply, Set.mem_image, SetLike.mem_coe, forall_exists_index,    and_imp, forall_apply_eq_imp_iff₂] at hC  obtain ⟨m, hm⟩ : ∃ m : ℕ, ‖(ϖ : K)‖ ^ m < (max C 1)⁻¹ :=    exists_pow_lt_of_lt_one (by positivity) <| Valued.toNormedField.norm_lt_one_iff.mpr      (Valuation.integer.v_irreducible_lt_one hϖ)  refine ⟨m, fun x hx ↦ (b.mem_span_iff_repr_mem _ _).2 fun i ↦    ⟨⟨(ϖ : K) ^ m * b.repr x i, Valuation.mem_integer_iff _ _|>.2 <|    Valued.toNormedField.norm_le_one_iff.1 ?_⟩, by simp⟩⟩  grw [norm_mul, norm_pow, ((norm_le_pi_norm _ i).trans (hC _ hx)).trans (le_max_left _ 1),    hm, inv_mul_cancel₀ (by positivity)]